source: vis_dev/vis-2.3/src/debug/debugUtilities.c @ 99

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

add part of cex

File size: 6.7 KB
Line 
1#include "debug.h"
2void printNodeArray(array_t * nodeArray)
3{
4  int i;
5  Ntk_Node_t* node;
6  arrayForEachItem(Ntk_Node_t *, nodeArray, i, node){
7    printf("%s\n",Ntk_NodeReadName(node)); 
8  }
9
10
11}
12
13void printLatch(st_table* CoiTable)
14{
15// COI contents
16   printf("*** COI ***\n");
17   st_generator    *stGen;
18   Ntk_Node_t * latch;
19   st_foreach_item(CoiTable, stGen, &latch, NULL) {
20        printf("%s\n",Ntk_NodeReadName(latch)); 
21  }
22}
23
24void printStringArray(array_t * array)
25{
26 
27  int i;
28  char * data;
29  arrayForEachItem(char *, array, i, data)
30  {
31    printf("%s\n",data);
32  }
33} 
34void printIntArray(array_t * array)
35{
36 
37  int i;
38  int data;
39  arrayForEachItem(int, array, i, data)
40  {
41    printf("%d\n",data);
42  }
43} 
44st_table * generateAllLatches(Ntk_Network_t * ntk)
45{
46    st_table        *CoiTable = st_init_table(st_ptrcmp, st_ptrhash);
47        lsGen           gen ;
48        Ntk_Node_t              *node;
49
50        Ntk_NetworkForEachNode(ntk,gen, node){
51                if (Ntk_NodeTestIsLatch(node)){
52                        st_insert(CoiTable, (char *) node, Ntk_NodeReadName(node));
53                }
54        }
55        return CoiTable;
56
57}
58
59
60void mdd_GetState_Values(
61mdd_manager *mgr ,
62mdd_t *  top, 
63FILE  * f) 
64{
65  mdd_t * T;
66  mdd_t * E;
67  int    id;
68  array_t * val = array_alloc(int, 4); 
69  static int level;
70  char c = ' ' ;
71
72  level++;
73
74  id = bdd_top_var_id(top);
75
76  mvar_type mv = 
77array_fetch(mvar_type, mdd_ret_mvar_list((mgr)),(id));
78 // fprintf(f,"(");
79
80  // Pour le Then
81  T=bdd_then(top);
82 
83 //variable belongs to what we are looking for
84// if(strstr(mv.name,var_name) !=NULL)
85  if(bdd_is_tautology(T,1)){
86    //array_insert(type, array, position, object)
87    fprintf(f,"%s = 1 ",mv.name);
88    //c = '+';
89  } else
90    if(!bdd_is_tautology(T,0)){
91      fprintf(f,"%s = 1 * ",mv.name);
92      //mdd_FunctionPrint(mgr, T,f);
93     // c = '+';
94    }
95
96  mdd_free(T);
97 
98  //pour le Else
99  E=bdd_else(top);
100  if(bdd_is_tautology(E,0)){
101    goto fin;
102  }
103 
104  if(bdd_is_tautology(E,1)){
105    fprintf(f,"%c %s = 0",c, mv.name);
106    goto fin;
107  }
108 
109  fprintf(f,"%c %s = 0 * ",c, mv.name);
110  /*
111  mdd_FunctionPrint(mgr, E,f);
112  mdd_free(E);
113*/
114 fin:
115  fprintf(f,")");
116  level--;
117  return;
118}
119/**Function********************************************************************
120 
121  Synopsis    [Performs the sat call]
122
123  Description [Retrun the result of SAT call, avec positionnement des options]
124  SideEffects []
125
126  SeeAlso     []
127
128******************************************************************************/
129
130int Dbg_SatCheck(char * forceAssigName, char * cnfFileName,int verbose
131)
132{
133 satManager_t *cm;
134 cm = sat_InitManager(0);
135 cm->comment = ALLOC(char, 2);
136 cm->comment[0] = ' ';
137 cm->comment[1] = '\0';
138 cm->stdOut = stdout;
139 cm->stdErr = stderr;
140
141 
142  satOption_t  *satOption;
143  array_t      *result = NIL(array_t);
144  int          maxSize;
145
146  satOption = sat_InitOption();
147  satOption->verbose = 2;
148  //satOption->unsatCoreFileName = "Ucore.txt";
149  satOption->clauseDeletionHeuristic = 0;
150  //satOption->coreGeneration = 1 ;
151  //satOption->minimizeConflictClause = 1;
152  if(forceAssigName != NULL)
153    satOption->forcedAssignArr = sat_ReadForcedAssignment(forceAssigName);
154   cm->option = satOption;
155   cm->each = sat_InitStatistics();
156
157  cm->unitLits = sat_ArrayAlloc(16);
158  cm->pureLits = sat_ArrayAlloc(16);
159
160  maxSize = 1024 << 8;
161  cm->nodesArray = ALLOC(long, maxSize);
162  cm->maxNodesArraySize = maxSize;
163  cm->nodesArraySize = satNodeSize;
164
165  sat_AllocLiteralsDB(cm);
166
167   sat_ReadCNF(cm,cnfFileName);
168   sat_Main(cm);
169
170if(verbose){
171   if(cm->status == SAT_UNSAT) {
172    if(cm->option->forcedAssignArr)
173      fprintf(cm->stdOut, "%s UNSAT under given assignment\n",
174              cm->comment);
175    fprintf(cm->stdOut, "%s UNSATISFIABLE\n", cm->comment);
176    fflush(cm->stdOut);
177    sat_ReportStatistics(cm, cm->each);
178    sat_FreeManager(cm);
179  }
180  else if(cm->status == SAT_SAT) {
181    fprintf(cm->stdOut, "%s SATISFIABLE\n", cm->comment);
182    fflush(cm->stdOut);
183    sat_PrintSatisfyingAssignment(cm);
184    sat_ReportStatistics(cm, cm->each);
185    sat_FreeManager(cm);
186  }
187}
188return cm->status;
189}
190/**Function********************************************************************
191 
192  Synopsis    [Generate a CNF of the network]
193
194  Description [Generate the set of clauses of the unroll network for a given
195  length and for a given cone of influence]
196  SideEffects []
197
198  SeeAlso     []
199
200******************************************************************************/
201BmcCnfClauses_t*
202Dbg_GenerateCNF(Ntk_Network_t * network, 
203BmcOption_t * options,
204st_table  *CoiTable
205){
206st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
207BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
208/*
209 *nodeToMvfAigTable maps each node to its multi-function And/Inv graph
210 */
211nodeToMvfAigTable =
212(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
213assert(nodeToMvfAigTable != NIL(st_table));
214/*
215 * Create a clause database
216 */
217cnfClauses = BmcCnfClausesAlloc();
218/*
219 * Generate clauses for an initialized path of length k
220 */
221BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
222                         cnfClauses, nodeToMvfAigTable, CoiTable);
223return cnfClauses;
224
225}
226/**Function********************************************************************
227 
228  Synopsis    [Return the default value of a Node]
229
230  Description [Given a table of a node , return its default value if it exists
231  else -1   This function only work for binary gate with only one default
232  value.]
233  SideEffects []
234
235  SeeAlso     []
236
237******************************************************************************/
238int Dbg_GetDefaultValue(Tbl_Table_t * table)
239{
240  Tbl_Entry_t * defEntry;
241  int defIndex;
242  lsList * rangeList;
243  Tbl_TableForEachDefaultEntry(table,defEntry,defIndex)
244  { 
245    rangeList = Tbl_EntryReadList(defEntry);
246    int length = lsLength(rangeList);
247    if ( length  != 1)
248      return -1;
249    Tbl_Range_t * range;
250    int valDefault;
251    lsGen gen;
252    Tbl_EntryForEachValue(defEntry,valDefault,gen,range){
253      return Tbl_RangeEnd(range);
254    }
255  }
256}
257/**Function********************************************************************
258 
259  Synopsis    [Test if a node is in a given submodule]
260
261  Description [Return true if the node is in one of the submdule,
262  else return false. The comparison is made by the name of the node
263  compare to the name of the submodule. Node name n that belongs to a
264  subsystem named sub as in the following form : sub.n]
265
266  SideEffects []
267
268  SeeAlso     []
269
270******************************************************************************/
271
272boolean Dbg_TestNodeInSubs(char* nodeName,array_t * subsName)
273{
274  assert(nodeName != NIL(char));
275  if(subsName == NIL(array_t))
276    return 0;
277  if(array_n(subsName) == 0)
278    return 0;
279  int i;
280  char * subName;
281  arrayForEachItem(char*, subsName, i, subName){
282      if(strstr(nodeName,subName) != NULL) 
283        return 1;
284  }
285  return 0;
286}
287
Note: See TracBrowser for help on using the repository browser.