abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcBmc.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bmcBmc.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT-based bounded model checking.]
8 
9  Synopsis [Simple BMC package.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: bmcBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "proof/fra/fra.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satStore.h"
24 #include "bmc.h"
25 
27 
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31 
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35 
36 /**Function*************************************************************
37 
38  Synopsis [Create timeframes of the manager for BMC.]
39 
40  Description [The resulting manager is combinational. POs correspond to \
41  the property outputs in each time-frame.]
42 
43  SideEffects []
44 
45  SeeAlso []
46 
47 ***********************************************************************/
48 Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
49 {
50  Aig_Man_t * pFrames;
51  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
52  int i, f;
53  assert( Saig_ManRegNum(pAig) > 0 );
54  pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
55  // map the constant node
56  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
57  // create variables for register outputs
58  Saig_ManForEachLo( pAig, pObj, i )
59  pObj->pData = Aig_ManConst0( pFrames );
60  // add timeframes
61  for ( f = 0; f < nFrames; f++ )
62  {
63  // create PI nodes for this frame
64  Saig_ManForEachPi( pAig, pObj, i )
65  pObj->pData = Aig_ObjCreateCi( pFrames );
66  // add internal nodes of this frame
67  Aig_ManForEachNode( pAig, pObj, i )
68  pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
69  // create POs for this frame
70  Saig_ManForEachPo( pAig, pObj, i )
71  Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
72  if ( f == nFrames - 1 )
73  break;
74  // save register inputs
75  Saig_ManForEachLi( pAig, pObj, i )
76  pObj->pData = Aig_ObjChild0Copy(pObj);
77  // transfer to register outputs
78  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
79  pObjLo->pData = pObjLi->pData;
80  }
81  Aig_ManCleanup( pFrames );
82  return pFrames;
83 }
84 
85 /**Function*************************************************************
86 
87  Synopsis [Returns the number of internal nodes that are not counted yet.]
88 
89  Description []
90 
91  SideEffects []
92 
93  SeeAlso []
94 
95 ***********************************************************************/
97 {
98  if ( !Aig_ObjIsNode(pObj) )
99  return 0;
100  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
101  return 0;
102  Aig_ObjSetTravIdCurrent(p, pObj);
103  return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) +
105 }
106 
107 /**Function*************************************************************
108 
109  Synopsis [Create timeframes of the manager for BMC.]
110 
111  Description [The resulting manager is combinational. POs correspond to
112  the property outputs in each time-frame.
113  The unrolling is stopped as soon as the number of nodes in the frames
114  exceeds the given maximum size.]
115 
116  SideEffects []
117 
118  SeeAlso []
119 
120 ***********************************************************************/
121 Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax )
122 {
123  Aig_Man_t * pFrames;
124  Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo;
125  int i, f, Counter = 0;
126  assert( Saig_ManRegNum(pAig) > 0 );
127  pFrames = Aig_ManStart( nSizeMax );
128  Aig_ManIncrementTravId( pFrames );
129  // map the constant node
130  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
131  // create variables for register outputs
132  Saig_ManForEachLo( pAig, pObj, i )
133  pObj->pData = Aig_ManConst0( pFrames );
134  // add timeframes
135  Counter = 0;
136  for ( f = 0; f < nFrames; f++ )
137  {
138  // create PI nodes for this frame
139  Saig_ManForEachPi( pAig, pObj, i )
140  pObj->pData = Aig_ObjCreateCi( pFrames );
141  // add internal nodes of this frame
142  Aig_ManForEachNode( pAig, pObj, i )
143  pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
144  // create POs for this frame
145  Saig_ManForEachPo( pAig, pObj, i )
146  {
147  pObjPo = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
148  Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
149  }
150  if ( Counter >= nSizeMax )
151  {
152  Aig_ManCleanup( pFrames );
153  return pFrames;
154  }
155  if ( f == nFrames - 1 )
156  break;
157  // save register inputs
158  Saig_ManForEachLi( pAig, pObj, i )
159  pObj->pData = Aig_ObjChild0Copy(pObj);
160  // transfer to register outputs
161  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
162  pObjLo->pData = pObjLi->pData;
163  }
164  Aig_ManCleanup( pFrames );
165  return pFrames;
166 }
167 
169 
170 #include "misc/util/utilMem.h"
171 
173 
174 
175 /**Function*************************************************************
176 
177  Synopsis [Performs BMC for the given AIG.]
178 
179  Description []
180 
181  SideEffects []
182 
183  SeeAlso []
184 
185 ***********************************************************************/
186 int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit )
187 {
188  extern Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit );
189  sat_solver * pSat;
190  Cnf_Dat_t * pCnf;
191  Aig_Man_t * pFrames, * pAigTemp;
192  Aig_Obj_t * pObj;
193  int status, Lit, i, RetValue = -1;
194  abctime clk;
195 
196  // derive the timeframes
197  clk = Abc_Clock();
198  if ( nCofFanLit )
199  {
200  pFrames = Gia_ManCofactorAig( pAig, nFrames, nCofFanLit );
201  if ( pFrames == NULL )
202  return -1;
203  }
204  else if ( nSizeMax > 0 )
205  {
206  pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
207  nFrames = Aig_ManCoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManCoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
208  }
209  else
210  pFrames = Saig_ManFramesBmc( pAig, nFrames );
211  if ( piFrame )
212  *piFrame = nFrames;
213  if ( fVerbose )
214  {
215  printf( "Running \"bmc\". AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
216  Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
217  Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
218  printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ",
219  nFrames, Aig_ManCiNum(pFrames), Aig_ManCoNum(pFrames),
220  Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
221  ABC_PRT( "Time", Abc_Clock() - clk );
222  fflush( stdout );
223  }
224  // rewrite the timeframes
225  if ( fRewrite )
226  {
227  clk = Abc_Clock();
228 // pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
229  pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
230  Aig_ManStop( pAigTemp );
231  if ( fVerbose )
232  {
233  printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ",
234  Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
235  ABC_PRT( "Time", Abc_Clock() - clk );
236  fflush( stdout );
237  }
238  }
239  // create the SAT solver
240  clk = Abc_Clock();
241  pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) );
242 //if ( s_fInterrupt )
243 //return -1;
244  pSat = sat_solver_new();
245  sat_solver_setnvars( pSat, pCnf->nVars );
246  for ( i = 0; i < pCnf->nClauses; i++ )
247  {
248  if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
249  assert( 0 );
250  }
251  if ( fVerbose )
252  {
253  printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
254  ABC_PRT( "Time", Abc_Clock() - clk );
255  fflush( stdout );
256  }
257  status = sat_solver_simplify(pSat);
258  if ( status == 0 )
259  {
260  if ( fVerbose )
261  {
262  printf( "The BMC problem is trivially UNSAT\n" );
263  fflush( stdout );
264  }
265  }
266  else
267  {
268  abctime clkPart = Abc_Clock();
269  Aig_ManForEachCo( pFrames, pObj, i )
270  {
271 //if ( s_fInterrupt )
272 //return -1;
273  Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
274  if ( fVerbose )
275  {
276  printf( "Solving output %2d of frame %3d ... \r",
277  i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
278  }
279  clk = Abc_Clock();
280  status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
281  if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
282  {
283  printf( "Solved %2d outputs of frame %3d. ",
284  Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
285  printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
286  ABC_PRT( "T", Abc_Clock() - clkPart );
287  clkPart = Abc_Clock();
288  fflush( stdout );
289  }
290  if ( status == l_False )
291  {
292 /*
293  Lit = lit_neg( Lit );
294  RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
295  assert( RetValue );
296  if ( pSat->qtail != pSat->qhead )
297  {
298  RetValue = sat_solver_simplify(pSat);
299  assert( RetValue );
300  }
301 */
302  }
303  else if ( status == l_True )
304  {
305  Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
306  int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
307  pModel[Aig_ManCiNum(pFrames)] = pObj->Id;
308  pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
309  ABC_FREE( pModel );
310  Vec_IntFree( vCiIds );
311 
312  if ( piFrame )
313  *piFrame = i / Saig_ManPoNum(pAig);
314  RetValue = 0;
315  break;
316  }
317  else
318  {
319  if ( piFrame )
320  *piFrame = i / Saig_ManPoNum(pAig);
321  RetValue = -1;
322  break;
323  }
324  }
325  }
326  sat_solver_delete( pSat );
327  Cnf_DataFree( pCnf );
328  Aig_ManStop( pFrames );
329  return RetValue;
330 }
331 
332 ////////////////////////////////////////////////////////////////////////
333 /// END OF FILE ///
334 ////////////////////////////////////////////////////////////////////////
335 
336 
338 
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
ABC_NAMESPACE_IMPL_START Aig_Man_t * Saig_ManFramesBmc(Aig_Man_t *pAig, int nFrames)
DECLARATIONS ///.
Definition: bmcBmc.c:48
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
int nClauses
Definition: cnf.h:61
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
void * pData
Definition: aig.h:87
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
int * pVarNums
Definition: cnf.h:63
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
#define l_True
Definition: SolverTypes.h:84
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Abc_Cex_t * Fra_SmlCopyCounterExample(Aig_Man_t *pAig, Aig_Man_t *pFrames, int *pModel)
Definition: fraSim.c:1117
static abctime Abc_Clock()
Definition: abc_global.h:279
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_Man_t * Saig_ManFramesBmcLimit(Aig_Man_t *pAig, int nFrames, int nSizeMax)
Definition: bmcBmc.c:121
stats_t stats
Definition: satSolver.h:156
Definition: cnf.h:56
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
ABC_NAMESPACE_IMPL_START Aig_Man_t * Dar_ManRwsat(Aig_Man_t *pAig, int fBalance, int fVerbose)
DECLARATIONS ///.
Definition: darScript.c:71
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
int ** pClauses
Definition: cnf.h:62
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Vec_Int_t * Cnf_DataCollectPiSatNums(Cnf_Dat_t *pCnf, Aig_Man_t *p)
Definition: cnfMan.c:104
static lit toLitCond(int v, int c)
Definition: satVec.h:143
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Definition: aig.h:69
static int Counter
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
int Saig_ManFramesCount_rec(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: bmcBmc.c:96
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
int Aig_ManLevelNum(Aig_Man_t *p)
Definition: aigDfs.c:486
ABC_INT64_T conflicts
Definition: satVec.h:154
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START int Saig_ManBmcSimple(Aig_Man_t *pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int *piFrame, int nCofFanLit)
Definition: bmcBmc.c:186
Aig_Man_t * Gia_ManCofactorAig(Aig_Man_t *p, int nFrames, int nCofFanLit)
Definition: giaAig.c:411
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
#define ABC_FREE(obj)
Definition: abc_global.h:232
#define ABC_PRT(a, t)
Definition: abc_global.h:220
#define l_False
Definition: SolverTypes.h:85
ABC_INT64_T propagations
Definition: satVec.h:154
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
ABC_INT64_T abctime
Definition: abc_global.h:278
int nLiterals
Definition: cnf.h:60
int Id
Definition: aig.h:85
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
int * Sat_SolverGetModel(sat_solver *p, int *pVars, int nVars)
Definition: satUtil.c:266
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91