/**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