diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-06 23:13:52 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-06 23:13:52 -0800 |
| commit | 9382c8fdd1feb4f69ab6d2e99dfc43658b14079d (patch) | |
| tree | 9b10fa1677367e9c1941e0f63f63df3dc63b0ab0 /src/aig/saig | |
| parent | 6a939b63828da5204387f681a451829aa35171f1 (diff) | |
| download | abc-9382c8fdd1feb4f69ab6d2e99dfc43658b14079d.tar.gz abc-9382c8fdd1feb4f69ab6d2e99dfc43658b14079d.tar.bz2 abc-9382c8fdd1feb4f69ab6d2e99dfc43658b14079d.zip | |
Trying to add BMC to random simulation.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saig.h | 1 | ||||
| -rw-r--r-- | src/aig/saig/saigDup.c | 44 |
2 files changed, 45 insertions, 0 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 6b85a3df..96fdde5e 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -168,6 +168,7 @@ extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * 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 ); +extern Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit ); /*=== saigHaig.c ==========================================================*/ extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose ); /*=== saigInd.c ==========================================================*/ diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index fce6cf42..7a0b990f 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -350,6 +350,50 @@ int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p ) return RetValue; } +/**Function************************************************************* + + Synopsis [Duplicates while ORing the POs of sequential circuit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit ) +{ + Aig_Man_t * pAigNew; + Aig_Obj_t * pObj; + int i; + assert( Aig_ManRegNum(pAig) <= Vec_IntSize(vInit) ); + // start the new manager + pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); + pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->nConstrs = pAig->nConstrs; + // map the constant node + Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); + // create variables for PIs + Aig_ManForEachPi( pAig, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pAigNew ); + // update the flop variables + Saig_ManForEachLo( pAig, pObj, i ) + pObj->pData = Aig_NotCond( pObj->pData, Vec_IntEntry(vInit, i) ); + // add internal nodes of this frame + Aig_ManForEachNode( pAig, pObj, i ) + pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // transfer to register outputs + Saig_ManForEachPo( pAig, pObj, i ) + Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) ); + // update the flop variables + Saig_ManForEachLi( pAig, pObj, i ) + Aig_ObjCreatePo( pAigNew, Aig_NotCond(Aig_ObjChild0Copy(pObj), Vec_IntEntry(vInit, i)) ); + // finalize + Aig_ManCleanup( pAigNew ); + Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) ); + return pAigNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |