Code for profiling arithmetic circuits.

4 files changed, 32 insertions, 7 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 8f51bf81..cd397c15 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -5387,6 +5387,10 @@ SOURCE=.\src\proof\acec\acecRe.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\proof\acec\acecSt.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\proof\acec\acecUtil.c
 # End Source File
 # End Group
diff --git a/src/aig/gia/giaTruth.c b/src/aig/gia/giaTruth.c
index 56cf8785..ce06fa0b 100644
--- a/src/aig/gia/giaTruth.c
+++ b/src/aig/gia/giaTruth.c
@@ -109,13 +109,15 @@ void Gia_ObjComputeTruthTable6Lut_rec( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTem
 {
     word uTruth0, uTruth1;
     Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
-    if ( !Gia_ObjIsAnd(pObj) )
+    if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
         return;
+    Gia_ObjSetTravIdCurrentId(p, iObj);
+    assert( Gia_ObjIsAnd(pObj) );
     Gia_ObjComputeTruthTable6Lut_rec( p, Gia_ObjFaninId0p(p, pObj), vTemp );
     Gia_ObjComputeTruthTable6Lut_rec( p, Gia_ObjFaninId1p(p, pObj), vTemp );
-    uTruth0 = Vec_WrdEntry( vTemp, Gia_ObjFanin0(pObj)->Value );
+    uTruth0 = Vec_WrdEntry( vTemp, Gia_ObjFaninId0p(p, pObj) );
     uTruth0 = Gia_ObjFaninC0(pObj) ? ~uTruth0 : uTruth0;
-    uTruth1 = Vec_WrdEntry( vTemp, Gia_ObjFanin1(pObj)->Value );
+    uTruth1 = Vec_WrdEntry( vTemp, Gia_ObjFaninId1p(p, pObj) );
     uTruth1 = Gia_ObjFaninC1(pObj) ? ~uTruth1 : uTruth1;
     Vec_WrdWriteEntry( vTemp, iObj, uTruth0 & uTruth1 );
 }
@@ -124,8 +126,12 @@ word Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp )
     int i, Fanin;
     assert( Vec_WrdSize(vTemp) == Gia_ManObjNum(p) );
     assert( Gia_ObjIsLut(p, iObj) );
+    Gia_ManIncrementTravId( p );
     Gia_LutForEachFanin( p, iObj, Fanin, i )
+    {
+        Gia_ObjSetTravIdCurrentId( p, Fanin );
         Vec_WrdWriteEntry( vTemp, Fanin, s_Truth6[i] );
+    }
     assert( i <= 6 );
     Gia_ObjComputeTruthTable6Lut_rec( p, iObj, vTemp );
     return Vec_WrdEntry( vTemp, iObj );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 372e1eb4..9bb1c09a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28192,9 +28192,10 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern void Gia_ManMuxProfiling( Gia_Man_t * p );
     extern void Gia_ManProfileStructures( Gia_Man_t * p, int nLimit, int fVerbose );
-    int c, fMuxes = 0, nLimit = 0, fVerbose = 0;
+    extern void Acec_StatsCollect( Gia_Man_t * p, int fVerbose );
+    int c, fNpn = 0, fMuxes = 0, nLimit = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nmvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nnmvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28209,6 +28210,9 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nLimit < 0 )
                 goto usage;
             break;
+        case 'n':
+            fNpn ^= 1;
+            break;
         case 'm':
             fMuxes ^= 1;
             break;
@@ -28226,16 +28230,26 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9MuxProfile(): There is no AIG.\n" );
         return 1;
     }
-    if ( fMuxes )
+    if ( fNpn )
+    {
+        if ( !Gia_ManHasMapping(pAbc->pGia) || Gia_ManLutSizeMax(pAbc->pGia) >= 4 )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9MuxProfile(): Expecting AIG mapped into 3-LUTs.\n" );
+            return 1;
+        }
+        Acec_StatsCollect( pAbc->pGia, fVerbose );
+    }
+    else if ( fMuxes )
         Gia_ManMuxProfiling( pAbc->pGia );
     else
         Gia_ManProfileStructures( pAbc->pGia, nLimit, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &profile [-N num] [-mvh]\n" );
+    Abc_Print( -2, "usage: &profile [-N num] [-nmvh]\n" );
     Abc_Print( -2, "\t         profile gate structures appearing in the AIG\n" );
     Abc_Print( -2, "\t-N num : limit on class size to show [default = %d]\n", nLimit );
+    Abc_Print( -2, "\t-n     : toggle profiling NPN-classes (for 3-LUT mapped AIGs) [default = %s]\n", fNpn? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle profiling MUX structures [default = %s]\n", fMuxes? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make
index 36137676..e66bf6e8 100644
--- a/src/proof/acec/module.make
+++ b/src/proof/acec/module.make
@@ -6,4 +6,5 @@ SRC +=    src/proof/acec/acecCore.c \
     src/proof/acec/acecFadds.c \
     src/proof/acec/acecOrder.c \
     src/proof/acec/acecPolyn.c \
+    src/proof/acec/acecSt.c \
     src/proof/acec/acecUtil.c