/**CHeaderFile***************************************************************** FileName [bmcInt.h] PackageName [bmc] Synopsis [Internal header declarations.] Author [Mohammad Awedh] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] Revision [$Id: bmcInt.h,v 1.52 2010/04/09 23:50:57 fabio Exp $] ******************************************************************************/ #ifndef _BMCINT #define _BMCINT /*---------------------------------------------------------------------------*/ /* Nested includes */ /*---------------------------------------------------------------------------*/ #include "cmd.h" #include "bmc.h" #include "baig.h" #include "ltl.h" #include "ltlInt.h" #include "sat.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ typedef enum { BmcVerbosityNone_c, BmcVerbositySome_c, BmcVerbosityMax_c } Bmc_VerbosityLevel; /* Specify the status of a property */ typedef enum { BmcPropertyUndecided_c, BmcPropertyPassed_c, BmcPropertyFailed_c } Bmc_PropertyStatus; /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /**Struct********************************************************************** Synopsis [A struct for keeping the command line options for bmc command.] ******************************************************************************/ struct BmcOption { FILE *ltlFile; /* contains the LTL formulae */ FILE *fairFile; /* contains the fairness constraints */ char *cnfFileName; /* File contains CNF clauses if -o option is used */ Bmc_VerbosityLevel verbosityLevel; int minK; int maxK; int step; int timeOutPeriod; long startTime; /* initial CPU time */ int rewriting; int dbgLevel; FILE * dbgOut; int inductiveStep; boolean printInputs; /* The folowing two pointers are used to point to the two tmp files that will be created in /tmp/ before calling the SAT solver. */ char *satInFile; char *satOutFile; boolean satSolverError; /* equal to TRUE if an error occurs in calling SAT solver */ int incremental; int cnfPrefix; int earlyTermination; /* Use early termination check */ int satSolver; /* 0 CirCUs 1 cusp */ int clauses; /* representation of clauses 0 CirCUs circuit 1 CirCUs CNF 2 CNF */ int encoding; /* encoding of LTL formula 0 Original encoding 1 Fixpoint 2 SNF 3 SNF-Fixpoint */ }; /**Struct********************************************************************** Synopsis [A struct to store CNF clauses] ******************************************************************************/ struct BmcCnfClauses { array_t *clauseArray; /* array to store CNF clauses. Each clause is terminated by the value 0. */ st_table *cnfIndexTable; /* store the index of the key (name, state) in the clauseArray. It uses to return the index of of already generated clauses. */ array_t *freezedKeys; /* When CNF is freezed, any new added key to cnfIndexTable will also be added to this array. When CNF restored, these keys in this array will be deleted from cnfIndexTable */ int nextIndex; /* holds the index of the next entry in clauseArray. */ int noOfClauses; /* total number of clauses */ int cnfGlobalIndex; /* the index of next variable. */ boolean emptyClause; /* equal TRUE if the last added clause was an empty clause. */ boolean freezed; /* TRUE if CNF is freezed */ }; /**Struct********************************************************************** Synopsis [A struct to store CNF state. When CNF is freezed, a new state is created. This structure keeps the value of the varaible in the current state.] ******************************************************************************/ struct BmcCnfStates { int nextIndex; int noOfClauses; int cnfGlobalIndex; int freezedKeySize; boolean emptyClause; boolean freezed; }; /**Struct********************************************************************** Synopsis [A struct to store the check for termination status. For more information, please refer to \cite{Awedh04}] ******************************************************************************/ struct BmcCheckForTermination { int k; /* The length of the path to be checked*/ int m; /* The vlaues of m and n in the termination criterion*/ int n; int checkLevel; /* Which predicate to be checked. */ Ltl_Automaton_t *automaton; int action; /* Next action */ bdd_t *internalConstraints; /* The OR of internal constraints*/ Ctlsp_Formula_t *externalConstraints; /* The OR of external constraints*/ }; /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Function prototypes */ /*---------------------------------------------------------------------------*/ EXTERN int BmcAutLtlCheckForTermination(Ntk_Network_t *network, array_t *constraintArray, BmcCheckForTermination_t *terminationStatus, st_table *nodeToMvfAigTable, st_table *CoiTable, BmcOption_t *options); EXTERN void BmcAutCnfGenerateClausesForPath(Ltl_Automaton_t *automaton, int fromState, int toState, int initialState, BmcCnfClauses_t *cnfClauses); EXTERN void BmcAutCnfGenerateClausesForSimpleCompositePath(Ntk_Network_t *network, Ltl_Automaton_t *automaton, int fromState, int toState, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable); EXTERN void BmcCnfNoLoopToAnyPreviouseCompositeStates(Ntk_Network_t *network, Ltl_Automaton_t *automaton, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable); EXTERN void BmcAutEncodeAutomatonStates(Ntk_Network_t *network, Ltl_Automaton_t *automaton); EXTERN void BmcAutEncodeAutomatonStates2(Ntk_Network_t *network, Ltl_Automaton_t *automaton); EXTERN void BmcAutEncodeAutomatonStates3(Ntk_Network_t *network, Ltl_Automaton_t *automaton); EXTERN void BmcAutBuildTransitionRelation(Ntk_Network_t *network, Ltl_Automaton_t *automaton); EXTERN mdd_t * BmcAutBuildMddForPropositionalFormula(Ntk_Network_t *network, Ltl_Automaton_t *automaton, Ctlsp_Formula_t *formula); EXTERN int BmcAutGenerateCnfForBddOffSet(bdd_t *function, int current, int next, BmcCnfClauses_t *cnfClauses, st_table *nsPsTable); EXTERN BmcCheckForTermination_t * BmcAutTerminationAlloc(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray); EXTERN Ltl_Automaton_t * BmcAutLtlToAutomaton(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula); EXTERN void BmcAutTerminationFree(BmcCheckForTermination_t *result); EXTERN int BmcBddSat(Ntk_Network_t *network, array_t *formulaArray, BmcOption_t *options); EXTERN Bmc_PropertyStatus BmcBddSatCheckLtlFormula(Ntk_Network_t *network, mdd_t *initialStates, mdd_t *targetStates, BmcOption_t *options, st_table *CoiTable); EXTERN void BmcLtlVerifyProp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options); EXTERN int BmcLtlCheckInductiveInvariant(Ntk_Network_t *network, bAigEdge_t property, BmcOption_t *options, st_table *CoiTable); EXTERN void BmcLtlVerifyGp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options); EXTERN void BmcLtlVerifyFp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options); EXTERN void BmcLtlVerifyFGp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options); EXTERN void BmcLtlVerifyUnitDepth(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options); EXTERN void BmcLtlVerifyGeneralLtl(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, array_t *constraintArray, BmcOption_t *options); EXTERN int BmcGenerateCnfForLtl(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, int i, int k, int l, BmcCnfClauses_t *cnfClauses); EXTERN void BmcLtlCheckSafety(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, BmcOption_t *options, st_table *CoiTable); EXTERN void BmcCirCUsLtlVerifyProp(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options); EXTERN int BmcCirCUsLtlCheckInductiveInvariant(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, BmcOption_t *options, st_table *CoiTable); EXTERN void BmcCirCUsLtlVerifyGp(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options); EXTERN void BmcCirCUsLtlVerifyFp(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options); EXTERN bAigEdge_t BmcCirCUsGenerateLogicForLtl(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, int loop); EXTERN bAigEdge_t BmcCirCUsGenerateLogicForLtlSNF(Ntk_Network_t *network, array_t *formulaArray, int fromState, int toState, int loop); EXTERN bAigEdge_t BmcCirCUsGenerateLogicForLtlFixPoint(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, array_t *loopArray); EXTERN bAigEdge_t BmcCirCUsGenerateLogicForLtlFixPointRecursive(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, int translation, array_t *loopArray, st_table *ltl2AigTable); EXTERN void BmcCirCUsLtlVerifyFGp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *coiTable, BmcOption_t *options); EXTERN void BmcCirCUsLtlVerifyGeneralLtl(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, array_t *constraintArray, BmcOption_t *options, int snf); EXTERN void BmcCirCUsLtlVerifyGeneralLtlFixPoint(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, array_t *constraintArray, BmcOption_t *options); EXTERN void BmcCirCUsLtlCheckSafety(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, BmcOption_t *options, st_table *coiTable); EXTERN bAigEdge_t BmcCirCUsConnectFromStateToState(Ntk_Network_t *network, int from, int to, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int withInitialState); EXTERN bAigEdge_t BmcCirCUsSimlePathConstraint(Ntk_Network_t *network, int fromState, int toState, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int withInitialState); EXTERN bAigEdge_t BmcCirCUsGenerateSimplePath(Ntk_Network_t *network, int from, int to, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int withInitialState); EXTERN void BmcCirCUsPrintCounterExample(Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable, int length, array_t *loop_arr, BmcOption_t *options, int withInitialState); EXTERN void BmcCirCUsPrintCounterExampleAiger(Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable, int length, array_t *loop_arr, BmcOption_t *options, int withInitialState); EXTERN bAigEdge_t BmcCirCUsCreatebAigOfPropFormula(Ntk_Network_t *network, bAig_Manager_t *manager, int bound, Ctlsp_Formula_t *ltl, int withInitialState); EXTERN bAigEdge_t BmcCirCUsCreatebAigOfPropFormulaOriginal(Ntk_Network_t *network, bAig_Manager_t *manager, Ctlsp_Formula_t *ltl); EXTERN satInterface_t * BmcCirCUsInterface(bAig_Manager_t *manager, Ntk_Network_t *network, bAigEdge_t object, array_t *auxObjectArray, BmcOption_t *bmcOption, satInterface_t *interface); EXTERN satInterface_t * BmcCirCUsInterfaceWithObjArr(bAig_Manager_t *manager, Ntk_Network_t *network, array_t *objectArray, array_t *auxObjectArray, BmcOption_t *bmcOption, satInterface_t *interface); EXTERN satManager_t * BmcCirCUsCreateManager(Ntk_Network_t *network); EXTERN st_table * BmcCirCUsGetCoiIndexTable(Ntk_Network_t *network, st_table *coiTable); EXTERN void BmcCirCUsAutLtlCheckTerminalAutomaton(Ntk_Network_t *network, bAig_Manager_t *aigManager, st_table *nodeToMvfAigTable, BmcCheckForTermination_t *terminationStatus, st_table *coiIndexTable, BmcOption_t *options); EXTERN bAigEdge_t BmcCirCUsBdd2Aig(Ntk_Network_t *network, bdd_t *function, int current, int next, Ltl_Automaton_t *automaton, bAig_Manager_t *aigManager, int withInitialState); EXTERN bAigEdge_t BmcCirCUsAutCreateAigForPath(Ntk_Network_t *network, bAig_Manager_t *aigManager, Ltl_Automaton_t *automaton, int fromState, int toState, int initialState); EXTERN bAigEdge_t BmcCirCUsAutCreateAigForSimplePath(Ntk_Network_t *network, bAig_Manager_t *aigManager, Ltl_Automaton_t *automaton, int fromState, int toState, int initialState); EXTERN bAigEdge_t BmcCirCUsCreateAigForSimpleCompositePath(Ntk_Network_t *network, bAig_Manager_t *aigManager, Ltl_Automaton_t *automaton, int fromState, int toState, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int initialState); EXTERN void BmcCirCUsAutLtlCheckForTermination(Ntk_Network_t *network, bAig_Manager_t *aigManager, st_table *nodeToMvfAigTable, BmcCheckForTermination_t *terminationStatus, st_table *coiIndexTable, BmcOption_t *options); EXTERN char * BmcCirCUsCallCirCUs(BmcOption_t *options); EXTERN char * BmcCirCUsCallCusp(BmcOption_t *options); EXTERN BmcOption_t * BmcOptionAlloc(void); EXTERN void BmcOptionFree(BmcOption_t *result); EXTERN char * BmcCreateTmpFile(void); EXTERN int CommandBddSat(Hrc_Manager_t ** hmgr, int argc, char ** argv); EXTERN mdd_t * BmcFsmEvaluateX(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd); EXTERN mdd_t * BmcComputeCloseCube(mdd_t *aSet, mdd_t *target, int *dist, array_t *Support, mdd_manager *mddMgr); EXTERN mAigEdge_t BmcCreateMaigOfInitialStates(Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *CoiTable); EXTERN mAigEdge_t BmcCreateMaigOfPropFormula(Ntk_Network_t *network, mAig_Manager_t *manager, Ctlsp_Formula_t *formula); EXTERN mdd_t * BmcCreateMddOfSafetyProperty(Fsm_Fsm_t *fsm, Ctlsp_Formula_t *formula); EXTERN int BmcGenerateCnfFormulaForAigFunction(bAig_Manager_t *manager, bAigEdge_t node, int k, BmcCnfClauses_t *cnfClauses); EXTERN int BmcGenerateCnfFormulaForBdd(bdd_t *bddFunction, int k, BmcCnfClauses_t *cnfClauses); EXTERN int BmcGenerateCnfFormulaForBddOffSet(bdd_t *bddFunction, int k, BmcCnfClauses_t *cnfClauses); EXTERN int BmcGenerateCnfForAigFunction(bAig_Manager_t *manager, Ntk_Network_t *network, bAigEdge_t node, int k, BmcCnfClauses_t *cnfClauses); EXTERN void BmcGenerateClausesFromStateTostate(bAig_Manager_t *manager, bAigEdge_t *fromAigArray, bAigEdge_t *toAigArray, int mvfSize, int fromState, int toState, BmcCnfClauses_t *cnfClauses, int outIndex); EXTERN void BmcWriteClauses(mAig_Manager_t *maigManager, FILE *cnfFile, BmcCnfClauses_t *cnfClauses, BmcOption_t *options); EXTERN array_t * BmcCheckSAT(BmcOption_t *options); EXTERN array_t * BmcCallCirCUs(BmcOption_t *options); EXTERN array_t * BmcCallCusp(BmcOption_t *options); EXTERN void BmcPrintCounterExample(Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *result, int length, st_table *CoiTable, BmcOption_t *options, array_t *loopClause); EXTERN void BmcPrintCounterExampleAiger(Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *result, int length, st_table *CoiTable, BmcOption_t *options, array_t *loopClause); EXTERN void BmcAutPrintCounterExample(Ntk_Network_t *network, Ltl_Automaton_t *automaton, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *result, int length, st_table *CoiTable, BmcOption_t *options, array_t *loopClause); EXTERN void BmcCnfGenerateClausesForPath(Ntk_Network_t *network, int from, int to, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable); EXTERN void BmcCnfGenerateClausesForLoopFreePath(Ntk_Network_t *network, int fromState, int toState, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable); EXTERN void BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates(Ntk_Network_t *network, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable); EXTERN void BmcCnfGenerateClausesForLoopToAnyPreviouseStates(Ntk_Network_t *network, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable); EXTERN void BmcCnfGenerateClausesFromStateToState(Ntk_Network_t *network, int from, int to, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable, int loop); EXTERN void BmcCnfGenerateClausesForAND(int a, int b, int c, BmcCnfClauses_t *cnfClauses); EXTERN void BmcCnfGenerateClausesForOR(int a, int b, int c, BmcCnfClauses_t *cnfClauses); EXTERN BmcCnfClauses_t * BmcCnfClausesAlloc(void); EXTERN void BmcCnfClausesFree(BmcCnfClauses_t *cnfClauses); EXTERN BmcCnfStates_t * BmcCnfClausesFreeze(BmcCnfClauses_t * cnfClauses); EXTERN void BmcCnfClausesUnFreeze(BmcCnfClauses_t *cnfClauses, BmcCnfStates_t *state); EXTERN void BmcCnfClausesRestore(BmcCnfClauses_t *cnfClauses, BmcCnfStates_t *state); EXTERN void BmcCnfInsertClause(BmcCnfClauses_t *cnfClauses, array_t *clause); EXTERN void BmcAddEmptyClause(BmcCnfClauses_t *cnfClauses); EXTERN int BmcCnfReadOrInsertNode(BmcCnfClauses_t *cnfClauses, nameType_t *nodeName, int state, int *nodeIndex); EXTERN void BmcGetCoiForLtlFormula(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable); EXTERN void BmcGetCoiForLtlFormulaRecursive(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable, st_table *visited); EXTERN void BmcGetCoiForNtkNode(Ntk_Node_t *node, st_table *CoiTable, st_table *visited); EXTERN mdd_t * BmcModelCheckAtomicFormula(Fsm_Fsm_t *modelFsm, Ctlsp_Formula_t *ctlFormula); EXTERN array_t * BmcReadFairnessConstraints(FILE *fp); EXTERN int BmcGetCnfVarIndexForBddNode(bdd_manager *bddManager, bdd_node *node, int state, BmcCnfClauses_t *cnfClauses); EXTERN void BmcRestoreAssertion(bAig_Manager_t *manager, satManager_t *cm); /**AutomaticEnd***************************************************************/ #endif /* _BMCINT */