Generation of dual-rail miter.

3 files changed, 184 insertions, 0 deletions

diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index cbd25a18..327b9dd5 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -10,6 +10,7 @@ SRC +=    src/aig/saig/saigAbs.c \
     src/aig/saig/saigCone.c \
     src/aig/saig/saigConstr.c \
     src/aig/saig/saigConstr2.c \
+    src/aig/saig/saigDual.c \
     src/aig/saig/saigDup.c \
     src/aig/saig/saigGlaCba.c \
     src/aig/saig/saigGlaPba.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index b22821ab..10a763ba 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -163,6 +163,9 @@ extern void              Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame
 /*=== saigConstr2.c ==========================================================*/
 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 fComplPo );
+extern void              Saig_ManBlockPo( Aig_Man_t * pAig, int nCycles );
 /*=== saigDup.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManDupOrpos( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 605e678e..e936602f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -276,6 +276,8 @@ static int Abc_CommandTestCex                ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandPdr                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandReconcile              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCexMin                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDualRail               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBlockPo                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandTraceStart             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -686,6 +688,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "pdr",           Abc_CommandPdr,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "reconcile",     Abc_CommandReconcile,        1 );
     Cmd_CommandAdd( pAbc, "Verification", "cexmin",        Abc_CommandCexMin,           0 );
+    Cmd_CommandAdd( pAbc, "Verification", "dualrail",      Abc_CommandDualRail,         1 );
+    Cmd_CommandAdd( pAbc, "Verification", "blockpo",       Abc_CommandBlockPo,          1 );
 
     Cmd_CommandAdd( pAbc, "ABC9",         "&get",          Abc_CommandAbc9Get,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&put",          Abc_CommandAbc9Put,          0 );
@@ -21087,6 +21091,182 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandDualRail( Abc_Frame_t * pAbc, int argc, char ** argv )
+{   
+    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;
+    int c;
+    int nDualPis = 0;
+    int fDualFfs = 0;
+    int fComplPo = 0;
+    int fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Ifcvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nDualPis = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nDualPis < 0 ) 
+                goto usage;
+            break;
+        case 'f':
+            fDualFfs ^= 1;
+            break;
+        case 'c':
+            fComplPo ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            Abc_Print( -2, "Unknown switch.\n");
+            goto usage;
+        }
+    }
+
+    // check the main AIG
+    pNtk = Abc_FrameReadNtk(pAbc);
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Main AIG: There is no current network.\n");
+        return 0;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
+        return 0;
+    }
+
+    // tranform    
+    pAig = Abc_NtkToDar( pNtk, 0, 1 );
+    pAigNew = Saig_ManDupDual( pAig, nDualPis, fDualFfs, fComplPo );
+    Aig_ManStop( pAig );
+    pNtkNew = Abc_NtkFromAigPhase( pAigNew );
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+    Aig_ManStop( pAigNew );
+
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: dualrail [-I num] [-fcvh]\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-I num : the number of first PIs interpreted as ternary [default = %d]\n", nDualPis );
+    Abc_Print( -2, "\t-f     : toggle ternary flop init values [default = %s]\n", fDualFfs? "yes": "const0 init values" );
+    Abc_Print( -2, "\t-c     : toggle complementing the miter output [default = %s]\n", fComplPo? "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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandBlockPo( Abc_Frame_t * pAbc, int argc, char ** argv )
+{   
+    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;
+    int c;
+    int nCycles = 0;
+    int fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCycles = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCycles < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            Abc_Print( -2, "Unknown switch.\n");
+            goto usage;
+        }
+    }
+
+    // check the main AIG
+    pNtk = Abc_FrameReadNtk(pAbc);
+    if ( pNtk == NULL )
+    {
+        Abc_Print( 1, "Main AIG: There is no current network.\n");
+        return 0;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
+        return 0;
+    }
+    if ( nCycles == 0 )
+    {
+        Abc_Print( 1, "The number of time frame is 0. The circuit is left unchanged.\n" );
+        return 0;
+    }
+
+    // transform
+    pAig = Abc_NtkToDar( pNtk, 0, 1 );
+    Saig_ManBlockPo( pAig, nCycles );
+    pNtkNew = Abc_NtkFromAigPhase( pAig );
+    Aig_ManStop( pAig );
+
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: blockpo [-F num] [-fvh]\n" );
+    Abc_Print( -2, "\t         forces the miter outputs to be \"true\" in the first F frames\n" );
+    Abc_Print( -2, "\t-F num : the number of time frames [default = %d]\n", nCycles );
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandTraceStart( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);