diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-18 23:53:02 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-18 23:53:02 -0700 |
commit | 72c09b86a0b6280c1472cc6cf09a31a9a336ef87 (patch) | |
tree | e6dbb3b8d8241989e476f382649cb0960a10542c /src/aig/gia | |
parent | 1fe2ba9ac0787906573f7b1cadf5ff535ee7444f (diff) | |
download | abc-72c09b86a0b6280c1472cc6cf09a31a9a336ef87.tar.gz abc-72c09b86a0b6280c1472cc6cf09a31a9a336ef87.tar.bz2 abc-72c09b86a0b6280c1472cc6cf09a31a9a336ef87.zip |
Scalable gate-level abstraction.
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaAbsGla2.c | 1021 |
1 files changed, 1021 insertions, 0 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c new file mode 100644 index 00000000..8149d4be --- /dev/null +++ b/src/aig/gia/giaAbsGla2.c @@ -0,0 +1,1021 @@ +/**CFile**************************************************************** + + FileName [gia.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Scalable gate-level abstraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: gia.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Ga2_Man_t_ Ga2_Man_t; // manager +struct Ga2_Man_t_ +{ + // user data + Gia_Man_t * pGia; // working AIG manager + Gia_ParVta_t * pPars; // parameters + // internal data + int nObjs; // the number of objects (abstracted and PPIs) + int nObjsAlloc; // the number of allocated objects + Vec_Int_t * vAbs; // array of abstracted objects + int nAbs; // starting abstraction +// Vec_Int_t * vExtra; // additional objects + // object structure + Vec_Int_t * pvLeaves; // leaves for each object + Vec_Int_t * pvCnf0; // positive CNF + Vec_Int_t * pvCnf1; // negative CNF + Vec_Int_t * pvMap; // mapping into SAT vars for each frame + // temporaries + Vec_Int_t * vCnf; + Vec_Int_t * vLits; + Vec_Int_t * vIsopMem; + // other data + sat_solver2 * pSat; // incremental SAT solver + int nSatVars; // the number of SAT variables + // statistics + clock_t timeStart; + clock_t timeInit; + clock_t timeSat; + clock_t timeUnsat; + clock_t timeCex; + clock_t timeOther; +}; + +// returns literal of this object, or -1 if the literal is not assigned +static inline int Ga2_ObjFindLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) +{ + Vec_Int_t * vMap; + assert( pObj->fPhase ); + if ( pObj->Value == 0 ) + return -1; + vMap = &p->pvMap[pObj->Value]; + if ( f < Vec_IntSize(vMap) ) + return -1; + return Vec_IntEntry( vMap, f ); +} +// inserts the literal for this object +static inline void Ga2_ObjAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f, int Lit ) +{ + Vec_Int_t * vMap; + assert( Lit > 1 ); + assert( pObj->fPhase ); + assert( Ga2_ObjFindLit(p, pObj, f) == -1 ); + if ( pObj->Value == 0 ) + pObj->Value = p->nObjs++; + vMap = &p->pvMap[pObj->Value]; + Vec_IntSetEntry( vMap, f, Lit ); +} +// returns +static inline int Ga2_ObjFindOrAddLit( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) +{ + int Lit = Ga2_ObjFindLit( p, pObj, f ); + if ( Lit == -1 ) + { + Lit = toLitCond( p->nSatVars++, 0 ); + Ga2_ObjAddLit( p, pObj, f, Lit ); + } + assert( Lit > 1 ); + return Lit; +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns AIG marked for CNF generation.] + + Description [The marking satisfies the following requirements: + Each marked node has the number of marked fanins no more than N.] + + SideEffects [Uses pObj->fPhase to store the markings.] + + SeeAlso [] + +***********************************************************************/ +int Ga2_ManBreakTree_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst, int N ) +{ // breaks a tree rooted at the node into N-feasible subtrees + int Val0, Val1; + if ( pObj->fPhase && !fFirst ) + return 1; + Val0 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin0(pObj), 0, N ); + Val1 = Ga2_ManBreakTree_rec( p, Gia_ObjFanin1(pObj), 0, N ); + if ( Val0 + Val1 < N ) + return Val0 + Val1; + if ( Val0 + Val1 == N ) + { + pObj->fPhase = 1; + return 1; + } + assert( Val0 + Val1 > N ); + assert( Val0 < N && Val1 < N ); + if ( Val0 >= Val1 ) + { + Gia_ObjFanin0(pObj)->fPhase = 1; + Val0 = 1; + } + else + { + Gia_ObjFanin1(pObj)->fPhase = 1; + Val1 = 1; + } + if ( Val0 + Val1 < N ) + return Val0 + Val1; + if ( Val0 + Val1 == N ) + { + pObj->fPhase = 1; + return 1; + } + assert( 0 ); + return -1; +} +int Ga2_ManCheckNodesAnd( Gia_Man_t * p, Vec_Int_t * vNodes ) +{ + Gia_Obj_t * pObj; + int i; + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + if ( (!Gia_ObjFanin0(pObj)->fPhase && Gia_ObjFaninC0(pObj)) || + (!Gia_ObjFanin1(pObj)->fPhase && Gia_ObjFaninC1(pObj)) ) + return 0; + return 1; +} +void Ga2_ManCollectNodes_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, int fFirst ) +{ + if ( pObj->fPhase && !fFirst ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Ga2_ManCollectNodes_rec( p, Gia_ObjFanin0(pObj), vNodes, 0 ); + Ga2_ManCollectNodes_rec( p, Gia_ObjFanin1(pObj), vNodes, 0 ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); + +} +void Ga2_ManCollectLeaves_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves, int fFirst ) +{ + if ( pObj->fPhase && !fFirst ) + { + Vec_IntPushUnique( vLeaves, Gia_ObjId(p, pObj) ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin0(pObj), vLeaves, 0 ); + Ga2_ManCollectLeaves_rec( p, Gia_ObjFanin1(pObj), vLeaves, 0 ); +} +int Ga2_ManMarkup( Gia_Man_t * p, int N ) +{ + clock_t clk = clock(); + Vec_Int_t * vLeaves; + Gia_Obj_t * pObj; + int i, CountMarks; + // label nodes with multiple fanouts and inputs MUXes + Gia_ManForEachObj( p, pObj, i ) + { + pObj->Value = 0; + if ( !Gia_ObjIsAnd(pObj) ) + continue; + Gia_ObjFanin0(pObj)->Value++; + Gia_ObjFanin1(pObj)->Value++; + if ( !Gia_ObjIsMuxType(pObj) ) + continue; + Gia_ObjFanin0(Gia_ObjFanin0(pObj))->Value++; + Gia_ObjFanin1(Gia_ObjFanin0(pObj))->Value++; + Gia_ObjFanin0(Gia_ObjFanin1(pObj))->Value++; + Gia_ObjFanin1(Gia_ObjFanin1(pObj))->Value++; + } + Gia_ManForEachObj( p, pObj, i ) + { + pObj->fPhase = 0; + if ( Gia_ObjIsAnd(pObj) ) + pObj->fPhase = (pObj->Value > 1); + else if ( Gia_ObjIsCo(pObj) ) + Gia_ObjFanin0(pObj)->fPhase = 1; + else + pObj->fPhase = 1; + pObj->Value = 0; + } + // add marks when needed + vLeaves = Vec_IntAlloc( 100 ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !pObj->fPhase ) + continue; + Vec_IntClear( vLeaves ); + Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 ); + if ( Vec_IntSize(vLeaves) > N ) + Ga2_ManBreakTree_rec( p, pObj, 1, N ); + } + // verify that the tree is split correctly + CountMarks = 0; + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !pObj->fPhase ) + continue; + Vec_IntClear( vLeaves ); + Ga2_ManCollectLeaves_rec( p, pObj, vLeaves, 1 ); + assert( Vec_IntSize(vLeaves) <= N ); +// printf( "%d ", Vec_IntSize(vLeaves) ); + CountMarks++; + } +// printf( "Internal nodes = %d. ", CountMarks ); + Abc_PrintTime( 1, "Time", clock() - clk ); + Vec_IntFree( vLeaves ); + return CountMarks; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gla_Man_t * Ga2_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) +{ + Gla_Man_t * p; + int Lit; + p = ABC_CALLOC( Gla_Man_t, 1 ); + p->pGia = pGia; + p->pPars = pPars; + // internal data + p->vAbs = Vec_IntAlloc( 100 ); +// p->vExtra = Vec_IntAlloc( 100 ); + // object structure + p->nObjsAlloc = 256; + p->pvLeaves = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc ); + p->pvCnf0 = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc ); + p->pvCnf1 = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc ); + p->pvMap = ABC_CALLOC( Vec_Int_t, p->nObjsAlloc ); + // temporaries + p->vCnf = Vec_IntAlloc( 100 ); + p->vLits = Vec_IntAlloc( 100 ); + p->vIsopMem = Vec_IntAlloc( 100 ); + // prepare AIG + p->timeStart = clock(); + Ga2_ManMarkup( pGia, 5 ); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ga2_ManStop( Gla_Man_t * p ) +{ + int i; +// if ( p->pPars->fVerbose ) + Abc_Print( 1, "SAT solver: Var = %d Cla = %d Conf = %d Reduce = %d Cex = %d ObjsAdded = %d\n", + sat_solver2_nvars(p->pSat), sat_solver2_nclauses(p->pSat), sat_solver2_nconflicts(p->pSat), p->pSat->nDBreduces, p->nCexes, p->nObjAdded ); + for ( i = 0; i < p->nObjsAlloc; i++ ) + { + ABC_FREE( p->pvLeaves->pArray ); + ABC_FREE( p->pvCnf0->pArray ); + ABC_FREE( p->pvCnf1->pArray ); + ABC_FREE( p->pvMap->pArray ); + } + ABC_FREE( p->pvLeaves ); + ABC_FREE( p->pvCnf0 ); + ABC_FREE( p->pvCnf1 ); + ABC_FREE( p->pvMap ); + Vec_IntFree( p->vCnf ); + Vec_IntFree( p->vLits ); + Vec_IntFree( p->vIsopMem ); + Vec_IntFree( p->vAbs ); +// Vec_IntFree( p->vExtra ); + sat_solver2_delete( p->pSat ); + ABC_FREE( p ); +} + + +/**Function************************************************************* + + Synopsis [Computes truth table for the marked node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ga2_ObjComputeTruth_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int fFirst ) +{ + unsigned Val0, Val1; + if ( pObj->fPhase && !fFirst ) + return pObj->Value; + assert( Gia_ObjIsAnd(pObj) ); + Val0 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin0(pObj), 0 ); + Val1 = Ga2_ObjComputeTruth_rec( p, Gia_ObjFanin1(pObj), 0 ); + return (Gia_ObjFaninC0(pObj) ? ~Val0 : Val0) & (Gia_ObjFaninC1(pObj) ? ~Val1 : Val1); +} +unsigned Ga2_ManComputeTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves ) +{ + static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + unsigned Res, Values[5]; + Gia_Obj_t * pObj; + int i; + // compute leaves + Vec_IntClear( vLeaves ); + Ga2_ManCollectLeaves_rec( p, pRoot, vLeaves, 1 ); + // assign elementary truth tables + Gia_ManForEachObjVec( vLeaves, p, pObj, i ) + { + assert( pObj->fPhase ); + Values[i] = pObj->Value; + pObj->Value = uTruth5[i]; + } + Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 ); + // return values + Gia_ManForEachObjVec( vLeaves, p, pObj, i ) + pObj->Value = Values[i]; + return Res; +} +void Ga2_ManComputeTest( Gia_Man_t * p ) +{ + clock_t clk; + Vec_Int_t * vLeaves; + Gia_Obj_t * pObj; + int i; + Ga2_ManMarkup( p, 5 ); + clk = clock(); + vLeaves = Vec_IntAlloc( 100 ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !pObj->fPhase ) + continue; + Ga2_ManComputeTruth( p, pObj, vLeaves ); + } + Vec_IntFree( vLeaves ); + Abc_PrintTime( 1, "Time", clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [Computes and minimizes the truth table.] + + Description [Array of input literals may contain 0 (const0), 1 (const1) + or 2 (literal). Upon exit, it contains the variables in the support.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Ga2_ObjTruthDepends( unsigned t, int v ) +{ + assert( v >= 0 && v <= 4 ); + if ( v == 0 ) + return ((t ^ (t >> 1)) & 0x55555555); + if ( v == 1 ) + return ((t ^ (t >> 2)) & 0x33333333); + if ( v == 2 ) + return ((t ^ (t >> 4)) & 0x0F0F0F0F); + if ( v == 3 ) + return ((t ^ (t >> 8)) & 0x00FF00FF); + if ( v == 4 ) + return ((t ^ (t >>16)) & 0x0000FFFF); + return -1; +} +unsigned Ga2_ObjComputeTruthSpecial( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vLits ) +{ + static unsigned uTruth5[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + unsigned Res, Values[5]; + Gia_Obj_t * pObj; + int i, k, Entry; + // assign elementary truth tables + Gia_ManForEachObjVec( vLeaves, p, pObj, i ) + { + assert( pObj->fPhase ); + Values[i] = pObj->Value; + Entry = Vec_IntEntry( vLits, i ); + assert( Entry >= 0 && Entry <= 2 ); + if ( Entry == 0 ) + pObj->Value = 0; + else if ( Entry == 1 ) + pObj->Value = ~0; + else // if ( Entry == 2 ) + pObj->Value = uTruth5[i]; + } + Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 ); + Vec_IntClear( vLits ); + if ( Res != 0 && Res != ~0 ) + { + // check if truth table depends on them + k = 0; + Gia_ManForEachObjVec( vLeaves, p, pObj, i ) + { + if ( Ga2_ObjTruthDepends( Res, i ) ) + { + pObj->Value = uTruth5[k++]; + Vec_IntPush( vLits, i ); + } + } + // recompute the truth table + Res = Ga2_ObjComputeTruth_rec( p, pRoot, 1 ); + // verify that the true table depends on them + for ( i = 0; i < Vec_IntSize(vLeaves); i++ ) + assert( (i < Vec_IntSize(vLits)) == (Ga2_ObjTruthDepends(Res, i) > 0) ); + } + // return values + Gia_ManForEachObjVec( vLeaves, p, pObj, i ) + pObj->Value = Values[i]; + return Res; +} + +/**Function************************************************************* + + Synopsis [Returns CNF of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCnf, Vec_Int_t * vCover ) +{ + extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth ); + int i, k, Cube, Literal, NewCube, RetValue; + assert( n == 5 ); + // transform truth table into the SOP + RetValue = Kit_TruthIsop( &uTruth, 5, vCover, 0 ); + assert( RetValue == 0 ); + // check the case of constant cover + Vec_IntClear( vCnf ); + Vec_IntForEachEntry( vCover, Cube, i ) + { + for ( k = 0; k < nVars; k++ ) + { + Literal = 3 & (Cube >> (k << 1)); + if ( Literal == 1 ) +// pCube[k] = '0'; + NewCube = NewCube * 3 + 0; + else if ( Literal == 2 ) +// pCube[k] = '1'; + NewCube = NewCube * 3 + 1; + else if ( Literal == 0 ) + NewCube = NewCube * 3 + 2; + else + assert( 0 ); + } + Vec_IntPush( vCnf, NewCube ); + } +} + + +/**Function************************************************************* + + Synopsis [Derives CNF for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ga2_ManCnfAddClause( Vec_Int_t * vCnf, int Lits[], int iLitOut, int ProofId ) +{ + int k, b, Clause, nClaLits, ClaLits[6]; +// for ( k = 0; k < p->pSopSizes[uTruth]; k++ ) + Vec_IntForEacEntry( vCnf, Clause, k ) + { + nClaLits = 0; + ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut; +// Clause = p->pSops[uTruth][k]; + for ( b = 3; b >= 0; b-- ) + { + if ( Clause % 3 == 0 ) // value 0 --> write positive literal + { + assert( Lits[b] > 1 ); + ClaLits[nClaLits++] = Lits[b]; + } + else if ( Clause % 3 == 1 ) // value 1 --> write negative literal + { + assert( Lits[b] > 1 ); + ClaLits[nClaLits++] = lit_neg(Lits[b]); + } + Clause = Clause / 3; + } + sat_solver2_addclause( p->pSat, ClaLits, ClaLits+nClaLits, ProofId ) ); + } +} +void Ga2_ManCnfAddPrecomputed( Ga2_Man_t * p, int uTruth, int Lits[], int iLitOut ) +{ + int i, k; + assert( uTruth > 0 && uTruth < 0xffff ); + // write positive/negative polarity + for ( i = 0; i < 2; i++ ) + { + if ( i ) + uTruth = 0xffff & ~uTruth; +// Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" ); + Vec_IntClear( p->vCnf ); + for ( k = 0; k < p->pSopSizes[uTruth]; k++ ) + Vec_IntPush( p->vCnf, p->pSops[uTruth][k] ); + Ga2_ManCnfAddClause( p->vCnf, Lits, (i ? lit_neg(iLitOut) : iLitOut), ProofId ); + } +} +void Ga2_ManCnfAddDerived( Ga2_Man_t * p, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int Lits[], int iLitOut ) +{ + Ga2_ManCnfAddClause( vCnf0, Lits, iLitOut, ProofId ); + Ga2_ManCnfAddClause( vCnf1, Lits, lit_neg(iLitOut), ProofId ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ga2_ManSetupNode( Ga2_Man_t * p, Gia_Obj_t * pObj ) +{ + int Id = p->nObjs++; + Vec_Int_t * vLeaves = &p->pvLeaves[Id]; + Vec_Int_t * vCnf0 = &p->pvCnfs0[Id]; + Vec_Int_t * vCnf1 = &p->pvCnfs1[Id]; + Vec_Int_t * vMap = &p->pvMaps[Id]; + unsigned uTruth; + assert( pObj->Value == 0 ); + assert( p->nObjs > 1 ); + // prepare leaves + if ( Vec_IntSize(vLeaves) == 0 ) + { + Vec_IntGrow( vLeaves, 5 ); + Ga2_ManCollectLeaves_rec( p->pGia, pObj, vLeaves, 1 ); + assert( Vec_IntSize(vLeaves) < 6 ); + // compute truth table + uTruth = Ga2_ManComputeTruth( p->pGia, pObj, vLeaves ); + // prepare CNF + Ga2_ManCnfCompute( uTruth, Vec_IntSize(vLeaves), vCnf0, p->vCover ); + uTruth = (~uTruth) & ~((~0) << (1 << Vec_IntSize(vLeaves))); + Ga2_ManCnfCompute( uTruth, Vec_IntSize(vLeaves), vCnf1, p->vCover ); + // prepare mapping + Vec_IntGrow( vLeaves, 100 ); + } + else + Vec_IntClear( vMap ); + // remember the number + pObj->Value = Id; + // realloc + if ( p->nObjs == p->nObjsAlloc ) + { + p->pvLeaves = ABC_REALLOC( Vec_Int_t, p->pvLeaves, 2 * p->nObjsAlloc ); + p->pvCnfs0 = ABC_REALLOC( Vec_Int_t, p->pvCnfs0, 2 * p->nObjsAlloc ); + p->pvCnfs1 = ABC_REALLOC( Vec_Int_t, p->pvCnfs1, 2 * p->nObjsAlloc ); + p->pvMaps = ABC_REALLOC( Vec_Int_t, p->pvMaps, 2 * p->nObjsAlloc ); + memset( p->pvLeaves + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc ); + memset( p->pvCnfs0 + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc ); + memset( p->pvCnfs1 + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc ); + memset( p->pvMaps + p->nObjsAlloc, 0, sizeof(Vec_Int_t) * p->nObjsAlloc ); + p->nObjsAlloc *= 2; + } +} +void Ga2_ManSetdownNode( Ga2_Man_t * p, Gia_Obj_t * pObj ) +{ + assert( pObj->Value > 0 ); + pObj->Value = 0; +} +void Ga2_ManAddNode( Ga2_Man_t * p, Gia_Obj_t * pObj, int f ) +{ + assert( pObj->Value > 0 ); + +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ga2_ManRestart( Ga2_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i; + assert( p->pGia != NULL ); + assert( p->pGia->vGateClasses != NULL ); + assert( Gia_ManPi(p->pGia, 0)->fPhase ); // marks are set + // clear mappings from objects + for ( i = 1; i < p->nObjs; i++ ) + { + Vec_IntShrink( &p->pvLeaves[i], 0 ); + Vec_IntShrink( &p->pvCnfs0[i], 0 ); + Vec_IntShrink( &p->pvCnfs1[i], 0 ); + Vec_IntShrink( &p->pvMaps[i], 0 ); + } + // clear SAT variable numbers (begin with 1) + if ( p->pSat ) sat_solver2_delete( p->pSat ); + p->pSat = sat_solver2_new(); + p->nSatVars = 1; + // create constant literal + Lit = toLitCond( 1, 1 ); + sat_solver2_addclause( p->pSat, &Lit, &Lit + 1, 0 ); + // collect abstraction + p->nObjs = 1; + Gia_ManCleanValue( p->pGia ); + Vec_IntClear( p->vAbs ); + Gia_ManForEachObj( p, pObj, i ) + { + if ( pObj->fPhase && Vec_IntEntry(p->pGia->vGateClasses, i) ) + { + Vec_IntPush( p->vAbs, i ); + Ga2_ManSetupNode( p, pObj ); + } + } + p->nAbs = Vec_IntSize( p->vAbs ); + // set runtime limit + if ( p->pPars->nTimeOut ) + sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + p->timeStart ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ga2_ManTranslate_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vClasses, int fFirst ) +{ + if ( pObj->fPhase && !fFirst ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Ga2_ManTranslate_rec( p, Gia_ObjFanin0(pObj), vClasses, 0 ); + Ga2_ManTranslate_rec( p, Gia_ObjFanin1(pObj), vClasses, 0 ); + Vec_IntWriteEntry( vClasses, Gia_ObjId(p, pObj), 1 ); +} +Vec_Int_t * Ga2_ManTranslate( Ga2_Man_t * p ) +{ + Vec_Int_t * vGateClasses; + Gia_Obj_t * pObj; + int i; + vGateClasses = Vec_IntStart( Gia_ManObjNum(p->pGia) ); + Gia_ManForEachObjVec( p->vAbs, p, pObj, i ) + Ga2_ManTranslate_rec( p, pObj, vGateClasses, 1 ); + return vGateClasses; +} + +/**Function************************************************************* + + Synopsis [Unrolls one timeframe.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ga2_ManUnroll( Ga2_Man_t * p, int f ) +{ + Gia_Obj_t * pObj, * pObjRi, * pLeaf; + unsigned uTruth; + int i, k, Lit, fFullTable; + // construct CNF for internal nodes + Gia_ManForEachObjVec( p->vAbs, p, pObj, i ) + { + // assign RO literal values (no need to add clauses) + assert( pObj->fPhase && pObj->Value ); + if ( Gia_ObjIsConst0(pObj) ) + { + Ga2_ObjAddLit( p, pObj, f, 3 ); // const 0 + continue; + } + if ( Gia_ObjIsRo(p->pGia, pObj) ) + { + pObjRi = Gia_ObjRoToRi(p->pGia, pObj); + Lit = f ? Ga2_ObjFindOrAddLit( p, pObjRi, f-1 ) : 3; // const 0 + Ga2_ObjAddLit( p, pObj, f, Lit ); + continue; + } + assert( Gia_ObjIsAnd(pObj) ); + vLeaves = Ga2_ManReadLeaves( p, pObj ); + // for nodes recently added to abstration, add CNF without const propagation + fFullTable = 1; + if ( i < p->nAbs ) + { + Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k ) + { + Lit = Ga2_ObjReadLit( p, pLeaf, f ); + if ( Lit == 2 || Lit == 3 ) + { + fFullTable = 0; + break; + } + } + } + if ( fFullTable ) + { + Vec_IntClear( p->vLits ); + Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k ) + Vec_IntWriteEntry( p->vLits, Ga2_ObjFindOrAddLit(p, pLeaf, f) ); + iLitOut = Ga2_ObjFindOrAddLit(p, pObj, f); + Ga2_ManCnfAddClause( vCnf0, Vec_IntArray(p->vLits), iLitOut, i < p->nAbs ? 0 : Gia_ObjId(p->pGia, pObj) ); + Ga2_ManCnfAddClause( vCnf1, Vec_IntArray(p->vLits), lit_neg(iLitOut), i < p->nAbs ? 0 : Gia_ObjId(p->pGia, pObj) ); + continue; + } + assert( i < p->nAbs ); + // collect literal types + Vec_IntClear( p->vLits ); + Gia_ManForEachObjVec( vLeaves, p->pGia, pLeaf, k ) + { + Lit = Ga2_ObjReadLit( p, pLeaf, f ); + if ( Lit == 3 ) // const 0 + Vec_IntPush( p->vLits, 0 ); + else if ( Lit == 2 ) // const 1 + Vec_IntPush( p->vLits, 1 ); + else + Vec_IntPush( p->vLits, 2 ); + } + uTruth = Ga2_ObjComputeTruthSpecial( p, pObj, vLeaves, p->vLits ); + if ( uTruth == 0 || uTruth == ~0 ) + Ga2_ObjAddLit( p, pObj, f, uTruth == 0 ? 3 : 2 ); // const 0 / 1 + else if ( uTruth == 0xAAAAAAAA || uTruth == 0x55555555 ) // buffer / inverter + { + Lit = Vec_IntEntry( p->vLits, 0 ); + pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit) ); + Lit = Ga2_ObjFindOrAddLit( p, pLeaf, f ); + Ga2_ObjAddLit( p, pObj, f, Abc_LitNotCond(Lit, uTruth == 0x55555555) ); + } + else + { + // replace numbers of literals by actual literals + Vec_IntForEachEntry( p->vLits, Lit, i ) + { + pLeaf = Gia_ManObj( p->pGia, Vec_IntEntry(vLeaves, Lit) ); + Lit = Ga2_ObjFindOrAddLit(p, pLeaf, f); + Vec_IntWriteEntry( p->vLits, Lit ); + } + // add CNF + iLitOut = Ga2_ObjFindOrAddLit(p, pObj, f); + Ga2_ManCnfAddPrecomputed( p, uTruth, Vec_IntArray(p->vLits), iLitOut ); + } + + } + // propagate literals to the PO and flop outputs + pObjRi = Gia_ManPo( p->pGia, 0 ); + Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(pObjRi), f ); + assert( Lit > 1 ); + Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObjRi) ); + Ga2_ObjAddLit( p, pObj, f, Lit ); + Gia_ManForEachObjVec( p->vAbs, p, pObj, i ) + { + if ( !Gia_ObjIsRo(p->pGia, pObj) ) + continue; + pObjRi = Gia_ObjRoToRi(p->pGia, pObj); + Lit = Ga2_ObjFindLit( p, Gia_ObjFanin0(pObjRi), f ); + assert( Lit > 1 ); + Lit = Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObjRi) ); + Ga2_ObjAddLit( p, pObjRi, f, Lit ); + } +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Vec_IntCheckUnique( Vec_Int_t * p ) +{ + int RetValue; + Vec_Int_t * pDup = Vec_IntDup( p ); + Vec_IntUniqify( pDup ); + RetValue = Vec_IntSize(p) - Vec_IntSize(pDup); + Vec_IntFree( pDup ); + return RetValue; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Ga2_ManRefine( Gla_Man_t * p ) +{ + return NULL; +} + +/**Function************************************************************* + + Synopsis [Performs gate-level abstraction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ga2_ManPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) +{ + Gla_Man_t * p; + Vec_Int_t * vCore, * vPPis; + clock_t clk = clock(); + int i, c, f, Lit, Status, RetValue = -1;; + // start the manager + p = Ga2_ManStart( pAig, pPars ); + // check trivial case + assert( Gia_ManPoNum(pAig) == 1 ); + ABC_FREE( pAig->pCexSeq ); + if ( Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManPo(pAig,0))) ) + { + if ( !Gia_ObjFaninC0(Gia_ManPo(pAig,0)) ) + { + printf( "Sequential miter is trivially UNSAT.\n" ); + return 1; + } + pAig->pCexSeq = Abc_CexMakeTriv( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), 1, 0 ); + printf( "Sequential miter is trivially SAT.\n" ); + return 0; + } + // create gate classes if not given + if ( pAig->vGateClasses == NULL ) + { + pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) ); + Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 ); + Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)), 1 ); + } + // start the manager + p = Gla_ManStart( pAig, pPars ); + p->timeInit = clock() - clk; + // perform initial abstraction + if ( p->pPars->fVerbose ) + { + Abc_Print( 1, "Running gate-level abstraction (GLA) with the following parameters:\n" ); + Abc_Print( 1, "FrameMax = %d ConfMax = %d Timeout = %d RatioMin = %d %%.\n", + pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->nRatioMin ); + Abc_Print( 1, "LearnStart = %d LearnDelta = %d LearnRatio = %d %%.\n", + pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce ); + Abc_Print( 1, "Frame %% Abs PPI FF LUT Confl Cex Vars Clas Lrns Time Mem\n" ); + } + // iterate unrolling + for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ ) + { + // create new SAT solver + Ga2_ManRestart( p ); + // unroll the circuit + for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ ) + { + // add one more time-frame + Ga2_ManUnroll( p, f ); + // check for counter-examples + for ( c = 0; ; c++ ) + { + // perform SAT solving + Lit = Ga2_ObjFindOrAddLit( p, Gia_ManPo(p->pGia, 0), f ); + Status = sat_solver2_solve( pSat, &iLit, &iLit+1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( Status == l_True ) // perform refinement + { + vPPis = Ga2_ManRefine( p ); + if ( vPPis == NULL ) + goto finish; + Vec_IntAppend( p->vAbs, vPPis ); + Vec_IntFree( vPPis ); + if ( Vec_IntCheckUnique(p->vAbs) ) + printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) ); + continue; + } + if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit ) // timeout + goto finish; + if ( Status == l_Undef ) // ran out of resources + goto finish; + assert( RetValue == l_False ); + // derive UNSAT core + vCore = (Vec_Int_t *)Sat_ProofCore( pSat ); + Vec_IntAppend( p->vAbs, vCore ); + Vec_IntSort( p->vAbs, 0 ); // check unique!!! + Vec_IntFree( vCore ); + if ( Vec_IntCheckUnique(p->vAbs) ) + printf( "Vector has %d duplicated entries.\n", Vec_IntCheckUnique(p->vAbs) ); + break; + } + if ( c > 0 ) + { + Vec_IntFreeP( &pAig->vGateClasses ); + pAig->vGateClasses = Ga2_ManTranslate( p ); + break; + } + } + // check if the number of objects is below limit + if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 ) + { + Status = l_Undef; + break; + } + } +finish: + // analize the results + if ( pAig->pCexSeq == NULL ) + { + if ( pAig->vGateClasses != NULL ) + Abc_Print( 1, "Replacing the old abstraction by a new one.\n" ); + Vec_IntFreeP( &pAig->vGateClasses ); + pAig->vGateClasses = Ga2_ManTranslate( p ); + if ( Status == l_Undef ) + { + if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit ) + Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f ); + else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit ) + Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f ); + else if ( Gia_GlaAbsCount(p,0,0) >= (p->nObjs - 1) * (100 - pPars->nRatioMin) / 100 ) + Abc_Print( 1, "The ratio of abstracted objects is less than %d %% in frame %d. ", pPars->nRatioMin, f ); + else + Abc_Print( 1, "Abstraction stopped for unknown reason in frame %d. ", f ); + } + else + { + p->pPars->iFrame++; + Abc_Print( 1, "SAT solver completed %d frames and produced an abstraction. ", f ); + } + } + else + { + if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) ) + Abc_Print( 1, " Gia_GlaPerform(): CEX verification has failed!\n" ); + Abc_Print( 1, "Counter-example detected in frame %d. ", f ); + p->pPars->iFrame = pCex->iFrame - 1; + Vec_IntFreeP( &pAig->vGateClasses ); + } + Abc_PrintTime( 1, "Time", clock() - clk ); + if ( p->pPars->fVerbose ) + { + p->timeOther = (clock() - clk) - p->timeUnsat - p->timeSat - p->timeCex - p->timeInit; + ABC_PRTP( "Runtime: Initializing", p->timeInit, clock() - clk ); + ABC_PRTP( "Runtime: Solver UNSAT", p->timeUnsat, clock() - clk ); + ABC_PRTP( "Runtime: Solver SAT ", p->timeSat, clock() - clk ); + ABC_PRTP( "Runtime: Refinement ", p->timeCex, clock() - clk ); + ABC_PRTP( "Runtime: Other ", p->timeOther, clock() - clk ); + ABC_PRTP( "Runtime: TOTAL ", clock() - clk, clock() - clk ); + Gla_ManReportMemory( p ); + } + Gla_ManStop( p ); + fflush( stdout ); + return RetValue; + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |