Updates to arithmetic verification.

abclib.dsp

@@ -5507,6 +5507,10 @@ SOURCE=.\src\proof\acec\acecInt.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\proof\acec\acecMult.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\proof\acec\acecNorm.c
 # End Source File
 # Begin Source File

src/aig/gia/gia.h

@@ -1514,6 +1514,7 @@ extern int                 Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimi
 extern word                Gia_LutComputeTruth6( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTruths );
 extern word                Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp );
 extern word                Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths );
+extern word                Gia_ObjComputeTruth6Cis( Gia_Man_t * p, int iLit, Vec_Int_t * vSupp, Vec_Wrd_t * vTemp );
 extern void                Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern word *              Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern void                Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax );

src/aig/gia/giaTruth.c

@@ -139,6 +139,57 @@ word Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes truth table up to 6 inputs in terms of CIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+word Gia_ObjComputeTruth6( Gia_Man_t * p, int iObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTemp )
+{
+    int i, Fanin;
+    assert( Vec_WrdSize(vTemp) == Gia_ManObjNum(p) );
+    assert( Vec_IntSize(vSupp) <= 6 );
+    Gia_ManIncrementTravId( p );
+    Vec_IntForEachEntry( vSupp, Fanin, i )
+    {
+        Gia_ObjSetTravIdCurrentId( p, Fanin );
+        Vec_WrdWriteEntry( vTemp, Fanin, s_Truth6[i] );
+    }
+    Gia_ObjComputeTruthTable6Lut_rec( p, iObj, vTemp );
+    return Vec_WrdEntry( vTemp, iObj );
+}
+void Gia_ObjComputeTruth6CisSupport_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vSupp )
+{
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+        return;
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_IntPushOrder( vSupp, iObj );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ObjComputeTruth6CisSupport_rec( p, Gia_ObjFaninId0p(p, pObj), vSupp );
+    Gia_ObjComputeTruth6CisSupport_rec( p, Gia_ObjFaninId1p(p, pObj), vSupp );
+}
+word Gia_ObjComputeTruth6Cis( Gia_Man_t * p, int iLit, Vec_Int_t * vSupp, Vec_Wrd_t * vTemp )
+{
+    int iObj = Abc_Lit2Var(iLit); 
+    Vec_IntClear( vSupp );
+    if ( !iObj ) return Abc_LitIsCompl(iLit) ? ~(word)0 : (word)0;
+    Gia_ManIncrementTravId( p );
+    Gia_ObjComputeTruth6CisSupport_rec( p, iObj, vSupp );
+    Gia_ObjComputeTruth6( p, iObj, vSupp, vTemp );
+    return Abc_LitIsCompl(iLit) ? ~Vec_WrdEntry(vTemp, iObj) : Vec_WrdEntry(vTemp, iObj);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes truth table up to 6 inputs.]
 
   Description []

src/base/wlc/wlcBlast.c

@@ -643,6 +643,31 @@ void Wlc_IntInsert( Vec_Int_t * vProd, Vec_Int_t * vLevel, int Node, int Level )
     Vec_IntInsert( vProd,  i + 1, Node  );
     Vec_IntInsert( vLevel, i + 1, Level );
 }
+void Wlc_BlastPrintMatrix( Gia_Man_t * p, Vec_Wec_t * vProds )
+{
+    Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+    Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    Vec_Int_t * vLevel;  word Truth;
+    int i, k, iLit; 
+    Vec_WecForEachLevel( vProds, vLevel, i )
+        Vec_IntForEachEntry( vLevel, iLit, k )
+        {
+            printf( "Obj = %4d : ", Abc_Lit2Var(iLit) );
+            printf( "Compl = %d  ", Abc_LitIsCompl(iLit) );
+            printf( "Rank = %2d  ", i );
+            Truth = Gia_ObjComputeTruth6Cis( p, iLit, vSupp, vTemp );
+            Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
+            if ( Vec_IntSize(vSupp) == 4 ) printf( "    " );
+            if ( Vec_IntSize(vSupp) == 3 ) printf( "      " );
+            if ( Vec_IntSize(vSupp) <= 2 ) printf( "       " );
+            printf( "  " );
+            Vec_IntPrint( vSupp );
+            if ( k == Vec_IntSize(vLevel)-1 )
+                printf( "\n" );
+        }
+    Vec_IntFree( vSupp );
+    Vec_WrdFree( vTemp );
+}
 void Wlc_BlastReduceMatrix( Gia_Man_t * pNew, Vec_Wec_t * vProds, Vec_Wec_t * vLevels, Vec_Int_t * vRes )
 {
     Vec_Int_t * vLevel, * vProd;
@@ -812,6 +837,7 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
         Vec_WecPush( vLevels, k, 0 );
     }
     //Vec_WecPrint( vProds, 0 );
+    //Wlc_BlastPrintMatrix( pNew, vProds );
     //printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) );
     Wlc_BlastReduceMatrix( pNew, vProds, vLevels, vRes );
 

src/proof/acec/acecInt.h

@@ -70,6 +70,8 @@ struct Acec_Box_t_
 /*=== acecCo.c ========================================================*/
 extern Vec_Int_t *   Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vAddCos, Vec_Int_t ** pvIns, Vec_Int_t ** pvOuts );
 extern Vec_Wec_t *   Gia_PolynCoreOrderArray( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * vRootBoxes );
+/*=== acecMult.c ========================================================*/
+extern Vec_Int_t *   Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec_t * vRootLits );
 /*=== acecNorm.c ========================================================*/
 extern Gia_Man_t *   Acec_InsertBox( Acec_Box_t * pBox, int fAll );
 /*=== acecTree.c ========================================================*/

src/proof/acec/acecTree.c

@@ -307,16 +307,16 @@ void Acec_TreeVerifyPhaseOne( Gia_Man_t * p, Vec_Int_t * vAdds, int iBox, Vec_Bi
     if ( fFadd ) // FADD
     {
         if ( TruthXor != 0x96 )
-            printf( "Fadd %d sum is wrong.\n", iBox );
+            printf( "Fadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
         if ( TruthMaj != 0xE8 )
-            printf( "Fadd %d carry is wrong.\n", iBox );
+            printf( "Fadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
     }
     else
     {
         if ( TruthXor != 0x66 )
-            printf( "Hadd %d sum is wrong.\n", iBox );
+            printf( "Hadd %d sum %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+3 ) );
         if ( TruthMaj != 0x88 )
-            printf( "Hadd %d carry is wrong.\n", iBox );
+            printf( "Hadd %d carry %d is wrong.\n", iBox, Vec_IntEntry( vAdds, 6*iBox+4 ) );
     }
 }
 void Acec_TreeVerifyPhases( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vBoxes, Vec_Bit_t * vPhase )
@@ -356,7 +356,9 @@ void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, in
     assert( Node != 0 );
     if ( Vec_BitEntry(vVisit, Node) )
     {
-        assert( Vec_BitEntry(vPhase, Node) == fPhase );
+        //assert( Vec_BitEntry(vPhase, Node) == fPhase );
+        if ( Vec_BitEntry(vPhase, Node) != fPhase )
+            printf( "Phase check failed for node %d.\n", Node );
         return;
     }
     Vec_BitWriteEntry( vVisit, Node, 1 );
@@ -386,7 +388,12 @@ void Acec_TreePhases_rec( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vMap, in
         Acec_TreePhases_rec( p, vAdds, vMap, iObj, fPhaseThis, vPhase, vInvHadds, vVisit );
     }
     if ( Vec_BitEntry(vVisit, iXor) )
-        assert( Vec_BitEntry(vPhase, iXor) == fXorPhase );
+    {
+        //assert( Vec_BitEntry(vPhase, iXor) == fXorPhase );
+        if ( Vec_BitEntry(vPhase, iXor) != fXorPhase )
+            printf( "Phase check failed for XOR %d.\n", iXor );
+        return;
+    }
     if ( fXorPhase )
         Vec_BitWriteEntry( vPhase, iXor, fXorPhase );
 }
@@ -448,7 +455,7 @@ void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds )
     int i, k, iBox;
     Vec_WecForEachLevel( vBoxes, vLevel, i )
     {
-        printf( " %4d : {", i );
+        printf( " %4d : %2d  {", i, Vec_IntSize(vLevel) );
         Vec_IntForEachEntry( vLevel, iBox, k )
             printf( " %s%d=(%d,%d)", Vec_IntEntry(vAdds, 6*iBox+2) == 0 ? "*":"", iBox, 
                                      Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) );
@@ -461,7 +468,7 @@ void Vec_WecPrintLits( Vec_Wec_t * p )
     int i, k, Entry;
     Vec_WecForEachLevel( p, vVec, i )
     {
-        printf( " %4d : {", i );
+        printf( " %4d : %2d  {", i, Vec_IntSize(vVec) );
         Vec_IntForEachEntry( vVec, Entry, k )
             printf( " %c%d", Abc_LitIsCompl(Entry) ? '-' : '+', Abc_Lit2Var(Entry) );
         printf( " }\n" );
@@ -473,7 +480,7 @@ void Acec_PrintRootLits( Vec_Wec_t * vRoots )
     int i, k, iObj;
     Vec_WecForEachLevel( vRoots, vLevel, i )
     {
-        printf( "Rank %d : ", i );
+        printf( "Rank %d : %2d  ", i, Vec_IntSize(vLevel) );
         Vec_IntForEachEntry( vLevel, iObj, k )
         {
             int fFadd = Abc_LitIsCompl(iObj);
@@ -573,6 +580,7 @@ Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, int fVerbose )
             Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits)  );
     if ( pBox && fVerbose )
         Acec_PrintBox( pBox, vAdds );
+//    Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
     Vec_WecFreeP( &vTrees );
     Vec_IntFree( vAdds );
     return pBox;

src/proof/acec/module.make

@@ -8,6 +8,7 @@ SRC +=    src/proof/acec/acecCl.c \
     src/proof/acec/acecPool.c \
     src/proof/acec/acecCover.c \
     src/proof/acec/acecFadds.c \
+    src/proof/acec/acecMult.c \
     src/proof/acec/acecNorm.c \
     src/proof/acec/acecOrder.c \
     src/proof/acec/acecPolyn.c \