source: vis_dev/vis-2.3/src/puresat/puresatRefine.c @ 56

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

vis2.3
File size: 14.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [puresatRefine.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/* Constant declarations                                                     */
52/*---------------------------------------------------------------------------*/
53
54/*---------------------------------------------------------------------------*/
55/* Structure declarations                                                    */
56/*---------------------------------------------------------------------------*/
57
58/*---------------------------------------------------------------------------*/
59/* Type declarations                                                         */
60/*---------------------------------------------------------------------------*/
61
62/*---------------------------------------------------------------------------*/
63/* Variable declarations                                                     */
64/*---------------------------------------------------------------------------*/
65
66/*---------------------------------------------------------------------------*/
67/* Macro declarations                                                        */
68/*---------------------------------------------------------------------------*/
69
70/**AutomaticStart*************************************************************/
71
72/*---------------------------------------------------------------------------*/
73/* Static function prototypes                                                */
74/*---------------------------------------------------------------------------*/
75
76
77/**AutomaticEnd***************************************************************/
78
79/*---------------------------------------------------------------------------*/
80/* Definition of exported functions                                          */
81/*---------------------------------------------------------------------------*/
82
83
84/*---------------------------------------------------------------------------*/
85/* Definition of internal functions                                          */
86/*---------------------------------------------------------------------------*/
87
88/**Function********************************************************************
89
90  Synopsis    [Refinement procedure of PURESAT algorithm]
91
92  Description [Refinement procedure of PURESAT algorithm]
93
94  SideEffects []
95
96  SeeAlso     []
97
98******************************************************************************/
99
100
101array_t * PureSatRefineOnAbs(Ntk_Network_t *network,
102                      PureSat_Manager_t *pm,
103                      bAigEdge_t  property,
104                      int latchThreshHold)
105{
106  mAig_Manager_t    *maigManager       = Ntk_NetworkReadMAigManager(network);
107  lsGen             gen;
108  Ntk_Node_t        *latch;
109  FILE              *fp, *fp1;
110  BmcOption_t       *options,*option2;
111  int        i,j,k,Length,beginPosition=0;
112  int        NumInSecondLevel=0;
113  array_t    * tmpRefinement,*tmpArray1,*tmpArray2;
114  array_t    *tmpModel,*tmpRefinement1;
115  /*st_table   * RefinementTable, *CandidateTable;*/
116  array_t    *Pclause, *tmpRefinement2, *tmpRefinement3, *oriSufArray;
117  char       buffer[1024],str[100];
118  char       *name, *coreFile, *tmpCoreFile, *coreFile1=(char *)0;
119  int         oldLength=0,oriCoreSize, CoreSize,weight;
120  st_table          *nodeToMvfAigTable;
121  BmcCnfStates_t    *cnfstate;
122  int             oldNumOfLatchInCore;
123  int             newNumOfLatchInCore,NumOfLatchInModel,round;
124  boolean     VarInCoreIsEnough = FALSE, LatchFromCore = FALSE;
125  boolean     firstTime = TRUE;
126  long t1,t2,t3,t4;
127  st_table * localSufAbsTable;
128  PureSat_IncreSATManager_t * pism = PureSatIncreSATManagerAlloc(pm);
129  satManager_t * cm = pism->cm;
130  BmcCnfClauses_t   * cnfClauses = pism->cnfClauses;
131  st_table *vertexTable = pm->vertexTable;
132  st_table *SufAbsTable = pm->SufAbsTable;
133  /*st_table *CoiTable = pm->CoiTable;*/
134  /*st_table *supportTable = pm->supportTable;*/
135  /* st_table *AbsTable = pm->AbsTable;*/
136   
137  t1 = util_cpu_ctime();
138
139  cm->option->clauseDeletionHeuristic = 0;
140  cm->option->incTraceObjective = 0;
141  pism->Length = pm->Length;
142  Length =  pm->Length;
143  coreFile = BmcCreateTmpFile();
144  tmpCoreFile = BmcCreateTmpFile();
145  strcpy(str,"coreFile: ");
146  strcat(str,coreFile);
147  strcat(str,", tmpCoreFile: ");
148  strcat(str,tmpCoreFile);
149  strcat(str,"\n");
150  if(pm->verbosity>=2)
151    fprintf(vis_stdout,"%s",str);
152  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
153  if (nodeToMvfAigTable == NIL(st_table)){
154    (void) fprintf(vis_stderr, "** bmc error: please run buid_partiton_maigs first\n");
155    exit (0);
156  }
157 
158  option2 = BmcOptionAlloc();
159  option2->satInFile = BmcCreateTmpFile();
160  option2->satOutFile = BmcCreateTmpFile();
161  options = BmcOptionAlloc();
162  options->satInFile = BmcCreateTmpFile();
163  options->satOutFile = BmcCreateTmpFile();
164
165  newNumOfLatchInCore = 0;
166  NumOfLatchInModel = 0;
167  tmpModel = array_alloc(char *,0);
168  oriSufArray = array_alloc(char *,0);
169  Ntk_NetworkForEachLatch(network, gen, latch){
170    name = Ntk_NodeReadName(latch);
171    if(st_lookup(vertexTable,name,NIL(char *))){
172      array_insert_last(char *,tmpModel,name);
173      NumOfLatchInModel++;
174    }
175    else
176      if(st_lookup(SufAbsTable,latch,NIL(char *))){
177        newNumOfLatchInCore++;
178        array_insert_last(char *,oriSufArray,name);
179      }
180  }
181 
182  localSufAbsTable = st_copy(SufAbsTable);
183  //tmpRefinement2 = array_alloc(char *,0);
184  tmpRefinement3 = array_alloc(char *,0);
185  //tmpArray1 = array_alloc(char *,0);
186  //tmpArray2 = array_alloc(char *,0);
187  weight = (NumOfLatchInModel+newNumOfLatchInCore+1)*10000;
188  round=0;
189 
190  round++;
191  if(pm->verbosity>=2)
192    fprintf(vis_stdout,"round: %d\n",round);
193  oldNumOfLatchInCore = newNumOfLatchInCore;
194  pm->ClsidxToLatchTable = st_init_table(st_numcmp,st_numhash);
195  PureSatGenerateClausesForPath_EnhanceInit(network,0,Length,pism,pm,nodeToMvfAigTable,localSufAbsTable);
196  Pclause = array_alloc(int,0);
197  array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(maigManager,property,
198                                                                      Length, cnfClauses));
199  BmcCnfInsertClause(cnfClauses, Pclause);
200  array_free(Pclause);
201  CoreSize=cnfClauses->noOfClauses;
202 
203  oriCoreSize = CoreSize;
204  cm->option->coreGeneration = 1;
205  cm->fp = fopen(tmpCoreFile, "w");
206  if(pm->verbosity>=2)
207    PureSatWriteClausesToFile(pism,maigManager,coreFile1);
208  t1 = util_cpu_ctime();
209  PureSatReadClauses(pism,pm);
210  sat_Main(cm);
211  t2 = util_cpu_ctime();
212  if(pm->verbosity>=2)
213    fprintf(vis_stdout,"time for SAT Solver(satMain): %g\n",(double)((t2-t1)/1000.0));
214 
215  fclose(cm->fp);
216  if(cm->status == SAT_SAT){
217    fprintf(vis_stderr,"This instance is supposed to be UNSAT, wrong and exit\n");
218    exit(0);
219  }
220  cm->stdOut = vis_stdout; 
221  cm->option->coreGeneration = 0;
222 
223  t2 = util_cpu_ctime();
224  if(pm->verbosity>=2)
225    fprintf(vis_stdout,"time for satMain: %g\n",(double)((t2-t1)/1000.0));
226  CoreSize = cm->numOfClsInCore;
227  if(pm->verbosity>=2)
228    fprintf(vis_stdout,"CoreSize:%d/OriCoreSize:%d\n", CoreSize,oriCoreSize);
229 
230  fp1 = fopen(coreFile, "w");
231  fp = fopen(tmpCoreFile, "r");
232  sprintf(buffer,"p cnf %d %d 0\n", cm->initNumVariables, cm->numOfClsInCore);
233  fputs(buffer, fp1);
234  while(fgets(buffer,1024,fp)){
235    fputs(buffer, fp1);
236  }
237  fclose(fp);
238  fclose(fp1);
239
240  //tmpRefinement1 = array_alloc(char *,0);
241  /* generate sufficient refinement */
242  st_free_table(localSufAbsTable);
243  localSufAbsTable = st_init_table(st_ptrcmp,st_ptrhash); 
244  t3 = util_cpu_ctime();
245  tmpRefinement1 = PureSatGetLatchFromTable(network,pm,coreFile);
246  t4 = util_cpu_ctime();
247  if(pm->verbosity>=2)
248    fprintf(vis_stdout,"time for PureSatGetLatchFromTable: %g\n",(double)((t4-t3)/1000.0));
249 
250  if(array_n(tmpRefinement1)>array_n(oriSufArray)){
251    array_free(tmpRefinement1);
252    tmpRefinement1 = array_dup(oriSufArray);
253  }
254  else{
255    array_free(oriSufArray);
256    oriSufArray = array_dup(tmpRefinement1);
257  }
258  if(pm->verbosity>=2)
259    fprintf(vis_stdout,"All latches picked from UNSAT Proof:\n");
260  arrayForEachItem(char *,tmpRefinement1,i,name){
261    if(pm->verbosity>=2)
262      fprintf(vis_stdout," %s  ",name);
263    latch = Ntk_NetworkFindNodeByName(network,name);
264    st_insert(localSufAbsTable,latch,(char *)0);
265  }
266  if(pm->verbosity>=2){
267    fprintf(vis_stdout,"\n");
268    fprintf(vis_stdout,"tmpModel: \n");
269  }
270  arrayForEachItem(char *,tmpModel,i,name){
271    if(pm->verbosity>=2)
272      fprintf(vis_stdout," %s  ",name);
273    latch = Ntk_NetworkFindNodeByName(network,name);
274    st_insert(localSufAbsTable,latch,(char *)0);
275  }
276  if(pm->verbosity>=2)
277    fprintf(vis_stdout,"\n");
278  newNumOfLatchInCore = array_n(tmpRefinement1);
279  BmcCnfClausesFree(pism->cnfClauses);
280 
281  if(pm->verbosity>=2)
282    fprintf(vis_stdout,"newNumOfLatchInCore/oldNumOfLatchInCore=%f\n",(double)newNumOfLatchInCore/(double)oldNumOfLatchInCore);
283 
284  /* Add the refinement to vertexTable*/
285  arrayForEachItem(char *,tmpRefinement1,i,name){
286    st_insert(vertexTable, name,(char*)0);
287  }
288 
289  pism->cnfClauses = BmcCnfClausesAlloc();
290  cnfClauses = pism->cnfClauses;
291  if(array_n(tmpRefinement1)) 
292    {
293      tmpRefinement = PureSatGenerateRingFromAbs(network,pm,tmpRefinement1,&NumInSecondLevel);
294      /* latchThreshHold = (latchThreshHold <= NumInSecondLevel) ? latchThreshHold:NumInSecondLevel;*/
295      array_free(tmpRefinement1);
296      LatchFromCore = TRUE;
297      for(i=0;i<array_n(tmpRefinement);i=i+latchThreshHold)
298        {
299          for(j=0;j<latchThreshHold;j++)
300            {
301              if((i+j)<array_n(tmpRefinement))
302                {
303                  name = array_fetch(char *,tmpRefinement,i+j);
304                  array_insert_last(char *,tmpRefinement3,name);
305                  if(pm->verbosity>=1)
306                    fprintf(vis_stdout, "picking %s\n",name);
307                }
308              else
309                break;
310            }
311          tmpRefinement2=array_dup(tmpModel);
312          array_append(tmpRefinement2,tmpRefinement3);
313          if(!PureSatExistCE(network,pism,option2,tmpRefinement2,property,pm,0)){
314            VarInCoreIsEnough = TRUE;
315            array_free(tmpRefinement2);
316            for(k=i+j;k<array_n(tmpRefinement);k++)
317              {
318                name = array_fetch(char *,tmpRefinement,k);
319                if(st_lookup(vertexTable,name,NIL(char *))){
320                  st_delete(vertexTable,&name,NIL(char *));
321                }
322              }
323            break;
324          }
325          firstTime = FALSE;
326          beginPosition = array_n(tmpRefinement2);
327          array_free(tmpRefinement2);
328          oldLength = Length;
329        } 
330      array_free(tmpRefinement);
331      tmpRefinement = array_dup(tmpRefinement3); /* now tmpRefinement1 contains the
332                                                   latches in Core*/
333      array_free(tmpRefinement3);
334      oldLength=0;
335      beginPosition=0;
336      BmcCnfClausesFree(pism->cnfClauses);
337      pism->cnfClauses = BmcCnfClausesAlloc();
338    }
339 
340#if 1
341  if(!VarInCoreIsEnough){
342    fprintf(vis_stderr,"this should never happen, wrong\n");
343    exit(0);
344  }
345#endif
346 
347  //tmpRefinement = array_dup(tmpRefinement1);
348  //array_free(tmpRefinement1);
349 
350# if 1
351  /*Refinement Minimization
352    try all the candidates*/
353  for(i=array_n(tmpRefinement)-1;i>=0;i--)
354    {
355      name = array_fetch(char *,tmpRefinement,i);
356      if(pm->verbosity>=1)
357        fprintf(vis_stdout,"RefMin: testing %s\n",name);
358      tmpArray2 = PureSatRemove_char(tmpRefinement,i);
359      tmpArray1 = array_dup(tmpModel);
360      array_append(tmpArray1,tmpArray2);
361      cnfstate = BmcCnfClausesFreeze(pism->cnfClauses);
362      if(PureSatExistCE(network,pism,option2,tmpArray1,property,pm,0))
363        array_free(tmpArray2);
364      else /*delete it*/
365        {
366          /*   i--;*/
367          name = array_fetch(char *, tmpRefinement,i);
368          if(st_lookup(vertexTable, name,NIL(char *)))
369            st_delete(vertexTable, &name, NIL(char *));
370          else
371            fprintf(vis_stderr," %s should be in vertexTable, Wrong!!!\n",name);
372          array_free(tmpRefinement);
373          tmpRefinement = tmpArray2;
374        }
375      array_free(tmpArray1);
376      BmcCnfClausesRestore(pism->cnfClauses, cnfstate);
377      FREE(cnfstate);
378    }
379  //BmcCnfClausesFree(pism->cnfClauses);
380#endif
381 
382  if(pm->verbosity>=1){
383    fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
384    arrayForEachItem(char *,tmpRefinement,i,name)
385      fprintf(vis_stdout,"%s\n",name);
386  }
387  BmcOptionFree(option2);
388  BmcOptionFree(options);
389  unlink(coreFile);
390  unlink(tmpCoreFile);
391  FREE(coreFile);
392  FREE(tmpCoreFile);
393  array_free(oriSufArray);
394  st_free_table(pm->ClsidxToLatchTable);
395  pm->ClsidxToLatchTable = NIL(st_table);
396  PureSatIncreSATManagerFree(pm,pism);
397  return tmpRefinement;
398}
399
400
401/*---------------------------------------------------------------------------*/
402/* Definition of static functions                                            */
403/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.