diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-03-09 19:59:35 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-03-09 19:59:35 -0800 |
| commit | fec988f6194fbab17cc18b72e6f907d5f990bbe8 (patch) | |
| tree | 0adf99e304f984f32201e3853fa2109ed5405e86 /src/proof/live | |
| parent | c46c957a0721004eb21c5f3d3f316ba1c8ab8df1 (diff) | |
| download | abc-fec988f6194fbab17cc18b72e6f907d5f990bbe8.tar.gz abc-fec988f6194fbab17cc18b72e6f907d5f990bbe8.tar.bz2 abc-fec988f6194fbab17cc18b72e6f907d5f990bbe8.zip | |
Renamed Aig_ObjPioNum to be Aig_ObjCioId.
Diffstat (limited to 'src/proof/live')
| -rw-r--r-- | src/proof/live/liveness.c | 6 | ||||
| -rw-r--r-- | src/proof/live/liveness_sim.c | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/proof/live/liveness.c b/src/proof/live/liveness.c index e457b3f8..654e1d68 100644 --- a/src/proof/live/liveness.c +++ b/src/proof/live/liveness.c @@ -527,7 +527,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); } @@ -830,7 +830,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch ); } @@ -2256,7 +2256,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); //assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); } diff --git a/src/proof/live/liveness_sim.c b/src/proof/live/liveness_sim.c index b99df807..f1ad794a 100644 --- a/src/proof/live/liveness_sim.c +++ b/src/proof/live/liveness_sim.c @@ -466,7 +466,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ assert( Aig_ManCheck( pNew ) ); #ifndef DUPLICATE_CKT_DEBUG - assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPoNum( pNew ) == 1 ); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); |