cec: Adding new algorithm for generating simulation vectors for SAT sweeping (SimGen)

src/aig/gia/gia.h

@@ -249,6 +249,11 @@ struct Gia_Man_t_
     int            iFirstPoId;
     int            iFirstAndObj;
     int            iFirstPoObj;
+    Vec_Str_t *    vTTISOPs;      // truth tables from ISOP computation
+    Vec_Int_t *    vTTLut;      // truth tables from ISOP computation
+    Vec_Int_t *    vMFFCsInfo;    // MFFC information
+    Vec_Int_t *    vMFFCsLuts;        // MFFCs for each lut
+    Vec_Ptr_t *    vLutsRankings;     // LUTs rankings of inputs
 };
 
 
@@ -1843,6 +1848,8 @@ extern void                 Bnd_ManPrintStats();
 // util
 extern Gia_Man_t*           Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec_Bit_t* vEI_phase, Vec_Bit_t* vEO_phase );
 
+extern int                  Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners );
+
 ABC_NAMESPACE_HEADER_END
 
 

src/aig/gia/giaResub.c

@@ -68,7 +68,7 @@ int Gia_ObjCheckMffc_rec( Gia_Man_t * p,Gia_Obj_t * pObj, int Limit, Vec_Int_t *
         return 0;
     return 1;
 }
-static inline int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners )
+int Gia_ObjCheckMffc( Gia_Man_t * p, Gia_Obj_t * pRoot, int Limit, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t * vInners )
 {
     int RetValue, iObj, i;
     Vec_IntClear( vNodes );

src/base/abci/abc.c

@@ -477,6 +477,7 @@ static int Abc_CommandAbc9Scorr              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Choice             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Sat                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SatEnum            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SimGen             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Fraig              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9CFraig             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Srm                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1276,6 +1277,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&choice",       Abc_CommandAbc9Choice,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&sat",          Abc_CommandAbc9Sat,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&satenum",      Abc_CommandAbc9SatEnum,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&fraigSimGen",      Abc_CommandAbc9SimGen,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&fraig",        Abc_CommandAbc9Fraig,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&cfraig",       Abc_CommandAbc9CFraig,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&srm",          Abc_CommandAbc9Srm,          0 );
@@ -39175,6 +39177,130 @@ int Abc_CommandAbc9SatEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Abc_CommandAbc9SimGen]
+
+  Description [This function calls SimGen tool]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+int Abc_CommandAbc9SimGen( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Cec_SimGenSetParDefault( Cec_ParSimGen_t * pPars );
+    extern Gia_Man_t * Cec_SimGenRun( Gia_Man_t * pAig, Cec_ParSimGen_t * pPars );
+
+    Cec_ParSimGen_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
+    int c;
+    Cec_SimGenSetParDefault( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "EOStiwvV" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'E':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->expId = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->expId < 0 )
+                goto usage;
+            break;
+        case 'O':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->bitwidthOutgold = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->bitwidthOutgold <= 0 )
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->bitwidthSim = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->bitwidthSim <= 0 )
+                goto usage;
+            break;
+        case 't':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-t\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->timeOutSim = atof(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->timeOutSim <= 0 )
+                goto usage;
+            break;
+        case 'i':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-i\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nMaxIter = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nMaxIter <= -2 )
+                goto usage;
+            break;
+        case 'w':
+            pPars->fUseWatchlist = 1;
+            break;
+        case 'v':
+            pPars->fVerbose = 1;
+            break;
+        case 'V':
+            pPars->fVeryVerbose = 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Fraig(): There is no AIG.\n" );
+        return 1;
+    }
+
+    pTemp = Cec_SimGenRun(pAbc->pGia, pPars );
+    if ( pAbc->pGia->pCexSeq != NULL )
+    {
+        pAbc->Status  = 0;
+        pAbc->nFrames = 0;
+        Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    }
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &fraigSimGen [-EOSsivV <num>] [-v] \n" );
+    Abc_Print( -2, "\t         performs combinational SAT sweeping applying SimGen\n" );
+    Abc_Print( -2, "\t-E num : the experiment ID for SimGen [default = %d]\n", pPars->expId );
+    Abc_Print( -2, "\t-O num : the bitwidth of the output gold [default = %d]\n", pPars->bitwidthOutgold );
+    Abc_Print( -2, "\t-S num : the bitwidth of the simulation vectors [default = %d]\n", pPars->bitwidthSim );
+    Abc_Print( -2, "\t-t num : the timeout value after which Smart Simulation Pattern Generation terminates [default = %.0f]\n", pPars->timeOutSim);
+    Abc_Print( -2, "\t-i num : the maximum number of iterations [default = %d]\n", pPars->nMaxIter );
+    Abc_Print( -2, "\t-w     : activates the watchlist feature [default = %d]\n", pPars->fUseWatchlist);
+    Abc_Print( -2, "\t-v     : verbose [default = %d]\n", pPars->fVerbose );
+    Abc_Print( -2, "\t-V     : very verbose [default = %d]\n", pPars->fVeryVerbose );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []

src/proof/cec/cec.h

@@ -201,6 +201,27 @@ struct Cec_ParSeq_t_
     int              fVerbose;      // verbose stats
 };
 
+// CEC SimGen parameters
+typedef struct Cec_ParSimGen_t_ Cec_ParSimGen_t;
+struct Cec_ParSimGen_t_
+{
+    int              fVerbose;          // verbose flag
+    int              fVeryVerbose;      // verbose flag
+    int              expId;             // experiment ID for SimGen
+    int              bitwidthOutgold;   // bitwidth of the output gold
+    int              bitwidthSim;       // bitwidth of the simulation vectors
+    int              nMaxIter;          // maximum number of iterations
+    char *           outGold;           // data containing outgold
+    float            timeOutSim;        // timeout for simulation
+    int              fUseWatchlist;     // use watchlist
+    float            fImplicationTime;  // time spent in implication
+    int              nImplicationExecution; // number of times implication was executed
+    int              nImplicationSuccess; // number of times implication was successful
+    int              nImplicationTotalChecks; // number of times implication was checked
+    int              nImplicationSuccessChecks; // number of times implication was successful
+    Cec_ParFra_t *   pCECPars;             // parameters of CEC   
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////