diff options
-rw-r--r-- | abclib.dsp | 4 | ||||
-rw-r--r-- | src/base/abci/abc.c | 8 | ||||
-rw-r--r-- | src/sat/bmc/bmcUnroll.c | 455 | ||||
-rw-r--r-- | src/sat/bmc/module.make | 3 |
4 files changed, 467 insertions, 3 deletions
@@ -1409,6 +1409,10 @@ SOURCE=.\src\sat\bmc\bmcCexMin2.c SOURCE=.\src\sat\bmc\bmcCexTools.c # End Source File +# Begin Source File + +SOURCE=.\src\sat\bmc\bmcUnroll.c +# End Source File # End Group # End Group # Begin Group "opt" diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2baab045..e9d6d9e8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30355,7 +30355,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose ); // extern void Ga2_ManComputeTest( Gia_Man_t * p ); // extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); - extern void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); +// extern void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose ); + extern void Unr_ManTest( Gia_Man_t * pGia ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -30379,11 +30380,13 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" ); return 1; } +/* if ( pAbc->pCex == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Test(): There is no CEX.\n" ); return 1; } +*/ // Gia_ManFrontTest( pAbc->pGia ); // Gia_ManReduceConst( pAbc->pGia, 1 ); // Sat_ManTest( pAbc->pGia, Gia_ManCo(pAbc->pGia, 0), 0 ); @@ -30401,7 +30404,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_IsoTest( pAbc->pGia, fVerbose ); // Ga2_ManComputeTest( pAbc->pGia ); // Bmc_CexTest( pAbc->pGia, pAbc->pCex, fVerbose ); - Gia_IsoTest( pAbc->pGia, pAbc->pCex, 0 ); +// Gia_IsoTest( pAbc->pGia, pAbc->pCex, 0 ); + Unr_ManTest( pAbc->pGia ); return 0; usage: Abc_Print( -2, "usage: &test [-svh]\n" ); diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c new file mode 100644 index 00000000..b9c414ca --- /dev/null +++ b/src/sat/bmc/bmcUnroll.c @@ -0,0 +1,455 @@ +/**CFile**************************************************************** + + FileName [bmcUnroll.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [Unrolling manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define UNR_DIFF_NULL 0xFFFF + +typedef struct Unr_Obj_t_ Unr_Obj_t; // 24 bytes + (RankMax-1) * 4 bytes +struct Unr_Obj_t_ +{ + unsigned hFan0; // address of the fanin + unsigned hFan1; // address of the fanin + unsigned fCompl0 : 1; // complemented bit + unsigned fCompl1 : 1; // complemented bit + unsigned uRDiff0 : 15; // rank diff of the fanin + unsigned uRDiff1 : 15; // rank diff of the fanin + unsigned RankMax : 16; // max rank diff between node and its fanout + unsigned RankCur : 16; // cur rank of the node + unsigned OrigId; // original object ID + unsigned Res[1]; // RankMax entries +}; + +typedef struct Unr_Man_t_ Unr_Man_t; +struct Unr_Man_t_ +{ + // input data + Gia_Man_t * pGia; // the user's AIG manager + Gia_Man_t * pNew; // unrolling manager + int nObjs; // the number of objects + // intermediate data + Vec_Int_t * vOrder; // ordering of GIA objects + Vec_Int_t * vOrderLim; // beginning of each time frame + Vec_Int_t * vTents; // tents of GIA objects + Vec_Int_t * vRanks; // ranks of GIA objects + // unrolling data + int * pObjs; // storage for unroling objects + int * pEnd; // end of storage + Vec_Int_t * vObjLim; // handle of the first object in each frame + Vec_Int_t * vResLits; // resulting literals + Vec_Int_t * vCiMap; // mapping of GIA CIs into unrolling objects + Vec_Int_t * vPoMap; // mapping of GIA POs into unrolling objects +}; + +static inline Unr_Obj_t * Unr_ManObj( Unr_Man_t * p, int h ) { assert( h >= 0 && h < p->pEnd - p->pObjs ); return (Unr_Obj_t *)(p->pObjs + h); } +static inline int Unr_ManFanin0Value( Unr_Man_t * p, Unr_Obj_t * pObj ) +{ + Unr_Obj_t * pFanin = Unr_ManObj( p, pObj->hFan0 ); + int Index = (pFanin->RankCur + pFanin->RankMax - pObj->uRDiff0) % pFanin->RankMax; + assert( pFanin->RankCur <= pFanin->RankMax ); + assert( pObj->uRDiff0 <= pFanin->RankMax ); + return Abc_LitNotCond( pFanin->Res[Index], pObj->fCompl0 ); +} +static inline int Unr_ManFanin1Value( Unr_Man_t * p, Unr_Obj_t * pObj ) +{ + Unr_Obj_t * pFanin = Unr_ManObj( p, pObj->hFan1 ); + int Index = (pFanin->RankCur + pFanin->RankMax - pObj->uRDiff1) % pFanin->RankMax; + assert( pFanin->RankCur <= pFanin->RankMax ); + assert( pObj->uRDiff1 <= pFanin->RankMax ); + return Abc_LitNotCond( pFanin->Res[Index], pObj->fCompl1 ); +} +static inline void Unr_ManObjSetValue( Unr_Man_t * p, Unr_Obj_t * pObj, int Value ) +{ + pObj->Res[ pObj->RankCur ] = Value; + pObj->RankCur = (pObj->RankCur + 1) % pObj->RankMax; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_IntWriteMaxEntry( Vec_Int_t * p, int i, int Entry ) +{ + assert( i >= 0 && i < p->nSize ); + p->pArray[i] = Abc_MaxInt( p->pArray[i], Entry ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Unr_ManProfileRanks( Vec_Int_t * vRanks ) +{ + int RankMax = Vec_IntFindMax( vRanks ); + Vec_Int_t * vCounts = Vec_IntStart( RankMax+1 ); + int i, Rank, Count, nExtras = 0; + Vec_IntForEachEntry( vRanks, Rank, i ) + Vec_IntAddToEntry( vCounts, Rank, 1 ); + Vec_IntForEachEntry( vCounts, Count, i ) + { + printf( "%2d : %8d (%6.2f %%)\n", i, Count, 100.0 * Count / Vec_IntSize(vRanks) ); + nExtras += Count * i; + } + printf( "Extra space = %d (%6.2f %%)\n", nExtras, 100.0 * nExtras / Vec_IntSize(vRanks) ); + Vec_IntFree( vCounts ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Unr_ManSetup_rec( Unr_Man_t * p, int iObj, int iTent, Vec_Int_t * vRoots ) +{ + Gia_Obj_t * pObj; + int iFanin; + if ( Vec_IntEntry(p->vTents, iObj) >= 0 ) + return; + Vec_IntWriteEntry(p->vTents, iObj, iTent); + pObj = Gia_ManObj( p->pGia, iObj ); + if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) ) + { + Unr_ManSetup_rec( p, (iFanin = Gia_ObjFaninId0(pObj, iObj)), iTent, vRoots ); + Vec_IntWriteMaxEntry( p->vRanks, iFanin, iTent - Vec_IntEntry(p->vTents, iFanin) ); + } + if ( Gia_ObjIsAnd(pObj) ) + { + Unr_ManSetup_rec( p, (iFanin = Gia_ObjFaninId1(pObj, iObj)), iTent, vRoots ); + Vec_IntWriteMaxEntry( p->vRanks, iFanin, iTent - Vec_IntEntry(p->vTents, iFanin) ); + } + else if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + Vec_IntPush( vRoots, (iFanin = Gia_ObjId(p->pGia, Gia_ObjRoToRi(p->pGia, pObj))) ); + Vec_IntWriteMaxEntry( p->vRanks, iFanin, 1 ); + } + Vec_IntPush( p->vOrder, iObj ); +} +void Unr_ManSetup( Unr_Man_t * p ) +{ + Vec_Int_t * vRoots, * vRoots2, * vMap; + Gia_Obj_t * pObj, * pObjRi; + Unr_Obj_t * pUnrObj; + int i, k, t, iObj, nInts, * pInts; + clock_t clk = clock(); + vRoots = Vec_IntAlloc( 100 ); + vRoots2 = Vec_IntAlloc( 100 ); + // create zero rank + assert( Vec_IntSize(p->vOrder) == 0 ); + Vec_IntPush( p->vOrder, 0 ); + Vec_IntPush( p->vOrderLim, Vec_IntSize(p->vOrder) ); + Vec_IntWriteEntry( p->vTents, 0, 0 ); + Vec_IntWriteEntry( p->vRanks, 0, 0 ); + // start from the POs + Gia_ManForEachPo( p->pGia, pObj, i ) + Unr_ManSetup_rec( p, Gia_ObjId(p->pGia, pObj), 0, vRoots ); + // iterate through tents + while ( Vec_IntSize(vRoots) > 0 ) + { + Vec_IntPush( p->vOrderLim, Vec_IntSize(p->vOrder) ); + Vec_IntClear( vRoots2 ); + Vec_IntForEachEntry( vRoots, iObj, i ) + Unr_ManSetup_rec( p, iObj, Vec_IntSize(p->vOrderLim)-1, vRoots2 ); + ABC_SWAP( Vec_Int_t *, vRoots, vRoots2 ); + } + Vec_IntPush( p->vOrderLim, Vec_IntSize(p->vOrder) ); + Vec_IntWriteEntry( p->vRanks, 0, 0 ); + Vec_IntFree( vRoots ); + Vec_IntFree( vRoots2 ); + // allocate memory + nInts = Vec_IntSize(p->vOrder) * (sizeof(Unr_Obj_t) / sizeof(int)) + Vec_IntSum(p->vRanks); + p->pObjs = pInts = ABC_CALLOC( int, nInts ); + p->pEnd = p->pObjs + nInts; + vMap = Vec_IntStartFull( p->nObjs ); + // create const0 node + pUnrObj = Unr_ManObj( p, pInts - p->pObjs ); + pUnrObj->RankMax = 1; + pUnrObj->uRDiff0 = pUnrObj->uRDiff1 = UNR_DIFF_NULL; + pUnrObj->Res[0] = 0; // const0 + pInts += sizeof(Unr_Obj_t) / sizeof(int); + // mark up the entries + assert( Vec_IntSize(p->vObjLim) == 0 ); + Vec_IntPush( p->vObjLim, pInts - p->pObjs ); + for ( t = Vec_IntSize(p->vOrderLim) - 2; t >= 0; t-- ) + { + int Beg = Vec_IntEntry(p->vOrderLim, t); + int End = Vec_IntEntry(p->vOrderLim, t+1); + Vec_IntForEachEntryStartStop( p->vOrder, iObj, i, Beg, End ) + { + pObj = Gia_ManObj( p->pGia, iObj ); + pUnrObj = Unr_ManObj( p, pInts - p->pObjs ); + pUnrObj->uRDiff0 = pUnrObj->uRDiff1 = UNR_DIFF_NULL; + if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) ) + { + pUnrObj->hFan0 = Vec_IntEntry( vMap, Gia_ObjFaninId0(pObj, iObj) ); + pUnrObj->fCompl0 = Gia_ObjFaninC0(pObj); + pUnrObj->uRDiff0 = Vec_IntEntry(p->vTents, iObj) - Vec_IntEntry(p->vTents, Gia_ObjFaninId0(pObj, iObj)); + } + if ( Gia_ObjIsAnd(pObj) ) + { + pUnrObj->hFan1 = Vec_IntEntry( vMap, Gia_ObjFaninId1(pObj, iObj) ); + pUnrObj->fCompl1 = Gia_ObjFaninC1(pObj); + pUnrObj->uRDiff1 = Vec_IntEntry(p->vTents, iObj) - Vec_IntEntry(p->vTents, Gia_ObjFaninId1(pObj, iObj)); + } + else if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + pObjRi = Gia_ObjRoToRi(p->pGia, pObj); + pUnrObj->hFan0 = Vec_IntEntry( vMap, Gia_ObjId(p->pGia, pObjRi) ); + pUnrObj->fCompl0 = 0; + pUnrObj->uRDiff0 = 1; + } + pUnrObj->RankMax = Vec_IntEntry(p->vRanks, iObj) + 1; + pUnrObj->RankCur = 0; + pUnrObj->OrigId = iObj; + for ( k = 0; k < (int)pUnrObj->RankMax; k++ ) + pUnrObj->Res[k] = -1; + Vec_IntWriteEntry( vMap, iObj, pInts - p->pObjs ); + pInts += sizeof(Unr_Obj_t) / sizeof(int) + pUnrObj->RankMax - 1; + } + Vec_IntPush( p->vObjLim, pInts - p->pObjs ); + } + assert( pInts - p->pObjs == nInts ); + Vec_IntFreeP( &p->vOrder ); + Vec_IntFreeP( &p->vOrderLim ); + Vec_IntFreeP( &p->vTents ); +Unr_ManProfileRanks( p->vRanks ); + Vec_IntFreeP( &p->vRanks ); + // store CI/PO objects; + Gia_ManForEachCi( p->pGia, pObj, i ) + Vec_IntPush( p->vCiMap, Vec_IntEntry(vMap, Gia_ObjId(p->pGia, pObj)) ); + Gia_ManForEachPo( p->pGia, pObj, i ) + Vec_IntPush( p->vPoMap, Vec_IntEntry(vMap, Gia_ObjId(p->pGia, pObj)) ); + Vec_IntFreeP( &vMap ); + + printf( "Memory usage = %6.2f MB\n", 4.0 * nInts / (1<<20) ); + Abc_PrintTime( 1, "Time", clock() - clk ); +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Unr_Man_t * Unr_ManAlloc( Gia_Man_t * pGia ) +{ + Unr_Man_t * p; + p = ABC_CALLOC( Unr_Man_t, 1 ); + p->pGia = pGia; + p->nObjs = Gia_ManObjNum(pGia); + p->pNew = Gia_ManStart( 10000 ); + p->vOrder = Vec_IntAlloc( p->nObjs ); + p->vOrderLim = Vec_IntAlloc( 100 ); + p->vTents = Vec_IntStartFull( p->nObjs ); + p->vRanks = Vec_IntStart( p->nObjs ); + p->vObjLim = Vec_IntAlloc( 100 ); + p->vResLits = Vec_IntAlloc( Gia_ManPoNum(pGia) ); + p->vCiMap = Vec_IntAlloc( Gia_ManCiNum(pGia) ); + p->vPoMap = Vec_IntAlloc( Gia_ManPoNum(pGia) ); + return p; +} +void Unr_ManFree( Unr_Man_t * p ) +{ + Gia_ManStop( p->pNew ); + // intermediate data + Vec_IntFreeP( &p->vOrder ); + Vec_IntFreeP( &p->vOrderLim ); + Vec_IntFreeP( &p->vTents ); + Vec_IntFreeP( &p->vRanks ); + // unrolling data + Vec_IntFreeP( &p->vObjLim ); + Vec_IntFreeP( &p->vResLits ); + Vec_IntFreeP( &p->vCiMap ); + Vec_IntFreeP( &p->vPoMap ); + ABC_FREE( p->pObjs ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Perform smart unrolling.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Unr_ManUnroll( Unr_Man_t * p, int nFrames ) +{ + Gia_Man_t * pGia, * pFrames; + Unr_Obj_t * pUnrObj; + int f, i, iLit, iLit0, iLit1, hStart; + pFrames = Gia_ManStart( 10000 ); + pFrames->pName = Abc_UtilStrsav( p->pGia->pName ); + Gia_ManHashAlloc( pFrames ); + // create flop values + for ( i = 0; i < Gia_ManRegNum(p->pGia); i++ ) + { + pUnrObj = Unr_ManObj(p, Vec_IntEntry(p->vCiMap, Gia_ManPiNum(p->pGia) + i)); + Unr_ManObjSetValue( p, pUnrObj, 0 ); + } + for ( f = 0; f < nFrames; f++ ) + { + for ( i = 0; i < Gia_ManPiNum(p->pGia); i++ ) + { + pUnrObj = Unr_ManObj(p, Vec_IntEntry(p->vCiMap, Gia_ManPiNum(p->pGia) + i)); + Unr_ManObjSetValue( p, pUnrObj, Gia_ManAppendCi(pFrames) ); + } + hStart = f < Vec_IntSize(p->vObjLim)-1 ? Vec_IntEntry( p->vObjLim, Vec_IntSize(p->vObjLim)-2 - f ) : 0; + while ( p->pObjs + hStart < p->pEnd ) + { + pUnrObj = Unr_ManObj( p, hStart ); + if ( pUnrObj->uRDiff0 != UNR_DIFF_NULL && pUnrObj->uRDiff1 != UNR_DIFF_NULL ) + { + iLit0 = Unr_ManFanin0Value( p, pUnrObj ); + iLit1 = Unr_ManFanin1Value( p, pUnrObj ); + iLit = Gia_ManAppendAnd( pFrames, iLit0, iLit1 ); + Unr_ManObjSetValue( p, pUnrObj, iLit ); + } + else if ( pUnrObj->uRDiff1 == UNR_DIFF_NULL ) + { + iLit = Unr_ManFanin0Value( p, pUnrObj ); + Unr_ManObjSetValue( p, pUnrObj, iLit ); + } + hStart += sizeof(Unr_Obj_t) / sizeof(int) + pUnrObj->RankMax - 1; + } + assert( p->pObjs + hStart == p->pEnd ); + } + Gia_ManHashStop( pFrames ); + Gia_ManSetRegNum( pFrames, 0 ); + pFrames = Gia_ManCleanup( pGia = pFrames ); + Gia_ManStop( pGia ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Perform naive unrolling.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Unr_ManUnrollSimple( Gia_Man_t * pGia, int nFrames ) +{ + Gia_Man_t * pFrames; + Gia_Obj_t * pObj, * pObjRi; + int f, i; + pFrames = Gia_ManStart( Gia_ManObjNum(pGia) * nFrames ); + pFrames->pName = Abc_UtilStrsav( pGia->pName ); + Gia_ManHashAlloc( pFrames ); + Gia_ManConst0(pGia)->Value = 0; + Gia_ManForEachRi( pGia, pObj, i ) + pObj->Value = 0; + for ( f = 0; f < nFrames; f++ ) + { + Gia_ManForEachPi( pGia, pObj, i ) + pObj->Value = Gia_ManAppendCi(pFrames); + Gia_ManForEachRiRo( pGia, pObjRi, pObj, i ) + pObj->Value = pObjRi->Value; + Gia_ManForEachAnd( pGia, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( pGia, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + Gia_ManForEachPo( pGia, pObj, i ) + Gia_ManAppendCo( pFrames, pObj->Value ); + } + Gia_ManHashStop( pFrames ); + Gia_ManSetRegNum( pFrames, 0 ); + pFrames = Gia_ManCleanup( pGia = pFrames ); + Gia_ManStop( pGia ); + return pFrames; +} + +/**Function************************************************************* + + Synopsis [Perform evaluation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Unr_ManTest( Gia_Man_t * pGia ) +{ +// Gia_Man_t * pFrames0, * pFrames1; + int nFrames = 10; + Unr_Man_t * p; + p = Unr_ManAlloc( pGia ); + Unr_ManSetup( p ); +// pFrames0 = Unr_ManUnroll( p, nFrames ); + Unr_ManFree( p ); +// pFrames1 = Unr_ManUnrollSimple( pGia, nFrames ); +//Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0 ); +//Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0 ); +// Gia_ManStop( pFrames0 ); +// Gia_ManStop( pFrames1 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index 41747be7..b35577fb 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -5,4 +5,5 @@ SRC += src/sat/bmc/bmc.c \ src/sat/bmc/bmcCexCut.c \ src/sat/bmc/bmcCexMin1.c \ src/sat/bmc/bmcCexMin2.c \ - src/sat/bmc/bmcCexTools.c + src/sat/bmc/bmcCexTools.c \ + src/sat/bmc/bmcUnroll.c |