Skip to content

A
abc
Commit a0052e22 by Alan Mishchenko
Options

Added switch 'cexcut -m' to generate bad states for all frames after G.

parent c2e467d5
Showing with 164 additions and 24 deletions
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) ); }
......
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) );
......
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;
......
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;
......
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 );
......
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 );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment