source: vis_dev/vis-2.3/src/puresat/puresatIPRefine.c @ 36

Last change on this file since 36 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 25.6 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [puresatIPRefine.c]
4
5  PackageName [puresat]
6
7  Synopsis    [Abstraction refinement for large scale invariant checking.]
8
9  Description [This file contains the functions to check invariant properties
10  by the PureSAT abstraction refinement algorithm, which is entirely based on
11  SAT solver, the input of which could be either CNF or AIG. It has several
12  parts:
13
14  * Localization-reduction base Abstraction
15  * K-induction or interpolation to prove the truth of a property
16  * Bounded Model Checking to find bugs
17  * Incremental concretization based methods to verify abstract bugs
18  * Incremental SAT solver to improve efficiency
19  * UNSAT proof based method to obtain refinement
20  * AROSAT to bring in only necessary latches into unsat proofs
21  * Bridge abstraction to get compact coarse refinement
22  * Refinement minization to guarrantee minimal refinements
23  * Unsat proof-based refinement minimization to eliminate multiple candidate
24    by on SAT test
25  * Refinement prediction to decrease the number of refinement iterations
26  * Dynamic switching to redistribute computional resources to improve
27    efficiency
28
29  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
30  paper of Li et al., "A satisfiability-based appraoch to abstraction
31  refinement in model checking", " Abstraction in symbolic model checking
32  using satisfiability as the only decision procedure", "Efficient computation
33  of small abstraction refinements", and "Efficient abstraction refinement in
34  interpolation-based unbounded model checking"]
35
36  Author      [Bing Li]
37
38  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
39  All rights reserved.
40
41  Permission is hereby granted, without written agreement and without
42  license or royalty fees, to use, copy, modify, and distribute this
43  software and its documentation for any purpose, provided that the
44  above copyright notice and the following two paragraphs appear in
45  all copies of this software.]
46
47******************************************************************************/
48#include "puresatInt.h"
49
50
51/*---------------------------------------------------------------------------*/
52/* Constant declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55/*---------------------------------------------------------------------------*/
56/* Structure declarations                                                    */
57/*---------------------------------------------------------------------------*/
58
59/*---------------------------------------------------------------------------*/
60/* Type declarations                                                         */
61/*---------------------------------------------------------------------------*/
62
63/*---------------------------------------------------------------------------*/
64/* Variable declarations                                                     */
65/*---------------------------------------------------------------------------*/
66
67/*---------------------------------------------------------------------------*/
68/* Macro declarations                                                        */
69/*---------------------------------------------------------------------------*/
70
71/**AutomaticStart*************************************************************/
72
73/*---------------------------------------------------------------------------*/
74/* Static function prototypes                                                */
75/*---------------------------------------------------------------------------*/
76
77/**AutomaticEnd***************************************************************/
78
79/*---------------------------------------------------------------------------*/
80/* Definition of exported functions                                          */
81/*---------------------------------------------------------------------------*/
82
83/**Function********************************************************************
84
85  Synopsis    [Generate sufficient set from unsat proof]
86
87  Description []
88
89  SideEffects []
90
91  SeeAlso     []
92
93******************************************************************************/
94
95#if UNSATCORE
96void PureSat_GetSufAbsFromCoreRecur(mAig_Manager_t *manager,
97                                    satManager_t * cm,
98                                    RTnode_t RTnode,
99                                    st_table *ctTable,
100                                    st_table *refineTable,
101                                    FILE * fp)
102#else
103void PureSat_GetSufAbsFromCoreRecur(mAig_Manager_t *manager,
104                                    satManager_t * cm,
105                                    RTnode_t RTnode,
106                                    st_table *ctTable,
107                                    st_table *refineTable)
108#endif
109{
110  int i,ct;
111  bAigTimeFrame_t *tf = manager->timeframeWOI;
112  char *name;
113  bAigEdge_t v,*lp;
114  st_table *table;
115  st_generator *stgen;
116  RTManager_t * rm = cm->rm;
117
118  if(RT_flag(RTnode)&RT_VisitedMask)
119    return;
120
121  RT_flag(RTnode) |= RT_VisitedMask;
122  /*leaf*/
123  if(RT_pivot(RTnode)==0){
124#if DBG
125    assert(RT_oriClsIdx(RTnode)==0);
126#endif
127    if(RT_oriClsIdx(RTnode)!=0)
128      lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
129    else
130
131      lp = RT_formula(RTnode) + cm->rm->fArray;
132    for(i=0;i<RT_fSize(RTnode);i++,lp++){
133      if(RT_oriClsIdx(RTnode)!=0)
134        v = SATgetNode(*lp);
135      else
136        v = *lp;
137      if(*lp<0)
138        continue;
139
140#if UNSATCORE
141      v = SATnormalNode(v);
142      fprintf(fp,"%d_%d ",v,SATclass(v));
143      if(SATflags(v)&DummyMask)
144        fprintf(fp,"DM ");
145      if(SATflags(v)&VisibleVarMask)
146        fprintf(fp,"Visible  ");
147      else
148        if(SATflags(v)&StateBitMask)
149          fprintf(fp, "InvSV  ");
150
151#endif
152      v = SATnormalNode(v);
153      if((SATflags(v)&VisibleVarMask)){
154
155        if(SATclass(v)==0){
156          if(!st_lookup(tf->idx2name,(char*)v,&name)&&
157             !st_lookup(tf->MultiLatchTable,(char*)v,&table))
158            continue;
159        }
160#if 1
161        /* at least 2 times to be choosen as a candidate*/
162        if(st_lookup(ctTable,(char*)v,&ct)){
163          if(ct<0)
164            continue;
165          if(ct>=1){
166
167            if(!st_lookup(tf->MultiLatchTable,(char*)v,&table)){
168              int retVal = st_lookup(tf->idx2name,(char*)v,&name);
169              assert(retVal);
170              st_insert(refineTable,(char*)name,(char*)0);
171              st_insert(ctTable,(char*)v,(char*)-1);
172
173            }
174            else{
175#ifdef TIMEFRAME_VERIFY_
176              fprintf(vis_stdout,"%d is in MultiLatchTable: ",v);
177#endif
178              st_foreach_item(table,stgen,(char**)&name,
179                              NIL(char*)){
180#ifdef TIMEFRAME_VERIFY_
181                fprintf(vis_stdout,"%s   ",name);
182#endif
183                st_insert(refineTable,(char*)name,(char*)0);
184              }
185#ifdef TIMEFRAME_VERIFY_
186              fprintf(vis_stdout,"\n");
187#endif
188              st_insert(ctTable,(char*)v,(char*)-1);
189            }
190          }
191        }
192        else{
193          ct=1;
194          st_insert(ctTable,(char*)v,(char*)(long)ct);
195        }
196#else
197        retVal = st_lookup(tf->idx2name,(char*)v,(char**)&name);
198        assert(retVal);
199        st_insert(refineTable,(char*)name,(char*)0);
200
201#endif
202      }/* if(SATflags(v)&StateBitMask){*/
203    }
204#if UNSATCORE
205    fprintf(fp,"0\n");
206#endif
207  }
208  /*non leaf*/
209  else{
210    assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL);
211#if UNSATCORE
212    PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_left(RTnode),
213                                   ctTable,refineTable,fp);
214    PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_right(RTnode),
215                                   ctTable,refineTable,fp);
216#else
217    PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_left(RTnode),
218                                   ctTable,refineTable);
219    PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_right(RTnode),
220                                   ctTable,refineTable);
221#endif
222  }
223  return;
224}
225
226/**Function********************************************************************
227
228  Synopsis    [Generate sufficient set from unsat proof by bridge abstraction]
229
230  Description []
231
232  SideEffects []
233
234  SeeAlso     []
235
236******************************************************************************/
237
238//new pick latch
239#if UNSATCORE
240void PureSat_GetSufAbsFromCoreRecur_2side(mAig_Manager_t *manager,
241                                          satManager_t * cm,
242                                          RTnode_t RTnode,
243                                          st_table *ctTable,
244                                          st_table *refineTable,
245                                          st_table *SufNameTable,
246                                          FILE * fp)
247#else
248void PureSat_GetSufAbsFromCoreRecur_2side(mAig_Manager_t *manager,
249                                          satManager_t * cm,
250                                          RTnode_t RTnode,
251                                          st_table *ctTable,
252                                          st_table *refineTable,
253                                          st_table *SufNameTable)
254#endif
255{
256  int i,j,find,find1,times;
257  bAigTimeFrame_t *tf = manager->timeframeWOI;
258  char *name,*name1;
259  bAigEdge_t v,v1,*lp,*lp1, *lp2, left,right;
260  st_table *table;
261  st_generator *stgen;
262  RTManager_t * rm = cm->rm;
263  long maxNode;
264
265  if(RT_flag(RTnode)&RT_VisitedMask)
266    return;
267
268  RT_flag(RTnode) |= RT_VisitedMask;
269
270  if(RT_pivot(RTnode)==0){
271#if DBG
272    assert(RT_oriClsIdx(RTnode)==0);
273#endif
274    if(RT_oriClsIdx(RTnode)!=0)
275      lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
276    else
277
278      lp = RT_formula(RTnode) + cm->rm->fArray;
279    lp1 = lp;
280    (cm->line)++;
281    for(i=0;i<RT_fSize(RTnode);i++,lp++){
282      if(RT_oriClsIdx(RTnode)!=0)
283        v = SATgetNode(*lp);
284      else
285        v = *lp;
286      if(*lp<0)
287        continue;
288#if UNSATCORE
289      v = SATnormalNode(v);
290      fprintf(fp,"%d_%d ",v,SATclass(v));
291      if(SATflags(v)&DummyMask)
292        fprintf(fp,"DM ");
293      if(SATflags(v)&VisibleVarMask)
294        fprintf(fp,"Visible  ");
295      else
296        if(SATflags(v)&StateBitMask)
297          fprintf(fp, "InvSV  ");
298
299#endif
300      v = SATnormalNode(v);
301#if LAI
302      /*mark every node in core for latch interface abs*/
303      flags(v) |= VisitedMask;
304#endif
305      if(SATflags(v)&VisibleVarMask){
306        if((SATclass(v)==0)&&
307           (st_lookup(tf->idx2name,(char*)v,&name)==0)&&
308           (st_lookup(tf->MultiLatchTable,(char*)v,&table)==0))
309            continue;
310
311        lp2 = lp1;
312        left = SATnormalNode(leftChild(v));
313        right = SATnormalNode(rightChild(v));
314        //find largest node
315        maxNode = -1;
316        for(j=0;j<RT_fSize(RTnode);j++,lp2++){
317          if(RT_oriClsIdx(RTnode)!=0)
318            v1 = SATgetNode(*lp2);
319          else
320            v1 = *lp2;
321          if(maxNode < SATnormalNode(v1))
322            maxNode = SATnormalNode(v1);
323        }
324        if(maxNode == v){
325#if DBG
326          lp2 = lp1;
327          for(j=0;j<RT_fSize(RTnode);j++,lp2++){
328            if(RT_oriClsIdx(RTnode)!=0)
329              v1 = SATgetNode(*lp2);
330            else
331              v1 = *lp2;
332            if(*lp2<0||SATnormalNode(v1)==v)
333              continue;
334            assert((SATnormalNode(v1) == SATnormalNode(leftChild(v)))||
335                   SATnormalNode(v1) == SATnormalNode(rightChild(v)));
336          }
337#endif
338          SATflags(v) |= Visited2Mask; /*left side*/
339        }
340        else{
341#if DBG
342          lp2 = lp1;
343          for(j=0;j<RT_fSize(RTnode);j++,lp2++){
344            if(RT_oriClsIdx(RTnode)!=0)
345              v1 = SATgetNode(*lp2);
346            else
347              v1 = *lp2;
348            if(*lp2<0||SATnormalNode(v1)==maxNode)
349              continue;
350            assert((SATnormalNode(v1) == SATnormalNode(leftChild(maxNode)))||
351                   (SATnormalNode(v1) == SATnormalNode(rightChild(maxNode))));
352          }
353#endif
354          SATflags(v) |= Visited3Mask; /*right side*/
355#if THROUGHPICK
356          /*pick latch due to split*/
357            if(SATflags(v)&VPGVMask){
358              if(SATclass(maxNode)<=1)
359                SATflags(v) |= NewMask; /*the same tf*/
360              else
361                SATflags(v) |= Visited4Mask; /* larger tf*/
362            }
363#endif
364        }
365
366      }
367
368#if THROUGHPICK
369      if((SATflags(v)&VisibleVarMask)&&
370         (((SATflags(v)&Visited2Mask)&&(SATflags(v)&Visited3Mask))||
371         ((SATflags(v)&Visited4Mask)&&(SATflags(v)&NewMask)))){
372#else
373      if((SATflags(v)&VisibleVarMask)&&
374         ((SATflags(v)&Visited2Mask)&&(SATflags(v)&Visited3Mask))){
375#endif
376        times = 1;
377        if(!st_lookup(tf->MultiLatchTable,(char*)v,&table)){
378          int retVal = st_lookup(tf->idx2name,(char*)v,&name);
379          assert(retVal);
380
381          if(st_lookup(refineTable,(char*)name,&times))
382            times++;
383          st_insert(refineTable,(char*)name,(char*)(long)times);
384        }
385
386        /*for iden latches, we only add one, which is enough*/
387        else{
388          find = 0;
389          find1 = 0;
390          st_foreach_item(table,stgen,(char**)&name,
391                          NIL(char*)){
392            if(st_lookup(refineTable,name,NIL(char*))){
393              find = 1;
394              break;
395            }
396            if(find1==0){
397              if(st_lookup(SufNameTable,name, NIL(char*))){
398                name1 = name;
399                find1 = 1;
400              }
401            }
402          }
403          if(find==0){
404            times = 1;
405            if(st_lookup(refineTable,(char*)name1,&times))
406              times++;
407            st_insert(refineTable,(char*)name1,(char*)(long)times);
408
409          }
410        }
411
412
413      }
414    }
415#if UNSATCORE
416   fprintf(fp,"0\n");
417#endif
418  }
419    /*non leaf*/
420  else{
421    assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL);
422#if UNSATCORE
423    PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_left(RTnode),
424                                   ctTable,refineTable,SufNameTable,fp);
425    PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_right(RTnode),
426                                   ctTable,refineTable,SufNameTable,fp);
427#else
428    PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_left(RTnode),
429                                   ctTable,refineTable,SufNameTable);
430    PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_right(RTnode),
431                                   ctTable,refineTable,SufNameTable);
432#endif
433  }
434  return;
435}
436
437
438
439/**Function********************************************************************
440
441  Synopsis    [Generate sufficient set from unsat proof]
442
443  Description []
444
445  SideEffects []
446
447  SeeAlso     []
448
449******************************************************************************/
450
451array_t * PureSat_GetSufAbsFromCore(Ntk_Network_t *network,
452                                    satManager_t * cm,
453                                    PureSat_Manager_t *pm,
454                                    bAigEdge_t property,
455                                    st_table * SufAbsNameTable)
456{
457  array_t * refArray = array_alloc(char *,0);
458  char *name;
459  st_generator *stgen;
460  Ntk_Node_t *latch;
461  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
462  st_table * ctTable = st_init_table(st_numcmp,st_numhash);
463  st_table * refineTable = st_init_table(strcmp,st_strhash);
464  int times;
465#if UNSATCORE
466  FILE * fp = fopen("unsatcore.txt","w");
467#endif
468#if LAI
469  st_table * refineTable1 = st_init_table(strcmp,st_strhash);
470
471#endif
472
473
474  PureSat_CleanMask(manager,ResetVisited1234NewMask);
475#if UNSATCORE
476  fprintf(fp,"p cnf %d line, # nodes:%d\n",
477          cm->initNumVariables,cm->nodesArraySize);
478  cm->line = 0;
479  PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,cm->rm->root,
480                                 ctTable,refineTable,SufAbsNameTable,fp);
481  fprintf(fp,"total lines: %d\n",cm->line);
482#else
483  PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,cm->rm->root,
484                                 ctTable,refineTable,SufAbsNameTable);
485
486#endif
487  PureSat_CleanMask(manager,ResetVisited1234NewMask);
488
489#if LAI
490  ResetRTree(cm->rm);
491  PureSat_GetLIAForNode(manager,property);
492  PureSat_GetSufAbsByLIA(manager,cm,cm->rm->root,
493                        refineTable1);
494#endif
495
496
497  st_foreach_item(refineTable,stgen,&name,&times){
498    latch = Ntk_NetworkFindNodeByName(network,name);
499
500    if(!st_lookup(pm->vertexTable,(char*)name,NIL(char*))&&
501      st_lookup(pm->SufAbsTable, (char*)latch,NIL(char*))){
502      array_insert_last(char *,refArray,name);
503      if(pm->verbosity>=2)
504        fprintf(vis_stdout,"ref cand:%s %d\n",name,times);
505    }
506  }
507
508#if LAI
509  st_foreach_item(refineTable1,stgen,(char**)&name,NIL(char*)){
510    latch = Ntk_NetworkFindNodeByName(network,name);
511    if(!st_lookup(pm->vertexTable,(char*)name,NIL(char*))&&
512       st_lookup(pm->CoiTable, (char*)latch,NIL(char*))){
513      if(pm->verbosity>=2)
514        fprintf(vis_stdout,"from LIA ref candidate:%s\n",name);
515
516    }
517  }
518#endif
519
520#if UNSATCORE
521  fclose(fp);
522#endif
523
524  st_free_table(ctTable);
525  st_free_table(refineTable);
526#if LAI
527  st_free_table(refineTable1);
528#endif
529  return refArray;
530}
531
532
533
534/**Function********************************************************************
535
536  Synopsis    [Main procedure of refinement computation]
537
538  Description []
539
540  SideEffects []
541
542  SeeAlso     []
543
544******************************************************************************/
545
546array_t *PureSat_RefineOnAbs(Ntk_Network_t *network,
547                             PureSat_Manager_t *pm,
548                             bAigEdge_t property,
549                             array_t *previousResultArray,
550                             int latchThreshHold,
551                             int * sccArray,
552                             array_t * sufArray)
553{
554  array_t * tmpRef,*tmpRef1,*tmpRef2,*tmpRef3;
555  array_t * tmpModel = array_alloc(char *,0),*tmpArray1,*tmpArray2;
556  satManager_t *cm;
557  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
558  st_table *table;
559  char * name;
560  int i,j;
561  int NumInSecondLevel;
562  st_generator *stgen;
563  Ntk_Node_t *latch;
564  double t1,t2,t3,t4;
565  st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
566  st_table * junkTable;
567  int noArosat = 1;
568
569
570  tmpRef = array_alloc(char *,0);
571  st_foreach_item(pm->SufAbsTable,stgen,&latch,NIL(char*)){
572    name = Ntk_NodeReadName(latch);
573    if(st_lookup(pm->vertexTable,name,NIL(char *)))
574      array_insert_last(char *,tmpModel,name);
575    array_insert_last(char *,tmpRef,name);
576    st_insert(SufAbsNameTable,name,(char *)0);
577
578  }
579
580  t1 = util_cpu_ctime();
581  manager->assertArray = sat_ArrayAlloc(1);
582  sat_ArrayInsert(manager->assertArray,manager->InitState);
583  cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
584  if(pm->Arosat){
585    cm->option->decisionHeuristic &= RESET_LC;
586    cm->option->decisionHeuristic |= DVH_DECISION;
587    cm->option->arosat = 1;
588  }
589  cm->option->coreGeneration = 1;
590  cm->option->AbRf = 1;
591  cm->property = property;
592  cm->option->IP = 1;
593  PureSat_CleanMask(manager,ResetVisibleVarMask);
594  PuresatMarkVisibleVarWithVPGV(network,tmpRef,pm,0,pm->Length+1);
595  array_free(tmpRef);
596  t3 = util_cpu_ctime();
597  PureSatPreprocess(network,cm,pm,SufAbsNameTable,pm->Length);
598  t4 = util_cpu_ctime();
599  pm->tPro += t4-t3;
600  if(pm->verbosity>=2)
601    fprintf(vis_stdout,"process time:%g,total:%g\n",
602           (double)((t4-t3)/1000.0),pm->tPro/1000);
603
604  if(cm->option->arosat){
605    PureSatCreateLayer(network,pm,cm,tmpModel,sufArray);
606    cm->Length = pm->Length;
607    AS_Main(cm);
608    noArosat = 0;
609    st_foreach_item(cm->layerTable,stgen,&table,NIL(char*))
610      st_free_table(table);
611    st_free_table(cm->layerTable);
612    FREE(cm->assignedArray);
613    FREE(cm->numArray);
614  }
615  else
616    sat_Main(cm);
617
618  manager->NodesArray = cm->nodesArray;;
619  assert(cm->status==SAT_UNSAT);
620  t3 = util_cpu_ctime();
621  PureSatPostprocess(manager,cm,pm);
622  PureSatProcessDummy(manager,cm,cm->rm->root);
623  ResetRTree(cm->rm);
624  t4 = util_cpu_ctime();
625  pm->tPro += t4-t3;
626  if(pm->verbosity>=2)
627    fprintf(vis_stdout,"process time:%g,total:%g\n",
628           (double)((t4-t3)/1000.0),pm->tPro/1000);
629  t2 = util_cpu_ctime();
630  pm->tCoreGen += t2 - t1;
631  if(pm->verbosity>=2)
632    fprintf(vis_stdout,"time for UNsat core generation:%g,total:%g\n",
633           (double)(t2-t1)/1000.0,pm->tCoreGen/1000.0);
634
635  t1 = util_cpu_ctime();
636  tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable);
637  t2 = util_cpu_ctime();
638
639  st_free_table(SufAbsNameTable);
640  RT_Free(cm->rm);
641  sat_ArrayFree(manager->assertArray);
642  PureSat_SatFreeManager(cm);
643
644  /*Get suff set*/
645  tmpRef2 = array_alloc(char *,0);
646  tmpRef3 = array_alloc(char *,0);
647  tmpArray1 = array_alloc(char *,0);
648  tmpArray2 = array_alloc(char *,0);
649
650  if(noArosat){
651    t1 = util_cpu_ctime();
652    if(array_n(tmpRef1)){
653      tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
654                                        &NumInSecondLevel);
655      array_free(pm->latchArray);
656    }
657
658  }
659  else{
660    if(array_n(tmpRef1)){
661      tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
662                                        &NumInSecondLevel);
663      array_free(pm->latchArray);
664    }
665    else
666      tmpRef = array_alloc(char*,0);
667#if NOREFMIN
668    if(pm->verbosity>=1){
669      fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
670      arrayForEachItem(char *,tmpRef,i,name)
671        fprintf(vis_stdout,"%s\n",name);
672    }
673    PureSatAddIdenLatchToAbs(network,pm,tmpRef);
674    array_free(tmpRef1);
675    array_free(tmpModel);
676    return tmpRef;
677#endif
678  }
679
680
681  /*Ref Minimization
682    //try all the candidates*/
683  t1 = util_cpu_ctime();
684
685  if(pm->CoreRefMin && array_n(tmpRef)>=5){
686    if(pm->verbosity>=1)
687      fprintf(vis_stdout,"Core Ref Min\n");
688    junkTable = st_init_table(strcmp,st_strhash);
689    for(i=array_n(tmpRef)-1;i>=0;i--)
690      {
691        array_t * tmpA;
692        name = array_fetch(char *,tmpRef,i);
693        if(pm->verbosity>=1)
694          fprintf(vis_stdout,"RefMin: testing %s\n",name);
695        tmpArray2 = PureSatRemove_char(tmpRef,i);
696        if(st_lookup(junkTable,name,NIL(char))){
697          array_free(tmpRef);
698          tmpRef = tmpArray2;
699          if(pm->verbosity>=1)
700            fprintf(vis_stdout,"%s is junk\n",name);
701          continue;
702        }
703        tmpA = array_dup(tmpModel);
704        array_append(tmpA,tmpArray2);
705
706        t3 = util_cpu_time();
707        tmpArray1 = array_alloc(char*,0);
708        arrayForEachItem(char*,tmpA,j,name)
709          if(!st_lookup(junkTable,name,NIL(char)))
710            array_insert_last(char*,tmpArray1,name);
711        array_free(tmpA);
712
713        if(!PureSat_ConcretTest_Core(network,pm,tmpArray1,property,
714                                     previousResultArray,junkTable)){
715          /*then the candidate can' be deleted*/
716          t4 = util_cpu_time();
717          if(pm->verbosity>=2)
718            fprintf(vis_stdout," %g\n",(t4-t3)/1000);
719          array_free(tmpArray2);
720        }
721        else /*delete it*/
722          {
723            t4 = util_cpu_time();
724            if(pm->verbosity>=2)
725              fprintf(vis_stdout,"time: %g\n",(t4-t3)/1000);
726            array_free(tmpRef);
727            tmpRef = tmpArray2;
728          }
729        array_free(tmpArray1);
730      }
731    st_free_table(junkTable);
732  }
733  else{
734    for(i=array_n(tmpRef)-1;i>=0;i--)
735      {
736        name = array_fetch(char *,tmpRef,i);
737
738        if(pm->verbosity>=1)
739          fprintf(vis_stdout,"RefMin: testing %s\n",name);
740        tmpArray2 = PureSatRemove_char(tmpRef,i);
741        tmpArray1 = array_dup(tmpModel);
742        array_append(tmpArray1,tmpArray2);
743
744        t3 = util_cpu_time();
745        if(!PureSat_ConcretTest(network,pm,tmpArray1,property,
746                                previousResultArray,0,0,0)){
747          t4 = util_cpu_time();
748          if(pm->verbosity>=2)
749            fprintf(vis_stdout," %g\n",(t4-t3)/1000);
750          array_free(tmpArray2);
751        }
752        else /*delete it*/
753          {
754            t4 = util_cpu_time();
755            if(pm->verbosity>=2)
756              fprintf(vis_stdout,"time: %g\n",(t4-t3)/1000);
757            array_free(tmpRef);
758            tmpRef = tmpArray2;
759          }
760        array_free(tmpArray1);
761      }
762  }
763
764
765  t2 = util_cpu_ctime();
766  pm->tRefMin += t2 - t1;
767  if(pm->verbosity>=2)
768    fprintf(vis_stdout,"\ntime for Ref Min: %g, total:%g\n",
769           (t2-t1)/1000,pm->tRefMin/1000);
770  if(pm->verbosity>=1){
771    fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
772    arrayForEachItem(char *,tmpRef,i,name)
773      fprintf(vis_stdout,"%s\n",name);
774  }
775  PureSatAddIdenLatchToAbs(network,pm,tmpRef);
776  array_free(tmpRef1);
777  array_free(tmpModel);
778  return tmpRef;
779}
780
781
782/**Function********************************************************************
783
784  Synopsis    [Refinement procedure without refinement minimization]
785
786  Description []
787
788  SideEffects []
789
790  SeeAlso     []
791
792******************************************************************************/
793
794
795array_t *PureSat_RefineOnAbs_DA(Ntk_Network_t *network,
796                             PureSat_Manager_t *pm,
797                             bAigEdge_t property,
798                             array_t *previousResultArray,
799                             int latchThreshHold,
800                             int * sccArray,
801                             array_t * sufArray)
802{
803  array_t * tmpRef,*tmpRef1,*tmpRef2,*tmpRef3; //= array_alloc(char *,0);
804  array_t * tmpModel = array_alloc(char *,0),*tmpArray1,*tmpArray2;
805  satManager_t *cm;
806  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
807  st_table *table;
808  char * name;
809  int i;
810  int NumInSecondLevel;
811  st_generator *stgen;
812  Ntk_Node_t *latch;
813  double t1,t2,t3,t4;
814  st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
815  int noArosat = 1;
816
817
818  tmpRef = array_alloc(char *,0);
819  st_foreach_item(pm->SufAbsTable,stgen,&latch,NIL(char*)){
820    name = Ntk_NodeReadName(latch);
821    if(st_lookup(pm->vertexTable,name,NIL(char *)))
822      array_insert_last(char *,tmpModel,name);
823    array_insert_last(char *,tmpRef,name);
824    st_insert(SufAbsNameTable,name,(char *)0);
825
826  }
827
828  t1 = util_cpu_ctime();
829  manager->assertArray = sat_ArrayAlloc(1);
830  sat_ArrayInsert(manager->assertArray,manager->InitState);
831  cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
832#if AROSAT
833  cm->option->decisionHeuristic &= RESET_LC;
834  cm->option->decisionHeuristic |= DVH_DECISION;
835  cm->option->arosat = 1;
836#endif
837  cm->option->coreGeneration = 1;
838  cm->option->AbRf = 1;
839
840  cm->option->IP = 1;
841  cm->property = property;
842  PureSat_CleanMask(manager,ResetVisibleVarMask);
843  PuresatMarkVisibleVarWithVPGV(network,tmpRef,pm,0,pm->Length+1);
844  array_free(tmpRef);
845  t3 = util_cpu_ctime();
846  PureSatPreprocess(network,cm,pm,SufAbsNameTable,pm->Length);
847  t4 = util_cpu_ctime();
848  pm->tPro += t4-t3;
849  if(pm->verbosity>=2)
850    fprintf(vis_stdout,"process time:%g,total:%g\n",
851           (double)((t4-t3)/1000.0),pm->tPro/1000);
852#if DBG
853  PureSatCheckCoi(manager);
854#endif
855  if(cm->option->arosat){
856    PureSatCreateLayer(network,pm,cm,tmpModel,sufArray);
857    cm->Length = pm->Length;
858    AS_Main(cm);
859    noArosat = 0;
860    st_foreach_item(cm->layerTable,stgen,&table,NIL(char*))
861      st_free_table(table);
862    st_free_table(cm->layerTable);
863    FREE(cm->assignedArray);
864    FREE(cm->numArray);
865  }
866  else
867    sat_Main(cm);
868  manager->NodesArray = cm->nodesArray;;
869  assert(cm->status==SAT_UNSAT);
870  t3 = util_cpu_ctime();
871  PureSatPostprocess(manager,cm,pm);
872  PureSatProcessDummy(manager,cm,cm->rm->root);
873  ResetRTree(cm->rm);
874  t4 = util_cpu_ctime();
875  pm->tPro += t4-t3;
876  if(pm->verbosity>=2)
877    fprintf(vis_stdout,"process time:%g,total:%g\n",
878           (double)((t4-t3)/1000.0),pm->tPro/1000);
879  t2 = util_cpu_ctime();
880  pm->tCoreGen += t2 - t1;
881  if(pm->verbosity>=2)
882    fprintf(vis_stdout,"time for UNsat core generation:%g,total:%g\n",
883           (double)(t2-t1)/1000.0,pm->tCoreGen/1000.0);
884#if DBG
885  PureSat_CheckFanoutFanin(manager);
886#endif
887  t1 = util_cpu_ctime();
888  tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable);
889  t2 = util_cpu_ctime();
890
891  st_free_table(SufAbsNameTable);
892  RT_Free(cm->rm);
893  sat_ArrayFree(manager->assertArray);
894  PureSat_SatFreeManager(cm);
895
896  /*Get suff set*/
897
898  tmpRef2 = array_alloc(char *,0);
899  tmpRef3 = array_alloc(char *,0);
900  tmpArray1 = array_alloc(char *,0);
901  tmpArray2 = array_alloc(char *,0);
902
903  if(noArosat){
904    t1 = util_cpu_ctime();
905    if(array_n(tmpRef1)){
906     tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
907                                        &NumInSecondLevel);
908
909      array_free(pm->latchArray);
910    }
911  }
912  /*if arosat*/
913  else{
914    if(array_n(tmpRef1)){
915      tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
916                                        &NumInSecondLevel);
917      array_free(pm->latchArray);
918    }
919    else
920      tmpRef = array_alloc(char*,0);
921
922    if(pm->verbosity>=1){
923      fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
924      arrayForEachItem(char *,tmpRef,i,name)
925        fprintf(vis_stdout,"%s\n",name);
926    }
927    PureSatAddIdenLatchToAbs(network,pm,tmpRef);
928    array_free(tmpRef1);
929    array_free(tmpModel);
930    return tmpRef;
931  }
932}
Note: See TracBrowser for help on using the repository browser.