ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
llb2Core.c File Reference
#include "llbInt.h"
Include dependency graph for llb2Core.c:

Go to the source code of this file.

Classes

struct  Llb_Img_t_
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Llb_Img_t_ Llb_Img_t
 DECLARATIONS ///.
 

Functions

DdNode * Llb_CoreComputeCube (DdManager *dd, Vec_Int_t *vVars, int fUseVarIndex, char *pValues)
 FUNCTION DEFINITIONS ///.
 
Abc_Cex_t * Llb_CoreDeriveCex (Llb_Img_t *p)
 
int Llb_CoreReachability_int (Llb_Img_t *p, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1)
 
int Llb_CoreReachability (Llb_Img_t *p)
 
Vec_Ptr_t * Llb_CoreConstructAll (Aig_Man_t *p, Vec_Ptr_t *vResult, Vec_Int_t *vVarsNs, abctime TimeTarget)
 
void Llb_CoreSetVarMaps (Llb_Img_t *p)
 
Llb_Img_t * Llb_CoreStart (Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
 
void Llb_CoreStop (Llb_Img_t *p)
 
int Llb_CoreExperiment (Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars, Vec_Ptr_t *vResult, abctime TimeTarget)
 
int Llb_ManReachMinCut (Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
 

Typedef Documentation

◆ Llb_Img_t

typedef typedefABC_NAMESPACE_IMPL_START struct Llb_Img_t_ Llb_Img_t

DECLARATIONS ///.

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

FileName [llb2Core.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Core procedure.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
llb2Core.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 30 of file llb2Core.c.

Function Documentation

◆ Llb_CoreComputeCube()

DdNode * Llb_CoreComputeCube ( DdManager * dd,
Vec_Int_t * vVars,
int fUseVarIndex,
char * pValues )

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes cube composed of given variables with given values.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file llb2Core.c.

69{
70 DdNode * bRes, * bVar, * bTemp;
71 int i, iVar, Index;
72 abctime TimeStop;
73 TimeStop = dd->TimeStop; dd->TimeStop = 0;
74 bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
75 Vec_IntForEachEntry( vVars, Index, i )
76 {
77 iVar = fUseVarIndex ? Index : i;
78 bVar = Cudd_NotCond( Cudd_bddIthVar(dd, iVar), (int)(pValues == NULL || pValues[i] != 1) );
79 bRes = Cudd_bddAnd( dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
80 Cudd_RecursiveDeref( dd, bTemp );
81 }
82 Cudd_Deref( bRes );
83 dd->TimeStop = TimeStop;
84 return bRes;
85}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the caller graph for this function:

◆ Llb_CoreConstructAll()

Vec_Ptr_t * Llb_CoreConstructAll ( Aig_Man_t * p,
Vec_Ptr_t * vResult,
Vec_Int_t * vVarsNs,
abctime TimeTarget )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 534 of file llb2Core.c.

535{
536 DdManager * dd;
537 Vec_Ptr_t * vDdMans;
538 Vec_Ptr_t * vLower, * vUpper = NULL;
539 int i;
540 vDdMans = Vec_PtrStart( Vec_PtrSize(vResult) );
541 Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vResult, vLower, i )
542 {
543 if ( i < Vec_PtrSize(vResult) - 1 )
544 dd = Llb_ImgPartition( p, vLower, vUpper, TimeTarget );
545 else
546 dd = Llb_DriverLastPartition( p, vVarsNs, TimeTarget );
547 if ( dd == NULL )
548 {
549 Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
550 {
551 if ( dd == NULL )
552 continue;
553 if ( dd->bFunc )
554 Cudd_RecursiveDeref( dd, dd->bFunc );
555 Extra_StopManager( dd );
556 }
557 Vec_PtrFree( vDdMans );
558 return NULL;
559 }
560 Vec_PtrWriteEntry( vDdMans, i, dd );
561 vUpper = vLower;
562 }
563 return vDdMans;
564}
p
Cube * p
Definition exorList.c:222
Extra_StopManager
void Extra_StopManager(DdManager *dd)
Definition extraBddMisc.c:223
Llb_DriverLastPartition
DdManager * Llb_DriverLastPartition(Aig_Man_t *p, Vec_Int_t *vVarsNs, abctime TimeTarget)
Definition llb2Driver.c:163
Llb_ImgPartition
DdManager * Llb_ImgPartition(Aig_Man_t *p, Vec_Ptr_t *vLower, Vec_Ptr_t *vUpper, abctime TimeTarget)
Definition llb2Image.c:183
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition vecPtr.h:63
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_CoreDeriveCex()

Abc_Cex_t * Llb_CoreDeriveCex ( Llb_Img_t * p)

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

Synopsis [Derives counter-example by backward reachability.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file llb2Core.c.

99{
100 Abc_Cex_t * pCex;
101 Aig_Obj_t * pObj;
102 Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
103 DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
104 int i, v, RetValue, nPiOffset;
105 char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
106 assert( Vec_PtrSize(p->vRings) > 0 );
107
108 p->dd->TimeStop = 0;
109 p->ddR->TimeStop = 0;
110
111 // get supports and quantified variables
112 Vec_PtrReverseOrder( p->vDdMans );
113 vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsNs, p->vVarsCs, 1, 0 );
114 Llb_ImgSchedule( vSupps, &vQuant0, &vQuant1, 0 );
115 Vec_VecFree( (Vec_Vec_t *)vSupps );
116 Llb_ImgQuantifyReset( p->vDdMans );
117// Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0 );
118
119 // allocate room for the counter-example
120 pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
121 pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
122 pCex->iPo = -1;
123
124 // get the last cube
125 bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
126 RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
127 Cudd_RecursiveDeref( p->ddR, bOneCube );
128 assert( RetValue );
129
130 // write PIs of counter-example
131 nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
132 Saig_ManForEachPi( p->pAig, pObj, i )
133 if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
134 Abc_InfoSetBit( pCex->pData, nPiOffset + i );
135
136 // write state in terms of NS variables
137 if ( Vec_PtrSize(p->vRings) > 1 )
138 {
139 bState = Llb_CoreComputeCube( p->dd, p->vVarsNs, 1, pValues ); Cudd_Ref( bState );
140 }
141 // perform backward analysis
142 Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
143 {
144 if ( v == Vec_PtrSize(p->vRings) - 1 )
145 continue;
146 // compute the next states
147 bImage = Llb_ImgComputeImage( p->pAig, p->vDdMans, p->dd, bState,
148 vQuant0, vQuant1, p->vDriRefs, p->pPars->TimeTarget, 1, 0, 0 );
149 assert( bImage != NULL );
150 Cudd_Ref( bImage );
151 Cudd_RecursiveDeref( p->dd, bState );
152//Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
153
154 // move reached states into ring manager
155 bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
156 Cudd_RecursiveDeref( p->dd, bTemp );
157
158 // intersect with the previous set
159 bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
160 Cudd_RecursiveDeref( p->ddR, bImage );
161
162 // find any assignment of the BDD
163 RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
164 Cudd_RecursiveDeref( p->ddR, bOneCube );
165 assert( RetValue );
166
167 // write PIs of counter-example
168 nPiOffset -= Saig_ManPiNum(p->pAig);
169 Saig_ManForEachPi( p->pAig, pObj, i )
170 if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
171 Abc_InfoSetBit( pCex->pData, nPiOffset + i );
172
173 // check that we get the init state
174 if ( v == 0 )
175 {
176 Saig_ManForEachLo( p->pAig, pObj, i )
177 assert( pValues[i] == 0 );
178 break;
179 }
180
181 // write state in terms of NS variables
182 bState = Llb_CoreComputeCube( p->dd, p->vVarsNs, 1, pValues ); Cudd_Ref( bState );
183 }
184 assert( nPiOffset == Saig_ManRegNum(p->pAig) );
185 // update the output number
186 RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
187 assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
188 pCex->iPo = RetValue;
189 // cleanup
190 ABC_FREE( pValues );
191 Vec_VecFree( (Vec_Vec_t *)vQuant0 );
192 Vec_VecFree( (Vec_Vec_t *)vQuant1 );
193 return pCex;
194}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Extra_TransferPermute
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
Definition extraBddMisc.c:87
Llb_CoreComputeCube
DdNode * Llb_CoreComputeCube(DdManager *dd, Vec_Int_t *vVars, int fUseVarIndex, char *pValues)
FUNCTION DEFINITIONS ///.
Definition llb2Core.c:68
Llb_ImgQuantifyReset
void Llb_ImgQuantifyReset(Vec_Ptr_t *vDdMans)
Definition llb2Image.c:340
Llb_ImgSchedule
void Llb_ImgSchedule(Vec_Ptr_t *vSupps, Vec_Ptr_t **pvQuant0, Vec_Ptr_t **pvQuant1, int fVerbose)
Definition llb2Image.c:122
Llb_ImgSupports
Vec_Ptr_t * Llb_ImgSupports(Aig_Man_t *p, Vec_Ptr_t *vDdMans, Vec_Int_t *vStart, Vec_Int_t *vStop, int fAddPis, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition llb2Image.c:48
Llb_ImgComputeImage
DdNode * Llb_ImgComputeImage(Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, DdManager *dd, DdNode *bInit, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1, Vec_Int_t *vDriRefs, abctime TimeTarget, int fBackward, int fReorder, int fVerbose)
Definition llb2Image.c:364
Saig_ManFindFailedPoCex
int Saig_ManFindFailedPoCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition saigDup.c:436
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
assert
#define assert(ex)
Definition util_old.h:213
Vec_Vec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Vec_t_ Vec_Vec_t
INCLUDES ///.
Definition vecVec.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_CoreExperiment()

int Llb_CoreExperiment ( Aig_Man_t * pInit,
Aig_Man_t * pAig,
Gia_ParLlb_t * pPars,
Vec_Ptr_t * vResult,
abctime TimeTarget )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 694 of file llb2Core.c.

695{
696 int RetValue;
697 Llb_Img_t * p;
698// printf( "\n" );
699// pPars->fVerbose = 1;
700 p = Llb_CoreStart( pInit, pAig, pPars );
701 p->vDdMans = Llb_CoreConstructAll( pAig, vResult, p->vVarsNs, TimeTarget );
702 if ( p->vDdMans == NULL )
703 {
704 if ( !pPars->fSilent )
705 printf( "Reached timeout (%d seconds) while deriving the partitions.\n", pPars->TimeLimit );
706 Llb_CoreStop( p );
707 return -1;
708 }
709 RetValue = Llb_CoreReachability( p );
710 Llb_CoreStop( p );
711 return RetValue;
712}
Llb_CoreConstructAll
Vec_Ptr_t * Llb_CoreConstructAll(Aig_Man_t *p, Vec_Ptr_t *vResult, Vec_Int_t *vVarsNs, abctime TimeTarget)
Definition llb2Core.c:534
Llb_Img_t
typedefABC_NAMESPACE_IMPL_START struct Llb_Img_t_ Llb_Img_t
DECLARATIONS ///.
Definition llb2Core.c:30
Llb_CoreStop
void Llb_CoreStop(Llb_Img_t *p)
Definition llb2Core.c:650
Llb_CoreStart
Llb_Img_t * Llb_CoreStart(Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
Definition llb2Core.c:618
Llb_CoreReachability
int Llb_CoreReachability(Llb_Img_t *p)
Definition llb2Core.c:499
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_CoreReachability()

int Llb_CoreReachability ( Llb_Img_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 499 of file llb2Core.c.

500{
501 Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
502 int RetValue;
503 // get supports and quantified variables
504 if ( p->pPars->fBackward )
505 {
506 Vec_PtrReverseOrder( p->vDdMans );
507 vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsNs, p->vVarsCs, 0, p->pPars->fVeryVerbose );
508 }
509 else
510 vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsCs, p->vVarsNs, 0, p->pPars->fVeryVerbose );
511 Llb_ImgSchedule( vSupps, &vQuant0, &vQuant1, p->pPars->fVeryVerbose );
512 Vec_VecFree( (Vec_Vec_t *)vSupps );
513 // remove variables
514 Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0, p->pPars->fVeryVerbose );
515 // perform reachability
516 RetValue = Llb_CoreReachability_int( p, vQuant0, vQuant1 );
517 Vec_VecFree( (Vec_Vec_t *)vQuant0 );
518 Vec_VecFree( (Vec_Vec_t *)vQuant1 );
519 return RetValue;
520}
Llb_CoreReachability_int
int Llb_CoreReachability_int(Llb_Img_t *p, Vec_Ptr_t *vQuant0, Vec_Ptr_t *vQuant1)
Definition llb2Core.c:207
Llb_ImgQuantifyFirst
void Llb_ImgQuantifyFirst(Aig_Man_t *pAig, Vec_Ptr_t *vDdMans, Vec_Ptr_t *vQuant0, int fVerbose)
Definition llb2Image.c:288
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_CoreReachability_int()

int Llb_CoreReachability_int ( Llb_Img_t * p,
Vec_Ptr_t * vQuant0,
Vec_Ptr_t * vQuant1 )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 207 of file llb2Core.c.

208{
209 int * pLoc2Glo = p->pPars->fBackward? Vec_IntArray( p->vCs2Glo ) : Vec_IntArray( p->vNs2Glo );
210 int * pLoc2GloR = p->pPars->fBackward? Vec_IntArray( p->vNs2Glo ) : Vec_IntArray( p->vCs2Glo );
211 int * pGlo2Loc = p->pPars->fBackward? Vec_IntArray( p->vGlo2Ns ) : Vec_IntArray( p->vGlo2Cs );
212 DdNode * bCurrent, * bReached, * bNext, * bTemp;
213 abctime clk2, clk = Abc_Clock();
214 int nIters, nBddSize;//, iOutFail = -1;
215/*
216 // compute time to stop
217 if ( p->pPars->TimeLimit )
218 p->pPars->TimeTarget = Abc_Clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
219 else
220 p->pPars->TimeTarget = 0;
221*/
222
223 if ( Abc_Clock() > p->pPars->TimeTarget )
224 {
225 if ( !p->pPars->fSilent )
226 printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit );
227 p->pPars->iFrame = -1;
228 return -1;
229 }
230
231 // set the stop time parameter
232 p->dd->TimeStop = p->pPars->TimeTarget;
233 p->ddG->TimeStop = p->pPars->TimeTarget;
234 p->ddR->TimeStop = p->pPars->TimeTarget;
235
236 // compute initial states
237 if ( p->pPars->fBackward )
238 {
239 // create init state in the global manager
240 bTemp = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );
241 if ( bTemp == NULL )
242 {
243 if ( !p->pPars->fSilent )
244 printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
245 p->pPars->iFrame = -1;
246 return -1;
247 }
248 Cudd_Ref( bTemp );
249 // create bad state in the ring manager
250 p->ddR->bFunc = Llb_CoreComputeCube( p->ddR, p->vVarsCs, 0, NULL ); Cudd_Ref( p->ddR->bFunc );
251 bCurrent = Llb_BddQuantifyPis( p->pInit, p->ddR, bTemp ); Cudd_Ref( bCurrent );
252 Cudd_RecursiveDeref( p->ddR, bTemp );
253 bReached = Cudd_bddTransfer( p->ddR, p->ddG, bCurrent ); Cudd_Ref( bReached );
254 Cudd_RecursiveDeref( p->ddR, bCurrent );
255 // move init state to the working manager
256 bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Loc );
257 if ( bCurrent == NULL )
258 {
259 Cudd_RecursiveDeref( p->ddG, bReached );
260 if ( !p->pPars->fSilent )
261 printf( "Reached timeout (%d seconds) during transfer 0.\n", p->pPars->TimeLimit );
262 p->pPars->iFrame = -1;
263 return -1;
264 }
265 Cudd_Ref( bCurrent );
266 }
267 else
268 {
269 // create bad state in the ring manager
270 p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );
271 if ( p->ddR->bFunc == NULL )
272 {
273 if ( !p->pPars->fSilent )
274 printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
275 p->pPars->iFrame = -1;
276 return -1;
277 }
278 Cudd_Ref( p->ddR->bFunc );
279 // create init state in the working and global manager
280 bCurrent = Llb_CoreComputeCube( p->dd, p->vVarsCs, 1, NULL ); Cudd_Ref( bCurrent );
281 bReached = Llb_CoreComputeCube( p->ddG, p->vVarsCs, 0, NULL ); Cudd_Ref( bReached );
282//Extra_bddPrint( p->dd, bCurrent ); printf( "\n" );
283//Extra_bddPrint( p->ddG, bReached ); printf( "\n" );
284 }
285
286 // compute onion rings
287 for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
288 {
289 clk2 = Abc_Clock();
290 // check the runtime limit
291 if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
292 {
293 if ( !p->pPars->fSilent )
294 printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
295 p->pPars->iFrame = nIters - 1;
296 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
297 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
298 return -1;
299 }
300
301 // save the onion ring
302 bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pLoc2GloR );
303 if ( bTemp == NULL )
304 {
305 if ( !p->pPars->fSilent )
306 printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
307 p->pPars->iFrame = nIters - 1;
308 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
309 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
310 return -1;
311 }
312 Cudd_Ref( bTemp );
313 Vec_PtrPush( p->vRings, bTemp );
314
315 // check it for bad states
316 if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
317 {
318 assert( p->pInit->pSeqModel == NULL );
319 if ( !p->pPars->fBackward )
320 p->pInit->pSeqModel = Llb_CoreDeriveCex( p );
321 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
322 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
323 if ( !p->pPars->fSilent )
324 {
325 if ( !p->pPars->fBackward )
326 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, p->pInit->pName, nIters );
327 else
328 Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
329 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
330 }
331 p->pPars->iFrame = nIters - 1;
332 return 0;
333 }
334
335 // compute the next states
336 bNext = Llb_ImgComputeImage( p->pAig, p->vDdMans, p->dd, bCurrent,
337 vQuant0, vQuant1, p->vDriRefs, p->pPars->TimeTarget,
338 p->pPars->fBackward, p->pPars->fReorder, p->pPars->fVeryVerbose );
339 if ( bNext == NULL )
340 {
341 if ( !p->pPars->fSilent )
342 printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
343 p->pPars->iFrame = nIters - 1;
344 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
345 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
346 return -1;
347 }
348 Cudd_Ref( bNext );
349 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
350//Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" );
351
352 // remap these states into the global manager
353// bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo ); Cudd_Ref( bNext );
354// Cudd_RecursiveDeref( p->dd, bTemp );
355
356// bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pLoc2Glo, p->pPars->TimeTarget );
357 bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo );
358 if ( bNext == NULL )
359 {
360 if ( !p->pPars->fSilent )
361 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
362 p->pPars->iFrame = nIters - 1;
363 Cudd_RecursiveDeref( p->dd, bTemp );
364 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
365 return -1;
366 }
367 Cudd_Ref( bNext );
368 Cudd_RecursiveDeref( p->dd, bTemp );
369
370 nBddSize = Cudd_DagSize(bNext);
371 // check if there are any new states
372 if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states
373 {
374 Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
375 break;
376 }
377
378 // get the new states
379 bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );
380 if ( bCurrent == NULL )
381 {
382 if ( !p->pPars->fSilent )
383 printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
384 p->pPars->iFrame = nIters - 1;
385 Cudd_RecursiveDeref( p->ddG, bNext );
386 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
387 return -1;
388 }
389 Cudd_Ref( bCurrent );
390
391 // remap these states into the current state vars
392// bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc ); Cudd_Ref( bCurrent );
393// Cudd_RecursiveDeref( p->ddG, bTemp );
394
395// bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc, p->pPars->TimeTarget );
396 bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc );
397 if ( bCurrent == NULL )
398 {
399 if ( !p->pPars->fSilent )
400 printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
401 p->pPars->iFrame = nIters - 1;
402 Cudd_RecursiveDeref( p->ddG, bTemp );
403 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
404 return -1;
405 }
406 Cudd_Ref( bCurrent );
407 Cudd_RecursiveDeref( p->ddG, bTemp );
408
409 // add to the reached states
410 bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext ); Cudd_Ref( bReached );
411 Cudd_RecursiveDeref( p->ddG, bTemp );
412 Cudd_RecursiveDeref( p->ddG, bNext );
413 bNext = NULL;
414
415 if ( p->pPars->fVeryVerbose )
416 {
417 double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
418// Extra_bddPrint( p->ddG, bReached );printf( "\n" );
419 fprintf( stdout, " Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
420 fflush( stdout );
421 }
422 if ( p->pPars->fVerbose )
423 {
424 fprintf( stdout, "F =%3d : ", nIters );
425 fprintf( stdout, "Image =%6d ", nBddSize );
426 fprintf( stdout, "(%4d%4d) ",
427 Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
428 fprintf( stdout, "Reach =%6d ", Cudd_DagSize(bReached) );
429 fprintf( stdout, "(%4d%4d) ",
430 Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
431 Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
432 }
433
434 // check timeframe limit
435 if ( nIters == p->pPars->nIterMax - 1 )
436 {
437 if ( !p->pPars->fSilent )
438 printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax );
439 p->pPars->iFrame = nIters;
440 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
441 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
442 return -1;
443 }
444 }
445 if ( bReached == NULL )
446 {
447 p->pPars->iFrame = nIters - 1;
448 return 0; // reachable
449 }
450 if ( bCurrent )
451 Cudd_RecursiveDeref( p->dd, bCurrent );
452 // report the stats
453 if ( p->pPars->fVerbose )
454 {
455 double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
456 if ( nIters >= p->pPars->nIterMax )
457 fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
458 else
459 fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
460 fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
461 fflush( stdout );
462 }
463 if ( p->pPars->fDumpReached )
464 {
465 Llb_ManDumpReached( p->ddG, bReached, p->pAig->pName, "reached.blif" );
466 printf( "Reached states with %d BDD nodes are dumpted into file \"reached.blif\".\n", Cudd_DagSize(bReached) );
467 }
468 Cudd_RecursiveDeref( p->ddG, bReached );
469 if ( nIters >= p->pPars->nIterMax )
470 {
471 if ( !p->pPars->fSilent )
472 {
473 printf( "Verified only for states reachable in %d frames. ", nIters );
474 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
475 }
476 p->pPars->iFrame = p->pPars->nIterMax;
477 return -1; // undecided
478 }
479 if ( !p->pPars->fSilent )
480 {
481 printf( "The miter is proved unreachable after %d iterations. ", nIters );
482 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
483 }
484 p->pPars->iFrame = nIters - 1;
485 return 1; // unreachable
486}
Llb_BddComputeBad
ABC_NAMESPACE_IMPL_START DdNode * Llb_BddComputeBad(Aig_Man_t *pInit, DdManager *dd, abctime TimeOut)
DECLARATIONS ///.
Definition llb2Bad.c:45
Llb_BddQuantifyPis
DdNode * Llb_BddQuantifyPis(Aig_Man_t *pInit, DdManager *dd, DdNode *bFunc)
Definition llb2Bad.c:109
Llb_CoreDeriveCex
Abc_Cex_t * Llb_CoreDeriveCex(Llb_Img_t *p)
Definition llb2Core.c:98
Llb_ManDumpReached
void Llb_ManDumpReached(DdManager *ddG, DdNode *bReached, char *pModel, char *pFileName)
Definition llb2Dump.c:63
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_CoreSetVarMaps()

void Llb_CoreSetVarMaps ( Llb_Img_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 577 of file llb2Core.c.

578{
579 Aig_Obj_t * pObj;
580 int i, iVarCs, iVarNs;
581 assert( p->vVarsCs != NULL );
582 assert( p->vVarsNs != NULL );
583 assert( p->vCs2Glo == NULL );
584 assert( p->vNs2Glo == NULL );
585 assert( p->vGlo2Cs == NULL );
586 assert( p->vGlo2Ns == NULL );
587 p->vCs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
588 p->vNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
589 p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
590 p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
591 for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
592 {
593 iVarCs = Vec_IntEntry( p->vVarsCs, i );
594 iVarNs = Vec_IntEntry( p->vVarsNs, i );
595 assert( iVarCs >= 0 && iVarCs < Aig_ManObjNumMax(p->pAig) );
596 assert( iVarNs >= 0 && iVarNs < Aig_ManObjNumMax(p->pAig) );
597 Vec_IntWriteEntry( p->vCs2Glo, iVarCs, i );
598 Vec_IntWriteEntry( p->vNs2Glo, iVarNs, i );
599 Vec_IntWriteEntry( p->vGlo2Cs, i, iVarCs );
600 Vec_IntWriteEntry( p->vGlo2Ns, i, iVarNs );
601 }
602 // add mapping of the PIs
603 Saig_ManForEachPi( p->pAig, pObj, i )
604 Vec_IntWriteEntry( p->vCs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
605}
Here is the caller graph for this function:

◆ Llb_CoreStart()

Llb_Img_t * Llb_CoreStart ( Aig_Man_t * pInit,
Aig_Man_t * pAig,
Gia_ParLlb_t * pPars )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 618 of file llb2Core.c.

619{
620 Llb_Img_t * p;
621 p = ABC_CALLOC( Llb_Img_t, 1 );
622 p->pInit = pInit;
623 p->pAig = pAig;
624 p->pPars = pPars;
625 p->dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
626 p->ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
627 p->ddR = Cudd_Init( Aig_ManCiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
628 Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
629 Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
630 Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
631 p->vRings = Vec_PtrAlloc( 100 );
632 p->vDriRefs = Llb_DriverCountRefs( pAig );
633 p->vVarsCs = Llb_DriverCollectCs( pAig );
634 p->vVarsNs = Llb_DriverCollectNs( pAig, p->vDriRefs );
635 Llb_CoreSetVarMaps( p );
636 return p;
637}
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Llb_CoreSetVarMaps
void Llb_CoreSetVarMaps(Llb_Img_t *p)
Definition llb2Core.c:577
Llb_DriverCountRefs
ABC_NAMESPACE_IMPL_START Vec_Int_t * Llb_DriverCountRefs(Aig_Man_t *p)
DECLARATIONS ///.
Definition llb2Driver.c:56
Llb_DriverCollectCs
Vec_Int_t * Llb_DriverCollectCs(Aig_Man_t *pAig)
Definition llb2Driver.c:106
Llb_DriverCollectNs
Vec_Int_t * Llb_DriverCollectNs(Aig_Man_t *pAig, Vec_Int_t *vDriRefs)
Definition llb2Driver.c:78
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_CoreStop()

void Llb_CoreStop ( Llb_Img_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 650 of file llb2Core.c.

651{
652 DdManager * dd;
653 DdNode * bTemp;
654 int i;
655 if ( p->vDdMans )
656 Vec_PtrForEachEntry( DdManager *, p->vDdMans, dd, i )
657 {
658 if ( dd->bFunc )
659 Cudd_RecursiveDeref( dd, dd->bFunc );
660 if ( dd->bFunc2 )
661 Cudd_RecursiveDeref( dd, dd->bFunc2 );
662 Extra_StopManager( dd );
663 }
664 Vec_PtrFreeP( &p->vDdMans );
665 if ( p->ddR->bFunc )
666 Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
667 Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
668 Cudd_RecursiveDeref( p->ddR, bTemp );
669 Vec_PtrFree( p->vRings );
670 Extra_StopManager( p->dd );
671 Extra_StopManager( p->ddG );
672 Extra_StopManager( p->ddR );
673 Vec_IntFreeP( &p->vDriRefs );
674 Vec_IntFreeP( &p->vVarsCs );
675 Vec_IntFreeP( &p->vVarsNs );
676 Vec_IntFreeP( &p->vCs2Glo );
677 Vec_IntFreeP( &p->vNs2Glo );
678 Vec_IntFreeP( &p->vGlo2Cs );
679 Vec_IntFreeP( &p->vGlo2Ns );
680 ABC_FREE( p );
681}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_ManReachMinCut()

int Llb_ManReachMinCut ( Aig_Man_t * pAig,
Gia_ParLlb_t * pPars )

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

Synopsis [Finds balanced cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 725 of file llb2Core.c.

726{
727 extern Vec_Ptr_t * Llb_ManComputeCuts( Aig_Man_t * p, int Num, int fVerbose, int fVeryVerbose );
728 Vec_Ptr_t * vResult;
729 Aig_Man_t * p;
730 int RetValue = -1;
731 abctime clk = Abc_Clock();
732
733 // compute time to stop
734 pPars->TimeTarget = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
735
736 p = Aig_ManDupFlopsOnly( pAig );
737//Aig_ManShow( p, 0, NULL );
738 if ( pPars->fVerbose )
739 Aig_ManPrintStats( pAig );
740 if ( pPars->fVerbose )
741 Aig_ManPrintStats( p );
742 Aig_ManFanoutStart( p );
743
744 vResult = Llb_ManComputeCuts( p, pPars->nPartValue, pPars->fVerbose, pPars->fVeryVerbose );
745
746 if ( pPars->TimeLimit && Abc_Clock() > pPars->TimeTarget )
747 {
748 if ( !pPars->fSilent )
749 printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit );
750
751 Vec_VecFree( (Vec_Vec_t *)vResult );
752 Aig_ManFanoutStop( p );
753 Aig_ManCleanMarkAB( p );
754 Aig_ManStop( p );
755 return RetValue;
756 }
757
758 if ( !pPars->fSkipReach )
759 RetValue = Llb_CoreExperiment( pAig, p, pPars, vResult, pPars->TimeTarget );
760
761 Vec_VecFree( (Vec_Vec_t *)vResult );
762 Aig_ManFanoutStop( p );
763 Aig_ManCleanMarkAB( p );
764 Aig_ManStop( p );
765
766 if ( RetValue == -1 )
767 Abc_PrintTime( 1, "Total runtime of the min-cut-based reachability engine", Abc_Clock() - clk );
768 return RetValue;
769}
Aig_ManFanoutStart
void Aig_ManFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition aigFanout.c:56
Aig_ManFanoutStop
void Aig_ManFanoutStop(Aig_Man_t *p)
Definition aigFanout.c:89
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition aigMan.c:379
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManCleanMarkAB
void Aig_ManCleanMarkAB(Aig_Man_t *p)
Definition aigUtil.c:186
Aig_ManDupFlopsOnly
Aig_Man_t * Aig_ManDupFlopsOnly(Aig_Man_t *p)
Definition aigDup.c:871
Llb_CoreExperiment
int Llb_CoreExperiment(Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars, Vec_Ptr_t *vResult, abctime TimeTarget)
Definition llb2Core.c:694
Llb_ManComputeCuts
Vec_Ptr_t * Llb_ManComputeCuts(Aig_Man_t *p, int Num, int fVerbose, int fVeryVerbose)
Definition llb2Flow.c:1226
Here is the call graph for this function: