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

Last change on this file since 43 was 42, checked in by cecile, 13 years ago

Fault candidates OK

File size: 5.6 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
Note: See TracBrowser for help on using the repository browser.