Experiments with word-level data structures.

3 files changed, 107 insertions, 10 deletions

diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c
index b4e5f009..b42a4791 100644
--- a/src/base/wln/wlnRead.c
+++ b/src/base/wln/wlnRead.c
@@ -2137,6 +2137,7 @@ void Rtl_LibSetReplace( Rtl_Lib_t * p, Vec_Wec_t * vGuide )
         pNtk->iCopy = -1;
     Vec_WecForEachLevel( vGuide, vLevel, i )
     {
+        int Type  = Vec_IntEntry( vLevel, 1 );
         int Name1 = Vec_IntEntry( vLevel, 2 );
         int Name2 = Vec_IntEntry( vLevel, 3 );
         int iNtk  = Rtl_LibFindTwoModules( p, Name1, Name2 );
@@ -2145,6 +2146,8 @@ void Rtl_LibSetReplace( Rtl_Lib_t * p, Vec_Wec_t * vGuide )
             printf( "Cannot find networks \"%s\" and \"%s\" in the design.\n", Rtl_LibStr(p, Name1), Rtl_LibStr(p, Name2) ); 
             break;
         }
+        if ( Type != Rtl_LibStrId(p, "equal") )
+            continue;
         iNtk1 = iNtk >> 16;
         iNtk2 = iNtk & 0xFFFF;
         pNtk1 = Rtl_LibNtk(p, iNtk1);
@@ -2215,9 +2218,9 @@ void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
     abctime clk = Abc_Clock(); int Status;
     Rtl_Ntk_t * pTop = pNtk ? (Rtl_Ntk_t *)pNtk : Rtl_LibTop( pLib );
     Gia_Man_t * pSwp = Cec4_ManSimulateTest3( pTop->pGia, 1000000, 0 );
-    int RetValue = Gia_ManAndNum(pSwp) == 0;
+    int RetValue = Gia_ManAndNum(pSwp);
     Gia_ManStop( pSwp );
-    if ( RetValue )
+    if ( RetValue == 0 )
         printf( "Verification problem solved after SAT sweeping!  " );
     else
     {
@@ -2229,7 +2232,7 @@ void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
         if ( Status == 1 )
             printf( "Verification problem solved after CEC!  " );
         else
-            printf( "Verification problem is NOT solved!  " );
+            printf( "Verification problem is NOT solved (miter has %d nodes)!  ", RetValue );
     }
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }
@@ -2248,35 +2251,113 @@ void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk )
 ***********************************************************************/
 void Wln_SolveEqual( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
 {
+    abctime clk = Abc_Clock(); 
     Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
     Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
-    printf( "Proving equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
-/*
+    printf( "\nProving equivalence of \"%s\" and \"%s\"...\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
     if ( Gia_ManCiNum(pNtk1->pGia) != Gia_ManCiNum(pNtk2->pGia) || 
          Gia_ManCoNum(pNtk1->pGia) != Gia_ManCoNum(pNtk2->pGia) )
     {
         printf( "The number of inputs/outputs does not match.\n" );
     }
+    else if ( 1 )
+    {
+        Gia_Man_t * pGia = Gia_ManMiter( pNtk1->pGia, pNtk2->pGia, 0, 0, 0, 0, 0 );
+        Gia_Man_t * pNew = Cec4_ManSimulateTest3( pGia, 10000000, 0 );
+        //printf( "Miter %d -> %d\n",  Gia_ManAndNum(pGia),  Gia_ManAndNum(pNew) );
+        if ( Gia_ManAndNum(pNew) == 0 )
+            Abc_Print( 1, "Networks are equivalent.  " );
+        else
+            Abc_Print( 1, "Networks are UNDECIDED.  " );
+        Gia_ManStopP( &pNew );
+        Gia_ManStopP( &pGia );
+    }
     else
     {
         int Status = Cec_ManVerifyTwo( pNtk1->pGia, pNtk2->pGia, 0 );
         if ( Status == 1 )
-            printf( "The networks are equivalence.\n" );
+            printf( "The networks are equivalent.  " );
         else
-            printf( "The networks are NOT equivalent.\n" );
+            printf( "The networks are NOT equivalent.  " );
     }
-*/
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts )
+{
+    int i, * pWire, iFirst = -1, Counts[4] = {0}, nBits = 0;
+    assert( p->nOutputs == 1 );
+    Rtl_NtkForEachWire( p, pWire, i )
+    {
+        if ( pWire[0] & 1 ) // PI
+            Counts[0]++, Counts[1] += pWire[1];
+        if ( pWire[0] & 2 ) // PO
+            Counts[2]++, Counts[3] += pWire[1];
+    }
+    assert( p->nInputs  == Counts[0] );
+    assert( p->nOutputs == Counts[2] );
+    *pnOuts = Counts[3];
+    Rtl_NtkForEachWire( p, pWire, i )
+    {
+        if ( pWire[0] & 1 ) // PI
+        {
+            if ( pWire[1] == Counts[3] )
+                return nBits;
+            nBits += pWire[1];
+        }
+    }
+    return -1;
+}
+Gia_Man_t * Gia_ManMoveSharedFirst( Gia_Man_t * pGia, int iFirst, int nBits )
+{
+    Vec_Int_t * vPiPerm = Vec_IntAlloc( Gia_ManPiNum(pGia) );
+    Gia_Man_t * pTemp; int i, n;
+    for ( n = 0; n < 2; n++ )
+        for ( i = 0; i < Gia_ManPiNum(pGia); i++ )
+            if ( n == (i >= iFirst && i < iFirst + nBits) )
+                Vec_IntPush( vPiPerm, i );
+    pTemp = Gia_ManDupPerm( pGia, vPiPerm );
+    Vec_IntFree( vPiPerm );
+    return pTemp;
 }
 void Wln_SolveInverse( Rtl_Lib_t * p, int iNtk1, int iNtk2 )
 {
+    abctime clk = Abc_Clock(); 
     Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 );
     Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 );
-    printf( "Proving inverse equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
+    int Res = printf( "\nProving inverse equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) );
+    int nOuts1, iFirst1 = Gia_ManFindFirst( pNtk1, &nOuts1 );
+    int nOuts2, iFirst2 = Gia_ManFindFirst( pNtk2, &nOuts2 );
+    Gia_Man_t * pGia1 = Gia_ManMoveSharedFirst( pNtk1->pGia, iFirst1, nOuts1 );
+    Gia_Man_t * pGia2 = Gia_ManMoveSharedFirst( pNtk2->pGia, iFirst2, nOuts2 );
+    if ( 1 )
+    {
+        Gia_Man_t * pGia  = Gia_ManMiterInverse( pGia1, pGia2, 0, 0 );
+        Gia_Man_t * pNew  = Cec4_ManSimulateTest3( pGia, 10000000, 0 );
+        //printf( "Miter %d -> %d\n",  Gia_ManAndNum(pGia),  Gia_ManAndNum(pNew) );
+        if ( Gia_ManAndNum(pNew) == 0 )
+            Abc_Print( 1, "Networks are equivalent.  " );
+        else
+            Abc_Print( 1, "Networks are UNDECIDED.  " );
+        Gia_ManStopP( &pNew );
+        Gia_ManStopP( &pGia );
+    }
+    else
+    {
+        int Status = Cec_ManVerifyTwoInv( pGia1, pGia2, 0 );
+        if ( Status == 1 )
+            printf( "The networks are equivalent.  " );
+        else
+            printf( "The networks are NOT equivalent.  " );
+    }
+    Res = 0;
+    Gia_ManStopP( &pGia1 );
+    Gia_ManStopP( &pGia2 );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 }
 void Wln_SolveProperty( Rtl_Lib_t * p, int iNtk )
 {
     Rtl_Ntk_t * pNtk = Rtl_LibNtk( p, iNtk );
-    printf( "Proving property \"%s\".\n", Rtl_NtkName(pNtk) );
+    printf( "\nProving property \"%s\".\n", Rtl_NtkName(pNtk) );
     Rtl_LibSolve( p, pNtk );
 }
 Vec_Int_t * Wln_ReadNtkRoots( Rtl_Lib_t * p, Vec_Wec_t * vGuide ) 
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 7c101570..40aa9799 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -206,6 +206,7 @@ struct Cec_ParSeq_t_
 /*=== cecCec.c ==========================================================*/
 extern int           Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars );
 extern int           Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose );
+extern int           Cec_ManVerifyTwoInv( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose );
 extern int           Cec_ManVerifySimple( Gia_Man_t * p );
 /*=== cecChoice.c ==========================================================*/
 extern Gia_Man_t *   Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars );
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index cfa07ff8..f6a1ab52 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -465,6 +465,21 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
     Gia_ManStop( pMiter );
     return RetValue;
 }
+int Cec_ManVerifyTwoInv( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
+{
+    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+    Gia_Man_t * pMiter;
+    int RetValue;
+    Cec_ManCecSetDefaultParams( pPars );
+    pPars->fVerbose = fVerbose;
+    pMiter = Gia_ManMiterInverse( p0, p1, 1, pPars->fVerbose );
+    if ( pMiter == NULL )
+        return -1;
+    RetValue = Cec_ManVerify( pMiter, pPars );
+    p0->pCexComb = pMiter->pCexComb; pMiter->pCexComb = NULL;
+    Gia_ManStop( pMiter );
+    return RetValue;
+}
 
 /**Function*************************************************************