diff options
Diffstat (limited to 'src/aig/gia/giaAbsRef.c')
| -rw-r--r-- | src/aig/gia/giaAbsRef.c | 1001 |
1 files changed, 0 insertions, 1001 deletions
diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c deleted file mode 100644 index 8a5aedc5..00000000 --- a/src/aig/gia/giaAbsRef.c +++ /dev/null @@ -1,1001 +0,0 @@ -/**CFile**************************************************************** - - FileName [giaAbsRef.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Scalable AIG package.] - - Synopsis [Refinement manager.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: giaAbsRef.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "gia.h" -#include "giaAbsRef.h" -#include "sat/bsat/satSolver2.h" - -ABC_NAMESPACE_IMPL_START - -/* - Description of the refinement manager - - This refinement manager should be - * started by calling Rnm_ManStart() - this procedure takes one argument, the user's seq miter as a GIA manager - - the manager should have only one property output - - this manager should not change while the refinement manager is alive - - it cannot be used by external applications for any purpose - - when the refinement manager stop, GIA manager is the same as at the beginning - - in the meantime, it will have some data-structures attached to its nodes... - * stopped by calling Rnm_ManStop() - * between starting and stopping, refinements are obtained by calling Rnm_ManRefine() - - Procedure Rnm_ManRefine() takes the following arguments: - * the refinement manager previously started by Rnm_ManStart() - * counter-example (CEX) obtained by abstracting some logic of GIA - * mapping (vMap) of inputs of the CEX into the object IDs of the GIA manager - - only PI, flop outputs, and internal AND nodes can be used in vMap - - the ordering of objects in vMap is not important - - however, the index of a non-PI object in vMap is used as its priority - (the smaller the index, the more likely this non-PI object apears in a refinement) - - only the logic between PO and the objects listed in vMap is traversed by the manager - (as a result, GIA can be arbitrarily large, but only objects used in the abstraction - and the pseudo-PI, that is, objects in the cut, will be visited by the manager) - * flag fPropFanout defines whether value propagation is done through the fanout - - it this flag is enabled, theoretically refinement should be better (the result smaller) - * flag fVerbose may print some statistics - - The refinement manager returns a minimal-size array of integer IDs of GIA objects - which should be added to the abstraction to possibly prevent the given counter-example - - only flop output and internal AND nodes from vMap may appear in the resulting array - - if the resulting array is empty, the CEX is a true CEX - (in other words, non-PI objects are not needed to set the PO value to 1) - - Verification of the selected refinement is performed by - - initializing all PI objects in vMap to value 0 or 1 they have in the CEX - - initializing all remaining objects in vMap to value X - - initializing objects used in the refiment to value 0 or 1 they have in the CEX - - simulating through as many timeframes as required by the CEX - - if the PO value in the last frame is 1, the refinement is correct - (however, the minimality of the refinement is not currently checked) - -*/ - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Rnm_Obj_t_ Rnm_Obj_t; // refinement object -struct Rnm_Obj_t_ -{ - unsigned Value : 1; // binary value - unsigned fVisit : 1; // visited object - unsigned fVisit0 : 1; // visited object - unsigned fPPi : 1; // PPI object - unsigned Prio : 24; // priority (0 - highest) -}; - -struct Rnm_Man_t_ -{ - // user data - Gia_Man_t * pGia; // working AIG manager (it is completely owned by this package) - Abc_Cex_t * pCex; // counter-example - Vec_Int_t * vMap; // mapping of CEX inputs into objects (PI + PPI, in any order) - int fPropFanout; // propagate fanouts - int fVerbose; // verbose flag - // traversing data - Vec_Int_t * vObjs; // internal objects used in value propagation - Vec_Str_t * vCounts; // fanin counters - Vec_Int_t * vFanins; // fanins - // SAT solver - sat_solver2 * pSat; // incremental SAT solver - Vec_Int_t * vSatVars; // SAT variables - Vec_Int_t * vSat2Ids; // mapping of SAT variables into object IDs - Vec_Int_t * vIsopMem; // memory for ISOP computation - // internal data - Rnm_Obj_t * pObjs; // refinement objects - int nObjs; // the number of used objects - int nObjsAlloc; // the number of allocated objects - int nObjsFrame; // the number of used objects in each frame - int nCalls; // total number of calls - int nRefines; // total refined objects - int nVisited; // visited during justification - // statistics - clock_t timeFwd; // forward propagation - clock_t timeBwd; // backward propagation - clock_t timeVer; // ternary simulation - clock_t timeTotal; // other time -}; - -// accessing the refinement object -static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f ) -{ - assert( Gia_ObjIsConst0(pObj) || pObj->Value ); - assert( (int)pObj->Value < p->nObjsFrame ); - assert( f >= 0 && f <= p->pCex->iFrame ); - return p->pObjs + f * p->nObjsFrame + pObj->Value; -} - -static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); } -static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); } -static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); } -static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); } -static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); } -static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; } - -static inline int Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) ); } -static inline void Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c ); } -static inline int Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj ) { int c = Rnm_ObjCount(p, pObj); if ( c < 16 ) Rnm_ObjSetCount(p, pObj, c+1); return c; } - -static inline int Rnm_ObjSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj) ); } -static inline void Rnm_ObjSetSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj, int c) { Vec_IntWriteEntry( p->vSatVars, Gia_ObjId(p->pGia, pObj), c ); } -static inline int Rnm_ObjFindOrAddSatVar( Rnm_Man_t * p, Gia_Obj_t * pObj) { if ( Rnm_ObjSatVar(p, pObj) == 0 ) { Rnm_ObjSetSatVar(p, pObj, Vec_IntSize(p->vSat2Ids)); Vec_IntPush(p->vSat2Ids, Gia_ObjId(p->pGia, pObj)); }; return 2*Rnm_ObjSatVar(p, pObj); } - -extern void Ga2_ManCnfAddStatic( sat_solver2 * pSat, Vec_Int_t * vCnf0, Vec_Int_t * vCnf1, int * pLits, int iLitOut, int ProofId ); - -extern Vec_Int_t * Ga2_ManCnfCompute( unsigned uTruth, int nVars, Vec_Int_t * vCover ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs UNSAT-core-based refinement.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rnm_ManRefineCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vVisited, Vec_Int_t * vFlops ) -{ - Vec_Int_t * vLeaves; - Gia_Obj_t * pFanin; - int k; - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) - return; - Gia_ObjSetTravIdCurrent(p, pObj); - if ( Gia_ObjIsCi(pObj) ) - { - if ( Gia_ObjIsRo(p, pObj) ) - Vec_IntPush( vFlops, Gia_ObjId(p, pObj) ); - return; - } - assert( Gia_ObjIsAnd(pObj) ); - vLeaves = Ga2_ObjLeaves( p, pObj ); - Gia_ManForEachObjVec( vLeaves, p, pFanin, k ) - Rnm_ManRefineCollect_rec( p, pFanin, vVisited, vFlops ); - Vec_IntPush( vVisited, Gia_ObjId(p, pObj) ); -} - -Vec_Int_t * Rnm_ManRefineUnsatCore( Rnm_Man_t * p, Vec_Int_t * vPPIs ) -{ - Vec_Int_t * vCnf0, * vCnf1; - Vec_Int_t * vLeaves, * vLits, * vPpi2Map; - Vec_Int_t * vVisited, * vFlops, * vCore, * vCoreFinal; - Gia_Obj_t * pObj, * pFanin; - int i, k, f, Status, Entry, pLits[5], iBit = p->pCex->nRegs; - // map PPIs into their positions in the map // CAN BE MADE FASTER - vPpi2Map = Vec_IntAlloc( Vec_IntSize(vPPIs) ); - Vec_IntForEachEntry( vPPIs, Entry, i ) - { - Entry = Vec_IntFind( p->vMap, Entry ); - assert( Entry >= 0 ); - Vec_IntPush( vPpi2Map, Entry ); - } - // collect nodes between selected PPIs and CIs - vFlops = Vec_IntAlloc( 100 ); - vVisited = Vec_IntAlloc( 100 ); - Gia_ManIncrementTravId( p->pGia ); - Gia_ManForEachObjVec( vPPIs, p->pGia, pObj, i ) -// if ( !Gia_ObjIsRo(p->pGia, pObj) ) // SKIP PPIs that are flops - Rnm_ManRefineCollect_rec( p->pGia, pObj, vVisited, vFlops ); - // create SAT variables and SAT solver - Vec_IntFill( p->vSat2Ids, 1, -1 ); - assert( p->pSat == NULL ); - p->pSat = sat_solver2_new(); - Vec_IntFill( p->vSatVars, Gia_ManObjNum(p->pGia), 0 ); // NO NEED TO CLEAN EACH TIME - // assign PPI variables - Gia_ManForEachObjVec( vFlops, p->pGia, pObj, i ) - Rnm_ObjFindOrAddSatVar( p, pObj ); - // assign other variables - Gia_ManForEachObjVec( vVisited, p->pGia, pObj, i ) - { - vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) - pLits[k] = Rnm_ObjFindOrAddSatVar( p, pFanin ); - vCnf0 = Ga2_ManCnfCompute( Ga2_ObjTruth(p->pGia, pObj), Vec_IntSize(vLeaves), p->vIsopMem ); - vCnf1 = Ga2_ManCnfCompute( ~Ga2_ObjTruth(p->pGia, pObj), Vec_IntSize(vLeaves), p->vIsopMem ); - Ga2_ManCnfAddStatic( p->pSat, vCnf0, vCnf1, pLits, Rnm_ObjFindOrAddSatVar(p, pObj), Rnm_ObjFindOrAddSatVar(p, pObj)/2 ); - Vec_IntFree( vCnf0 ); - Vec_IntFree( vCnf1 ); - } - -// printf( "\n" ); - - p->pSat->pPrf2 = Prf_ManAlloc(); - Prf_ManRestart( p->pSat->pPrf2, NULL, sat_solver2_nlearnts(p->pSat), Vec_IntSize(p->vSat2Ids) ); - - // iterate UNSAT core computation for each timeframe - vLits = Vec_IntAlloc( 100 ); - vCoreFinal = Vec_IntAlloc( 100 ); - for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) - { - // collect values of PPIs in this timeframe - Vec_IntClear( vLits ); - Gia_ManForEachObjVec( vPPIs, p->pGia, pObj, i ) - { - Entry = Abc_InfoHasBit( p->pCex->pData, iBit + Vec_IntEntry(vPpi2Map, i) ); - Vec_IntPush( vLits, Abc_LitNotCond( Rnm_ObjFindOrAddSatVar(p, pObj), !Entry ) ); - } - - // handle the first timeframe in a special vay - if ( f == 0 ) - Gia_ManForEachObjVec( vFlops, p->pGia, pObj, i ) - if ( Vec_IntFind( vPPIs, Gia_ObjId(p->pGia, pObj) ) == -1 ) - Vec_IntPush( vLits, Abc_LitNotCond( Rnm_ObjFindOrAddSatVar(p, pObj), 1 ) ); -/* - // uniqify literals and detect special conflicts - Vec_IntUniqify( vLits ); - Vec_IntForEachEntryStart( vLits, Entry, i, 1 ) - if ( Vec_IntEntry(vLits, i-1) == Abc_LitNot(Entry) ) - break; - if ( i < Vec_IntSize(vLits) ) - printf( "triv_unsat " ); - else -*/ - - Status = sat_solver2_solve( p->pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - if ( Status != l_False ) - continue; - vCore = (Vec_Int_t *)Sat_ProofCore( p->pSat ); -// vCore = Vec_IntAlloc( 0 ); - // add to the UNSAT core - Vec_IntAppend( vCoreFinal, vCore ); - -// printf( "Frame %d : ", f ); -// Vec_IntPrint( vCore ); - Vec_IntFree( vCore ); - } - assert( iBit == p->pCex->nBits ); - Vec_IntUniqify( vCoreFinal ); - Vec_IntFree( vLits ); - Prf_ManStopP( &p->pSat->pPrf2 ); - sat_solver2_delete( p->pSat ); - p->pSat = NULL; - - // translate from entry into ID - Vec_IntForEachEntry( vCoreFinal, Entry, i ) - { - assert( Vec_IntEntry(p->vSat2Ids, Entry) >= 0 ); - assert( Vec_IntEntry(p->vSat2Ids, Entry) < Gia_ManObjNum(p->pGia) ); - Vec_IntWriteEntry( vCoreFinal, i, Vec_IntEntry(p->vSat2Ids, Entry) ); - } - // if there are flop outputs, add them - Gia_ManForEachObjVec( vPPIs, p->pGia, pObj, i ) - if ( Gia_ObjIsRo(p->pGia, pObj) ) - Vec_IntPush( vCoreFinal, Gia_ObjId(p->pGia, pObj) ); - Vec_IntUniqify( vCoreFinal ); - -// printf( "\n" ); -// Vec_IntPrint( vPPIs ); -// Vec_IntPrint( vCoreFinal ); - -// printf( "\n" ); - - // clean SAT variable numbers - Gia_ManForEachObjVec( vVisited, p->pGia, pObj, i ) - { - Rnm_ObjSetSatVar( p, pObj, 0 ); - vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) - Rnm_ObjSetSatVar( p, pFanin, 0 ); - } - Vec_IntFree( vFlops ); - Vec_IntFree( vVisited ); - Vec_IntFree( vPpi2Map ); - return vCoreFinal; -} - - -/**Function************************************************************* - - Synopsis [Creates a new manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Rnm_Man_t * Rnm_ManStart( Gia_Man_t * pGia ) -{ - Rnm_Man_t * p; - assert( Gia_ManPoNum(pGia) == 1 ); - p = ABC_CALLOC( Rnm_Man_t, 1 ); - p->pGia = pGia; - p->vObjs = Vec_IntAlloc( 100 ); - p->vCounts = Vec_StrStart( Gia_ManObjNum(pGia) ); - p->vFanins = Vec_IntAlloc( 1000 ); - p->vSatVars = Vec_IntAlloc( 0 ); - p->vSat2Ids = Vec_IntAlloc( 1000 ); - p->vIsopMem = Vec_IntAlloc( 0 ); - p->nObjsAlloc = 10000; - p->pObjs = ABC_ALLOC( Rnm_Obj_t, p->nObjsAlloc ); - if ( p->pGia->vFanout == NULL ) - Gia_ManStaticFanoutStart( p->pGia ); - Gia_ManCleanValue(pGia); - Gia_ManCleanMark0(pGia); - Gia_ManCleanMark1(pGia); - return p; -} -void Rnm_ManStop( Rnm_Man_t * p, int fProfile ) -{ - if ( !p ) return; - // print runtime statistics - if ( fProfile && p->nCalls ) - { - double MemGia = sizeof(Gia_Man_t) + sizeof(Gia_Obj_t) * p->pGia->nObjsAlloc + sizeof(int) * p->pGia->nTravIdsAlloc; - double MemOther = sizeof(Rnm_Man_t) + sizeof(Rnm_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs); - clock_t timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer; - printf( "Abstraction refinement runtime statistics:\n" ); - ABC_PRTP( "Sensetization", p->timeFwd, p->timeTotal ); - ABC_PRTP( "Justification", p->timeBwd, p->timeTotal ); - ABC_PRTP( "Verification ", p->timeVer, p->timeTotal ); - ABC_PRTP( "Other ", timeOther, p->timeTotal ); - ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); - printf( "Total calls = %d. Average refine = %.1f. GIA mem = %.3f MB. Other mem = %.3f MB.\n", - p->nCalls, 1.0*p->nRefines/p->nCalls, MemGia/(1<<20), MemOther/(1<<20) ); - } - - Gia_ManCleanMark0(p->pGia); - Gia_ManCleanMark1(p->pGia); - Gia_ManStaticFanoutStop(p->pGia); -// Gia_ManSetPhase(p->pGia); - Vec_IntFree( p->vIsopMem ); - Vec_IntFree( p->vSatVars ); - Vec_IntFree( p->vSat2Ids ); - Vec_StrFree( p->vCounts ); - Vec_IntFree( p->vFanins ); - Vec_IntFree( p->vObjs ); - ABC_FREE( p->pObjs ); - ABC_FREE( p ); -} -double Rnm_ManMemoryUsage( Rnm_Man_t * p ) -{ - return (double)(sizeof(Rnm_Man_t) + sizeof(Rnm_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs)); -} - - -/**Function************************************************************* - - Synopsis [Collect internal objects to be used in value propagation.] - - Description [Resulting array vObjs contains RO, AND, PO/RI in a topo order.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rnm_ManCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vObjs, int nAddOn ) -{ - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) - return; - Gia_ObjSetTravIdCurrent(p, pObj); - if ( Gia_ObjIsCo(pObj) ) - Rnm_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs, nAddOn ); - else if ( Gia_ObjIsAnd(pObj) ) - { - Rnm_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs, nAddOn ); - Rnm_ManCollect_rec( p, Gia_ObjFanin1(pObj), vObjs, nAddOn ); - } - else if ( !Gia_ObjIsRo(p, pObj) ) - assert( 0 ); - pObj->Value = Vec_IntSize(vObjs) + nAddOn; - Vec_IntPush( vObjs, Gia_ObjId(p, pObj) ); -} -void Rnm_ManCollect( Rnm_Man_t * p ) -{ - Gia_Obj_t * pObj = NULL; - int i; - // mark const/PIs/PPIs - Gia_ManIncrementTravId( p->pGia ); - Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) ); - Gia_ManConst0(p->pGia)->Value = 0; - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); - Gia_ObjSetTravIdCurrent( p->pGia, pObj ); - pObj->Value = 1 + i; - } - // collect objects - Vec_IntClear( p->vObjs ); - Rnm_ManCollect_rec( p->pGia, Gia_ManPo(p->pGia, 0), p->vObjs, 1 + Vec_IntSize(p->vMap) ); - Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) - if ( Gia_ObjIsRo(p->pGia, pObj) ) - Rnm_ManCollect_rec( p->pGia, Gia_ObjRoToRi(p->pGia, pObj), p->vObjs, 1 + Vec_IntSize(p->vMap) ); - // the last object should be a CO - assert( Gia_ObjIsCo(pObj) ); - assert( (int)pObj->Value == Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) ); -} -void Rnm_ManCleanValues( Rnm_Man_t * p ) -{ - Gia_Obj_t * pObj; - int i; - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - pObj->Value = 0; - Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) - pObj->Value = 0; -} - -/**Function************************************************************* - - Synopsis [Performs sensitization analysis.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Rnm_ManSensitize( Rnm_Man_t * p ) -{ - Rnm_Obj_t * pRnm, * pRnm0, * pRnm1; - Gia_Obj_t * pObj; - int f, i, iBit = p->pCex->nRegs; - // const0 is initialized automatically in all timeframes - for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis ) - { - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) ); - pRnm = Rnm_ManObj( p, pObj, f ); - pRnm->Value = Abc_InfoHasBit( p->pCex->pData, iBit + i ); - if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI - { - assert( pObj->Value > 0 ); - pRnm->Prio = pObj->Value; - pRnm->fPPi = 1; - } - } - Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i ) - { - assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) ); - pRnm = Rnm_ManObj( p, pObj, f ); - assert( !pRnm->fPPi ); - if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - if ( f == 0 ) - continue; - pRnm0 = Rnm_ManObj( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 ); - pRnm->Value = pRnm0->Value; - pRnm->Prio = pRnm0->Prio; - continue; - } - if ( Gia_ObjIsCo(pObj) ) - { - pRnm0 = Rnm_ManObj( p, Gia_ObjFanin0(pObj), f ); - pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj)); - pRnm->Prio = pRnm0->Prio; - continue; - } - assert( Gia_ObjIsAnd(pObj) ); - pRnm0 = Rnm_ManObj( p, Gia_ObjFanin0(pObj), f ); - pRnm1 = Rnm_ManObj( p, Gia_ObjFanin1(pObj), f ); - pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) & (pRnm1->Value ^ Gia_ObjFaninC1(pObj)); - if ( pRnm->Value == 1 ) - pRnm->Prio = Abc_MaxInt( pRnm0->Prio, pRnm1->Prio ); - else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRnm1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) - pRnm->Prio = Abc_MinInt( pRnm0->Prio, pRnm1->Prio ); // choice - else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 ) - pRnm->Prio = pRnm0->Prio; - else - pRnm->Prio = pRnm1->Prio; - } - } - assert( iBit == p->pCex->nBits ); - pRnm = Rnm_ManObj( p, Gia_ManPo(p->pGia, 0), p->pCex->iFrame ); - if ( pRnm->Value != 1 ) - printf( "Output value is incorrect.\n" ); - return pRnm->Prio; -} - - -/**Function************************************************************* - - Synopsis [Drive implications of the given node towards primary outputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rnm_ManJustifyPropFanout_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect ) -{ - Rnm_Obj_t * pRnm0, * pRnm1, * pRnm = Rnm_ManObj( p, pObj, f ); - Gia_Obj_t * pFanout = NULL; - int i, k;//, Id = Gia_ObjId(p->pGia, pObj); - assert( pRnm->fVisit == 0 ); - pRnm->fVisit = 1; - if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 ) - { - Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1; - p->nVisited++; - } - if ( pRnm->fPPi ) - { - assert( (int)pRnm->Prio > 0 ); - for ( i = p->pCex->iFrame; i >= 0; i-- ) - if ( !Rnm_ManObj(p, pObj, i)->fVisit ) - Rnm_ManJustifyPropFanout_rec( p, pObj, i, vSelect ); - Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) ); - return; - } - if ( (Gia_ObjIsCo(pObj) && f == p->pCex->iFrame) || Gia_ObjIsPo(p->pGia, pObj) ) - return; - if ( Gia_ObjIsRi(p->pGia, pObj) ) - { - pFanout = Gia_ObjRiToRo(p->pGia, pObj); - if ( !Rnm_ManObj(p, pFanout, f+1)->fVisit ) - Rnm_ManJustifyPropFanout_rec( p, pFanout, f+1, vSelect ); - return; - } - assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) ); - Gia_ObjForEachFanoutStatic( p->pGia, pObj, pFanout, k ) - { - Rnm_Obj_t * pRnmF; - if ( pFanout->Value == 0 ) - continue; - pRnmF = Rnm_ManObj(p, pFanout, f); - if ( pRnmF->fPPi || pRnmF->fVisit ) - continue; - if ( Gia_ObjIsCo(pFanout) ) - { - Rnm_ManJustifyPropFanout_rec( p, pFanout, f, vSelect ); - continue; - } - assert( Gia_ObjIsAnd(pFanout) ); - pRnm0 = Rnm_ManObj( p, Gia_ObjFanin0(pFanout), f ); - pRnm1 = Rnm_ManObj( p, Gia_ObjFanin1(pFanout), f ); - if ( ((pRnm0->Value ^ Gia_ObjFaninC0(pFanout)) == 0 && pRnm0->fVisit) || - ((pRnm1->Value ^ Gia_ObjFaninC1(pFanout)) == 0 && pRnm1->fVisit) || - ( ((pRnm0->Value ^ Gia_ObjFaninC0(pFanout)) == 1 && pRnm0->fVisit) && - ((pRnm1->Value ^ Gia_ObjFaninC1(pFanout)) == 1 && pRnm1->fVisit) ) ) - Rnm_ManJustifyPropFanout_rec( p, pFanout, f, vSelect ); - } -} -void Rnm_ManJustify_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect ) -{ - Rnm_Obj_t * pRnm = Rnm_ManObj( p, pObj, f ); - int i;//, Id = Gia_ObjId(p->pGia, pObj); - if ( pRnm->fVisit ) - return; - if ( p->fPropFanout ) - Rnm_ManJustifyPropFanout_rec( p, pObj, f, vSelect ); - else - { - pRnm->fVisit = 1; - if ( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 ) - { - Rnm_ManObj( p, pObj, 0 )->fVisit0 = 1; - p->nVisited++; - } - } - if ( pRnm->fPPi ) - { - assert( (int)pRnm->Prio > 0 ); - if ( p->fPropFanout ) - { - for ( i = p->pCex->iFrame; i >= 0; i-- ) - if ( !Rnm_ManObj(p, pObj, i)->fVisit ) - Rnm_ManJustifyPropFanout_rec( p, pObj, i, vSelect ); - } - else - { - Vec_IntPush( vSelect, Gia_ObjId(p->pGia, pObj) ); -// for ( i = p->pCex->iFrame; i >= 0; i-- ) -// Rnm_ManObj(p, pObj, i)->fVisit = 1; - } - return; - } - if ( Gia_ObjIsPi(p->pGia, pObj) || Gia_ObjIsConst0(pObj) ) - return; - if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - if ( f > 0 ) - Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)), f-1, vSelect ); - return; - } - if ( Gia_ObjIsAnd(pObj) ) - { - Rnm_Obj_t * pRnm0 = Rnm_ManObj( p, Gia_ObjFanin0(pObj), f ); - Rnm_Obj_t * pRnm1 = Rnm_ManObj( p, Gia_ObjFanin1(pObj), f ); - if ( pRnm->Value == 1 ) - { - if ( pRnm0->Prio > 0 ) - Rnm_ManJustify_rec( p, Gia_ObjFanin0(pObj), f, vSelect ); - if ( pRnm1->Prio > 0 ) - Rnm_ManJustify_rec( p, Gia_ObjFanin1(pObj), f, vSelect ); - } - else // select one value - { - if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRnm1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) - { - if ( pRnm0->Prio <= pRnm1->Prio ) // choice - { - if ( pRnm0->Prio > 0 ) - Rnm_ManJustify_rec( p, Gia_ObjFanin0(pObj), f, vSelect ); - } - else - { - if ( pRnm1->Prio > 0 ) - Rnm_ManJustify_rec( p, Gia_ObjFanin1(pObj), f, vSelect ); - } - } - else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 ) - { - if ( pRnm0->Prio > 0 ) - Rnm_ManJustify_rec( p, Gia_ObjFanin0(pObj), f, vSelect ); - } - else if ( (pRnm1->Value ^ Gia_ObjFaninC1(pObj)) == 0 ) - { - if ( pRnm1->Prio > 0 ) - Rnm_ManJustify_rec( p, Gia_ObjFanin1(pObj), f, vSelect ); - } - else assert( 0 ); - } - } - else assert( 0 ); -} - -/**Function************************************************************* - - Synopsis [Performs refinement.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rnm_ManVerifyUsingTerSim( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, Vec_Int_t * vObjs, Vec_Int_t * vRes ) -{ - Gia_Obj_t * pObj; - int i, f, iBit = pCex->nRegs; - Gia_ObjTerSimSet0( Gia_ManConst0(p) ); - for ( f = 0; f <= pCex->iFrame; f++, iBit += pCex->nPis ) - { - Gia_ManForEachObjVec( vMap, p, pObj, i ) - { - pObj->Value = Abc_InfoHasBit( pCex->pData, iBit + i ); - if ( !Gia_ObjIsPi(p, pObj) ) - Gia_ObjTerSimSetX( pObj ); - else if ( pObj->Value ) - Gia_ObjTerSimSet1( pObj ); - else - Gia_ObjTerSimSet0( pObj ); - } - Gia_ManForEachObjVec( vRes, p, pObj, i ) // vRes is subset of vMap - { - if ( pObj->Value ) - Gia_ObjTerSimSet1( pObj ); - else - Gia_ObjTerSimSet0( pObj ); - } - Gia_ManForEachObjVec( vObjs, p, pObj, i ) - { - if ( Gia_ObjIsCo(pObj) ) - Gia_ObjTerSimCo( pObj ); - else if ( Gia_ObjIsAnd(pObj) ) - Gia_ObjTerSimAnd( pObj ); - else if ( f == 0 ) - Gia_ObjTerSimSet0( pObj ); - else - Gia_ObjTerSimRo( p, pObj ); - } - } - Gia_ManForEachObjVec( vMap, p, pObj, i ) - pObj->Value = 0; - pObj = Gia_ManPo( p, 0 ); - if ( !Gia_ObjTerSimGet1(pObj) ) - Abc_Print( 1, "\nRefinement verification has failed!!!\n" ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Rnm_ManPrintSelected( Rnm_Man_t * p, Vec_Int_t * vSelected ) -{ - Gia_Obj_t * pObj; - int i, Counter = 0; - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - { - if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI - { - if ( Vec_IntFind(vSelected, Gia_ObjId(p->pGia, pObj)) >= 0 ) - printf( "1" ), Counter++; - else - printf( "0" ); - } - else - printf( "-" ); - } - printf( " %3d\n", Counter ); -} - - - - - -/**Function************************************************************* - - Synopsis [Perform structural analysis.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Ga2_StructAnalize( Gia_Man_t * p, Vec_Int_t * vFront, Vec_Int_t * vInter, Vec_Int_t * vSelect ) -{ - Vec_Int_t * vLeaves; - Gia_Obj_t * pObj, * pFanin; - int i, k; - // clean labels - Gia_ManForEachObj( p, pObj, i ) - pObj->fMark0 = pObj->fMark1 = 0; - // label frontier - Gia_ManForEachObjVec( vFront, p, pObj, i ) - pObj->fMark0 = 1, pObj->fMark1 = 0; - // label objects - Gia_ManForEachObjVec( vInter, p, pObj, i ) - pObj->fMark1 = 0, pObj->fMark1 = 1; - // label selected - Gia_ManForEachObjVec( vSelect, p, pObj, i ) - pObj->fMark1 = 1, pObj->fMark1 = 1; - // explore selected - printf( "\n" ); - Gia_ManForEachObjVec( vSelect, p, pObj, i ) - { - printf( "Selected %6d : ", Gia_ObjId(p, pObj) ); - printf( "\n" ); - vLeaves = Ga2_ObjLeaves( p, pObj ); - Gia_ManForEachObjVec( vLeaves, p, pFanin, k ) - { - printf( " " ); - printf( "%6d ", Gia_ObjId(p, pFanin) ); - if ( pFanin->fMark0 && pFanin->fMark1 ) - printf( "select" ); - else if ( pFanin->fMark0 && !pFanin->fMark1 ) - printf( "front" ); - else if ( !pFanin->fMark0 && pFanin->fMark1 ) - printf( "internal" ); - else if ( !pFanin->fMark0 && !pFanin->fMark1 ) - printf( "new" ); - printf( "\n" ); - } - } -} - - -/**Function************************************************************* - - Synopsis [Finds essential objects.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Ga2_FilterSelected( Rnm_Man_t * p, Vec_Int_t * vSelect ) -{ - Vec_Int_t * vNew, * vLeaves; - Gia_Obj_t * pObj, * pFanin; - int i, k, RetValue;//, Counters[3] = {0}; -/* - // check that selected are not visited - Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i ) - assert( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 1 ); - Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i ) - if ( Vec_IntFind(vSelect, Gia_ObjId(p->pGia, pObj)) == -1 ) - assert( Rnm_ManObj( p, pObj, 0 )->fVisit0 == 0 ); -*/ - - // verify -// Gia_ManForEachObj( p->pGia, pObj, i ) -// assert( Rnm_ObjCount(p, pObj) == 0 ); - - // increment fanin counters - Vec_IntClear( p->vFanins ); - Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i ) - { - vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) - if ( Rnm_ObjAddToCount(p, pFanin) == 0 ) - Vec_IntPush( p->vFanins, Gia_ObjId(p->pGia, pFanin) ); - } - - // find selected objects, which create potential constraints - // - flop objects - // - objects whose fanin belongs to the justified area - // - objects whose fanins overlap - // (these do not guantee reconvergence, but may potentially have it) - // (other objects cannot have reconvergence, even if they are added) - vNew = Vec_IntAlloc( 100 ); - Gia_ManForEachObjVec( vSelect, p->pGia, pObj, i ) - { - if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - Vec_IntPush( vNew, Gia_ObjId(p->pGia, pObj) ); - continue; - } - vLeaves = Ga2_ObjLeaves( p->pGia, pObj ); - Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) - { - if ( Gia_ObjIsConst0(pFanin) - || (pFanin->Value && Rnm_ManObj(p, pFanin, 0)->fVisit0 == 1) - || Rnm_ObjCount(p, pFanin) > 1 - ) - { - Vec_IntPush( vNew, Gia_ObjId(p->pGia, pObj) ); - break; - } - } -// Gia_ManForEachObjVec( vLeaves, p->pGia, pFanin, k ) -// { -// Counters[1] += (pFanin->Value && Rnm_ManObj( p, pFanin, 0 )->fVisit0 == 1); -// Counters[2] += (Rnm_ObjCount(p, pFanin) > 1); -// } - } - RetValue = Vec_IntUniqify( vNew ); - assert( RetValue == 0 ); - -// printf( "\n*** Select = %5d. New = %5d. Flops = %5d. Visited = %5d. Fanins = %5d.\n", -// Vec_IntSize(vSelect), Vec_IntSize(vNew), Counters[0], Counters[1], Counters[2] ); - - // clear fanin counters - Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i ) - Rnm_ObjSetCount( p, pObj, 0 ); - return vNew; -} - - -/**Function************************************************************* - - Synopsis [Computes the refinement for a given counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fPostProcess, int fVerbose ) -{ - int fVerify = 0; -// int fPostProcess = 1; - Vec_Int_t * vSelected = Vec_IntAlloc( 100 ); - Vec_Int_t * vNew; - clock_t clk, clk2 = clock(); - int RetValue; - p->nCalls++; -// Gia_ManCleanValue( p->pGia ); - // initialize - p->pCex = pCex; - p->vMap = vMap; - p->fPropFanout = fPropFanout; - p->fVerbose = fVerbose; - // collects used objects - Rnm_ManCollect( p ); - // initialize datastructure - p->nObjsFrame = 1 + Vec_IntSize(vMap) + Vec_IntSize(p->vObjs); - p->nObjs = p->nObjsFrame * (pCex->iFrame + 1); - if ( p->nObjs > p->nObjsAlloc ) - p->pObjs = ABC_REALLOC( Rnm_Obj_t, p->pObjs, (p->nObjsAlloc = p->nObjs + 10000) ); - memset( p->pObjs, 0, sizeof(Rnm_Obj_t) * p->nObjs ); - // propagate priorities - clk = clock(); - if ( Rnm_ManSensitize( p ) ) // the CEX is not a true CEX - { - p->timeFwd += clock() - clk; - // select refinement - clk = clock(); - p->nVisited = 0; - Rnm_ManJustify_rec( p, Gia_ObjFanin0(Gia_ManPo(p->pGia, 0)), pCex->iFrame, vSelected ); - RetValue = Vec_IntUniqify( vSelected ); -// assert( RetValue == 0 ); - p->timeBwd += clock() - clk; - } - - if ( fPostProcess ) - { - vNew = Ga2_FilterSelected( p, vSelected ); - if ( Vec_IntSize(vNew) > 0 ) - { - Vec_IntFree( vSelected ); - vSelected = vNew; - } - else - { - Vec_IntFree( vNew ); - // printf( "\nBig refinement.\n" ); - } - } - else - { -/* - vNew = Rnm_ManRefineUnsatCore( p, vSelected ); - if ( Vec_IntSize(vNew) > 0 ) - { - Vec_IntFree( vSelected ); - vSelected = vNew; -// Vec_IntFree( vNew ); - } - else - { - Vec_IntFree( vNew ); - // printf( "\nBig refinement.\n" ); - } -*/ - } - - // clean values - Rnm_ManCleanValues( p ); - - // verify (empty) refinement - if ( fVerify ) - { - clk = clock(); - Rnm_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected ); - p->timeVer += clock() - clk; - } - -// printf( "\nOriginal (%d): \n", Vec_IntSize(p->vMap) ); -// Rnm_ManPrintSelected( p, vSelected ); - -// Ga2_StructAnalize( p->pGia, vMap, p->vObjs, vSelected ); -// printf( "\nObjects = %5d. Visited = %5d.\n", Vec_IntSize(p->vObjs), p->nVisited ); - -// Vec_IntReverseOrder( vSelected ); - p->timeTotal += clock() - clk2; - p->nRefines += Vec_IntSize(vSelected); - return vSelected; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |