ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
int2Bmc.c File Reference
#include "int2Int.h"
Include dependency graph for int2Bmc.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Gia_Man_t * Int2_ManDupInit (Gia_Man_t *p, int fVerbose)
 DECLARATIONS ///.
 
int Int2_ManCheckInit (Gia_Man_t *p)
 MACRO DEFINITIONS ///.
 
Gia_Man_t * Int2_ManFrameInit (Gia_Man_t *p, int nFrames, int fVerbose)
 
sat_solver * Int2_ManSetupBmcSolver (Gia_Man_t *p, int nFrames)
 
void Int2_ManCreateFrames (Int2_Man_t *p, int iFrame, Vec_Int_t *vPrefCos)
 
int Int2_ManCheckBmc (Int2_Man_t *p, Vec_Int_t *vCube)
 

Function Documentation

◆ Int2_ManCheckBmc()

int Int2_ManCheckBmc ( Int2_Man_t * p,
Vec_Int_t * vCube )

Definition at line 318 of file int2Bmc.c.

319{
320 int status;
321 if ( vCube == NULL )
322 {
323 Gia_Obj_t * pObj;
324 int i, iLit;
325 Gia_ManForEachPo( p->pGia, pObj, i )
326 {
327 iLit = Int2_ManCheckFrames( p, 0, Gia_ObjId(p->pGia, pObj) );
328 if ( iLit == 0 )
329 continue;
330 if ( iLit == 1 )
331 return 0;
332 status = sat_solver_solve( p->pSatPref, &iLit, &iLit + 1, 0, 0, 0, 0 );
333 if ( status == l_False )
334 continue;
335 if ( status == l_True )
336 return 0;
337 return -1;
338 }
339 return 1;
340 }
341 status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
342 if ( status == l_False )
343 return 1;
344 if ( status == l_True )
345 return 0;
346 return -1;
347}
l_True
#define l_True
Definition bmcBmcS.c:35
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
p
Cube * p
Definition exorList.c:222
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
Here is the caller graph for this function:

◆ Int2_ManCheckInit()

int Int2_ManCheckInit ( Gia_Man_t * p)

MACRO DEFINITIONS ///.

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

Synopsis [Returns 1 if AIG has transition into init state.]

Description []

SideEffects []

SeeAlso []

Definition at line 92 of file int2Bmc.c.

93{
94 sat_solver * pSat;
95 Cnf_Dat_t * pCnf;
96 Gia_Man_t * pNew;
97 Gia_Obj_t * pObj;
98 Vec_Int_t * vLits;
99 int i, Lit, RetValue = 0;
100 assert( Gia_ManRegNum(p) > 0 );
101 pNew = Jf_ManDeriveCnf( p, 0 );
102 pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
103 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
104 if ( pSat != NULL )
105 {
106 vLits = Vec_IntAlloc( Gia_ManRegNum(p) );
107 Gia_ManForEachRi( pNew, pObj, i )
108 {
109 Lit = pCnf->pVarNums[ Gia_ObjId(pNew, Gia_ObjFanin0(pObj)) ];
110 Lit = Abc_Var2Lit( Lit, Gia_ObjFaninC0(pObj) );
111 Vec_IntPush( vLits, Abc_LitNot(Lit) );
112 }
113 if ( sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ) == l_True )
114 RetValue = 1;
115 Vec_IntFree( vLits );
116 sat_solver_delete( pSat );
117 }
118 Cnf_DataFree( pCnf );
119 Gia_ManStop( pNew );
120 return RetValue;
121}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
sat_solver
#define sat_solver
Definition cecSatG2.c:34
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_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
Jf_ManDeriveCnf
Gia_Man_t * Jf_ManDeriveCnf(Gia_Man_t *p, int fCnfObjIds)
Definition giaJf.c:1749
Cnf_DataWriteIntoSolver
void * Cnf_DataWriteIntoSolver(Cnf_Dat_t *p, int nFrames, int fInit)
Definition cnfMan.c:579
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition cnf.h:63
Gia_Man_t_::pData
void * pData
Definition gia.h:198
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Int2_ManCreateFrames()

void Int2_ManCreateFrames ( Int2_Man_t * p,
int iFrame,
Vec_Int_t * vPrefCos )

Definition at line 219 of file int2Bmc.c.

220{
221 Gia_Obj_t * pObj;
222 int i, Entry, iLit;
223 // create storage room for unfolded IDs
224 for ( i = Vec_PtrSize(p->vMapFrames); i <= iFrame; i++ )
225 Vec_PtrPush( p->vMapFrames, Vec_IntStartFull( Gia_ManObjNum(p->pGia) ) );
226 assert( Vec_PtrSize(p->vMapFrames) == iFrame + 1 );
227 // create constant 0 node
228 if ( f == 0 )
229 {
230 iLit = 1;
231 Int2_ManWriteFrames( p, iFrame, iObj, 0 );
232 sat_solver_addclause( p->pGiaPref, &iLit, &iLit + 1 );
233 }
234 // start the stack
235 Vec_IntClear( p->vStack );
236 Vec_IntForEachEntry( vPrefCos, Entry, i )
237 {
238 pObj = Gia_ManCo( p->pGia, Entry );
239 Vec_IntPush( p->vStack, iFrame );
240 Vec_IntPush( p->vStack, Gia_ObjId(p->pGia, pObj) );
241 }
242 // construct unfolded AIG
243 while ( Vec_IntSize(p->vStack) > 0 )
244 {
245 int iObj = Vec_IntPop(p->vStack);
246 int iFrame = Vec_IntPop(p->vStack);
247 if ( Int2_ManCheckFrames(p, iFrame, iObj) >= 0 )
248 continue;
249 pObj = Gia_ManObj( p->pGia, iObj );
250 if ( Gia_ObjIsPi(p->pGia, pObj) )
251 Int2_ManWriteFrames( p, iFrame, iObj, Gia_ManAppendCi(p->pFrames) );
252 else if ( iFrame == 0 && Gia_ObjIsRo(p->pGia, iObj) )
253 Int2_ManWriteFrames( p, iFrame, iObj, 0 );
254 else if ( Gia_ObjIsRo(p->pGia, iObj) )
255 {
256 int iObjF = Gia_ObjId( p->pGia, Gia_ObjRoToRi(p->pGia, pObj) );
257 int iLit = Int2_ManCheckFrames( p, iFrame-1, iObjF );
258 if ( iLit >= 0 )
259 Int2_ManWriteFrames( p, iFrame, iObj, iLit );
260 else
261 {
262 Vec_IntPush( p->vStack, iFrame );
263 Vec_IntPush( p->vStack, iObj );
264 Vec_IntPush( p->vStack, iFrame-1 );
265 Vec_IntPush( p->vStack, iObjF );
266 }
267 }
268 else if ( Gia_ObjIsCo(pObj) )
269 {
270 int iObjF = Gia_ObjFaninId0(p->pGia, iObj) );
271 int iLit = Int2_ManCheckFrames( p, iFrame, iObjF );
272 if ( iLit >= 0 )
273 Int2_ManWriteFrames( p, iFrame, iObj, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
274 else
275 {
276 Vec_IntPush( p->vStack, iFrame );
277 Vec_IntPush( p->vStack, iObj );
278 Vec_IntPush( p->vStack, iFrame );
279 Vec_IntPush( p->vStack, iObjF );
280 }
281 }
282 else if ( Gia_ObjIsAnd(pObj) )
283 {
284 int iObjF0 = Gia_ObjFaninId0(p->pGia, iObj) );
285 int iLit0 = Int2_ManCheckFrames( p, iFrame, iObjF0 );
286 int iObjF1 = Gia_ObjFaninId1(p->pGia, iObj) );
287 int iLit1 = Int2_ManCheckFrames( p, iFrame, iObjF1 );
288 if ( iLit0 >= 0 && iLit1 >= 0 )
289 {
290 Entry = Gia_ManObjNum(pFrames);
291 iLit = Gia_ManHashAnd(pFrames, iLit0, iLit1);
292 Int2_ManWriteFrames( p, iFrame, iObj, iLit );
293 if ( Entry < Gia_ManObjNum(pFrames) )
294 {
295 assert( !Abc_LitIsCompl(iLit) );
296 sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), 0 );
297 }
298 }
299 else
300 {
301 Vec_IntPush( p->vStack, iFrame );
302 Vec_IntPush( p->vStack, iObj );
303 if ( iLit0 < 0 )
304 {
305 Vec_IntPush( p->vStack, iFrame );
306 Vec_IntPush( p->vStack, iObjF0 );
307 }
308 if ( iLit1 < 0 )
309 {
310 Vec_IntPush( p->vStack, iFrame );
311 Vec_IntPush( p->vStack, iObjF1 );
312 }
313 }
314 }
315 else assert( 0 );
316 }
317}
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver_add_and
#define sat_solver_add_and
Definition cecSatG2.c:38
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Int2_ManDupInit()

ABC_NAMESPACE_IMPL_START Gia_Man_t * Int2_ManDupInit ( Gia_Man_t * p,
int fVerbose )

DECLARATIONS ///.

CFile****************************************************************

FileName [int2Bmc.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [BMC used inside IMC.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 1, 2013.]

Revision [

Id
int2Bmc.c,v 1.00 2013/12/01 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Trasnforms AIG to transition into the init state.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file int2Bmc.c.

47{
48 Gia_Man_t * pNew, * pTemp;
49 Gia_Obj_t * pObj, * pObjRi, * pObjRo;
50 int i, iCtrl;
51 assert( Gia_ManRegNum(p) > 0 );
52 pNew = Gia_ManStart( 10000 );
53 pNew->pName = Abc_UtilStrsav( p->pName );
54 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
55 Gia_ManConst0(p)->Value = 0;
56 Gia_ManForEachCi( p, pObj, i )
57 {
58 if ( i == Gia_ManPiNum(p) )
59 iCtrl = Gia_ManAppendCi( pNew );
60 pObj->Value = Gia_ManAppendCi( pNew );
61 }
62 Gia_ManHashAlloc( pNew );
63 Gia_ManForEachAnd( p, pObj, i )
64 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
65 Gia_ManForEachPo( p, pObj, i )
66 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
67 Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
68 Gia_ManAppendCo( pNew, Gia_ManHashMux( pNew, iCtrl, pObjRo->Value, Gia_ObjFanin0Copy(pObjRi) ) );
69 Gia_ManHashStop( pNew );
70 Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
71 // remove dangling
72 pNew = Gia_ManCleanup( pTemp = pNew );
73 if ( fVerbose )
74 printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n",
75 Gia_ManAndNum(pTemp), Gia_ManAndNum(pNew) );
76 Gia_ManStop( pTemp );
77 return pNew;
78}
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition giaMan.c:764
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_ManHashMux
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition giaHash.c:692
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition gia.h:1256
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_Man_t_::pSpec
char * pSpec
Definition gia.h:100
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Here is the call graph for this function:

◆ Int2_ManFrameInit()

Gia_Man_t * Int2_ManFrameInit ( Gia_Man_t * p,
int nFrames,
int fVerbose )

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

Synopsis [Creates the BMC instance in the SAT solver.]

Description [The PIs are mapped in the natural order. The flop inputs are the last Gia_ManRegNum(p) variables of resulting SAT solver.]

SideEffects []

SeeAlso []

Definition at line 136 of file int2Bmc.c.

137{
138 Gia_Man_t * pFrames, * pTemp;
139 Gia_Obj_t * pObj;
140 int i, f;
141 pFrames = Gia_ManStart( 10000 );
142 pFrames->pName = Abc_UtilStrsav( p->pName );
143 pFrames->pSpec = Abc_UtilStrsav( p->pSpec );
144 Gia_ManConst0(p)->Value = 0;
145 // perform structural hashing
146 Gia_ManHashAlloc( pFrames );
147 for ( f = 0; f < nFrames; f++ )
148 {
149 Gia_ManForEachPi( p, pObj, i )
150 pObj->Value = Gia_ManAppendCi( pFrames );
151 Gia_ManForEachRo( p, pObj, i )
152 pObj->Value = f ? Gia_ObjRoToRi(p, pObj)->Value : 0;
153 Gia_ManForEachAnd( p, pObj, i )
154 pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
155 Gia_ManForEachRi( p, pObj, i )
156 pObj->Value = Gia_ObjFanin0Copy(pObj);
157 }
158 Gia_ManHashStop( pFrames );
159 // create flop inputs
160 Gia_ManForEachRi( p, pObj, i )
161 pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) );
162 // remove dangling
163 pFrames = Gia_ManCleanup( pTemp = pFrames );
164 if ( fVerbose )
165 printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n",
166 Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) );
167 Gia_ManStop( pTemp );
168 return pFrames;
169}
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Int2_ManSetupBmcSolver()

sat_solver * Int2_ManSetupBmcSolver ( Gia_Man_t * p,
int nFrames )

Definition at line 170 of file int2Bmc.c.

171{
172 Gia_Man_t * pFrames, * pTemp;
173 Cnf_Dat_t * pCnf;
174 sat_solver * pSat;
175 // unfold for the given number of timeframes
176 pFrames = Int2_ManFrameInit( p, nFrames, 1 );
177 assert( Gia_ManRegNum(pFrames) == 0 );
178 // derive CNF for the timeframes
179 pFrames = Jf_ManDeriveCnf( pTemp = pFrames, 0 ); Gia_ManStop( pTemp );
180 pCnf = (Cnf_Dat_t *)pFrames->pData; pFrames->pData = NULL;
181 // create SAT solver
182 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
183 if ( pSat != NULL )
184 {
185 Gia_Obj_t * pObj;
186 int i, nVars = sat_solver_nvars( pSat );
187 sat_solver_setnvars( pSat, nVars + Gia_ManPoNum(pFrames) );
188 // add clauses for the POs
189 Gia_ManForEachCo( pFrames, pObj, i )
190 sat_solver_add_buffer( pSat, nVars + i, pCnf->pVarNums[Gia_ObjId(pFrames, Gia_ObjFanin0(pObj))], Gia_ObjFaninC0(pObj) );
191 }
192 Cnf_DataFree( pCnf );
193 Gia_ManStop( pFrames );
194 return pSat;
195}
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Int2_ManFrameInit
Gia_Man_t * Int2_ManFrameInit(Gia_Man_t *p, int nFrames, int fVerbose)
Definition int2Bmc.c:136
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
Here is the call graph for this function: