From 6e74c46bcfbf48029d17835754fd570f283fb9d8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 13 Apr 2011 22:41:54 -0700 Subject: Enabled new BDD-based reachability engine 'reachy'. --- src/aig/aig/aigDoms.c | 66 +++- src/aig/aig/aigPack.c | 6 +- src/aig/gia/gia.h | 4 + src/aig/llb/llb4Image.c | 770 ++++++++++++++++++++++++++++++++++++++ src/aig/llb/llb4Map.c | 123 ++++++ src/aig/llb/llb4Nonlin.c | 914 +++++++++++++++++++++++++++++++++++++++++++++ src/aig/llb/llbInt.h | 10 +- src/aig/llb/module.make | 4 +- src/base/abci/abc.c | 139 +++++++ src/base/abci/abcIf.c | 2 +- src/bdd/cudd/cuddCompose.c | 3 + src/misc/vec/vecVec.h | 4 + 12 files changed, 2036 insertions(+), 9 deletions(-) create mode 100644 src/aig/llb/llb4Image.c create mode 100644 src/aig/llb/llb4Map.c create mode 100644 src/aig/llb/llb4Nonlin.c (limited to 'src') diff --git a/src/aig/aig/aigDoms.c b/src/aig/aig/aigDoms.c index e909ac41..0ac2b358 100644 --- a/src/aig/aig/aigDoms.c +++ b/src/aig/aig/aigDoms.c @@ -207,9 +207,9 @@ void Aig_ManDomPrint( Aig_Sto_t * pSto ) { Aig_Obj_t * pObj; int i; - Saig_ManForEachLo( pSto->pAig, pObj, i ) + Saig_ManForEachPi( pSto->pAig, pObj, i ) { - printf( "*** LO %4d %4d :\n", i, pObj->Id ); + printf( "*** PI %4d %4d :\n", i, pObj->Id ); Aig_ObjDomVecPrint( pSto, (Vec_Ptr_t *)Vec_PtrEntry(pSto->vDoms, pObj->Id) ); } } @@ -647,6 +647,45 @@ Aig_Sto_t * Aig_ManComputeDomsFlops( Aig_Man_t * pAig, int Limit ) return pSto; } +/**Function************************************************************* + + Synopsis [Computes multi-node dominators.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Sto_t * Aig_ManComputeDomsPis( Aig_Man_t * pAig, int Limit ) +{ + Aig_Sto_t * pSto; + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i, clk = clock(); + pSto = Aig_ManDomStart( pAig, Limit ); + // initialize flop inputs + Aig_ManForEachPo( pAig, pObj, i ) + Aig_ObjAddTriv( pSto, pObj->Id, Vec_PtrAlloc(1) ); + // compute internal nodes + vNodes = Aig_ManDfsReverse( pAig ); + Aig_ManMarkFlopTfi( pAig ); + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + if ( Aig_ObjIsTravIdCurrent(pSto->pAig, pObj) ) + Aig_ObjDomCompute( pSto, pObj ); + Vec_PtrFree( vNodes ); + // compute combinational inputs + Saig_ManForEachPi( pAig, pObj, i ) + Aig_ObjDomCompute( pSto, pObj ); + // print statistics + printf( "Nodes =%4d. PIs =%4d. Doms =%9d. Ave =%8.2f. ", + pSto->nDomNodes, Saig_ManPiNum(pSto->pAig), pSto->nDomsTotal, +// pSto->nDomsFilter1, pSto->nDomsFilter2, + 1.0 * pSto->nDomsTotal / (pSto->nDomNodes + Saig_ManPiNum(pSto->pAig)) ); + Abc_PrintTime( 1, "Time", clock() - clk ); + return pSto; +} /**Function************************************************************* @@ -971,7 +1010,7 @@ void Aig_ObjDomFindGood( Aig_Sto_t * pSto ) SeeAlso [] ***********************************************************************/ -void Aig_ManComputeDomsTest( Aig_Man_t * pAig, int Num ) +void Aig_ManComputeDomsTest2( Aig_Man_t * pAig, int Num ) { Aig_Sto_t * pSto; // int i; @@ -988,6 +1027,27 @@ void Aig_ManComputeDomsTest( Aig_Man_t * pAig, int Num ) Aig_ManFanoutStop( pAig ); } +/**Function************************************************************* + + Synopsis [Computes multi-node dominators.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManComputeDomsTest( Aig_Man_t * pAig ) +{ + Aig_Sto_t * pSto; + Aig_ManFanoutStart( pAig ); + pSto = Aig_ManComputeDomsPis( pAig, 1 ); + Aig_ManDomPrint( pSto ); + Aig_ManDomStop( pSto ); + Aig_ManFanoutStop( pAig ); +} + diff --git a/src/aig/aig/aigPack.c b/src/aig/aig/aigPack.c index 493e4995..0ecbf533 100644 --- a/src/aig/aig/aigPack.c +++ b/src/aig/aig/aigPack.c @@ -113,10 +113,10 @@ void Aig_ManPackPrintCare( Aig_ManPack_t * p ) Aig_ManForEachPi( p->pAig, pObj, i ) { Sign = Vec_WrdEntry( p->vPiCare, i ); - Extra_PrintBinary( stdout, (unsigned *)&Sign, 64 ); - printf( "\n" ); +// Extra_PrintBinary( stdout, (unsigned *)&Sign, 64 ); +// printf( "\n" ); } - printf( "\n" ); +// printf( "\n" ); } diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 4059153d..16259a1e 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -316,6 +316,10 @@ static inline void Gia_ObjSetValue( Gia_Obj_t * pObj, int i ) { static inline int Gia_ObjPhase( Gia_Obj_t * pObj ) { return pObj->fPhase; } static inline int Gia_ObjPhaseReal( Gia_Obj_t * pObj ) { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj); } +static inline int Gia_ManIdToCioId( Gia_Man_t * p, int Id ) { return Gia_ObjCioId( Gia_ManObj(p, Id) ); } +static inline int Gia_ManCiIdToId( Gia_Man_t * p, int CiId ) { return Gia_ObjId( p, Gia_ManCi(p, CiId) ); } +static inline int Gia_ManCoIdToId( Gia_Man_t * p, int CoId ) { return Gia_ObjId( p, Gia_ManCo(p, CoId) ); } + static inline int Gia_ObjIsPi( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) < Gia_ManPiNum(p); } static inline int Gia_ObjIsPo( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCo(pObj) && Gia_ObjCioId(pObj) < Gia_ManPoNum(p); } static inline int Gia_ObjIsRo( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) >= Gia_ManPiNum(p); } diff --git a/src/aig/llb/llb4Image.c b/src/aig/llb/llb4Image.c new file mode 100644 index 00000000..b882ac65 --- /dev/null +++ b/src/aig/llb/llb4Image.c @@ -0,0 +1,770 @@ +/**CFile**************************************************************** + + FileName [llb3Image.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD based reachability.] + + Synopsis [Computes image using partitioned structure.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: llb3Image.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Llb_Var_t_ Llb_Var_t; +struct Llb_Var_t_ +{ + int iVar; // variable number + int nScore; // variable score + Vec_Int_t * vParts; // partitions +}; + +typedef struct Llb_Prt_t_ Llb_Prt_t; +struct Llb_Prt_t_ +{ + int iPart; // partition number + int nSize; // the number of BDD nodes + DdNode * bFunc; // the partition + Vec_Int_t * vVars; // support +}; + +typedef struct Llb_Mgr_t_ Llb_Mgr_t; +struct Llb_Mgr_t_ +{ + DdManager * dd; // working BDD manager + Vec_Int_t * vVars2Q; // variables to quantify + // internal + Llb_Prt_t ** pParts; // partitions + Llb_Var_t ** pVars; // variables + int iPartFree; // next free partition + int nVars; // the number of BDD variables + int nSuppMax; // maximum support size + // temporary + int * pSupp; // temporary support storage +}; + +static inline Llb_Var_t * Llb_MgrVar( Llb_Mgr_t * p, int i ) { return p->pVars[i]; } +static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i ) { return p->pParts[i]; } + +// iterator over vars +#define Llb_MgrForEachVar( p, pVar, i ) \ + for ( i = 0; (i < p->nVars) && (((pVar) = Llb_MgrVar(p, i)), 1); i++ ) if ( pVar == NULL ) {} else +// iterator over parts +#define Llb_MgrForEachPart( p, pPart, i ) \ + for ( i = 0; (i < p->iPartFree) && (((pPart) = Llb_MgrPart(p, i)), 1); i++ ) if ( pPart == NULL ) {} else + +// iterator over vars of one partition +#define Llb_PartForEachVar( p, pPart, pVar, i ) \ + for ( i = 0; (i < Vec_IntSize(pPart->vVars)) && (((pVar) = Llb_MgrVar(p, Vec_IntEntry(pPart->vVars,i))), 1); i++ ) +// iterator over parts of one variable +#define Llb_VarForEachPart( p, pVar, pPart, i ) \ + for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ ) + +// statistics +//int timeBuild, timeAndEx, timeOther; +//int nSuppMax; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Removes one variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4RemoveVar( Llb_Mgr_t * p, Llb_Var_t * pVar ) +{ + assert( p->pVars[pVar->iVar] == pVar ); + p->pVars[pVar->iVar] = NULL; + Vec_IntFree( pVar->vParts ); + ABC_FREE( pVar ); +} + +/**Function************************************************************* + + Synopsis [Removes one partition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4RemovePart( Llb_Mgr_t * p, Llb_Prt_t * pPart ) +{ + assert( p->pParts[pPart->iPart] == pPart ); + p->pParts[pPart->iPart] = NULL; + Vec_IntFree( pPart->vVars ); + Cudd_RecursiveDeref( p->dd, pPart->bFunc ); + ABC_FREE( pPart ); +} + +/**Function************************************************************* + + Synopsis [Create cube with singleton variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_Nonlin4CreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart ) +{ + DdNode * bCube, * bTemp; + Llb_Var_t * pVar; + int i, TimeStop; + TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; + bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); + Llb_PartForEachVar( p, pPart, pVar, i ) + { + assert( Vec_IntSize(pVar->vParts) > 0 ); + if ( Vec_IntSize(pVar->vParts) != 1 ) + continue; + assert( Vec_IntEntry(pVar->vParts, 0) == pPart->iPart ); + bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + Cudd_Deref( bCube ); + p->dd->TimeStop = TimeStop; + return bCube; +} + +/**Function************************************************************* + + Synopsis [Create cube of variables appearing only in two partitions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_Nonlin4CreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 ) +{ + DdNode * bCube, * bTemp; + Llb_Var_t * pVar; + int i, TimeStop; + TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; + bCube = Cudd_ReadOne(p->dd); Cudd_Ref( bCube ); + Llb_PartForEachVar( p, pPart1, pVar, i ) + { + assert( Vec_IntSize(pVar->vParts) > 0 ); + if ( Vec_IntSize(pVar->vParts) != 2 ) + continue; + if ( (Vec_IntEntry(pVar->vParts, 0) == pPart1->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart2->iPart) || + (Vec_IntEntry(pVar->vParts, 0) == pPart2->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart1->iPart) ) + { + bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) ); Cudd_Ref( bCube ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } + } + Cudd_Deref( bCube ); + p->dd->TimeStop = TimeStop; + return bCube; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if partition has singleton variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_Nonlin4HasSingletonVars( Llb_Mgr_t * p, Llb_Prt_t * pPart ) +{ + Llb_Var_t * pVar; + int i; + Llb_PartForEachVar( p, pPart, pVar, i ) + if ( Vec_IntSize(pVar->vParts) == 1 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if partition has singleton variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4Print( Llb_Mgr_t * p ) +{ + Llb_Prt_t * pPart; + Llb_Var_t * pVar; + int i, k; + printf( "\n" ); + Llb_MgrForEachVar( p, pVar, i ) + { + printf( "Var %3d : ", i ); + Llb_VarForEachPart( p, pVar, pPart, k ) + printf( "%d ", pPart->iPart ); + printf( "\n" ); + } + Llb_MgrForEachPart( p, pPart, i ) + { + printf( "Part %3d : ", i ); + Llb_PartForEachVar( p, pPart, pVar, k ) + printf( "%d ", pVar->iVar ); + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Quantifies singles belonging to one partition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_Nonlin4Quantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart ) +{ + Llb_Var_t * pVar; + Llb_Prt_t * pTemp; + Vec_Ptr_t * vSingles; + DdNode * bCube, * bTemp; + int i, RetValue, nSizeNew; + // create cube to be quantified + bCube = Llb_Nonlin4CreateCube1( p, pPart ); Cudd_Ref( bCube ); + assert( !Cudd_IsConstant(bCube) ); + // derive new function + pPart->bFunc = Cudd_bddExistAbstract( p->dd, bTemp = pPart->bFunc, bCube ); Cudd_Ref( pPart->bFunc ); + Cudd_RecursiveDeref( p->dd, bTemp ); + Cudd_RecursiveDeref( p->dd, bCube ); + // get support + vSingles = Vec_PtrAlloc( 0 ); + nSizeNew = Cudd_DagSize(pPart->bFunc); + Extra_SupportArray( p->dd, pPart->bFunc, p->pSupp ); + Llb_PartForEachVar( p, pPart, pVar, i ) + if ( p->pSupp[pVar->iVar] ) + { + assert( Vec_IntSize(pVar->vParts) > 1 ); + pVar->nScore -= pPart->nSize - nSizeNew; + } + else + { + RetValue = Vec_IntRemove( pVar->vParts, pPart->iPart ); + assert( RetValue ); + pVar->nScore -= pPart->nSize; + if ( Vec_IntSize(pVar->vParts) == 0 ) + Llb_Nonlin4RemoveVar( p, pVar ); + else if ( Vec_IntSize(pVar->vParts) == 1 ) + Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) ); + } + + // update partition + pPart->nSize = nSizeNew; + Vec_IntClear( pPart->vVars ); + for ( i = 0; i < p->nVars; i++ ) + if ( p->pSupp[i] && Vec_IntEntry(p->vVars2Q, i) ) + Vec_IntPush( pPart->vVars, i ); + // remove other variables + Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i ) + Llb_Nonlin4Quantify1( p, pTemp ); + Vec_PtrFree( vSingles ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Quantifies singles belonging to one partition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_Nonlin4Quantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 ) +{ + int fVerbose = 0; + Llb_Var_t * pVar; + Llb_Prt_t * pTemp; + Vec_Ptr_t * vSingles; + DdNode * bCube, * bFunc; + int i, RetValue, nSuppSize; + int iPart1 = pPart1->iPart; + int iPart2 = pPart2->iPart; + + // create cube to be quantified + bCube = Llb_Nonlin4CreateCube2( p, pPart1, pPart2 ); Cudd_Ref( bCube ); +if ( fVerbose ) +{ +printf( "\n" ); +printf( "\n" ); +Llb_Nonlin4Print( p ); +printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart ); +Extra_bddPrintSupport( p->dd, bCube ); printf( "\n" ); +} + bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube ); + if ( bFunc == NULL ) + { + Cudd_RecursiveDeref( p->dd, bCube ); + return 0; + } + Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( p->dd, bCube ); + + // create new partition + pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 ); + pTemp->iPart = p->iPartFree++; + pTemp->nSize = Cudd_DagSize(bFunc); + pTemp->bFunc = bFunc; + pTemp->vVars = Vec_IntAlloc( 8 ); + // update variables + Llb_PartForEachVar( p, pPart1, pVar, i ) + { + RetValue = Vec_IntRemove( pVar->vParts, pPart1->iPart ); + assert( RetValue ); + pVar->nScore -= pPart1->nSize; + } + // update variables + Llb_PartForEachVar( p, pPart2, pVar, i ) + { + RetValue = Vec_IntRemove( pVar->vParts, pPart2->iPart ); + assert( RetValue ); + pVar->nScore -= pPart2->nSize; + } + // add variables to the new partition + nSuppSize = 0; + Extra_SupportArray( p->dd, bFunc, p->pSupp ); + for ( i = 0; i < p->nVars; i++ ) + { + nSuppSize += p->pSupp[i]; + if ( p->pSupp[i] && Vec_IntEntry(p->vVars2Q, i) ) + { + pVar = Llb_MgrVar( p, i ); + pVar->nScore += pTemp->nSize; + Vec_IntPush( pVar->vParts, pTemp->iPart ); + Vec_IntPush( pTemp->vVars, i ); + } + } + p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize ); + // remove variables and collect partitions with singleton variables + vSingles = Vec_PtrAlloc( 0 ); + Llb_PartForEachVar( p, pPart1, pVar, i ) + { + if ( Vec_IntSize(pVar->vParts) == 0 ) + Llb_Nonlin4RemoveVar( p, pVar ); + else if ( Vec_IntSize(pVar->vParts) == 1 ) + { + if ( fVerbose ) + printf( "Adding partition %d because of var %d.\n", + Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar ); + Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) ); + } + } + Llb_PartForEachVar( p, pPart2, pVar, i ) + { + if ( pVar == NULL ) + continue; + if ( Vec_IntSize(pVar->vParts) == 0 ) + Llb_Nonlin4RemoveVar( p, pVar ); + else if ( Vec_IntSize(pVar->vParts) == 1 ) + { + if ( fVerbose ) + printf( "Adding partition %d because of var %d.\n", + Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar ); + Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) ); + } + } + // remove partitions + Llb_Nonlin4RemovePart( p, pPart1 ); + Llb_Nonlin4RemovePart( p, pPart2 ); + // remove other variables +if ( fVerbose ) +Llb_Nonlin4Print( p ); + Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i ) + { +if ( fVerbose ) +printf( "Updating partitiong %d with singlton vars.\n", pTemp->iPart ); + Llb_Nonlin4Quantify1( p, pTemp ); + } +if ( fVerbose ) +Llb_Nonlin4Print( p ); + Vec_PtrFree( vSingles ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes volume of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4CutNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + return; + Aig_ObjSetTravIdCurrent(p, pObj); + if ( Saig_ObjIsLi(p, pObj) ) + { + Llb_Nonlin4CutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes); + return; + } + if ( Aig_ObjIsConst1(pObj) ) + return; + assert( Aig_ObjIsNode(pObj) ); + Llb_Nonlin4CutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes); + Llb_Nonlin4CutNodes_rec(p, Aig_ObjFanin1(pObj), vNodes); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Computes volume of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_Nonlin4CutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper ) +{ + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + // mark the lower cut with the traversal ID + Aig_ManIncrementTravId(p); + Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i ) + Aig_ObjSetTravIdCurrent( p, pObj ); + // count the upper cut + vNodes = Vec_PtrAlloc( 100 ); + Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i ) + Llb_Nonlin4CutNodes_rec( p, pObj, vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Starts non-linear quantification scheduling.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4AddPair( Llb_Mgr_t * p, int iPart, int iVar ) +{ + if ( p->pVars[iVar] == NULL ) + { + p->pVars[iVar] = ABC_CALLOC( Llb_Var_t, 1 ); + p->pVars[iVar]->iVar = iVar; + p->pVars[iVar]->nScore = 0; + p->pVars[iVar]->vParts = Vec_IntAlloc( 8 ); + } + Vec_IntPush( p->pVars[iVar]->vParts, iPart ); + Vec_IntPush( p->pParts[iPart]->vVars, iVar ); +} + +/**Function************************************************************* + + Synopsis [Starts non-linear quantification scheduling.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4AddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc ) +{ + int k, nSuppSize; + assert( !Cudd_IsConstant(bFunc) ); + // create partition + p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 ); + p->pParts[i]->iPart = i; + p->pParts[i]->bFunc = bFunc; Cudd_Ref( bFunc ); + p->pParts[i]->vVars = Vec_IntAlloc( 8 ); + // add support dependencies + nSuppSize = 0; + Extra_SupportArray( p->dd, bFunc, p->pSupp ); + for ( k = 0; k < p->nVars; k++ ) + { + nSuppSize += p->pSupp[k]; + if ( p->pSupp[k] && Vec_IntEntry(p->vVars2Q, k) ) + Llb_Nonlin4AddPair( p, i, k ); + } + p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize ); +} + +/**Function************************************************************* + + Synopsis [Checks that each var appears in at least one partition.] + + Description [] + + SideEffects [] + + SeeAlso [] +**********************************************************************/ +void Llb_Nonlin4CheckVars( Llb_Mgr_t * p ) +{ + Llb_Var_t * pVar; + int i; + Llb_MgrForEachVar( p, pVar, i ) + assert( Vec_IntSize(pVar->vParts) > 1 ); +} + +/**Function************************************************************* + + Synopsis [Find next partition to quantify] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_Nonlin4NextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t ** ppPart2 ) +{ + Llb_Var_t * pVar, * pVarBest = NULL; + Llb_Prt_t * pPart, * pPart1Best = NULL, * pPart2Best = NULL; + int i; + Llb_Nonlin4CheckVars( p ); + // find variable with minimum score + Llb_MgrForEachVar( p, pVar, i ) + if ( pVarBest == NULL || pVarBest->nScore > pVar->nScore ) + pVarBest = pVar; + if ( pVarBest == NULL ) + return 0; + // find two partitions with minimum size + Llb_VarForEachPart( p, pVarBest, pPart, i ) + { + if ( pPart1Best == NULL ) + pPart1Best = pPart; + else if ( pPart2Best == NULL ) + pPart2Best = pPart; + else if ( pPart1Best->nSize > pPart->nSize || pPart2Best->nSize > pPart->nSize ) + { + if ( pPart1Best->nSize > pPart2Best->nSize ) + pPart1Best = pPart; + else + pPart2Best = pPart; + } + } + *ppPart1 = pPart1Best; + *ppPart2 = pPart2Best; + return 1; +} + +/**Function************************************************************* + + Synopsis [Recomputes scores after variable reordering.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4RecomputeScores( Llb_Mgr_t * p ) +{ + Llb_Prt_t * pPart; + Llb_Var_t * pVar; + int i, k; + Llb_MgrForEachPart( p, pPart, i ) + pPart->nSize = Cudd_DagSize(pPart->bFunc); + Llb_MgrForEachVar( p, pVar, i ) + { + pVar->nScore = 0; + Llb_VarForEachPart( p, pVar, pPart, k ) + pVar->nScore += pPart->nSize; + } +} + +/**Function************************************************************* + + Synopsis [Recomputes scores after variable reordering.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4VerifyScores( Llb_Mgr_t * p ) +{ + Llb_Prt_t * pPart; + Llb_Var_t * pVar; + int i, k, nScore; + Llb_MgrForEachPart( p, pPart, i ) + assert( pPart->nSize == Cudd_DagSize(pPart->bFunc) ); + Llb_MgrForEachVar( p, pVar, i ) + { + nScore = 0; + Llb_VarForEachPart( p, pVar, pPart, k ) + nScore += pPart->nSize; + assert( nScore == pVar->nScore ); + } +} + +/**Function************************************************************* + + Synopsis [Starts non-linear quantification scheduling.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q ) +{ + Llb_Mgr_t * p; + DdNode * bFunc; + int i; + p = ABC_CALLOC( Llb_Mgr_t, 1 ); + p->dd = dd; + p->vVars2Q = vVars2Q; + p->nVars = Cudd_ReadSize(dd); + p->iPartFree = Vec_PtrSize(vParts); + p->pVars = ABC_CALLOC( Llb_Var_t *, p->nVars ); + p->pParts = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree + 2 ); + p->pSupp = ABC_ALLOC( int, Cudd_ReadSize(dd) ); + // add pairs (refs are consumed inside) + Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i ) + Llb_Nonlin4AddPartition( p, i, bFunc ); + // add partition + Llb_Nonlin4AddPartition( p, p->iPartFree++, bCurrent ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops non-linear quantification scheduling.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4Free( Llb_Mgr_t * p ) +{ + Llb_Prt_t * pPart; + Llb_Var_t * pVar; + int i; + Llb_MgrForEachVar( p, pVar, i ) + Llb_Nonlin4RemoveVar( p, pVar ); + Llb_MgrForEachPart( p, pPart, i ) + Llb_Nonlin4RemovePart( p, pPart ); + ABC_FREE( p->pVars ); + ABC_FREE( p->pParts ); + ABC_FREE( p->pSupp ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Performs image computation.] + + Description [Computes image of BDDs (vFuncs).] + + SideEffects [BDDs in vFuncs are derefed inside. The result is refed.] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q ) +{ + Llb_Prt_t * pPart, * pPart1, * pPart2; + Llb_Mgr_t * p; + DdNode * bFunc, * bTemp; + int i, nReorders; + // start the manager + p = Llb_Nonlin4Alloc( dd, vParts, bCurrent, vVars2Q ); + // remove singles + Llb_MgrForEachPart( p, pPart, i ) + if ( Llb_Nonlin4HasSingletonVars(p, pPart) ) + Llb_Nonlin4Quantify1( p, pPart ); + // compute scores + Llb_Nonlin4RecomputeScores( p ); + // iteratively quantify variables + while ( Llb_Nonlin4NextPartitions(p, &pPart1, &pPart2) ) + { + nReorders = Cudd_ReadReorderings(dd); + if ( !Llb_Nonlin4Quantify2( p, pPart1, pPart2 ) ) + { + Llb_Nonlin4Free( p ); + return NULL; + } + if ( nReorders < Cudd_ReadReorderings(dd) ) + Llb_Nonlin4RecomputeScores( p ); + else + Llb_Nonlin4VerifyScores( p ); + } + // load partitions + bFunc = Cudd_ReadOne(p->dd); Cudd_Ref( bFunc ); + Llb_MgrForEachPart( p, pPart, i ) + { + bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc ); Cudd_Ref( bFunc ); + Cudd_RecursiveDeref( p->dd, bTemp ); + } +// nSuppMax = p->nSuppMax; + Llb_Nonlin4Free( p ); + // return + Cudd_Deref( bFunc ); + return bFunc; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llb4Map.c b/src/aig/llb/llb4Map.c new file mode 100644 index 00000000..9dabb19d --- /dev/null +++ b/src/aig/llb/llb4Map.c @@ -0,0 +1,123 @@ +/**CFile**************************************************************** + + FileName [llb2Map.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: llb2Map.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "llbInt.h" +#include "abc.h" +#include "if.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns internal nodes used in the mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin ) +{ + extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan ); + extern If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ); + extern void Gia_ManSetIfParsDefault( If_Par_t * pPars ); + If_Par_t Pars, * pPars = &Pars; + If_Man_t * pIfMan; + If_Obj_t * pAnd; + Abc_Ntk_t * pNtk; + Abc_Obj_t * pNode; + Vec_Int_t * vNodes; + Aig_Obj_t * pObj; + int i; + + // create ABC network + pNtk = Abc_NtkFromAigPhase( pAig ); + assert( Abc_NtkIsStrash(pNtk) ); + + // derive mapping parameters + Gia_ManSetIfParsDefault( pPars ); + pPars->nLutSize = nLutSize; + + // get timing information + pPars->pTimesArr = Abc_NtkGetCiArrivalFloats(pNtk); + pPars->pTimesReq = NULL; + + // perform LUT mapping + pIfMan = Abc_NtkToIf( pNtk, pPars ); + if ( pIfMan == NULL ) + { + Abc_NtkDelete( pNtk ); + return NULL; + } + if ( !If_ManPerformMapping( pIfMan ) ) + { + Abc_NtkDelete( pNtk ); + If_ManStop( pIfMan ); + return NULL; + } + + // mark nodes in the AIG used in the mapping + Aig_ManCleanMarkA( pAig ); + Aig_ManForEachNode( pAig, pObj, i ) + { + pNode = (Abc_Obj_t *)pObj->pData; + if ( pNode == NULL ) + continue; + pAnd = (If_Obj_t *)pNode->pCopy; + if ( pAnd == NULL ) + continue; + if ( pAnd->nRefs > 0 && (int)If_ObjCutBest(pAnd)->nLeaves >= nLutMin ) + pObj->fMarkA = 1; + } + Abc_NtkDelete( pNtk ); + If_ManStop( pIfMan ); + + // unmark flop drivers + Saig_ManForEachLi( pAig, pObj, i ) + Aig_ObjFanin0(pObj)->fMarkA = 0; + + // collect mapping + vNodes = Vec_IntAlloc( 100 ); + Aig_ManForEachNode( pAig, pObj, i ) + if ( pObj->fMarkA ) + Vec_IntPush( vNodes, Aig_ObjId(pObj) ); + Aig_ManCleanMarkA( pAig ); + return vNodes; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c new file mode 100644 index 00000000..1a6f538c --- /dev/null +++ b/src/aig/llb/llb4Nonlin.c @@ -0,0 +1,914 @@ +/**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 $] + +***********************************************************************/ + +#include "llbInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Llb_Mnx_t_ Llb_Mnx_t; +struct Llb_Mnx_t_ +{ + // user info + Aig_Man_t * pAig; // AIG manager + Gia_ParLlb_t * pPars; // parameters + + // intermediate BDDs + DdManager * dd; // BDD manager + DdNode * bBad; // bad states in terms of CIs + DdNode * bReached; // reached states + DdNode * bCurrent; // from states + DdNode * bNext; // to states + Vec_Ptr_t * vRings; // onion rings in ddR + Vec_Ptr_t * vRoots; // BDDs for partitions + + // structural info + Vec_Int_t * vOrder; // for each object ID, its BDD variable number or -1 + Vec_Int_t * vVars2Q; // 1 if variable is quantifiable; 0 othervise + + int timeImage; + int timeRemap; + int timeReo; + int timeOther; + int timeTotal; +}; + +static inline int Llb_MnxBddVar( Vec_Int_t * vOrder, Aig_Obj_t * pObj ) { return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); } + +//extern int timeBuild, timeAndEx, timeOther; +//extern int nSuppMax; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes bad in working manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder ) +{ + Vec_Ptr_t * vNodes; + DdNode * bBdd, * bBdd0, * bBdd1, * bTemp, * bResult; + Aig_Obj_t * pObj; + int i; + Aig_ManCleanData( pAig ); + // assign elementary variables + Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) ); + // compute internal nodes + vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vPos), Saig_ManPoNum(pAig) ); + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + { + if ( !Aig_ObjIsNode(pObj) ) + continue; + bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); + bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); + if ( bBdd == NULL ) + { + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + Vec_PtrFree( vNodes ); + return NULL; + } + Cudd_Ref( bBdd ); + pObj->pData = bBdd; + } + // quantify PIs of each PO + bResult = Cudd_ReadLogicZero( dd ); Cudd_Ref( bResult ); + Saig_ManForEachPo( pAig, pObj, i ) + { + bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + bResult = Cudd_bddOr( dd, bTemp = bResult, bBdd0 ); + if ( bResult == NULL ) + { + Cudd_RecursiveDeref( dd, bTemp ); + break; + } + Cudd_Ref( bResult ); + Cudd_RecursiveDeref( dd, bTemp ); + } + // deref + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + Vec_PtrFree( vNodes ); + if ( bResult ) + Cudd_Deref( bResult ); +//if ( bResult ) +//printf( "Bad state = %d.\n", Cudd_DagSize(bResult) ); + return bResult; +} + +/**Function************************************************************* + + Synopsis [Derives BDDs for the partitions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Llb_Nonlin4DerivePartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder ) +{ + Vec_Ptr_t * vRoots; + Aig_Obj_t * pObj; + DdNode * bBdd, * bBdd0, * bBdd1, * bPart; + int i; + Aig_ManCleanData( pAig ); + // assign elementary variables + Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) ); + Aig_ManForEachNode( pAig, pObj, i ) + if ( Llb_MnxBddVar(vOrder, pObj) >= 0 ) + { + pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) ); + Cudd_Ref( (DdNode *)pObj->pData ); + } + Saig_ManForEachLi( pAig, pObj, i ) + pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) ); + // compute intermediate BDDs + vRoots = Vec_PtrAlloc( 100 ); + Aig_ManForEachNode( pAig, pObj, i ) + { + bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) ); + bBdd = Cudd_bddAnd( dd, bBdd0, bBdd1 ); + if ( bBdd == NULL ) + goto finish; + Cudd_Ref( bBdd ); + if ( pObj->pData == NULL ) + { + pObj->pData = bBdd; + continue; + } + // create new partition + bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd ); + if ( bPart == NULL ) + goto finish; + Cudd_Ref( bPart ); + Cudd_RecursiveDeref( dd, bBdd ); + Vec_PtrPush( vRoots, bPart ); +//printf( "%d ", Cudd_DagSize(bPart) ); + } + // compute register output BDDs + Saig_ManForEachLi( pAig, pObj, i ) + { + bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); + bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd0 ); + if ( bPart == NULL ) + goto finish; + Cudd_Ref( bPart ); + Vec_PtrPush( vRoots, bPart ); +//printf( "%d ", Cudd_DagSize(bPart) ); + } +//printf( "\n" ); + Aig_ManForEachNode( pAig, pObj, i ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + return vRoots; + // early termination +finish: + Aig_ManForEachNode( pAig, pObj, i ) + if ( pObj->pData ) + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); + Vec_PtrForEachEntry( DdNode *, vRoots, bPart, i ) + Cudd_RecursiveDeref( dd, bPart ); + Vec_PtrFree( vRoots ); + return NULL; +} + +/**Function************************************************************* + + Synopsis [Find simple variable ordering.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_Nonlin4CreateOrderSimple( Aig_Man_t * pAig ) +{ + Vec_Int_t * vOrder; + Aig_Obj_t * pObj; + int i, Counter = 0; + vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) ); + Aig_ManForEachPi( pAig, pObj, i ) + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); + Saig_ManForEachLi( pAig, pObj, i ) + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); + return vOrder; +} + +/**Function************************************************************* + + Synopsis [Find good static variable ordering.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4CreateOrderSmart_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter ) +{ + Aig_Obj_t * pFanin0, * pFanin1; + if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) + return; + Aig_ObjSetTravIdCurrent( pAig, pObj ); + assert( Llb_MnxBddVar(vOrder, pObj) < 0 ); + if ( Aig_ObjIsPi(pObj) ) + { + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ ); + return; + } + // try fanins with higher level first + pFanin0 = Aig_ObjFanin0(pObj); + pFanin1 = Aig_ObjFanin1(pObj); +// if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) ) + if ( pFanin0->Level > pFanin1->Level ) + { + Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter ); + Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter ); + } + else + { + Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter ); + Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter ); + } + if ( pObj->fMarkA ) + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ ); +} + +/**Function************************************************************* + + Synopsis [Collect nodes with the given fanout count.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_Nonlin4CollectHighRefNodes( Aig_Man_t * pAig, int nFans ) +{ + Vec_Int_t * vNodes; + Aig_Obj_t * pObj; + int i; + Aig_ManCleanMarkA( pAig ); + Aig_ManForEachNode( pAig, pObj, i ) + if ( Aig_ObjRefs(pObj) >= nFans ) + pObj->fMarkA = 1; + // unmark flop drivers + Saig_ManForEachLi( pAig, pObj, i ) + Aig_ObjFanin0(pObj)->fMarkA = 0; + // collect mapping + vNodes = Vec_IntAlloc( 100 ); + Aig_ManForEachNode( pAig, pObj, i ) + if ( pObj->fMarkA ) + Vec_IntPush( vNodes, Aig_ObjId(pObj) ); + Aig_ManCleanMarkA( pAig ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Find good static variable ordering.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_Nonlin4CreateOrderSmart( Aig_Man_t * pAig ) +{ + Vec_Int_t * vNodes = NULL; + Vec_Int_t * vOrder; + Aig_Obj_t * pObj; + int i, Counter = 0; +/* + // mark internal nodes to be used + Aig_ManCleanMarkA( pAig ); + vNodes = Llb_Nonlin4CollectHighRefNodes( pAig, 4 ); + Aig_ManForEachNodeVec( pAig, vNodes, pObj, i ) + pObj->fMarkA = 1; +printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) ); +*/ + + // collect nodes in the order + vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) ); + Aig_ManIncrementTravId( pAig ); + Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) ); + Saig_ManForEachLi( pAig, pObj, i ) + { + Llb_Nonlin4CreateOrderSmart_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter ); + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); + } + Aig_ManForEachPi( pAig, pObj, i ) + if ( Llb_MnxBddVar(vOrder, pObj) < 0 ) + Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); + assert( Counter <= Aig_ManPiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) ); + Aig_ManCleanMarkA( pAig ); + Vec_IntFreeP( &vNodes ); + return vOrder; +} + + +/**Function************************************************************* + + Synopsis [Creates quantifiable varaibles for both types of traversal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Llb_Nonlin4CreateVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fForward ) +{ + Vec_Int_t * vVars2Q; + Aig_Obj_t * pObj; + int i; + vVars2Q = Vec_IntAlloc( 0 ); + Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 ); + if ( fForward ) + { + Saig_ManForEachLi( pAig, pObj, i ) + Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 ); + } + else + { + Aig_ManForEachPi( pAig, pObj, i ) + Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 ); + } + return vVars2Q; +} + +/**Function************************************************************* + + Synopsis [Compute initial state in terms of current state variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4SetupVarMap( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder ) +{ + DdNode ** pVarsX, ** pVarsY; + Aig_Obj_t * pObjLo, * pObjLi; + int i; + pVarsX = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) ); + pVarsY = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) ); + Saig_ManForEachLiLo( pAig, pObjLo, pObjLi, i ) + { + pVarsX[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLo) ); + pVarsY[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) ); + } + Cudd_SetVarMap( dd, pVarsX, pVarsY, Aig_ManRegNum(pAig) ); + ABC_FREE( pVarsX ); + ABC_FREE( pVarsY ); +} + +/**Function************************************************************* + + Synopsis [Compute initial state in terms of current state variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_Nonlin4ComputeInitState( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder ) +{ + Aig_Obj_t * pObj; + DdNode * bRes, * bVar, * bTemp; + int i, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; + bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); + Saig_ManForEachLo( pAig, pObj, i ) + { + bVar = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) ); + bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bRes ); + dd->TimeStop = TimeStop; + return bRes; +} + +/**Function************************************************************* + + Synopsis [Compute initial state in terms of current state variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Llb_Nonlin4ComputeCube( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, char * pValues ) +{ + Aig_Obj_t * pObj, * pObjLi; + DdNode * bRes, * bVar, * bTemp; + int i, TimeStop; + TimeStop = dd->TimeStop; dd->TimeStop = 0; + bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes ); + Saig_ManForEachLo( pAig, pObj, i ) + { + if ( pValues[Llb_MnxBddVar(vOrder, pObj)] == 2 ) + continue; + // get the correspoding flop input variable + pObjLi = Saig_ObjLoToLi(pAig, pObj); + bVar = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) ); + if ( pValues[Llb_MnxBddVar(vOrder, pObj)] == 0 ) + bVar = Cudd_Not(bVar); + // create cube + bRes = Cudd_bddAnd( dd, bTemp = bRes, bVar ); Cudd_Ref( bRes ); + Cudd_RecursiveDeref( dd, bTemp ); + } + Cudd_Deref( bRes ); + dd->TimeStop = TimeStop; + return bRes; +} + + +/**Function************************************************************* + + Synopsis [Derives counter-example by backward reachability.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Cex_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p ) +{ + Abc_Cex_t * pCex; + Aig_Obj_t * pObj; + DdNode * bState, * bImage, * bOneCube, * bRing; + int i, v, RetValue, nPiOffset; + char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->dd) ); + assert( Vec_PtrSize(p->vRings) > 0 ); + // disable the timeout + p->dd->TimeStop = 0; + + // update quantifiable vars + Vec_IntFreeP( &p->vVars2Q ); + p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, p->pAig, p->vOrder, 0 ); + + // allocate room for the counter-example + pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) ); + pCex->iFrame = Vec_PtrSize(p->vRings) - 1; + pCex->iPo = -1; + + // get the last cube + bOneCube = Cudd_bddIntersect( p->dd, (DdNode *)Vec_PtrEntryLast(p->vRings), p->bBad ); Cudd_Ref( bOneCube ); + RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues ); + Cudd_RecursiveDeref( p->dd, bOneCube ); + assert( RetValue ); + + // write PIs of counter-example + nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1); + Saig_ManForEachPi( p->pAig, pObj, i ) + if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 ) + Aig_InfoSetBit( pCex->pData, nPiOffset + i ); + + // write state in terms of NS variables + if ( Vec_PtrSize(p->vRings) > 1 ) + { + bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues ); Cudd_Ref( bState ); + } + // perform backward analysis + Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v ) + { + if ( v == Vec_PtrSize(p->vRings) - 1 ) + continue; + // compute the next states + bImage = Llb_Nonlin4Image( p->dd, p->vRoots, bState, p->vVars2Q ); + assert( bImage != NULL ); + Cudd_Ref( bImage ); + Cudd_RecursiveDeref( p->dd, bState ); + + // intersect with the previous set + bOneCube = Cudd_bddIntersect( p->dd, bImage, bRing ); Cudd_Ref( bOneCube ); + Cudd_RecursiveDeref( p->dd, bImage ); + + // find any assignment of the BDD + RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues ); + Cudd_RecursiveDeref( p->dd, bOneCube ); + assert( RetValue ); + + // write PIs of counter-example + nPiOffset -= Saig_ManPiNum(p->pAig); + Saig_ManForEachPi( p->pAig, pObj, i ) + if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 ) + Aig_InfoSetBit( pCex->pData, nPiOffset + i ); + + // check that we get the init state + if ( v == 0 ) + { + Saig_ManForEachLo( p->pAig, pObj, i ) + assert( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 0 ); + break; + } + + // write state in terms of NS variables + bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues ); Cudd_Ref( bState ); + } + assert( nPiOffset == Saig_ManRegNum(p->pAig) ); + // update the output number +//Abc_CexPrint( pCex ); + RetValue = Saig_ManFindFailedPoCex( p->pAig, pCex ); + assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pAig) ); // invalid CEX!!! + pCex->iPo = RetValue; + // cleanup + ABC_FREE( pValues ); + return pCex; +} + + +/**Function************************************************************* + + Synopsis [Perform reachability with hints.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) +{ + DdNode * bAux; + int nIters, nBddSizeFr, nBddSizeTo, nBddSizeTo2; + int clkTemp, clkIter, clk = clock(); + assert( Aig_ManRegNum(p->pAig) > 0 ); + + // compute time to stop + if ( p->pPars->TimeLimit ) + p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC; + else + p->pPars->TimeTarget = 0; + // set the stop time parameter + p->dd->TimeStop = p->pPars->TimeTarget; + + // create bad state in the ring manager + if ( !p->pPars->fSkipOutCheck ) + { + p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder ); + if ( p->bBad == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = -1; + return -1; + } + Cudd_Ref( p->bBad ); + } + + // compute the starting set of states + p->bCurrent = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder ); Cudd_Ref( p->bCurrent ); + p->bReached = p->bCurrent; Cudd_Ref( p->bCurrent ); + for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ ) + { + clkIter = clock(); + // check the runtime limit + if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = nIters - 1; + return -1; + } + + // save the onion ring + Vec_PtrPush( p->vRings, p->bCurrent ); Cudd_Ref( p->bCurrent ); + + // check it for bad states + if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->dd, p->bCurrent, Cudd_Not(p->bBad) ) ) + { + assert( p->pAig->pSeqModel == NULL ); + if ( !p->pPars->fBackward ) + p->pAig->pSeqModel = Llb_Nonlin4DeriveCex( p ); + if ( !p->pPars->fSilent ) + { + if ( !p->pPars->fBackward ) + printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pAig->pSeqModel->iPo, nIters ); + else + printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); + Abc_PrintTime( 1, "Time", clock() - clk ); + } + p->pPars->iFrame = nIters - 1; + return 0; + } + + // compute the next states + clkTemp = clock(); + p->bNext = Llb_Nonlin4Image( p->dd, p->vRoots, p->bCurrent, p->vVars2Q ); + if ( p->bNext == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during image computation in quantification.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = nIters - 1; + return -1; + } + Cudd_Ref( p->bNext ); + p->timeImage += clock() - clkTemp; + + // remap into current states + clkTemp = clock(); + p->bNext = Cudd_bddVarMap( p->dd, bAux = p->bNext ); + if ( p->bNext == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during remapping next states.\n", p->pPars->TimeLimit ); + Cudd_RecursiveDeref( p->dd, bAux ); + p->pPars->iFrame = nIters - 1; + return -1; + } + Cudd_Ref( p->bNext ); + Cudd_RecursiveDeref( p->dd, bAux ); + p->timeRemap += clock() - clkTemp; + + // collect statistics + if ( p->pPars->fVerbose ) + { + nBddSizeFr = Cudd_DagSize( p->bCurrent ); + nBddSizeTo = Cudd_DagSize( bAux ); + nBddSizeTo2 = Cudd_DagSize( p->bNext ); + } + Cudd_RecursiveDeref( p->dd, p->bCurrent ); p->bCurrent = NULL; + + // derive new states + p->bCurrent = Cudd_bddAnd( p->dd, p->bNext, Cudd_Not(p->bReached) ); + if ( p->bCurrent == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = nIters - 1; + return -1; + } + Cudd_Ref( p->bCurrent ); + Cudd_RecursiveDeref( p->dd, p->bNext ); p->bNext = NULL; + if ( Cudd_IsConstant(p->bCurrent) ) + break; + + // add to the reached set + p->bReached = Cudd_bddOr( p->dd, bAux = p->bReached, p->bCurrent ); + if ( p->bReached == NULL ) + { + if ( !p->pPars->fSilent ) + printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit ); + p->pPars->iFrame = nIters - 1; + Cudd_RecursiveDeref( p->dd, bAux ); + return -1; + } + Cudd_Ref( p->bReached ); + Cudd_RecursiveDeref( p->dd, bAux ); + + // report the results + if ( p->pPars->fVerbose ) + { + printf( "I =%5d : ", nIters ); + printf( "Fr =%7d ", nBddSizeFr ); + printf( "ImNs =%7d ", nBddSizeTo ); + printf( "ImCs =%7d ", nBddSizeTo2 ); + printf( "Rea =%7d ", Cudd_DagSize(p->bReached) ); + printf( "(%4d %4d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) ); + Abc_PrintTime( 1, "T", clock() - clkIter ); + } +/* + if ( pPars->fVerbose ) + { + double nMints = Cudd_CountMinterm(p->dd, bReached, Saig_ManRegNum(p->pAig) ); +// Extra_bddPrint( p->dd, bReached );printf( "\n" ); + printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) ); + fflush( stdout ); + } +*/ + if ( nIters == p->pPars->nIterMax - 1 ) + { + if ( !p->pPars->fSilent ) + printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax ); + p->pPars->iFrame = nIters; + return -1; + } + } + + // report the stats + if ( p->pPars->fVerbose ) + { + double nMints = Cudd_CountMinterm(p->dd, p->bReached, Saig_ManRegNum(p->pAig) ); + if ( p->bCurrent && Cudd_IsConstant(p->bCurrent) ) + printf( "Reachability analysis completed after %d frames.\n", nIters ); + else + printf( "Reachability analysis is stopped after %d frames.\n", nIters ); + printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) ); + fflush( stdout ); + } + if ( p->bCurrent == NULL || !Cudd_IsConstant(p->bCurrent) ) + { + if ( !p->pPars->fSilent ) + printf( "Verified only for states reachable in %d frames. ", nIters ); + p->pPars->iFrame = p->pPars->nIterMax; + return -1; // undecided + } + // report + if ( !p->pPars->fSilent ) + printf( "The miter is proved unreachable after %d iterations. ", nIters ); + p->pPars->iFrame = nIters - 1; + Abc_PrintTime( 1, "Time", clock() - clk ); + return 1; // unreachable +} + +/**Function************************************************************* + + Synopsis [Reorders BDDs in the working manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, int fVerbose ) +{ + int clk = clock(); + if ( fVerbose ) + Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); + if ( fVerbose ) + Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + if ( fTwice ) + { + Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 ); + if ( fVerbose ) + Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) ); + } + if ( fVerbose ) + Abc_PrintTime( 1, "Time", clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) +{ + Llb_Mnx_t * p; + p = ABC_CALLOC( Llb_Mnx_t, 1 ); + p->pAig = pAig; + p->pPars = pPars; +// p->vOrder = Llb_Nonlin4CreateOrderSimple( pAig ); + p->vOrder = Llb_Nonlin4CreateOrderSmart( pAig ); + p->dd = Cudd_Init( Vec_IntSize(p->vOrder), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Llb_Nonlin4SetupVarMap( p->dd, pAig, p->vOrder ); + Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); + p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, pAig, p->vOrder, 1 ); + p->vRoots = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder ); + p->vRings = Vec_PtrAlloc( 100 ); + if ( pPars->fReorder ) + Llb_Nonlin4Reorder( p->dd, 0, 1 ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Llb_MnxStop( Llb_Mnx_t * p ) +{ + DdNode * bTemp; + int i; + if ( p->pPars->fVerbose ) + { + p->timeReo = Cudd_ReadReorderingTime(p->dd); + p->timeOther = p->timeTotal - p->timeImage - p->timeRemap; + ABC_PRTP( "Image ", p->timeImage, p->timeTotal ); + ABC_PRTP( "Remap ", p->timeRemap, p->timeTotal ); + ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); + ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + ABC_PRTP( " reo ", p->timeReo, p->timeTotal ); + } + // remove BDDs + if ( p->bBad ) + Cudd_RecursiveDeref( p->dd, p->bBad ); + if ( p->bReached ) + Cudd_RecursiveDeref( p->dd, p->bReached ); + if ( p->bCurrent ) + Cudd_RecursiveDeref( p->dd, p->bCurrent ); + if ( p->bNext ) + Cudd_RecursiveDeref( p->dd, p->bNext ); + Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i ) + Cudd_RecursiveDeref( p->dd, bTemp ); + Vec_PtrForEachEntry( DdNode *, p->vRoots, bTemp, i ) + Cudd_RecursiveDeref( p->dd, bTemp ); + // remove arrays + Vec_PtrFree( p->vRings ); + Vec_PtrFree( p->vRoots ); + Extra_StopManager( p->dd ); + Vec_IntFreeP( &p->vOrder ); + Vec_IntFreeP( &p->vVars2Q ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [Finds balanced cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ) +{ + Llb_Mnx_t * pMnn; + int RetValue = -1; + if ( pPars->fVerbose ) + Aig_ManPrintStats( pAig ); + if ( !pPars->fSkipReach ) + { + int clk = clock(); + pMnn = Llb_MnxStart( pAig, pPars ); + RetValue = Llb_Nonlin4Reachability( pMnn ); + pMnn->timeTotal = clock() - clk; + Llb_MnxStop( pMnn ); + } + return RetValue; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h index 496d975d..357ddb5c 100644 --- a/src/aig/llb/llbInt.h +++ b/src/aig/llb/llbInt.h @@ -176,12 +176,20 @@ extern DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeav extern DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder ); extern void Llb_NonlinImageQuit(); -/*=== llb3Image.c ======================================================*/ +/*=== llb3Image.c =======================================================*/ extern 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, int Limit, int TimeTarget ); /*=== llb3Nonlin.c ======================================================*/ extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd ); +/*=== llb4Image.c =======================================================*/ +extern DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q ); +/*=== llb4Map.c =========================================================*/ +//extern Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin ); +/*=== llb4Nonlin.c ======================================================*/ +extern int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ); + + ABC_NAMESPACE_HEADER_END diff --git a/src/aig/llb/module.make b/src/aig/llb/module.make index 56beca25..028e9fe4 100644 --- a/src/aig/llb/module.make +++ b/src/aig/llb/module.make @@ -16,4 +16,6 @@ SRC += src/aig/llb/llb.c \ src/aig/llb/llb2Flow.c \ src/aig/llb/llb2Image.c \ src/aig/llb/llb3Image.c \ - src/aig/llb/llb3Nonlin.c + src/aig/llb/llb3Nonlin.c \ + src/aig/llb/llb4Image.c \ + src/aig/llb/llb4Nonlin.c diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b100ba19..99d44937 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -373,6 +373,7 @@ static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9ReachM ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ReachP ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ReachN ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9ReachY ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Undo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -784,6 +785,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&reachm", Abc_CommandAbc9ReachM, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reachp", Abc_CommandAbc9ReachP, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reachn", Abc_CommandAbc9ReachN, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&reachy", Abc_CommandAbc9ReachY, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&undo", Abc_CommandAbc9Undo, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); @@ -8528,6 +8530,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Aig_ManTerSimulate( pAig ); Aig_ManStop( pAig ); } +*/ +/* +{ + extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut ); + Ssm_ManExperiment( "m\\big1.ssim", "m\\big1_.ssim" ); +} */ return 0; usage: @@ -27957,6 +27965,137 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_ParLlb_t Pars, * pPars = &Pars; + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + Aig_Man_t * pMan; + char * pLogFileName = NULL; + int c; + extern int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars ); + + // set defaults + Llb_ManSetDefaultParams( pPars ); + pPars->fReorder = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "BFTLryzvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBddMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBddMax < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nIterMax < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->TimeLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->TimeLimit < 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" ); + goto usage; + } + pLogFileName = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'r': + pPars->fReorder ^= 1; + break; + case 'y': + pPars->fSkipOutCheck ^= 1; + break; + case 'z': + pPars->fSkipReach ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9ReachN(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9ReachN(): The current AIG has no latches.\n" ); + return 0; + } + if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) ) + { + Abc_Print( -1, "Abc_CommandAbc9ReachN(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) ); + return 0; + } + pMan = Gia_ManToAigSimple( pAbc->pGia ); + pAbc->Status = Llb_Nonlin4CoreReach( pMan, pPars ); + pAbc->nFrames = pPars->iFrame; + Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel ); + if ( pLogFileName ) + Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachn" ); + Aig_ManStop( pMan ); + return 0; + +usage: + Abc_Print( -2, "usage: &reachy [-BFT num] [-L file] [-ryzvh]\n" ); + Abc_Print( -2, "\t model checking via BDD-based reachability (non-linear-QS-based)\n" ); + Abc_Print( -2, "\t-B num : the BDD node increase when hints kick in [default = %d]\n", pPars->nBddMax ); + Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax ); + Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit ); + Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); + Abc_Print( -2, "\t-r : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" ); + Abc_Print( -2, "\t-y : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" ); + Abc_Print( -2, "\t-z : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" ); + Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); +// Abc_Print( -2, "\t-w : prints additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index ce1366de..7f7c68c4 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ); +extern If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars ); static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk ); extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover ); static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj ); diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c index e3b2e556..8dd8f8c5 100644 --- a/src/bdd/cudd/cuddCompose.c +++ b/src/bdd/cudd/cuddCompose.c @@ -1251,6 +1251,9 @@ cuddBddVarMapRecur( return(Cudd_NotCond(res,F != f)); } + if ( manager->TimeStop && manager->TimeStop < clock() ) + return NULL; + /* Split and recur on children of this node. */ T = cuddBddVarMapRecur(manager,cuddT(F)); if (T == NULL) return(NULL); diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h index 83c334b4..cb3b3445 100644 --- a/src/misc/vec/vecVec.h +++ b/src/misc/vec/vecVec.h @@ -64,6 +64,8 @@ struct Vec_Vec_t_ for ( i = Vec_VecSize(vGlob)-1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) #define Vec_VecForEachLevelReverseStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ for ( i = LevelStart-1; (i >= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) +#define Vec_VecForEachLevelTwo( vGlob1, vGlob2, vVec1, vVec2, i ) \ + for ( i = 0; (i < Vec_VecSize(vGlob1)) && (((vVec1) = (Vec_Ptr_t*)Vec_VecEntry(vGlob1, i)), 1) && (((vVec2) = (Vec_Ptr_t*)Vec_VecEntry(vGlob2, i)), 1); i++ ) // iterators through levels #define Vec_VecForEachLevelInt( vGlob, vVec, i ) \ @@ -78,6 +80,8 @@ struct Vec_Vec_t_ for ( i = Vec_VecSize(vGlob)-1; (i >= 0) && (((vVec) = (Vec_Int_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) #define Vec_VecForEachLevelIntReverseStartStop( vGlob, vVec, i, LevelStart, LevelStop ) \ for ( i = LevelStart-1; (i >= LevelStop) && (((vVec) = (Vec_Int_t*)Vec_VecEntry(vGlob, i)), 1); i-- ) +#define Vec_VecForEachLevelIntTwo( vGlob1, vGlob2, vVec1, vVec2, i ) \ + for ( i = 0; (i < Vec_VecSize(vGlob1)) && (((vVec1) = (Vec_Int_t*)Vec_VecEntry(vGlob1, i)), 1) && (((vVec2) = (Vec_Int_t*)Vec_VecEntry(vGlob2, i)), 1); i++ ) // iteratores through entries #define Vec_VecForEachEntry( Type, vGlob, pEntry, i, k ) \ -- cgit v1.2.3