diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-29 16:21:25 +0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-07-29 16:21:25 +0700 |
commit | dac71e9b3397eb545776f88e3a35f7343f0add00 (patch) | |
tree | 392a7605d23267e44eff68b887103381be894004 /src/aig/gia | |
parent | ce38474c74176b25bb244f7d17777517f0e9e6e4 (diff) | |
download | abc-dac71e9b3397eb545776f88e3a35f7343f0add00.tar.gz abc-dac71e9b3397eb545776f88e3a35f7343f0add00.tar.bz2 abc-dac71e9b3397eb545776f88e3a35f7343f0add00.zip |
Added deriving abstraction in GIA from the precomputed flop map.
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
-rw-r--r-- | src/aig/gia/giaAbs.c | 40 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 75 |
3 files changed, 82 insertions, 34 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 195abcc9..3beed711 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -656,6 +656,7 @@ extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, i extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); +extern Gia_Man_t * Gia_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses ); /*=== giaEnable.c ==========================================================*/ extern void Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose ); extern Gia_Man_t * Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose ); diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 7a4e51f4..2f7959a8 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -120,12 +120,12 @@ Vec_Int_t * Gia_ManClasses2Flops( Vec_Int_t * vFlopClasses ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManCexAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops ) +Gia_Man_t * Gia_ManDupAbstractionAig( Gia_Man_t * p, Vec_Int_t * vFlops ) { Gia_Man_t * pGia; Aig_Man_t * pNew, * pTemp; pNew = Gia_ManToAig( p, 0 ); - pNew = Saig_ManDeriveAbstraction( pTemp = pNew, vFlops ); + pNew = Saig_ManDupAbstraction( pTemp = pNew, vFlops ); Aig_ManStop( pTemp ); pGia = Gia_ManFromAig( pNew ); // pGia->vCiNumsOrig = pNew->vCiNumsOrig; @@ -168,32 +168,6 @@ void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) /**Function************************************************************* - Synopsis [Derives abstraction using the latch map.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia ) -{ - Vec_Int_t * vFlops; - Gia_Man_t * pAbs = NULL; - if ( pGia->vFlopClasses == NULL ) - { - printf( "Gia_ManCexAbstractionDerive(): Abstraction latch map is missing.\n" ); - return NULL; - } - vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); - pAbs = Gia_ManCexAbstraction( pGia, vFlops ); - Vec_IntFree( vFlops ); - return pAbs; -} - -/**Function************************************************************* - Synopsis [Refines abstraction using the latch map.] Description [] @@ -273,8 +247,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo return 0; } // derive abstraction - vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses ); - pAbs = Gia_ManCexAbstraction( pGia, vFlops ); + pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses ); // refine abstraction using PBA pAig = Gia_ManToAigSimple( pAbs ); Gia_ManStop( pAbs ); @@ -283,6 +256,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo // derive new classes if ( vFlopsNew != NULL ) { + vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew ); Vec_IntFree( pGia->vFlopClasses ); pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected ); @@ -292,7 +266,6 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbo Vec_IntFree( vFlops ); return 1; } - Vec_IntFree( vFlops ); // found counter-eample for the abstracted model // or exceeded conflict limit return 0; @@ -321,8 +294,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p ) pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) ); } // derive abstraction - vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses ); - pAbs = Gia_ManCexAbstraction( pGia, vFlops ); + pAbs = Gia_ManDupAbstraction( pGia, pGia->vFlopClasses ); // refine abstraction using PBA pAig = Gia_ManToAigSimple( pAbs ); Gia_ManStop( pAbs ); @@ -331,6 +303,7 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p ) // derive new classes if ( vFlopsNew != NULL ) { + vFlops = Gia_ManClasses2Flops( pGia->vFlopClasses ); // vSelected = Saig_ManFlopsSelect( vFlops, vFlopsNew ); vSelected = NULL; Vec_IntFree( pGia->vFlopClasses ); @@ -341,7 +314,6 @@ int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p ) Vec_IntFree( vFlops ); return 1; } - Vec_IntFree( vFlops ); // found counter-eample for the abstracted model // or exceeded conflict limit return 0; diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 0c9e2fb7..9942d37f 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1506,6 +1506,81 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupAbstraction_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return; + Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin1(pObj) ); + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Performs abstraction of the AIG to preserve the included flops.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupAbstraction( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, nFlops = 0; + Gia_ManFillValue( p ); + // start the new manager + pNew = Gia_ManStart( 5000 ); + pNew->pName = Gia_UtilStrsav( p->pName ); + // create PIs + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + // create additional PIs + Gia_ManForEachRo( p, pObj, i ) + if ( !Vec_IntEntry(vFlopClasses, i) ) + pObj->Value = Gia_ManAppendCi(pNew); + // create ROs + Gia_ManForEachRo( p, pObj, i ) + if ( Vec_IntEntry(vFlopClasses, i) ) + pObj->Value = Gia_ManAppendCi(pNew); + // create POs + Gia_ManHashAlloc( pNew ); + Gia_ManForEachPo( p, pObj, i ) + { + Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + // create RIs + Gia_ManForEachRi( p, pObj, i ) + if ( Vec_IntEntry(vFlopClasses, i) ) + { + Gia_ManDupAbstraction_rec( pNew, Gia_ObjFanin0(pObj) ); + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + nFlops++; + } + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, nFlops ); + // clean up + pNew = Gia_ManSeqCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |