source: vis_dev/vis-2.3/src/puresat/puresatFlatIP.c @ 14

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

vis2.3
File size: 14.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [puresatFlatIP.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 "maigInt.h"
49#include "puresatInt.h"
50/*---------------------------------------------------------------------------*/
51/* Constant declarations                                                     */
52/*---------------------------------------------------------------------------*/
53
54/*---------------------------------------------------------------------------*/
55/* Type declarations                                                         */
56/*---------------------------------------------------------------------------*/
57
58
59/*---------------------------------------------------------------------------*/
60/* Structure declarations                                                    */
61/*---------------------------------------------------------------------------*/
62
63
64/*---------------------------------------------------------------------------*/
65/* Variable declarations                                                     */
66/*---------------------------------------------------------------------------*/
67
68/*---------------------------------------------------------------------------*/
69/* Macro declarations                                                        */
70/*---------------------------------------------------------------------------*/
71
72/**AutomaticStart*************************************************************/
73
74/*---------------------------------------------------------------------------*/
75/* Static function prototypes                                                */
76/*---------------------------------------------------------------------------*/
77
78
79/**AutomaticEnd***************************************************************/
80
81/*---------------------------------------------------------------------------*/
82/* Definition of exported functions                                          */
83/*---------------------------------------------------------------------------*/
84
85
86/*---------------------------------------------------------------------------*/
87/* Definition of internal functions                                          */
88/*---------------------------------------------------------------------------*/
89/**Function********************************************************************
90
91  Synopsis    []
92
93  Description []
94
95  SideEffects []
96
97  SeeAlso     []
98
99******************************************************************************/
100
101
102/**Function********************************************************************
103
104  Synopsis    [Interpolation algorithm without abstraction refinement]
105
106  Description [Interpolation algorithm without abstraction refinement]
107
108  SideEffects []
109
110  SeeAlso     []
111
112******************************************************************************/
113
114boolean PureSatCheckInv_FlatIP(Ntk_Network_t * network,
115                               Ctlsp_Formula_t *ltlFormula,
116                               PureSat_Manager_t *pm)
117{
118  int NumofCurrentLatch=0,k;
119  bAig_Manager_t    *manager;
120  bAigEdge_t        property;
121  st_table * nodeToMvfAigTable;
122  double t1,t2,t0;
123  int first;
124  array_t           *previousResultArray;
125  BmcOption_t  *options = BmcOptionAlloc();
126  IP_Manager_t * ipm = IPManagerAlloc();
127  boolean firstTime;
128  int round=0, oldLength=0, nodes_in_coi=0;
129  st_table * tmpTable;
130  int oldPos1;
131  satManager_t * cm;
132  bAigEdge_t state, tmpState;
133  double tIP=0,tCon=0,tUnsat=0;
134  RTManager_t *rm;
135
136
137  pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
138  PureSatBmcGetCoiForLtlFormula(network, ltlFormula,pm->CoiTable);
139  ipm->CoiTable = pm->CoiTable;
140
141  options->printInputs = pm->printInputs;
142  options->dbgOut = pm->dbgOut;
143  pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
144  t0 = util_cpu_ctime();
145  NumofCurrentLatch=0;
146  t1 = util_cpu_ctime();
147  PureSatBmcGetCoiForLtlFormula_New(network, ltlFormula,pm->CoiTable);
148  t2 = util_cpu_ctime();
149
150  manager = Ntk_NetworkReadMAigManager(network);
151  if (manager == NIL(mAig_Manager_t)) {
152    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
153    BmcOptionFree(options);
154    return 1;
155  }
156 nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
157                                                         MVFAIG_NETWORK_APPL_KEY);
158
159 previousResultArray    = array_alloc(bAigEdge_t, 0);
160 first = 0;
161 manager->ipm = ipm;
162 t1 = util_cpu_ctime();
163 manager->test2LevelMini = 1;
164 bAig_PureSat_InitTimeFrame(network,manager,pm,0);
165 manager->test2LevelMini = 0;
166 if(pm->verbosity>=1) {
167   fprintf(vis_stdout,"after Init timeframe:\n");
168   PureSat_PrintAigStatus(manager);
169 }
170 manager->class_ = 1;
171 manager->test2LevelMini = 0;
172 property = PureSatCreatebAigOfPropFormula(network,
173            manager, 0, ltlFormula, BMC_NO_INITIAL_STATES);
174 property = bAig_Not(property);
175 if(property==0)
176   return TRUE;
177 if(property==1)
178   return FALSE;
179 manager->assertArray = sat_ArrayAlloc(1);
180 sat_ArrayInsert(manager->assertArray,manager->InitState);
181 cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
182 cm->option->coreGeneration = 0;
183 cm->option->IP = 0;
184 if(pm->verbosity>=1)
185   fprintf(vis_stdout,"test length 0\n");
186 sat_Main(cm);
187 manager->NodesArray = cm->nodesArray;
188 if(cm->status==SAT_SAT){
189   if(pm->dbgLevel == 1){
190     fprintf(vis_stdout,"find counter example of length 0\n");
191     BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
192                                0, 0,options, BMC_NO_INITIAL_STATES);
193   }
194   if(pm->dbgLevel == 2){
195     BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, pm->CoiTable,
196                                0, 0,options, BMC_NO_INITIAL_STATES);
197   }
198   return FALSE;
199 }
200 cm->option->coreGeneration = 1;
201 PureSat_SatFreeManager(cm);
202
203 manager->test2LevelMini = 1;
204 bAig_PureSat_ExpandTimeFrame(network, manager,pm,1, BMC_NO_INITIAL_STATES);
205  manager->class_ = 2;
206 manager->test2LevelMini = 0;
207 property = PureSatCreatebAigOfPropFormula(network,
208                manager, 1, ltlFormula, BMC_NO_INITIAL_STATES);
209 property = bAig_Not(property);
210 if(property==0)
211   return TRUE;
212 if(property==1)
213   return FALSE;
214 if(pm->verbosity>=1) {
215   fprintf(vis_stdout,"after Init timeframe:\n");
216   PureSat_PrintAigStatus(manager);
217 }
218 state = manager->InitState;
219
220
221 cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
222 cm->option->coreGeneration = 0;
223 cm->option->IP = 0;
224 if(pm->verbosity>=1) {
225  fprintf(vis_stdout,"test length 1\n");
226 }
227 sat_Main(cm);
228 manager->NodesArray = cm->nodesArray;
229  if(cm->status==SAT_SAT){
230   if(pm->dbgLevel == 1){
231     fprintf(vis_stdout,"find counter example of length 1\n");
232     BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
233                        1, 0,options, BMC_NO_INITIAL_STATES);
234   }
235   if(pm->dbgLevel == 2){
236     BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, pm->CoiTable,
237                        1, 0,options, BMC_NO_INITIAL_STATES);
238   }
239   return FALSE;
240 }
241 cm->option->coreGeneration = 1;
242 PureSat_SatFreeManager(cm);
243
244 t2 = util_cpu_ctime();
245 if(pm->verbosity>=2)
246   fprintf(vis_stdout,"Time for testing Length 0 and 1: %g\n",(double)((t2-t1)/1000.0));
247
248 pm->Length = k;
249 k = 1;
250 PureSat_CleanMask(manager,ResetGlobalVarMask);
251 PureSat_MarkGlobalVar(manager,1);
252 while(1){
253   oldLength = k;
254   if(k==1)
255     k++;
256   else
257     k += round-1;
258   pm->Length = k;
259   if(pm->verbosity>=1)
260     fprintf(vis_stdout,"\nk = %d InitState = %ld\n",k,manager->InitState);
261   manager->test2LevelMini = 1;
262   bAig_PureSat_ExpandTimeFrame(network, manager,pm, k, BMC_NO_INITIAL_STATES);
263   manager->test2LevelMini = 0;
264   if(pm->verbosity>=1) {
265     fprintf(vis_stdout,"After expand TF\n");
266     PureSat_PrintAigStatus(manager);
267   }
268
269   /*build property aig nodes*/
270   manager->class_ = k+1;
271   property = PureSatCreatebAigOfPropFormula(network,
272              manager, k, ltlFormula, BMC_NO_INITIAL_STATES);
273   property = bAig_Not(property);
274   if(property==0)
275     return TRUE;
276   if(property==1)
277     return FALSE;
278   oldPos1 = manager->nodesArraySize-bAigNodeSize;
279   if(pm->verbosity>=1) {
280     fprintf(vis_stdout,"After expanding TF and building property\n");
281     PureSat_PrintAigStatus(manager);
282   }
283   firstTime = TRUE;
284   round = 0;
285   state = manager->InitState;
286
287   while(1){
288     round++;
289     if(pm->verbosity>=1)
290       fprintf(vis_stdout,"round:%d for k = %d\n",round,k);
291     manager->assertArray = sat_ArrayAlloc(1);
292     if(state!=bAig_One)
293       sat_ArrayInsert(manager->assertArray,state);
294     cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
295
296     if(cm->status==0){
297       if(pm->verbosity>=1)
298         fprintf(vis_stdout,"normal COI:\n");
299       nodes_in_coi = PureSat_CountNodesInCoi(cm);
300       if(pm->verbosity>=2)
301         fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
302       t1 = util_cpu_ctime();
303       sat_Main(cm);
304       if(pm->verbosity>=2)
305         sat_ReportStatistics(cm,cm->each);
306
307       rm = cm->rm;
308       t2 = util_cpu_ctime();
309       tUnsat = tUnsat+t2-t1;
310       if(pm->verbosity>=2)
311         fprintf(vis_stdout,"time for Unsat:%g, Total:%g\n",
312                (double)((t2-t1)/1000.0),tUnsat/1000);
313       if(manager->NodesArray!=cm->nodesArray)
314         /*cm->nodesArray may be reallocated */
315         manager->NodesArray = cm->nodesArray;
316     }
317
318     if(cm->status == SAT_SAT){
319       /*SAT: first time->find bug, otherwise increase length*/
320       if(firstTime){
321         if(pm->dbgLevel == 1){
322           fprintf(vis_stdout,"found CEX of length %d\n",k);
323           BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
324                      k, 0,options, BMC_NO_INITIAL_STATES);
325         }
326         if(pm->dbgLevel == 2){
327           BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, pm->CoiTable,
328                      k, 0,options, BMC_NO_INITIAL_STATES);
329         }
330         sat_ArrayFree(manager->assertArray);
331         manager->assertArray = 0;
332         RT_Free(cm->rm);
333         PureSat_SatFreeManager(cm);
334         return FALSE;
335       }
336       /*find bogus bug, abort, increase length*/
337       else{
338         /* BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
339                                      k, 0,options, BMC_NO_INITIAL_STATES);*/
340         if(pm->verbosity>=1)
341           fprintf(vis_stdout,"find bogus bug at length k=%d,round=%d,increase length\n",k,round);
342
343         sat_ArrayFree(manager->assertArray);
344         RT_Free(cm->rm);
345         PureSat_SatFreeManager(cm);
346         break;
347       }
348     }
349     else{
350       /*UNSAT: get IP, add to init states, until reach convergence, which
351         means property is true
352         IP generation*/
353       assert(cm->currentDecision>=-1);
354       if(cm->currentDecision!=-1)
355         sat_Backtrack(cm, -1);
356       /*get rid of Conflict Clauses*/
357       PureSat_ResetManager(manager,cm,0);
358
359       /*Generate interpolant and test convergence*/
360       if(cm->option->coreGeneration&&cm->status == SAT_UNSAT){
361         manager->class_ = 1;
362         t1 = util_cpu_ctime();
363         tmpState = sat_GenerateFwdIP(manager,cm,cm->rm->root,1);
364         manager->IPState = PureSat_MapIP(manager,tmpState,1,0);
365         ResetRTree(rm);
366
367         /*Wheneven there is baigNode generated, Reset_Manager is necessary,
368           since NodeArray may be reallocated, # of Nodes changed*/
369         PureSat_ResetManager(manager,cm,0);
370         t2 = util_cpu_ctime();
371         tIP = tIP+t2-t1;
372         if(pm->verbosity>=2)
373           fprintf(vis_stdout,"time for generating IP:%g, Total:%g\n",
374                  (double)((t2-t1)/1000.0),tIP/1000);
375         if(pm->verbosity>=1){
376           fprintf(vis_stdout,"After generate IP,%ld:\n",manager->IPState);
377           PureSat_PrintAigStatus(manager);
378         }
379         manager->class_ = 2;
380         t1 = util_cpu_ctime();
381         RT_Free(cm->rm);
382         if(pm->verbosity>=1)
383           PureSat_PrintAigStatus(manager);
384
385         PureSat_ResetManager(manager,cm,0);
386       }
387
388       t1 = util_cpu_ctime();
389
390       /*Convergence test for interpolation*/
391       if(PureSat_TestConvergeForIP(manager,pm,cm,state,manager->IPState)){
392         t2 = util_cpu_ctime();
393         tCon = tCon+t2-t1;
394         if(pm->verbosity>=2)
395           fprintf(vis_stdout,"time for generating Convergence:%g, Total:%g\n",
396                  (double)((t2-t1)/1000.0),tCon/1000);
397         if(pm->verbosity>=1){
398           fprintf(vis_stdout,"After test convergence:\n");
399           PureSat_PrintAigStatus(manager);
400         }
401         fprintf(vis_stdout,"property is true\n");
402         PureSat_SatFreeManager(cm);
403         return TRUE;
404       }
405       else{
406         t2 = util_cpu_ctime();
407         tCon = tCon+t2-t1;
408         if(pm->verbosity>=2)
409           fprintf(vis_stdout,"time for generating Convergence:%g, Total:%g\n",
410                  (double)((t2-t1)/1000.0),tCon/1000);
411         if(pm->verbosity>=1){
412           fprintf(vis_stdout,"After test convergence:\n");
413           PureSat_PrintAigStatus(manager);
414         }
415         manager->class_ = 0;
416         state = PureSat_Or(manager,state,manager->IPState);
417         PureSat_ResetManager(manager,cm,0);
418         if(pm->verbosity>=1)
419           fprintf(vis_stdout,"new InitState:%ld\n",state);
420       }
421     }/*else*/
422     sat_ArrayFree(manager->assertArray);
423     manager->assertArray = 0;
424     PureSat_SatFreeManager(cm);
425     firstTime = FALSE;
426   }/*inner While(1){*/
427 }/*outer While(1){*/
428 st_free_table(tmpTable);
429
430 sat_ArrayFree(manager->EqArray);
431 return TRUE;
432}
Note: See TracBrowser for help on using the repository browser.