source: vis_dev/dev/utilities.c @ 53

Last change on this file since 53 was 20, checked in by cecile, 13 years ago

main modified
File size: 12.9 KB
Line 
1#include "utilities.h"
2/*---------------------------------------------------------------------------*/
3/* Read_blif_mv                                                              */
4/*---------------------------------------------------------------------------*/
5Hrc_Manager_t * rlmv(FILE * file)
6{
7                return  Io_BlifMvRead( file, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE);
8
9}
10/*---------------------------------------------------------------------------*/
11/* flatten_hierarchy                                                         */
12/*---------------------------------------------------------------------------*/
13Ntk_Network_t * flatten_hier(Hrc_Manager_t * hmgr)
14{
15        assert(hmgr != NULL);
16        int            sweep       = 1;
17        int            verbose     = 0;
18        lsList         varNameList = (lsList) NULL;
19        Ntk_Network_t *ntk;
20        // flatten
21        Hrc_Node_t    *currentNode = Hrc_ManagerReadCurrentNode(hmgr);
22        ntk = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, NULL);
23
24        Hrc_NodeAddApplInfo(currentNode, NTK_HRC_NODE_APPL_KEY,
25                      (Hrc_ApplInfoFreeFn) Ntk_NetworkFreeCallback,
26                      (Hrc_ApplInfoChangeFn) NULL,  // not currently used by hrc
27                      (void *) ntk);
28        Ntk_NetworkSweep(ntk, verbose);
29        return ntk;
30
31}
32/*---------------------------------------------------------------------------*/
33/* Build_partition_maigs                                                     */
34/*---------------------------------------------------------------------------*/
35
36st_table * build_partition_maigs(Ntk_Network_t * ntk)
37{
38        Ntk_Node_t    *node, *latch;
39    lsGen          gen;
40        int i;
41        array_t       *result;
42        array_t           *inputs;
43        array_t       *roots;
44        st_table      *leaves;
45        st_table      *nodeToMvfAigTable;  /* mapes each node with its mvfAig */
46        MvfAig_Function_t  *mvfAig;
47        mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(ntk);
48        if (manager == NIL(mAig_Manager_t)) {
49                manager = mAig_initAig();
50                Ntk_NetworkSetMAigManager(ntk, manager);
51        }
52          roots = array_alloc(Ntk_Node_t *, 0);
53  Ntk_NetworkForEachCombOutput(ntk, gen, node) {
54    array_insert_last(Ntk_Node_t *, roots, node);
55  }
56  Ntk_NetworkForEachNode(ntk, gen, node) {
57    if(Ntk_NodeTestIsShadow(node))      continue;
58    if(Ntk_NodeTestIsCombInput(node))   continue;
59    if(Ntk_NodeTestIsCombOutput(node))continue;
60
61    if(Ntk_NodeReadNumFanouts(node) == 0 && Ntk_NodeReadNumFanins(node)) {
62        /**
63      fprintf(vis_stdout, "WARNING : dangling node %s\n", Ntk_NodeReadName(node));
64      **/
65      array_insert_last(Ntk_Node_t *, roots, node);
66    }
67  }
68
69  leaves = st_init_table(st_ptrcmp, st_ptrhash);
70
71  inputs = array_alloc(Ntk_Node_t *, 16);
72  Ntk_NetworkForEachCombInput(ntk, gen, node) {
73    array_insert_last(Ntk_Node_t *, inputs, node);
74  }
75  array_sort(inputs, nodenameCompare);
76  for(i=0; i<array_n(inputs); i++) {
77    node = array_fetch(Ntk_Node_t *, inputs, i);
78    st_insert(leaves,  node, (char *) ntmaig_UNUSED);
79    Ntk_NodeSetMAigId(node, 
80                       mAig_CreateVar(manager,
81                                      Ntk_NodeReadName(node),
82                                      Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
83  }
84  result = ntmaig_NetworkBuildMvfAigs(ntk, roots, leaves);
85
86  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(ntk, 
87                                                  MVFAIG_NETWORK_APPL_KEY);
88  Ntk_NetworkForEachLatch(ntk, gen, latch) {
89                node  = Ntk_LatchReadDataInput(latch);
90                st_lookup(nodeToMvfAigTable, node,  &mvfAig);
91                Ntk_NodeSetMAigId(node, mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig));
92                node  = Ntk_LatchReadInitialInput(latch);
93                st_lookup(nodeToMvfAigTable, node,  &mvfAig);
94                Ntk_NodeSetMAigId(node,   mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig));
95        }
96
97        roots->num = 0;
98        Ntk_NetworkForEachLatch(ntk, gen, latch) {
99                if(!st_lookup(nodeToMvfAigTable, latch,  &mvfAig))
100                        array_insert_last(Ntk_Node_t *, roots, latch);
101                }
102  result = ntmaig_NetworkBuildMvfAigs(ntk, roots, leaves);
103  array_free(roots);
104  array_free(inputs);
105  st_free_table(leaves);
106  MvfAig_FunctionArrayFree(result);
107  return nodeToMvfAigTable;
108}
109/*---------------------------------------------------------------------------*/
110/* Create unroll circuit k steps                                             */
111/*---------------------------------------------------------------------------*/
112void printLatch(st_table* CoiTable)
113{
114// COI contents
115   printf("*** COI ***\n");
116   st_generator    *stGen;
117   Ntk_Node_t * latch;
118   st_foreach_item(CoiTable, stGen, &latch, NULL) {
119        printf("%s\n",Ntk_NodeReadName(latch)); 
120  }
121}
122
123st_table * generateAllLatches(Ntk_Network_t * ntk)
124{
125    st_table        *CoiTable = st_init_table(st_ptrcmp, st_ptrhash);
126        lsGen           gen ;
127        Ntk_Node_t              *node;
128
129        Ntk_NetworkForEachNode(ntk,gen, node){
130                if (Ntk_NodeTestIsLatch(node)){
131                        st_insert(CoiTable, (char *) node, (char *) 0);
132                }
133        }
134        return CoiTable;
135
136}
137void build_unroll_circuit(Ntk_Network_t * ntk, int bound,BmcOption_t * options,BmcCnfClauses_t* cnfClauses)
138{
139    st_table        *CoiTable =  generateAllLatches(ntk);
140        lsGen           gen ;
141        Ntk_Node_t              *node;
142
143
144       
145        Ntk_NetworkForEachNode(ntk,gen, node){
146                if (Ntk_NodeTestIsLatch(node)){
147                        st_insert(CoiTable, (char *) node, (char *) 0);
148                }
149        }
150
151         options->verbosityLevel = BmcVerbosityMax_c;
152         options->satSolver = CirCUs;
153         options->timeOutPeriod = 0;
154         options->printInputs = TRUE;
155         options->minK = bound;
156         options->maxK = bound;
157         options->step = bound;
158         options->dbgLevel = 1;
159
160     //nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph
161     st_table* nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(ntk, MVFAIG_NETWORK_APPL_KEY);
162     assert(nodeToMvfAigTable != NIL(st_table));
163
164     // Create clauses database
165         int initState = BMC_INITIAL_STATES;
166         BmcCnfGenerateClausesForPath(ntk, 0, bound, initState, cnfClauses, nodeToMvfAigTable, CoiTable);
167
168}
169
170void printSATAssig( array_t* result)
171{
172        int k;
173        printf("RESULT : \n");
174        for(k=0; k< array_n(result); k++){
175                printf("%d\n",array_fetch(int, result, k));
176        }
177}
178void printNodeToMvFaigTable(st_table* nodeToMvfAigTable)
179{
180        // nodeToMvFaigTable contents
181        st_generator    *stGen;
182        Ntk_Node_t * latch;
183        printf("*** NODETOMV ***\n");
184        st_foreach_item(nodeToMvfAigTable, stGen, &latch, NULL) {
185                printf("%s , %d\n",Ntk_NodeReadName(latch),Ntk_NodeReadMAigId(latch)); 
186        }
187        printf("***************\n");
188}
189void printCNFIndex(BmcCnfClauses_t* cnfClauses)
190{
191        // Cnf index Table content
192        st_generator    *stGen;
193        nameType_t      *nodeName;
194        int index,i,k;
195        printf("*** cnfIndextable ***\n");
196        st_foreach_item(cnfClauses->cnfIndexTable, stGen,&nodeName,&index){
197                printf("(%s,%d)\n",nodeName, index);
198        }
199}
200void printCNFClauses(BmcCnfClauses_t* cnfClauses)
201{
202        int i,k;
203        printf("*** clause table ***\n");
204        for (i = 0; i < cnfClauses->nextIndex; i++) {
205                k = array_fetch(int, cnfClauses->clauseArray, i);
206                printf("%d%c", k, (k == 0) ? '\n' : ' ');
207    }
208}
209void
210printClauseLits(satManager_t *cm,long concl,FILE * file)
211{
212  long i, node, var_idx,*lit;
213
214  for(i=0, lit = (long*)SATfirstLit(concl); i<SATnumLits(concl);i++, lit++){
215    node = SATgetNode(*lit);
216    var_idx = SATnodeID(node);
217    if(SATisInverted(node))
218      fprintf(file,"%ld ", -var_idx);
219    else
220      fprintf(file,"%ld ",var_idx);
221  }
222  fprintf(file,"0\n");
223}
224
225int getClsIndex(long concl,int numVarInCnf)
226{
227        int clsIndex;
228        clsIndex = concl -  numVarInCnf * satNodeSize;
229    clsIndex = (clsIndex/satNodeSize)-1;
230        return clsIndex;
231
232}
233
234void printSatArrayCore(satManager_t *cm,satArray_t *clauseIndexInCore)
235{
236        int i,v,clsIndex;
237     for(i=0; i<clauseIndexInCore->num; i++) {
238                v = clauseIndexInCore->space[i];
239                clsIndex = getClsIndex(v,cm->initNumVariables);
240                printf("\nclause idx = %d\n",clsIndex);
241                printClauseLits(cm,v,vis_stdout);
242         }             
243}
244void printSatArrayCoreToCnf(satManager_t *cm,satArray_t *clauseIndexInCore, char *filename)
245{
246        FILE * file = fopen(filename,"w");
247        fprintf(file,"p cnf %d %d\n",clauseIndexInCore->num,cm->initNumVariables);
248        int i,v,clsIndex;
249     for(i=0; i<clauseIndexInCore->num; i++) {
250                v = clauseIndexInCore->space[i];
251                clsIndex = getClsIndex(v,cm->initNumVariables);
252                //printf("\nclause idx = %d\n",clsIndex);
253                printClauseLits(cm,v,file);
254         }             
255         fclose(file);
256}
257
258array_t * checkSATCircus( satManager_t *cm,BmcOption_t * options, boolean unsatcore,    satArray_t *clauseIndexInCore)
259{
260
261  satOption_t  *satOption;
262  array_t      *result = NIL(array_t);
263  int          maxSize;
264
265  satOption = sat_InitOption();
266  satOption->verbose = options->verbosityLevel;
267  //satOption->unsatCoreFileName = "Ucore.txt";
268  satOption->clauseDeletionHeuristic = 0;
269  satOption->coreGeneration = unsatcore;
270  satOption->minimizeConflictClause = 1;
271
272  cm->comment = ALLOC(char, 2);
273  cm->comment[0] = ' ';
274  cm->comment[1] = '\0';
275  cm->stdOut = stdout;
276  cm->stdErr = stderr;
277
278  cm->option = satOption;
279  cm->each = sat_InitStatistics();
280
281  cm->unitLits = sat_ArrayAlloc(16);
282  cm->pureLits = sat_ArrayAlloc(16);
283
284  maxSize = 10000 << (bAigNodeSize-4);
285  cm->nodesArray = ALLOC(bAigEdge_t, maxSize);
286  cm->maxNodesArraySize = maxSize;
287  cm->nodesArraySize = bAigNodeSize;
288
289  sat_AllocLiteralsDB(cm);
290       
291  sat_ReadCNF(cm, options->satInFile);
292  sat_Main(cm);
293   if(cm->status == SAT_UNSAT) {
294    if (options->verbosityLevel != BmcVerbosityNone_c){
295      (void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
296          }
297          if(unsatcore)
298          {
299                clauseIndexInCore =  cm->clauseIndexInCore;
300          }
301    fflush(cm->stdOut);
302
303        }else if(cm->status == SAT_SAT) {
304    if (options->verbosityLevel != BmcVerbosityNone_c){
305      (void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
306    }
307    fflush(cm->stdOut);
308    result = array_alloc(int, 0);
309    {
310      int i, size, value;
311     
312      size = cm->initNumVariables * bAigNodeSize;
313      for(i=bAigNodeSize; i<=size; i+=bAigNodeSize) {
314                value = SATvalue(i);
315                if(value == 1) {
316                        array_insert_last(int, result, SATnodeID(i));
317                }
318                else if(value == 0) {
319                        array_insert_last(int, result, -(SATnodeID(i)));
320                }
321      }
322    }
323  }
324  return result;
325
326}
327int findIndex(BmcCnfClauses_t* cnfClauses , char * nodeName)
328{       
329        int index;
330        st_lookup(cnfClauses->cnfIndexTable,nodeName,&index);
331        return index;
332
333}
334
335mdd_t * buildBdd4StateVal(array_t* stateName, int max, array_t * val,
336mdd_manager * mddManager)
337{
338        array_t * mvar_val= array_alloc(int,0);
339        array_t * mvar_name= array_alloc(char*,0);
340        array_t * mvar_strides= NIL(array_t);
341
342    if(array_n(stateName) == 1)
343        {
344                array_insert_last(int, mvar_val,max);
345                array_insert_last(char*, mvar_name,array_fetch(char*, stateName,0));
346        }
347        else
348        {
349                int i;
350                for( i = 0;i<max;i++)  array_insert_last(int, mvar_val,1);
351                mvar_name = array_dup(stateName);
352
353                printf(" Num of var , %d %d \n",array_n(stateName),array_n(mvar_val));
354               
355        }
356       
357        mdd_create_variables(mddManager, mvar_val,mvar_name, mvar_strides);
358
359        array_t *mvar_list = mdd_ret_mvar_list(mddManager);
360        array_t *bvar_list = mdd_ret_bvar_list(mddManager);
361
362        bvar_type bv = array_fetch(bvar_type, bvar_list, 0);
363
364        mvar_type mv;
365        bdd_node* f,*f2, * left, *right;
366        int i,v, value,mask;
367
368        f =  bdd_read_one(mddManager);
369        bdd_ref(f);
370        mv = array_fetch(mvar_type, mvar_list, 0);
371        printf("mvar name: %s;%d\n", mv.name,array_n(bvar_list)); 
372//      for(v=0;v<array_n(val); v++)
373//      {       
374                value = array_fetch(int,val,0);
375                mask = 1;
376                for(i= array_n(bvar_list)-1;i>=0; i--)
377                {
378                  printf("---->value %d , %d, %d \n",value,(value & mask),i);
379                        left =  bdd_bdd_ith_var(mddManager,i);
380                        if((value&mask) > 0)
381                                right =  bdd_bdd_and(mddManager,left,f);
382                        else
383                                right =  bdd_bdd_and(mddManager,bdd_not_bdd_node(left),f);
384                        bdd_ref(right);
385                        bdd_recursive_deref(mddManager,f);
386                        f = right;
387                        mask = mask *2;
388                }
389
390        for(v=1;v<array_n(val); v++)
391        {       
392                value = array_fetch(int,val,v);
393                mask = 1;
394                printf("----val_value : %d\n",value);
395                f2 =  bdd_read_one(mddManager);
396                bdd_ref(f2);
397
398                for(i= array_n(bvar_list)-1;i>=0; i--)
399                {
400                  printf("---->value %d , %d, %d \n",value,(value & mask),i);
401                        left =  bdd_bdd_ith_var(mddManager,i);
402                        if((value&mask) > 0)
403                                right =  bdd_bdd_and(mddManager,left,f2);
404                        else
405                                right =  bdd_bdd_and(mddManager,bdd_not_bdd_node(left),f2);
406                        bdd_ref(right);
407                        bdd_recursive_deref(mddManager,f2);
408                        f2 = right;
409                        mask = mask *2;
410                }
411                right =  bdd_bdd_or(mddManager,f2,f);
412                bdd_ref(right);
413                bdd_recursive_deref(mddManager,f2);
414                bdd_recursive_deref(mddManager,f);
415                f = right;
416        }
417               
418        mdd_t * mdd = bdd_construct_bdd_t(mddManager, f);
419        mdd_print_support(mdd); 
420        //FILE * file = fopen("bdd.dot","w");
421        //bdd_dump_dot(mddManager, 1, &f, NULL, NULL,file);
422
423        //fclose(file);
424        array_free(mvar_val);
425        array_free(mvar_name);
426
427        return mdd;
428       
429}
430
431
432void addObjState(array_t* stateName, int max, array_t * val, int steps,BmcCnfClauses_t *cnfClauses)
433{
434               
435        mdd_manager * mddManager = mdd_init_empty();
436        mdd_t * mdd =  buildBdd4StateVal(stateName, max,val,mddManager);
437        int index;
438        index = BmcGenerateCnfFormulaForBdd(mdd,steps, cnfClauses);
439        printf("number of clause : %d index %d \n", cnfClauses-> noOfClauses,index);
440
441        array_t * newClause;
442        newClause = array_alloc(int,1);
443        array_insert(int,newClause,0,index);
444        BmcCnfInsertClause(cnfClauses, newClause);
445
446
447
448
449        array_free(newClause);
450        mdd_quit(mddManager);
451
452       
453}
Note: See TracBrowser for help on using the repository browser.