luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

New abstraction code.

This commit is contained in:
Alan Mishchenko 2011-10-19 16:03:15 +07:00
parent 397bebf8a5
commit 19ce8396f0
3 changed files with 13 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/aig/gia/giaAbs.c
View File

@ -377,9 +377,9 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
SeeAlso []
***********************************************************************/
int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf )
int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
{
extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fUseCnf, int fVerbose );
extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Vec_Int_t * vGateClasses;
Aig_Man_t * pAig;
@ -393,7 +393,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf )
*/
// perform abstraction
pAig = Gia_ManToAigSimple( pGia );
vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fUseCnf, p->fVerbose );
vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
Aig_ManStop( pAig );
// update the map

11
src/aig/saig/saigAbsGla.c
View File

@ -454,7 +454,7 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
SeeAlso []
***********************************************************************/
Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fUseCnf )
Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fNaiveCnf )
{
Aig_GlaMan_t * p;
int i;
@ -482,7 +482,7 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fUseCnf )
Vec_IntPush( p->vVar2Inf, -1 );
// CNF computation
if ( fUseCnf )
if ( !fNaiveCnf )
{
p->vLeaves = Vec_PtrAlloc( 100 );
p->vVolume = Vec_PtrAlloc( 100 );
@ -650,7 +650,7 @@ void Aig_GlaExtendIncluded( Aig_GlaMan_t * p )
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fUseCnf, int fVerbose )
Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
{
int nStart = 0;
Vec_Int_t * vResult = NULL;
@ -672,7 +672,7 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
}
// start the solver
p = Aig_GlaManStart( pAig, fUseCnf );
p = Aig_GlaManStart( pAig, fNaiveCnf );
p->nFramesMax = nFramesMax;
p->nConfLimit = nConfLimit;
p->fVerbose = fVerbose;
@ -774,7 +774,8 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
}
// prepare return value
Aig_GlaExtendIncluded( p );
if ( !fNaiveCnf )
Aig_GlaExtendIncluded( p );
vResult = p->vIncluded; p->vIncluded = NULL;
Aig_GlaManStop( p );
return vResult;

8
src/base/abci/abc.c
View File

@ -28888,7 +28888,7 @@ usage:
int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Saig_ParBmc_t Pars, * pPars = &Pars;
int c, fUseCnf = 1;
int c, fNaiveCnf = 0;
Saig_ParBmcSetDefaultParams( pPars );
pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
pPars->nFramesMax = 50; //pPars->nStart + 10;
@ -28954,7 +28954,7 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
break;
case 'c':
fUseCnf ^= 1;
fNaiveCnf ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
@ -28975,7 +28975,7 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fUseCnf );
pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf );
if ( pPars->nStart == 0 )
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
@ -28990,7 +28990,7 @@ usage:
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-c : toggle using smarter CNF computation [default = %s]\n", fUseCnf? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using naive CNF computation [default = %s]\n", fNaiveCnf? "yes": "no" );
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");
return 1;