summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c17
-rw-r--r--src/misc/vec/vecHsh4.h208
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcBmcAnd.c425
4 files changed, 640 insertions, 11 deletions
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 ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-04 14:37:04 +0000