diff options
author | Mathias Soeken <mathias.soeken@gmail.com> | 2017-02-22 19:00:28 -0800 |
---|---|---|
committer | Mathias Soeken <mathias.soeken@gmail.com> | 2017-02-22 19:00:28 -0800 |
commit | 28e8e7f3e79d1391a2f3a31cefe3afe234aa3b8e (patch) | |
tree | 6b7962dc72653e3bf615c5901854774eca9d23c8 /src/proof/pdr/pdrTsim.c | |
parent | 5af44731bff0061c724912cf76e86dddbb4f2c7a (diff) | |
parent | dd8cc7e9a27e2bd962d612911c6fd9508c6c1e0d (diff) | |
download | abc-28e8e7f3e79d1391a2f3a31cefe3afe234aa3b8e.tar.gz abc-28e8e7f3e79d1391a2f3a31cefe3afe234aa3b8e.tar.bz2 abc-28e8e7f3e79d1391a2f3a31cefe3afe234aa3b8e.zip |
Merged alanmi/abc into default
Diffstat (limited to 'src/proof/pdr/pdrTsim.c')
-rw-r--r-- | src/proof/pdr/pdrTsim.c | 134 |
1 files changed, 74 insertions, 60 deletions
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 32d1c857..acbf70f5 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -364,7 +364,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) Vec_Int_t * vRes = p->vRes; // final result (flop literals) Aig_Obj_t * pObj; int i, Entry, RetValue; - abctime clk = Abc_Clock(); + //abctime clk = Abc_Clock(); // collect CO objects Vec_IntClear( vCoObjs ); @@ -404,67 +404,65 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL ); assert( RetValue ); -#if 1 - // try removing high-priority flops - Vec_IntClear( vCi2Rem ); - Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + // iteratively remove flops + if ( p->pPars->fFlopPrio ) { - if ( !Saig_ObjIsLo( p->pAig, pObj ) ) - continue; - Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) - continue; - Vec_IntClear( vUndo ); - if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) - Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); - else - Pdr_ManExtendUndo( p->pAig, vUndo ); - } - // try removing low-priority flops - Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) - { - if ( !Saig_ObjIsLo( p->pAig, pObj ) ) - continue; - Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) - continue; - Vec_IntClear( vUndo ); - if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) - Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); - else - Pdr_ManExtendUndo( p->pAig, vUndo ); - } -#else - // try removing low-priority flops - Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) - { - if ( !Saig_ObjIsLo( p->pAig, pObj ) ) - continue; - Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) - continue; - Vec_IntClear( vUndo ); - if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) - Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); - else - Pdr_ManExtendUndo( p->pAig, vUndo ); + // collect flops and sort them by priority + Vec_IntClear( vRes ); + Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + { + if ( !Saig_ObjIsLo( p->pAig, pObj ) ) + continue; + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); + Vec_IntPush( vRes, Entry ); + } + Vec_IntSelectSortCost( Vec_IntArray(vRes), Vec_IntSize(vRes), vPrio ); + + // try removing flops starting from low-priority to high-priority + Vec_IntClear( vCi2Rem ); + Vec_IntForEachEntry( vRes, Entry, i ) + { + pObj = Aig_ManCi( p->pAig, Saig_ManPiNum(p->pAig) + Entry ); + assert( Saig_ObjIsLo( p->pAig, pObj ) ); + Vec_IntClear( vUndo ); + if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) + Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); + else + Pdr_ManExtendUndo( p->pAig, vUndo ); + } } - // try removing high-priority flops - Vec_IntClear( vCi2Rem ); - Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + else { - if ( !Saig_ObjIsLo( p->pAig, pObj ) ) - continue; - Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); - if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) - continue; - Vec_IntClear( vUndo ); - if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) - Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); - else - Pdr_ManExtendUndo( p->pAig, vUndo ); + // try removing low-priority flops first + Vec_IntClear( vCi2Rem ); + Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + { + if ( !Saig_ObjIsLo( p->pAig, pObj ) ) + continue; + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); + if ( Vec_IntEntry(vPrio, Entry) ) + continue; + Vec_IntClear( vUndo ); + if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) + Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); + else + Pdr_ManExtendUndo( p->pAig, vUndo ); + } + // try removing high-priority flops next + Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i ) + { + if ( !Saig_ObjIsLo( p->pAig, pObj ) ) + continue; + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); + if ( !Vec_IntEntry(vPrio, Entry) ) + continue; + Vec_IntClear( vUndo ); + if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) ) + Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) ); + else + Pdr_ManExtendUndo( p->pAig, vUndo ); + } } -#endif if ( p->pPars->fVeryVerbose ) Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); @@ -474,9 +472,25 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem ); // derive the set of resulting registers Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits ); assert( Vec_IntSize(vRes) > 0 ); - p->tTsim += Abc_Clock() - clk; + //p->tTsim += Abc_Clock() - clk; + + // move abstracted literals from flops to inputs + if ( p->pPars->fUseAbs && p->vAbsFlops ) + { + int i, iLit, k = 0; + Vec_IntForEachEntry( vRes, iLit, i ) + { + if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop + Vec_IntWriteEntry( vRes, k++, iLit ); + else + Vec_IntPush( vPiLits, 2*Saig_ManPiNum(p->pAig) + iLit ); + } + Vec_IntShrink( vRes, k ); + } pRes = Pdr_SetCreate( vRes, vPiLits ); - assert( k == 0 || !Pdr_SetIsInit(pRes, -1) ); + //ZH: Disabled assertion because this invariant doesn't hold with down + //because of the join operation which can bring in initial states + //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) ); return pRes; } |