Skip to content

A
abc
Commit 6f0b87dd by Alan Mishchenko
Options

New abstraction code.

parent e4bd4d54
Showing with 521 additions and 250 deletions
src/aig/gia/gia.h
...@@ -603,6 +603,7 @@ Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia ); ...@@ -603,6 +603,7 @@ Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose ); int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame ); extern int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit, int nTimeLimit, int fVerbose, int * piFrame );
extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars ); extern int Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars );
/*=== giaAiger.c ===========================================================*/ /*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName ); extern int Gia_FileSize( char * pFileName );
extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck ); extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
...@@ -659,6 +660,7 @@ extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); ...@@ -659,6 +660,7 @@ extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias );
extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes );
extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ); extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
extern Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses );
/*=== giaEnable.c ==========================================================*/ /*=== giaEnable.c ==========================================================*/
extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ); extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );
......
src/aig/gia/giaAbs.c
...@@ -366,6 +366,42 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit ...@@ -366,6 +366,42 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
} }
/**Function*************************************************************
Synopsis [Derive unrolled timeframes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars )
{
extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
Vec_Int_t * vGateClasses;
Aig_Man_t * pAig;
/*
// check if flop classes are given
if ( pGia->vGateClasses == NULL )
{
Abc_Print( 0, "Initial gate map is not given. Trivial abstraction is assumed.\n" );
pGia->vGateClasses = Vec_IntStart( Gia_ManObjNum(pGia) );
}
*/
// perform abstraction
pAig = Gia_ManToAigSimple( pGia );
vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
Aig_ManStop( pAig );
// update the map
Vec_IntFreeP( &pGia->vGateClasses );
pGia->vGateClasses = vGateClasses;
return 1;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/gia/giaAig.c
...@@ -350,6 +350,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p ) ...@@ -350,6 +350,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p )
else else
assert( 0 ); assert( 0 );
pObj->Value = Gia_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) ); pObj->Value = Gia_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) );
assert( i == 0 || Aig_ObjId(ppNodes[i]) == i );
} }
Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) ); Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
ABC_FREE( ppNodes ); ABC_FREE( ppNodes );
......
src/aig/gia/giaDup.c
...@@ -1586,8 +1586,8 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) ...@@ -1586,8 +1586,8 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
Synopsis [Performs abstraction of the AIG to preserve the included gates.] Synopsis [Performs abstraction of the AIG to preserve the included gates.]
Description [The array contains PIs, LOs, and internal nodes included. Description [The array contains 1 for those objects (const, RO, AND)
0=unsed, 1=PI, 2=PPI, 3=FF, 4=AND.] that are included in the abstraction; 0, otherwise.]
SideEffects [] SideEffects []
...@@ -1596,51 +1596,110 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) ...@@ -1596,51 +1596,110 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{ {
Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes;
Gia_Man_t * pNew, * pTemp; Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i, nFlops = 0; int i, nFlops = 0;
assert( Gia_ManPoNum(p) == 1 ); assert( Gia_ManPoNum(p) == 1 );
Gia_ManFillValue( p ); assert( Vec_IntSize(vGateClasses) == Gia_ManObjNum(p) );
// create included objects and their fanins
vAssigned = Gia_GlaCollectAssigned( p, vGateClasses );
// create additional arrays
vPis = Vec_IntAlloc( 1000 );
vPPis = Vec_IntAlloc( 1000 );
vFlops = Vec_IntAlloc( 1000 );
vNodes = Vec_IntAlloc( 1000 );
Gia_ManForEachObjVec( vAssigned, p, pObj, i )
{
if ( Gia_ObjIsPi(p, pObj) )
Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
else if ( !Vec_IntEntry(vGateClasses, Gia_ObjId(p,pObj)) )
Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
else if ( Gia_ObjIsAnd(pObj) )
Vec_IntPush( vNodes, Gia_ObjId(p,pObj) );
else if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vFlops, Gia_ObjId(p,pObj) );
else assert( Gia_ObjIsConst0(pObj) );
}
// start the new manager // start the new manager
pNew = Gia_ManStart( 5000 ); pNew = Gia_ManStart( 5000 );
pNew->pName = Gia_UtilStrsav( p->pName ); pNew->pName = Gia_UtilStrsav( p->pName );
// create PIs // create constant
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0; Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i ) // create PIs
if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 1 ) Gia_ManForEachObjVec( vPis, p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew); pObj->Value = Gia_ManAppendCi(pNew);
// create additional PIs // create additional PIs
Gia_ManForEachPi( p, pObj, i ) Gia_ManForEachObjVec( vPPis, p, pObj, i )
if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 2 )
pObj->Value = Gia_ManAppendCi(pNew); pObj->Value = Gia_ManAppendCi(pNew);
// create ROs // create ROs
Gia_ManForEachRo( p, pObj, i ) Gia_ManForEachObjVec( vFlops, p, pObj, i )
if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 3 )
pObj->Value = Gia_ManAppendCi(pNew); pObj->Value = Gia_ManAppendCi(pNew);
// create POs // create internal nodes
Gia_ManHashAlloc( pNew ); Gia_ManForEachObjVec( vNodes, p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
// create PO
Gia_ManForEachPo( p, pObj, i ) Gia_ManForEachPo( p, pObj, i )
{ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
// create RIs // create RIs
Gia_ManForEachRo( p, pObj, i ) Gia_ManForEachObjVec( vFlops, p, pObj, i )
if ( Vec_IntEntry(vGateClasses, Gia_ObjId(p, pObj)) == 3 ) Gia_ObjRoToRi(p, pObj)->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ObjRoToRi(p, pObj)) );
{ Gia_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
pObj = Gia_ObjRoToRi(p, pObj);
Gia_ManDupAbsFlops_rec( pNew, Gia_ObjFanin0(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
nFlops++;
}
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, nFlops );
// clean up // clean up
pNew = Gia_ManSeqCleanup( pTemp = pNew ); pNew = Gia_ManSeqCleanup( pTemp = pNew );
assert( Gia_ManObjNum(pTemp) == Gia_ManObjNum(pNew) );
Gia_ManStop( pTemp ); Gia_ManStop( pTemp );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vFlops );
Vec_IntFree( vNodes );
Vec_IntFree( vAssigned );
return pNew; return pNew;
} }
/**Function*************************************************************
Synopsis [Returns the array of neighbors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vAssigned;
Gia_Obj_t * pObj;
int i, Entry;
vAssigned = Vec_IntAlloc( 1000 );
Vec_IntForEachEntry( vGateClasses, Entry, i )
{
if ( Entry == 0 )
continue;
assert( Entry == 1 );
pObj = Gia_ManObj( p, i );
Vec_IntPush( vAssigned, Gia_ObjId(p, pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, pObj) );
Vec_IntPush( vAssigned, Gia_ObjFaninId1p(p, pObj) );
}
else if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vAssigned, Gia_ObjFaninId0p(p, Gia_ObjRoToRi(p, pObj)) );
else assert( Gia_ObjIsConst0(pObj) );
}
Vec_IntUniqify( vAssigned );
return vAssigned;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/aig/gia/giaMan.c
...@@ -179,7 +179,8 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) ...@@ -179,7 +179,8 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p )
} }
Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 ); Counter0 = Vec_IntCountEntry( p->vFlopClasses, 0 );
Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 ); Counter1 = Vec_IntCountEntry( p->vFlopClasses, 1 );
printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d ", Counter0, Counter1 ); printf( "Flop-level abstraction: Excluded FFs = %d Included FFs = %d (%.2f %%) ",
Counter0, Counter1, 100.0*Counter1/(Counter0 + Counter1 + 1) );
if ( Counter0 + Counter1 < Gia_ManRegNum(p) ) if ( Counter0 + Counter1 < Gia_ManRegNum(p) )
printf( "and there are other FF classes..." ); printf( "and there are other FF classes..." );
printf( "\n" ); printf( "\n" );
...@@ -198,7 +199,10 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p ) ...@@ -198,7 +199,10 @@ void Gia_ManPrintFlopClasses( Gia_Man_t * p )
***********************************************************************/ ***********************************************************************/
void Gia_ManPrintGateClasses( Gia_Man_t * p ) void Gia_ManPrintGateClasses( Gia_Man_t * p )
{ {
int i, Counter[5]; Vec_Int_t * vAssigned, * vPis, * vPPis, * vFlops, * vNodes;
Gia_Obj_t * pObj;
int i;
if ( p->vGateClasses == NULL ) if ( p->vGateClasses == NULL )
return; return;
if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) ) if ( Vec_IntSize(p->vGateClasses) != Gia_ManObjNum(p) )
...@@ -206,12 +210,38 @@ void Gia_ManPrintGateClasses( Gia_Man_t * p ) ...@@ -206,12 +210,38 @@ void Gia_ManPrintGateClasses( Gia_Man_t * p )
printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" ); printf( "Gia_ManPrintGateClasses(): The number of flop map entries differs from the number of flops.\n" );
return; return;
} }
for ( i = 0; i < 5; i++ )
Counter[i] = Vec_IntCountEntry( p->vGateClasses, i ); // create included objects and their fanins
printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d AND = %d Unused = %d\n", vAssigned = Gia_GlaCollectAssigned( p, p->vGateClasses );
Counter[1], Counter[2], Counter[3], Counter[4], Counter[0] );
if ( Counter[0] + Counter[1] + Counter[2] + Counter[3] + Counter[4] != Gia_ManObjNum(p) ) // create additional arrays
printf( "Gia_ManPrintGateClasses(): Mismatch in the object count.\n" ); vPis = Vec_IntAlloc( 1000 );
vPPis = Vec_IntAlloc( 1000 );
vFlops = Vec_IntAlloc( 1000 );
vNodes = Vec_IntAlloc( 1000 );
Gia_ManForEachObjVec( vAssigned, p, pObj, i )
{
if ( Gia_ObjIsPi(p, pObj) )
Vec_IntPush( vPis, Gia_ObjId(p,pObj) );
else if ( !Vec_IntEntry(p->vGateClasses, Gia_ObjId(p,pObj)) )
Vec_IntPush( vPPis, Gia_ObjId(p,pObj) );
else if ( Gia_ObjIsAnd(pObj) )
Vec_IntPush( vNodes, Gia_ObjId(p,pObj) );
else if ( Gia_ObjIsRo(p, pObj) )
Vec_IntPush( vFlops, Gia_ObjId(p,pObj) );
else assert( Gia_ObjIsConst0(pObj) );
}
printf( "Gate-level abstraction: PI = %d PPI = %d FF = %d (%.2f %%) AND = %d (%.2f %%)\n",
Vec_IntSize(vPis), Vec_IntSize(vPPis),
Vec_IntSize(vFlops), 100.0*Vec_IntSize(vFlops)/(Gia_ManRegNum(p)+1),
Vec_IntSize(vNodes), 100.0*Vec_IntSize(vNodes)/(Gia_ManAndNum(p)+1) );
Vec_IntFree( vPis );
Vec_IntFree( vPPis );
Vec_IntFree( vFlops );
Vec_IntFree( vNodes );
Vec_IntFree( vAssigned );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/aig/saig/saigAbsGla.c
...@@ -37,20 +37,24 @@ struct Aig_GlaMan_t_ ...@@ -37,20 +37,24 @@ struct Aig_GlaMan_t_
int nFramesMax; int nFramesMax;
int fVerbose; int fVerbose;
// abstraction // abstraction
Vec_Int_t * vAbstr; // collects objects used in the abstraction Vec_Int_t * vAssigned; // collects objects whose SAT variables have been created
Vec_Int_t * vUsed; // maps object ID into its status (0=unused; 1=used) Vec_Int_t * vIncluded; // maps obj ID into its status (0=unused; 1=included in abstraction)
// components
Vec_Int_t * vPis; // primary inputs Vec_Int_t * vPis; // primary inputs
Vec_Int_t * vPPis; // pseudo primary inputs Vec_Int_t * vPPis; // pseudo primary inputs
Vec_Int_t * vFlops; // flops Vec_Int_t * vFlops; // flops
Vec_Int_t * vNodes; // nodes Vec_Int_t * vNodes; // nodes
// unrolling // unrolling
int iFrame;
int nFrames; int nFrames;
Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID Vec_Int_t * vObj2Vec; // maps obj ID into its vec ID
Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID) Vec_Int_t * vVec2Var; // maps vec ID into its sat Var (nFrames per vec ID)
Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID Vec_Int_t * vVar2Inf; // maps sat Var into its frame and obj ID
// SAT solver // SAT solver
sat_solver * pSat; sat_solver * pSat;
// statistics
int timeSat;
int timeRef;
int timeTotal;
}; };
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -59,121 +63,6 @@ struct Aig_GlaMan_t_ ...@@ -59,121 +63,6 @@ struct Aig_GlaMan_t_
/**Function************************************************************* /**Function*************************************************************
Synopsis [Performs abstraction of the AIG to preserve the included gates.]
Description [The array contains 1 if the obj is included; 0 otherwise.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_GlaDupAbsGates( Aig_Man_t * p, Vec_Int_t * vUsed, int * pnRealPis )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i, nFlops = 0, RetValue;
assert( Aig_ManPoNum(p) == 1 );
// start the new manager
pNew = Aig_ManStart( 5000 );
pNew->pName = Aig_UtilStrsav( p->pName );
// create constant
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
// create PIs
Saig_ManForEachPi( p, pObj, i )
if ( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) )
pObj->pData = Aig_ObjCreatePi(pNew);
if ( pnRealPis )
*pnRealPis = Aig_ManPiNum(pNew);
// create additional PIs
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
if ( Vec_IntEntry(vUsed, Aig_ObjId(pObjLo)) && !Vec_IntEntry(vUsed, Aig_ObjId(pObjLi)) )
pObjLo->pData = Aig_ObjCreatePi(pNew);
Aig_ManForEachNode( p, pObj, i )
{
if ( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) &&
(!Vec_IntEntry(vUsed, Aig_ObjFaninId0(pObj)) ||
!Vec_IntEntry(vUsed, Aig_ObjFaninId1(pObj))) )
pObj->pData = Aig_ObjCreatePi(pNew);
}
// create ROs
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
if ( Vec_IntEntry(vUsed, Aig_ObjId(pObjLo)) && Vec_IntEntry(vUsed, Aig_ObjId(pObjLi)) )
pObjLo->pData = Aig_ObjCreatePi(pNew), nFlops++;
// create internal nodes
Aig_ManForEachNode( p, pObj, i )
{
if ( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) &&
Vec_IntEntry(vUsed, Aig_ObjFaninId0(pObj)) &&
Vec_IntEntry(vUsed, Aig_ObjFaninId1(pObj)) )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
// create PO
Saig_ManForEachPo( p, pObj, i )
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
// create RIs
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
if ( Vec_IntEntry(vUsed, Aig_ObjId(pObjLo)) && Vec_IntEntry(vUsed, Aig_ObjId(pObjLi)) )
pObjLi->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObjLi) );
Aig_ManSetRegNum( pNew, nFlops );
// clean up
RetValue = Aig_ManCleanup( pNew );
assert( RetValue == 0 );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i, nFlops = 0, RetValue;
assert( Aig_ManPoNum(p) == 1 );
// start the new manager
pNew = Aig_ManStart( 5000 );
pNew->pName = Aig_UtilStrsav( p->pAig->pName );
// create constant
Aig_ManCleanData( p->pAig );
Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
// create PIs
Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// create additional PIs
Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// create ROs
Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// create internal nodes
Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create PO
Saig_ManForEachPo( p->pAig, pObj, i )
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
// create RIs
Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i )
Saig_ObjLoToLi(p->pAig, pObj)->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(Saig_ObjLoToLi(p->pAig, pObj)) );
Aig_ManSetRegNum( pNew, Vec_IntSize(p->vFlops) );
// clean up
RetValue = Aig_ManCleanup( pNew );
assert( RetValue == 0 );
return pNew;
}
/**Function*************************************************************
Synopsis [Adds constant to the solver.] Synopsis [Adds constant to the solver.]
Description [] Description []
...@@ -183,7 +72,7 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p ) ...@@ -183,7 +72,7 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl ) static inline int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl )
{ {
lit Lit = toLitCond( iVar, fCompl ); lit Lit = toLitCond( iVar, fCompl );
if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) ) if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
...@@ -202,7 +91,7 @@ int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl ) ...@@ -202,7 +91,7 @@ int Aig_GlaAddConst( sat_solver * pSat, int iVar, int fCompl )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) static inline int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
{ {
lit Lits[2]; lit Lits[2];
...@@ -230,7 +119,7 @@ int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) ...@@ -230,7 +119,7 @@ int Aig_GlaAddBuffer( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ) static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
{ {
lit Lits[3]; lit Lits[3];
...@@ -253,6 +142,155 @@ int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fComp ...@@ -253,6 +142,155 @@ int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fComp
return 1; return 1;
} }
/**Function*************************************************************
Synopsis [Returns the array of neighbors.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Aig_GlaCollectAssigned( Aig_Man_t * p, Vec_Int_t * vGateClasses )
{
Vec_Int_t * vAssigned;
Aig_Obj_t * pObj;
int i, Entry;
vAssigned = Vec_IntAlloc( 1000 );
Vec_IntForEachEntry( vGateClasses, Entry, i )
{
if ( Entry == 0 )
continue;
assert( Entry == 1 );
pObj = Aig_ManObj( p, i );
Vec_IntPush( vAssigned, Aig_ObjId(pObj) );
if ( Aig_ObjIsNode(pObj) )
{
Vec_IntPush( vAssigned, Aig_ObjFaninId0(pObj) );
Vec_IntPush( vAssigned, Aig_ObjFaninId1(pObj) );
}
else if ( Saig_ObjIsLo(p, pObj) )
Vec_IntPush( vAssigned, Aig_ObjFaninId0(Saig_ObjLoToLi(p, pObj)) );
else assert( Aig_ObjIsConst1(pObj) );
}
Vec_IntUniqify( vAssigned );
return vAssigned;
}
/**Function*************************************************************
Synopsis [Derives abstraction components (PIs, PPIs, flops, nodes).]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
{
Aig_Obj_t * pObj;
int i, Entry;
/*
// make sure every neighbor of included objects is assigned a variable
Vec_IntForEachEntry( p->vIncluded, Entry, i )
{
if ( Entry == 0 )
continue;
assert( Entry == 1 );
pObj = Aig_ManObj( p->pAig, i );
if ( Vec_IntFind( p->vAssigned, Aig_ObjId(pObj) ) == -1 )
printf( "Aig_GlaCollectAbstr(): Object not found\n" );
if ( Aig_ObjIsNode(pObj) )
{
if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObj) ) == -1 )
printf( "Aig_GlaCollectAbstr(): Node's fanin is not found\n" );
if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId1(pObj) ) == -1 )
printf( "Aig_GlaCollectAbstr(): Node's fanin is not found\n" );
}
else if ( Saig_ObjIsLo(p->pAig, pObj) )
{
Aig_Obj_t * pObjLi;
pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
if ( Vec_IntFind( p->vAssigned, Aig_ObjFaninId0(pObjLi) ) == -1 )
printf( "Aig_GlaCollectAbstr(): Flop's fanin is not found\n" );
}
else assert( Aig_ObjIsConst1(pObj) );
}
*/
Vec_IntClear( p->vPis );
Vec_IntClear( p->vPPis );
Vec_IntClear( p->vFlops );
Vec_IntClear( p->vNodes );
Vec_IntForEachEntryReverse( p->vAssigned, Entry, i )
{
pObj = Aig_ManObj( p->pAig, Entry );
if ( Saig_ObjIsPi(p->pAig, pObj) )
Vec_IntPush( p->vPis, Aig_ObjId(pObj) );
else if ( !Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) )
Vec_IntPush( p->vPPis, Aig_ObjId(pObj) );
else if ( Aig_ObjIsNode(pObj) )
Vec_IntPush( p->vNodes, Aig_ObjId(pObj) );
else if ( Saig_ObjIsLo(p->pAig, pObj) )
Vec_IntPush( p->vFlops, Aig_ObjId(pObj) );
else assert( Aig_ObjIsConst1(pObj) );
}
}
/**Function*************************************************************
Synopsis [Derives abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i, nFlops = 0, RetValue;
assert( Saig_ManPoNum(p->pAig) == 1 );
// start the new manager
pNew = Aig_ManStart( 5000 );
pNew->pName = Aig_UtilStrsav( p->pAig->pName );
// create constant
Aig_ManCleanData( p->pAig );
Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
// create PIs
Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// create additional PIs
Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// create ROs
Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i )
pObj->pData = Aig_ObjCreatePi(pNew);
// create internal nodes
Aig_ManForEachObjVec( p->vNodes, p->pAig, pObj, i )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
// create PO
Saig_ManForEachPo( p->pAig, pObj, i )
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
// create RIs
Aig_ManForEachObjVec( p->vFlops, p->pAig, pObj, i )
{
assert( Saig_ObjIsLo(p->pAig, pObj) );
pObj = Saig_ObjLoToLi( p->pAig, pObj );
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
}
Aig_ManSetRegNum( pNew, Vec_IntSize(p->vFlops) );
// clean up
RetValue = Aig_ManCleanup( pNew );
assert( RetValue == 0 );
return pNew;
}
/**Function************************************************************* /**Function*************************************************************
...@@ -268,17 +306,15 @@ int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fComp ...@@ -268,17 +306,15 @@ int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fComp
int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
{ {
int i, iVecId, iSatVar; int i, iVecId, iSatVar;
if ( !Vec_IntEntry(p->vUsed, Aig_ObjId(pObj)) ) assert( k < p->nFrames );
{
Vec_IntWriteEntry( p->vUsed, Aig_ObjId(pObj), 1 );
Vec_IntPush( p->vAbstr, Aig_ObjId(pObj) );
}
iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) ); iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
if ( iVecId == 0 ) if ( iVecId == 0 )
{ {
iVecId = Vec_IntSize( p->vVec2Var ) / p->nFrames; iVecId = Vec_IntSize( p->vVec2Var ) / p->nFrames;
for ( i = 0; i < p->nFrames; i++ ) for ( i = 0; i < p->nFrames; i++ )
Vec_IntPush( p->vVec2Var, 0 ); Vec_IntPush( p->vVec2Var, 0 );
Vec_IntWriteEntry( p->vObj2Vec, Aig_ObjId(pObj), iVecId );
Vec_IntPushOrderReverse( p->vAssigned, Aig_ObjId(pObj) );
} }
iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + k ); iSatVar = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + k );
if ( iSatVar == 0 ) if ( iSatVar == 0 )
...@@ -304,23 +340,38 @@ int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) ...@@ -304,23 +340,38 @@ int Aig_GlaFetchVar( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
***********************************************************************/ ***********************************************************************/
int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k ) int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
{ {
assert( Vec_IntEntry(vUsed, Aig_ObjId(pObj)) ); if ( k == p->nFrames )
{
int i, j, nVecIds = Vec_IntSize( p->vVec2Var ) / p->nFrames;
Vec_Int_t * vVec2VarNew = Vec_IntAlloc( 4 * nVecIds * p->nFrames );
for ( i = 0; i < nVecIds; i++ )
{
for ( j = 0; j < p->nFrames; j++ )
Vec_IntPush( vVec2VarNew, Vec_IntEntry( p->vVec2Var, i * p->nFrames + j ) );
for ( j = 0; j < p->nFrames; j++ )
Vec_IntPush( vVec2VarNew, i ? 0 : -1 );
}
Vec_IntFree( p->vVec2Var );
p->vVec2Var = vVec2VarNew;
p->nFrames *= 2;
}
assert( k < p->nFrames );
assert( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) );
if ( Aig_ObjIsConst1(pObj) ) if ( Aig_ObjIsConst1(pObj) )
return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 0 ); return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 0 );
if ( Saig_ObjIsPi(p->pAig, pObj) )
return 1;
if ( Saig_ObjIsLo(p->pAig, pObj) ) if ( Saig_ObjIsLo(p->pAig, pObj) )
{ {
Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj); Aig_Obj_t * pObjLi = Saig_ObjLoToLi(p->pAig, pObj);
if ( k == 0 ) if ( k == 0 )
{
Aig_GlaFetchVar( p, Aig_ObjFanin0(pObjLi), 0 );
return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 1 ); return Aig_GlaAddConst( p->pSat, Aig_GlaFetchVar(p, pObj, k), 1 );
if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObjLi)) ) }
return 1; return Aig_GlaAddBuffer( p->pSat, Aig_GlaFetchVar(p, pObj, k),
return Aig_GlaAddBuffer( p->pSat, Aig_GlaFetchVar(p, pObj, k), Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1), Aig_ObjFaninC0(pObjLi) ); Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1),
Aig_ObjFaninC0(pObjLi) );
} }
assert( Aig_ObjIsNode(pObj) ); assert( Aig_ObjIsNode(pObj) );
if ( Vec_IntEntry(p->vUsed, Aig_ObjFaninId0(pObj)) && Vec_IntEntry(p->vUsed, Aig_ObjFaninId1(pObj)) )
return 0;
return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k), return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k),
Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k), Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k),
Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k), Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k),
...@@ -345,9 +396,9 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig ) ...@@ -345,9 +396,9 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig )
p = ABC_CALLOC( Aig_GlaMan_t, 1 ); p = ABC_CALLOC( Aig_GlaMan_t, 1 );
p->pAig = pAig; p->pAig = pAig;
p->vAbstr = Vec_IntAlloc( 1000 ); p->vAssigned = Vec_IntAlloc( 1000 );
p->vUsed = Vec_IntStart( Aig_ManObjNumMax(pAig) ); p->vIncluded = Vec_IntStart( Aig_ManObjNumMax(pAig) );
p->nFrames = 16; p->nFrames = 32;
p->vPis = Vec_IntAlloc( 1000 ); p->vPis = Vec_IntAlloc( 1000 );
p->vPPis = Vec_IntAlloc( 1000 ); p->vPPis = Vec_IntAlloc( 1000 );
...@@ -367,7 +418,7 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig ) ...@@ -367,7 +418,7 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig )
// start the SAT solver // start the SAT solver
p->pSat = sat_solver_new(); p->pSat = sat_solver_new();
sat_solver_setnvars( p->pSat, 1000 ); sat_solver_setnvars( p->pSat, 256 );
return p; return p;
} }
...@@ -385,8 +436,8 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig ) ...@@ -385,8 +436,8 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig )
***********************************************************************/ ***********************************************************************/
void Aig_GlaManStop( Aig_GlaMan_t * p ) void Aig_GlaManStop( Aig_GlaMan_t * p )
{ {
Vec_IntFreeP( &p->vAbstr ); Vec_IntFreeP( &p->vAssigned );
Vec_IntFreeP( &p->vUsed ); Vec_IntFreeP( &p->vIncluded );
Vec_IntFreeP( &p->vPis ); Vec_IntFreeP( &p->vPis );
Vec_IntFreeP( &p->vPPis ); Vec_IntFreeP( &p->vPPis );
...@@ -413,57 +464,47 @@ void Aig_GlaManStop( Aig_GlaMan_t * p ) ...@@ -413,57 +464,47 @@ void Aig_GlaManStop( Aig_GlaMan_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Aig_GlaCollectAbstr( Aig_GlaMan_t * p ) Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p, int iFrame )
{ {
Aig_Obj_t * pObj, * pObjLi, * pObjLo; Abc_Cex_t * pCex;
int i; Aig_Obj_t * pObj;
Vec_IntClear( p->vPis ); int i, f, iVecId, iSatId;
Vec_IntClear( p->vPPis ); pCex = Abc_CexAlloc( Vec_IntSize(p->vFlops), Vec_IntSize(p->vPis) + Vec_IntSize(p->vPPis), iFrame+1 );
Vec_IntClear( p->vFlops ); pCex->iFrame = iFrame;
Vec_IntClear( p->vNodes ); Aig_ManForEachObjVec( p->vPis, p->pAig, pObj, i )
Saig_ManForEachPi( p->pAig, pObj, i )
if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObj)) )
Vec_IntPush( p->vPis, Aig_ObjId(pObj) );
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObjLo)) )
{ {
if ( Vec_IntEntry(p->vUsed, Aig_ObjFaninId0(pObjLi)) ) iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
Vec_IntPush( p->vFlops, Aig_ObjId(pObjLo) ); assert( iVecId > 0 );
else for ( f = 0; f <= iFrame; f++ )
Vec_IntPush( p->vPPis, Aig_ObjId(pObjLo) ); {
iSatId = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + f );
if ( iSatId == 0 )
continue;
assert( iSatId > 0 );
if ( sat_solver_var_value(p->pSat, iSatId) )
Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + i );
} }
}
Aig_ManForEachNode( p->pAig, pObj, i ) Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i )
if ( Vec_IntEntry(p->vUsed, Aig_ObjId(pObj)) )
{ {
if ( Vec_IntEntry(p->vUsed, Aig_ObjFaninId0(pObj)) && Vec_IntEntry(p->vUsed, Aig_ObjFaninId1(pObj)) ) iVecId = Vec_IntEntry( p->vObj2Vec, Aig_ObjId(pObj) );
Vec_IntPush( p->vNodes, Aig_ObjId(pObjLo) ); assert( iVecId > 0 );
else for ( f = 0; f <= iFrame; f++ )
Vec_IntPush( p->vPPis, Aig_ObjId(pObjLo) ); {
iSatId = Vec_IntEntry( p->vVec2Var, iVecId * p->nFrames + f );
if ( iSatId == 0 )
continue;
assert( iSatId > 0 );
if ( sat_solver_var_value(p->pSat, iSatId) )
Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Vec_IntSize(p->vPis) + i );
} }
}
return pCex;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Prints current abstraction statistics.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p )
{
return NULL;
}
/**Function*************************************************************
Synopsis []
Description [] Description []
...@@ -472,45 +513,72 @@ Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p ) ...@@ -472,45 +513,72 @@ Abc_Cex_t * Aig_GlaDeriveCex( Aig_GlaMan_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r ) void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c )
{ {
printf( "Fra %3d : Ref %3d : PI =%6d PPI =%6d Flop =%6d Node =%6d\n", if ( r == 0 )
f, r, Vec_IntSize(p->vPis), Vec_IntSize(p->vPPis), Vec_IntSize(p->vFlops), Vec_IntSize(p->vNodes) ); printf( "== %3d ==", f );
else
printf( " " );
printf( " %4d PI =%6d PPI =%6d FF =%6d Node =%6d Var =%7d Conf =%6d\n",
r, Vec_IntSize(p->vPis), Vec_IntSize(p->vPPis), Vec_IntSize(p->vFlops), Vec_IntSize(p->vNodes), v, c );
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Perform variable frame abstraction.] Synopsis [Performs gate-level localization abstraction.]
Description [] Description [Returns array of objects included in the abstraction. This array
may contain only const1, flop outputs, and internal nodes, that is, objects
that should have clauses added to the SAT solver.]
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbose ) Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
{ {
int nStart = 0;
Vec_Int_t * vResult = NULL;
Aig_GlaMan_t * p; Aig_GlaMan_t * p;
Aig_Man_t * pAbs; Aig_Man_t * pAbs;
Aig_Obj_t * pObj; Aig_Obj_t * pObj;
Abc_Cex_t * pCex; Abc_Cex_t * pCex;
Vec_Int_t * vPPisToRefine; Vec_Int_t * vPPiRefine;
int f, g, r, i, iSatVar, Lit, Entry, RetValue; int f, g, r, i, iSatVar, Lit, Entry, RetValue;
int nConfBef, nConfAft, clk, clkTotal = clock();
assert( Saig_ManPoNum(pAig) == 1 ); assert( Saig_ManPoNum(pAig) == 1 );
if ( fVerbose )
{
if ( TimeLimit )
printf( "Abstracting from frame %d to frame %d with timeout %d sec.\n", nStart, nFramesMax, TimeLimit );
else
printf( "Abstracting from frame %d to frame %d with no timeout.\n", nStart, nFramesMax );
}
// start the solver // start the solver
p = Aig_GlaManStart( pAig ); p = Aig_GlaManStart( pAig );
p->nFramesMax = nFramesMax; p->nFramesMax = nFramesMax;
p->nConfLimit = nConfLimit; p->nConfLimit = nConfLimit;
p->fVerbose = fVerbose; p->fVerbose = fVerbose;
// include constant node
Vec_IntWriteEntry( p->vIncluded, 0, 1 );
Aig_GlaFetchVar( p, Aig_ManConst1(pAig), 0 );
// set runtime limit
if ( TimeLimit )
sat_solver_set_runtime_limit( p->pSat, clock() + TimeLimit * CLOCKS_PER_SEC );
// iterate over the timeframes // iterate over the timeframes
for ( f = 0; f < nFramesMax; f++ ) for ( f = 0; f < nFramesMax; f++ )
{ {
// initialize abstraction in this timeframe // initialize abstraction in this timeframe
Aig_ManForEachObjVec( p->vAbstr, pAig, pObj, i ) Aig_ManForEachObjVec( p->vAssigned, pAig, pObj, i )
Aig_GlaObjAddToSolver( p, pObj, f ); if ( Vec_IntEntry(p->vIncluded, Aig_ObjId(pObj)) )
if ( !Aig_GlaObjAddToSolver( p, pObj, f ) )
printf( "Error! SAT solver became UNSAT.\n" );
// create output literal to represent property failure // create output literal to represent property failure
pObj = Aig_ManPo( pAig, 0 ); pObj = Aig_ManPo( pAig, 0 );
...@@ -518,41 +586,83 @@ void Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerb ...@@ -518,41 +586,83 @@ void Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerb
Lit = toLitCond( iSatVar, Aig_ObjFaninC0(pObj) ); Lit = toLitCond( iSatVar, Aig_ObjFaninC0(pObj) );
// try solving the abstraction // try solving the abstraction
Aig_GlaPrintAbstr( p, f, -1 ); Aig_GlaCollectAbstr( p );
for ( r = 0; r < 1000000; r++ ) for ( r = 0; r < 1000000; r++ )
{ {
// try to find a counter-example
clk = clock();
nConfBef = p->pSat->stats.conflicts;
RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1,
(ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
nConfAft = p->pSat->stats.conflicts;
p->timeSat += clock() - clk;
if ( RetValue != l_True ) if ( RetValue != l_True )
{
if ( fVerbose )
{
if ( r == 0 )
printf( "== %3d ==", f );
else
printf( " " );
if ( TimeLimit && clock() > clkTotal + TimeLimit * CLOCKS_PER_SEC )
printf( " SAT solver timed out after %d seconds.\n", TimeLimit );
else if ( RetValue != l_False )
printf( " SAT solver returned UNDECIDED after %5d conflicts.\n", nConfAft - nConfBef );
else
printf( " SAT solver returned UNSAT after %5d conflicts.\n", nConfAft - nConfBef );
}
break; break;
// derive abstraction }
Aig_GlaCollectAbstr( p ); clk = clock();
// derive counter-example
pCex = Aig_GlaDeriveCex( p );
// derive abstraction // derive abstraction
pAbs = Aig_GlaDeriveAbs( p ); pAbs = Aig_GlaDeriveAbs( p );
// derive counter-example
pCex = Aig_GlaDeriveCex( p, f );
// verify the counter-example
RetValue = Saig_ManVerifyCex( pAbs, pCex );
if ( RetValue == 0 )
printf( "Error! CEX is invalid.\n" );
// perform refinement // perform refinement
vPPisToRefine = Saig_ManCbaFilterInputs( pAig, Vec_IntSize(p->vPis), pCex, 0 ); vPPiRefine = Saig_ManCbaFilterInputs( pAbs, Vec_IntSize(p->vPis), pCex, 0 );
// update Vec_IntForEachEntry( vPPiRefine, Entry, i )
Vec_IntForEachEntry( vPPisToRefine, Entry, i )
{ {
pObj = Aig_ManObj( pAig, Vec_IntEntry(p->vPPis, Entry) );
assert( Aig_ObjIsNode(pObj) || Saig_ObjIsLo(p->pAig, pObj) );
assert( Vec_IntEntry( p->vIncluded, Aig_ObjId(pObj) ) == 0 );
Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 );
for ( g = 0; g <= f; g++ ) for ( g = 0; g <= f; g++ )
Aig_GlaObjAddToSolver( p, Aig_ManObj(pAig, Vec_IntEntry(p->vPPis, Entry)), g ); if ( !Aig_GlaObjAddToSolver( p, pObj, g ) )
printf( "Error! SAT solver became UNSAT.\n" );
} }
Vec_IntFree( vPPisToRefine ); Vec_IntFree( vPPiRefine );
// print abstraction Aig_ManStop( pAbs );
Aig_GlaPrintAbstr( p, f, r ); Abc_CexFree( pCex );
p->timeRef += clock() - clk;
// prepare abstraction
Aig_GlaCollectAbstr( p );
if ( fVerbose )
Aig_GlaPrintAbstr( p, f, r, p->pSat->size, nConfAft - nConfBef );
} }
if ( RetValue != l_False ) if ( RetValue != l_False )
break; break;
} }
Aig_GlaPrintAbstr( p, f, -1 ); p->timeTotal = clock() - clkTotal;
if ( f == nFramesMax ) if ( f == nFramesMax )
printf( "Finished %d frames without exceeding conflict limit (%d).\n", f, nConfLimit ); printf( "Finished %d frames without exceeding conflict limit (%d).\n", f, nConfLimit );
else else
printf( "Ran out of conflict limit (%d) at frame %d.\n", nConfLimit, f ); printf( "Ran out of conflict limit (%d) at frame %d.\n", nConfLimit, f );
// print stats
if ( fVerbose )
{
ABC_PRTP( "Sat ", p->timeSat, p->timeTotal );
ABC_PRTP( "Ref ", p->timeRef, p->timeTotal );
ABC_PRTP( "Total ", p->timeTotal, p->timeTotal );
}
// prepare return value
vResult = p->vIncluded; p->vIncluded = NULL;
Aig_GlaManStop( p ); Aig_GlaManStop( p );
return vResult;
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/base/abci/abc.c
...@@ -28858,12 +28858,12 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -28858,12 +28858,12 @@ int Abc_CommandAbc9GlaDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
*/ */
if ( pAbc->pGia->vGateClasses == NULL ) if ( pAbc->pGia->vGateClasses == NULL )
{ {
Abc_Print( -1, "Abstraction flop map is missing.\n" ); Abc_Print( -1, "Abstraction gate map is missing.\n" );
return 0; return 0;
} }
// pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses ); pTemp = Gia_ManDupAbsGates( pAbc->pGia, pAbc->pGia->vGateClasses );
// Abc_CommandUpdate9( pAbc, pTemp ); Abc_CommandUpdate9( pAbc, pTemp );
printf( "This command is currently not enabled.\n" ); // printf( "This command is currently not enabled.\n" );
return 0; return 0;
usage: usage:
...@@ -28890,8 +28890,9 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -28890,8 +28890,9 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
Saig_ParBmc_t Pars, * pPars = &Pars; Saig_ParBmc_t Pars, * pPars = &Pars;
int c; int c;
Saig_ParBmcSetDefaultParams( pPars ); Saig_ParBmcSetDefaultParams( pPars );
pPars->nStart = 0;//(pAbc->nFrames >= 0) ? pAbc->nFrames : 0; pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
pPars->nFramesMax = pPars->nStart + 10; pPars->nFramesMax = 50; //pPars->nStart + 10;
pPars->nConfLimit = 5000;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTvh" ) ) != EOF )
{ {
...@@ -28971,11 +28972,11 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -28971,11 +28972,11 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "The network is combinational.\n" ); Abc_Print( -1, "The network is combinational.\n" );
return 0; return 0;
} }
// pAbc->Status = Gia_ManCbaPerform( pAbc->pGia, pPars ); pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars );
// if ( pPars->nStart == 0 ) if ( pPars->nStart == 0 )
// pAbc->nFrames = pPars->iFrame; pAbc->nFrames = pPars->iFrame;
// Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
printf( "This command is currently not enabled.\n" ); // printf( "This command is currently not enabled.\n" );
return 0; return 0;
usage: usage:
......
src/misc/vec/vecInt.h
...@@ -657,6 +657,36 @@ static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry ) ...@@ -657,6 +657,36 @@ static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
static inline void Vec_IntPushOrderReverse( Vec_Int_t * p, int Entry )
{
int i;
if ( p->nSize == p->nCap )
{
if ( p->nCap < 16 )
Vec_IntGrow( p, 16 );
else
Vec_IntGrow( p, 2 * p->nCap );
}
p->nSize++;
for ( i = p->nSize-2; i >= 0; i-- )
if ( p->pArray[i] < Entry )
p->pArray[i+1] = p->pArray[i];
else
break;
p->pArray[i+1] = Entry;
}
/**Function*************************************************************
Synopsis [Inserts the entry while preserving the increasing order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Vec_IntPushUniqueOrder( Vec_Int_t * p, int Entry ) static inline int Vec_IntPushUniqueOrder( Vec_Int_t * p, int Entry )
{ {
int i; int i;
......
src/sat/bsat/satSolver.c
...@@ -1485,6 +1485,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit ...@@ -1485,6 +1485,8 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
// int nConfs = 0; // int nConfs = 0;
double Ratio = (s->stats.learnts == 0)? 0.0 : double Ratio = (s->stats.learnts == 0)? 0.0 :
s->stats.learnts_literals / (double)s->stats.learnts; s->stats.learnts_literals / (double)s->stats.learnts;
if ( s->nRuntimeLimit && clock() > s->nRuntimeLimit )
break;
if (s->verbosity >= 1) if (s->verbosity >= 1)
{ {
......
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