Experiments with inductive don't-cares.

src/base/abci/abc.c

@@ -4585,13 +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 );
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     Sfm_Par_t Pars, * pPars = &Pars;
-    int c;
+    int c, fIndDCs = 0;
     // set defaults
     Sfm_ParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZNdaevwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCZNdaeivwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4692,6 +4693,9 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'e':
             pPars->fMoreEffort ^= 1;
             break;
+        case 'i':
+            fIndDCs ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -4714,16 +4718,44 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "This command can only be applied to a logic network.\n" );
         return 1;
     }
-    // modify the current network
-    if ( !Abc_NtkPerformMfs( pNtk, pPars ) )
+    if ( fIndDCs )
     {
-        Abc_Print( -1, "Resynthesis has failed.\n" );
-        return 1;
+        if ( pAbc->nIndFrames <= 1 )
+        {
+            Abc_Print( -1, "The number of k-inductive frames is not specified.\n" );
+            return 1;
+        }
+        if ( pAbc->vIndFlops == NULL )
+        {
+            Abc_Print( -1, "The set of k-inductive flops is not specified.\n" );
+            return 1;
+        }
+        if ( Vec_IntSize(pAbc->vIndFlops) != Abc_NtkLatchNum(pNtk) )
+        {
+            Abc_Print( -1, "The saved flop count (%d) does not match that of the current network (%d).\n", 
+                Vec_IntSize(pAbc->vIndFlops), Abc_NtkLatchNum(pNtk) );
+            return 1;
+        }
+        // modify the current network
+        if ( !Abc_NtkMfsAfterICheck( pNtk, pAbc->nIndFrames, pAbc->vIndFlops, pPars ) )
+        {
+            Abc_Print( -1, "Resynthesis has failed.\n" );
+            return 1;
+        }
+    }
+    else
+    {
+        // modify the current network
+        if ( !Abc_NtkPerformMfs( pNtk, pPars ) )
+        {
+            Abc_Print( -1, "Resynthesis has failed.\n" );
+            return 1;
+        }
     }
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: mfs2 [-WFDMLCZN <num>] [-daevwh]\n" );
+    Abc_Print( -2, "usage: mfs2 [-WFDMLCZN <num>] [-daeivwh]\n" );
     Abc_Print( -2, "\t           performs don't-care-based optimization of logic networks\n" );
     Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n",             pPars->nTfoLevMax );
     Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n",                pPars->nFanoutMax );
@@ -4736,6 +4768,7 @@ usage:
     Abc_Print( -2, "\t-d       : toggle performing redundancy removal [default = %s]\n",                        pPars->fRrOnly? "yes": "no" );
     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-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");
@@ -32928,10 +32961,12 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9ICheck(): The AIG is combinational.\n" );
         return 0;
     }
+    Vec_IntFreeP( &pAbc->vIndFlops );
     if ( fSearch )
-        Bmc_PerformISearch( pAbc->pGia, nFramesMax, nTimeOut, fReverse, fDump, fVerbose );
+        pAbc->vIndFlops = Bmc_PerformISearch( pAbc->pGia, nFramesMax, nTimeOut, fReverse, fDump, fVerbose );
     else
         Bmc_PerformICheck( pAbc->pGia, nFramesMax, nTimeOut, fEmpty, fVerbose );
+    pAbc->nIndFrames = nFramesMax;
     return 0;
 
 usage:

src/base/abci/abcMfs.c

@@ -49,16 +49,16 @@ Abc_Ntk_t * Abc_NtkUnrollAndDrop( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops
     Abc_Ntk_t * pNew; 
     Abc_Obj_t * pFanin, * pNode;
     Vec_Ptr_t * vNodes;
-    int i, k, f, iObj;
-    assert( Abc_NtkIsLogic(pNtk) );
-    assert( Vec_IntSize(vFlops) <= Abc_NtkLatchNum(p) );
+    int i, k, f, Value;
+    assert( Abc_NtkIsLogic(p) );
+    assert( Vec_IntSize(vFlops) == Abc_NtkLatchNum(p) );
     *piPivot = -1;
     // start the network
     pNew = Abc_NtkAlloc( p->ntkType, p->ntkFunc, 1 );
     pNew->pName = Extra_UtilStrsav(Abc_NtkName(p));
     // add the PIs corresponding to flop outputs
     Abc_NtkForEachLatchOutput( p, pNode, i )
-        Abc_ObjFanout0(pNode)->pCopy = Abc_NtkCreatePi( pNew );
+        pNode->pCopy = Abc_NtkCreatePi( pNew );
     // iterate unrolling
     vNodes = Abc_NtkDfs( p, 0 );
     for ( f = 0; f < nFrames; f++ )
@@ -71,9 +71,11 @@ Abc_Ntk_t * Abc_NtkUnrollAndDrop( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops
             Abc_ObjForEachFanin( pNode, pFanin, k )
                 Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy );
         }
+        Abc_NtkForEachCo( p, pNode, i )
+            pNode->pCopy = Abc_ObjFanin0(pNode)->pCopy;
         Abc_NtkForEachPo( p, pNode, i )
-            Abc_ObjAddFanin( Abc_NtkCreatePo(pNew), Abc_ObjFanin0(pNode)->pCopy );
-        // transfer to outputs
+            Abc_ObjAddFanin( Abc_NtkCreatePo(pNew), pNode->pCopy );
+        // transfer to flop outputs
         Abc_NtkForEachLatch( p, pNode, i )
             Abc_ObjFanout0(pNode)->pCopy = Abc_ObjFanin0(pNode)->pCopy;
         if ( f == 0 )
@@ -81,10 +83,11 @@ Abc_Ntk_t * Abc_NtkUnrollAndDrop( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops
     }
     Vec_PtrFree( vNodes );
     // add final POs
-    Vec_IntForEachEntry( vFlops, iObj, i )
+    Vec_IntForEachEntry( vFlops, Value, i )
     {
-        assert( iObj >= 0 && iObj < Abc_NtkLatchNum(p) );
-        pNode = Abc_NtkCo( p, Abc_NtkPiNum(p) + iObj );
+        if ( Value == 0 )
+            continue;
+        pNode = Abc_NtkCo( p, Abc_NtkPiNum(p) + i );
         Abc_ObjAddFanin( Abc_NtkCreatePo(pNew), Abc_ObjFanin0(pNode)->pCopy );
     }
     Abc_NtkAddDummyPiNames( pNew );
@@ -235,7 +238,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs2( Abc_Ntk_t * pNtk, int iPivot )
     // set fixed attributes
     Abc_NtkForEachNode( pNtk, pObj, i )
         if ( i >= iPivot )
-            Vec_StrWriteEntry( vFixed, i, (char)1 );
+            Vec_StrWriteEntry( vFixed, pObj->iTemp, (char)1 );
     return Sfm_NtkConstruct( vFanins, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), vFixed, NULL, vTruths );
 }
 
@@ -359,7 +362,7 @@ int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-void 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, Vec_Int_t * vFlops, Sfm_Par_t * pPars )
 {
     Sfm_Ntk_t * pp;
     int nFaninMax, nNodes;
@@ -371,7 +374,7 @@ void Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops, Sfm_
     if ( nFaninMax > 6 )
     {
         Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 6 fanins.\n" );
-        return;
+        return 0;
     }
     // derive unfolded network
     pNtk = Abc_NtkUnrollAndDrop( p, nFrames, vFlops, &iPivot );
@@ -392,8 +395,9 @@ void Abc_NtkMfsAfterICheck( Abc_Ntk_t * p, int nFrames, Vec_Int_t * vFlops, Sfm_
         if( pPars->fVerbose )
             Abc_Print( 1, "The network has %d nodes changed by \"mfs\".\n", nNodes );
     }
+    Abc_NtkDelete( pNtk );
     Sfm_NtkFree( pp );
-    return;
+    return 1;
 
 }
 

src/base/main/mainFrame.c

@@ -202,6 +202,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
             ABC_FREE( pTemp );
         Vec_PtrFree( p->vPlugInComBinPairs );
     }
+    Vec_IntFreeP( &p->vIndFlops );
     Vec_PtrFreeP( &p->vLTLProperties_global );
     Abc_FrameDeleteAllNetworks( p );
     ABC_FREE( p->pDrivingCell );

src/base/main/mainInt.h

@@ -96,6 +96,9 @@ struct Abc_Frame_t_
     // timing constraints
     char *          pDrivingCell;  // name of the driving cell
     float           MaxLoad;       // maximum output load
+    // inductive don't-cares
+    Vec_Int_t *     vIndFlops;
+    int             nIndFrames;
 
     // new code
     Gia_Man_t *     pGia;          // alternative current network as a light-weight AIG

src/sat/bmc/bmc.h

@@ -132,7 +132,7 @@ extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, i
 extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 /*=== bmcICheck.c ==========================================================*/
 extern void              Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
-extern void              Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose );
+extern Vec_Int_t *       Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose );
 /*=== bmcUnroll.c ==========================================================*/
 extern Unr_Man_t *       Unr_ManUnrollStart( Gia_Man_t * pGia, int fVerbose );
 extern Gia_Man_t *       Unr_ManUnrollFrame( Unr_Man_t * p, int f );

src/sat/bmc/bmcICheck.c

@@ -397,9 +397,9 @@ void Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRe
     Gia_ManStop( pMiter );
 //    Vec_IntFree( vLits );
 }
-void Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose )
+Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose )
 {
-    Vec_Int_t * vLits;
+    Vec_Int_t * vLits, * vFlops;
     int i, f;
     printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
         Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
@@ -426,7 +426,15 @@ void Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fRever
                 printf( "%d ", i );
         printf( "\n" );
     }       
+    // save flop indexes
+    vFlops = Vec_IntAlloc( Gia_ManRegNum(p) );
+    for ( i = 0; i < Gia_ManRegNum(p); i++ )
+        if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
+            Vec_IntPush( vFlops, 1 );
+        else
+            Vec_IntPush( vFlops, 0 );
     Vec_IntFree( vLits );
+    return vFlops;
 }
 
 ////////////////////////////////////////////////////////////////////////