Skip to content

A
abc
Commit dd867b40 by Alan Mishchenko
Options

Added transformation of CEX after 'fix_aig' and checking of transformed CEXes using 'testcex -a'.

parent df418d6c
Showing with 129 additions and 24 deletions
src/base/abc/abcLatch.c
......@@ -712,6 +712,57 @@ Abc_Ntk_t * Abc_NtkCRetime( Abc_Ntk_t * pNtk, int fVerbose )
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Resimulates CEX and return the ID of the PO that failed.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkVerifyCex( Abc_Ntk_t * pNtk, Abc_Cex_t * p )
{
Abc_Obj_t * pObj;
int RetValue, i, k, iBit = 0;
assert( Abc_NtkIsStrash(pNtk) );
assert( p->nPis == Abc_NtkPiNum(pNtk) );
assert( p->nRegs == Abc_NtkLatchNum(pNtk) );
Abc_NtkCleanMarkC( pNtk );
Abc_AigConst1(pNtk)->fMarkC = 1;
// initialize flops
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjFanout0(pObj)->fMarkC = Abc_InfoHasBit(p->pData, iBit++);
// simulate timeframes
for ( i = 0; i <= p->iFrame; i++ )
{
Abc_NtkForEachPi( pNtk, pObj, k )
pObj->fMarkC = Abc_InfoHasBit(p->pData, iBit++);
Abc_NtkForEachNode( pNtk, pObj, k )
pObj->fMarkC = (Abc_ObjFanin0(pObj)->fMarkC ^ Abc_ObjFaninC0(pObj)) &
(Abc_ObjFanin1(pObj)->fMarkC ^ Abc_ObjFaninC1(pObj));
Abc_NtkForEachCo( pNtk, pObj, k )
pObj->fMarkC = Abc_ObjFanin0(pObj)->fMarkC ^ Abc_ObjFaninC0(pObj);
Abc_NtkForEachLatch( pNtk, pObj, k )
Abc_ObjFanout0(pObj)->fMarkC = Abc_ObjFanin0(pObj)->fMarkC;
}
assert( iBit == p->nBits );
// figure out the number of failed output
RetValue = -1;
Abc_NtkForEachPo( pNtk, pObj, i )
{
if ( pObj->fMarkC )
{
RetValue = i;
break;
}
}
Abc_NtkCleanMarkC( pNtk );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/abci/abc.c
......@@ -16185,13 +16185,16 @@ usage:
int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c;
int c, fUseCex = 0;
// set defaults
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
{
switch ( c )
{
case 'c':
fUseCex ^= 1;
break;
case 'h':
goto usage;
default:
......@@ -16205,6 +16208,35 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( fUseCex )
{
char * pInit;
Abc_Cex_t * pTemp;
int k, nFlopsX = 0;
if ( pAbc->pCex == NULL )
{
Abc_Print( -1, "Current CEX is not available.\n" );
return 1;
}
pInit = Abc_NtkCollectLatchValuesStr( pAbc->pNtkCur );
// count the number of X-valued flops
for ( k = 0; k < Abc_NtkLatchNum(pAbc->pNtkCur); k++ )
nFlopsX += (int)(pInit[k] == 'x');
// compare this value
if ( Abc_NtkPiNum(pNtk) + nFlopsX != pAbc->pCex->nPis )
{
Abc_Print( -1, "The number of PIs (%d) plus X-valued flops (%d) in the original network does not match the number of PIs in the current CEX (%d).\n",
Abc_NtkPiNum(pNtk), Abc_NtkLatchNum(pNtk), pAbc->pCex->nPis );
return 1;
}
pAbc->pCex = Abc_CexTransformUndc( pTemp = pAbc->pCex, pInit );
assert( pAbc->pCex->nPis == Abc_NtkPiNum(pAbc->pNtkCur) );
assert( pAbc->pCex->nRegs == Abc_NtkLatchNum(pAbc->pNtkCur) );
Abc_CexFree( pTemp );
ABC_FREE( pInit );
return 0;
}
if ( Abc_NtkIsComb(pNtk) )
{
Abc_Print( -1, "The current network is combinational.\n" );
......@@ -16222,8 +16254,9 @@ int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: undc [-h]\n" );
Abc_Print( -2, "usage: undc [-ch]\n" );
Abc_Print( -2, "\t converts latches with DC init values into free PIs\n" );
Abc_Print( -2, "\t-c : toggles transforming CEX after \"logic;undc;st;zero\" [default = %s]\n", fUseCex? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
......@@ -23617,28 +23650,17 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
else if ( Abc_NtkPiNum(pNtk) != pAbc->pCex->nPis )
Abc_Print( 1, "Main AIG: The number of PIs (%d) is different from cex (%d).\n", Abc_NtkPiNum(pNtk), pAbc->pCex->nPis );
// else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs )
// Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs );
// else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo )
// Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
else
{
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
// if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
extern int Abc_NtkVerifyCex( Abc_Ntk_t * pNtk, Abc_Cex_t * p );
int iPoOld = pAbc->pCex->iPo;
pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pGia, pAbc->pCex, nOutputs );
pAbc->pCex->iPo = Abc_NtkVerifyCex( pNtk, pAbc->pCex );
if ( pAbc->pCex->iPo == -1 )
{
// pAbc->pCex->iPo = iPoOld;
Abc_Print( 1, "Main AIG: The cex does not fail any outputs.\n" );
}
else if ( iPoOld != pAbc->pCex->iPo )
Abc_Print( 1, "Main AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
else
Abc_Print( 1, "Main AIG: The cex is correct.\n" );
Gia_ManStop( pGia );
Aig_ManStop( pAig );
}
}
else
......@@ -23648,20 +23670,12 @@ int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "And AIG: There is no current network.\n");
else if ( Gia_ManPiNum(pAbc->pGia) != pAbc->pCex->nPis )
Abc_Print( 1, "And AIG: The number of PIs (%d) is different from cex (%d).\n", Gia_ManPiNum(pAbc->pGia), pAbc->pCex->nPis );
// else if ( Gia_ManRegNum(pAbc->pGia) != pAbc->pCex->nRegs )
// Abc_Print( 1, "And AIG: The number of registers (%d) is different from cex (%d).\n", Gia_ManRegNum(pAbc->pGia), pAbc->pCex->nRegs );
// else if ( Gia_ManPoNum(pAbc->pGia) <= pAbc->pCex->iPo )
// Abc_Print( 1, "And AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo );
else
{
// if ( !Gia_ManVerifyCex( pAbc->pGia, pAbc->pCex, 0 ) )
int iPoOld = pAbc->pCex->iPo;
pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pAbc->pGia, pAbc->pCex, nOutputs );
if ( pAbc->pCex->iPo == -1 )
{
// pAbc->pCex->iPo = iPoOld;
Abc_Print( 1, "And AIG: The cex does not fail any outputs.\n" );
}
else if ( iPoOld != pAbc->pCex->iPo )
Abc_Print( 1, "And AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
else
src/misc/util/utilCex.c
......@@ -436,6 +436,45 @@ Abc_Cex_t * Abc_CexTransformTempor( Abc_Cex_t * p, int nPisOld, int nPosOld, int
/**Function*************************************************************
Synopsis [Transform CEX after "logic; undc; st; zero".]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Abc_CexTransformUndc( Abc_Cex_t * p, char * pInit )
{
Abc_Cex_t * pCex;
int nFlops = strlen(pInit);
int i, f, iBit, iAddPi = 0, nAddPis = 0;
// count how many flops got a new PI
for ( i = 0; i < nFlops; i++ )
nAddPis += (int)(pInit[i] == 'x');
// create new CEX
pCex = Abc_CexAlloc( nFlops, p->nPis - nAddPis, p->iFrame + 1 );
pCex->iPo = p->iPo;
pCex->iFrame = p->iFrame;
for ( iBit = 0; iBit < nFlops; iBit++ )
{
if ( pInit[iBit] == '1' || (pInit[iBit] == 'x' && Abc_InfoHasBit(p->pData, p->nRegs + p->nPis - nAddPis + iAddPi)) )
Abc_InfoSetBit( pCex->pData, iBit );
iAddPi += (int)(pInit[iBit] == 'x');
}
assert( iAddPi == nAddPis );
// add timeframes
for ( f = 0; f <= p->iFrame; f++ )
for ( i = 0; i < pCex->nPis; i++, iBit++ )
if ( Abc_InfoHasBit(p->pData, p->nRegs + p->nPis * f + i) )
Abc_InfoSetBit( pCex->pData, iBit );
assert( iBit == pCex->nBits );
return pCex;
}
/**Function*************************************************************
Synopsis [Derives permuted CEX using permutation of its inputs.]
Description []
......
src/misc/util/utilCex.h
......@@ -70,6 +70,7 @@ extern void Abc_CexFreeP( Abc_Cex_t ** p );
extern void Abc_CexFree( Abc_Cex_t * p );
extern Abc_Cex_t * Abc_CexTransformPhase( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld );
extern Abc_Cex_t * Abc_CexTransformTempor( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld );
extern Abc_Cex_t * Abc_CexTransformUndc( Abc_Cex_t * p, char * pInit );
extern Abc_Cex_t * Abc_CexPermute( Abc_Cex_t * p, Vec_Int_t * vMapOld2New );
extern Abc_Cex_t * Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t * vPermNew );
extern int Abc_CexCountOnes( Abc_Cex_t * p );
......
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