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

Last change on this file since 93 was 44, checked in by cecile, 13 years ago

abnormal predicate done

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