Extending command 'dump_equv' to match inputs by name.

2 files changed, 68 insertions, 17 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e3794106..bbb4e819 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14828,12 +14828,12 @@ usage:
 ***********************************************************************/
 int Abc_CommandDumpEquiv( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fVerbose );
+    extern void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fByName, int fVerbose );
     Abc_Ntk_t * pNtks[2] = {NULL};
     char * pFileName[2], * pFileNameOut;
-    int c, nConfs = 1000, fVerbose = 0;
+    int c, nConfs = 1000, fByName = 1, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cnvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14848,6 +14848,9 @@ int Abc_CommandDumpEquiv( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConfs < 0 )
                 goto usage;
             break;
+        case 'n':
+            fByName ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -14872,20 +14875,25 @@ int Abc_CommandDumpEquiv( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         Abc_NtkToAig( pNtks[c] );
     }
-    if ( Abc_NtkCiNum(pNtks[0]) != Abc_NtkCiNum(pNtks[1]) )
-        Abc_Print( -1, "The number of primary inputs of networks \"%s\" and \"%s\" does not match.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]) );
+//    if ( Abc_NtkCiNum(pNtks[0]) != Abc_NtkCiNum(pNtks[1]) )
+//        Abc_Print( -1, "The number of primary inputs of networks \"%s\" and \"%s\" does not match.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]) );
 //    else if ( Abc_NtkCoNum(pNtks[0]) != Abc_NtkCoNum(pNtks[1]) )
 //        Abc_Print( -1, "The number of primary outputs of networks \"%s\" and \"%s\" does not match.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]) );
-    else
-        Abc_NtkDumpEquiv( pNtks, pFileNameOut, nConfs, fVerbose );
+//    else
+        Abc_NtkDumpEquiv( pNtks, pFileNameOut, nConfs, fByName, fVerbose );
     Abc_NtkDelete( pNtks[0] );
     Abc_NtkDelete( pNtks[1] );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dump_equiv [-C num] [-vh] <file1.blif> <file2.blif> <file_dump_equiv.txt>\n" );
+    Abc_Print( -2, "usage: dump_equiv [-C num] [-nvh] <file1.blif> <file2.blif> <file_dump_equiv.txt>\n" );
     Abc_Print( -2, "\t          computes equivalence classes of nodes in <file1> and <file2>\n" );
+    Abc_Print( -2, "\t          By default this procedure performs matching of primary inputs by name.\n" );
+    Abc_Print( -2, "\t          Those inputs that cannot be matched are treated as free variables.\n" );
+    Abc_Print( -2, "\t          There is no effort to match primary outputs. Indeed, if two outputs\n" );
+    Abc_Print( -2, "\t          are equivalent, they will belong to the same equivalence class in the end.\n" );
     Abc_Print( -2, "\t-C num  : the maximum number of conflicts at each node [default = %d]\n", nConfs );
+    Abc_Print( -2, "\t-n      : enable matching of primary inputs by order [default = %s]\n", fByName? "yes": "no" );
     Abc_Print( -2, "\t-v      : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     Abc_Print( -2, "\t<file1> : first network whose nodes are considered\n" );
diff --git a/src/base/abci/abcDress3.c b/src/base/abci/abcDress3.c
index f18eb217..6150f41d 100644
--- a/src/base/abci/abcDress3.c
+++ b/src/base/abci/abcDress3.c
@@ -112,7 +112,7 @@ int Abc_ConvertHopToGia( Gia_Man_t * p, Hop_Obj_t * pRoot )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk )
+void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk, Vec_Int_t * vMap )
 {
     Hop_Man_t * pHopMan;
     Hop_Obj_t * pHopObj;
@@ -125,7 +125,7 @@ void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk )
     // image primary inputs
     Abc_NtkCleanCopy( pNtk );
     Abc_NtkForEachCi( pNtk, pNode, i )
-        pNode->iTemp = Gia_ManCiLit(p, i);
+        pNode->iTemp = Gia_ManCiLit(p, Vec_IntEntry(vMap, i));
     // iterate through nodes used in the mapping
     vNodes = Abc_NtkDfs( pNtk, 1 );
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
@@ -143,25 +143,68 @@ void Abc_NtkAigToGiaOne( Gia_Man_t * p, Abc_Ntk_t * pNtk )
     Abc_NtkForEachCo( pNtk, pNode, i )
         Gia_ManAppendCo( p, Abc_ObjFanin0(pNode)->iTemp );
 }
-Gia_Man_t * Abc_NtkAigToGiaTwo( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+Gia_Man_t * Abc_NtkAigToGiaTwo( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fByName )
 {
     Gia_Man_t * p;
     Gia_Obj_t * pObj;
     Abc_Obj_t * pNode;
-    int i;
+    Vec_Int_t * vMap1, * vMap2;
+    int i, Index = 0;
     assert( Abc_NtkIsAigLogic(pNtk1) );
     assert( Abc_NtkIsAigLogic(pNtk2) );
+    // find common variables
+    if ( fByName )
+    {
+        int nCommon = 0;
+        vMap1 = Vec_IntStartNatural( Abc_NtkCiNum(pNtk1) );
+        vMap2 = Vec_IntAlloc( Abc_NtkCiNum(pNtk2) );
+        Abc_NtkForEachCi( pNtk1, pNode, i )
+            pNode->iTemp = Index++;
+        assert( Index == Abc_NtkCiNum(pNtk1) );
+        Abc_NtkForEachCi( pNtk2, pNode, i )
+        {
+            int Num = Nm_ManFindIdByName( pNtk1->pManName, Abc_ObjName(pNode), ABC_OBJ_PI );
+            if ( Num < 0 )
+                Num = Nm_ManFindIdByName( pNtk1->pManName, Abc_ObjName(pNode), ABC_OBJ_BO );
+            assert( Num < 0 || Abc_ObjIsCi(Abc_NtkObj(pNtk1, Num)) );
+            if ( Num >= 0 )
+                Vec_IntPush( vMap2, Abc_NtkObj(pNtk1, Num)->iTemp ), nCommon++;
+            else
+                Vec_IntPush( vMap2, Index++ );
+        }
+        // report
+        printf( "Matched %d vars by name.", nCommon );
+        if ( nCommon != Abc_NtkCiNum(pNtk1) )
+            printf( " Netlist1 has %d unmatched vars.", Abc_NtkCiNum(pNtk1) - nCommon );
+        if ( nCommon != Abc_NtkCiNum(pNtk2) )
+            printf( " Netlist2 has %d unmatched vars.", Abc_NtkCiNum(pNtk2) - nCommon );
+        printf( "\n" );
+    }
+    else
+    {
+        vMap1 = Vec_IntStartNatural( Abc_NtkCiNum(pNtk1) );
+        vMap2 = Vec_IntStartNatural( Abc_NtkCiNum(pNtk2) );
+        // report
+        printf( "Matched %d vars by order.", Abc_MinInt(Abc_NtkCiNum(pNtk1), Abc_NtkCiNum(pNtk2)) );
+        if ( Abc_NtkCiNum(pNtk1) < Abc_NtkCiNum(pNtk2) )
+            printf( " The last %d vars of Netlist2 are unmatched vars.", Abc_NtkCiNum(pNtk2) - Abc_NtkCiNum(pNtk1) );
+        if ( Abc_NtkCiNum(pNtk1) > Abc_NtkCiNum(pNtk2) )
+            printf( " The last %d vars of Netlist1 are unmatched vars.", Abc_NtkCiNum(pNtk1) - Abc_NtkCiNum(pNtk2) );
+        printf( "\n" );
+    }
     // create new manager
     p = Gia_ManStart( 10000 );
     p->pName = Abc_UtilStrsav( Abc_NtkName(pNtk1) );
     p->pSpec = Abc_UtilStrsav( Abc_NtkSpec(pNtk1) );
-    Abc_NtkForEachCi( pNtk1, pNode, i )
+    for ( i = 0; i < Index; i++ )
         Gia_ManAppendCi(p);
     // add logic
     Gia_ManHashAlloc( p );
-    Abc_NtkAigToGiaOne( p, pNtk1 );
-    Abc_NtkAigToGiaOne( p, pNtk2 );
+    Abc_NtkAigToGiaOne( p, pNtk1, vMap1 );
+    Abc_NtkAigToGiaOne( p, pNtk2, vMap2 );
     Gia_ManHashStop( p );
+    Vec_IntFree( vMap1 );
+    Vec_IntFree( vMap2 );
     // add extra POs to dangling nodes
     Gia_ManCreateValueRefs( p );
     Gia_ManForEachAnd( p, pObj, i )
@@ -268,12 +311,12 @@ void Abc_NtkDumpEquivFile( char * pFileName, Vec_Int_t * vClasses, Abc_Ntk_t * p
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fVerbose )
+void Abc_NtkDumpEquiv( Abc_Ntk_t * pNtks[2], char * pFileName, int nConfs, int fByName, int fVerbose )
 {
     //abctime clk = Abc_Clock();
     Vec_Int_t * vClasses;
     // derive shared AIG for the two networks
-    Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1] );
+    Gia_Man_t * pGia = Abc_NtkAigToGiaTwo( pNtks[0], pNtks[1], fByName );
     if ( fVerbose )
         printf( "Computing equivalences for networks \"%s\" and \"%s\" with conflict limit %d.\n", Abc_NtkName(pNtks[0]), Abc_NtkName(pNtks[1]), nConfs );
     // compute equivalences in this AIG