Upgrading reparametrization to perform (non-range-equivalent) removal of logic.

2 files changed, 141 insertions, 3 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index fe0ed932..988d50a2 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -4814,6 +4814,62 @@ Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicate AIG by creating a cut between logic fed by PIs]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManHighLightFlopLogic( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj; int i;
+    Gia_ManForEachPi( p, pObj, i )
+        pObj->fMark0 = 0;
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->fMark0 = 1;
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 | Gia_ObjFanin1(pObj)->fMark0;
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0;
+}
+Gia_Man_t * Gia_ManDupReplaceCut( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew;  int i;
+    Gia_Obj_t * pObj, * pFanin;
+    Gia_ManHighLightFlopLogic( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    // create PIs for nodes pointed to from above the cut
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !pObj->fMark0 )
+            continue;
+        pFanin = Gia_ObjFanin0(pObj);
+        if ( !pFanin->fMark0 && !~pFanin->Value )
+            pFanin->Value = Gia_ManAppendCi(pNew);
+        pFanin = Gia_ObjFanin1(pObj);
+        if ( !pFanin->fMark0 && !~pFanin->Value )
+            pFanin->Value = Gia_ManAppendCi(pNew);
+    }
+    // create flop outputs
+    Gia_ManForEachRo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    // create internal nodes
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManDupOrderDfs_rec( pNew, p, pObj );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    Gia_ManCleanMark0( p );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a5251c7a..3eafcfb9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -527,6 +527,7 @@ static int Abc_CommandAbc9Mfsd               ( Abc_Frame_t * pAbc, int argc, cha
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMin             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandAbc9AbsCreate          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9AbsDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9AbsRefine          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1227,6 +1228,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmin",       Abc_CommandAbc9CexMin,       0 );
 
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_create",   Abc_CommandAbc9AbsCreate,    0 );
     Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_derive",   Abc_CommandAbc9AbsDerive,    0 );
     Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_refine",   Abc_CommandAbc9AbsRefine,    0 );
     Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_derive",   Abc_CommandAbc9GlaDerive,    0 );
@@ -39498,13 +39500,15 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Rpm( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    extern Gia_Man_t * Gia_ManDupReplaceCut( Gia_Man_t * p );
     Gia_Man_t * pTemp;
     int c, nCutMax   = 16;
+    int fUseNaive    =  0;
     int fUseOldAlgo  =  0;
     int fVerbose     =  0;
     int fVeryVerbose =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cavwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cnavwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -39519,6 +39523,9 @@ int Abc_CommandAbc9Rpm( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nCutMax < 0 )
                 goto usage;
             break;
+        case 'n':
+            fUseNaive ^= 1;
+            break;
         case 'a':
             fUseOldAlgo ^= 1;
             break;
@@ -39539,7 +39546,9 @@ int Abc_CommandAbc9Rpm( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Rpm(): There is no AIG.\n" );
         return 0;
     }
-    if ( fUseOldAlgo )
+    if ( fUseNaive )
+        pTemp = Gia_ManDupReplaceCut( pAbc->pGia );
+    else if ( fUseOldAlgo )
         pTemp = Abs_RpmPerformOld( pAbc->pGia, fVerbose );
     else
         pTemp = Abs_RpmPerform( pAbc->pGia, nCutMax, fVerbose, fVeryVerbose );
@@ -39547,9 +39556,10 @@ int Abc_CommandAbc9Rpm( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &rpm [-C num] [-avwh]\n" );
+    Abc_Print( -2, "usage: &rpm [-C num] [-navwh]\n" );
     Abc_Print( -2, "\t         performs structural reparametrization\n" );
     Abc_Print( -2, "\t-C num : max cut size for testing range equivalence [default = %d]\n", nCutMax );
+    Abc_Print( -2, "\t-n     : toggle using naive reparametrization [default = %s]\n", fUseNaive? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggle using old algorithm [default = %s]\n", fUseOldAlgo? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
@@ -44848,6 +44858,78 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9AbsCreate( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp = NULL;
+    char * pStr, * pFlopNum;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9AbsCreate(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "The network is combinational.\n" );
+        return 0;
+    }
+    if ( pAbc->pGia->vFlopClasses != NULL )
+    {
+        Abc_Print( -1, "Abstraction flop map is already defined.\n" );
+        return 0;
+    }
+    pAbc->pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pAbc->pGia) );
+    // read the flop list
+    if ( argc != globalUtilOptind + 1 )
+    {
+        Abc_Print( -1, "Flop list should be specified on the command line.\n" );
+        return 0;
+    }
+    pStr = argv[globalUtilOptind];
+    // parse flop list
+    pFlopNum = strtok( pStr, " ," );
+    while ( pFlopNum )
+    {
+        int iFlop = atoi(pFlopNum);
+        assert( iFlop >= 0 && iFlop < Gia_ManRegNum(pAbc->pGia) );
+        Vec_IntWriteEntry( pAbc->pGia->vFlopClasses, iFlop, 1 );
+        pFlopNum = strtok( NULL, " ," );
+    }
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &abs_create [-vh] <comma-separated_list_of_zero-based_flop_ids>\n" );
+    Abc_Print( -2, "\t        creates new flop map by reading user's input\n" );
+    Abc_Print( -2, "\t-v    : toggle printing verbose information [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_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;