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

Enabling &gla for combinational miters.

This commit is contained in:
Alan Mishchenko 2012-07-18 23:52:41 -07:00
parent 6b2da3978f
commit 1fe2ba9ac0
3 changed files with 13 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/aig/gia/giaAbsGla.c
View File

@ -1391,6 +1391,8 @@ Vec_Int_t * Gla_ManTranslate( Gla_Man_t * p )
{
nUsageCount = Vec_IntEntry(p->vCoreCounts, pObj->iGiaObj);
assert( nUsageCount >= 0 );
if ( nUsageCount == 0 )
nUsageCount++;
pGiaObj = Gla_ManGiaObj( p, pObj );
if ( Gia_ObjIsConst0(pGiaObj) || Gia_ObjIsRo(p->pGia, pGiaObj) )
{
@ -1918,15 +1920,10 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
clk2 = clock();
vCore = Gla_ManUnsatCore( p, f, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status, &nConfls );
assert( (vCore != NULL) == (Status == 1) );
if ( Status == -1 ) // resource limit is reached
if ( Status == -1 || (p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit) ) // resource limit is reached
{
Gla_ManRollBack( p );
goto finish;
}
// check timeout
if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit )
{
Gla_ManRollBack( p );
if ( Gia_ManRegNum(p->pGia) > 1 ) // for comb cases, return the abstration
Gla_ManRollBack( p );
goto finish;
}
if ( vCore != NULL )
@ -2053,6 +2050,8 @@ int Gia_GlaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars, int fStartVta )
}
finish:
// analize the results
if ( p->pPars->fVerbose )
printf( "\n" );
if ( pCex == NULL )
{
if ( pAig->vGateClasses != NULL )

2
src/aig/gia/giaAbsVta.c
View File

@ -1698,6 +1698,8 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
}
finish:
// analize the results
if ( p->pPars->fVerbose )
printf( "\n" );
if ( pCex == NULL )
{
if ( Vec_PtrSize(p->vCores) == 0 )

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

@ -27576,24 +27576,12 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9GlaDerive(): There is no AIG.\n" );
return 1;
}
/*
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
/*
{
int i;
assert( pAbc->pGia->vGateClasses == NULL );
pAbc->pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAbc->pGia) );
for ( i = 0; i < Gia_ManObjNum(pAbc->pGia); i++ )
{
if ( rand() % 3 == i % 3 )
{
Vec_IntWriteEntry( pAbc->pGia->vGateClasses, i, rand() % 5 );
}
}
}
*/
if ( pAbc->pGia->vGateClasses == NULL )
{
@ -28174,12 +28162,14 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Print( -1, "There is no AIG.\n" );
return 0;
}
}
/*
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "The network is combinational.\n" );
return 0;
}
*/
if ( Gia_ManPoNum(pAbc->pGia) > 1 )
{
Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" );