summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaAbs.c17
-rw-r--r--src/aig/saig/saig.h2
-rw-r--r--src/aig/saig/saigAbsCba.c87
-rw-r--r--src/base/abci/abc.c16
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");
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-29 20:52:26 +0000