diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-05-07 12:19:11 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-05-07 12:19:11 -0700 |
| commit | 4b21edde650c8098e4b1b62042bb3096577d39dd (patch) | |
| tree | b2f8e1c3e46ff05a079967a5947d0d6381bed603 /src/aig/saig | |
| parent | e2e3f6a2281b65632a139933cfc5021a84257a3a (diff) | |
| download | abc-4b21edde650c8098e4b1b62042bb3096577d39dd.tar.gz abc-4b21edde650c8098e4b1b62042bb3096577d39dd.tar.bz2 abc-4b21edde650c8098e4b1b62042bb3096577d39dd.zip | |
Improvements in sequential verification.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigMiter.c | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 4d775314..12a1486d 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -325,7 +325,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) Aig_Man_t * p, * pAig; Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, f; - assert( nFrames > 1 ); +// assert( nFrames > 1 ); assert( Saig_ManPiNum(pBot) == Saig_ManPiNum(pTop) ); assert( Saig_ManPoNum(pBot) == Saig_ManPoNum(pTop) ); assert( Saig_ManRegNum(pBot) == Saig_ManRegNum(pTop) ); @@ -347,16 +347,11 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) // add internal nodes of this frame Aig_ManForEachNode( pAig, pObj, i ) pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - if ( f == nFrames - 1 ) - { - // create POs for this frame - Aig_ManForEachPo( pAig, pObj, i ) - Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) ); - break; - } // create POs for this frame - Saig_ManForEachPo( pAig, pObj, i ) + Aig_ManForEachPo( pAig, pObj, i ) Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) ); + if ( f == nFrames - 1 ) + break; // save register inputs Saig_ManForEachLi( pAig, pObj, i ) pObj->pData = Aig_ObjChild0Copy(pObj); |