From 36bc5703adc870bd6c8cb143dd638fe33a1e74b2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 7 Jan 2012 12:11:25 +0700 Subject: Gate level abstraction. --- src/aig/gia/giaAbsVta.c | 316 ++++++++++++------------------------------------ 1 file changed, 78 insertions(+), 238 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index 7cc00556..12d83132 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -28,6 +28,22 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +typedef struct Vta_Obj_t_ Vta_Obj_t; // object +struct Vta_Obj_t_ +{ + int iObj; + int iFrame; + int iNext; + unsigned Prio : 24; + unsigned Value : 2; + unsigned fAdded : 1; + unsigned fVisit : 1; + unsigned fPi : 1; + unsigned fConst : 1; + int fFlop : 1; + int fAnd : 1; +}; + typedef struct Vta_Man_t_ Vta_Man_t; // manager struct Vta_Man_t_ { @@ -38,138 +54,26 @@ struct Vta_Man_t_ int nTimeMax; int fVerbose; // internal data - int nSatVars; // the number of SAT variables - int nObjUsed; // the number objects used - int Shift; // bit count for obj number - int Mask; // bit mask for obj number - Vec_Int_t * vOrder; // map Num to Id - Vec_Int_t * vId2Num; // map Id to Num - Vec_Int_t * vFraLims; // frame limits - Vec_Int_t * vOne2Sat; // map (Frame; Num) to Sat - Vec_Int_t * vCla2One; // map clause to (Frame; Num) - Vec_Int_t * vNumAbs; // abstraction for each timeframe + int nObjs; // the number of objects + int nObjsAlloc; // the number of objects + int nBins; // number of hash table entries + int * pBins; // hash table bins + Vta_Obj_t * pObjs; // hash table bins + // other data + Vec_Int_t * vTemp; sat_solver2 * pSat; }; -static inline int Vta_FraNum2One( Vta_Man_t * p, int f, int n ) { return (f << p->Shift) | n; } -static inline int Vta_One2Fra( Vta_Man_t * p, int i ) { return i >> p->Shift; } -static inline int Vta_One2Num( Vta_Man_t * p, int i ) { return i & p->Mask; } - -static inline void Vta_SetSatVar( Vta_Man_t * p, int f, int n ) -{ - int One = Vta_FraNum2One( p, f, n ); - int * pPlace = Vec_IntEntryP( p->vOne2Sat, One ); - assert( *pPlace == 0 ); - *pPlace = p->nSatVars++; - // create additional var for ROs of frame 0 -} -static inline int Vta_GetSatVar( Vta_Man_t * p, int f, int n ) -{ - int One = Vta_FraNum2One( p, f, n ); - int * pPlace = Vec_IntEntryP( p->vOne2Sat, One ); - assert( *pPlace == 0 ); - return *pPlace; -} -static inline int Vta_GetSatVarObj( Vta_Man_t * p, int f, Gia_Obj_t * pObj ) -{ - return Vta_GetSatVar( p, f, Vec_IntEntry(p->vId2Num, Gia_ObjId(p->pGia, pObj)) ); -} - -extern Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_Int_t ** pvRoots ); - -// check the first value of vOrder!!! +static inline Vta_Obj_t * Vec_ManObj( Vta_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; } +static inline int Vta_ObjId( Vta_Man_t * p, Vta_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Adds one time-frame to the solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Vga_ManGrow( Vta_Man_t * p, int fThis ) -{ - static int PrevF = -1; - Gia_Obj_t * pObj, * pObj2; - int Beg, End, One, i, c, f, iOutVar, nClauses; - assert( ++PrevF == fThis ); - assert( fThis >= 0 && fThis < p->nFramesMax ); - - // create variable for the output - iOutVar = p->nSatVars++; - - // add variables for this frame - for ( f = fThis; f >= 0; f-- ) - { - Beg = Vec_IntEntry( p->vFraLims, fThis-f ); - End = Vec_IntEntry( p->vFraLims, fThis-f+1 ); - for ( i = End-1; i >= Beg; i-- ) - Vta_SetSatVar( p, f, i ); - } - - // create clauses for the output - pObj = Gia_ManPo( p->pGia, 0 ); - nClauses = sat_solver2_add_buffer( p->pSat, - iOutVar, - Vta_GetSatVarObj( p, f, Gia_ObjFanin0(pObj) ), - Gia_ObjFaninC0(pObj), 0 ); - - // add clauses for this frame - for ( f = fThis; f >= 0; f-- ) - { - Beg = Vec_IntEntry( p->vFraLims, fThis-f ); - End = Vec_IntEntry( p->vFraLims, fThis-f+1 ); - for ( i = End-1; i >= Beg; i-- ) - { - nClauses = 0; - pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vOrder, i) ); - if ( Gia_ObjIsAnd(pObj) ) - nClauses = sat_solver2_add_and( p->pSat, - Vta_GetSatVarObj( p, f, pObj ), - Vta_GetSatVarObj( p, f, Gia_ObjFanin0(pObj) ), - Vta_GetSatVarObj( p, f, Gia_ObjFanin1(pObj) ), - Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); - else if ( Gia_ObjIsRo(p->pGia, pObj) ) - { - if ( f == 0 ) - { - nClauses = sat_solver2_add_constraint( p->pSat, - Vta_GetSatVarObj( p, f, pObj ), - 1, 0 ); - } - else - { - pObj2 = Gia_ObjRoToRi(p->pGia, pObj); - nClauses = sat_solver2_add_buffer( p->pSat, - Vta_GetSatVarObj( p, f, pObj ), - Vta_GetSatVarObj( p, f-1, Gia_ObjFanin0(pObj2) ), - Gia_ObjFaninC0(pObj2), 0 ); - } - } - else if ( Gia_ObjIsConst0(pObj) ) - { - nClauses = sat_solver2_add_const( p->pSat, - Vta_GetSatVarObj( p, f, pObj ), - 1, 0 ); - } - One = Vta_FraNum2One( p, f, i ); - for ( c = 0; c < nClauses; c++ ) - Vec_IntPush( p->vCla2One, One ); - } - } -} - /**Function************************************************************* - Synopsis [Create manager.] + Synopsis [] Description [] @@ -189,22 +93,14 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, int nFramesMax, int nConfMax, int nT p->nTimeMax = nTimeMax; p->fVerbose = fVerbose; // internal data - p->vOrder = Gia_VtaCollect( pGia, &p->vFraLims, NULL ); - Vec_IntWriteEntry( p->vOrder, 0, 0 ); - p->vId2Num = Vec_IntInvert( p->vOrder, 0 ); - Vec_IntWriteEntry( p->vOrder, 0, -1 ); - Vec_IntWriteEntry( p->vId2Num, 0, -1 ); - // internal data - p->nObjUsed = Vec_IntEntry( p->vFraLims, nFramesMax ); - p->Shift = Gia_Base2Log( p->nObjUsed ); - p->Mask = (1 << p->Shift) - 1; - // internal data - p->vOne2Sat = Vec_IntStart( (1 << p->Shift) * nFramesMax ); - p->vCla2One = Vec_IntAlloc( 100000 ); Vec_IntPush( p->vCla2One, -1 ); - p->vNumAbs = Vec_IntAlloc( p->nObjUsed ); + p->nObjsAlloc = (1 << 20); + p->pObjs = ABC_CALLOC( Vta_Obj_t, p->nObjsAlloc ); + p->nObjs = 1; + p->nBins = Gia_PrimeCudd( p->nObjsAlloc/3 ); + p->pBins = ABC_CALLOC( int, p->nBins ); + // other data + p->vTemp = Vec_IntAlloc( 1000 ); p->pSat = sat_solver2_new(); - sat_solver2_setnvars( p->pSat, 10000 ); - p->nSatVars = 1; return p; } @@ -221,12 +117,10 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, int nFramesMax, int nConfMax, int nT ***********************************************************************/ void Vga_ManStop( Vta_Man_t * p ) { - Vec_IntFreeP( &p->vOrder ); - Vec_IntFreeP( &p->vId2Num ); - Vec_IntFreeP( &p->vFraLims ); - Vec_IntFreeP( &p->vOne2Sat ); - Vec_IntFreeP( &p->vCla2One ); + Vec_IntFreeP( &p->vTemp ); sat_solver2_delete( p->pSat ); + ABC_FREE( p->pBins ); + ABC_FREE( p->pObjs ); ABC_FREE( p ); } @@ -234,7 +128,7 @@ void Vga_ManStop( Vta_Man_t * p ) /**Function************************************************************* - Synopsis [Duplicate AIG with the given ordering of nodes.] + Synopsis [] Description [] @@ -243,35 +137,14 @@ void Vga_ManStop( Vta_Man_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_VtaDup( Gia_Man_t * p, Vec_Int_t * vOrder ) +static inline int Vga_ManHash( int iObj, int iFrame, int nBins ) { - Gia_Man_t * pNew; - Gia_Obj_t * pObj; - int i, nFlops = 0; - Gia_ManFillValue( p ); - pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); - Gia_ManConst0(p)->Value = 0; - Gia_ManForEachPi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi(pNew); - Gia_ManForEachObjVec( vOrder, p, pObj, i ) - if ( i && Gia_ObjIsRo(p, pObj) ) - pObj->Value = Gia_ManAppendCi(pNew), nFlops++; - Gia_ManForEachObjVec( vOrder, p, pObj, i ) - if ( i && Gia_ObjIsAnd(pObj) ) - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManForEachPo( p, pObj, i ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManForEachObjVec( vOrder, p, pObj, i ) - if ( i && Gia_ObjIsRo(p, pObj) && (pObj = Gia_ObjRoToRi(p, pObj)) ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManSetRegNum( pNew, nFlops ); - return pNew; + return ((iObj + iFrame)*(iObj + iFrame + 1)) % nBins; } /**Function************************************************************* - Synopsis [Collect nodes/flops involved in different timeframes.] + Synopsis [] Description [] @@ -280,26 +153,46 @@ Gia_Man_t * Gia_VtaDup( Gia_Man_t * p, Vec_Int_t * vOrder ) SeeAlso [] ***********************************************************************/ -void Gia_VtaCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vOrder, Vec_Int_t * vRoots ) +static inline int * Vga_ManLookup( Vta_Man_t * p, int iObj, int iFrame ) +{ + Vta_Obj_t * pThis; + int * pPlace = p->pBins + Vga_ManHash( iObj, iFrame, p->nBins ); + for ( pThis = Vec_ManObj(p, *pPlace); + pThis; pPlace = &pThis->iNext, + pThis = Vec_ManObj(p, *pPlace) ) + if ( pThis->iObj == iObj && pThis->iFrame == iFrame ) + break; + return pPlace; +} +static inline Vta_Obj_t * Vga_ManFind( Vta_Man_t * p, int iObj, int iFrame ) +{ + int * pPlace = Vga_ManLookup( p, iObj, iFrame ); + return Vec_ManObj(p, *pPlace); +} +static inline Vta_Obj_t * Vga_ManFindOrAdd( Vta_Man_t * p, int iObj, int iFrame ) { - if ( pObj->fMark0 ) - return; - pObj->fMark0 = 1; - if ( Gia_ObjIsConst0(pObj) ) - return; - if ( Gia_ObjIsAnd(pObj) ) - { - Gia_VtaCollect_rec( p, Gia_ObjFanin0(pObj), vOrder, vRoots ); - Gia_VtaCollect_rec( p, Gia_ObjFanin1(pObj), vOrder, vRoots ); - } - else if ( Gia_ObjIsRo(p, pObj) ) - Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) ); - Vec_IntPush( vOrder, Gia_ObjId(p, pObj) ); + int * pPlace = Vga_ManLookup( p, iObj, iFrame ); + Vta_Obj_t * pThis = Vec_ManObj(p, *pPlace); + if ( pThis ) + return pThis; + *pPlace = p->nObjs++; + pThis = Vec_ManObj(p, *pPlace); + pThis->iObj = iObj; + pThis->iFrame = iFrame; + return pThis; +} +static inline void Vga_ManDelete( Vta_Man_t * p, int iObj, int iFrame ) +{ + int * pPlace = Vga_ManLookup( p, iObj, iFrame ); + Vta_Obj_t * pThis = Vec_ManObj(p, *pPlace); + assert( pThis != NULL ); + *pPlace = pThis->iNext; + pThis->iNext = -1; } /**Function************************************************************* - Synopsis [Collect nodes/flops involved in different timeframes.] + Synopsis [] Description [] @@ -308,62 +201,6 @@ void Gia_VtaCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vOrder, Ve SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_Int_t ** pvRoots ) -{ - Vec_Int_t * vOrder; // resulting ordering of PI/RO/And - Vec_Int_t * vFraLims; // frame limits - Vec_Int_t * vRoots; // CO roots - Gia_Obj_t * pObj; - int i, StopPoint; - - Gia_ManCheckMark0( p ); - - // create roots - vRoots = Vec_IntAlloc( 1000 ); - Gia_ManForEachPo( p, pObj, i ) - Vec_IntPush( vRoots, Gia_ObjId(p, pObj) ); - - // start order - vOrder = Vec_IntAlloc( Gia_ManObjNum(p) ); - Vec_IntPush( vOrder, -1 ); - - // start limits - vFraLims = Vec_IntAlloc( 1000 ); - Vec_IntPush( vFraLims, Vec_IntSize(vOrder) ); - - // collect new nodes - StopPoint = Vec_IntSize(vRoots); - Gia_ManForEachObjVec( vRoots, p, pObj, i ) - { - if ( i == StopPoint ) - { - Vec_IntPush( vFraLims, Vec_IntSize(vOrder) ); - StopPoint = Vec_IntSize(vRoots); - } - Gia_VtaCollect_rec( p, Gia_ObjFanin0(pObj), vOrder, vRoots ); - } - assert( i == StopPoint ); - Vec_IntPush( vFraLims, Vec_IntSize(vOrder) ); - -/* - // add unmarked PIs - Gia_ManForEachPi( p, pObj, i ) - if ( !pObj->fMark0 ) - Vec_IntPush( vOrder, Gia_ObjId(p, pObj) ); -*/ - - // clean/return - Gia_ManCleanMark0( p ); - if ( pvFraLims ) - *pvFraLims = vFraLims; - else - Vec_IntFree( vFraLims ); - if ( pvRoots ) - *pvRoots = vRoots; - else - Vec_IntFree( vRoots ); - return vOrder; -} /**Function************************************************************* @@ -378,6 +215,7 @@ Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_Int_t ** ***********************************************************************/ Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ) { +/* Vec_Int_t * vOrder, * vFraLims, * vRoots; Gia_Man_t * pCopy; int i, Entry; @@ -403,6 +241,8 @@ Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ) Vec_IntFree( vFraLims ); Vec_IntFree( vRoots ); return pCopy; +*/ + return NULL; } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3