Memory abstraction.

src/base/wlc/wlc.h

@@ -369,7 +369,7 @@ extern void           Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
 extern Vec_Int_t *    Wlc_NtkCollectMemory( Wlc_Ntk_t * p );
 extern void           Wlc_NtkPrintMemory( Wlc_Ntk_t * p );
 extern Wlc_Ntk_t *    Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p );
-extern int            Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbose );
+extern int            Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbose, int fVerbose );
 /*=== wlcNdr.c ========================================================*/
 extern Wlc_Ntk_t *    Wlc_ReadNdr( char * pFileName );
 extern void           Wlc_WriteNdr( Wlc_Ntk_t * pNtk, char * pFileName );

src/base/wlc/wlcCom.c

@@ -903,9 +903,9 @@ usage:
 int Abc_CommandMemAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
-    int c, nIterMax = 1000, fPdrVerbose = 0, fVerbose = 0;
+    int c, nIterMax = 1000, fDumpAbs = 0, fPdrVerbose = 0, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Iwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Idwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -920,6 +920,9 @@ int Abc_CommandMemAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nIterMax <= 0 )
                 goto usage;
             break;
+        case 'd':
+            fDumpAbs ^= 1;
+            break;
         case 'w':
             fPdrVerbose ^= 1;
             break;
@@ -937,14 +940,15 @@ int Abc_CommandMemAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
         return 0;
     }
-    Wlc_NtkMemAbstract( pNtk, nIterMax, fPdrVerbose, fVerbose );
+    Wlc_NtkMemAbstract( pNtk, nIterMax, fDumpAbs, fPdrVerbose, fVerbose );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%memabs [-I num] [-wvh]\n" );
+    Abc_Print( -2, "usage: %%memabs [-I num] [-dwvh]\n" );
     Abc_Print( -2, "\t         memory abstraction for word-level networks\n" );
     Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n",  nIterMax );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle dumping abstraction as an AIG [default = %s]\n",fDumpAbs? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing verbose PDR output [default = %s]\n",  fPdrVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }

src/base/wlc/wlcMem.c

@@ -355,7 +355,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_
     Wlc_Obj_t * pObj, * pCounter, * pConst, * pAdder, * pConstr = NULL;
     Vec_Int_t * vNewObjs = NULL;
     Vec_Int_t * vFanins  = Vec_IntAlloc( 100 );
-    int i, Po0, Po1, AdderBits = 4, nBits = 0;
+    int i, Po0, Po1, AdderBits = 16, nBits = 0;
 
     // mark memory nodes
     Wlc_NtkCleanMarks( p );
@@ -816,7 +816,7 @@ Wlc_Ntk_t * Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p )
     return pNewFull;
 }
 
-int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbose )
+int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbose, int fVerbose )
 {
     abctime clk = Abc_Clock();
     Wlc_Ntk_t * pNewFull, * pNew; Aig_Man_t * pAig, * pTempAig;
@@ -861,7 +861,6 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbo
         Aig_ManStop( pTempAig );
         pAbs = Gia_ManFromAigSimple( pAig );
         Aig_ManStop( pAig );
-        //Gia_AigerWrite( pAbs, "mem_abs.aig", 0, 0 );
 
         // try to prove abstracted GIA by converting it to AIG and calling PDR
         pAig = Gia_ManToAigSimple( pAbs );
@@ -875,6 +874,13 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbo
             Wlc_NtkPrintCex( p, pNew, pCex );
         Wlc_NtkFree( pNew );
 
+        if ( fDumpAbs )
+        {
+            char * pFileName = "mem_abs.aig";
+            Gia_AigerWrite( pAbs, pFileName, 0, 0 );
+            printf( "Iteration %3d: Dumped abstraction in file \"%s\" after finding CEX in frame %d.\n", nIters, pFileName, pCex ? pCex->iFrame : -1 );
+        }
+
         // check if proved or undecided
         if ( pCex == NULL ) 
         {

src/base/wlc/wlcShow.c

@@ -162,7 +162,7 @@ void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
         if ( vBold && !pNode->Mark )
             continue;
         pNode = Wlc_ObjCo2PoFo(p, i);
-        fprintf( pFile, "  NodePo%d [label = \"%s_in %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) ); 
+        fprintf( pFile, "  NodePo%d [label = \"%s%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjIsPo(pNode)? "":"_in",  Wlc_ObjRange(pNode) ); 
         fprintf( pFile, ", shape = %s", i < Wlc_NtkPoNum(p) ? "invtriangle" : "box" );
         fprintf( pFile, ", color = coral, fillcolor = coral" );
         fprintf( pFile, "];\n" );