Added limit on the number of flops to add in one iteration of &abs_cba.

4 files changed, 118 insertions, 4 deletions

diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 37f5e315..2b5414e7 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -273,7 +273,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
     Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
     Gia_Man_t * pAbs;
     Aig_Man_t * pAig, * pOrig;
-    Vec_Int_t * vAbsFfsToAdd;
+    Vec_Int_t * vAbsFfsToAdd, * vAbsFfsToAddBest;
     // check if flop classes are given
     if ( pGia->vFlopClasses == NULL )
     {
@@ -298,6 +298,21 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars )
         Aig_ManStop( pAig );
         return 0;
     }
+    // select the most useful flops among those to be added
+    if ( p->nFfToAddMax > 0 && Vec_IntSize(vAbsFfsToAdd) > p->nFfToAddMax )
+    {
+        // compute new flops
+        Aig_Man_t * pAigBig = Gia_ManToAigSimple( pGia );
+        vAbsFfsToAddBest = Saig_ManCbaFilterFlops( pAigBig, pAig->pSeqModel, pGia->vFlopClasses, vAbsFfsToAdd, p->nFfToAddMax );
+        Aig_ManStop( pAigBig );
+        assert( Vec_IntSize(vAbsFfsToAddBest) == p->nFfToAddMax );
+        if ( p->fVerbose )
+            printf( "Filtering flops based on cost (%d -> %d).\n", Vec_IntSize(vAbsFfsToAdd), Vec_IntSize(vAbsFfsToAddBest) );
+        // update
+        Vec_IntFree( vAbsFfsToAdd );
+        vAbsFfsToAdd = vAbsFfsToAddBest;
+
+    }
     Aig_ManStop( pAig );
     // update flop classes
     Gia_ManFlopsAddToClasses( pGia->vFlopClasses, vAbsFfsToAdd );
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 36b41daf..0914c993 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -65,6 +65,7 @@ struct Saig_ParBmc_t_
     int         nPisAbstract; // the number of PIs to abstract
     int         fSolveAll;    // does not stop at the first SAT output
     int         fDropSatOuts; // replace sat outputs by constant 0
+    int         nFfToAddMax;  // max number of flops to add during CBA
     int         fVerbose;     // verbose 
     int         iFrame;       // explored up to this frame
     int         nFailOuts;    // the number of failed outputs
@@ -131,6 +132,7 @@ extern Vec_Int_t *       Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses );
 extern Vec_Int_t *       Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops );
 extern Abc_Cex_t *       Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs );
 /*=== sswAbsCba.c ==========================================================*/
+extern Vec_Int_t *       Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
 extern Abc_Cex_t *       Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose );
 extern Vec_Int_t *       Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
 extern Vec_Int_t *       Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars );
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 4d9cef57..32b9c129 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -49,6 +49,90 @@ struct Saig_ManCba_t_
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+
+/**Function*************************************************************
+
+  Synopsis    [Selects the best flops from the given array.]
+
+  Description [Selects the best 'nFfsToSelect' flops among the array 
+  'vAbsFfsToAdd' of flops that should be added to the abstraction.
+  To this end, this procedure simulates the original AIG (pAig) using
+  the given CEX (pAbsCex), which was detected for the abstraction.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect )
+{
+    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+    Vec_Int_t * vMapEntries, * vFlopCosts, * vFlopAddCosts, * vFfsToAddBest;
+    int i, k, f, Entry, iBit, * pPerm;
+    assert( Aig_ManRegNum(pAig) == Vec_IntSize(vFlopClasses) );
+    assert( Vec_IntSize(vAbsFfsToAdd) > nFfsToSelect );
+    // map previously abstracted flops into their original numbers
+    vMapEntries = Vec_IntAlloc( Vec_IntSize(vFlopClasses) );
+    Vec_IntForEachEntry( vFlopClasses, Entry, i )
+        if ( Entry == 0 )
+            Vec_IntPush( vMapEntries, i );
+    // simulate one frame at a time
+    assert( Saig_ManPiNum(pAig) + Vec_IntSize(vMapEntries) == pAbsCex->nPis );
+    vFlopCosts = Vec_IntStart( Vec_IntSize(vMapEntries) );
+    // initialize the flops
+    Aig_ManCleanMarkB(pAig);
+    Aig_ManConst1(pAig)->fMarkB = 1;
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->fMarkB = 0;
+    for ( f = 0; f < pAbsCex->iFrame; f++ )
+    {
+        // override the flop values according to the cex
+        iBit = pAbsCex->nRegs + f * pAbsCex->nPis + Saig_ManPiNum(pAig);
+        Vec_IntForEachEntry( vMapEntries, Entry, k )
+            Saig_ManLo(pAig, Entry)->fMarkB = Aig_InfoHasBit(pAbsCex->pData, iBit + k);
+        // simulate
+        Aig_ManForEachNode( pAig, pObj, k )
+            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+        Aig_ManForEachPo( pAig, pObj, k )
+            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+        // transfer
+        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMarkB = pObjRi->fMarkB;
+        // compare
+        iBit = pAbsCex->nRegs + (f + 1) * pAbsCex->nPis + Saig_ManPiNum(pAig);
+        Vec_IntForEachEntry( vMapEntries, Entry, k )
+            if ( Saig_ManLi(pAig, Entry)->fMarkB != (unsigned)Aig_InfoHasBit(pAbsCex->pData, iBit + k) )
+                Vec_IntAddToEntry( vFlopCosts, k, 1 );
+    }
+//    Vec_IntForEachEntry( vFlopCosts, Entry, i )
+//        printf( "%d ", Entry );
+//    printf( "\n" );
+    // remap the cost
+    vFlopAddCosts = Vec_IntAlloc( Vec_IntSize(vAbsFfsToAdd) );
+    Vec_IntForEachEntry( vAbsFfsToAdd, Entry, i )
+        Vec_IntPush( vFlopAddCosts, -Vec_IntEntry(vFlopCosts, Entry) );
+    // sort the flops
+    pPerm = Abc_SortCost( Vec_IntArray(vFlopAddCosts), Vec_IntSize(vFlopAddCosts) );
+    // shrink the array
+    vFfsToAddBest = Vec_IntAlloc( nFfsToSelect );
+    for ( i = 0; i < nFfsToSelect; i++ )
+    {
+//        printf( "%d ", Vec_IntEntry(vFlopAddCosts, pPerm[i]) );
+        Vec_IntPush( vFfsToAddBest, Vec_IntEntry(vAbsFfsToAdd, pPerm[i]) );
+    }
+//    printf( "\n" );
+    // cleanup
+    ABC_FREE( pPerm );
+    Vec_IntFree( vMapEntries );
+    Vec_IntFree( vFlopCosts );
+    Vec_IntFree( vFlopAddCosts );
+    Aig_ManCleanMarkB(pAig);
+    // return the computed flops
+    return vFfsToAddBest;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Duplicate with literals.]
@@ -637,7 +721,8 @@ Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * p
     }
     if ( pPars->fVerbose )
     {
-        printf( "Adding %d registers to the abstraction (total = %d).  ", Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
+        printf( "Adding %d registers to the abstraction (total = %d).  ", 
+            Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
         Abc_PrintTime( 1, "Time", clock() - clk );
     }
     return vAbsFfsToAdd;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 951c91bb..9da96731 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -28597,7 +28597,7 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nStart     = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
     pPars->nFramesMax = pPars->nStart + 10;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28634,6 +28634,17 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nConfLimit < 0 ) 
                 goto usage;
             break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFfToAddMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFfToAddMax < 0 ) 
+                goto usage;
+            break;
         case 'T':
             if ( globalUtilOptind >= argc )
             {
@@ -28671,11 +28682,12 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &abs_cba [-SFCT num] [-vh]\n" );
+    Abc_Print( -2, "usage: &abs_cba [-SFCMT num] [-vh]\n" );
     Abc_Print( -2, "\t         refines abstracted flop map with proof-based abstraction\n" );
     Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
     Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
     Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");