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

Go to the source code of this file.

Classes

struct  Llb_Mnn_t_
 

Typedefs

typedef typedefABC_NAMESPACE_IMPL_START struct Llb_Mnn_t_ Llb_Mnn_t
 DECLARATIONS ///.
 

Functions

int Llb_NonlinFindBestVar (DdManager *dd, DdNode *bFunc, Aig_Man_t *pAig)
 FUNCTION DEFINITIONS ///.
 
void Llb_NonlinTrySubsetting (DdManager *dd, DdNode *bFunc)
 
void Llb_NonlinPrepareVarMap (Llb_Mnn_t *p)
 
DdNode * Llb_NonlinComputeInitState (Aig_Man_t *pAig, DdManager *dd)
 
Abc_Cex_t * Llb_NonlinDeriveCex (Llb_Mnn_t *p)
 
int Llb_NonlinReoHook (DdManager *dd, char *Type, void *Method)
 
int Llb_NonlinCompPerms (DdManager *dd, int *pVar2Lev)
 
int Llb_NonlinReachability (Llb_Mnn_t *p)
 
Llb_Mnn_t * Llb_MnnStart (Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
 
void Llb_MnnStop (Llb_Mnn_t *p)
 
void Llb_NonlinExperiment (Aig_Man_t *pAig, int Num)
 
int Llb_NonlinCoreReach (Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
 

Variables

abctime timeBuild
 
abctime timeAndEx
 
abctime timeOther
 
int nSuppMax
 

Typedef Documentation

◆ Llb_Mnn_t

typedef typedefABC_NAMESPACE_IMPL_START struct Llb_Mnn_t_ Llb_Mnn_t

DECLARATIONS ///.

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

FileName [llb2Nonlin.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [BDD based reachability.]

Synopsis [Non-linear quantification scheduling.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 30 of file llb3Nonlin.c.

Function Documentation

◆ Llb_MnnStart()

Llb_Mnn_t * Llb_MnnStart ( Aig_Man_t * pInit,
Aig_Man_t * pAig,
Gia_ParLlb_t * pPars )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 698 of file llb3Nonlin.c.

699{
700 Llb_Mnn_t * p;
701 Aig_Obj_t * pObj;
702 int i;
703 p = ABC_CALLOC( Llb_Mnn_t, 1 );
704 p->pInit = pInit;
705 p->pAig = pAig;
706 p->pPars = pPars;
707 p->dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
708 p->ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
709 p->ddR = Cudd_Init( Aig_ManCiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
710 Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
711 Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
712 Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
713 p->vRings = Vec_PtrAlloc( 100 );
714 // create leaves
715 p->vLeaves = Vec_PtrAlloc( Aig_ManCiNum(pAig) );
716 Aig_ManForEachCi( pAig, pObj, i )
717 Vec_PtrPush( p->vLeaves, pObj );
718 // create roots
719 p->vRoots = Vec_PtrAlloc( Aig_ManCoNum(pAig) );
720 Saig_ManForEachLi( pAig, pObj, i )
721 Vec_PtrPush( p->vRoots, pObj );
722 // variables to quantify
723 p->pOrderL = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
724 p->pOrderL2= ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
725 p->pOrderG = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
726 p->pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
727 Aig_ManForEachCi( pAig, pObj, i )
728 p->pVars2Q[Aig_ObjId(pObj)] = 1;
729 for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
730 p->pOrderL[i] = p->pOrderL2[i] = p->pOrderG[i] = i;
731 Llb_NonlinPrepareVarMap( p );
732 return p;
733}
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
p
Cube * p
Definition exorList.c:222
Llb_NonlinPrepareVarMap
void Llb_NonlinPrepareVarMap(Llb_Mnn_t *p)
Definition llb3Nonlin.c:175
Llb_Mnn_t
typedefABC_NAMESPACE_IMPL_START struct Llb_Mnn_t_ Llb_Mnn_t
DECLARATIONS ///.
Definition llb3Nonlin.c:30
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_MnnStop()

void Llb_MnnStop ( Llb_Mnn_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 746 of file llb3Nonlin.c.

747{
748 DdNode * bTemp;
749 int i;
750 if ( p->pPars->fVerbose )
751 {
752 p->timeOther = p->timeTotal - p->timeImage - p->timeTran1 - p->timeTran2 - p->timeGloba;
753 p->timeReoG = Cudd_ReadReorderingTime(p->ddG);
754 ABC_PRTP( "Image ", p->timeImage, p->timeTotal );
755 ABC_PRTP( " build ", timeBuild, p->timeTotal );
756 ABC_PRTP( " and-ex ", timeAndEx, p->timeTotal );
757 ABC_PRTP( " other ", timeOther, p->timeTotal );
758 ABC_PRTP( "Transfer1", p->timeTran1, p->timeTotal );
759 ABC_PRTP( "Transfer2", p->timeTran2, p->timeTotal );
760 ABC_PRTP( "Global ", p->timeGloba, p->timeTotal );
761 ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
762 ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
763 ABC_PRTP( " reo ", p->timeReo, p->timeTotal );
764 ABC_PRTP( " reoG ", p->timeReoG, p->timeTotal );
765 }
766 if ( p->ddR->bFunc )
767 Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
768 Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
769 Cudd_RecursiveDeref( p->ddR, bTemp );
770 Vec_PtrFree( p->vRings );
771 if ( p->ddG->bFunc )
772 Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc );
773 if ( p->ddG->bFunc2 )
774 Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
775// printf( "manager1\n" );
776// Extra_StopManager( p->dd );
777// printf( "manager2\n" );
778 Extra_StopManager( p->ddG );
779// printf( "manager3\n" );
780 Extra_StopManager( p->ddR );
781 Vec_IntFreeP( &p->vCs2Glo );
782 Vec_IntFreeP( &p->vNs2Glo );
783 Vec_IntFreeP( &p->vGlo2Cs );
784 Vec_IntFreeP( &p->vGlo2Ns );
785 Vec_PtrFree( p->vLeaves );
786 Vec_PtrFree( p->vRoots );
787 ABC_FREE( p->pVars2Q );
788 ABC_FREE( p->pOrderL );
789 ABC_FREE( p->pOrderL2 );
790 ABC_FREE( p->pOrderG );
791 ABC_FREE( p );
792}
ABC_PRTP
#define ABC_PRTP(a, t, T)
Definition abc_global.h:258
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Extra_StopManager
void Extra_StopManager(DdManager *dd)
Definition extraBddMisc.c:223
timeOther
abctime timeOther
Definition llb3Image.c:82
timeAndEx
abctime timeAndEx
Definition llb3Image.c:82
timeBuild
abctime timeBuild
Definition llb3Image.c:82
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_NonlinCompPerms()

int Llb_NonlinCompPerms ( DdManager * dd,
int * pVar2Lev )

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

Synopsis [Perform reachability with hints.]

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file llb3Nonlin.c.

403{
404 DdSubtable * pSubt;
405 int i, Sum = 0, Entry;
406 for ( i = 0; i < dd->size; i++ )
407 {
408 pSubt = &(dd->subtables[dd->perm[i]]);
409 if ( pSubt->keys == pSubt->dead + 1 )
410 continue;
411 Entry = Abc_MaxInt(dd->perm[i], pVar2Lev[i]) - Abc_MinInt(dd->perm[i], pVar2Lev[i]);
412 Sum += Entry;
413//printf( "%d-%d(%d) ", dd->perm[i], pV2L[i], Entry );
414 }
415 return Sum;
416}
Here is the caller graph for this function:

◆ Llb_NonlinComputeInitState()

DdNode * Llb_NonlinComputeInitState ( Aig_Man_t * pAig,
DdManager * dd )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file llb3Nonlin.c.

215{
216 Aig_Obj_t * pObj;
217 DdNode * bRes, * bVar, * bTemp;
218 int i, iVar;
219 abctime TimeStop;
220 TimeStop = dd->TimeStop; dd->TimeStop = 0;
221 bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
222 Saig_ManForEachLo( pAig, pObj, i )
223 {
224 iVar = (Cudd_ReadSize(dd) == Aig_ManRegNum(pAig)) ? i : Aig_ObjId(pObj);
225 bVar = Cudd_bddIthVar( dd, iVar );
226 bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
227 Cudd_RecursiveDeref( dd, bTemp );
228 }
229 Cudd_Deref( bRes );
230 dd->TimeStop = TimeStop;
231 return bRes;
232}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Here is the caller graph for this function:

◆ Llb_NonlinCoreReach()

int Llb_NonlinCoreReach ( Aig_Man_t * pAig,
Gia_ParLlb_t * pPars )

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

Synopsis [Finds balanced cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 840 of file llb3Nonlin.c.

841{
842 Llb_Mnn_t * pMnn;
843 Aig_Man_t * p;
844 int RetValue = -1;
845
846 p = Aig_ManDupFlopsOnly( pAig );
847//Aig_ManShow( p, 0, NULL );
848 if ( pPars->fVerbose )
849 Aig_ManPrintStats( pAig );
850 if ( pPars->fVerbose )
851 Aig_ManPrintStats( p );
852
853 if ( !pPars->fSkipReach )
854 {
855 abctime clk = Abc_Clock();
856 pMnn = Llb_MnnStart( pAig, p, pPars );
857 RetValue = Llb_NonlinReachability( pMnn );
858 pMnn->timeTotal = Abc_Clock() - clk;
859 Llb_MnnStop( pMnn );
860 }
861
862 Aig_ManStop( p );
863 return RetValue;
864}
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_ManDupFlopsOnly
Aig_Man_t * Aig_ManDupFlopsOnly(Aig_Man_t *p)
Definition aigDup.c:871
Llb_NonlinReachability
int Llb_NonlinReachability(Llb_Mnn_t *p)
Definition llb3Nonlin.c:429
Llb_MnnStop
void Llb_MnnStop(Llb_Mnn_t *p)
Definition llb3Nonlin.c:746
Llb_MnnStart
Llb_Mnn_t * Llb_MnnStart(Aig_Man_t *pInit, Aig_Man_t *pAig, Gia_ParLlb_t *pPars)
Definition llb3Nonlin.c:698
Here is the call graph for this function:

◆ Llb_NonlinDeriveCex()

Abc_Cex_t * Llb_NonlinDeriveCex ( Llb_Mnn_t * p)

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

Synopsis [Derives counter-example by backward reachability.]

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file llb3Nonlin.c.

247{
248 Abc_Cex_t * pCex;
249 Aig_Obj_t * pObj;
250 Vec_Int_t * vVarsNs;
251 DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
252 int i, v, RetValue, nPiOffset;
253 char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
254 assert( Vec_PtrSize(p->vRings) > 0 );
255
256 p->dd->TimeStop = 0;
257 p->ddR->TimeStop = 0;
258
259 // update quantifiable vars
260 memset( p->pVars2Q, 0, sizeof(int) * Cudd_ReadSize(p->dd) );
261 vVarsNs = Vec_IntAlloc( Aig_ManRegNum(p->pAig) );
262 Saig_ManForEachLi( p->pAig, pObj, i )
263 {
264 p->pVars2Q[Aig_ObjId(pObj)] = 1;
265 Vec_IntPush( vVarsNs, Aig_ObjId(pObj) );
266 }
267/*
268 Saig_ManForEachLo( p->pAig, pObj, i )
269 printf( "%d ", pObj->Id );
270 printf( "\n" );
271 Saig_ManForEachLi( p->pAig, pObj, i )
272 printf( "%d(%d) ", pObj->Id, Aig_ObjFaninId0(pObj) );
273 printf( "\n" );
274*/
275 // allocate room for the counter-example
276 pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
277 pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
278 pCex->iPo = -1;
279
280 // get the last cube
281 bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
282 RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
283 Cudd_RecursiveDeref( p->ddR, bOneCube );
284 assert( RetValue );
285
286 // write PIs of counter-example
287 nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
288 Saig_ManForEachPi( p->pAig, pObj, i )
289 if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
290 Abc_InfoSetBit( pCex->pData, nPiOffset + i );
291
292 // write state in terms of NS variables
293 if ( Vec_PtrSize(p->vRings) > 1 )
294 {
295 bState = Llb_CoreComputeCube( p->dd, vVarsNs, 1, pValues ); Cudd_Ref( bState );
296 }
297 // perform backward analysis
298 Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
299 {
300 if ( v == Vec_PtrSize(p->vRings) - 1 )
301 continue;
302//Extra_bddPrintSupport( p->dd, bState ); printf( "\n" );
303//Extra_bddPrintSupport( p->dd, bRing ); printf( "\n" );
304 // compute the next states
305 bImage = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bState,
306 p->pPars->fReorder, p->pPars->fVeryVerbose, NULL ); // consumed reference
307 assert( bImage != NULL );
308 Cudd_Ref( bImage );
309//Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
310
311 // move reached states into ring manager
312 bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
313 Cudd_RecursiveDeref( p->dd, bTemp );
314
315 // intersect with the previous set
316 bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
317 Cudd_RecursiveDeref( p->ddR, bImage );
318
319 // find any assignment of the BDD
320 RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
321 Cudd_RecursiveDeref( p->ddR, bOneCube );
322 assert( RetValue );
323
324 // write PIs of counter-example
325 nPiOffset -= Saig_ManPiNum(p->pAig);
326 Saig_ManForEachPi( p->pAig, pObj, i )
327 if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
328 Abc_InfoSetBit( pCex->pData, nPiOffset + i );
329
330 // check that we get the init state
331 if ( v == 0 )
332 {
333 Saig_ManForEachLo( p->pAig, pObj, i )
334 assert( pValues[i] == 0 );
335 break;
336 }
337
338 // write state in terms of NS variables
339 bState = Llb_CoreComputeCube( p->dd, vVarsNs, 1, pValues ); Cudd_Ref( bState );
340 }
341 assert( nPiOffset == Saig_ManRegNum(p->pAig) );
342 // update the output number
343//Abc_CexPrint( pCex );
344 RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
345 assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
346 pCex->iPo = RetValue;
347 // cleanup
348 ABC_FREE( pValues );
349 Vec_IntFree( vVarsNs );
350 return pCex;
351}
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
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_NonlinImage
DdNode * Llb_NonlinImage(Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, DdManager *dd, DdNode *bCurrent, int fReorder, int fVerbose, int *pOrder)
Definition llb3Image.c:884
Saig_ManFindFailedPoCex
int Saig_ManFindFailedPoCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition saigDup.c:436
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
memset
char * memset()
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition vecPtr.h:63
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_NonlinExperiment()

void Llb_NonlinExperiment ( Aig_Man_t * pAig,
int Num )

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

Synopsis [Finds balanced cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 806 of file llb3Nonlin.c.

807{
808 Llb_Mnn_t * pMnn;
809 Gia_ParLlb_t Pars, * pPars = &Pars;
810 Aig_Man_t * p;
811 abctime clk = Abc_Clock();
812
813 Llb_ManSetDefaultParams( pPars );
814 pPars->fVerbose = 1;
815
816 p = Aig_ManDupFlopsOnly( pAig );
817//Aig_ManShow( p, 0, NULL );
818 Aig_ManPrintStats( pAig );
819 Aig_ManPrintStats( p );
820
821 pMnn = Llb_MnnStart( pAig, p, pPars );
822 Llb_NonlinReachability( pMnn );
823 pMnn->timeTotal = Abc_Clock() - clk;
824 Llb_MnnStop( pMnn );
825
826 Aig_ManStop( p );
827}
Llb_ManSetDefaultParams
void Llb_ManSetDefaultParams(Gia_ParLlb_t *pPars)
MACRO DEFINITIONS ///.
Definition llb1Core.c:46
Gia_ParLlb_t
typedefABC_NAMESPACE_HEADER_START struct Gia_ParLlb_t_ Gia_ParLlb_t
INCLUDES ///.
Definition llb.h:41
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_NonlinFindBestVar()

int Llb_NonlinFindBestVar ( DdManager * dd,
DdNode * bFunc,
Aig_Man_t * pAig )

FUNCTION DEFINITIONS ///.

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

Synopsis [Finds variable whose 0-cofactor is the smallest.]

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file llb3Nonlin.c.

87{
88 int fVerbose = 0;
89 Aig_Obj_t * pObj;
90 DdNode * bCof, * bVar;
91 int i, iVar, iVarBest = -1, iValue, iValueBest = ABC_INFINITY, Size0Best = -1;
92 int Size, Size0, Size1;
93 abctime clk = Abc_Clock();
94 Size = Cudd_DagSize(bFunc);
95// printf( "Original = %6d. SuppSize = %3d. Vars = %3d.\n",
96// Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Aig_ManRegNum(pAig) );
97 Saig_ManForEachLo( pAig, pObj, i )
98 {
99 iVar = Aig_ObjId(pObj);
100
101if ( fVerbose )
102printf( "Var =%3d : ", iVar );
103 bVar = Cudd_bddIthVar(dd, iVar);
104
105 bCof = Cudd_bddAnd( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof );
106 Size0 = Cudd_DagSize(bCof);
107if ( fVerbose )
108printf( "Supp0 =%3d ", Cudd_SupportSize(dd, bCof) );
109if ( fVerbose )
110printf( "Size0 =%6d ", Size0 );
111 Cudd_RecursiveDeref( dd, bCof );
112
113 bCof = Cudd_bddAnd( dd, bFunc, bVar ); Cudd_Ref( bCof );
114 Size1 = Cudd_DagSize(bCof);
115if ( fVerbose )
116printf( "Supp1 =%3d ", Cudd_SupportSize(dd, bCof) );
117if ( fVerbose )
118printf( "Size1 =%6d ", Size1 );
119 Cudd_RecursiveDeref( dd, bCof );
120
121 iValue = Abc_MaxInt(Size0, Size1) - Abc_MinInt(Size0, Size1) + Size0 + Size1 - Size;
122if ( fVerbose )
123printf( "D =%6d ", Size0 + Size1 - Size );
124if ( fVerbose )
125printf( "B =%6d ", Abc_MaxInt(Size0, Size1) - Abc_MinInt(Size0, Size1) );
126if ( fVerbose )
127printf( "S =%6d\n", iValue );
128 if ( Size0 > 1 && Size1 > 1 && iValueBest > iValue )
129 {
130 iValueBest = iValue;
131 iVarBest = i;
132 Size0Best = Size0;
133 }
134 }
135 printf( "BestVar = %4d/%4d. Value =%6d. Orig =%6d. Size0 =%6d. ",
136 iVarBest, Aig_ObjId(Saig_ManLo(pAig,iVarBest)), iValueBest, Size, Size0Best );
137 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
138 return iVarBest;
139}
ABC_INFINITY
#define ABC_INFINITY
MACRO DEFINITIONS ///.
Definition abc_global.h:250

◆ Llb_NonlinPrepareVarMap()

void Llb_NonlinPrepareVarMap ( Llb_Mnn_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file llb3Nonlin.c.

176{
177 Aig_Obj_t * pObjLi, * pObjLo, * pObj;
178 int i, iVarLi, iVarLo;
179 p->vCs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
180 p->vNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
181 p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
182 p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
183 Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
184 {
185 iVarLi = Aig_ObjId(pObjLi);
186 iVarLo = Aig_ObjId(pObjLo);
187 assert( iVarLi >= 0 && iVarLi < Aig_ManObjNumMax(p->pAig) );
188 assert( iVarLo >= 0 && iVarLo < Aig_ManObjNumMax(p->pAig) );
189 Vec_IntWriteEntry( p->vCs2Glo, iVarLo, i );
190 Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
191 Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
192 Vec_IntWriteEntry( p->vGlo2Ns, i, iVarLi );
193 }
194 // add mapping of the PIs
195 Saig_ManForEachPi( p->pAig, pObj, i )
196 {
197 Vec_IntWriteEntry( p->vCs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
198 Vec_IntWriteEntry( p->vNs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
199 }
200}
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition saig.h:101
Here is the caller graph for this function:

◆ Llb_NonlinReachability()

int Llb_NonlinReachability ( Llb_Mnn_t * p)

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

Synopsis [Perform reachability with hints.]

Description []

SideEffects []

SeeAlso []

Definition at line 429 of file llb3Nonlin.c.

430{
431 DdNode * bTemp, * bNext;
432 int nIters, nBddSize0, nBddSize = -1, NumCmp;//, Limit = p->pPars->nBddMax;
433 abctime clk2, clk3, clk = Abc_Clock();
434 assert( Aig_ManRegNum(p->pAig) > 0 );
435
436 // compute time to stop
437 p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
438
439 // set the stop time parameter
440 p->dd->TimeStop = p->pPars->TimeTarget;
441 p->ddG->TimeStop = p->pPars->TimeTarget;
442 p->ddR->TimeStop = p->pPars->TimeTarget;
443
444 // set reordering hooks
445 assert( p->dd->bFunc == NULL );
446// p->dd->bFunc = (DdNode *)p->pAig;
447// Cudd_AddHook( p->dd, Llb_NonlinReoHook, CUDD_POST_REORDERING_HOOK );
448
449 // create bad state in the ring manager
450 p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );
451 if ( p->ddR->bFunc == NULL )
452 {
453 if ( !p->pPars->fSilent )
454 printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
455 p->pPars->iFrame = -1;
456 return -1;
457 }
458 Cudd_Ref( p->ddR->bFunc );
459 // compute the starting set of states
460 Cudd_Quit( p->dd );
461 p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 1, p->pPars->TimeTarget );
462 if ( p->dd == NULL )
463 {
464 if ( !p->pPars->fSilent )
465 printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
466 p->pPars->iFrame = -1;
467 return -1;
468 }
469 p->dd->bFunc = Llb_NonlinComputeInitState( p->pAig, p->dd ); Cudd_Ref( p->dd->bFunc ); // current
470 p->ddG->bFunc = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc ); // reached
471 p->ddG->bFunc2 = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc2 ); // frontier
472 for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
473 {
474 // check the runtime limit
475 clk2 = Abc_Clock();
476 if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
477 {
478 if ( !p->pPars->fSilent )
479 printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
480 p->pPars->iFrame = nIters - 1;
481 Llb_NonlinImageQuit();
482 return -1;
483 }
484
485 // save the onion ring
486 bTemp = Extra_TransferPermute( p->dd, p->ddR, p->dd->bFunc, Vec_IntArray(p->vCs2Glo) );
487 if ( bTemp == NULL )
488 {
489 if ( !p->pPars->fSilent )
490 printf( "Reached timeout (%d seconds) during ring transfer.\n", p->pPars->TimeLimit );
491 p->pPars->iFrame = nIters - 1;
492 Llb_NonlinImageQuit();
493 return -1;
494 }
495 Cudd_Ref( bTemp );
496 Vec_PtrPush( p->vRings, bTemp );
497
498 // check it for bad states
499 if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
500 {
501 assert( p->pInit->pSeqModel == NULL );
502 if ( !p->pPars->fBackward )
503 p->pInit->pSeqModel = Llb_NonlinDeriveCex( p );
504 if ( !p->pPars->fSilent )
505 {
506 if ( !p->pPars->fBackward )
507 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, nIters );
508 else
509 Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
510 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
511 }
512 p->pPars->iFrame = nIters - 1;
513 Llb_NonlinImageQuit();
514 return 0;
515 }
516
517 // compute the next states
518 clk3 = Abc_Clock();
519 nBddSize0 = Cudd_DagSize( p->dd->bFunc );
520 bNext = Llb_NonlinImageCompute( p->dd->bFunc, p->pPars->fReorder, 0, 1, p->pOrderL ); // consumes ref
521// bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent,
522// p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, p->pPars->TimeTarget );
523 if ( bNext == NULL )
524 {
525 if ( !p->pPars->fSilent )
526 printf( "Reached timeout (%d seconds) during image computation in quantification.\n", p->pPars->TimeLimit );
527 p->pPars->iFrame = nIters - 1;
528 Llb_NonlinImageQuit();
529 return -1;
530 }
531 Cudd_Ref( bNext );
532 nBddSize = Cudd_DagSize( bNext );
533 p->timeImage += Abc_Clock() - clk3;
534
535
536 // transfer to the state manager
537 clk3 = Abc_Clock();
538 Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
539 p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) );
540// p->ddG->bFunc2 = Extra_bddAndPermute( p->ddG, Cudd_Not(p->ddG->bFunc), p->dd, bNext, Vec_IntArray(p->vNs2Glo) );
541 if ( p->ddG->bFunc2 == NULL )
542 {
543 if ( !p->pPars->fSilent )
544 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
545 p->pPars->iFrame = nIters - 1;
546 Cudd_RecursiveDeref( p->dd, bNext );
547 Llb_NonlinImageQuit();
548 return -1;
549 }
550 Cudd_Ref( p->ddG->bFunc2 );
551 Cudd_RecursiveDeref( p->dd, bNext );
552 p->timeTran1 += Abc_Clock() - clk3;
553
554 // save permutation
555 NumCmp = Llb_NonlinCompPerms( p->dd, p->pOrderL2 );
556 // save order before image computation
557 memcpy( p->pOrderL2, p->dd->perm, sizeof(int) * p->dd->size );
558 // update the image computation manager
559 p->timeReo += Cudd_ReadReorderingTime(p->dd);
560 p->ddLocReos += Cudd_ReadReorderings(p->dd);
561 p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd);
562 Llb_NonlinImageQuit();
563 p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0, p->pPars->TimeTarget );
564 if ( p->dd == NULL )
565 {
566 if ( !p->pPars->fSilent )
567 printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
568 p->pPars->iFrame = nIters - 1;
569 return -1;
570 }
571 //Extra_TestAndPerm( p->ddG, Cudd_Not(p->ddG->bFunc), p->ddG->bFunc2 );
572
573 // derive new states
574 clk3 = Abc_Clock();
575 p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) );
576 if ( p->ddG->bFunc2 == NULL )
577 {
578 if ( !p->pPars->fSilent )
579 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
580 p->pPars->iFrame = nIters - 1;
581 Cudd_RecursiveDeref( p->ddG, bTemp );
582 Llb_NonlinImageQuit();
583 return -1;
584 }
585 Cudd_Ref( p->ddG->bFunc2 );
586 Cudd_RecursiveDeref( p->ddG, bTemp );
587 p->timeGloba += Abc_Clock() - clk3;
588
589 if ( Cudd_IsConstant(p->ddG->bFunc2) )
590 break;
591 // add to the reached set
592 clk3 = Abc_Clock();
593 p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 );
594 if ( p->ddG->bFunc == NULL )
595 {
596 if ( !p->pPars->fSilent )
597 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
598 p->pPars->iFrame = nIters - 1;
599 Cudd_RecursiveDeref( p->ddG, bTemp );
600 Llb_NonlinImageQuit();
601 return -1;
602 }
603 Cudd_Ref( p->ddG->bFunc );
604 Cudd_RecursiveDeref( p->ddG, bTemp );
605 p->timeGloba += Abc_Clock() - clk3;
606
607 // reset permutation
608// RetValue = Cudd_CheckZeroRef( dd );
609// assert( RetValue == 0 );
610// Cudd_ShuffleHeap( dd, pOrderG );
611
612 // move new states to the working manager
613 clk3 = Abc_Clock();
614 p->dd->bFunc = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) );
615 if ( p->dd->bFunc == NULL )
616 {
617 if ( !p->pPars->fSilent )
618 printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
619 p->pPars->iFrame = nIters - 1;
620 Llb_NonlinImageQuit();
621 return -1;
622 }
623 Cudd_Ref( p->dd->bFunc );
624 p->timeTran2 += Abc_Clock() - clk3;
625
626 // report the results
627 if ( p->pPars->fVerbose )
628 {
629 printf( "I =%3d : ", nIters );
630 printf( "Fr =%7d ", nBddSize0 );
631 printf( "Im =%7d ", nBddSize );
632 printf( "(%4d %4d) ", p->ddLocReos, p->ddLocGrbs );
633 printf( "Rea =%6d ", Cudd_DagSize(p->ddG->bFunc) );
634 printf( "(%4d %4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
635 printf( "S =%4d ", nSuppMax );
636 printf( "cL =%5d ", NumCmp );
637 printf( "cG =%5d ", Llb_NonlinCompPerms( p->ddG, p->pOrderG ) );
638 Abc_PrintTime( 1, "T", Abc_Clock() - clk2 );
639 memcpy( p->pOrderG, p->ddG->perm, sizeof(int) * p->ddG->size );
640 }
641/*
642 if ( pPars->fVerbose )
643 {
644 double nMints = Cudd_CountMinterm(ddG, bReached, Saig_ManRegNum(pAig) );
645// Extra_bddPrint( ddG, bReached );printf( "\n" );
646 printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(pAig)) );
647 fflush( stdout );
648 }
649*/
650 if ( nIters == p->pPars->nIterMax - 1 )
651 {
652 if ( !p->pPars->fSilent )
653 printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax );
654 p->pPars->iFrame = nIters;
655 Llb_NonlinImageQuit();
656 return -1;
657 }
658 }
659 Llb_NonlinImageQuit();
660
661 // report the stats
662 if ( p->pPars->fVerbose )
663 {
664 double nMints = Cudd_CountMinterm(p->ddG, p->ddG->bFunc, Saig_ManRegNum(p->pAig) );
665 if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
666 printf( "Reachability analysis is stopped after %d frames.\n", nIters );
667 else
668 printf( "Reachability analysis completed after %d frames.\n", nIters );
669 printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
670 fflush( stdout );
671 }
672 if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
673 {
674 if ( !p->pPars->fSilent )
675 printf( "Verified only for states reachable in %d frames. ", nIters );
676 p->pPars->iFrame = p->pPars->nIterMax;
677 return -1; // undecided
678 }
679 // report
680 if ( !p->pPars->fSilent )
681 printf( "The miter is proved unreachable after %d iterations. ", nIters );
682 p->pPars->iFrame = nIters - 1;
683 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
684 return 1; // unreachable
685}
Llb_BddComputeBad
ABC_NAMESPACE_IMPL_START DdNode * Llb_BddComputeBad(Aig_Man_t *pInit, DdManager *dd, abctime TimeOut)
DECLARATIONS ///.
Definition llb2Bad.c:45
Llb_NonlinImageQuit
void Llb_NonlinImageQuit()
Definition llb3Image.c:1075
Llb_NonlinImageCompute
DdNode * Llb_NonlinImageCompute(DdNode *bCurrent, int fReorder, int fDrop, int fVerbose, int *pOrder)
Definition llb3Image.c:999
Llb_NonlinImageStart
DdManager * Llb_NonlinImageStart(Aig_Man_t *pAig, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vRoots, int *pVars2Q, int *pOrder, int fFirst, abctime TimeTarget)
Definition llb3Image.c:963
nSuppMax
int nSuppMax
Definition llb3Image.c:83
Llb_NonlinCompPerms
int Llb_NonlinCompPerms(DdManager *dd, int *pVar2Lev)
Definition llb3Nonlin.c:402
Llb_NonlinDeriveCex
Abc_Cex_t * Llb_NonlinDeriveCex(Llb_Mnn_t *p)
Definition llb3Nonlin.c:246
Llb_NonlinComputeInitState
DdNode * Llb_NonlinComputeInitState(Aig_Man_t *pAig, DdManager *dd)
Definition llb3Nonlin.c:214
memcpy
char * memcpy()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Llb_NonlinReoHook()

int Llb_NonlinReoHook ( DdManager * dd,
char * Type,
void * Method )

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

Synopsis [Perform reachability with hints.]

Description []

SideEffects []

SeeAlso []

Definition at line 365 of file llb3Nonlin.c.

366{
367 Aig_Man_t * pAig = (Aig_Man_t *)dd->bFunc;
368 Aig_Obj_t * pObj;
369 int i;
370 printf( "Order: " );
371 for ( i = 0; i < Cudd_ReadSize(dd); i++ )
372 {
373 pObj = Aig_ManObj( pAig, i );
374 if ( pObj == NULL )
375 continue;
376 if ( Saig_ObjIsPi(pAig, pObj) )
377 printf( "pi" );
378 else if ( Saig_ObjIsLo(pAig, pObj) )
379 printf( "lo" );
380 else if ( Saig_ObjIsPo(pAig, pObj) )
381 printf( "po" );
382 else if ( Saig_ObjIsLi(pAig, pObj) )
383 printf( "li" );
384 else continue;
385 printf( "%d=%d ", i, dd->perm[i] );
386 }
387 printf( "\n" );
388 return 1;
389}

◆ Llb_NonlinTrySubsetting()

void Llb_NonlinTrySubsetting ( DdManager * dd,
DdNode * bFunc )

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

Synopsis [Finds variable whose 0-cofactor is the smallest.]

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file llb3Nonlin.c.

154{
155 DdNode * bNew;
156 printf( "Original = %6d. SuppSize = %3d. ",
157 Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc) );
158 bNew = Cudd_SubsetHeavyBranch( dd, bFunc, Cudd_SupportSize(dd, bFunc), 1000 ); Cudd_Ref( bNew );
159 printf( "Result = %6d. SuppSize = %3d.\n",
160 Cudd_DagSize(bNew), Cudd_SupportSize(dd, bNew) );
161 Cudd_RecursiveDeref( dd, bNew );
162}

Variable Documentation

◆ nSuppMax

int nSuppMax
extern

Definition at line 83 of file llb3Image.c.

◆ timeAndEx

abctime timeAndEx

Definition at line 68 of file llb3Nonlin.c.

◆ timeBuild

abctime timeBuild
extern

Definition at line 82 of file llb3Image.c.

◆ timeOther

abctime timeOther

Definition at line 68 of file llb3Nonlin.c.