From f05986f7b393f570b486a0d7e5cb203e66dac1f8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 7 Apr 2016 15:54:50 -0700 Subject: Supporting edges in delay-optimization in &satlut. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaEdge.c | 152 +++++++++++++++++++++++++++++++++++++++++++++--- src/aig/gia/giaSatLut.c | 97 ++++++++++++++++++++++++++---- src/aig/gia/giaSweep.c | 1 + src/base/abci/abc.c | 5 ++ 5 files changed, 236 insertions(+), 20 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 8c282a51..6a1dc99e 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1447,6 +1447,7 @@ extern int Gia_ManBoxCoNum( Gia_Man_t * p ); extern int Gia_ManClockDomainNum( Gia_Man_t * p ); extern int Gia_ManIsSeqWithBoxes( Gia_Man_t * p ); extern int Gia_ManIsNormalized( Gia_Man_t * p ); +extern Vec_Int_t * Gia_ManOrderWithBoxes( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupUnnormalize( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupUnshuffleInputs( Gia_Man_t * p ); diff --git a/src/aig/gia/giaEdge.c b/src/aig/gia/giaEdge.c index f67f0b3c..f633c97c 100644 --- a/src/aig/gia/giaEdge.c +++ b/src/aig/gia/giaEdge.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "gia.h" +#include "misc/tim/tim.h" ABC_NAMESPACE_IMPL_START @@ -196,11 +197,77 @@ int Gia_ManEvalEdgeDelay( Gia_Man_t * p ) Vec_IntFreeP( &p->vEdgeDelay ); p->vEdgeDelay = Vec_IntStart( Gia_ManObjNum(p) ); if ( Gia_ManHasMapping(p) ) - Gia_ManForEachLut( p, iLut ) - Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) ); + { + if ( p->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pManTime) ) + { + Gia_Obj_t * pObj; + Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p ); + Tim_ManIncrementTravId( (Tim_Man_t*)p->pManTime ); + Gia_ManForEachObjVec( vNodes, p, pObj, k ) + { + iLut = Gia_ObjId( p, pObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjIsLut(p, iLut) ) + Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) ); + } + else if ( Gia_ObjIsCi(pObj) ) + { + int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj) ); + Vec_IntWriteEntry( p->vEdgeDelay, iLut, arrTime ); + } + else if ( Gia_ObjIsCo(pObj) ) + { + int arrTime = Vec_IntEntry( p->vEdgeDelay, Gia_ObjFaninId0(pObj, iLut) ); + Tim_ManSetCoArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj), arrTime ); + } + else if ( !Gia_ObjIsConst0(pObj) ) + assert( 0 ); + } + Vec_IntFree( vNodes ); + } + else + { + Gia_ManForEachLut( p, iLut ) + Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) ); + } + } else if ( Gia_ManHasMapping2(p) ) - Gia_ManForEachLut2( p, iLut ) - Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) ); + { + if ( p->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pManTime) ) + { + Gia_Obj_t * pObj; + Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p ); + Tim_ManIncrementTravId( (Tim_Man_t*)p->pManTime ); + Gia_ManForEachObjVec( vNodes, p, pObj, k ) + { + iLut = Gia_ObjId( p, pObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjIsLut2(p, iLut) ) + Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) ); + } + else if ( Gia_ObjIsCi(pObj) ) + { + int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj) ); + Vec_IntWriteEntry( p->vEdgeDelay, iLut, arrTime ); + } + else if ( Gia_ObjIsCo(pObj) ) + { + int arrTime = Vec_IntEntry( p->vEdgeDelay, Gia_ObjFaninId0(pObj, iLut) ); + Tim_ManSetCoArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj), arrTime ); + } + else if ( !Gia_ObjIsConst0(pObj) ) + assert( 0 ); + } + Vec_IntFree( vNodes ); + } + else + { + Gia_ManForEachLut2( p, iLut ) + Vec_IntWriteEntry( p->vEdgeDelay, iLut, Gia_ObjEvalEdgeDelay(p, iLut, p->vEdgeDelay) ); + } + } else assert( 0 ); Gia_ManForEachCoDriverId( p, iLut, k ) DelayMax = Abc_MaxInt( DelayMax, Vec_IntEntry(p->vEdgeDelay, iLut) ); @@ -310,11 +377,77 @@ int Gia_ManComputeEdgeDelay( Gia_Man_t * p ) p->vEdge2 = Vec_IntStart( Gia_ManObjNum(p) ); p->vEdgeDelay = Vec_IntStart( Gia_ManObjNum(p) ); if ( Gia_ManHasMapping(p) ) - Gia_ManForEachLut( p, iLut ) - Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 ); + { + if ( p->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pManTime) ) + { + Gia_Obj_t * pObj; + Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p ); + Tim_ManIncrementTravId( (Tim_Man_t*)p->pManTime ); + Gia_ManForEachObjVec( vNodes, p, pObj, k ) + { + iLut = Gia_ObjId( p, pObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjIsLut(p, iLut) ) + Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 ); + } + else if ( Gia_ObjIsCi(pObj) ) + { + int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj) ); + Vec_IntWriteEntry( p->vEdgeDelay, iLut, arrTime ); + } + else if ( Gia_ObjIsCo(pObj) ) + { + int arrTime = Vec_IntEntry( p->vEdgeDelay, Gia_ObjFaninId0(pObj, iLut) ); + Tim_ManSetCoArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj), arrTime ); + } + else if ( !Gia_ObjIsConst0(pObj) ) + assert( 0 ); + } + Vec_IntFree( vNodes ); + } + else + { + Gia_ManForEachLut( p, iLut ) + Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 ); + } + } else if ( Gia_ManHasMapping2(p) ) - Gia_ManForEachLut2( p, iLut ) - Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 ); + { + if ( p->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pManTime) ) + { + Gia_Obj_t * pObj; + Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p ); + Tim_ManIncrementTravId( (Tim_Man_t*)p->pManTime ); + Gia_ManForEachObjVec( vNodes, p, pObj, k ) + { + iLut = Gia_ObjId( p, pObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjIsLut2(p, iLut) ) + Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 ); + } + else if ( Gia_ObjIsCi(pObj) ) + { + int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj) ); + Vec_IntWriteEntry( p->vEdgeDelay, iLut, arrTime ); + } + else if ( Gia_ObjIsCo(pObj) ) + { + int arrTime = Vec_IntEntry( p->vEdgeDelay, Gia_ObjFaninId0(pObj, iLut) ); + Tim_ManSetCoArrival( (Tim_Man_t*)p->pManTime, Gia_ObjCioId(pObj), arrTime ); + } + else if ( !Gia_ObjIsConst0(pObj) ) + assert( 0 ); + } + Vec_IntFree( vNodes ); + } + else + { + Gia_ManForEachLut2( p, iLut ) + Gia_ObjComputeEdgeDelay( p, iLut, p->vEdgeDelay, p->vEdge1, p->vEdge2 ); + } + } else assert( 0 ); Gia_ManForEachCoDriverId( p, iLut, k ) DelayMax = Abc_MaxInt( DelayMax, Vec_IntEntry(p->vEdgeDelay, iLut) ); @@ -414,10 +547,11 @@ int Gia_ObjComputeEdgeDelay2( Gia_Man_t * p, int iObj, Vec_Int_t * vDelay, Vec_I } int Gia_ManComputeEdgeDelay2( Gia_Man_t * p ) { - int k, iLut, DelayMax = 0, EdgeCount = 0; + int k, iLut, DelayMax = 0; Vec_Int_t * vFanMax1 = Vec_IntStart( Gia_ManObjNum(p) ); Vec_Int_t * vFanMax2 = Vec_IntStart( Gia_ManObjNum(p) ); Vec_Int_t * vCountMax = Vec_IntStart( Gia_ManObjNum(p) ); + assert( p->pManTime == NULL ); Vec_IntFreeP( &p->vEdgeDelay ); Vec_IntFreeP( &p->vEdge1 ); Vec_IntFreeP( &p->vEdge2 ); diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index 9b905753..f314733d 100644 --- a/src/aig/gia/giaSatLut.c +++ b/src/aig/gia/giaSatLut.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "gia.h" +#include "misc/tim/tim.h" #include "sat/bsat/satStore.h" #include "misc/util/utilNam.h" #include "map/scl/sclCon.h" @@ -303,27 +304,101 @@ int Sbl_ManCreateTiming( Sbl_Man_t * p, int DelayStart ) int DelayMax = DelayStart, Delay, iLut, iFan, k; // compute arrival times Vec_IntFill( p->vArrs, Gia_ManObjNum(p->pGia), 0 ); - Gia_ManForEachLut2( p->pGia, iLut ) + if ( p->pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pGia->pManTime) ) { - vFanins = Gia_ObjLutFanins2(p->pGia, iLut); - Delay = Sbl_ManComputeDelay( p, iLut, vFanins ); - Vec_IntWriteEntry( p->vArrs, iLut, Delay ); - DelayMax = Abc_MaxInt( DelayMax, Delay ); + Gia_Obj_t * pObj; + Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p->pGia ); + Tim_ManIncrementTravId( (Tim_Man_t*)p->pGia->pManTime ); + Gia_ManForEachObjVec( vNodes, p->pGia, pObj, k ) + { + iLut = Gia_ObjId( p->pGia, pObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjIsLut2(p->pGia, iLut) ) + { + vFanins = Gia_ObjLutFanins2(p->pGia, iLut); + Delay = Sbl_ManComputeDelay( p, iLut, vFanins ); + Vec_IntWriteEntry( p->vArrs, iLut, Delay ); + DelayMax = Abc_MaxInt( DelayMax, Delay ); + } + } + else if ( Gia_ObjIsCi(pObj) ) + { + int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj) ); + Vec_IntWriteEntry( p->vArrs, iLut, arrTime ); + } + else if ( Gia_ObjIsCo(pObj) ) + { + int arrTime = Vec_IntEntry( p->vArrs, Gia_ObjFaninId0(pObj, iLut) ); + Tim_ManSetCoArrival( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj), arrTime ); + } + else if ( !Gia_ObjIsConst0(pObj) ) + assert( 0 ); + } + Vec_IntFree( vNodes ); + } + else + { + Gia_ManForEachLut2( p->pGia, iLut ) + { + vFanins = Gia_ObjLutFanins2(p->pGia, iLut); + Delay = Sbl_ManComputeDelay( p, iLut, vFanins ); + Vec_IntWriteEntry( p->vArrs, iLut, Delay ); + DelayMax = Abc_MaxInt( DelayMax, Delay ); + } } // compute required times Vec_IntFill( p->vReqs, Gia_ManObjNum(p->pGia), ABC_INFINITY ); Gia_ManForEachCoDriverId( p->pGia, iLut, k ) Vec_IntDowndateEntry( p->vReqs, iLut, DelayMax ); - Gia_ManForEachLut2Reverse( p->pGia, iLut ) + if ( p->pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)p->pGia->pManTime) ) { - Delay = Vec_IntEntry(p->vReqs, iLut) - 1; - vFanins = Gia_ObjLutFanins2(p->pGia, iLut); - Vec_IntForEachEntry( vFanins, iFan, k ) - Vec_IntDowndateEntry( p->vReqs, iFan, Delay ); + Gia_Obj_t * pObj; + Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( p->pGia ); + Tim_ManIncrementTravId( (Tim_Man_t*)p->pGia->pManTime ); + Tim_ManInitPoRequiredAll( (Tim_Man_t*)p->pGia->pManTime, DelayMax ); + Gia_ManForEachObjVecReverse( vNodes, p->pGia, pObj, k ) + { + iLut = Gia_ObjId( p->pGia, pObj ); + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjIsLut2(p->pGia, iLut) ) + { + Delay = Vec_IntEntry(p->vReqs, iLut) - 1; + vFanins = Gia_ObjLutFanins2(p->pGia, iLut); + Vec_IntForEachEntry( vFanins, iFan, k ) + Vec_IntDowndateEntry( p->vReqs, iFan, Delay ); + } + } + else if ( Gia_ObjIsCi(pObj) ) + { + int reqTime = Vec_IntEntry( p->vReqs, iLut ); + Tim_ManSetCiRequired( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj), reqTime ); + } + else if ( Gia_ObjIsCo(pObj) ) + { + int reqTime = Tim_ManGetCoRequired( (Tim_Man_t*)p->pGia->pManTime, Gia_ObjCioId(pObj) ); + Vec_IntWriteEntry( p->vReqs, Gia_ObjFaninId0(pObj, iLut), reqTime ); + } + else if ( !Gia_ObjIsConst0(pObj) ) + assert( 0 ); + } + Vec_IntFree( vNodes ); + } + else + { + Gia_ManForEachLut2Reverse( p->pGia, iLut ) + { + Delay = Vec_IntEntry(p->vReqs, iLut) - 1; + vFanins = Gia_ObjLutFanins2(p->pGia, iLut); + Vec_IntForEachEntry( vFanins, iFan, k ) + Vec_IntDowndateEntry( p->vReqs, iFan, Delay ); + } } return DelayMax; } + /**Function************************************************************* Synopsis [Given mapping in p->vSolCur, check if mapping meets delay.] @@ -379,7 +454,7 @@ int Sbl_ManEvaluateMapping( Sbl_Man_t * p, int DelayGlo ) { abctime clk = Abc_Clock(); Vec_Int_t * vFanins; - int i, iLut, iAnd, Delay, Required; + int i, iLut = -1, iAnd, Delay, Required; if ( p->pGia->vEdge1 ) return Sbl_ManEvaluateMappingEdge( p, DelayGlo ); Vec_IntClear( p->vPath ); diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c index 06e49f1f..4c2ced07 100644 --- a/src/aig/gia/giaSweep.c +++ b/src/aig/gia/giaSweep.c @@ -421,6 +421,7 @@ void Gia_ManCheckIntegrityWithBoxes( Gia_Man_t * p ) int i, nCountReg = 0, nCountCarry = 0; if ( p->pManTime == NULL ) return; + ABC_FREE( p->pRefs ); Gia_ManCreateRefs( p ); for ( i = Gia_ManPoNum(p) - Gia_ManRegBoxNum(p); i < Gia_ManPoNum(p); i++ ) { diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dd64a9da..407cadc9 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -34862,6 +34862,11 @@ int Abc_CommandAbc9Edge( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 0, "Current AIG has mapping into %d-LUTs.\n", Gia_ManLutSizeMax(pAbc->pGia) ); return 0; } + if ( pAbc->pGia->pManTime && fReverse ) + { + Abc_Print( 0, "Reverse computation does not work when boxes are present.\n" ); + return 0; + } if ( fReverse ) DelayMax = Gia_ManComputeEdgeDelay2( pAbc->pGia ); else -- cgit v1.2.3