Updates to arithmetic verification.

4 files changed, 400 insertions, 5 deletions

diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h
index 381ab8d1..c4c8061e 100644
--- a/src/proof/acec/acecInt.h
+++ b/src/proof/acec/acecInt.h
@@ -76,6 +76,7 @@ extern Vec_Wec_t *   Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdd
 /*=== acecMult.c ========================================================*/
 extern Vec_Int_t *   Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits );
 extern Vec_Bit_t *   Acec_BoothFindPPG( Gia_Man_t * p );
+extern Vec_Bit_t *   Acec_MultMarkPPs( Gia_Man_t * p );
 /*=== acecNorm.c ========================================================*/
 extern void          Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] );
 extern Gia_Man_t *   Acec_InsertBox( Acec_Box_t * pBox, int fAll );
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
index ba9405ac..c63fdde2 100644
--- a/src/proof/acec/acecMult.c
+++ b/src/proof/acec/acecMult.c
@@ -435,6 +435,72 @@ Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec
 
 /**Function*************************************************************
 
+  Synopsis    [Mark nodes whose function is exactly that of a Booth PP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Bit_t * Acec_MultMarkPPs( Gia_Man_t * p )
+{
+    word Saved[32] = {
+        ABC_CONST(0xF335ACC0F335ACC0),
+        ABC_CONST(0x35C035C035C035C0),
+        ABC_CONST(0xD728D728D728D728),
+        ABC_CONST(0xFD80FD80FD80FD80),
+        ABC_CONST(0xACC0ACC0ACC0ACC0),
+        ABC_CONST(0x7878787878787878),
+        ABC_CONST(0x2828282828282828),
+        ABC_CONST(0xD0D0D0D0D0D0D0D0),
+        ABC_CONST(0x8080808080808080),
+        ABC_CONST(0x8888888888888888),
+        ABC_CONST(0xAAAAAAAAAAAAAAAA),
+        ABC_CONST(0x5555555555555555),
+
+        ABC_CONST(0xD5A8D5A8D5A8D5A8),
+        ABC_CONST(0x2A572A572A572A57),
+        ABC_CONST(0xF3C0F3C0F3C0F3C0),
+        ABC_CONST(0x5858585858585858),
+        ABC_CONST(0xA7A7A7A7A7A7A7A7),
+        ABC_CONST(0x2727272727272727),
+        ABC_CONST(0xD8D8D8D8D8D8D8D8)
+    };
+
+    Vec_Bit_t * vRes = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+    int i, iObj, nProds = 0;
+    Gia_ManCleanMark0(p);
+    Gia_ManForEachAndId( p, iObj )
+    {
+        word Truth = Gia_ObjComputeTruth6Cis( p, Abc_Var2Lit(iObj, 0), vSupp, vTemp );
+        if ( Vec_IntSize(vSupp) > 6  )
+            continue;
+        vSupp->nSize = Abc_Tt6MinBase( &Truth, vSupp->pArray, vSupp->nSize );
+        if ( Vec_IntSize(vSupp) > 5  )
+            continue;
+        for ( i = 0; i < 32 && Saved[i]; i++ )
+        {
+            if ( Truth == Saved[i] || Truth == ~Saved[i] )
+            {
+                Vec_BitWriteEntry( vRes, iObj, 1 );
+                nProds++;
+                break;
+            }
+        }
+    }
+    Gia_ManCleanMark0(p);
+    printf( "Collected %d pps.\n", nProds );
+    Vec_IntFree( vSupp );
+    Vec_WrdFree( vTemp );
+    return vRes;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
diff --git a/src/proof/acec/acecStruct.c b/src/proof/acec/acecStruct.c
new file mode 100644
index 00000000..6702e13b
--- /dev/null
+++ b/src/proof/acec/acecStruct.c
@@ -0,0 +1,271 @@
+/**CFile****************************************************************
+
+  FileName    [acecStruct.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: acecStruct.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "acecInt.h"
+#include "misc/vec/vecWec.h"
+#include "misc/extra/extra.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_StructDetectXorRoots( Gia_Man_t * p )
+{
+    Vec_Int_t * vXors = Vec_IntAlloc( 100 );
+    Vec_Bit_t * vXorIns = Vec_BitStart( Gia_ManObjNum(p) );
+    Gia_Obj_t * pFan0, * pFan1, * pObj; 
+    int i, k = 0, Entry;
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            continue;
+        Vec_IntPush( vXors, i );
+        Vec_BitWriteEntry( vXorIns, Gia_ObjId(p, Gia_Regular(pFan0)), 1 );
+        Vec_BitWriteEntry( vXorIns, Gia_ObjId(p, Gia_Regular(pFan1)), 1 );
+    }
+    // collect XORs that not inputs of other XORs
+    Vec_IntForEachEntry( vXors, Entry, i )
+        if ( !Vec_BitEntry(vXorIns, Entry) )
+            Vec_IntWriteEntry( vXors, k++, Entry );
+    Vec_IntShrink( vXors, k );
+    Vec_BitFree( vXorIns );
+    return vXors;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_StructAssignRanks( Gia_Man_t * p, Vec_Int_t * vXorRoots )
+{
+    Vec_Int_t * vDoubles = Vec_IntAlloc( 100 );
+    Gia_Obj_t * pFan0, * pFan1, * pObj; 
+    int i, k, Fanins[2], Entry, Rank;
+    // map roots into their ranks
+    Vec_Int_t * vRanks = Vec_IntStartFull( Gia_ManObjNum(p) ); 
+    Vec_IntForEachEntry( vXorRoots, Entry, i )
+        Vec_IntWriteEntry( vRanks, Entry, i );
+    // map nodes into their ranks
+    Gia_ManForEachAndReverse( p, pObj, i )
+    {
+        if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            continue;
+        Rank = Vec_IntEntry( vRanks, i );
+        // skip XORs that are not part of any tree
+        if ( Rank == -1 )
+            continue;
+        // iterate through XOR inputs
+        Fanins[0] = Gia_ObjId(p, Gia_Regular(pFan0));
+        Fanins[1] = Gia_ObjId(p, Gia_Regular(pFan1));
+        for ( k = 0; k < 2; k++ )
+        {
+            Entry = Vec_IntEntry( vRanks, Fanins[k] );
+            if ( Entry == Rank ) // the same tree -- allow fanout in this tree
+                continue;
+            if ( Entry == -1 )
+                Vec_IntWriteEntry( vRanks, Fanins[k], Rank );
+            else
+                Vec_IntPush( vDoubles, Fanins[k] );
+            if ( Entry != -1 && Gia_ObjIsAnd(Gia_ManObj(p, Fanins[k])))
+            printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Fanins[k], Entry, Rank );
+        }
+    }
+    // remove duplicated entries
+    Vec_IntForEachEntry( vDoubles, Entry, i )
+        Vec_IntWriteEntry( vRanks, Entry, -1 );
+    Vec_IntFree( vDoubles );
+    return vRanks;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Wec_t * Acec_FindTreeLeaves( Gia_Man_t * p, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks )
+{
+    Vec_Bit_t * vMapXors = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Wec_t * vTreeLeaves = Vec_WecStart( Vec_IntSize(vXorRoots) );
+    Gia_Obj_t * pFan0, * pFan1, * pObj; 
+    int i, k, Fanins[2], Rank;
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+            continue;
+        Vec_BitWriteEntry( vMapXors, i, 1 );
+        Rank = Vec_IntEntry( vRanks, i );
+        // skip XORs that are not part of any tree
+        if ( Rank == -1 )
+            continue;
+        // iterate through XOR inputs
+        Fanins[0] = Gia_ObjId(p, Gia_Regular(pFan0));
+        Fanins[1] = Gia_ObjId(p, Gia_Regular(pFan1));
+        for ( k = 0; k < 2; k++ )
+        {
+            if ( Vec_BitEntry(vMapXors, Fanins[k]) )
+            {
+                assert( Rank == Vec_IntEntry(vRanks, Fanins[k]) );
+                continue;
+            }
+            Vec_WecPush( vTreeLeaves, Rank, Fanins[k] );
+        }
+    }
+    Vec_BitFree( vMapXors );
+    return vTreeLeaves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Acec_FindShadows( Gia_Man_t * p, Vec_Int_t * vRanks )
+{
+    Vec_Int_t * vShadows = Vec_IntDup( vRanks );
+    Gia_Obj_t * pObj; int i, Shad0, Shad1;
+    Gia_ManForEachCi( p, pObj, i )
+        Vec_IntWriteEntry( vShadows, Gia_ObjId(p, pObj), -1 );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Vec_IntEntry(vShadows, i) >= 0 )
+            continue;
+        Shad0 = Vec_IntEntry(vShadows, Gia_ObjFaninId0(pObj, i));
+        Shad1 = Vec_IntEntry(vShadows, Gia_ObjFaninId1(pObj, i));
+        if ( Shad0 == Shad1 && Shad0 != -1 )
+            Vec_IntWriteEntry(vShadows, i, Shad0);
+    }
+    return vShadows;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Acec_CollectSupp_rec( Gia_Man_t * p, int iNode, int Rank, Vec_Int_t * vRanks )
+{
+    Gia_Obj_t * pObj;
+    int nSize;
+    if ( Gia_ObjIsTravIdCurrentId(p, iNode) )
+        return 0;
+    Gia_ObjSetTravIdCurrentId(p, iNode);
+    pObj = Gia_ManObj(p, iNode);
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( Vec_IntEntry(vRanks, iNode) == Rank )
+        return 1;
+    nSize = Acec_CollectSupp_rec( p, Gia_ObjFaninId0(pObj, iNode), Rank, vRanks );
+    nSize += Acec_CollectSupp_rec( p, Gia_ObjFaninId1(pObj, iNode), Rank, vRanks );
+    return nSize;
+}
+Vec_Wec_t * Acec_FindNexts( Gia_Man_t * p, Vec_Int_t * vRanks, Vec_Int_t * vShadows, Vec_Wec_t * vTreeLeaves )
+{
+    Vec_Wec_t * vNexts = Vec_WecStart( Vec_WecSize(vTreeLeaves) );
+    Vec_Int_t * vTree;
+    int i, k, Node, Fanins[2], Shad0, Shad1, Rank, nSupp;
+    Vec_WecForEachLevel( vTreeLeaves, vTree, i )
+        Vec_IntForEachEntry( vTree, Node, k )
+        {
+            Gia_Obj_t * pObj = Gia_ManObj(p, Node);
+            if ( !Gia_ObjIsAnd(pObj) )
+                continue;
+            Fanins[0] = Gia_ObjFaninId0(pObj, Node);
+            Fanins[1] = Gia_ObjFaninId1(pObj, Node);
+            Shad0 = Vec_IntEntry(vShadows, Fanins[0]);
+            Shad1 = Vec_IntEntry(vShadows, Fanins[1]);
+            if ( Shad0 != Shad1 || Shad0 == -1 )
+                continue;
+            // check support size of Node in terms of the shadow of its fanins
+            Rank = Vec_IntEntry( vRanks, Node );
+            assert( Rank != Shad0 );
+            Gia_ManIncrementTravId( p );
+            nSupp = Acec_CollectSupp_rec( p, Node, Shad0, vRanks );
+            assert( nSupp > 1 );
+            if ( nSupp > 3 )
+                continue;
+            Vec_IntPushUniqueOrder( Vec_WecEntry(vNexts, Shad0), Rank );
+        }
+    return vNexts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_StructTest( Gia_Man_t * p )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c
index acbde1a0..71e0b7b3 100644
--- a/src/proof/acec/acecXor.c
+++ b/src/proof/acec/acecXor.c
@@ -44,6 +44,35 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+void Acec_CheckXors( Gia_Man_t * p, Vec_Int_t * vXors )
+{
+    Gia_Obj_t * pFan0, * pFan1;
+    Vec_Int_t * vCount2 = Vec_IntAlloc( Gia_ManObjNum(p) );
+    int i, Entry, Count = 0;
+    for ( i = 0; 4*i < Vec_IntSize(vXors); i++ )
+        if ( Vec_IntEntry(vXors, 4*i+3) == 0 )
+            Vec_IntAddToEntry( vCount2, Vec_IntEntry(vXors, 4*i), 1 );
+    Vec_IntForEachEntry( vCount2, Entry, i )
+        if ( Entry > 1 )
+            printf( "*** Obj %d has %d two-input XOR cuts.\n", i, Entry ), Count++;
+        else if ( Entry == 1 && Gia_ObjRecognizeExor(Gia_ManObj(p, i), &pFan0, &pFan1) )
+            printf( "*** Obj %d cannot be recognized as XOR.\n", i );
+    if ( Count == 0 )
+        printf( "*** There no multiple two-input XOR cuts.\n" );
+    Vec_IntFree( vCount2 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Vec_Int_t * Acec_OrderTreeRoots( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vXorRoots, Vec_Int_t * vRanks )
 {
     Vec_Int_t * vOrder = Vec_IntAlloc( Vec_IntSize(vXorRoots) );
@@ -151,7 +180,6 @@ Vec_Int_t * Acec_FindXorRoots( Gia_Man_t * p, Vec_Int_t * vXors )
         if ( !Vec_BitEntry(vMapXorIns, Vec_IntEntry(vXors, 4*i)) )
             Vec_IntPushUniqueOrder( vXorRoots, Vec_IntEntry(vXors, 4*i) );
     Vec_BitFree( vMapXorIns );
-//Vec_IntRemove( vXorRoots, 54 );
     return vXorRoots;
 }
 // collects XOR trees belonging to each of XOR roots
@@ -184,8 +212,9 @@ Vec_Int_t * Acec_RankTrees( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vXorRo
                 Vec_IntWriteEntry( vRanks, Node, Rank );
             else
                 Vec_IntPush( vDoubles, Node );
-            //if ( Entry != -1 )
-            //printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Rank );
+
+            if ( Entry != -1 && Gia_ObjIsAnd(Gia_ManObj(p, Node)))
+            printf( "Xor node %d belongs to Tree %d and Tree %d.\n", Node, Entry, Rank );
         }
     }
     // remove duplicated entries
@@ -211,6 +240,7 @@ Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vA
         for ( k = 1; k < 4; k++ )
         {
             int Fanin = Vec_IntEntry(vXors, 4*i+k);
+            //int RankFanin = Vec_IntEntry(vRanks, Fanin);
             if ( Fanin == 0 )
                 continue;
             if ( Vec_BitEntry(vMapXors, Fanin) )
@@ -218,6 +248,8 @@ Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vA
                 assert( Rank == Vec_IntEntry(vRanks, Fanin) );
                 continue;
             }
+//            if ( Vec_BitEntry(vMapXors, Fanin) && Rank == RankFanin )
+//                continue;
             if ( Vec_IntEntry(vMapMajs, Fanin) == -1 ) // no adder driving this input
                 Vec_WecPush( vXorLeaves, Rank, Fanin );
             else if ( Vec_IntEntry(vRanks, Xor) > 0 ) // save adder box
@@ -230,7 +262,26 @@ Vec_Wec_t * Acec_FindXorLeaves( Gia_Man_t * p, Vec_Int_t * vXors, Vec_Int_t * vA
         *pvAddBoxes = vAddBoxes;
     return vXorLeaves;
 }
+void Acec_CheckBoothPPs( Gia_Man_t * p, Vec_Wec_t * vLitLeaves )
+{
+    Vec_Bit_t * vMarked = Acec_MultMarkPPs( p );
+    Vec_Int_t * vLevel;
+    int i, k, iLit;
+    Vec_WecForEachLevel( vLitLeaves, vLevel, i )
+    {
+        int CountPI = 0, CountB = 0, CountNB = 0;
+        Vec_IntForEachEntry( vLevel, iLit, k )
+            if ( !Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
+                CountPI++;
+            else if ( Vec_BitEntry( vMarked, Abc_Lit2Var(iLit) ) )
+                CountB++;
+            else
+                CountNB++;
 
+        printf( "Rank %2d : Lits = %5d    PI = %d  Booth = %5d  Non-Booth = %5d\n", i, Vec_IntSize(vLevel), CountPI, CountB, CountNB );
+    }
+    Vec_BitFree( vMarked );
+}
 Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBoxes, Vec_Wec_t * vXorLeaves, Vec_Int_t * vXorRoots )
 {
     extern Vec_Int_t * Acec_TreeCarryMap( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes );
@@ -315,6 +366,8 @@ Acec_Box_t * Acec_FindBox( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vAddBox
         Vec_IntSort( vLevel, 0 );
     Vec_WecForEachLevel( pBox->vRootLits, vLevel, i )
         Vec_IntSort( vLevel, 1 );
+
+    //Acec_CheckBoothPPs( p, pBox->vLeafLits );
     return pBox;
 }
 
@@ -331,9 +384,13 @@ Acec_Box_t * Acec_ProduceBox( Gia_Man_t * p, int fVerbose )
 
     Gia_ManLevelNum(p);
 
+    //Acec_CheckXors( p, vXors );
+
     //Ree_ManPrintAdders( vAdds, 1 );
-    printf( "Detected %d full-adders and %d half-adders.  Found %d XOR-cuts.  ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    if ( fVerbose )
+        printf( "Detected %d full-adders and %d half-adders.  Found %d XOR-cuts.  ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 
     vXorRoots = Acec_OrderTreeRoots( p, vAdds, vTemp = vXorRoots, vRanks );
     Vec_IntFree( vTemp );