Adding new features to 'dualrail'.

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.]