ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
bmcICheck.c File Reference
#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "aig/gia/giaAig.h"
Include dependency graph for bmcICheck.c:

Go to the source code of this file.

Functions

sat_solver * Bmc_DeriveSolver (Gia_Man_t *p, Gia_Man_t *pMiter, Cnf_Dat_t *pCnf, int nFramesMax, int nTimeOut, int fVerbose)
 
void Bmc_PerformICheck (Gia_Man_t *p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose)
 
void Bmc_PerformFindFlopOrder_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vRegs)
 
void Bmc_PerformFindFlopOrder (Gia_Man_t *p, Vec_Int_t *vRegs)
 
int Bmc_PerformISearchOne (Gia_Man_t *p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fVerbose, Vec_Int_t *vLits)
 
Vec_Int_t * Bmc_PerformISearch (Gia_Man_t *p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose)
 

Function Documentation

◆ Bmc_DeriveSolver()

sat_solver * Bmc_DeriveSolver ( Gia_Man_t * p,
Gia_Man_t * pMiter,
Cnf_Dat_t * pCnf,
int nFramesMax,
int nTimeOut,
int fVerbose )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file bmcICheck.c.

92{
93 sat_solver * pSat;
94 Vec_Int_t * vLits;
95 Gia_Obj_t * pObj, * pObj0, * pObj1;
96 int i, k, iVar0, iVar1, iVarOut;
97 int VarShift = 0;
98
99 // start the SAT solver
100 pSat = sat_solver_new();
101 sat_solver_setnvars( pSat, Gia_ManRegNum(p) + Gia_ManCoNum(p) + pCnf->nVars * (nFramesMax + 1) );
102 sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
103
104 // add one large OR clause
105 vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
106 Gia_ManForEachCo( p, pObj, i )
107 Vec_IntPush( vLits, Abc_Var2Lit(Gia_ManRegNum(p) + i, 0) );
108 sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
109
110 // load the last timeframe
111 Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) );
112 VarShift += Gia_ManRegNum(p) + Gia_ManCoNum(p);
113
114 // add XOR clauses
115 Gia_ManForEachPo( p, pObj, i )
116 {
117 pObj0 = Gia_ManPo( pMiter, 2*i+0 );
118 pObj1 = Gia_ManPo( pMiter, 2*i+1 );
119 iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
120 iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
121 iVarOut = Gia_ManRegNum(p) + i;
122 sat_solver_add_xor( pSat, iVar0, iVar1, iVarOut, 0 );
123 }
124 Gia_ManForEachRi( p, pObj, i )
125 {
126 pObj0 = Gia_ManRi( pMiter, i );
127 pObj1 = Gia_ManRi( pMiter, i + Gia_ManRegNum(p) );
128 iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
129 iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
130 iVarOut = Gia_ManRegNum(p) + Gia_ManPoNum(p) + i;
131 sat_solver_add_xor_and( pSat, iVarOut, iVar0, iVar1, i );
132 }
133 // add timeframe clauses
134 for ( i = 0; i < pCnf->nClauses; i++ )
135 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
136 assert( 0 );
137
138 // add other timeframes
139 for ( k = 0; k < nFramesMax; k++ )
140 {
141 // collect variables of the RO nodes
142 Vec_IntClear( vLits );
143 Gia_ManForEachRo( pMiter, pObj, i )
144 Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pMiter, pObj)] );
145 // lift CNF again
146 Cnf_DataLiftGia( pCnf, pMiter, pCnf->nVars );
147 VarShift += pCnf->nVars;
148 // stitch the clauses
149 Gia_ManForEachRi( pMiter, pObj, i )
150 {
151 iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj)];
152 iVar1 = Vec_IntEntry( vLits, i );
153 if ( iVar1 == -1 )
154 continue;
155 sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
156 }
157 // add equality clauses for the COs
158 Gia_ManForEachPo( p, pObj, i )
159 {
160 pObj0 = Gia_ManPo( pMiter, 2*i+0 );
161 pObj1 = Gia_ManPo( pMiter, 2*i+1 );
162 iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
163 iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
164 sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
165 }
166 Gia_ManForEachRi( p, pObj, i )
167 {
168 pObj0 = Gia_ManRi( pMiter, i );
169 pObj1 = Gia_ManRi( pMiter, i + Gia_ManRegNum(p) );
170 iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
171 iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
172 sat_solver_add_buffer_enable( pSat, iVar0, iVar1, i, 0 );
173 }
174 // add timeframe clauses
175 for ( i = 0; i < pCnf->nClauses; i++ )
176 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
177 assert( 0 );
178 }
179// sat_solver_compress( pSat );
180 Cnf_DataLiftGia( pCnf, pMiter, -VarShift );
181 Vec_IntFree( vLits );
182 return pSat;
183}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver_add_xor
#define sat_solver_add_xor
Definition cecSatG2.c:39
sat_solver
#define sat_solver
Definition cecSatG2.c:34
p
Cube * p
Definition exorList.c:222
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition gia.h:1250
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
Cnf_Dat_t_::nVars
int nVars
Definition cnf.h:59
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition cnf.h:63
Cnf_Dat_t_::pClauses
int ** pClauses
Definition cnf.h:62
Cnf_Dat_t_::nClauses
int nClauses
Definition cnf.h:61
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_PerformFindFlopOrder()

void Bmc_PerformFindFlopOrder ( Gia_Man_t * p,
Vec_Int_t * vRegs )

Definition at line 322 of file bmcICheck.c.

323{
324 Gia_Obj_t * pObj;
325 int i, iReg, k = 0;
326 // start with POs
327 Vec_IntClear( vRegs );
328 Gia_ManForEachPo( p, pObj, i )
329 Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
330 // add flop outputs in the B
331 Gia_ManIncrementTravId( p );
332 Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
333 Gia_ManForEachObjVec( vRegs, p, pObj, i )
334 {
335 assert( Gia_ObjIsPo(p, pObj) || Gia_ObjIsRo(p, pObj) );
336 if ( Gia_ObjIsRo(p, pObj) )
337 pObj = Gia_ObjRoToRi( p, pObj );
338 Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs );
339 }
340 // add dangling flops
341 Gia_ManForEachRo( p, pObj, i )
342 if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
343 Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
344 // remove POs; keep flop outputs only; remap ObjId into CiId
345 assert( Vec_IntSize(vRegs) == Gia_ManCoNum(p) );
346 Gia_ManForEachObjVec( vRegs, p, pObj, i )
347 {
348 if ( i < Gia_ManPoNum(p) )
349 continue;
350 iReg = Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
351 assert( iReg >= 0 && iReg < Gia_ManRegNum(p) );
352 Vec_IntWriteEntry( vRegs, k++, iReg );
353 }
354 Vec_IntShrink( vRegs, k );
355 assert( Vec_IntSize(vRegs) == Gia_ManRegNum(p) );
356}
Bmc_PerformFindFlopOrder_rec
void Bmc_PerformFindFlopOrder_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vRegs)
Definition bmcICheck.c:307
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_PerformFindFlopOrder_rec()

void Bmc_PerformFindFlopOrder_rec ( Gia_Man_t * p,
Gia_Obj_t * pObj,
Vec_Int_t * vRegs )

Function*************************************************************

Synopsis [Collect flops starting from the POs.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file bmcICheck.c.

308{
309 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
310 return;
311 Gia_ObjSetTravIdCurrent(p, pObj);
312 if ( Gia_ObjIsCi(pObj) )
313 {
314 if ( Gia_ObjIsRo(p, pObj) )
315 Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
316 return;
317 }
318 assert( Gia_ObjIsAnd(pObj) );
319 Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs );
320 Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin1(pObj), vRegs );
321}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_PerformICheck()

void Bmc_PerformICheck ( Gia_Man_t * p,
int nFramesMax,
int nTimeOut,
int fEmpty,
int fVerbose )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file bmcICheck.c.

197{
198 int fUseOldCnf = 0;
199 Gia_Man_t * pMiter, * pTemp;
200 Cnf_Dat_t * pCnf;
201 sat_solver * pSat;
202 Vec_Int_t * vLits, * vUsed;
203 int i, status, Lit;
204 int nLitsUsed, nLits, * pLits;
205 abctime clkStart = Abc_Clock();
206 assert( nFramesMax > 0 );
207 assert( Gia_ManRegNum(p) > 0 );
208
209 if ( fVerbose )
210 printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
211 Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
212
213 // create miter
214 pTemp = Gia_ManDup( p );
215 pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
216 Gia_ManStop( pTemp );
217 assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
218 assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
219 // derive CNF
220 if ( fUseOldCnf )
221 pCnf = Cnf_DeriveGiaRemapped( pMiter );
222 else
223 {
224 pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
225 Gia_ManStop( pTemp );
226 pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
227 }
228
229 // collect positive literals
230 vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
231 for ( i = 0; i < Gia_ManRegNum(p); i++ )
232 Vec_IntPush( vLits, Abc_Var2Lit(i, fEmpty) );
233
234 // iteratively compute a minimal M-inductive set of next-state functions
235 nLitsUsed = fEmpty ? 0 : Vec_IntSize(vLits);
236 vUsed = Vec_IntAlloc( Vec_IntSize(vLits) );
237 while ( 1 )
238 {
239 int fChanges = 0;
240 // derive SAT solver
241 pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
242// sat_solver_bookmark( pSat );
243 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
244 if ( status == l_Undef )
245 {
246 printf( "Timeout reached after %d seconds.\n", nTimeOut );
247 break;
248 }
249 if ( status == l_True )
250 {
251 printf( "The problem is satisfiable (the current set is not M-inductive).\n" );
252 break;
253 }
254 assert( status == l_False );
255 // call analize_final
256 nLits = sat_solver_final( pSat, &pLits );
257 // mark used literals
258 Vec_IntFill( vUsed, Vec_IntSize(vLits), 0 );
259 for ( i = 0; i < nLits; i++ )
260 Vec_IntWriteEntry( vUsed, Abc_Lit2Var(pLits[i]), 1 );
261
262 // check if there are any positive unused
263 Vec_IntForEachEntry( vLits, Lit, i )
264 {
265 assert( i == Abc_Lit2Var(Lit) );
266 if ( Abc_LitIsCompl(Lit) )
267 continue;
268 if ( Vec_IntEntry(vUsed, i) )
269 continue;
270 // positive literal became unused
271 Vec_IntWriteEntry( vLits, i, Abc_LitNot(Lit) );
272 nLitsUsed--;
273 fChanges = 1;
274 }
275 // report the results
276 if ( fVerbose )
277 printf( "M =%4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
278 nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter),
279 Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
280 sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
281 if ( fVerbose )
282 Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
283 // count the number of negative literals
284 sat_solver_delete( pSat );
285 if ( !fChanges || fEmpty )
286 break;
287// break;
288// sat_solver_rollback( pSat );
289 }
290 Cnf_DataFree( pCnf );
291 Gia_ManStop( pMiter );
292 Vec_IntFree( vLits );
293 Vec_IntFree( vUsed );
294}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
Bmc_DeriveSolver
sat_solver * Bmc_DeriveSolver(Gia_Man_t *p, Gia_Man_t *pMiter, Cnf_Dat_t *pCnf, int nFramesMax, int nTimeOut, int fVerbose)
Definition bmcICheck.c:91
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition giaDup.c:720
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManMiter
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition giaDup.c:2983
Jf_ManDeriveCnf
Gia_Man_t * Jf_ManDeriveCnf(Gia_Man_t *p, int fCnfObjIds)
Definition giaJf.c:1749
sat_solver_nconflicts
int sat_solver_nconflicts(sat_solver *s)
Definition satSolver.c:2381
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Gia_Man_t_::pData
void * pData
Definition gia.h:198
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:

◆ Bmc_PerformISearch()

Vec_Int_t * Bmc_PerformISearch ( Gia_Man_t * p,
int nFramesMax,
int nTimeOut,
int fReverse,
int fBackTopo,
int fDump,
int fVerbose )

Definition at line 489 of file bmcICheck.c.

490{
491 Vec_Int_t * vLits, * vFlops;
492 int i, f;
493 if ( fVerbose )
494 printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops with %s %s flop order:\n",
495 Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p), fReverse ? "reverse":"direct", fBackTopo ? "backward":"natural" );
496 fflush( stdout );
497
498 // collect positive literals
499 vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
500 for ( i = 0; i < Gia_ManRegNum(p); i++ )
501 Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
502
503 for ( f = 1; f <= nFramesMax; f++ )
504 if ( Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fBackTopo, fVerbose, vLits ) )
505 {
506 Vec_IntFree( vLits );
507 return NULL;
508 }
509
510 // dump the numbers of the flops
511 if ( fDump )
512 {
513 int nLitsUsed = 0;
514 for ( i = 0; i < Gia_ManRegNum(p); i++ )
515 if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
516 nLitsUsed++;
517 printf( "The set contains %d (out of %d) next-state functions with 0-based numbers:\n", nLitsUsed, Gia_ManRegNum(p) );
518 for ( i = 0; i < Gia_ManRegNum(p); i++ )
519 if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
520 printf( "%d ", i );
521 printf( "\n" );
522 }
523 // save flop indexes
524 vFlops = Vec_IntAlloc( Gia_ManRegNum(p) );
525 for ( i = 0; i < Gia_ManRegNum(p); i++ )
526 if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
527 Vec_IntPush( vFlops, 1 );
528 else
529 Vec_IntPush( vFlops, 0 );
530 Vec_IntFree( vLits );
531 return vFlops;
532}
Bmc_PerformISearchOne
int Bmc_PerformISearchOne(Gia_Man_t *p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fVerbose, Vec_Int_t *vLits)
Definition bmcICheck.c:370
Here is the call graph for this function:

◆ Bmc_PerformISearchOne()

int Bmc_PerformISearchOne ( Gia_Man_t * p,
int nFramesMax,
int nTimeOut,
int fReverse,
int fBackTopo,
int fVerbose,
Vec_Int_t * vLits )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 370 of file bmcICheck.c.

371{
372 int fUseOldCnf = 0;
373 Gia_Man_t * pMiter, * pTemp;
374 Cnf_Dat_t * pCnf;
375 sat_solver * pSat;
376 Vec_Int_t * vRegs = NULL;
377// Vec_Int_t * vLits;
378 int i, Iter, status;
379 int nLitsUsed, RetValue = 0;
380 abctime clkStart = Abc_Clock();
381 assert( nFramesMax > 0 );
382 assert( Gia_ManRegNum(p) > 0 );
383
384 // create miter
385 pTemp = Gia_ManDup( p );
386 pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
387 Gia_ManStop( pTemp );
388 assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
389 assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
390 // derive CNF
391 if ( fUseOldCnf )
392 pCnf = Cnf_DeriveGiaRemapped( pMiter );
393 else
394 {
395 //pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
396 //Gia_ManStop( pTemp );
397 //pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
398 pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0, 0 );
399 }
400/*
401 // collect positive literals
402 vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
403 for ( i = 0; i < Gia_ManRegNum(p); i++ )
404 Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
405*/
406 // derive SAT solver
407 pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
408 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
409 if ( status == l_True )
410 {
411 printf( "I = %4d : ", nFramesMax );
412 printf( "Problem is satisfiable.\n" );
413 sat_solver_delete( pSat );
414 Cnf_DataFree( pCnf );
415 Gia_ManStop( pMiter );
416 return 1;
417 }
418 if ( status == l_Undef )
419 {
420 printf( "ICheck: Timeout reached after %d seconds. \n", nTimeOut );
421 RetValue = 1;
422 goto cleanup;
423 }
424 assert( status == l_False );
425
426 // count the number of positive literals
427 nLitsUsed = 0;
428 for ( i = 0; i < Gia_ManRegNum(p); i++ )
429 if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
430 nLitsUsed++;
431
432 // try removing variables
433 vRegs = Vec_IntStartNatural( Gia_ManRegNum(p) );
434 if ( fBackTopo )
435 Bmc_PerformFindFlopOrder( p, vRegs );
436 if ( fReverse )
437 Vec_IntReverseOrder( vRegs );
438// for ( Iter = 0; Iter < Gia_ManRegNum(p); Iter++ )
439 Vec_IntForEachEntry( vRegs, i, Iter )
440 {
441// i = fReverse ? Gia_ManRegNum(p) - 1 - Iter : Iter;
442 if ( Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
443 continue;
444 Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
445 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
446 if ( status == l_Undef )
447 {
448 printf( "ICheck: Timeout reached after %d seconds. \n", nTimeOut );
449 RetValue = 1;
450 goto cleanup;
451 }
452 if ( status == l_True )
453 Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
454 else if ( status == l_False )
455 nLitsUsed--;
456 else assert( 0 );
457 // report the results
458 //printf( "Round %d: ", o );
459 if ( fVerbose )
460 {
461 printf( "I = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
462 i, (nFramesMax+1) * Gia_ManAndNum(pMiter),
463 Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
464 sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
465 ABC_PRTr( "Time", Abc_Clock() - clkStart );
466 fflush( stdout );
467 }
468 }
469 // report the results
470 //printf( "Round %d: ", o );
471 if ( fVerbose )
472 {
473 printf( "M = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
474 nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter),
475 Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
476 sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
477 Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
478 fflush( stdout );
479 }
480cleanup:
481 // cleanup
482 sat_solver_delete( pSat );
483 Cnf_DataFree( pCnf );
484 Gia_ManStop( pMiter );
485 Vec_IntFree( vRegs );
486// Vec_IntFree( vLits );
487 return RetValue;
488}
ABC_PRTr
#define ABC_PRTr(a, t)
Definition abc_global.h:256
Bmc_PerformFindFlopOrder
void Bmc_PerformFindFlopOrder(Gia_Man_t *p, Vec_Int_t *vRegs)
Definition bmcICheck.c:322
Mf_ManGenerateCnf
void * Mf_ManGenerateCnf(Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose)
Definition giaMf.c:1877
Here is the call graph for this function:
Here is the caller graph for this function: