summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaBalance.c54
-rw-r--r--src/base/abci/abc.c9
-rw-r--r--src/opt/dau/dau.h2
-rw-r--r--src/opt/dau/dauGia.c19
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcBmcAnd.c7
6 files changed, 78 insertions, 14 deletions
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index cdf36e7a..5855fc3d 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -36,13 +36,14 @@ struct Dam_Man_t_
{
Gia_Man_t * pGia; // user's AIG
Vec_Int_t * vNod2Set; // node ID into fanin set
- Vec_Int_t * vDiv2Nod; // div ID into fanin set
- Vec_Int_t * vSetStore; // stored multisets
- Vec_Int_t * vNodStore; // stored divisors
+ Vec_Int_t * vDiv2Nod; // div ID into root node set
+ Vec_Int_t * vSetStore; // fanin set storage
+ Vec_Int_t * vNodStore; // root node set storage
Vec_Flt_t * vCounts; // occur counts
Vec_Int_t * vNodLevR; // node reverse level
Vec_Int_t * vDivLevR; // divisor reverse level
- Vec_Que_t * vQue; // pairs by count
+ Vec_Int_t * vVisit; // visited MUXes
+ Vec_Que_t * vQue; // pairs by their weight
Hash_IntMan_t * vHash; // pair hash table
abctime clkStart; // starting the clock
int nLevelMax; // maximum level
@@ -386,11 +387,13 @@ Dam_Man_t * Dam_ManAlloc( Gia_Man_t * pGia )
Dam_Man_t * p;
p = ABC_CALLOC( Dam_Man_t, 1 );
p->clkStart = Abc_Clock();
+ p->vVisit = Vec_IntAlloc( 1000 );
p->pGia = pGia;
return p;
}
void Dam_ManFree( Dam_Man_t * p )
{
+ Vec_IntFreeP( &p->vVisit );
Vec_IntFreeP( &p->vDivLevR );
Vec_IntFreeP( &p->vNodLevR );
Vec_IntFreeP( &p->vNod2Set );
@@ -425,6 +428,10 @@ void Dam_ManCollectSets_rec( Dam_Man_t * p, int Id )
return;
if ( Gia_ObjIsMux(p->pGia, pObj) )
{
+ if ( pObj->fMark0 )
+ return;
+ pObj->fMark0 = 1;
+ Vec_IntPush( p->vVisit, Id );
Dam_ManCollectSets_rec( p, Gia_ObjFaninId0(pObj, Id) );
Dam_ManCollectSets_rec( p, Gia_ObjFaninId1(pObj, Id) );
Dam_ManCollectSets_rec( p, Gia_ObjFaninId2(p->pGia, Id) );
@@ -451,9 +458,12 @@ void Dam_ManCollectSets( Dam_Man_t * p )
p->vNod2Set = Vec_IntStart( Gia_ManObjNum(p->pGia) );
p->vSetStore = Vec_IntAlloc( Gia_ManObjNum(p->pGia) );
Vec_IntPush( p->vSetStore, -1 );
+ Vec_IntClear( p->vVisit );
Gia_ManForEachCo( p->pGia, pObj, i )
Dam_ManCollectSets_rec( p, Gia_ObjFaninId0p(p->pGia, pObj) );
ABC_FREE( p->pGia->pRefs );
+ Gia_ManForEachObjVec( p->vVisit, p->pGia, pObj, i )
+ pObj->fMark0 = 0;
}
/**Function*************************************************************
@@ -900,7 +910,7 @@ void Dam_ManUpdate( Dam_Man_t * p, int iDiv )
SeeAlso []
***********************************************************************/
-Gia_Man_t * Dam_ManMultiExtractInt( Gia_Man_t * pGia, int nNewNodesMax, int fVerbose, int fVeryVerbose )
+Gia_Man_t * Dam_ManAreaBalanceInt( Gia_Man_t * pGia, int nNewNodesMax, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew;
Dam_Man_t * p;
@@ -935,14 +945,14 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
{
Gia_Man_t * pNew0, * pNew, * pNew1, * pNew2;
// get the starting manager
- pNew0 = Gia_ManHasMapping(p) ? (Gia_Man_t *)Dsm_ManDeriveGia(p) : p;
+ pNew0 = Gia_ManHasMapping(p) ? (Gia_Man_t *)Dsm_ManDeriveGia(p, 0) : p;
if ( fVerbose ) Gia_ManPrintStats( pNew0, NULL );
// derive internal manager
pNew = fSimpleAnd ? Gia_ManDup( pNew0 ) : Gia_ManDupMuxes( pNew0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
if ( pNew0 != p ) Gia_ManStop( pNew0 );
// perform the operation
- pNew1 = Dam_ManMultiExtractInt( pNew, nNewNodesMax, fVerbose, fVeryVerbose );
+ pNew1 = Dam_ManAreaBalanceInt( pNew, nNewNodesMax, fVerbose, fVeryVerbose );
if ( fVerbose ) Gia_ManPrintStats( pNew1, NULL );
Gia_ManStop( pNew );
// derive the final result
@@ -952,6 +962,36 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
return pNew2;
}
+/**Function*************************************************************
+
+ Synopsis [Synthesis script.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Jf_Par_t Pars, * pPars = &Pars;
+ Jf_ManSetDefaultPars( pPars );
+ // perform balancing
+ pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+ // perform mapping
+ pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+// Gia_ManStop( pTemp );
+ // perform balancing
+ pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
+ if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
+ Gia_ManStop( pTemp );
+ return pNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c7a1c268..0e1c9b84 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32163,6 +32163,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nConfLimit = 0; // maximum number of conflicts at a node
pPars->fLoadCnf = 0; // dynamic CNF loading
pPars->fDumpFrames = 0; // dump unrolled timeframes
+ pPars->fUseSynth = 0; // use synthesis
pPars->fVerbose = 0; // verbose
pPars->fVeryVerbose = 0; // very verbose
pPars->fNotVerbose = 0; // skip line-by-line print-out
@@ -32170,7 +32171,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nFailOuts = 0; // the number of failed outputs
pPars->nDropOuts = 0; // the number of dropped outputs
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "SFAcdvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SFAcdsvwh" ) ) != EOF )
{
switch ( c )
{
@@ -32213,6 +32214,9 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
pPars->fDumpFrames ^= 1;
break;
+ case 's':
+ pPars->fUseSynth ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -32236,13 +32240,14 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &bmc [-SFA num] [-cdvwh]\n" );
+ Abc_Print( -2, "usage: &bmc [-SFA num] [-cdsvwh]\n" );
Abc_Print( -2, "\t performs bounded model checking\n" );
Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd );
Abc_Print( -2, "\t-c : toggle dynamic CNF loading [default = %s]\n", pPars->fLoadCnf? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping unfolded timeframes [default = %s]\n", pPars->fDumpFrames? "yes": "no" );
+ Abc_Print( -2, "\t-s : toggle synthesizing unrolled timeframes [default = %s]\n", pPars->fUseSynth? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index a928fecf..92641b71 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -89,7 +89,7 @@ extern int Dau_DsdCheck1Step( word * pTruth, int nVarsInit );
/*=== dauGia.c ==========================================================*/
extern int Dsm_ManTruthToGia( void * p, word * pTruth, Vec_Int_t * vLeaves, Vec_Int_t * vCover );
-extern void * Dsm_ManDeriveGia( void * p );
+extern void * Dsm_ManDeriveGia( void * p, int fUseMuxes );
/*=== dauMerge.c ==========================================================*/
extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index a714f622..2712effc 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -68,7 +68,10 @@ int Dau_DsdToGiaCompose_rec( Gia_Man_t * pGia, word Func, int * pFanins, int nVa
return Dau_DsdToGiaCompose_rec( pGia, Func, pFanins, nVars );
t0 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars );
t1 = Dau_DsdToGiaCompose_rec( pGia, Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars );
- return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 );
+ if ( pGia->pMuxes )
+ return Gia_ManHashMuxReal( pGia, pFanins[nVars], t1, t0 );
+ else
+ return Gia_ManHashMux( pGia, pFanins[nVars], t1, t0 );
}
/**Function*************************************************************
@@ -110,7 +113,10 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
for ( (*p)++; *p < q; (*p)++ )
{
Lit = Dau_DsdToGia_rec( pGia, pStr, p, pMatches, pLits, vCover );
- Res = Gia_ManHashXor( pGia, Res, Lit );
+ if ( pGia->pMuxes )
+ Res = Gia_ManHashXorReal( pGia, Res, Lit );
+ else
+ Res = Gia_ManHashXor( pGia, Res, Lit );
}
assert( *p == q );
return Abc_LitNotCond( Res, fCompl );
@@ -156,7 +162,10 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
assert( **p == '{' && *q == '}' );
*p = q;
}
- Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
+ if ( pGia->pMuxes )
+ Res = Gia_ManHashMuxReal( pGia, Temp[0], Temp[1], Temp[2] );
+ else
+ Res = Gia_ManHashMux( pGia, Temp[0], Temp[1], Temp[2] );
return Abc_LitNotCond( Res, fCompl );
}
if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
@@ -250,7 +259,7 @@ void Dsm_ManReportStats()
SeeAlso []
***********************************************************************/
-void * Dsm_ManDeriveGia( void * pGia )
+void * Dsm_ManDeriveGia( void * pGia, int fUseMuxes )
{
Gia_Man_t * p = (Gia_Man_t *)pGia;
Gia_Man_t * pNew, * pTemp;
@@ -263,6 +272,8 @@ void * Dsm_ManDeriveGia( void * pGia )
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ if ( fUseMuxes )
+ pNew->pMuxes = ABC_CALLOC( unsigned, pNew->nObjsAlloc );
// map primary inputs
Gia_ManFillValue(p);
Gia_ManConst0(p)->Value = 0;
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 072040c5..65c24e93 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -82,6 +82,7 @@ struct Bmc_AndPar_t_
int nConfLimit; // maximum number of conflicts at a node
int fLoadCnf; // dynamic CNF loading
int fDumpFrames; // dump unrolled timeframes
+ int fUseSynth; // use synthesis
int fVerbose; // verbose
int fVeryVerbose; // very verbose
int fNotVerbose; // skip line-by-line print-out
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 1f203373..964ba54e 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -769,11 +769,18 @@ Abc_Cex_t * Gia_ManBmcCexGen( Bmc_Mna_t * pMan, Gia_Man_t * p, int iOut )
***********************************************************************/
int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
+ extern Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
Bmc_Mna_t * p;
int nFramesMax, f, i=0, Lit, status, RetValue = -2;
abctime clk = Abc_Clock();
p = Bmc_MnaAlloc();
p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
+ if ( pPars->fUseSynth )
+ {
+ Gia_Man_t * pTemp = p->pFrames;
+ p->pFrames = Dam_ManAigSyn( pTemp, pPars->fVerbose, 0 );
+ Gia_ManStop( pTemp );
+ }
nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia);
if ( pPars->fVerbose )
{
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 10:04:20 +0000