diff options
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r-- | src/base/abci/abc.c | 41 |
1 files changed, 31 insertions, 10 deletions
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; |