diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-17 12:21:48 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-06-17 12:21:48 -0700 |
commit | dd867b404acec3d7e22663189bdf1108435a381d (patch) | |
tree | 1292cf2e5c574224e274d2716b263b849f785201 /src/base | |
parent | df418d6cba58a529e02ff143388c8514282bc70b (diff) | |
download | abc-dd867b404acec3d7e22663189bdf1108435a381d.tar.gz abc-dd867b404acec3d7e22663189bdf1108435a381d.tar.bz2 abc-dd867b404acec3d7e22663189bdf1108435a381d.zip |
Added transformation of CEX after 'fix_aig' and checking of transformed CEXes using 'testcex -a'.
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abc/abcLatch.c | 51 | ||||
-rw-r--r-- | src/base/abci/abc.c | 62 |
2 files changed, 89 insertions, 24 deletions
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c index 6c9961a1..8481e582 100644 --- a/src/base/abc/abcLatch.c +++ b/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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3fc68dda..3e0a26ff 100644 --- a/src/base/abci/abc.c +++ b/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 |