From dac71e9b3397eb545776f88e3a35f7343f0add00 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 29 Jul 2011 16:21:25 +0700 Subject: Added deriving abstraction in GIA from the precomputed flop map. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaAbs.c | 40 ++++-------------------- src/aig/gia/giaDup.c | 75 +++++++++++++++++++++++++++++++++++++++++++++ src/aig/saig/saig.h | 2 +- src/aig/saig/saigAbsStart.c | 6 ++-- src/aig/saig/saigDup.c | 44 +++++++++++++------------- src/base/abci/abc.c | 9 ++++-- 7 files changed, 115 insertions(+), 62 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; @@ -166,32 +166,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.] @@ -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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 93375fd8..d2ef8838 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -154,7 +154,7 @@ extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFr /*=== saigDup.c ==========================================================*/ extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p ); extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ); -extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); +extern Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ); extern int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p ); /*=== saigHaig.c ==========================================================*/ diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c index 6ec2c21d..13d11224 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/aig/saig/saigAbsStart.c @@ -204,7 +204,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo Vec_IntForEachEntryStart( vFlops, Entry, i, 1 ) assert( Vec_IntEntry(vFlops, i-1) != Entry ); - return Saig_ManDeriveAbstraction( p, vFlops ); + return Saig_ManDupAbstraction( p, vFlops ); } /**Function************************************************************* @@ -223,7 +223,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, Aig_Man_t * pAbs; Vec_Int_t * vFlopsNew; int i, Entry, clk = clock(); - pAbs = Saig_ManDeriveAbstraction( p, vFlops ); + pAbs = Saig_ManDupAbstraction( p, vFlops ); if ( fSensePath ) vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose ); else @@ -291,7 +291,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ) Vec_IntPush( vFlops, iFlop ); */ // create the resulting AIG - pAbs = Saig_ManDeriveAbstraction( p, vFlops ); + pAbs = Saig_ManDupAbstraction( p, vFlops ); if ( !pPars->fVerbose ) { printf( "Init : " ); diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index b2b33bdb..103cdf7b 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -127,26 +127,6 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ) return pAigNew; } -/**Function************************************************************* - - Synopsis [Duplicates the AIG manager recursively.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) -{ - if ( pObj->pData ) - return (Aig_Obj_t *)pObj->pData; - Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) ); - Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) ); - return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) )); -} - /**Function************************************************************* Synopsis [Trims the model by removing PIs without fanout.] @@ -191,6 +171,26 @@ Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates the AIG manager recursively.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) +{ + if ( pObj->pData ) + return (Aig_Obj_t *)pObj->pData; + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) ); + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) ); + return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) )); +} + /**Function************************************************************* Synopsis [Performs abstraction of the AIG to preserve the included flops.] @@ -202,14 +202,14 @@ Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) +Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) { Aig_Man_t * pNew;//, * pTemp; Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, Entry; Aig_ManCleanData( p ); // start the new manager - pNew = Aig_ManStart( Aig_ManNodeNum(p) ); + pNew = Aig_ManStart( 5000 ); pNew->pName = Aig_UtilStrsav( p->pName ); // map the constant node Aig_ManConst1(p)->pData = Aig_ManConst1( pNew ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 2492fb37..20c1e471 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27955,13 +27955,18 @@ int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "The network is combinational.\n" ); return 0; } - pTemp = Gia_ManCexAbstractionDerive( pAbc->pGia ); + if ( pAbc->pGia->vFlopClasses == NULL ) + { + Abc_Print( -1, "Abstraction flop map is missing.\n" ); + return 0; + } + pTemp = Gia_ManDupAbstraction( pAbc->pGia, pAbc->pGia->vFlopClasses ); Abc_CommandUpdate9( pAbc, pTemp ); return 0; usage: Abc_Print( -2, "usage: &abs_derive [-vh]\n" ); - Abc_Print( -2, "\t performs abstraction using the pre-computed flop map\n" ); + Abc_Print( -2, "\t derives abstracted model using the pre-computed flop map\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; -- cgit v1.2.3