mirror of https://github.com/YosysHQ/abc.git
New abstraction code.
This commit is contained in:
Alan Mishchenko
parent
efd310af3e
commit
397bebf8a5
|
|
@ -603,7 +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 );
|
||||
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_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars );
|
||||
extern int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf );
|
||||
/*=== giaAiger.c ===========================================================*/
|
||||
extern int Gia_FileSize( char * pFileName );
|
||||
extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
|
||||
|
|
|
|||
|
|
@ -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 Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fUseCnf )
|
||||
{
|
||||
extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
|
||||
extern Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fUseCnf, 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 )
|
|||
*/
|
||||
// perform abstraction
|
||||
pAig = Gia_ManToAigSimple( pGia );
|
||||
vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
|
||||
vGateClasses = Aig_GlaManTest( pAig, p->nFramesMax, p->nConfLimit, p->nTimeOut, fUseCnf, p->fVerbose );
|
||||
Aig_ManStop( pAig );
|
||||
|
||||
// update the map
|
||||
|
|
|
|||
|
|
@ -1582,6 +1582,27 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses )
|
|||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Duplicates the AIG manager recursively.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_ManDupAbsGates_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj )
|
||||
{
|
||||
if ( ~pObj->Value )
|
||||
return;
|
||||
assert( Gia_ObjIsAnd(pObj) );
|
||||
Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin0(pObj) );
|
||||
Gia_ManDupAbsGates_rec( pNew, Gia_ObjFanin1(pObj) );
|
||||
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs abstraction of the AIG to preserve the included gates.]
|
||||
|
|
@ -1642,6 +1663,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses )
|
|||
// create internal nodes
|
||||
Gia_ManForEachObjVec( vNodes, p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
|
||||
// Gia_ManDupAbsGates_rec( pNew, pObj );
|
||||
// create PO
|
||||
Gia_ManForEachPo( p, pObj, i )
|
||||
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@
|
|||
|
||||
#include "saig.h"
|
||||
#include "satSolver.h"
|
||||
#include "cnf.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -49,6 +50,12 @@ struct Aig_GlaMan_t_
|
|||
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 * vVar2Inf; // maps sat Var into its frame and obj ID
|
||||
// CNF computation
|
||||
Vec_Ptr_t * vLeaves;
|
||||
Vec_Ptr_t * vVolume;
|
||||
Vec_Int_t * vCover;
|
||||
Vec_Ptr_t * vObj2Cnf;
|
||||
Vec_Int_t * vLits;
|
||||
// SAT solver
|
||||
sat_solver * pSat;
|
||||
// statistics
|
||||
|
|
@ -153,7 +160,7 @@ static inline int Aig_GlaAddNode( sat_solver * pSat, int iVar, int iVar0, int iV
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Aig_GlaCollectAssigned( Aig_Man_t * p, Vec_Int_t * vGateClasses )
|
||||
Vec_Int_t * Aig_GlaCollectAssigned_( Aig_Man_t * p, Vec_Int_t * vGateClasses )
|
||||
{
|
||||
Vec_Int_t * vAssigned;
|
||||
Aig_Obj_t * pObj;
|
||||
|
|
@ -240,6 +247,27 @@ void Aig_GlaCollectAbstr( Aig_GlaMan_t * p )
|
|||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Duplicates the AIG manager recursively.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Aig_GlaDeriveAbs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )
|
||||
{
|
||||
if ( pObj->pData )
|
||||
return;
|
||||
assert( Aig_ObjIsNode(pObj) );
|
||||
Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin0(pObj) );
|
||||
Aig_GlaDeriveAbs_rec( pNew, Aig_ObjFanin1(pObj) );
|
||||
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives abstraction.]
|
||||
|
|
@ -274,7 +302,8 @@ Aig_Man_t * Aig_GlaDeriveAbs( Aig_GlaMan_t * p )
|
|||
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) );
|
||||
// pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
Aig_GlaDeriveAbs_rec( pNew, pObj );
|
||||
// create PO
|
||||
Saig_ManForEachPo( p->pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
|
||||
|
|
@ -371,11 +400,47 @@ int Aig_GlaObjAddToSolver( Aig_GlaMan_t * p, Aig_Obj_t * pObj, int k )
|
|||
Aig_GlaFetchVar(p, Aig_ObjFanin0(pObjLi), k-1),
|
||||
Aig_ObjFaninC0(pObjLi) );
|
||||
}
|
||||
assert( Aig_ObjIsNode(pObj) );
|
||||
return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k),
|
||||
Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k),
|
||||
Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k),
|
||||
Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
|
||||
else
|
||||
{
|
||||
Vec_Int_t * vClauses;
|
||||
int i, Entry;
|
||||
assert( Aig_ObjIsNode(pObj) );
|
||||
if ( p->vObj2Cnf == NULL )
|
||||
return Aig_GlaAddNode( p->pSat, Aig_GlaFetchVar(p, pObj, k),
|
||||
Aig_GlaFetchVar(p, Aig_ObjFanin0(pObj), k),
|
||||
Aig_GlaFetchVar(p, Aig_ObjFanin1(pObj), k),
|
||||
Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
|
||||
// derive clauses
|
||||
assert( pObj->fMarkA );
|
||||
vClauses = Vec_PtrEntry( p->vObj2Cnf, Aig_ObjId(pObj) );
|
||||
if ( vClauses == NULL )
|
||||
{
|
||||
Vec_PtrWriteEntry( p->vObj2Cnf, Aig_ObjId(pObj), (vClauses = Vec_IntAlloc(16)) );
|
||||
Cnf_ComputeClauses( p->pAig, pObj, p->vLeaves, p->vVolume, NULL, p->vCover, vClauses );
|
||||
}
|
||||
// derive variables
|
||||
Cnf_CollectLeaves( pObj, p->vLeaves, 0 );
|
||||
Vec_PtrForEachEntry( Aig_Obj_t *, p->vLeaves, pObj, i )
|
||||
Aig_GlaFetchVar( p, pObj, k );
|
||||
// translate clauses
|
||||
assert( Vec_IntSize(vClauses) >= 2 );
|
||||
assert( Vec_IntEntry(vClauses, 0) == 0 );
|
||||
Vec_IntForEachEntry( vClauses, Entry, i )
|
||||
{
|
||||
if ( Entry == 0 )
|
||||
{
|
||||
Vec_IntClear( p->vLits );
|
||||
continue;
|
||||
}
|
||||
Vec_IntPush( p->vLits, (Entry & 1) ^ (2 * Aig_GlaFetchVar(p, Aig_ManObj(p->pAig, Entry >> 1), k)) );
|
||||
if ( i == Vec_IntSize(vClauses) - 1 || Vec_IntEntry(vClauses, i+1) == 0 )
|
||||
{
|
||||
if ( !sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits)+Vec_IntSize(p->vLits) ) )
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
@ -389,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 )
|
||||
Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig, int fUseCnf )
|
||||
{
|
||||
Aig_GlaMan_t * p;
|
||||
int i;
|
||||
|
|
@ -416,6 +481,17 @@ Aig_GlaMan_t * Aig_GlaManStart( Aig_Man_t * pAig )
|
|||
Vec_IntPush( p->vVar2Inf, -1 );
|
||||
Vec_IntPush( p->vVar2Inf, -1 );
|
||||
|
||||
// CNF computation
|
||||
if ( fUseCnf )
|
||||
{
|
||||
p->vLeaves = Vec_PtrAlloc( 100 );
|
||||
p->vVolume = Vec_PtrAlloc( 100 );
|
||||
p->vCover = Vec_IntAlloc( 1 << 16 );
|
||||
p->vObj2Cnf = Vec_PtrStart( Aig_ManObjNumMax(pAig) );
|
||||
p->vLits = Vec_IntAlloc( 100 );
|
||||
Cnf_DeriveFastMark( pAig );
|
||||
}
|
||||
|
||||
// start the SAT solver
|
||||
p->pSat = sat_solver_new();
|
||||
sat_solver_setnvars( p->pSat, 256 );
|
||||
|
|
@ -448,6 +524,16 @@ void Aig_GlaManStop( Aig_GlaMan_t * p )
|
|||
Vec_IntFreeP( &p->vVec2Var );
|
||||
Vec_IntFreeP( &p->vVar2Inf );
|
||||
|
||||
if ( p->vObj2Cnf )
|
||||
{
|
||||
Vec_PtrFreeP( &p->vLeaves );
|
||||
Vec_PtrFreeP( &p->vVolume );
|
||||
Vec_IntFreeP( &p->vCover );
|
||||
Vec_VecFreeP( (Vec_Vec_t **)&p->vObj2Cnf );
|
||||
Vec_IntFreeP( &p->vLits );
|
||||
Aig_ManCleanMarkA( p->pAig );
|
||||
}
|
||||
|
||||
if ( p->pSat )
|
||||
sat_solver_delete( p->pSat );
|
||||
ABC_FREE( p );
|
||||
|
|
@ -523,6 +609,34 @@ void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c )
|
|||
r, Vec_IntSize(p->vPis), Vec_IntSize(p->vPPis), Vec_IntSize(p->vFlops), Vec_IntSize(p->vNodes), v, c );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints current abstraction statistics.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Aig_GlaExtendIncluded( Aig_GlaMan_t * p )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i, k;
|
||||
Aig_ManForEachNode( p->pAig, pObj, i )
|
||||
{
|
||||
if ( !Vec_IntEntry( p->vIncluded, i ) )
|
||||
continue;
|
||||
Cnf_ComputeClauses( p->pAig, pObj, p->vLeaves, p->vVolume, NULL, p->vCover, p->vNodes );
|
||||
Vec_PtrForEachEntry( Aig_Obj_t *, p->vVolume, pObj, k )
|
||||
{
|
||||
assert( Aig_ObjId(pObj) <= i );
|
||||
Vec_IntWriteEntry( p->vIncluded, Aig_ObjId(pObj), 1 );
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs gate-level localization abstraction.]
|
||||
|
|
@ -536,7 +650,7 @@ void Aig_GlaPrintAbstr( Aig_GlaMan_t * p, int f, int r, int v, int c )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
|
||||
Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int TimeLimit, int fUseCnf, int fVerbose )
|
||||
{
|
||||
int nStart = 0;
|
||||
Vec_Int_t * vResult = NULL;
|
||||
|
|
@ -558,7 +672,7 @@ Vec_Int_t * Aig_GlaManTest( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, in
|
|||
}
|
||||
|
||||
// start the solver
|
||||
p = Aig_GlaManStart( pAig );
|
||||
p = Aig_GlaManStart( pAig, fUseCnf );
|
||||
p->nFramesMax = nFramesMax;
|
||||
p->nConfLimit = nConfLimit;
|
||||
p->fVerbose = fVerbose;
|
||||
|
|
@ -660,6 +774,7 @@ 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 );
|
||||
vResult = p->vIncluded; p->vIncluded = NULL;
|
||||
Aig_GlaManStop( p );
|
||||
return vResult;
|
||||
|
|
|
|||
|
|
@ -28888,13 +28888,13 @@ usage:
|
|||
int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
Saig_ParBmc_t Pars, * pPars = &Pars;
|
||||
int c;
|
||||
int c, fUseCnf = 1;
|
||||
Saig_ParBmcSetDefaultParams( pPars );
|
||||
pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
|
||||
pPars->nFramesMax = 50; //pPars->nStart + 10;
|
||||
pPars->nConfLimit = 5000;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTvh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTcvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -28953,6 +28953,9 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( pPars->nTimeOut < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'c':
|
||||
fUseCnf ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
pPars->fVerbose ^= 1;
|
||||
break;
|
||||
|
|
@ -28972,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 );
|
||||
pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fUseCnf );
|
||||
if ( pPars->nStart == 0 )
|
||||
pAbc->nFrames = pPars->iFrame;
|
||||
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
|
||||
|
|
@ -28980,13 +28983,14 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &gla_cba [-SFCMT num] [-vh]\n" );
|
||||
Abc_Print( -2, "usage: &gla_cba [-SFCMT num] [-cvh]\n" );
|
||||
Abc_Print( -2, "\t refines abstracted object map with CEX-based abstraction\n" );
|
||||
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
|
||||
Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
|
||||
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-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
return 1;
|
||||
|
|
|
|||
Loading…
Reference in New Issue