summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abc/abcLatch.c51
-rw-r--r--src/base/abci/abc.c62
-rw-r--r--src/misc/util/utilCex.c39
-rw-r--r--src/misc/util/utilCex.h1
4 files changed, 129 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
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 08a56317..3acd7f77 100644
--- a/src/misc/util/utilCex.c
+++ b/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 []
diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h
index c6904a60..4163a1fe 100644
--- a/src/misc/util/utilCex.h
+++ b/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 );
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-26 09:21:28 +0000