source: vis_dev/vis-2.3/src/puresat/puresatBMC.c @ 84

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

vis2.3
File size: 53.3 KB
RevLine 
[14]1/**CFile***********************************************************************
2
3  FileName    [puresatMain.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    [Insert clauses of (Si!=Sj) for k-induction checking]
91
92  Description [Insert clauses of (Si!=Sj) for k-induction checking]
93
94  SideEffects []
95
96  SeeAlso     []
97
98******************************************************************************/
99
100void PureSatInsertNewClauseForSimplePath(array_t *vertexArray,
101                                         Ntk_Network_t *network,
102                                         int step1,
103                                         int step2,
104                                         BmcCnfClauses_t *cnfClauses,
105                                         st_table *nodeToMvfAigTable)
106{
107  int i,j,k,mvfSize,index1,index2, cnfIndex;
108  Ntk_Node_t * latch;
109  MvfAig_Function_t *latchMvfAig;
110  bAigEdge_t * latchBAig;
111  array_t * tmpclause, *clauseArray, * clause, * clause1,*latchClause;
112  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
113  char * Name;
114  boolean nextLatch = FALSE;
115
116  latchClause = array_alloc(int,0);
117  arrayForEachItem(char *,vertexArray,j,Name)
118    {
119      nextLatch = FALSE;
120      clause = array_alloc(int,0); /*(-A + -A1 + -A2 + -A3)*/
121      clauseArray  = array_alloc(array_t *,0);/*(A + -A1)(A + -A2)(A + -A3)*/
122      latch = Ntk_NetworkFindNodeByName(network,Name);
123      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
124      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
125        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
126        array_free(latchMvfAig);
127        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
128      }
129      mvfSize   = array_n(latchMvfAig);
130      latchBAig = ALLOC(bAigEdge_t, mvfSize); 
131
132      for(i=0; i< mvfSize; i++){
133        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
134        }
135      for(i=0; i< mvfSize; i++){
136        if (latchBAig[i] == bAig_One)
137          nextLatch=TRUE;break;   /* the clause is always true */
138      }
139
140      if(!nextLatch)
141        {
142          for(i=0; i< mvfSize; i++){
143            latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
144            index1 = BmcGenerateCnfFormulaForAigFunction(manager,latchBAig[i],step1,cnfClauses);
145            index2 = BmcGenerateCnfFormulaForAigFunction(manager,latchBAig[i],step2,cnfClauses);
146           
147            cnfIndex = cnfClauses->cnfGlobalIndex++; 
148            tmpclause  = array_alloc(int, 3);
149            array_insert(int, tmpclause, 0, -index2);
150            array_insert(int, tmpclause, 1, -index1);
151            array_insert(int, tmpclause, 2,  cnfIndex);
152            BmcCnfInsertClause(cnfClauses, tmpclause);
153            array_free(tmpclause);
154           
155            tmpclause  = array_alloc(int, 2);
156            array_insert(int, tmpclause, 0, index2);
157            array_insert(int, tmpclause, 1, -cnfIndex);
158            BmcCnfInsertClause(cnfClauses, tmpclause);
159            array_free(tmpclause);
160           
161            tmpclause  = array_alloc(int, 2);
162            array_insert(int, tmpclause, 0, index1);
163            array_insert(int, tmpclause, 1, -cnfIndex);
164            BmcCnfInsertClause(cnfClauses, tmpclause);
165            array_free(tmpclause);
166           
167            /*(-A + A1 + A2 + A3)*/
168            array_insert_last(int,clause,cnfIndex);
169            /*(A + -A1)(A + -A2)(A + -A3)*/
170            clause1 = array_alloc(int,0);/*(A + -A1/2/3)*/
171            array_insert_last(int,clause1,-cnfIndex);
172            array_insert_last(array_t *,clauseArray,clause1);
173           
174          }
175         
176          cnfIndex = cnfClauses->cnfGlobalIndex++; /*A*/
177          /*(A + -A1)(A + -A2)(A + -A3)*/
178          arrayForEachItem(array_t *,clauseArray,k,clause1)
179            {
180              array_insert_last(int,clause1,cnfIndex);
181              BmcCnfInsertClause(cnfClauses,clause1);
182              array_free(clause1);
183            }
184          array_free(clauseArray);
185         
186          /*(-A + A1 + A2 + A3)*/
187          array_insert_last(int,clause,-cnfIndex);
188          BmcCnfInsertClause(cnfClauses,clause);
189          array_free(clause);
190         
191          /*(C + -A + -B)*/
192          array_insert_last(int,latchClause,-cnfIndex);
193        }
194      FREE(latchBAig);
195    }
196  cnfIndex = cnfClauses->cnfGlobalIndex++; /* C*/
197  array_insert_last(int,latchClause,cnfIndex); /*(C + -A + -B)*/
198  BmcCnfInsertClause(cnfClauses,latchClause);
199  array_free(latchClause);
200 
201  /*(-C)*/
202  latchClause = array_alloc(int,0);
203  array_insert_last(int,latchClause,-cnfIndex);
204  BmcCnfInsertClause(cnfClauses,latchClause);
205  array_free(latchClause);
206}
207
208
209/**Function********************************************************************
210
211  Synopsis    [Insert clauses of (Si!=I) for k-induction checking]
212
213  Description [Insert clauses of (Si!=I) for k-induction checking]
214
215  SideEffects []
216
217  SeeAlso     []
218
219******************************************************************************/
220
221void PureSatInsertNewClauseForInit(array_t *vertexArray,
222                               Ntk_Network_t *network,
223                               int step1,
224                               int step2,
225                               BmcCnfClauses_t *cnfClauses,
226                               st_table *nodeToMvfAigTable)
227{
228  int i,j,k,mvfSize,index1=0,index2=0, cnfIndex;
229  Ntk_Node_t * latch, *latchInit;
230  MvfAig_Function_t *initMvfAig,*latchMvfAig;
231  bAigEdge_t * latchBAig,* initBAig;
232  array_t * tmpclause, *clauseArray, * clause, * clause1,*latchClause;
233  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
234  char * Name;
235  boolean nextLatch = FALSE;
236
237  latchClause = array_alloc(int,0);
238  arrayForEachItem(char *,vertexArray,j,Name)
239    {
240      nextLatch = FALSE;
241      clause = array_alloc(int,0); /*(-A + -A1 + -A2 + -A3)*/
242      clauseArray  = array_alloc(array_t *,0);/*(A + -A1)(A + -A2)(A + -A3)*/
243      latch = Ntk_NetworkFindNodeByName(network,Name);
244      latchInit  = Ntk_LatchReadInitialInput(latch);
245      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
246      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
247        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
248        array_free(latchMvfAig);
249        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
250      }
251      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
252
253       
254      mvfSize   = array_n(latchMvfAig);
255      latchBAig = ALLOC(bAigEdge_t, mvfSize); 
256      initBAig  = ALLOC(bAigEdge_t, mvfSize);
257      /* printf("mvfSize = %d \n",mvfSize);*/
258
259      for(i=0; i< mvfSize; i++){
260        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
261        initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
262        }
263     
264      for(i=0; i< mvfSize; i++){
265        if ((initBAig[i] == bAig_One) && (latchBAig[i] == bAig_One))
266         {
267           nextLatch=TRUE;
268           break;   /* the clause is always true */
269         }
270      }
271
272     
273      if(!nextLatch)
274        {
275          for(i=0; i< mvfSize; i++){
276            initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
277            latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
278            if(initBAig[i]==bAig_Zero ||latchBAig[i]==bAig_Zero)
279              {
280                continue;
281              }
282            if(initBAig[i]!=bAig_One)
283              {
284                index1 = BmcGenerateCnfFormulaForAigFunction(manager,initBAig[i],step1,cnfClauses);
285              }
286            if(latchBAig[i]!=bAig_One)
287              {
288                index2 = BmcGenerateCnfFormulaForAigFunction(manager,latchBAig[i],step2,cnfClauses);
289              }
290           
291            cnfIndex = cnfClauses->cnfGlobalIndex++;
292            if (initBAig[i] == bAig_One){
293              tmpclause  = array_alloc(int, 2);
294              array_insert(int, tmpclause, 0, -index2);
295              array_insert(int, tmpclause, 1, cnfIndex);
296              BmcCnfInsertClause(cnfClauses, tmpclause);
297              array_free(tmpclause); 
298             
299              tmpclause  = array_alloc(int, 2);
300              array_insert(int, tmpclause, 0, index2);
301              array_insert(int, tmpclause, 1, -cnfIndex);
302              BmcCnfInsertClause(cnfClauses, tmpclause);
303              array_free(tmpclause);       
304             
305            } else if (latchBAig[i] == bAig_One){
306              tmpclause  = array_alloc(int, 2);
307              array_insert(int, tmpclause, 0, -index1);
308              array_insert(int, tmpclause, 1, cnfIndex);
309              BmcCnfInsertClause(cnfClauses, tmpclause);
310              array_free(tmpclause);
311             
312              tmpclause  = array_alloc(int, 2);
313              array_insert(int, tmpclause, 0, index1);
314              array_insert(int, tmpclause, 1, -cnfIndex);
315              BmcCnfInsertClause(cnfClauses, tmpclause);
316              array_free(tmpclause);
317             
318            } else {
319            tmpclause  = array_alloc(int, 3);
320            array_insert(int, tmpclause, 0, -index2);
321            array_insert(int, tmpclause, 1, -index1);
322            array_insert(int, tmpclause, 2,  cnfIndex);
323            BmcCnfInsertClause(cnfClauses, tmpclause);
324            array_free(tmpclause);
325           
326            tmpclause  = array_alloc(int, 2);
327            array_insert(int, tmpclause, 0, index2);
328            array_insert(int, tmpclause, 1, -cnfIndex);
329            BmcCnfInsertClause(cnfClauses, tmpclause);
330            array_free(tmpclause);
331           
332            tmpclause  = array_alloc(int, 2);
333            array_insert(int, tmpclause, 0, index1);
334            array_insert(int, tmpclause, 1, -cnfIndex);
335            BmcCnfInsertClause(cnfClauses, tmpclause);
336            array_free(tmpclause);
337            }
338            /*(-A + A1 + A2 + A3)*/
339            array_insert_last(int,clause,cnfIndex);
340            /*(A + -A1)(A + -A2)(A + -A3)*/
341            clause1 = array_alloc(int,0);/*(A + -A1/2/3)*/
342            array_insert_last(int,clause1,-cnfIndex);
343            array_insert_last(array_t *,clauseArray,clause1);
344           
345          }/* for(i=0; i< mvfSize;*/
346         
347          cnfIndex = cnfClauses->cnfGlobalIndex++; /*A*/
348          /*(A + -A1)(A + -A2)(A + -A3)*/
349          arrayForEachItem(array_t *,clauseArray,k,clause1)
350            {
351              array_insert_last(int,clause1,cnfIndex);
352              BmcCnfInsertClause(cnfClauses,clause1);
353              array_free(clause1);
354            }
355          array_free(clauseArray);
356         
357          /*(-A + A1 + A2 + A3)*/
358          array_insert_last(int,clause,-cnfIndex);
359          BmcCnfInsertClause(cnfClauses,clause);
360          array_free(clause);
361         
362          /*(C + -A + -B)*/
363          array_insert_last(int,latchClause,-cnfIndex);
364        }/* if(!nextLatch)*/
365      FREE(latchBAig); 
366      FREE(initBAig);
367    }/*arrayForEach..*/
368  cnfIndex = cnfClauses->cnfGlobalIndex++; /* C*/
369  array_insert_last(int,latchClause,cnfIndex); /*(C + -A + -B)*/
370  BmcCnfInsertClause(cnfClauses,latchClause);
371  array_free(latchClause);
372 
373  /*(-C)*/
374  latchClause = array_alloc(int,0);
375  array_insert_last(int,latchClause,-cnfIndex);
376  BmcCnfInsertClause(cnfClauses,latchClause);
377  array_free(latchClause);
378}
379
380
381/**Function********************************************************************
382
383  Synopsis    [Insert clauses of initial states for k-induction checking]
384
385  Description [Insert clauses of initial states for k-induction checking]
386
387  SideEffects []
388
389  SeeAlso     []
390
391******************************************************************************/
392void PureSatSetInitStatesForSimplePath(array_t * vertexArray,
393                          Ntk_Network_t *network,
394                          BmcCnfClauses_t *cnfClauses,
395                          st_table * nodeToMvfAigTable)
396{
397  mAig_Manager_t  *maigManager   = Ntk_NetworkReadMAigManager(network);
398  Ntk_Node_t         *latch, *latchInit;
399  MvfAig_Function_t  *initMvfAig, *latchMvfAig;
400  bAigEdge_t         *initBAig, *latchBAig;
401  int                i,j, mvfSize;
402  char               *nodeName;
403 
404  for(j=0;j<array_n(vertexArray);j++)
405    {
406      nodeName = array_fetch(char *,vertexArray,j);
407      latch = Ntk_NetworkFindNodeByName(network,nodeName);
408      latchInit  = Ntk_LatchReadInitialInput(latch);
409      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
410      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
411      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
412        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
413        array_free(latchMvfAig);
414        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
415      }
416     
417      mvfSize   = array_n(initMvfAig);
418      initBAig  = ALLOC(bAigEdge_t, mvfSize);
419      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
420     
421      for(i=0; i< mvfSize; i++){
422        latchBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(latchMvfAig, i));
423        initBAig[i]  = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(initMvfAig,  i));
424      }
425      BmcGenerateClausesFromStateTostate(maigManager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
426      FREE(initBAig);
427      FREE(latchBAig);
428    } 
429}
430
431
432/**Function********************************************************************
433
434  Synopsis    [k-induction checking from SSS'00 FMCAD paper ]
435
436  Description [k-induction checking from SSS'00 FMCAD paper ]
437
438  SideEffects []
439
440  SeeAlso     []
441
442******************************************************************************/
443boolean PureSatExistASimplePath(Ntk_Network_t *network,
444                              PureSat_IncreSATManager_t * pism,
445                              array_t * vertexArray,
446                              bAigEdge_t property,
447                              PureSat_Manager_t * pm)
448{
449  mAig_Manager_t  *maigManager   = Ntk_NetworkReadMAigManager(network);
450  Ntk_Node_t         *latch, *latchData, *latchInit;
451  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
452  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
453  int                i,j, k, mvfSize,propertyIndex;
454  char               *nodeName;
455  array_t            * Pclause = array_alloc(int,0);
456  st_table           *nodeToMvfAigTable;
457  BmcCnfStates_t     *cnfstate1,*cnfstate2;
458  array_t            *supportLatches;
459  int                 status;
460  int beginPosition = pism->beginPosition;
461  int Length = pism->Length;
462  int oldLength = pism->oldLength;
463  BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
464  satManager_t * cm = pism->cm;
465 
466  /* construct loopfree path;*/
467  nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
468  if (nodeToMvfAigTable == NIL(st_table)){
469    (void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
470    exit(0);
471  }
472
473  for(j=beginPosition;j<array_n(vertexArray);j++){
474    nodeName = array_fetch(char *,vertexArray,j);
475    latch = Ntk_NetworkFindNodeByName(network,nodeName);
476    latchInit  = Ntk_LatchReadInitialInput(latch);
477    latchData  = Ntk_LatchReadDataInput(latch);
478    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
479    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
480    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
481   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
482     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
483     array_free(latchMvfAig);
484     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
485   }
486   
487    mvfSize   = array_n(initMvfAig);
488    initBAig  = ALLOC(bAigEdge_t, mvfSize);
489    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
490    latchBAig = ALLOC(bAigEdge_t, mvfSize);
491   
492    for(i=0; i< mvfSize; i++){
493      dataBAig[i]  = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
494      latchBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(latchMvfAig, i));
495      initBAig[i]  = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(initMvfAig,  i));
496    }
497   
498    /* BmcGenerateClausesFromStateTostate(maigManager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);*/
499    for (k=0; k < oldLength; k++){
500      BmcGenerateClausesFromStateTostate(maigManager, dataBAig,latchBAig, mvfSize, k, k+1, cnfClauses, 0);
501    }
502    FREE(initBAig);
503    FREE(dataBAig);
504    FREE(latchBAig);
505  } /*st_foreach_item(vertexTable,*/
506
507  if(oldLength<Length){
508    for(j=0;j<array_n(vertexArray);j++){
509      nodeName = array_fetch(char *,vertexArray,j);
510      latch = Ntk_NetworkFindNodeByName(network,nodeName);
511      latchInit  = Ntk_LatchReadInitialInput(latch);
512      latchData  = Ntk_LatchReadDataInput(latch);
513      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
514      dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
515      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
516   
517      mvfSize   = array_n(initMvfAig);
518      initBAig  = ALLOC(bAigEdge_t, mvfSize);
519      dataBAig  = ALLOC(bAigEdge_t, mvfSize);
520      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
521     
522      for(i=0; i< mvfSize; i++){
523        dataBAig[i]  = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
524        latchBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(latchMvfAig, i));
525        initBAig[i]  = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(initMvfAig,  i));
526      }
527     
528      for (k=oldLength; k <Length; k++){
529        BmcGenerateClausesFromStateTostate(maigManager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
530      }
531      FREE(initBAig);
532      FREE(dataBAig);
533      FREE(latchBAig);
534    }
535  }/*if(oldLength!=0){*/
536
537  if(pm->verbosity>=1)
538    fprintf(vis_stdout,"forward simple path testing...\n");
539  cnfstate1 = BmcCnfClausesFreeze(cnfClauses);
540 
541  /*generate NODE(i)!=NODE(i+1)*/
542  for(i=1;i<Length;i++)
543    for(j=i+1;j<=Length;j++)
544      PureSatInsertNewClauseForSimplePath(vertexArray,network,i,j,cnfClauses,nodeToMvfAigTable); /*Si!=Sj*/
545 
546  cnfstate2 = BmcCnfClausesFreeze(cnfClauses);
547  supportLatches = PureSatGetImmediateSupportLatches(network, 0, vertexArray);
548  /*I(S0)*/
549  PureSatSetInitStatesForSimplePath(supportLatches/*vertexArray*/,network,cnfClauses,nodeToMvfAigTable);
550  /*generate all.!I(S(1...i)), the first constraint*/
551  for(i=1;i<=Length;i++)
552    PureSatInsertNewClauseForInit(supportLatches/*vertexArray*/,network,-1,i,cnfClauses,nodeToMvfAigTable);
553  array_free(supportLatches);
554
555  pism->propertyPos = cnfstate1->nextIndex;
556  PureSatReadClauses(pism,pm);
557  /*no incremental */
558  if(!pm->incre){
559    if(cm->savedConflictClauses)
560      sat_ArrayFree(cm->savedConflictClauses);
561    cm->savedConflictClauses = 0;
562  }
563  sat_Main(cm);
564  status = cm->status;
565  PureSatCleanSat(cm);
566  BmcCnfClausesRestore(cnfClauses, cnfstate1);
567
568  if(status == SAT_SAT)
569    {
570      if(pm->verbosity>=1)
571        fprintf(vis_stdout,"backward simple path testing...\n");
572      cnfstate2 = BmcCnfClausesFreeze(cnfClauses);
573      /*generate NODE(i)!=NODE(i+1)*/
574      for(i=1;i<Length;i++)
575        for(j=i+1;j<=Length;j++)
576          PureSatInsertNewClauseForSimplePath(vertexArray,network,i,j,cnfClauses,nodeToMvfAigTable);
577      /*!P(S(i))*/
578      propertyIndex =  BmcGenerateCnfFormulaForAigFunction(maigManager,property, Length, cnfClauses);
579      array_insert_last(int, Pclause,propertyIndex);
580      BmcCnfInsertClause(cnfClauses, Pclause);
581      array_free(Pclause);
582      /*all.P(S(0,...i-1))*/
583      property = bAig_Not(property);
584      for(k=0; k <= Length-1; k++){
585        propertyIndex =  BmcGenerateCnfFormulaForAigFunction(maigManager,property,k, cnfClauses);
586        Pclause = array_alloc(int,0);
587        array_insert_last(int, Pclause, propertyIndex);
588        BmcCnfInsertClause(cnfClauses, Pclause);
589        array_free(Pclause);
590      }
591
592      pism->propertyPos = cnfstate2->nextIndex;
593      PureSatReadClauses(pism,pm);
594      /*no incremental */
595      if(!pm->incre){
596        if(cm->savedConflictClauses)
597          sat_ArrayFree(cm->savedConflictClauses);
598        cm->savedConflictClauses = 0;
599      }
600      sat_Main(cm);
601      status = cm->status;
602      PureSatCleanSat(cm);
603      if(status == SAT_SAT)
604        {
605          BmcCnfClausesRestore(cnfClauses, cnfstate1);
606          FREE(cnfstate1);
607          FREE(cnfstate2);
608          return TRUE;
609        }
610    }
611  FREE(cnfstate1);
612  FREE(cnfstate2);
613  return  FALSE;
614}
615
616/**Function********************************************************************
617
618  Synopsis    [checking the existence of a path of certain length]
619
620  Description [checking the existence of a path of certain length ]
621
622  SideEffects []
623
624  SeeAlso     []
625
626******************************************************************************/
627
628boolean PureSatExistCE(Ntk_Network_t * network,
629                       PureSat_IncreSATManager_t * pism,
630                       BmcOption_t *options,
631                       array_t *vertexArray,
632                       bAigEdge_t property,
633                       PureSat_Manager_t * pm,
634                       int extractCexInfo)
635{
636  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
637  Ntk_Node_t         *latch, *latchData, *latchInit;
638  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
639  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
640  int                i,j, k, mvfSize;
641  char               *nodeName;
642  array_t            *result;
643  array_t            *Pclause = array_alloc(int, 0);
644  FILE               *cnfFile;
645  st_table           *nodeToMvfAigTable;
646  BmcCnfStates_t    *cnfstate;
647  int beginPosition = pism->beginPosition;
648  int oldLength = pism->oldLength;
649  int Length = pism->Length;
650  BmcCnfClauses_t *cnfClauses = pism->cnfClauses;
651
652  double t2, t1 = util_cpu_ctime();
653
654  options->verbosityLevel = (Bmc_VerbosityLevel) pm->verbosity;
655  nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
656  if (nodeToMvfAigTable == NIL(st_table)){
657    (void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
658    exit(0);
659  }
660
661
662#if 1
663 { 
664   array_t *supportLatches = PureSatGetImmediateSupportLatches(network, beginPosition, vertexArray);
665   arrayForEachItem(char *, supportLatches, j, nodeName) {
666     latch = Ntk_NetworkFindNodeByName(network, nodeName);
667    latchInit  = Ntk_LatchReadInitialInput(latch);
668    latchData  = Ntk_LatchReadDataInput(latch);
669    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
670    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
671    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
672    if (latchMvfAig ==  NIL(MvfAig_Function_t)){
673      latchMvfAig = Bmc_NodeBuildMVF(network, latch);
674      array_free(latchMvfAig);
675      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
676    }
677   
678    mvfSize   = array_n(initMvfAig);
679    initBAig  = ALLOC(bAigEdge_t, mvfSize);
680    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
681    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
682   
683    for(i=0; i< mvfSize; i++){
684      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
685      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
686      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
687    }
688   
689    BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
690    FREE(initBAig);
691    FREE(dataBAig);
692    FREE(latchBAig);
693  }   
694   array_free(supportLatches);
695 }
696
697 
698  for(j=beginPosition;j<array_n(vertexArray);j++){
699    nodeName = array_fetch(char *,vertexArray,j);
700    latch = Ntk_NetworkFindNodeByName(network,nodeName);
701    latchInit  = Ntk_LatchReadInitialInput(latch);
702    latchData  = Ntk_LatchReadDataInput(latch);
703    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
704    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
705    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
706   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
707     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
708     array_free(latchMvfAig);
709     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
710   }
711   
712    mvfSize   = array_n(initMvfAig);
713    initBAig  = ALLOC(bAigEdge_t, mvfSize);
714    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
715    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
716   
717    for(i=0; i< mvfSize; i++){
718      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
719      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
720      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
721    }
722    /* BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);*/
723    for (k=0; k <oldLength; k++){
724      BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
725    }
726    FREE(initBAig);
727    FREE(dataBAig);
728    FREE(latchBAig);
729  } /*st_foreach_item(vertexTable,*/
730#else
731  /*build TR for more latches*/
732 
733  for(j=beginPosition;j<array_n(vertexArray);j++){
734    nodeName = array_fetch(char *,vertexArray,j);
735    latch = Ntk_NetworkFindNodeByName(network,nodeName);
736    latchInit  = Ntk_LatchReadInitialInput(latch);
737    latchData  = Ntk_LatchReadDataInput(latch);
738    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
739    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
740    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
741   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
742     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
743     array_free(latchMvfAig);
744     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
745   }
746   
747    mvfSize   = array_n(initMvfAig);
748    initBAig  = ALLOC(bAigEdge_t, mvfSize);
749    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
750    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
751   
752    for(i=0; i< mvfSize; i++){
753      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
754      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
755      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
756    }
757    BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
758    for (k=0; k <oldLength; k++){
759      BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
760    }
761    FREE(initBAig);
762    FREE(dataBAig);
763    FREE(latchBAig);
764  } /*st_foreach_item(vertexTable,*/
765#endif
766
767  /* for more length*/
768  if(oldLength<Length){
769    for(j=0;j<array_n(vertexArray);j++){
770      nodeName = array_fetch(char *,vertexArray,j);
771      latch = Ntk_NetworkFindNodeByName(network,nodeName);
772      latchInit  = Ntk_LatchReadInitialInput(latch);
773      latchData  = Ntk_LatchReadDataInput(latch);
774      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
775      dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
776      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
777      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
778        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
779        array_free(latchMvfAig);
780        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
781      }
782   
783      mvfSize   = array_n(initMvfAig);
784      initBAig  = ALLOC(bAigEdge_t, mvfSize);
785      dataBAig  = ALLOC(bAigEdge_t, mvfSize);
786      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
787     
788      for(i=0; i< mvfSize; i++){
789        dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
790        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
791        initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
792      }
793     
794      for (k=oldLength; k<Length; k++){
795        BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
796      }
797      FREE(initBAig);
798      FREE(dataBAig);
799      FREE(latchBAig);
800    }
801  }
802 
803
804   k=Length;
805   cnfstate = BmcCnfClausesFreeze(cnfClauses);
806   /* for(k=0; k <= Length; k++){*/
807   array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager, property,k, cnfClauses));
808   /*    } */
809   BmcCnfInsertClause(cnfClauses, Pclause);
810   array_free(Pclause);
811   cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
812   BmcWriteClauses(manager, cnfFile, cnfClauses, options);
813   (void) fclose(cnfFile);
814   result = BmcCheckSAT(options);
815   BmcCnfClausesRestore(cnfClauses, cnfstate);
816   FREE(cnfstate);
817   
818  t2 = util_cpu_ctime();
819  /*timeElapse_Sol += t2-t1;*/
820  if(pm->verbosity>=2)
821    fprintf(vis_stdout, "timeElapse_sol_noIncre: += %g\n", (double)((t2-t1)/1000.0));
822
823 
824  if(extractCexInfo && pm->dbgLevel>=1 && result!=NIL(array_t)){
825    pm->result = array_dup(result);
826  }
827 
828  if(result!=NIL(array_t))
829    {
830      if(pm->verbosity>=2)
831        fprintf(vis_stdout, "find CEX\n");
832      array_free(result);
833      return TRUE;
834    }
835  else
836    {
837      if(pm->verbosity>=2)
838        fprintf(vis_stdout, "didn't find CEX\n");
839       return FALSE;
840    }
841}
842
843/**Function********************************************************************
844
845  Synopsis    [Incrementally checking the existence of a path of certain length]
846
847  Description [Incrementally checking the existence of a path of certain length ]
848
849  SideEffects []
850
851  SeeAlso     []
852
853******************************************************************************/
854
855boolean PureSatIncreExistCE(Ntk_Network_t * network,
856                     PureSat_IncreSATManager_t *pism,
857                     array_t *vertexArray,
858                     bAigEdge_t property,
859                     PureSat_Manager_t * pm)
860{
861  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
862  Ntk_Node_t         *latch, *latchData, *latchInit;
863  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
864  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
865  int                i,j, k, mvfSize;
866  int                status;
867  char               *nodeName;
868  array_t            *Pclause = array_alloc(int, 0);
869  st_table           *nodeToMvfAigTable;
870  BmcCnfStates_t    *cnfstate;
871  int beginPosition = pism->beginPosition;
872  int Length = pism->Length;
873  int oldLength = pism->oldLength;
874  BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
875  satManager_t * cm = pism->cm;
876
877  nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
878  if (nodeToMvfAigTable == NIL(st_table)){
879    (void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
880    exit(0);
881  }
882
883 { 
884   array_t *supportLatches = PureSatGetImmediateSupportLatches(network, beginPosition, vertexArray);
885   arrayForEachItem(char *, supportLatches, j, nodeName) {
886     latch = Ntk_NetworkFindNodeByName(network, nodeName);
887    latchInit  = Ntk_LatchReadInitialInput(latch);
888    latchData  = Ntk_LatchReadDataInput(latch);
889    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
890    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
891    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
892    if (latchMvfAig ==  NIL(MvfAig_Function_t)){
893      latchMvfAig = Bmc_NodeBuildMVF(network, latch);
894      array_free(latchMvfAig);
895      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
896    }
897   
898    mvfSize   = array_n(initMvfAig);
899    initBAig  = ALLOC(bAigEdge_t, mvfSize);
900    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
901    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
902   
903    for(i=0; i< mvfSize; i++){
904      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
905      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
906      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
907    }
908   
909    BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
910    FREE(initBAig);
911    FREE(dataBAig);
912    FREE(latchBAig);
913  } 
914   array_free(supportLatches);
915 }
916 
917  for(j=beginPosition;j<array_n(vertexArray);j++){
918    nodeName = array_fetch(char *,vertexArray,j);
919    latch = Ntk_NetworkFindNodeByName(network,nodeName);
920    latchInit  = Ntk_LatchReadInitialInput(latch);
921    latchData  = Ntk_LatchReadDataInput(latch);
922    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
923    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
924    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
925   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
926     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
927     array_free(latchMvfAig);
928     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
929   }
930   
931    mvfSize   = array_n(initMvfAig);
932    initBAig  = ALLOC(bAigEdge_t, mvfSize);
933    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
934    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
935   
936    for(i=0; i< mvfSize; i++){
937      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
938      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
939      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
940    }
941    BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
942    for (k=0; k <oldLength; k++){
943      BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
944    }
945    FREE(initBAig);
946    FREE(dataBAig);
947    FREE(latchBAig);
948  }
949
950  /* for more length*/
951  if(oldLength<Length){
952    for(j=0;j<array_n(vertexArray);j++){
953      nodeName = array_fetch(char *,vertexArray,j);
954      latch = Ntk_NetworkFindNodeByName(network,nodeName);
955      latchInit  = Ntk_LatchReadInitialInput(latch);
956      latchData  = Ntk_LatchReadDataInput(latch);
957      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
958      dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
959      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
960      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
961        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
962        array_free(latchMvfAig);
963        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
964      }
965   
966      mvfSize   = array_n(initMvfAig);
967      initBAig  = ALLOC(bAigEdge_t, mvfSize);
968      dataBAig  = ALLOC(bAigEdge_t, mvfSize);
969      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
970     
971      for(i=0; i< mvfSize; i++){
972        dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
973        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
974        initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
975      }
976     
977      for (k=oldLength; k<Length; k++){
978        BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
979      }
980      FREE(initBAig);
981      FREE(dataBAig);
982      FREE(latchBAig);
983    }
984  }
985
986   k=Length;
987   cnfstate = BmcCnfClausesFreeze(cnfClauses);
988   /* for(k=0; k <= Length; k++){*/
989   array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager, property,k, cnfClauses));
990   /*    }*/
991   BmcCnfInsertClause(cnfClauses, Pclause);
992   array_free(Pclause);
993   pism->propertyPos = cnfstate->nextIndex;
994   PureSatReadClauses(pism, pm);
995   
996   /*no incremental */
997  if(!pm->incre){
998    if(cm->savedConflictClauses)
999      sat_ArrayFree(cm->savedConflictClauses);
1000    cm->savedConflictClauses = 0;
1001  }
1002   cm->status = 0;
1003   sat_Main(cm);
1004   status = cm->status;
1005   PureSatCleanSat(cm);
1006   BmcCnfClausesRestore(cnfClauses, cnfstate);
1007   FREE(cnfstate);
1008   if(status == SAT_SAT)
1009     {
1010       if(pm->verbosity>=1)
1011         fprintf(vis_stdout, "find CEX\n");
1012       return TRUE;
1013     }
1014   else
1015     {
1016       if(pm->verbosity>=1)
1017         fprintf(vis_stdout, "didn't find CEX\n");
1018       return FALSE;
1019     }
1020}
1021
1022/**Function********************************************************************
1023
1024  Synopsis    [Incrementally checking the existence of a path of certain length
1025  used by incremental concretization. For more information of incremental
1026  concretization, please check the BMC'03 and STTT'05
1027  paper of Li et al., "A satisfiability-based appraoch to abstraction
1028  refinement in model checking", and " Abstraction in symbolic model checking
1029  using satisfiability as the only decision procedure"]
1030
1031  Description [Incrementally checking the existence of a path of certain length
1032  used by incremental concretization. For more information of incremental
1033  concretization, please check the BMC'03 and STTT'05
1034  paper of Li et al., "A satisfiability-based appraoch to abstraction
1035  refinement in model checking", and " Abstraction in symbolic model checking
1036  using satisfiability as the only decision procedure"]
1037
1038  SideEffects []
1039
1040  SeeAlso     []
1041
1042******************************************************************************/
1043
1044boolean PureSatIncreExistCEForRefineOnAbs(Ntk_Network_t *network,
1045                                   PureSat_IncreSATManager_t *pism,
1046                                   array_t *vertexArray,
1047                                   bAigEdge_t property,
1048                                   boolean firstTime,
1049                                   PureSat_Manager_t * pm)
1050
1051{
1052  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
1053  Ntk_Node_t         *latch, *latchData, *latchInit;
1054  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
1055  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
1056  int                i,j, k, mvfSize, status;
1057  char               *nodeName;
1058  array_t            *Pclause = array_alloc(int, 0);
1059  st_table           *nodeToMvfAigTable;
1060  int beginPosition = pism->beginPosition;
1061  int Length = pism->Length;
1062  int oldLength = pism->oldLength;
1063  BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
1064  satManager_t * cm = pism->cm;
1065
1066  nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
1067  if (nodeToMvfAigTable == NIL(st_table)){
1068    (void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
1069    exit(0);
1070  }
1071 
1072 { 
1073   array_t *supportLatches = PureSatGetImmediateSupportLatches(network, beginPosition, vertexArray);
1074   arrayForEachItem(char *, supportLatches, j, nodeName) {
1075     latch = Ntk_NetworkFindNodeByName(network, nodeName);
1076    latchInit  = Ntk_LatchReadInitialInput(latch);
1077    latchData  = Ntk_LatchReadDataInput(latch);
1078    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
1079    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
1080    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1081    if (latchMvfAig ==  NIL(MvfAig_Function_t)){
1082      latchMvfAig = Bmc_NodeBuildMVF(network, latch);
1083      array_free(latchMvfAig);
1084      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1085    }
1086   
1087    mvfSize   = array_n(initMvfAig);
1088    initBAig  = ALLOC(bAigEdge_t, mvfSize);
1089    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
1090    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
1091   
1092    for(i=0; i< mvfSize; i++){
1093      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
1094      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
1095      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
1096    }
1097   
1098    BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
1099    FREE(initBAig);
1100    FREE(dataBAig);
1101    FREE(latchBAig);
1102  } 
1103   array_free(supportLatches);
1104 }
1105
1106 
1107  for(j=beginPosition;j<array_n(vertexArray);j++){
1108    nodeName = array_fetch(char *,vertexArray,j);
1109    latch = Ntk_NetworkFindNodeByName(network,nodeName);
1110    latchInit  = Ntk_LatchReadInitialInput(latch);
1111    latchData  = Ntk_LatchReadDataInput(latch);
1112    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
1113    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
1114    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1115   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
1116     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
1117     array_free(latchMvfAig);
1118     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1119   }
1120   
1121    mvfSize   = array_n(initMvfAig);
1122    initBAig  = ALLOC(bAigEdge_t, mvfSize);
1123    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
1124    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
1125   
1126    for(i=0; i< mvfSize; i++){
1127      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
1128      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
1129      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
1130    }
1131   
1132    /*BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);*/
1133    for (k=0; k <oldLength; k++){
1134      BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
1135    }
1136    FREE(initBAig);
1137    FREE(dataBAig);
1138    FREE(latchBAig);
1139  }
1140
1141  /*for more length */
1142  if(oldLength<Length){
1143    for(j=0;j<array_n(vertexArray);j++){
1144      nodeName = array_fetch(char *,vertexArray,j);
1145      latch = Ntk_NetworkFindNodeByName(network,nodeName);
1146      latchInit  = Ntk_LatchReadInitialInput(latch);
1147      latchData  = Ntk_LatchReadDataInput(latch);
1148      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
1149      dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
1150      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1151      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
1152        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
1153        array_free(latchMvfAig);
1154        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1155      }
1156   
1157      mvfSize   = array_n(initMvfAig);
1158      initBAig  = ALLOC(bAigEdge_t, mvfSize);
1159      dataBAig  = ALLOC(bAigEdge_t, mvfSize);
1160      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
1161     
1162      for(i=0; i< mvfSize; i++){
1163        dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
1164        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
1165        initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
1166      }
1167     
1168      for (k=oldLength; k<Length; k++){
1169        BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
1170      }
1171      FREE(initBAig);
1172      FREE(dataBAig);
1173      FREE(latchBAig);
1174    }
1175  }
1176 
1177 
1178  /*cnfstate = BmcCnfClausesFreeze(cnfClauses);*/
1179  if(firstTime){
1180    /* pism->propertyPos = cnfstate->nextIndex;*/
1181    array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager,
1182                                                                 property,Length, cnfClauses));
1183    BmcCnfInsertClause(cnfClauses, Pclause);
1184    array_free(Pclause);
1185  }
1186  PureSatReadClauses(pism,pm);
1187  sat_Main(cm);
1188  if(pm->dbgLevel>=1 && cm->status==SAT_SAT){
1189    pm->result = array_alloc(int, 0);
1190    {
1191      int size, value;
1192      size = cm->initNumVariables * satNodeSize;
1193      for(i=satNodeSize; i<=size; i+=satNodeSize) {
1194        value = SATvalue(i);
1195        if(value == 1) {
1196          array_insert_last(int, pm->result, SATnodeID(i));
1197        }
1198        else if(value == 0) {
1199          array_insert_last(int, pm->result, -(SATnodeID(i)));
1200        }
1201      }
1202    }
1203  }
1204  status = cm->status;
1205  PureSatCleanSat(cm);
1206  /*FREE(cnfstate);*/
1207  if(status == SAT_SAT)
1208    {
1209      if(pm->verbosity>=1)
1210        fprintf(vis_stdout, "find CEX\n");
1211      return TRUE;
1212    }
1213  else
1214    {
1215      if(pm->verbosity>=1)
1216        fprintf(vis_stdout, "didn't find CEX\n");
1217      return FALSE;
1218    }
1219}
1220
1221
1222/**Function********************************************************************
1223
1224  Synopsis    [Building the path together with ClsidxToLatchTable for later use
1225  by refinement extraction]
1226
1227  Description [Building the path together with ClsidxToLatchTable for later use
1228  by refinement extraction]
1229
1230  SideEffects []
1231
1232  SeeAlso     []
1233
1234******************************************************************************/
1235
1236void
1237PureSatGenerateClausesFromStateTostateWithTable(
1238   bAig_Manager_t  *manager,
1239   bAigEdge_t      *fromAigArray,
1240   bAigEdge_t      *toAigArray,
1241   int             mvfSize, 
1242   int             fromState,
1243   int             toState,
1244   BmcCnfClauses_t *cnfClauses,
1245   int             outIndex,
1246   st_table        *ClsidxToLatchTable,
1247   char            *nodeName) 
1248{
1249  array_t    *clause, *tmpclause;
1250  int        toIndex, fromIndex, cnfIndex;
1251  int        i;
1252 
1253  toIndex =0;
1254  fromIndex = 0;
1255 
1256  for(i=0; i< mvfSize; i++){
1257    if ((fromAigArray[i] == bAig_One) && (toAigArray[i] == bAig_One)){
1258      return;   /* the clause is always true */
1259    }
1260  }
1261  clause  = array_alloc(int, 0);
1262  for(i=0; i< mvfSize; i++){
1263    if ((fromAigArray[i] != bAig_Zero) && (toAigArray[i] != bAig_Zero)){
1264      if (toAigArray[i] != bAig_One){ 
1265         toIndex = BmcGenerateCnfFormulaForAigFunction(manager,toAigArray[i],
1266                                                       toState,cnfClauses);
1267      }
1268      if (fromAigArray[i] != bAig_One){ 
1269         fromIndex = BmcGenerateCnfFormulaForAigFunction(manager,fromAigArray[i],
1270                                                         fromState,cnfClauses);
1271      }
1272     cnfIndex = cnfClauses->cnfGlobalIndex++;  /* index of the output of the OR of T(from, to) */
1273     if (toAigArray[i] == bAig_One){   
1274       tmpclause  = array_alloc(int, 2);
1275       array_insert(int, tmpclause, 0, -fromIndex);
1276       array_insert(int, tmpclause, 1, cnfIndex);
1277       BmcCnfInsertClause(cnfClauses, tmpclause);
1278       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
1279       array_free(tmpclause); 
1280
1281       tmpclause  = array_alloc(int, 2);
1282       array_insert(int, tmpclause, 0, fromIndex);
1283       array_insert(int, tmpclause, 1, -cnfIndex);
1284       BmcCnfInsertClause(cnfClauses, tmpclause);
1285       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
1286       array_free(tmpclause);       
1287
1288     } else if (fromAigArray[i] == bAig_One){
1289       tmpclause  = array_alloc(int, 2);
1290       array_insert(int, tmpclause, 0, -toIndex);
1291       array_insert(int, tmpclause, 1, cnfIndex);
1292       BmcCnfInsertClause(cnfClauses, tmpclause);
1293       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
1294       array_free(tmpclause);
1295
1296       tmpclause  = array_alloc(int, 2);
1297       array_insert(int, tmpclause, 0, toIndex);
1298       array_insert(int, tmpclause, 1, -cnfIndex);
1299       BmcCnfInsertClause(cnfClauses, tmpclause);
1300       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
1301       array_free(tmpclause);
1302       
1303     } else {
1304       tmpclause  = array_alloc(int, 3);
1305       array_insert(int, tmpclause, 0, -toIndex);
1306       array_insert(int, tmpclause, 1, -fromIndex);
1307       array_insert(int, tmpclause, 2,  cnfIndex);
1308       BmcCnfInsertClause(cnfClauses, tmpclause);
1309       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
1310       array_free(tmpclause);
1311
1312       tmpclause  = array_alloc(int, 2);
1313       array_insert(int, tmpclause, 0, toIndex);
1314       array_insert(int, tmpclause, 1, -cnfIndex);
1315       BmcCnfInsertClause(cnfClauses, tmpclause);
1316       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
1317       array_free(tmpclause);
1318
1319       tmpclause  = array_alloc(int, 2);
1320       array_insert(int, tmpclause, 0, fromIndex);
1321       array_insert(int, tmpclause, 1, -cnfIndex);
1322       BmcCnfInsertClause(cnfClauses, tmpclause);
1323       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
1324       array_free(tmpclause);
1325     }
1326     array_insert_last(int, clause, cnfIndex);
1327    } /* if */
1328     
1329  } /* for i loop */
1330  if (outIndex != 0 ){
1331    array_insert_last(int, clause, -outIndex);
1332  }
1333  BmcCnfInsertClause(cnfClauses, clause);
1334  array_free(clause);
1335 
1336  return;
1337}
1338
1339
1340/**Function********************************************************************
1341
1342  Synopsis    [Building the path with enhanced initail states]
1343
1344  Description [Building the path with enhanced initail states]
1345
1346  SideEffects []
1347
1348  SeeAlso     []
1349
1350******************************************************************************/
1351
1352void
1353PureSatGenerateClausesForPath_EnhanceInit(
1354   Ntk_Network_t   *network,
1355   int             from,
1356   int             to,
1357   PureSat_IncreSATManager_t * pism,
1358   PureSat_Manager_t *  pm,
1359   st_table        *nodeToMvfAigTable,
1360   st_table        *CoiTable)
1361{
1362  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
1363  lsGen           gen;
1364 
1365  Ntk_Node_t         *latch, *latchData, *latchInit;
1366  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
1367  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
1368  int        i,j, k, mvfSize;
1369  array_t * vertexArray = array_alloc(char *,0);
1370  char * nodeName;
1371  BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
1372  st_table * ClsidxToLatchTable = pm->ClsidxToLatchTable;
1373
1374  if(from == 0){
1375    if(pm->verbosity>=2)
1376      fprintf(vis_stdout, "node in vertexArray: ");
1377    Ntk_NetworkForEachLatch(network, gen, latch) { 
1378      int tmp;
1379      if (!st_lookup_int(CoiTable, latch, &tmp)){
1380        continue;
1381      }
1382      nodeName = Ntk_NodeReadName(latch);
1383      array_insert_last(char *,vertexArray,nodeName);
1384      if(pm->verbosity>=2)
1385        fprintf(vis_stdout, "%s  ",nodeName);
1386    }
1387    if(pm->verbosity>=2)
1388      fprintf(vis_stdout, "\n");
1389   }
1390
1391  if(from == 0){ 
1392    array_t *supportLatches = PureSatGetImmediateSupportLatches(network, 0, vertexArray);
1393    arrayForEachItem(char *, supportLatches, j, nodeName) {
1394      latch = Ntk_NetworkFindNodeByName(network, nodeName);
1395      latchInit  = Ntk_LatchReadInitialInput(latch);
1396      latchData  = Ntk_LatchReadDataInput(latch);
1397      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
1398      dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
1399      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1400      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
1401        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
1402        array_free(latchMvfAig);
1403        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1404      }
1405     
1406      mvfSize   = array_n(initMvfAig);
1407      initBAig  = ALLOC(bAigEdge_t, mvfSize);
1408      dataBAig  = ALLOC(bAigEdge_t, mvfSize);
1409      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
1410     
1411      for(i=0; i< mvfSize; i++){
1412        dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
1413        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
1414        initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
1415      }
1416     
1417      BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
1418      FREE(initBAig);
1419      FREE(dataBAig);
1420      FREE(latchBAig);
1421    }
1422    array_free(supportLatches);
1423    array_free(vertexArray);
1424  }
1425 
1426  Ntk_NetworkForEachLatch(network, gen, latch) { 
1427    int tmp;
1428    if (!st_lookup_int(CoiTable, latch, &tmp)){
1429      continue;
1430    }
1431    nodeName = Ntk_NodeReadName(latch);
1432   latchInit  = Ntk_LatchReadInitialInput(latch);
1433   latchData  = Ntk_LatchReadDataInput(latch);
1434
1435   /* Get the multi-valued function for each node*/
1436   initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
1437   if (initMvfAig ==  NIL(MvfAig_Function_t)){
1438     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
1439     return;
1440   } 
1441   dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
1442   if (dataMvfAig ==  NIL(MvfAig_Function_t)){
1443     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchData));
1444     return;
1445   }
1446   latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1447   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
1448     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
1449     array_free(latchMvfAig);
1450     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
1451   }
1452     
1453   mvfSize   = array_n(initMvfAig);
1454   initBAig  = ALLOC(bAigEdge_t, mvfSize);
1455   dataBAig  = ALLOC(bAigEdge_t, mvfSize);
1456   latchBAig = ALLOC(bAigEdge_t, mvfSize);   
1457
1458   for(i=0; i< mvfSize; i++){
1459     dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
1460     latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
1461     initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
1462   } 
1463   /* Generate the CNF for the transition functions */   
1464   for (k=from; k < to; k++){
1465     PureSatGenerateClausesFromStateTostateWithTable(manager, dataBAig,latchBAig, mvfSize, k,
1466                                                       k+1, cnfClauses,0,ClsidxToLatchTable, nodeName);
1467   } /* for k state loop */
1468   FREE(initBAig);
1469   FREE(dataBAig);
1470   FREE(latchBAig);
1471  } /* ForEachLatch loop*/
1472
1473  return;
1474}
Note: See TracBrowser for help on using the repository browser.