summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-11-15 16:00:29 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-11-15 16:00:29 -0800
commita0052e22b43ff9d0125ca8e71f96589226e44e42 (patch)
tree01edb8daa0a79a466e34e55585a0d1102db6b977
parentc2e467d55b188cb1fa5db534a23a4dd6e8291078 (diff)
downloadabc-a0052e22b43ff9d0125ca8e71f96589226e44e42.tar.gz
abc-a0052e22b43ff9d0125ca8e71f96589226e44e42.tar.bz2
abc-a0052e22b43ff9d0125ca8e71f96589226e44e42.zip
Added switch 'cexcut -m' to generate bad states for all frames after G.
-rw-r--r--src/aig/gia/gia.h3
-rw-r--r--src/aig/gia/giaDup.c6
-rw-r--r--src/base/abci/abc.c26
-rw-r--r--src/misc/util/utilCex.c4
-rw-r--r--src/sat/bmc/bmc.h4
-rw-r--r--src/sat/bmc/bmcCexCut.c145
6 files changed, 164 insertions, 24 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d261e433..9d361fe8 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -316,6 +316,9 @@ 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_Obj2Lit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit(Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj)); }
+static inline Gia_Obj_t * Gia_Lit2Obj( Gia_Man_t * p, int iLit ) { return Gia_NotCond(Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit)); }
+
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) ); }
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index eddbd320..3b8980af 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1233,7 +1233,7 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
// there is no flops in p2
assert( Gia_ManRegNum(p2) == 0 );
// there is only one PO in p2
- assert( Gia_ManPoNum(p2) == 1 );
+// assert( Gia_ManPoNum(p2) == 1 );
// input count of p2 is equal to flop count of p1
assert( Gia_ManPiNum(p2) == Gia_ManRegNum(p1) );
@@ -1255,8 +1255,8 @@ Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
Gia_ManForEachAnd( p2, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
// add property output
- pObj = Gia_ManPo( p2, 0 );
- Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ Gia_ManForEachPo( p2, pObj, i )
+ Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
// add flop inputs
Gia_ManForEachRi( p1, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b490d3e3..89d1c6dd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22566,6 +22566,9 @@ int Abc_CommandCexLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
}
ABC_FREE( pAbc->pCex );
pAbc->pCex = Abc_CexDup( pAbc->pCex2, -1 );
+ // update status
+ pAbc->nFrames = pAbc->pCex2->iFrame;
+ pAbc->Status = 0;
return 0;
usage:
@@ -22590,13 +22593,14 @@ usage:
int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c;
- int iFrStart = 0;
- int iFrStop = ABC_INFINITY;
- int fCombOnly = 0;
- int fUseOne = 0;
- int fVerbose = 0;
+ int iFrStart = 0;
+ int iFrStop = ABC_INFINITY;
+ int fCombOnly = 0;
+ int fUseOne = 0;
+ int fAllFrames = 0;
+ int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FGcnvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FGcnmvh" ) ) != EOF )
{
switch ( c )
{
@@ -22628,6 +22632,9 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'n':
fUseOne ^= 1;
break;
+ case 'm':
+ fAllFrames ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -22662,7 +22669,7 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
Abc_Ntk_t * pNtkNew;
Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
- Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fCombOnly, fUseOne, fVerbose );
+ Aig_Man_t * pAigNew = Bmc_AigTargetStates( pAig, pAbc->pCex, iFrStart, iFrStop, fCombOnly, fUseOne, fAllFrames, fVerbose );
Aig_ManStop( pAig );
if ( pAigNew == NULL )
{
@@ -22687,12 +22694,13 @@ int Abc_CommandCexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: cexcut [-FG num] [-cvh]\n" );
+ Abc_Print( -2, "usage: cexcut [-FG num] [-cnmvh]\n" );
Abc_Print( -2, "\t creates logic for bad states using the current CEX\n" );
Abc_Print( -2, "\t-F num : 0-based number of the starting frame [default = %d]\n", iFrStart );
Abc_Print( -2, "\t-G num : 0-based number of the ending frame [default = %d]\n", iFrStop );
Abc_Print( -2, "\t-c : toggle outputting unate combinational circuit [default = %s]\n", fCombOnly? "yes": "no" );
Abc_Print( -2, "\t-n : toggle generating only one bad state [default = %s]\n", fUseOne? "yes": "no" );
+ Abc_Print( -2, "\t-m : toggle generating bad states for all frames after G [default = %s]\n", fAllFrames? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -22764,7 +22772,7 @@ int Abc_CommandCexMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "There is no saved cex.\n");
return 0;
}
- if ( iFrStop - iFrStart < pAbc->pCex->iFrame )
+ if ( iFrStop - iFrStart + pAbc->pCex->iPo < pAbc->pCex->iFrame )
{
Abc_Print( 1, "Current CEX does not allow to shorten the saved CEX.\n");
return 0;
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index edb246b9..01afd489 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -202,9 +202,9 @@ Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int i
assert( iFrBeg <= iFrEnd );
assert( pCex->nPis == pPart->nPis );
- assert( iFrEnd - iFrBeg >= pPart->iFrame );
+ assert( iFrEnd - iFrBeg + pPart->iPo >= pPart->iFrame );
- nFramesGain = (iFrEnd - iFrBeg) - pPart->iFrame;
+ nFramesGain = iFrEnd - iFrBeg + pPart->iPo - pPart->iFrame;
pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain );
pNew->iPo = pCex->iPo;
pNew->iFrame = pCex->iFrame - nFramesGain;
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 0e37656e..7cc5637b 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -75,8 +75,8 @@ extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFra
extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
/*=== bmcCexCut.c ==========================================================*/
-extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fVerbose );
-extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fVerbose );
+extern Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
+extern Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
/*=== bmcCexMin.c ==========================================================*/
extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
diff --git a/src/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c
index 7eafe492..3ce63459 100644
--- a/src/sat/bmc/bmcCexCut.c
+++ b/src/sat/bmc/bmcCexCut.c
@@ -225,7 +225,135 @@ Gia_Man_t * Bmc_GiaGenerateGiaOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t **
/**Function*************************************************************
- Synopsis []
+ Synopsis [Generates all frames from G to the last one.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Bmc_GiaGenerateGiaAllFrames( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd )
+{
+ Vec_Bit_t * vInitEnd;
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+ int f, i, k, iBitOld, iBit = 0, fCompl0, fCompl1;
+
+ // skip trough the first iFrEnd frames
+ Gia_ManCleanMark0(p);
+ Gia_ManForEachRo( p, pObj, k )
+ pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+ *pvInits = Vec_BitStart( Gia_ManRegNum(p) );
+ for ( i = 0; i < iFrEnd; i++ )
+ {
+ // remember values in frame iFrBeg
+ if ( i == iFrBeg )
+ Gia_ManForEachRo( p, pObjRo, k )
+ if ( pObjRo->fMark0 )
+ Vec_BitWriteEntry( *pvInits, k, 1 );
+ // simulate other values
+ Gia_ManForEachPi( p, pObj, k )
+ pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+ Gia_ManForEachAnd( p, pObj, k )
+ pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
+ (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+ Gia_ManForEachCo( p, pObj, k )
+ pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+ pObjRo->fMark0 = pObjRi->fMark0;
+ }
+ assert( i == iFrEnd );
+ vInitEnd = Vec_BitStart( Gia_ManRegNum(p) );
+ Gia_ManForEachRo( p, pObjRo, k )
+ if ( pObjRo->fMark0 )
+ Vec_BitWriteEntry( vInitEnd, k, 1 );
+
+ // create new AIG manager
+ pNew = Gia_ManStart( 10000 );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ Gia_ManForEachRo( p, pObjRo, k )
+ Gia_ManAppendCi(pNew);
+ Gia_ManHashStart( pNew );
+
+ Gia_ManConst0(p)->Value = 1;
+ Gia_ManForEachPi( p, pObj, k )
+ pObj->Value = 1;
+
+ iBitOld = iBit;
+ for ( f = iFrEnd; f <= pCex->iFrame; f++ )
+ {
+ // set up correct init state
+ Gia_ManForEachRo( p, pObjRo, k )
+ pObjRo->fMark0 = Vec_BitEntry( vInitEnd, k );
+ // simulate it for a few frames
+ iBit = iBitOld;
+ for ( i = iFrEnd; i < f; i++ )
+ {
+ Gia_ManForEachPi( p, pObj, k )
+ pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+ Gia_ManForEachAnd( p, pObj, k )
+ pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
+ (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+ Gia_ManForEachCo( p, pObj, k )
+ pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+ pObjRo->fMark0 = pObjRi->fMark0;
+ }
+ // start creating values
+ Gia_ManForEachRo( p, pObjRo, k )
+ pObjRo->Value = Abc_LitNotCond( Gia_Obj2Lit(pNew, Gia_ManPi(pNew, k)), !pObjRo->fMark0 );
+ for ( i = f; i <= pCex->iFrame; i++ )
+ {
+ Gia_ManForEachPi( p, pObj, k )
+ pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
+ Gia_ManForEachAnd( p, pObj, k )
+ {
+ fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
+ pObj->fMark0 = fCompl0 & fCompl1;
+ if ( pObj->fMark0 )
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+ else if ( !fCompl0 && !fCompl1 )
+ pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+ else if ( !fCompl0 )
+ pObj->Value = Gia_ObjFanin0(pObj)->Value;
+ else if ( !fCompl1 )
+ pObj->Value = Gia_ObjFanin1(pObj)->Value;
+ else assert( 0 );
+ assert( pObj->Value > 0 );
+ }
+ Gia_ManForEachCo( p, pObj, k )
+ {
+ pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+ pObj->Value = Gia_ObjFanin0(pObj)->Value;
+ assert( pObj->Value > 0 );
+ }
+ if ( i == pCex->iFrame )
+ break;
+ Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+ {
+ pObjRo->fMark0 = pObjRi->fMark0;
+ pObjRo->Value = pObjRi->Value;
+ }
+ }
+ assert( iBit == pCex->nBits );
+ // create PO
+ Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value );
+ }
+ Gia_ManHashStop( pNew );
+ Vec_BitFree( vInitEnd );
+
+ // cleanup
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Generates one frame.]
Description []
@@ -234,7 +362,7 @@ Gia_Man_t * Bmc_GiaGenerateGiaOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t **
SeeAlso []
***********************************************************************/
-Gia_Man_t * Bmc_GiaGenerateGiaAll( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd )
+Gia_Man_t * Bmc_GiaGenerateGiaAllOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj, * pObjRo, * pObjRi;
@@ -319,7 +447,6 @@ Gia_Man_t * Bmc_GiaGenerateGiaAll( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t **
return pNew;
}
-
/**Function*************************************************************
Synopsis [Generate GIA for target bad states.]
@@ -331,7 +458,7 @@ Gia_Man_t * Bmc_GiaGenerateGiaAll( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t **
SeeAlso []
***********************************************************************/
-Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fVerbose )
+Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
Vec_Bit_t * vInitNew;
@@ -352,8 +479,10 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
if ( fUseOne )
pNew = Bmc_GiaGenerateGiaOne( p, pCex, &vInitNew, iFrBeg, iFrEnd );
- else
- pNew = Bmc_GiaGenerateGiaAll( p, pCex, &vInitNew, iFrBeg, iFrEnd );
+ else if ( fAllFrames )
+ pNew = Bmc_GiaGenerateGiaAllFrames( p, pCex, &vInitNew, iFrBeg, iFrEnd );
+ else
+ pNew = Bmc_GiaGenerateGiaAllOne( p, pCex, &vInitNew, iFrBeg, iFrEnd );
if ( !fCombOnly )
{
@@ -381,7 +510,7 @@ Gia_Man_t * Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
SeeAlso []
***********************************************************************/
-Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fVerbose )
+Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose )
{
Aig_Man_t * pAig;
Gia_Man_t * pGia, * pRes;
@@ -392,7 +521,7 @@ Aig_Man_t * Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, in
Gia_ManStop( pGia );
return NULL;
}
- pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fUseOne, fVerbose );
+ pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fUseOne, fAllFrames, fVerbose );
Gia_ManStop( pGia );
pAig = Gia_ManToAigSimple( pRes );
Gia_ManStop( pRes );