source: vis_dev/vis-2.3/src/bmc/bmcInt.h @ 41

Last change on this file since 41 was 41, checked in by cecile, 12 years ago

new command generate cnf from network
File size: 18.7 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [bmcInt.h]
4
5  PackageName [bmc]
6
7  Synopsis    [Internal header declarations.]
8
9  Author      [Mohammad Awedh]
10
11  Copyright   [This file was created at the University of Colorado at Boulder.
12  The University of Colorado at Boulder makes no warranty about the suitability
13  of this software for any purpose.  It is presented on an AS IS basis.]
14
15  Revision    [$Id: bmcInt.h,v 1.52 2010/04/09 23:50:57 fabio Exp $]
16
17******************************************************************************/
18
19#ifndef _BMCINT
20#define _BMCINT
21
22/*---------------------------------------------------------------------------*/
23/* Nested includes                                                           */
24/*---------------------------------------------------------------------------*/
25
26#include "cmd.h"
27#include "bmc.h"
28#include "baig.h"
29#include "ltl.h"
30#include "ltlInt.h"
31#include "sat.h"
32
33/*---------------------------------------------------------------------------*/
34/* Constant declarations                                                     */
35/*---------------------------------------------------------------------------*/
36
37
38/*---------------------------------------------------------------------------*/
39/* Type declarations                                                         */
40/*---------------------------------------------------------------------------*/
41
42typedef enum {
43  BmcVerbosityNone_c,
44  BmcVerbositySome_c,
45  BmcVerbosityMax_c
46} Bmc_VerbosityLevel;
47
48/*
49  Specify the status of a property
50 */
51
52typedef enum {
53  BmcPropertyUndecided_c,
54  BmcPropertyPassed_c,
55  BmcPropertyFailed_c
56} Bmc_PropertyStatus;
57
58
59
60/*---------------------------------------------------------------------------*/
61/* Structure declarations                                                    */
62/*---------------------------------------------------------------------------*/
63
64/**Struct**********************************************************************
65
66  Synopsis    [A struct for keeping the command line options for bmc command.]
67
68******************************************************************************/
69struct BmcOption {
70  FILE               *ltlFile;  /* contains the LTL formulae */
71  FILE               *fairFile; /* contains the fairness constraints */
72  char               *cnfFileName; /* File contains CNF clauses if -o option
73                                      is used */
74  Bmc_VerbosityLevel verbosityLevel;
75  int                minK;
76  int                maxK;
77  int                step;
78  int                timeOutPeriod;
79  long               startTime; /* initial CPU time */
80  int                rewriting;
81  int                dbgLevel;
82  FILE *             dbgOut;
83  int                inductiveStep;
84  boolean            printInputs;
85  /* The folowing two pointers are used to point to the two tmp files that will
86     be created in /tmp/ before calling the SAT solver. */
87  char               *satInFile; 
88  char               *satOutFile;
89  boolean            satSolverError;  /* equal to TRUE if an error occurs in calling SAT solver */
90  int                incremental;
91  int                cnfPrefix;
92  int                earlyTermination; /* Use early termination check */
93  int                satSolver;   /*
94                                    0 CirCUs
95                                    1 cusp
96                                  */
97  int                clauses;   /* representation of clauses
98                                   0 CirCUs circuit
99                                   1 CirCUs CNF
100                                   2 CNF
101                                */
102  int                encoding;   /* encoding of LTL formula
103                                   0 Original encoding
104                                   1 Fixpoint
105                                   2 SNF
106                                   3 SNF-Fixpoint
107                                */
108};
109
110/**Struct**********************************************************************
111
112  Synopsis    [A struct to store CNF clauses]
113
114******************************************************************************/
115struct BmcCnfClauses {
116  array_t   *clauseArray;    /* array to store CNF clauses. Each clause is
117                                terminated by the value 0.                        */
118  st_table  *cnfIndexTable;  /* store the index of the key (name, state) in
119                                the clauseArray. It uses to return the index of
120                                of already generated clauses.                     */
121  array_t   *freezedKeys;    /* When CNF is freezed, any new added key to
122                                cnfIndexTable will also be added to this
123                                array. When CNF restored, these keys in this
124                                array will be deleted from cnfIndexTable          */
125  int       nextIndex;      /* holds the index of the next entry in clauseArray.  */
126  int       noOfClauses;    /* total number of clauses */
127  int       cnfGlobalIndex; /* the index of next variable.                        */
128  boolean   emptyClause;    /* equal TRUE if the last added clause was an empty
129                               clause.                                           */
130  boolean   freezed;        /* TRUE if CNF is freezed */
131};
132
133/**Struct**********************************************************************
134
135  Synopsis    [A struct to store CNF state. When CNF is freezed, a new state
136               is created. This structure keeps the value of the varaible in
137               the current state.]
138
139******************************************************************************/
140struct BmcCnfStates {
141  int       nextIndex;     
142  int       noOfClauses;   
143  int       cnfGlobalIndex;
144  int       freezedKeySize;
145  boolean   emptyClause;
146  boolean   freezed;
147};
148
149/**Struct**********************************************************************
150
151  Synopsis [A struct to store the check for termination status. For more
152  information, please refer to \cite{Awedh04}]
153
154******************************************************************************/
155struct BmcCheckForTermination {
156  int       k;   /* The length of the path to be checked*/
157  int       m;   /* The vlaues of m and n in the termination criterion*/
158  int       n;
159  int       checkLevel; /* Which predicate to be checked. */
160  Ltl_Automaton_t *automaton;
161  int       action; /* Next action */
162  bdd_t           *internalConstraints; /* The OR of internal constraints*/
163  Ctlsp_Formula_t *externalConstraints;  /* The OR of external constraints*/
164};
165
166
167/**AutomaticStart*************************************************************/
168
169/*---------------------------------------------------------------------------*/
170/* Function prototypes                                                       */
171/*---------------------------------------------------------------------------*/
172
173EXTERN int BmcAutLtlCheckForTermination(Ntk_Network_t *network, array_t *constraintArray, BmcCheckForTermination_t *terminationStatus, st_table *nodeToMvfAigTable, st_table *CoiTable, BmcOption_t *options);
174EXTERN void BmcAutCnfGenerateClausesForPath(Ltl_Automaton_t *automaton, int fromState, int toState, int initialState, BmcCnfClauses_t *cnfClauses);
175EXTERN 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);
176EXTERN void BmcCnfNoLoopToAnyPreviouseCompositeStates(Ntk_Network_t *network, Ltl_Automaton_t *automaton, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable);
177EXTERN void BmcAutEncodeAutomatonStates(Ntk_Network_t *network, Ltl_Automaton_t *automaton);
178EXTERN void BmcAutEncodeAutomatonStates2(Ntk_Network_t *network, Ltl_Automaton_t *automaton);
179EXTERN void BmcAutEncodeAutomatonStates3(Ntk_Network_t *network, Ltl_Automaton_t *automaton);
180EXTERN void BmcAutBuildTransitionRelation(Ntk_Network_t *network, Ltl_Automaton_t *automaton);
181EXTERN mdd_t * BmcAutBuildMddForPropositionalFormula(Ntk_Network_t *network, Ltl_Automaton_t *automaton, Ctlsp_Formula_t *formula);
182EXTERN int BmcAutGenerateCnfForBddOffSet(bdd_t *function, int current, int next, BmcCnfClauses_t *cnfClauses, st_table *nsPsTable);
183EXTERN BmcCheckForTermination_t * BmcAutTerminationAlloc(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray);
184EXTERN Ltl_Automaton_t * BmcAutLtlToAutomaton(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula);
185EXTERN void BmcAutTerminationFree(BmcCheckForTermination_t *result);
186EXTERN int BmcBddSat(Ntk_Network_t *network, array_t *formulaArray, BmcOption_t *savons);
187EXTERN Bmc_PropertyStatus BmcBddSatCheckLtlFormula(Ntk_Network_t *network, mdd_t *initialStates, mdd_t *targetStates, BmcOption_t *options, st_table *CoiTable);
188EXTERN void BmcLtlVerifyProp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options);
189EXTERN int BmcLtlCheckInductiveInvariant(Ntk_Network_t *network, bAigEdge_t property, BmcOption_t *options, st_table *CoiTable);
190EXTERN void BmcLtlVerifyGp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options);
191EXTERN void BmcLtlVerifyFp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options);
192EXTERN void BmcLtlVerifyFGp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options);
193EXTERN void BmcLtlVerifyUnitDepth(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options);
194EXTERN void BmcLtlVerifyGeneralLtl(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, array_t *constraintArray, BmcOption_t *options);
195EXTERN int BmcGenerateCnfForLtl(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, int i, int k, int l, BmcCnfClauses_t *cnfClauses);
196EXTERN void BmcLtlCheckSafety(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, BmcOption_t *options, st_table *CoiTable);
197EXTERN void BmcCirCUsLtlVerifyProp(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options);
198EXTERN int BmcCirCUsLtlCheckInductiveInvariant(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, BmcOption_t *options, st_table *CoiTable);
199EXTERN void BmcCirCUsLtlVerifyGp(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options);
200EXTERN void BmcCirCUsLtlVerifyFp(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, BmcOption_t *options);
201EXTERN bAigEdge_t BmcCirCUsGenerateLogicForLtl(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, int loop);
202EXTERN bAigEdge_t BmcCirCUsGenerateLogicForLtlSNF(Ntk_Network_t *network, array_t *formulaArray, int fromState, int toState, int loop);
203EXTERN bAigEdge_t BmcCirCUsGenerateLogicForLtlFixPoint(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, array_t *loopArray);
204EXTERN bAigEdge_t BmcCirCUsGenerateLogicForLtlFixPointRecursive(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, int from, int to, int translation, array_t *loopArray, st_table *ltl2AigTable);
205EXTERN void BmcCirCUsLtlVerifyFGp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *coiTable, BmcOption_t *options);
206EXTERN void BmcCirCUsLtlVerifyGeneralLtl(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, array_t *constraintArray, BmcOption_t *options, int snf);
207EXTERN void BmcCirCUsLtlVerifyGeneralLtlFixPoint(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, st_table *coiTable, array_t *constraintArray, BmcOption_t *options);
208EXTERN void BmcCirCUsLtlCheckSafety(Ntk_Network_t *network, Ctlsp_Formula_t *ltl, BmcOption_t *options, st_table *coiTable);
209EXTERN bAigEdge_t BmcCirCUsConnectFromStateToState(Ntk_Network_t *network, int from, int to, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int withInitialState);
210EXTERN bAigEdge_t BmcCirCUsSimlePathConstraint(Ntk_Network_t *network, int fromState, int toState, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int withInitialState);
211EXTERN bAigEdge_t BmcCirCUsGenerateSimplePath(Ntk_Network_t *network, int from, int to, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int withInitialState);
212EXTERN void BmcCirCUsPrintCounterExample(Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable, int length, array_t *loop_arr, BmcOption_t *options, int withInitialState);
213EXTERN void BmcCirCUsPrintCounterExampleAiger(Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *coiTable, int length, array_t *loop_arr, BmcOption_t *options, int withInitialState);
214EXTERN bAigEdge_t BmcCirCUsCreatebAigOfPropFormula(Ntk_Network_t *network, bAig_Manager_t *manager, int bound, Ctlsp_Formula_t *ltl, int withInitialState);
215EXTERN bAigEdge_t BmcCirCUsCreatebAigOfPropFormulaOriginal(Ntk_Network_t *network, bAig_Manager_t *manager, Ctlsp_Formula_t *ltl);
216EXTERN satInterface_t * BmcCirCUsInterface(bAig_Manager_t *manager, Ntk_Network_t *network, bAigEdge_t object, array_t *auxObjectArray, BmcOption_t *bmcOption, satInterface_t *interface);
217EXTERN satInterface_t * BmcCirCUsInterfaceWithObjArr(bAig_Manager_t *manager, Ntk_Network_t *network, array_t *objectArray, array_t *auxObjectArray, BmcOption_t *bmcOption, satInterface_t *interface);
218EXTERN satManager_t * BmcCirCUsCreateManager(Ntk_Network_t *network);
219EXTERN st_table * BmcCirCUsGetCoiIndexTable(Ntk_Network_t *network, st_table *coiTable);
220EXTERN void BmcCirCUsAutLtlCheckTerminalAutomaton(Ntk_Network_t *network, bAig_Manager_t *aigManager, st_table *nodeToMvfAigTable, BmcCheckForTermination_t *terminationStatus, st_table *coiIndexTable, BmcOption_t *options);
221EXTERN bAigEdge_t BmcCirCUsBdd2Aig(Ntk_Network_t *network, bdd_t *function, int current, int next, Ltl_Automaton_t *automaton, bAig_Manager_t *aigManager, int withInitialState);
222EXTERN bAigEdge_t BmcCirCUsAutCreateAigForPath(Ntk_Network_t *network, bAig_Manager_t *aigManager, Ltl_Automaton_t *automaton, int fromState, int toState, int initialState);
223EXTERN bAigEdge_t BmcCirCUsAutCreateAigForSimplePath(Ntk_Network_t *network, bAig_Manager_t *aigManager, Ltl_Automaton_t *automaton, int fromState, int toState, int initialState);
224EXTERN 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);
225EXTERN void BmcCirCUsAutLtlCheckForTermination(Ntk_Network_t *network, bAig_Manager_t *aigManager, st_table *nodeToMvfAigTable, BmcCheckForTermination_t *terminationStatus, st_table *coiIndexTable, BmcOption_t *options);
226EXTERN char * BmcCirCUsCallCirCUs(BmcOption_t *options);
227EXTERN char * BmcCirCUsCallCusp(BmcOption_t *options);
228EXTERN BmcOption_t * BmcOptionAlloc(void);
229EXTERN void BmcOptionFree(BmcOption_t *result);
230EXTERN char * BmcCreateTmpFile(void);
231EXTERN int CommandBddSat(Hrc_Manager_t ** hmgr, int argc, char ** argv);
232EXTERN mdd_t * BmcFsmEvaluateX(Fsm_Fsm_t *modelFsm, mdd_t *targetMdd);
233EXTERN mdd_t * BmcComputeCloseCube(mdd_t *aSet, mdd_t *target, int *dist, array_t *Support, mdd_manager *mddMgr);
234EXTERN mAigEdge_t BmcCreateMaigOfInitialStates(Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *CoiTable);
235EXTERN mAigEdge_t BmcCreateMaigOfPropFormula(Ntk_Network_t *network, mAig_Manager_t *manager, Ctlsp_Formula_t *formula);
236EXTERN mdd_t * BmcCreateMddOfSafetyProperty(Fsm_Fsm_t *fsm, Ctlsp_Formula_t *formula);
237EXTERN int BmcGenerateCnfFormulaForAigFunction(bAig_Manager_t *manager, bAigEdge_t node, int k, BmcCnfClauses_t *cnfClauses);
238EXTERN int BmcGenerateCnfFormulaForBdd(bdd_t *bddFunction, int k, BmcCnfClauses_t *cnfClauses);
239EXTERN int BmcGenerateCnfFormulaForBddOffSet(bdd_t *bddFunction, int k, BmcCnfClauses_t *cnfClauses);
240EXTERN int BmcGenerateCnfForAigFunction(bAig_Manager_t *manager, Ntk_Network_t *network, bAigEdge_t node, int k, BmcCnfClauses_t *cnfClauses);
241EXTERN void BmcGenerateClausesFromStateTostate(bAig_Manager_t *manager, bAigEdge_t *fromAigArray, bAigEdge_t *toAigArray, int mvfSize, int fromState, int toState, BmcCnfClauses_t *cnfClauses, int outIndex);
242EXTERN void BmcWriteClauses(mAig_Manager_t *maigManager, FILE *cnfFile, BmcCnfClauses_t *cnfClauses, BmcOption_t *options);
243EXTERN array_t * BmcCheckSAT(BmcOption_t *options);
244EXTERN array_t * BmcCallCirCUs(BmcOption_t *options);
245EXTERN array_t * BmcCallCusp(BmcOption_t *options);
246EXTERN 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);
247EXTERN 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);
248EXTERN 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);
249EXTERN void BmcCnfGenerateClausesForPath(Ntk_Network_t *network, int from, int to, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable);
250EXTERN void BmcCnfGenerateClausesForLoopFreePath(Ntk_Network_t *network, int fromState, int toState, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable);
251EXTERN void BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates(Ntk_Network_t *network, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable);
252EXTERN void BmcCnfGenerateClausesForLoopToAnyPreviouseStates(Ntk_Network_t *network, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable);
253EXTERN void BmcCnfGenerateClausesFromStateToState(Ntk_Network_t *network, int from, int to, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable, int loop);
254EXTERN void BmcCnfGenerateClausesForAND(int a, int b, int c, BmcCnfClauses_t *cnfClauses);
255EXTERN void BmcCnfGenerateClausesForOR(int a, int b, int c, BmcCnfClauses_t *cnfClauses);
256EXTERN BmcCnfClauses_t * BmcCnfClausesAlloc(void);
257EXTERN void BmcCnfClausesFree(BmcCnfClauses_t *cnfClauses);
258EXTERN BmcCnfStates_t * BmcCnfClausesFreeze(BmcCnfClauses_t * cnfClauses);
259EXTERN void BmcCnfClausesUnFreeze(BmcCnfClauses_t *cnfClauses, BmcCnfStates_t *state);
260EXTERN void BmcCnfClausesRestore(BmcCnfClauses_t *cnfClauses, BmcCnfStates_t *state);
261EXTERN void BmcCnfInsertClause(BmcCnfClauses_t *cnfClauses, array_t *clause);
262EXTERN void BmcAddEmptyClause(BmcCnfClauses_t *cnfClauses);
263EXTERN int BmcCnfReadOrInsertNode(BmcCnfClauses_t *cnfClauses, nameType_t *nodeName, int state, int *nodeIndex);
264EXTERN void BmcGetCoiForLtlFormula(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable);
265EXTERN void BmcGetCoiForLtlFormulaRecursive(Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable, st_table *visited);
266EXTERN void BmcGetCoiForNtkNode(Ntk_Node_t *node, st_table *CoiTable, st_table *visited);
267EXTERN mdd_t * BmcModelCheckAtomicFormula(Fsm_Fsm_t *modelFsm, Ctlsp_Formula_t *ctlFormula);
268EXTERN array_t * BmcReadFairnessConstraints(FILE *fp);
269EXTERN int BmcGetCnfVarIndexForBddNode(bdd_manager *bddManager, bdd_node *node, int state, BmcCnfClauses_t *cnfClauses);
270EXTERN void BmcRestoreAssertion(bAig_Manager_t *manager, satManager_t *cm);
271
272/**AutomaticEnd***************************************************************/
273
274#endif /* _BMCINT */
Note: See TracBrowser for help on using the repository browser.