diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 17 | ||||
| -rw-r--r-- | src/misc/vec/vecHsh4.h | 208 | ||||
| -rw-r--r-- | src/sat/bmc/bmc.h | 1 | ||||
| -rw-r--r-- | src/sat/bmc/bmcBmcAnd.c | 425 |
5 files changed, 644 insertions, 11 deletions
@@ -2779,6 +2779,10 @@ SOURCE=.\src\misc\vec\vecHsh.h # End Source File # Begin Source File +SOURCE=.\src\misc\vec\vecHsh4.h +# End Source File +# Begin Source File + SOURCE=.\src\misc\vec\vecInt.h # End Source File # Begin Source File diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4ee8245d..5cc4fe97 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -31781,6 +31781,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) memset( pPars, 0, sizeof(Bmc_AndPar_t) ); pPars->nStart = 0; // starting timeframe pPars->nFramesMax = 0; // maximum number of timeframes + pPars->nFramesAdd = 50; // the number of additional frames pPars->nConfLimit = 0; // maximum number of conflicts at a node pPars->fLoadCnf = 0; // dynamic CNF loading pPars->fDumpFrames = 0; // dump unrolled timeframes @@ -31791,7 +31792,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nFailOuts = 0; // the number of failed outputs pPars->nDropOuts = 0; // the number of dropped outputs Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFcdvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFAcdvwh" ) ) != EOF ) { switch ( c ) { @@ -31817,6 +31818,17 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nFramesMax < 0 ) goto usage; break; + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesAdd < 0 ) + goto usage; + break; case 'c': pPars->fLoadCnf ^= 1; break; @@ -31844,10 +31856,11 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &bmc [-SF num] [-cdvwh]\n" ); + Abc_Print( -2, "usage: &bmc [-SFA num] [-cdvwh]\n" ); Abc_Print( -2, "\t performs bounded model checking\n" ); Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax ); + Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd ); Abc_Print( -2, "\t-c : toggle dynamic CNF loading [default = %s]\n", pPars->fLoadCnf? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dumping unfolded timeframes [default = %s]\n", pPars->fDumpFrames? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); diff --git a/src/misc/vec/vecHsh4.h b/src/misc/vec/vecHsh4.h new file mode 100644 index 00000000..bd44f35e --- /dev/null +++ b/src/misc/vec/vecHsh4.h @@ -0,0 +1,208 @@ +/**CFile**************************************************************** + + FileName [vecHsh4.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Resizable arrays.] + + Synopsis [Hashing pairs of integers into an integer.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: vecHsh4.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__misc__vec__vecHsh4_h +#define ABC__misc__vec__vecHsh4_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Hsh_Int4Obj_t_ Hsh_Int4Obj_t; +struct Hsh_Int4Obj_t_ +{ + int iData0; + int iData1; + int iRes; + int iNext; +}; + +typedef struct Hsh_Int4Man_t_ Hsh_Int4Man_t; +struct Hsh_Int4Man_t_ +{ + Vec_Int_t * vTable; // hash table + Vec_Int_t * vObjs; // hash objects +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Hsh_Int4Obj_t * Hsh_Int4Obj( Hsh_Int4Man_t * p, int iObj ) { return iObj ? (Hsh_Int4Obj_t *)Vec_IntEntryP(p->vObjs, 4*iObj) : NULL; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Hashing data entries composed of nSize integers.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Hsh_Int4Man_t * Hsh_Int4ManStart( int nSize ) +{ + Hsh_Int4Man_t * p; nSize += 100; + p = ABC_CALLOC( Hsh_Int4Man_t, 1 ); + p->vTable = Vec_IntStart( Abc_PrimeCudd(nSize) ); + p->vObjs = Vec_IntAlloc( 4*nSize ); + Vec_IntFill( p->vObjs, 4, 0 ); + return p; +} +static inline void Hsh_Int4ManStop( Hsh_Int4Man_t * p ) +{ + Vec_IntFree( p->vObjs ); + Vec_IntFree( p->vTable ); + ABC_FREE( p ); +} +static inline int Hsh_Int4ManEntryNum( Hsh_Int4Man_t * p ) +{ + return Vec_IntSize(p->vObjs)/4 - 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Hsh_Int4ManHash( int iData0, int iData1, int nTableSize ) +{ + return (4177 * iData0 + 7873 * iData1) % nTableSize; +} +static inline int * Hsh_Int4ManLookup( Hsh_Int4Man_t * p, int iData0, int iData1 ) +{ + Hsh_Int4Obj_t * pObj; + int * pPlace = Vec_IntEntryP( p->vTable, Hsh_Int4ManHash(iData0, iData1, Vec_IntSize(p->vTable)) ); + for ( ; (pObj = Hsh_Int4Obj(p, *pPlace)); pPlace = &pObj->iNext ) + if ( pObj->iData0 == iData0 && pObj->iData1 == iData1 ) + return pPlace; + assert( *pPlace == 0 ); + return pPlace; +} +static inline int Hsh_Int4ManFind( Hsh_Int4Man_t * p, int iData0, int iData1 ) +{ + Hsh_Int4Obj_t * pObj; + int * pPlace = Vec_IntEntryP( p->vTable, Hsh_Int4ManHash(iData0, iData1, Vec_IntSize(p->vTable)) ); + for ( ; (pObj = Hsh_Int4Obj(p, *pPlace)); pPlace = &pObj->iNext ) + if ( pObj->iData0 == iData0 && pObj->iData1 == iData1 ) + return pObj->iRes; + assert( *pPlace == 0 ); + return -1; +} +static inline int Hsh_Int4ManInsert( Hsh_Int4Man_t * p, int iData0, int iData1, int iRes ) +{ + Hsh_Int4Obj_t * pObj; + int i, nObjs, * pPlace; + nObjs = Vec_IntSize(p->vObjs)/4; + if ( nObjs > Vec_IntSize(p->vTable) ) + { + Vec_IntFill( p->vTable, Abc_PrimeCudd(2*Vec_IntSize(p->vTable)), 0 ); + for ( i = 1; i < nObjs; i++ ) + { + pObj = Hsh_Int4Obj( p, i ); + pObj->iNext = 0; + pPlace = Hsh_Int4ManLookup( p, pObj->iData0, pObj->iData1 ); + assert( *pPlace == 0 ); + *pPlace = i; + } + } + pPlace = Hsh_Int4ManLookup( p, iData0, iData1 ); + if ( *pPlace ) + return 0; + assert( *pPlace == 0 ); + *pPlace = nObjs; + Vec_IntPush( p->vObjs, iData0 ); + Vec_IntPush( p->vObjs, iData1 ); + Vec_IntPush( p->vObjs, iRes ); + Vec_IntPush( p->vObjs, 0 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Test procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Hsh_Int4ManHashArrayTest() +{ + Hsh_Int4Man_t * p; + int RetValue; + + p = Hsh_Int4ManStart( 10 ); + + RetValue = Hsh_Int4ManInsert( p, 10, 11, 12 ); + assert( RetValue ); + + RetValue = Hsh_Int4ManInsert( p, 20, 21, 22 ); + assert( RetValue ); + + RetValue = Hsh_Int4ManInsert( p, 10, 11, 12 ); + assert( !RetValue ); + + RetValue = Hsh_Int4ManFind( p, 20, 21 ); + assert( RetValue == 22 ); + + RetValue = Hsh_Int4ManFind( p, 20, 22 ); + assert( RetValue == -1 ); + + Hsh_Int4ManStop( p ); +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +ABC_NAMESPACE_HEADER_END + +#endif + diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 3c59f605..08db89a7 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -77,6 +77,7 @@ struct Bmc_AndPar_t_ { int nStart; // starting timeframe int nFramesMax; // maximum number of timeframes + int nFramesAdd; // the number of additional frames int nConfLimit; // maximum number of conflicts at a node int fLoadCnf; // dynamic CNF loading int fDumpFrames; // dump unrolled timeframes diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index 8dadd619..39b4cb46 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -43,12 +43,333 @@ struct Bmc_Mna_t_ abctime clkStart; // starting time }; +static inline int Gia_ManTerSimInfoGet( unsigned * pInfo, int i ) +{ + return 3 & (pInfo[i >> 4] >> ((i & 15) << 1)); +} +static inline void Gia_ManTerSimInfoSet( unsigned * pInfo, int i, int Value ) +{ + assert( Value >= GIA_ZER && Value <= GIA_UND ); + Value ^= Gia_ManTerSimInfoGet( pInfo, i ); + pInfo[i >> 4] ^= (Value << ((i & 15) << 1)); +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* + Synopsis [Performs ternary simulation of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Bmc_MnaTernary( Gia_Man_t * p, int nFrames, int nFramesAdd, int fVerbose, int * iFirst ) +{ + Vec_Ptr_t * vStates; + unsigned * pState; + int nStateWords = Abc_BitWordNum( 2*Gia_ManCoNum(p) ); + Gia_Obj_t * pObj, * pObjRo; + int f, i, Count[4]; + abctime clk = Abc_Clock(); + Gia_ManConst0(p)->Value = GIA_ZER; + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = GIA_UND; + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = GIA_ZER; + *iFirst = -1; + vStates = Vec_PtrAlloc( 100 ); + for ( f = 0; ; f++ ) + { + // if frames are given, break at frames + if ( nFrames && f == nFrames ) + break; + // if frames are not given, break after nFramesAdd from the first x-valued + if ( !nFrames && *iFirst >= 0 && f == *iFirst + nFramesAdd ) + break; + // aassign CI values + Gia_ManForEachRiRo( p, pObj, pObjRo, i ) + pObjRo->Value = pObj->Value; + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_XsimAndCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); + // compute and save CO values + pState = ABC_ALLOC( unsigned, nStateWords ); + Gia_ManForEachCo( p, pObj, i ) + { + pObj->Value = Gia_XsimNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); + Gia_ManTerSimInfoSet( pState, i, pObj->Value ); + if ( *iFirst == -1 && i < Gia_ManPoNum(p) && pObj->Value == GIA_UND ) + *iFirst = f; + } + Vec_PtrPush( vStates, pState ); + // print statistics + if ( !fVerbose ) + continue; + Count[0] = Count[1] = Count[2] = Count[3] = 0; + Gia_ManForEachRi( p, pObj, i ) + Count[pObj->Value]++; + printf( "%5d : 0 =%7d 1 =%7d x =%7d all =%7d out = %s\n", + f, Count[GIA_ZER], Count[GIA_ONE], Count[GIA_UND], Gia_ManRegNum(p), + Gia_ManPo(p, 0)->Value == GIA_UND ? "x" : "0" ); + } +// assert( Vec_PtrSize(vStates) == nFrames ); + if ( fVerbose ) + printf( "Finished %d frames. First x-valued PO is in frame %d. ", nFrames, *iFirst ); + if ( fVerbose ) + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return vStates; +} + + +/**Function************************************************************* + + Synopsis [Collect AIG nodes for the group of POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_MnaCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, unsigned * pState ) +{ + if ( pObj->fPhase ) + return; + pObj->fPhase = 1; + if ( Gia_ObjIsAnd(pObj) ) + { + Bmc_MnaCollect_rec( p, Gia_ObjFanin0(pObj), vNodes, pState ); + Bmc_MnaCollect_rec( p, Gia_ObjFanin1(pObj), vNodes, pState ); + pObj->Value = Gia_XsimAndCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); + } + else if ( Gia_ObjIsRo(p, pObj) ) + pObj->Value = pState ? Gia_ManTerSimInfoGet( pState, Gia_ObjCioId(Gia_ObjRoToRi(p, pObj)) ) : GIA_ZER; + else if ( Gia_ObjIsPi(p, pObj) ) + pObj->Value = GIA_UND; + else assert( 0 ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); +} +void Bmc_MnaCollect( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, unsigned * pState ) +{ + Gia_Obj_t * pObj; + int i; + Vec_IntClear( vNodes ); + Gia_ManConst0(p)->fPhase = 1; + Gia_ManConst0(p)->Value = GIA_ZER; + Gia_ManForEachObjVec( vCos, p, pObj, i ) + { + assert( Gia_ObjIsCo(pObj) ); + Bmc_MnaCollect_rec( p, Gia_ObjFanin0(pObj), vNodes, pState ); + pObj->Value = Gia_XsimNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); + assert( pObj->Value == GIA_UND ); + } +} + +/**Function************************************************************* + + Synopsis [Select related logic cones for the COs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_MnaSelect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves ) +{ + if ( !pObj->fPhase ) + return; + pObj->fPhase = 0; + assert( pObj->Value == GIA_UND ); + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjFanin0(pObj)->Value == GIA_UND ) + Bmc_MnaSelect_rec( p, Gia_ObjFanin0(pObj), vLeaves ); + else assert( Gia_ObjFanin0(pObj)->Value + Gia_ObjFaninC0(pObj) == GIA_ONE ); + if ( Gia_ObjFanin1(pObj)->Value == GIA_UND ) + Bmc_MnaSelect_rec( p, Gia_ObjFanin1(pObj), vLeaves ); + else assert( Gia_ObjFanin1(pObj)->Value + Gia_ObjFaninC1(pObj) == GIA_ONE ); + } + else if ( Gia_ObjIsRo(p, pObj) ) + Vec_IntPush( vLeaves, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) ); +} +void Bmc_MnaSelect( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Vec_Int_t * vLeaves ) +{ + Gia_Obj_t * pObj; + int i; + Vec_IntClear( vLeaves ); + Gia_ManForEachObjVec( vCos, p, pObj, i ) + Bmc_MnaSelect_rec( p, Gia_ObjFanin0(pObj), vLeaves ); + Gia_ManConst0(p)->fPhase = 0; + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->fPhase = 0; +} + +/**Function************************************************************* + + Synopsis [Build AIG for the selected cones.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_MnaBuild_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew, Vec_Int_t * vMap ) +{ + if ( !pObj->fPhase ) + return; + pObj->fPhase = 0; + assert( pObj->Value == GIA_UND ); + if ( Gia_ObjIsAnd(pObj) ) + { + int iLit0 = 1, iLit1 = 1; + if ( Gia_ObjFanin0(pObj)->Value == GIA_UND ) + Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap ); + if ( Gia_ObjFanin1(pObj)->Value == GIA_UND ) + Bmc_MnaBuild_rec( p, Gia_ObjFanin1(pObj), pNew, vMap ); + if ( Gia_ObjFanin0(pObj)->Value == GIA_UND ) + iLit0 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) ); + if ( Gia_ObjFanin1(pObj)->Value == GIA_UND ) + iLit1 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId1p(p, pObj)), Gia_ObjFaninC1(pObj) ); + Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManHashAnd(pNew, iLit0, iLit1) ); + } + else if ( Gia_ObjIsRo(p, pObj) ) + assert( Vec_IntEntry(vMap, Gia_ObjId(p, pObj)) != -1 ); + else if ( Gia_ObjIsPi(p, pObj) ) + Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) ); + else assert( 0 ); +} +void Bmc_MnaBuild( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Gia_Man_t * pNew, Vec_Int_t * vMap ) +{ + Gia_Obj_t * pObj; + int i, iLit; + Gia_ManForEachObjVec( vCos, p, pObj, i ) + { + assert( Gia_ObjIsCo(pObj) ); + Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap ); + iLit = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) ); + Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), iLit ); + } + Gia_ManConst0(p)->fPhase = 0; + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->fPhase = 0; +} + + +/**Function************************************************************* + + Synopsis [Compute the first non-trivial timeframe.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd, int fVerbose ) +{ + Gia_Obj_t * pObj; + Gia_Man_t * pNew, * pTemp; + Vec_Ptr_t * vStates, * vBegins; + Vec_Int_t * vRoots, * vCone, * vLeaves, * vMap; + unsigned * pStateF, * pStateP; + int f, i, iFirst; + Gia_ManCleanPhase( pGia ); + vCone = Vec_IntAlloc( 1000 ); + vLeaves = Vec_IntAlloc( 1000 ); + // perform ternary simulation + vStates = Bmc_MnaTernary( pGia, nFramesMax, nFramesAdd, fVerbose, &iFirst ); + // go backward + vBegins = Vec_PtrStart( Vec_PtrSize(vStates) ); + for ( f = Vec_PtrSize(vStates) - 1; f >= 0; f-- ) + { + // get ternary states + pStateF = (unsigned *)Vec_PtrEntry(vStates, f); + pStateP = f ? (unsigned *)Vec_PtrEntry(vStates, f-1) : 0; + // collect roots of this frame + vRoots = Vec_IntAlloc( 100 ); + Gia_ManForEachPo( pGia, pObj, i ) + if ( Gia_ManTerSimInfoGet( pStateF, Gia_ObjCioId(pObj) ) == GIA_UND ) + Vec_IntPush( vRoots, Gia_ObjId(pGia, pObj) ); + // add leaves from the previous frame + Vec_IntAppend( vRoots, vLeaves ); + Vec_PtrWriteEntry( vBegins, f, vRoots ); + // find the cone + Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone + Bmc_MnaSelect( pGia, vRoots, vCone, vLeaves ); // computes vLeaves + if ( fVerbose ) + printf( "Frame %4d : Roots = %6d Leaves = %6d Cone = %6d\n", + f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) ); + if ( Vec_IntSize(vLeaves) == 0 ) + break; + // it is possible that some of the POs are still ternary... + } + assert( f >= 0 ); + // go forward + vMap = Vec_IntStartFull( Gia_ManObjNum(pGia) ); + pNew = Gia_ManStart( 10000 ); + pNew->pName = Abc_UtilStrsav( pGia->pName ); + Gia_ManHashStart( pNew ); + for ( f = 0; f < Vec_PtrSize(vStates); f++ ) + { + vRoots = (Vec_Int_t *)Vec_PtrEntry( vBegins, f ); + if ( vRoots == NULL ) + { + Gia_ManForEachPo( pGia, pObj, i ) + Gia_ManAppendCo( pNew, 0 ); + continue; + } + // get ternary states + pStateF = (unsigned *)Vec_PtrEntry(vStates, f); + pStateP = f ? (unsigned *)Vec_PtrEntry(vStates, f-1) : 0; + // clean POs + Gia_ManForEachPo( pGia, pObj, i ) + Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pObj), 0 ); + // find the cone + Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone + Bmc_MnaBuild( pGia, vRoots, vCone, pNew, vMap ); // computes pNew + if ( fVerbose ) + printf( "Frame %4d : Roots = %6d Leaves = %6d Cone = %6d\n", + f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) ); + // create POs + Gia_ManForEachPo( pGia, pObj, i ) + Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) ); + // set a new map + Gia_ManForEachObjVec( vRoots, pGia, pObj, i ) + if ( Gia_ObjIsRi(pGia, pObj) ) + Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, Gia_ObjRiToRo(pGia, pObj)), Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) ); +// else if ( Gia_ObjIsPo(pGia, pObj) ) +// Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) ); +// else assert( 0 ); + } + Gia_ManHashStop( pNew ); + Vec_VecFree( (Vec_Vec_t *)vBegins ); + Vec_PtrFreeFree( vStates ); + Vec_IntFree( vLeaves ); + Vec_IntFree( vCone ); + Vec_IntFree( vMap ); + // cleanup +// Gia_ManPrintStats( pNew, NULL ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); +// Gia_ManPrintStats( pNew, NULL ); + return pNew; +} + + + +/**Function************************************************************* + Synopsis [BMC manager manipulation.] Description [] @@ -255,7 +576,7 @@ void Gia_ManBmcAddCone_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj ) else Vec_IntPush( p->vInputs, iObj ); } -void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart ) +void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart, int iStop ) { Gia_Obj_t * pObj; int i; @@ -263,7 +584,7 @@ void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart ) Vec_IntClear( p->vInputs ); Vec_IntClear( p->vOutputs ); Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 ); - for ( i = iStart; i < Gia_ManPoNum(p->pFrames); i++ ) + for ( i = iStart; i < iStop; i++ ) { pObj = Gia_ManPo(p->pFrames, i); if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) ) @@ -289,10 +610,10 @@ void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart ) SeeAlso [] ***********************************************************************/ -int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart ) +int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart, int iStop ) { int i; - for ( i = iStart; i < Gia_ManPoNum(pFrames); i++ ) + for ( i = iStart; i < iStop; i++ ) if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) ) return 0; return 1; @@ -309,24 +630,25 @@ int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart ) SeeAlso [] ***********************************************************************/ -int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) +int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { Unr_Man_t * pUnroll; - Bmc_Mna_t * p = Bmc_MnaAlloc(); + Bmc_Mna_t * p; int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY; int f, i=0, Lit, status, RetValue = -2; + p = Bmc_MnaAlloc(); pUnroll = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose ); for ( f = 0; f < nFramesMax; f++ ) { p->pFrames = Unr_ManUnrollFrame( pUnroll, f ); - if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia) ) ) + if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) ) { // create another slice - Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia) ); + Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ); // create CNF in the SAT solver Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs ); // try solving the outputs - for ( i = f * Gia_ManPoNum(pGia); i < Gia_ManPoNum(p->pFrames); i++ ) + for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ ) { Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i); if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) ) @@ -380,6 +702,91 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) return RetValue; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) +{ + Bmc_Mna_t * p; + int nFramesMax, f, i=0, Lit, status, RetValue = -2; + p = Bmc_MnaAlloc(); + p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose ); + nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia); + if ( pPars->fVerbose ) + printf( "Performed unfolding for %d frames.\n", nFramesMax ); + if ( pPars->fVerbose ) + Gia_ManPrintStats( p->pFrames, NULL ); + for ( f = 0; f < nFramesMax; f++ ) + { + if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) ) + { + // create another slice + Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ); + // create CNF in the SAT solver + Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs ); + // try solving the outputs + for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ ) + { + Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i); + if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) ) + continue; + Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 ); + status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( status == l_False ) // unsat + continue; + if ( status == l_True ) // sat + RetValue = 0; + if ( status == l_Undef ) // undecided + RetValue = -1; + break; + } + // report statistics + if ( pPars->fVerbose ) + { + printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ", + f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames), + p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes), + sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); + } + } + if ( RetValue != -2 ) + { + if ( RetValue == -1 ) + printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f ); + else + { + printf( "Output %d of miter \"%s\" was asserted in frame %d. ", + i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f ); + Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); + } + break; + } + } + if ( RetValue == -2 ) + RetValue = -1; + // dump unfolded frames + if ( pPars->fDumpFrames ) + { + p->pFrames = Gia_ManCleanup( p->pFrames ); + Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 ); + printf( "Dumped unfolded frames into file \"frames.aig\".\n" ); + Gia_ManStop( p->pFrames ); + } + // cleanup + Gia_ManStop( p->pFrames ); + Bmc_MnaFree( p ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |