diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-28 10:41:55 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-07-28 10:41:55 -0700 |
| commit | 1bb918167e2c2822eef8b1ea708bfb51ef70e6d1 (patch) | |
| tree | 4aa50672d60e16aa0f1fcc2e7bcbe8f3c35b5b66 | |
| parent | 9895f30d95f326211a397c75a8964ad5cfd12ad5 (diff) | |
| download | abc-1bb918167e2c2822eef8b1ea708bfb51ef70e6d1.tar.gz abc-1bb918167e2c2822eef8b1ea708bfb51ef70e6d1.tar.bz2 abc-1bb918167e2c2822eef8b1ea708bfb51ef70e6d1.zip | |
Serious bug fix in 'scorr -F <num>' with <num> > 1.
| -rw-r--r-- | src/aig/aig/aigDfs.c | 14 | ||||
| -rw-r--r-- | src/aig/aig/aigUtil.c | 29 | ||||
| -rw-r--r-- | src/proof/ssw/sswSweep.c | 3 |
3 files changed, 38 insertions, 8 deletions
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 8afec81e..d560fc29 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -199,6 +199,20 @@ void Aig_ManDfsAll_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes ) Aig_ManDfsAll_rec( p, Aig_ObjFanin1(pObj), vNodes ); Vec_PtrPush( vNodes, pObj ); } +Vec_Ptr_t * Aig_ManDfsArray( Aig_Man_t * p, Aig_Obj_t ** pNodes, int nNodes ) +{ + Vec_Ptr_t * vNodes; + int i; + Aig_ManIncrementTravId( p ); + vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) ); + // add constant + Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); + Vec_PtrPush( vNodes, Aig_ManConst1(p) ); + // collect nodes reachable in the DFS order + for ( i = 0; i < nNodes; i++ ) + Aig_ManDfsAll_rec( p, pNodes[i], vNodes ); + return vNodes; +} /**Function************************************************************* diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 6637e1a4..767015c9 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -653,23 +653,36 @@ void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, i void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig ) { assert( !Aig_IsComplement(pObj) ); - printf( "Node %p : ", pObj ); + printf( "Node %d : ", pObj->Id ); if ( Aig_ObjIsConst1(pObj) ) printf( "constant 1" ); else if ( Aig_ObjIsCi(pObj) ) - printf( "PI" ); + printf( "CI" ); else if ( Aig_ObjIsCo(pObj) ) { - printf( "PO" ); - printf( "%p%s", - Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " ") ); + printf( "CO( " ); + printf( "%d%s )", + Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") ); } else - printf( "AND( %p%s, %p%s )", - Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " "), - Aig_ObjFanin1(pObj), (Aig_ObjFaninC1(pObj)? "\'" : " ") ); + printf( "AND( %d%s, %d%s )", + Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " "), + Aig_ObjFanin1(pObj)->Id, (Aig_ObjFaninC1(pObj)? "\'" : " ") ); printf( " (refs = %3d)", Aig_ObjRefs(pObj) ); } +void Aig_ObjPrintVerboseCone( Aig_Man_t * p, Aig_Obj_t * pRoot, int fHaig ) +{ + extern Vec_Ptr_t * Aig_ManDfsArray( Aig_Man_t * p, Aig_Obj_t ** pNodes, int nNodes ); + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj; + int i; + vNodes = Aig_ManDfsArray( p, &pRoot, 1 ); + Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) + Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" ); + printf( "\n" ); + Vec_PtrFree( vNodes ); + +} /**Function************************************************************* diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c index 6db673cc..77cb24de 100644 --- a/src/proof/ssw/sswSweep.c +++ b/src/proof/ssw/sswSweep.c @@ -287,6 +287,9 @@ clk = Abc_Clock(); Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) ); + // sweep flops + Saig_ManForEachLo( p->pAig, pObj, i ) + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL ); // sweep internal nodes Aig_ManForEachNode( p->pAig, pObj, i ) { |