Updates to arithmetic verification.

5 files changed, 313 insertions, 9 deletions

diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h
index f39041c8..c61b4485 100644
--- a/src/proof/acec/acec.h
+++ b/src/proof/acec/acec.h
@@ -53,7 +53,7 @@ ABC_NAMESPACE_HEADER_START
 /*=== acecCore.c ========================================================*/
 extern int           Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars );
 /*=== acecFadds.c ========================================================*/
-extern Vec_Int_t *   Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose );
+extern Vec_Int_t *   Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** vCutsXor2 );
 extern Vec_Int_t *   Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose );
 /*=== acecOrder.c ========================================================*/
 extern Vec_Int_t *   Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose );
diff --git a/src/proof/acec/acecCover.c b/src/proof/acec/acecCover.c
new file mode 100644
index 00000000..e0d16419
--- /dev/null
+++ b/src/proof/acec/acecCover.c
@@ -0,0 +1,263 @@
+/**CFile****************************************************************
+
+  FileName    [acecCover.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [CEC for arithmetic circuits.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: acecCover.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_AcecMark_rec( Gia_Man_t * p, int iObj, int fFirst )
+{
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    if ( pObj->fMark0 && !fFirst )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    pObj->fMark1 = 1;
+    Gia_AcecMark_rec( p, Gia_ObjFaninId0(pObj, iObj), 0 );
+    Gia_AcecMark_rec( p, Gia_ObjFaninId1(pObj, iObj), 0 );
+}
+void Gia_AcecMarkFadd( Gia_Man_t * p, int * pSigs )
+{
+//    if ( Gia_ManObj(p, pSigs[3])->fMark1 || Gia_ManObj(p, pSigs[4])->fMark1 )
+//        return;
+    Gia_ManObj( p, pSigs[0] )->fMark0 = 1;
+    Gia_ManObj( p, pSigs[1] )->fMark0 = 1;
+    Gia_ManObj( p, pSigs[2] )->fMark0 = 1;
+//    assert( !Gia_ManObj(p, pSigs[3])->fMark1 );
+//    assert( !Gia_ManObj(p, pSigs[4])->fMark1 );
+    Gia_AcecMark_rec( p, pSigs[3], 1 );
+    Gia_AcecMark_rec( p, pSigs[4], 1 );
+}
+void Gia_AcecMarkHadd( Gia_Man_t * p, int * pSigs )
+{
+    Gia_Obj_t * pObj = Gia_ManObj( p, pSigs[0] );
+    int iFan0 = Gia_ObjFaninId0( pObj, pSigs[0] );
+    int iFan1 = Gia_ObjFaninId1( pObj, pSigs[0] );
+    Gia_ManObj( p, iFan0 )->fMark0 = 1;
+    Gia_ManObj( p, iFan1 )->fMark0 = 1;
+    Gia_AcecMark_rec( p, pSigs[0], 1 );
+    Gia_AcecMark_rec( p, pSigs[1], 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect XORs reachable from the last output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_AcecCollectXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Bit_t * vMap, Vec_Int_t * vXors )
+{
+    if ( !Gia_ObjIsXor(pObj) )//|| Vec_BitEntry(vMap, Gia_ObjId(p, pObj)) )
+        return;
+    Vec_IntPush( vXors, Gia_ObjId(p, pObj) );
+    Gia_AcecCollectXors_rec( p, Gia_ObjFanin0(pObj), vMap, vXors );
+    Gia_AcecCollectXors_rec( p, Gia_ObjFanin1(pObj), vMap, vXors );
+}
+Vec_Int_t * Gia_AcecCollectXors( Gia_Man_t * p, Vec_Bit_t * vMap )
+{
+    Vec_Int_t * vXors = Vec_IntAlloc( 100 );
+    Gia_Obj_t * pObj = Gia_ObjFanin0( Gia_ManCo(p, Gia_ManCoNum(p)-1) );
+    Gia_AcecCollectXors_rec( p, pObj, vMap, vXors );
+    return vXors;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_AcecExplore( Gia_Man_t * p, int fVerbose )
+{
+    Vec_Int_t * vNodes = Vec_IntAlloc( 100 );
+    Vec_Int_t * vFadds, * vHadds, * vXors;
+    Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(p) );
+    Gia_Obj_t * pObj; 
+    int i, nSupp, nCone, nHadds = 0;
+    assert( p->pMuxes != NULL );
+    vFadds = Gia_ManDetectFullAdders( p, fVerbose, NULL );
+    vHadds = Gia_ManDetectHalfAdders( p, fVerbose );
+
+    pObj = Gia_ManObj( p, 352 );
+    printf( "Xor = %d.\n", Gia_ObjIsXor(pObj) );
+    printf( "Fanin0 = %d.  Fanin1 = %d.\n", Gia_ObjFaninId0(pObj, 352), Gia_ObjFaninId1(pObj, 352) );
+    printf( "Fan00 = %d.  Fan01 = %d.   Fan10 = %d.  Fan11 = %d.\n", 
+        Gia_ObjFaninId0(Gia_ObjFanin0(pObj), Gia_ObjFaninId0(pObj, 352)), 
+        Gia_ObjFaninId1(Gia_ObjFanin0(pObj), Gia_ObjFaninId0(pObj, 352)), 
+        Gia_ObjFaninId0(Gia_ObjFanin1(pObj), Gia_ObjFaninId1(pObj, 352)), 
+        Gia_ObjFaninId1(Gia_ObjFanin1(pObj), Gia_ObjFaninId1(pObj, 352)) );
+
+    // create a map of all HADD/FADD outputs
+    for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ )
+    {
+        int * pSigs = Vec_IntEntryP(vHadds, 2*i);
+        Vec_BitWriteEntry( vMap, pSigs[0], 1 );
+        Vec_BitWriteEntry( vMap, pSigs[1], 1 );
+    }
+    for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ )
+    {
+        int * pSigs = Vec_IntEntryP(vFadds, 5*i);
+        Vec_BitWriteEntry( vMap, pSigs[3], 1 );
+        Vec_BitWriteEntry( vMap, pSigs[4], 1 );
+    }
+
+    Gia_ManCleanMark01( p );
+
+    // mark outputs
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ObjFanin0(pObj)->fMark0 = 1;
+
+    // collect XORs
+    vXors = Gia_AcecCollectXors( p, vMap );
+    Vec_BitFree( vMap );
+
+    printf( "Collected XORs: " );
+    Vec_IntPrint( vXors );
+
+    // mark their fanins
+    Gia_ManForEachObjVec( vXors, p, pObj, i )
+    {
+        pObj->fMark1 = 1;
+        Gia_ObjFanin0(pObj)->fMark0 = 1;
+        Gia_ObjFanin1(pObj)->fMark0 = 1;
+    }
+
+    // mark FADDs
+    for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ )
+        Gia_AcecMarkFadd( p, Vec_IntEntryP(vFadds, 5*i) );
+
+    // iterate through HADDs and find those that fit in
+    while ( 1 )
+    {
+        int fChange = 0;
+        for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ )
+        {
+            int * pSigs = Vec_IntEntryP(vHadds, 2*i);
+            if ( !Gia_ManObj(p, pSigs[0])->fMark0 || !Gia_ManObj(p, pSigs[1])->fMark0 )
+                continue;
+            if ( Gia_ManObj(p, pSigs[0])->fMark1 || Gia_ManObj(p, pSigs[1])->fMark1 )
+                continue;
+            Gia_AcecMarkHadd( p, pSigs );
+            fChange = 1;
+            nHadds++;
+        }
+        if ( !fChange )
+            break;
+    }
+    // print inputs to the adder network
+    Gia_ManForEachAnd( p, pObj, i )
+        if ( pObj->fMark0 && !pObj->fMark1 )
+        {
+            nSupp = Gia_ManSuppSize( p, &i, 1 );
+            nCone = Gia_ManConeSize( p, &i, 1 );
+            printf( "Node %5d : Supp = %5d.  Cone = %5d.\n", i, nSupp, nCone );
+            Vec_IntPush( vNodes, i );
+        }
+    printf( "Fadds = %d. Hadds = %d.  Root nodes found = %d.\n", Vec_IntSize(vFadds)/5, nHadds, Vec_IntSize(vNodes) );
+
+    Gia_ManCleanMark01( p );
+
+    Gia_ManForEachObjVec( vNodes, p, pObj, i )
+        pObj->fMark0 = 1;
+
+    Vec_IntFree( vFadds );
+    Vec_IntFree( vHadds );
+    Vec_IntFree( vNodes );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_AcecCover( Gia_Man_t * p )
+{
+    int fVerbose = 1;
+    int i, k, Entry;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vCutsXor2 = NULL;
+    Vec_Int_t * vFadds = Gia_ManDetectFullAdders( p, fVerbose, &vCutsXor2 );
+
+    // mark FADDs
+    Gia_ManCleanMark01( p );
+    for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ )
+        Gia_AcecMarkFadd( p, Vec_IntEntryP(vFadds, 5*i) );
+
+    k = 0;
+    Vec_IntForEachEntry( vCutsXor2, Entry, i )
+    {
+        if ( i % 3 != 2 )
+            continue;
+        pObj = Gia_ManObj( p, Entry );
+        if ( pObj->fMark1 )
+            continue;
+        printf( "%d ", Entry );
+    }
+    printf( "\n" );
+
+    Gia_ManCleanMark01( p );
+
+    Vec_IntFree( vFadds );
+    Vec_IntFree( vCutsXor2 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecFadds.c b/src/proof/acec/acecFadds.c
index 6b954398..7f6dcd53 100644
--- a/src/proof/acec/acecFadds.c
+++ b/src/proof/acec/acecFadds.c
@@ -59,6 +59,7 @@ Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose )
         {
             if ( !Gia_ObjIsXor(pObj) )
                 continue;
+            Count = 0;
             iFan0 = Gia_ObjFaninId0(pObj, i);
             iFan1 = Gia_ObjFaninId1(pObj, i);
             if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 0))) )
@@ -69,6 +70,7 @@ Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose )
                 Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
             if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 0))) )
                 Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++;
+            Counts[Count]++;
         }
     }
     else
@@ -116,7 +118,10 @@ Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose )
         printf( "\n" );
 
         Vec_IntForEachEntryDouble( vHadds, iXor, iAnd, i )
-            printf( "%3d : %5d %5d\n", i, iXor, iAnd );
+        {
+            pObj = Gia_ManObj( p, iXor );
+            printf( "%3d : %5d %5d -> %5d %5d\n", i, Gia_ObjFaninId0(pObj, iXor), Gia_ObjFaninId1(pObj, iXor), iXor, iAnd );
+        }
     }
     return vHadds;
 }
@@ -255,6 +260,8 @@ int Dtc_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut, int * pTruth )
     Dtc_ObjCleanTruth_rec( Gia_ManObj(p, iObj) );
     if ( pTruth ) 
         *pTruth = Truth;
+    if ( Truth == 0x66 || Truth == 0x99 )
+        return 3;
     if ( Truth == 0x96 || Truth == 0x69 )
         return 1;
     if ( Truth == 0xE8 || Truth == 0xD4 || Truth == 0xB2 || Truth == 0x71 ||
@@ -262,11 +269,13 @@ int Dtc_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut, int * pTruth )
         return 2;
     return 0;
 }
-void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj )
+void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Vec_Int_t * vCutsXor2, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj )
 {
     int fVerbose = 0;
     Vec_Int_t * vTemp;
     int i, k, c, Type, * pCut0, * pCut1, pCut[4];
+    if ( fVerbose )
+        printf( "Object %d = :\n", iObj );
     Vec_IntFill( vCuts, 2, 1 );
     Vec_IntPush( vCuts, iObj );
     Dtc_ForEachCut( pList0, pCut0, i )
@@ -277,8 +286,28 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
         if ( Dtc_ManCutCheckEqual(vCuts, pCut) )
             continue;
         Vec_IntAddToEntry( vCuts, 0, 1 );  
+        if ( fVerbose )
+            printf( "%d : ", pCut[0] );
         for ( c = 0; c <= pCut[0]; c++ )
+        {
             Vec_IntPush( vCuts, pCut[c] );
+            if ( fVerbose && c )
+                printf( "%d ", pCut[c] );
+        }
+        if ( fVerbose )
+            printf( "\n" );
+        if ( pCut[0] == 2 )
+        {
+            int Value = Dtc_ObjComputeTruth( p, iObj, pCut, NULL );
+            assert( Value == 3 || Value == 0 );
+            if ( Value == 3 )
+            {
+                Vec_IntPush( vCutsXor2, pCut[1] );
+                Vec_IntPush( vCutsXor2, pCut[2] );
+                Vec_IntPush( vCutsXor2, iObj );
+            }
+            continue;
+        }
         if ( pCut[0] != 3 )
             continue;
         Type = Dtc_ObjComputeTruth( p, iObj, pCut, NULL );
@@ -298,11 +327,12 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
         Vec_IntPush( vTemp, iObj );
     }
 }
-void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvCutsMaj, int fVerbose )
+void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor2, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvCutsMaj, int fVerbose )
 {
     Gia_Obj_t * pObj; 
     int * pList0, * pList1, i, nCuts = 0;
     Vec_Int_t * vTemp = Vec_IntAlloc( 1000 );
+    Vec_Int_t * vCutsXor2 = Vec_IntAlloc( Gia_ManAndNum(p) );
     Vec_Int_t * vCutsXor = Vec_IntAlloc( Gia_ManAndNum(p) );
     Vec_Int_t * vCutsMaj = Vec_IntAlloc( Gia_ManAndNum(p) );
     Vec_Int_t * vCuts = Vec_IntAlloc( 30 * Gia_ManAndNum(p) );
@@ -319,7 +349,7 @@ void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvC
     {
         pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, i)) );
         pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, i)) );
-        Dtc_ManCutMerge( p, i, pList0, pList1, vTemp, vCutsXor, vCutsMaj );
+        Dtc_ManCutMerge( p, i, pList0, pList1, vTemp, vCutsXor2, vCutsXor, vCutsMaj );
         Vec_IntWriteEntry( vCuts, i, Vec_IntSize(vCuts) );
         Vec_IntAppend( vCuts, vTemp );
         nCuts += Vec_IntEntry( vTemp, 0 );
@@ -329,6 +359,10 @@ void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvC
             Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p), 1.0*Vec_IntSize(vCuts)/Gia_ManAndNum(p) );
     Vec_IntFree( vTemp );
     Vec_IntFree( vCuts );
+    if ( pvCutsXor2 )
+        *pvCutsXor2 = vCutsXor2;
+    else
+        Vec_IntFree( vCutsXor2 );
     *pvCutsXor = vCutsXor;
     *pvCutsMaj = vCutsMaj;
 }
@@ -375,6 +409,12 @@ void Dtc_ManPrintFadds( Vec_Int_t * vFadds )
         printf( "%6d ", Vec_IntEntry(vFadds, 5*i+3) );
         printf( "%6d ", Vec_IntEntry(vFadds, 5*i+4) );
         printf( "\n" );
+
+        if ( i == 100 )
+        {
+            printf( "Skipping other FADDs.\n" );
+            break;
+        }
     }
 }
 int Dtc_ManCompare( int * pCut0, int * pCut1 )
@@ -394,10 +434,10 @@ int Dtc_ManCompare2( int * pCut0, int * pCut1 )
     return 0;
 }
 // returns array of 5-tuples containing inputs/sum/cout of each full adder
-Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose )
+Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** pvCutsXor2 )
 {
     Vec_Int_t * vCutsXor, * vCutsMaj, * vFadds;
-    Dtc_ManComputeCuts( p, &vCutsXor, &vCutsMaj, fVerbose );
+    Dtc_ManComputeCuts( p, pvCutsXor2, &vCutsXor, &vCutsMaj, fVerbose );
     qsort( Vec_IntArray(vCutsXor), Vec_IntSize(vCutsXor)/4, 16, (int (*)(const void *, const void *))Dtc_ManCompare );
     qsort( Vec_IntArray(vCutsMaj), Vec_IntSize(vCutsMaj)/4, 16, (int (*)(const void *, const void *))Dtc_ManCompare );
     vFadds = Dtc_ManFindCommonCuts( p, vCutsXor, vCutsMaj );
@@ -762,7 +802,7 @@ Gia_Man_t * Gia_ManDupWithNaturalBoxes( Gia_Man_t * p, int nFaddMin, int fVerbos
     assert( Gia_ManBoxNum(p) == 0 );
 
     // detect FADDs
-    vFadds = Gia_ManDetectFullAdders( p, fVerbose );
+    vFadds = Gia_ManDetectFullAdders( p, fVerbose, NULL );
     assert( Vec_IntSize(vFadds) % 5 == 0 );
     // map MAJ into its FADD
     vMap = Gia_ManCreateMap( p, vFadds );
diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c
index 9b2242d0..93ef7f10 100644
--- a/src/proof/acec/acecOrder.c
+++ b/src/proof/acec/acecOrder.c
@@ -198,7 +198,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
 ***********************************************************************/
 Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose )
 {
-    Vec_Int_t * vFadds  = Gia_ManDetectFullAdders( pGia, fVeryVerbose );
+    Vec_Int_t * vFadds  = Gia_ManDetectFullAdders( pGia, fVeryVerbose, NULL );
     Vec_Int_t * vHadds  = Gia_ManDetectHalfAdders( pGia, fVeryVerbose );
     Vec_Int_t * vRecord = Gia_PolynFindOrder( pGia, vFadds, vHadds, fVerbose, fVeryVerbose );
     Vec_Int_t * vOrder  = Vec_IntAlloc( Gia_ManAndNum(pGia) );
diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make
index c70b0a7d..900d3f5f 100644
--- a/src/proof/acec/module.make
+++ b/src/proof/acec/module.make
@@ -1,4 +1,5 @@
 SRC +=    src/proof/acec/acecCore.c \
+    src/proof/acec/acecCover.c \
     src/proof/acec/acecFadds.c \
     src/proof/acec/acecOrder.c \
     src/proof/acec/acecPolyn.c \