luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Added switches '-c' and '-n' to 'init'.

This commit is contained in:
Alan Mishchenko 2014-11-02 17:35:47 -08:00
parent 91885a6298
commit b4cf2f7448
3 changed files with 113 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

64
src/aig/saig/saigDup.c
View File

@ -304,6 +304,70 @@ int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
return RetValue;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManVerifyCexNoClear( Aig_Man_t * pAig, Abc_Cex_t * p )
{
Aig_Obj_t * pObj, * pObjRi, * pObjRo;
int RetValue, i, k, iBit = 0;
Aig_ManCleanMarkB(pAig);
Aig_ManConst1(pAig)->fMarkB = 1;
Saig_ManForEachLo( pAig, pObj, i )
pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
for ( i = 0; i <= p->iFrame; i++ )
{
Saig_ManForEachPi( pAig, pObj, k )
pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
Aig_ManForEachNode( pAig, pObj, k )
pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
(Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
Aig_ManForEachCo( pAig, pObj, k )
pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
if ( i == p->iFrame )
break;
Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
pObjRo->fMarkB = pObjRi->fMarkB;
}
assert( iBit == p->nBits );
RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
//Aig_ManCleanMarkB(pAig);
return RetValue;
}
Vec_Int_t * Saig_ManReturnFailingState( Aig_Man_t * pAig, Abc_Cex_t * p, int fNextOne )
{
Aig_Obj_t * pObj;
Vec_Int_t * vState;
int i, RetValue = Saig_ManVerifyCexNoClear( pAig, p );
if ( RetValue == 0 )
{
Aig_ManCleanMarkB(pAig);
printf( "CEX does fail the given sequential miter.\n" );
return NULL;
}
vState = Vec_IntAlloc( Aig_ManRegNum(pAig) );
if ( fNextOne )
{
Saig_ManForEachLi( pAig, pObj, i )
Vec_IntPush( vState, pObj->fMarkB );
}
else
{
Saig_ManForEachLo( pAig, pObj, i )
Vec_IntPush( vState, pObj->fMarkB );
}
Aig_ManCleanMarkB(pAig);
return vState;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]

60
src/base/abci/abc.c
View File

@ -16493,20 +16493,17 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
Abc_Obj_t * pObj;
char * pInitStr = NULL;
int fZeros = 0;
int fOnes = 0;
int fRandom = 0;
int fDontCare = 0;
int fUseCexCs = 0;
int fUseCexNs = 0;
int c, i;
int fZeros;
int fOnes;
int fRandom;
int fDontCare;
char * pInitStr;
// set defaults
fZeros = 0;
fOnes = 0;
fRandom = 0;
fDontCare = 0;
pInitStr = NULL;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Szordh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Szordcnh" ) ) != EOF )
{
switch ( c )
{
@ -16531,6 +16528,12 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDontCare ^= 1;
break;
case 'c':
fUseCexCs ^= 1;
break;
case 'n':
fUseCexNs ^= 1;
break;
case 'h':
goto usage;
default:
@ -16591,17 +16594,50 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_LatchSetInitDc( pObj );
}
else if ( fUseCexCs || fUseCexNs )
{
extern Vec_Int_t * Saig_ManReturnFailingState( Aig_Man_t * pMan, Abc_Cex_t * p, int fNextOne );
Aig_Man_t * pMan;
Vec_Int_t * vFailState;
if ( fUseCexCs && fUseCexNs )
{
Abc_Print( -1, "The two options (-c and -n) are incompatible.\n" );
return 0;
}
if ( !Abc_NtkIsStrash(pNtk) )
{
Abc_Print( -1, "The current network should be an AIG.\n" );
return 0;
}
if ( pAbc->pCex == NULL )
{
Abc_Print( -1, "The current CEX is not available.\n" );
return 0;
}
pMan = Abc_NtkToDar( pNtk, 0, 1 );
vFailState = Saig_ManReturnFailingState( pMan, pAbc->pCex, fUseCexNs );
//Vec_IntPrint( vFailState );
Aig_ManStop( pMan );
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( Vec_IntEntry( vFailState, i ) )
Abc_LatchSetInit1( pObj );
else
Abc_LatchSetInit0( pObj );
Vec_IntFree( vFailState );
}
else
Abc_Print( -1, "The initial states remain unchanged.\n" );
return 0;
usage:
Abc_Print( -2, "usage: init [-zordh] [-S <init_string>]\n" );
Abc_Print( -2, "usage: init [-zordcnh] [-S <init_string>]\n" );
Abc_Print( -2, "\t resets initial states of all latches\n" );
Abc_Print( -2, "\t-z : set zeros initial states [default = %s]\n", fZeros? "yes": "no" );
Abc_Print( -2, "\t-o : set ones initial states [default = %s]\n", fOnes? "yes": "no" );
Abc_Print( -2, "\t-d : set don't-care initial states [default = %s]\n", fDontCare? "yes": "no" );
Abc_Print( -2, "\t-r : set random initial states [default = %s]\n", fRandom? "yes": "no" );
Abc_Print( -2, "\t-c : set failure current state from the CEX (and run \"zero\") [default = %s]\n", fUseCexCs? "yes": "no" );
Abc_Print( -2, "\t-n : set next state after failure from the CEX (and run \"zero\") [default = %s]\n", fUseCexNs? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t-S str : (optional) initial state [default = unused]\n" );
return 1;

2
src/base/abci/abcDar.c
View File

@ -2307,7 +2307,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
if ( pPars->nDropOuts )
Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
}
Abc_Print( 1, " after %d frames", pPars->iFrame );
Abc_Print( 1, " after %d frames", pPars->iFrame+2 );
Abc_Print( 1, ". " );
}
}