Skip to content

A
abc
Commit cfa7be1a by Alan Mishchenko
Options

Integrating synthesis into the new BMC engine.

parent 38e577f5
Showing with 78 additions and 14 deletions
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 ///
////////////////////////////////////////////////////////////////////////
......
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");
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 );
......
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;
......
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
......
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 )
{
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment