From d52dafa6c2365837543f15be7abd274f8654ba14 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 12 Jan 2017 16:12:48 +0700
Subject: Updates to arithmetic verification.

---
 src/proof/acec/acecTree.c | 26 +++++++++++++++++---------
 1 file changed, 17 insertions(+), 9 deletions(-)

(limited to 'src/proof/acec/acecTree.c')

diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index 1c0af00a..53e1cb60 100644
--- a/src/proof/acec/acecTree.c
+++ b/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;
-- 
cgit v1.2.3