summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/saig/saig.h2
-rw-r--r--src/aig/saig/saigDual.c47
-rw-r--r--src/base/abci/abc.c41
-rw-r--r--src/base/abci/abcDar.c23
4 files changed, 95 insertions, 18 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 836a2051..89622491 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -117,7 +117,7 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
/*=== saigDual.c ==========================================================*/
-extern Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo );
+extern Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, Vec_Int_t * vDcFlops, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo, int fCheckZero, int fCheckOne );
extern void Saig_ManBlockPo( Aig_Man_t * pAig, int nCycles );
/*=== saigDup.c ==========================================================*/
extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p );
diff --git a/src/aig/saig/saigDual.c b/src/aig/saig/saigDual.c
index 62f479ee..7650c5ca 100644
--- a/src/aig/saig/saigDual.c
+++ b/src/aig/saig/saigDual.c
@@ -78,7 +78,7 @@ static inline void Saig_ObjDualFanin( Aig_Man_t * pAigNew, Vec_Ptr_t * vC
SeeAlso []
***********************************************************************/
-Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo )
+Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, Vec_Int_t * vDcFlops, int nDualPis, int fDualFfs, int fMiterFfs, int fComplPo, int fCheckZero, int fCheckOne )
{
Vec_Ptr_t * vCopies;
Aig_Man_t * pAigNew;
@@ -86,6 +86,7 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f
int i;
assert( Saig_ManPoNum(pAig) > 0 );
assert( nDualPis >= 0 && nDualPis <= Saig_ManPiNum(pAig) );
+ assert( vDcFlops == NULL || Vec_IntSize(vDcFlops) == Aig_ManRegNum(pAig) );
vCopies = Vec_PtrStart( 2*Aig_ManObjNum(pAig) );
// start the new manager
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
@@ -110,7 +111,10 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f
{
pTemp0 = Aig_ObjCreateCi( pAigNew );
pTemp1 = Aig_ObjCreateCi( pAigNew );
- pTemp0 = Aig_NotCond( pTemp0, !fDualFfs );
+ if ( vDcFlops )
+ pTemp0 = Aig_NotCond( pTemp0, !Vec_IntEntry(vDcFlops, i-Saig_ManPiNum(pAig)) );
+ else
+ pTemp0 = Aig_NotCond( pTemp0, !fDualFfs );
}
Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 0, Aig_And(pAigNew, pTemp0, Aig_Not(pTemp1)) );
Saig_ObjSetDual( vCopies, Aig_ObjId(pObj), 1, Aig_And(pAigNew, pTemp1, Aig_Not(pTemp0)) );
@@ -130,8 +134,21 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f
Saig_ManForEachLi( pAig, pObj, i )
{
Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
- pCare = Aig_Or( pAigNew, pTemp0, pTemp1 );
- pMiter = Aig_Or( pAigNew, pMiter, Aig_Not(pCare) );
+ if ( fCheckZero )
+ {
+ pCare = Aig_And( pAigNew, pTemp0, Aig_Not(pTemp1) );
+ pMiter = Aig_Or( pAigNew, pMiter, pCare );
+ }
+ else if ( fCheckOne )
+ {
+ pCare = Aig_And( pAigNew, Aig_Not(pTemp0), pTemp1 );
+ pMiter = Aig_Or( pAigNew, pMiter, pCare );
+ }
+ else // check X
+ {
+ pCare = Aig_And( pAigNew, Aig_Not(pTemp0), Aig_Not(pTemp1) );
+ pMiter = Aig_Or( pAigNew, pMiter, pCare );
+ }
}
}
else
@@ -139,8 +156,21 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f
Saig_ManForEachPo( pAig, pObj, i )
{
Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
- pCare = Aig_Or( pAigNew, pTemp0, pTemp1 );
- pMiter = Aig_Or( pAigNew, pMiter, Aig_Not(pCare) );
+ if ( fCheckZero )
+ {
+ pCare = Aig_And( pAigNew, pTemp0, Aig_Not(pTemp1) );
+ pMiter = Aig_Or( pAigNew, pMiter, pCare );
+ }
+ else if ( fCheckOne )
+ {
+ pCare = Aig_And( pAigNew, Aig_Not(pTemp0), pTemp1 );
+ pMiter = Aig_Or( pAigNew, pMiter, pCare );
+ }
+ else // check X
+ {
+ pCare = Aig_And( pAigNew, Aig_Not(pTemp0), Aig_Not(pTemp1) );
+ pMiter = Aig_Or( pAigNew, pMiter, pCare );
+ }
}
}
// create PO
@@ -150,7 +180,10 @@ Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, int nDualPis, int fDualFfs, int f
Saig_ManForEachLi( pAig, pObj, i )
{
Saig_ObjDualFanin( pAigNew, vCopies, pObj, 0, &pTemp0, &pTemp1 );
- pTemp0 = Aig_NotCond( pTemp0, !fDualFfs );
+ if ( vDcFlops )
+ pTemp0 = Aig_NotCond( pTemp0, !Vec_IntEntry(vDcFlops, i) );
+ else
+ pTemp0 = Aig_NotCond( pTemp0, !fDualFfs );
Aig_ObjCreateCo( pAigNew, pTemp0 );
Aig_ObjCreateCo( pAigNew, pTemp1 );
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c336e720..b5e5b906 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -23110,18 +23110,23 @@ usage:
***********************************************************************/
int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ extern Vec_Int_t * Abc_NtkFindDcLatches( Abc_Ntk_t * pNtk );
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
Abc_Ntk_t * pNtk, * pNtkNew = NULL;
Aig_Man_t * pAig, * pAigNew;
+ Vec_Int_t * vDcFlops = NULL;
int c;
- int nDualPis = 0;
- int fDualFfs = 0;
- int fMiterFfs = 0;
- int fComplPo = 0;
- int fVerbose = 0;
+ int nDualPis = 0;
+ int fDualFfs = 0;
+ int fDualDcFfs = 0;
+ int fMiterFfs = 0;
+ int fComplPo = 0;
+ int fCheckZero = 0;
+ int fCheckOne = 0;
+ int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Itfcvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Itxfczovh" ) ) != EOF )
{
switch ( c )
{
@@ -23139,12 +23144,21 @@ int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
fDualFfs ^= 1;
break;
+ case 'x':
+ fDualDcFfs ^= 1;
+ break;
case 'f':
fMiterFfs ^= 1;
break;
case 'c':
fComplPo ^= 1;
break;
+ case 'z':
+ fCheckZero ^= 1;
+ break;
+ case 'o':
+ fCheckOne ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -23169,27 +23183,34 @@ int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
- // tranform
+ if ( fDualDcFfs )
+ vDcFlops = Abc_NtkFindDcLatches( pNtk );
+
+ // transform
pAig = Abc_NtkToDar( pNtk, 0, 1 );
- pAigNew = Saig_ManDupDual( pAig, nDualPis, fDualFfs, fMiterFfs, fComplPo );
+ pAigNew = Saig_ManDupDual( pAig, vDcFlops, nDualPis, fDualFfs, fMiterFfs, fComplPo, fCheckZero, fCheckOne );
Aig_ManStop( pAig );
pNtkNew = Abc_NtkFromAigPhase( pAigNew );
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
Aig_ManStop( pAigNew );
+ Vec_IntFreeP( &vDcFlops );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
return 0;
usage:
- Abc_Print( -2, "usage: dualrail [-I num] [-tfcvh]\n" );
+ Abc_Print( -2, "usage: dualrail [-I num] [-txfczovh]\n" );
Abc_Print( -2, "\t transforms the current AIG into a dual-rail miter\n" );
Abc_Print( -2, "\t expressing the property \"at least one PO has ternary value\"\n" );
Abc_Print( -2, "\t (to compute an initialization sequence, use switches \"-tfc\")\n" );
Abc_Print( -2, "\t-I num : the number of first PIs interpreted as ternary [default = %d]\n", nDualPis );
- Abc_Print( -2, "\t-t : toggle ternary flop init values [default = %s]\n", fDualFfs? "yes": "const0 init values" );
+ Abc_Print( -2, "\t-t : toggle ternary flop init values for all flops [default = %s]\n", fDualFfs? "yes": "const0 init values" );
+ Abc_Print( -2, "\t-x : toggle ternary flop init values for DC-valued flops [default = %s]\n", fDualDcFfs? "yes": "const0 init values" );
Abc_Print( -2, "\t-f : toggle mitering flops instead of POs [default = %s]\n", fMiterFfs? "flops": "POs" );
Abc_Print( -2, "\t-c : toggle complementing the miter output [default = %s]\n", fComplPo? "yes": "no" );
+ Abc_Print( -2, "\t-z : toggle checking PO==0 instead of PO==X [default = %s]\n", fCheckZero? "yes": "no" );
+ Abc_Print( -2, "\t-o : toggle checking PO==1 instead of PO==X [default = %s]\n", fCheckOne? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 03df7fec..805b41a7 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -193,6 +193,29 @@ Aig_Man_t * Abc_NtkToDarBmc( Abc_Ntk_t * pNtk, Vec_Int_t ** pvMap )
/**Function*************************************************************
+ Synopsis [Collects information about what flops have unknown values.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkFindDcLatches( Abc_Ntk_t * pNtk )
+{
+ Vec_Int_t * vUnknown;
+ Abc_Obj_t * pObj;
+ int i;
+ vUnknown = Vec_IntStart( Abc_NtkLatchNum(pNtk) );
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ if ( Abc_LatchIsInitDc(pObj) )
+ Vec_IntWriteEntry( vUnknown, i, 1 );
+ return vUnknown;
+}
+
+/**Function*************************************************************
+
Synopsis [Converts the network from the AIG manager into ABC.]
Description [Assumes that registers are ordered after PIs/POs.]
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-29 10:12:01 +0000