Experiments with inductive don't-cares.

src/base/abci/abc.c

@@ -4585,14 +4585,14 @@ usage:
 int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars );
-    extern int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops, Sfm_Par_t * pPars );
+    extern int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t * vFlops, Sfm_Par_t * pPars );
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     Sfm_Par_t Pars, * pPars = &Pars;
-    int c, fIndDCs = 0;
+    int c, fIndDCs = 0, nFramesAdd = 0;
     // set defaults
     Sfm_ParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZNdaeivwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZNIdaeivwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4684,6 +4684,17 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nNodesMax < 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;
+            }
+            nFramesAdd = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesAdd < 0 )
+                goto usage;
+            break;
         case 'd':
             pPars->fRrOnly ^= 1;
             break;
@@ -4737,7 +4748,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 1;
         }
         // modify the current network
-        if ( !Abc_NtkMfsAfterICheck( pNtk, pAbc->nIndFrames, pAbc->vIndFlops, pPars ) )
+        if ( !Abc_NtkMfsAfterICheck( pNtk, pAbc->nIndFrames, nFramesAdd, pAbc->vIndFlops, pPars ) )
         {
             Abc_Print( -1, "Resynthesis has failed.\n" );
             return 1;
@@ -4769,6 +4780,7 @@ usage:
     Abc_Print( -2, "\t-a       : toggle minimizing area or area+edges [default = %s]\n",                        pPars->fArea? "area": "area+edges" );
     Abc_Print( -2, "\t-e       : toggle high-effort resubstitution [default = %s]\n",                           pPars->fMoreEffort? "yes": "no" );
     Abc_Print( -2, "\t-i       : toggle using inductive don't-cares [default = %s]\n",                          fIndDCs? "yes": "no" );
+    Abc_Print( -2, "\t-I       : the number of additional frames inserted [default = %d]\n",                    nFramesAdd );
     Abc_Print( -2, "\t-v       : toggle printing optimization summary [default = %s]\n",                        pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w       : toggle printing detailed stats for each node [default = %s]\n",                pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");

src/base/abci/abcMfs.c

@@ -298,12 +298,13 @@ int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkUnrollAndDrop( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops, int * piPivot )
+Abc_Ntk_t * Abc_NtkUnrollAndDrop( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t * vFlops, int * piPivot )
 {
     Abc_Ntk_t * pNtk; 
     Abc_Obj_t * pFanin, * pNode;
     Vec_Ptr_t * vNodes;
     int i, k, f, Value;
+    assert( nFramesAdd >= 0 );
     assert( Abc_NtkIsLogic(p) );
     assert( Vec_IntSize(vFlops) == Abc_NtkLatchNum(p) );
     *piPivot = -1;
@@ -315,7 +316,7 @@ Abc_Ntk_t * Abc_NtkUnrollAndDrop( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops
         pNode->pCopy = Abc_NtkCreatePi( pNtk );
     // iterate unrolling
     vNodes = Abc_NtkDfs( p, 0 );
-    for ( f = 0; f <= nFrames; f++ )
+    for ( f = 0; f <= nFrames + nFramesAdd; f++ )
     {
         if ( f > 0 )
         {
@@ -343,7 +344,7 @@ Abc_Ntk_t * Abc_NtkUnrollAndDrop( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops
         Abc_NtkForEachLatch( p, pNode, i )
             Abc_ObjFanout0(pNode)->pCopy = Abc_ObjFanin0(pNode)->pCopy;
         // add final POs
-        if ( f > 0 )
+        if ( f > nFramesAdd )
         {
             Vec_IntForEachEntry( vFlops, Value, i )
             {
@@ -427,7 +428,7 @@ void Abc_NtkReinsertNodes( Abc_Ntk_t * p, Abc_Ntk_t * pNtk, int iPivot )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops, Sfm_Par_t * pPars )
+int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, int nFramesAdd, Vec_Int_t * vFlops, Sfm_Par_t * pPars )
 {
     Sfm_Ntk_t * pp;
     int nFaninMax, nNodes;
@@ -444,7 +445,7 @@ int Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops, Sfm_P
     if ( !Abc_NtkHasSop(p) )
         Abc_NtkToSop( p, 0 );
     // derive unfolded network
-    pNtk = Abc_NtkUnrollAndDrop( p, nFrames, vFlops, &iPivot );
+    pNtk = Abc_NtkUnrollAndDrop( p, nFrames, nFramesAdd, vFlops, &iPivot );
     Io_WriteBlifLogic( pNtk, "unroll_dump.blif", 0 );
     // collect information
     pp = Abc_NtkExtractMfs2( pNtk, iPivot );