diff options
| -rw-r--r-- | src/base/wlc/wlc.h | 1 | ||||
| -rw-r--r-- | src/base/wlc/wlcCom.c | 11 | ||||
| -rw-r--r-- | src/base/wlc/wlcMem.c | 391 | ||||
| -rw-r--r-- | src/base/wlc/wlcNtk.c | 35 |
4 files changed, 284 insertions, 154 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 5498d9da..ca6b836a 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -395,6 +395,7 @@ extern void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ); extern void Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray ); extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type ); extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose ); +extern void Wlc_NtkPrintObjects( Wlc_Ntk_t * p ); extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ); extern char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq ); extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq ); diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index b8853dda..3fbe1ba8 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -309,9 +309,10 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) int fShowMem = 0; int fDistrib = 0; int fTwoSides = 0; + int fAllObjects = 0; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cmardtvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cmardtovh" ) ) != EOF ) { switch ( c ) { @@ -333,6 +334,9 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': fTwoSides ^= 1; break; + case 'o': + fAllObjects ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -356,9 +360,11 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_ADD ); if ( fShowMem ) Wlc_NtkPrintMemory( pNtk ); + if ( fAllObjects ) + Wlc_NtkPrintObjects( pNtk ); return 0; usage: - Abc_Print( -2, "usage: %%ps [-cmardtvh]\n" ); + Abc_Print( -2, "usage: %%ps [-cmardtovh]\n" ); Abc_Print( -2, "\t prints statistics\n" ); Abc_Print( -2, "\t-c : toggle printing cones [default = %s]\n", fShowCones? "yes": "no" ); Abc_Print( -2, "\t-m : toggle printing multipliers [default = %s]\n", fShowMulti? "yes": "no" ); @@ -366,6 +372,7 @@ usage: Abc_Print( -2, "\t-r : toggle printing memories [default = %s]\n", fShowMem? "yes": "no" ); Abc_Print( -2, "\t-d : toggle printing distrubition [default = %s]\n", fDistrib? "yes": "no" ); Abc_Print( -2, "\t-t : toggle printing stats for LHS and RHS [default = %s]\n", fTwoSides? "yes": "no" ); + Abc_Print( -2, "\t-o : toggle printing all objects [default = %s]\n", fAllObjects?"yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c index 52cb2e2d..328484bd 100644 --- a/src/base/wlc/wlcMem.c +++ b/src/base/wlc/wlcMem.c @@ -75,7 +75,7 @@ Vec_Int_t * Wlc_NtkCollectMemory( Wlc_Ntk_t * p ) void Wlc_NtkPrintMemory( Wlc_Ntk_t * p ) { Vec_Int_t * vMemory; - vMemory = Wlc_NtkCollectMemSizes( p ); + vMemory = Wlc_NtkCollectMemory( p ); Vec_IntSort( vMemory, 0 ); Wlc_NtkPrintNodeArray( p, vMemory ); Vec_IntFree( vMemory ); @@ -130,15 +130,20 @@ int Wlc_CountDcs( char * pInit ) } int Wlc_NtkDupOneObject( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int TypeNew, Vec_Int_t * vFanins ) { + int iObj = Wlc_ObjId(p, pObj); unsigned Type = pObj->Type; int iObjNew, nFanins = Wlc_ObjFaninNum(pObj); + int iObjCopy = Wlc_ObjCopy(p, iObj); pObj->Type = TypeNew; pObj->nFanins = 0; - iObjNew = Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins ); + iObjNew = Wlc_ObjDup( pNew, p, iObj, vFanins ); pObj->Type = Type; pObj->nFanins = (unsigned)nFanins; if ( TypeNew == WLC_OBJ_FO ) + { Vec_IntPush( pNew->vInits, -Wlc_ObjRange(pObj) ); + Wlc_ObjSetCopy( p, iObj, iObjCopy ); + } return iObjNew; } void Wlc_NtkDupOneBuffer( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins, int fIsFi ) @@ -164,8 +169,8 @@ Vec_Int_t * Wlc_NtkAbsCreateFlopOutputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_In int i, Entry, iObj, iFrame; Vec_IntForEachEntry( vNodeFrames, Entry, i ) { - iObj = Entry >> 10; - iFrame = Entry & 0x3FF; + iObj = Entry >> 11; + iFrame = (Entry >> 1) & 0x3FF; pObj = Wlc_NtkObj( p, iObj ); // address if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX ) @@ -184,23 +189,78 @@ Vec_Int_t * Wlc_NtkAbsCreateFlopOutputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_In else assert( 0 ); Vec_IntPush( vNewObjs, pFanin ? Wlc_NtkDupOneObject(pNew, p, pFanin, WLC_OBJ_FO, vFanins) : 0 ); } - assert( Vec_IntSize(vNewObjs) == Vec_IntCap(vNewObjs) ); + assert( Vec_IntSize(vNewObjs) == 2 * Vec_IntSize(vNodeFrames) ); return vNewObjs; } -Wlc_Obj_t * Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins, Vec_Int_t * vNewObjs, Vec_Wec_t * vConstrs ) +void Wlc_NtkAbsCreateFlopInputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins, Vec_Int_t * vNewObjs, Wlc_Obj_t * pCounter, int AdderBits ) { - Vec_Int_t * vLevel; + Wlc_Obj_t * pObj, * pFanin, * pFlop, * pCond, * pMux, * pConst; + int i, n, Entry, Value, iObj, iFrame; + Vec_IntForEachEntry( vNodeFrames, Entry, i ) + { + Value = Entry & 1; + iObj = Entry >> 11; + iFrame = (Entry >> 1) & 0x3FF; + pObj = Wlc_NtkObj( p, iObj ); + for ( n = 0; n < 2; n++ ) // n=0 -- address n=1 -- data + { + pFlop = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*i+n) ); + if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE ) + pFanin = Wlc_ObjCopyObj( pNew, p, n ? Wlc_ObjFanin2(p, pObj) : Wlc_ObjFanin1(p, pObj) ); + else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ ) + pFanin = n ? Wlc_NtkObj(pNew, Wlc_ObjCopy(p, iObj)) : Wlc_ObjCopyObj( pNew, p, Wlc_ObjFanin1(p, pObj) ); + else if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX ) + { + if ( n ) continue; + pFanin = Wlc_ObjCopyObj( pNew, p, Wlc_ObjFanin0(p, pObj) ); + if ( Value ) + { + Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pFanin) ); + pFanin = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_NOT, 0, 0, 0)); + Wlc_ObjAddFanins( pNew, pFanin, vFanins ); + } + } + else assert( 0 ); + assert( Wlc_ObjRange(pFlop) == Wlc_ObjRange(pFanin) ); + // create constant + pConst = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, AdderBits-1, 0)); + Vec_IntFill( vFanins, 1, iFrame ); + Wlc_ObjAddFanins( pNew, pConst, vFanins ); + // create equality + pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0)); + Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pConst), Wlc_ObjId(pNew, pCounter) ); + Wlc_ObjAddFanins( pNew, pCond, vFanins ); + // create MUX + pMux = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pFlop)-1, 0)); + Vec_IntClear( vFanins ); + Vec_IntPush( vFanins, Wlc_ObjId(pNew, pCond) ); + Vec_IntPush( vFanins, Wlc_ObjId(pNew, pFlop) ); + Vec_IntPush( vFanins, Wlc_ObjId(pNew, pFanin) ); + Wlc_ObjAddFanins( pNew, pMux, vFanins ); + Wlc_ObjSetCo( pNew, pMux, 1 ); + } + } +} +void Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins, Vec_Int_t * vNewObjs, Vec_Wec_t * vConstrs, Wlc_Obj_t * pConstrOut ) +{ + Vec_Int_t * vTrace; Vec_Int_t * vBitConstr = Vec_IntAlloc( 100 ); Vec_Int_t * vLevConstr = Vec_IntAlloc( 100 ); Wlc_Obj_t * pAddrs[2], * pDatas[2], * pCond, * pConstr = NULL; - int i, k, Entry, Index[2]; - Vec_WecForEachLevel( vConstrs, vLevel, i ) + int i, k, Entry, Index[2], iFrameLast, iFrameThis; + assert( Vec_IntSize(vNewObjs) == 2 * Vec_IntSize(vNodeFrames) ); + Vec_WecForEachLevel( vConstrs, vTrace, i ) { - assert( Vec_IntSize(vLevel) >= 2 ); + if ( Vec_IntSize(vTrace) == 0 ) + continue; + assert( Vec_IntSize(vTrace) >= 2 ); Vec_IntClear( vLevConstr ); - Index[0] = Vec_IntFind( vNodeFrames, Vec_IntEntry(vLevel, 0) ); - Index[1] = Vec_IntFind( vNodeFrames, Vec_IntEntryLast(vLevel) ); + iFrameThis = (Vec_IntEntry(vTrace, 0) >> 1) & 0x3FF; + iFrameLast = (Vec_IntEntryLast(vTrace) >> 1) & 0x3FF; + + Index[0] = Vec_IntFind( vNodeFrames, Vec_IntEntry(vTrace, 0) ); + Index[1] = Vec_IntFind( vNodeFrames, Vec_IntEntryLast(vTrace) ); assert( Index[0] >= 0 && Index[1] >= 0 ); pAddrs[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]) ); @@ -209,6 +269,17 @@ Wlc_Obj_t * Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * pDatas[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]+1) ); pDatas[1] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[1]+1) ); + // redirect the source in the last time frame to point to FOs + if ( iFrameThis == iFrameLast ) + { + pAddrs[0] = Wlc_ObjFo2Fi(pNew, pAddrs[0]); + pDatas[0] = Wlc_ObjFo2Fi(pNew, pDatas[0]); + } + + // redirect the sink in the last time frame to point to FOs + pAddrs[1] = Wlc_ObjFo2Fi(pNew, pAddrs[1]); + pDatas[1] = Wlc_ObjFo2Fi(pNew, pDatas[1]); + // equal addresses pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0)); Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pAddrs[0]), Wlc_ObjId(pNew, pAddrs[1]) ); @@ -221,12 +292,20 @@ Wlc_Obj_t * Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * Wlc_ObjAddFanins( pNew, pCond, vFanins ); Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) ); - Vec_IntForEachEntryStartStop( vLevel, Entry, k, 0, Vec_IntSize(vLevel)-1 ) + Vec_IntForEachEntryStartStop( vTrace, Entry, k, 1, Vec_IntSize(vTrace)-1 ) { - Index[0] = Vec_IntFind( vNodeFrames, Entry ); - pAddrs[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]) ); + iFrameThis = (Entry >> 1) & 0x3FF; + Index[0] = Vec_IntFind( vNodeFrames, Entry ); + assert( Index[0] >= 0 ); + pAddrs[0] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[0]) ); + // redirect the middle in the last time frame to point to FOs + if ( iFrameThis == iFrameLast ) + pAddrs[0] = Wlc_ObjFo2Fi(pNew, pAddrs[0]); if ( Vec_IntEntry(vNewObjs, 2*Index[0]+1) == 0 ) // MUX + { + assert( Wlc_ObjType(Wlc_NtkObj(p, Entry >> 11)) == WLC_OBJ_MUX ); Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pAddrs[0]) ); + } else // different addresses { assert( Wlc_ObjRange(pAddrs[0]) == Wlc_ObjRange(pAddrs[1]) ); @@ -266,64 +345,17 @@ Wlc_Obj_t * Wlc_NtkAbsCreateLogic( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * // cleanup Vec_IntFree( vBitConstr ); Vec_IntFree( vLevConstr ); - return pConstr; -} -void Wlc_NtkAbsCreateFlopInputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins, Vec_Int_t * vNewObjs, Wlc_Obj_t * pCounter, int AdderBits, Vec_Bit_t * vMuxVal ) -{ - Wlc_Obj_t * pObj, * pFanin, * pFlop, * pCond, * pMux, * pConst; - int i, n, Entry, iObj, iFrame, Index; - Vec_IntForEachEntry( vNodeFrames, Entry, i ) - { - iObj = Entry >> 10; - iFrame = Entry & 0x3FF; - pObj = Wlc_NtkObj( p, iObj ); - Index = Vec_IntFind( vNodeFrames, Entry ); - for ( n = 0; n < 2; n++ ) // n=0 -- address n=1 -- data - { - pFlop = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index+n) ); - if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE ) - pFanin = Wlc_ObjCopyObj( pNew, p, n ? Wlc_ObjFanin2(pNew, pObj) : Wlc_ObjFanin1(pNew, pObj) ); - else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ ) - pFanin = n ? Wlc_NtkObj(pNew, Wlc_ObjCopy(p, iObj)) : Wlc_ObjCopyObj( pNew, p, Wlc_ObjFanin1(pNew, pObj) ); - else if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX ) - { - if ( n ) continue; - pFanin = Wlc_ObjCopyObj( pNew, p, Wlc_ObjFanin0(p, pObj) ); - if ( Vec_BitEntry( vMuxVal, iFrame * Wlc_NtkObjNum(p) + iObj ) ) - { - Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pFanin) ); - pFanin = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_NOT, 0, 0, 0)); - Wlc_ObjAddFanins( pNew, pFanin, vFanins ); - } - } - else assert( 0 ); - assert( Wlc_ObjRange(pFlop) == Wlc_ObjRange(pFanin) ); - // create constant - pConst = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, AdderBits-1, 0)); - Vec_IntFill( vFanins, 1, iFrame ); - Wlc_ObjAddFanins( pNew, pConst, vFanins ); - // create equality - pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0)); - Vec_IntFillTwo( vFanins, 1, Wlc_ObjId(pNew, pConst), Wlc_ObjId(pNew, pCounter) ); - Wlc_ObjAddFanins( pNew, pCond, vFanins ); - // create MUX - pMux = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pFlop)-1, 0)); - Vec_IntClear( vFanins ); - Vec_IntPush( vFanins, Wlc_ObjId(pNew, pCond) ); - Vec_IntPush( vFanins, Wlc_ObjId(pNew, pFlop) ); - Vec_IntPush( vFanins, Wlc_ObjId(pNew, pFanin) ); - Wlc_ObjAddFanins( pNew, pMux, vFanins ); - Wlc_ObjSetCo( pNew, pMux, 1 ); - } - } + // add the constraint as fanin to the output + Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pConstr) ); + Wlc_ObjAddFanins( pNew, pConstrOut, vFanins ); } -Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_t * vMemFanins, int * piFirstMemPi, int * piFirstCi, int * piFirstMemCi, Vec_Wec_t * vConstrs, Vec_Int_t * vNodeFrames, Vec_Bit_t * vMuxVal ) +Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_t * vMemFanins, int * piFirstMemPi, int * piFirstCi, int * piFirstMemCi, Vec_Wec_t * vConstrs, Vec_Int_t * vNodeFrames ) { - Wlc_Ntk_t * pNew; + Wlc_Ntk_t * pNew, * pTemp; Wlc_Obj_t * pObj, * pCounter, * pConst, * pAdder, * pConstr = NULL; Vec_Int_t * vNewObjs = NULL; Vec_Int_t * vFanins = Vec_IntAlloc( 100 ); - int i, Po0, Po1, AdderBits = 20, nBits = 0; + int i, Po0, Po1, AdderBits = 4, nBits = 0; // mark memory nodes Wlc_NtkCleanMarks( p ); @@ -349,7 +381,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_ Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i ) if ( Wlc_ObjType(pObj) == WLC_OBJ_READ ) { - int iObjNew = Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins ); + Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins ); nBits += Wlc_ObjRange(pObj); } @@ -383,10 +415,6 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_ if ( !Wlc_ObjIsCi(pObj) && !pObj->Mark ) Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins ); - // create logic nodes for constraints - if ( vConstrs ) - pConstr = Wlc_NtkAbsCreateLogic( pNew, p, vNodeFrames, vFanins, vNewObjs, vConstrs ); - if ( Vec_IntSize(&p->vPoPairs) ) { // create miter for the PO pairs @@ -407,7 +435,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_ // create constraint output if ( vConstrs ) - Wlc_ObjSetCo( pNew, pConstr, 0 ); + Wlc_ObjSetCo( pNew, (pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BUF, 0, 0, 0))), 0 ); } else { @@ -416,8 +444,8 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_ if ( !pObj->Mark ) Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi ); // create constraint output - if ( pConstr ) - Wlc_ObjSetCo( pNew, pConstr, 0 ); + if ( vConstrs ) + Wlc_ObjSetCo( pNew, (pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BUF, 0, 0, 0))), 0 ); // duplicate FIs Wlc_NtkForEachCo( p, pObj, i ) if ( !Wlc_ObjIsPo(pObj) && !pObj->Mark ) @@ -441,7 +469,11 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_ // create flop inputs for constraint objects if ( vConstrs ) - Wlc_NtkAbsCreateFlopInputs( pNew, p, vNodeFrames, vFanins, vNewObjs, pCounter, AdderBits, vMuxVal ); + Wlc_NtkAbsCreateFlopInputs( pNew, p, vNodeFrames, vFanins, vNewObjs, pCounter, AdderBits ); + + // create constraint logic nodes + if ( vConstrs ) + Wlc_NtkAbsCreateLogic( pNew, p, vNodeFrames, vFanins, vNewObjs, vConstrs, pConstr ); // append init states pNew->pInits = Wlc_PrsConvertInitValues( pNew ); @@ -451,6 +483,9 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_ Vec_IntFree( vFanins ); Vec_IntFreeP( &vNewObjs ); Wlc_NtkCleanMarks( p ); + // derive topological order + pNew = Wlc_NtkDupDfs( pTemp = pNew, 0, 1 ); + Wlc_NtkFree( pTemp ); return pNew; } @@ -465,7 +500,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractMemory( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_ SeeAlso [] ***********************************************************************/ -Vec_Int_t * Wlc_NtkDeriveFirstTotal( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_t * vMemFanins, int iFirstMemPi, int iFirstMemCi ) +Vec_Int_t * Wlc_NtkDeriveFirstTotal( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Int_t * vMemFanins, int iFirstMemPi, int iFirstMemCi, int fVerbose ) { Vec_Int_t * vFirstTotal = Vec_IntStart( 3 * Vec_IntSize(vMemObjs) ); // contains pairs of (first CO bit: range) for each input/output of a node Wlc_Obj_t * pObj, * pFanin; int i, k, iFanin, nMemFanins = 0; @@ -499,15 +534,19 @@ Vec_Int_t * Wlc_NtkDeriveFirstTotal( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_In } } assert( nMemFanins == Vec_IntSize(vMemFanins) ); -// Vec_IntForEachEntry( vFirstTotal, iFanin, i ) -// printf( "%16s : %d(%d)\n", Wlc_ObjName(p, Vec_IntEntry(vMemObjs, i/3)), iFanin >> 10, iFanin & 0x3FF ); + if ( fVerbose ) + Vec_IntForEachEntry( vFirstTotal, iFanin, i ) + { + printf( "Obj %5d Fanin %5d : ", i/3, i%3 ); + printf( "%16s : %d(%d)\n", Wlc_ObjName(p, Vec_IntEntry(vMemObjs, i/3)), iFanin >> 10, iFanin & 0x3FF ); + } return vFirstTotal; } int Wlc_NtkCexResim( Gia_Man_t * pAbs, Abc_Cex_t * p, Vec_Int_t * vFirstTotal, int iBit, Vec_Wrd_t * vRes, int iFrame ) { Gia_Obj_t * pObj, * pObjRi, * pObjRo; int k, b, Entry, First, nBits; word Value; - // assuming that flop inputs have been assigned from previous timeframe + // assuming that flop outputs have been assigned in the previous timeframe // assign primary inputs Gia_ManForEachPi( pAbs, pObj, k ) pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); @@ -527,7 +566,7 @@ int Wlc_NtkCexResim( Gia_Man_t * pAbs, Abc_Cex_t * p, Vec_Int_t * vFirstTotal, i { if ( Entry == 0 ) { - Vec_WrdPush( vRes, ~(word)0 ); + Vec_WrdWriteEntry( vRes, Vec_IntSize(vFirstTotal)*iFrame + k, ~(word)0 ); continue; } First = Entry >> 10; @@ -542,19 +581,28 @@ int Wlc_NtkCexResim( Gia_Man_t * pAbs, Abc_Cex_t * p, Vec_Int_t * vFirstTotal, i } return iBit; } -Vec_Wrd_t * Wlc_NtkConvertCex( Wlc_Ntk_t * p, Vec_Int_t * vFirstTotal, Gia_Man_t * pAbs, Abc_Cex_t * pCex ) +Vec_Wrd_t * Wlc_NtkConvertCex( Vec_Int_t * vFirstTotal, Gia_Man_t * pAbs, Abc_Cex_t * pCex, int fVerbose ) { Vec_Wrd_t * vValues = Vec_WrdStartFull( Vec_IntSize(vFirstTotal) * (pCex->iFrame + 1) ); - int f, nBits = pCex->nRegs; + int k, f, nBits = pCex->nRegs; word Value; Gia_ManCleanMark0(pAbs); // init FOs to zero for ( f = 0; f <= pCex->iFrame; f++ ) nBits = Wlc_NtkCexResim( pAbs, pCex, vFirstTotal, nBits, vValues, f ); + if ( fVerbose ) + Vec_WrdForEachEntry( vValues, Value, k ) + { + if ( k % Vec_IntSize(vFirstTotal) == 0 ) + printf( "Frame %d:\n", k/Vec_IntSize(vFirstTotal) ); + printf( "Obj %5d Fanin %5d : ", k/3, k%3 ); + Extra_PrintBinary( stdout, (unsigned *)&Value, 32 ); + printf( "\n" ); + } return vValues; } /**Function************************************************************* - Synopsis [Derives refinement.] + Synopsis [Derives the reason for failure in terms of memory values.] Description [] @@ -570,46 +618,54 @@ void Wlc_NtkTrace_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFrame, Vec_Int_t * assert( iObj == Vec_IntEntry(vMemObjs, iNum) ); assert( iFrame >= 0 ); if ( Wlc_ObjIsPi(pObj) ) - Vec_IntPush( vRes, (iObj << 10) | iFrame ); - else if ( Wlc_ObjIsCo(pObj) ) + Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) ); + else if ( Wlc_ObjIsCi(pObj) && iFrame == 0 ) + { + int PiId = Vec_IntEntry(p->vInits, Wlc_ObjCiId(pObj)-Wlc_NtkPiNum(p) ); + int iPiObj = Wlc_ObjId( p, Wlc_NtkPi(p, PiId) ); + Vec_IntPush( vRes, (iPiObj << 11) | (iFrame << 1) ); + } + else if ( Wlc_ObjIsCi(pObj) ) Wlc_NtkTrace_rec( p, Wlc_ObjFo2Fi(p, pObj), iFrame - 1, vMemObjs, vValues, ValueA, vRes ); else if ( Wlc_ObjType(pObj) == WLC_OBJ_BUF ) Wlc_NtkTrace_rec( p, Wlc_ObjFanin0(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes ); else if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX ) { int Index = 3*(iFrame*Vec_IntSize(vMemObjs) + iNum); - Wlc_NtkTrace_rec( p, Vec_WrdEntry(vValues, Index) ? Wlc_ObjFanin2(p, pObj) : Wlc_ObjFanin1(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes ); - Vec_IntPush( vRes, (iObj << 10) | iFrame ); + int Value = (int)Vec_WrdEntry( vValues, Index ); + assert( Value == 0 && Value == 1 ); + Wlc_NtkTrace_rec( p, Value ? Wlc_ObjFanin2(p, pObj) : Wlc_ObjFanin1(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes ); + Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) | Value ); } else if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE ) { int Index = 3*(iFrame*Vec_IntSize(vMemObjs) + iNum); if ( Vec_WrdEntry(vValues, Index + 1) != ValueA ) // address Wlc_NtkTrace_rec( p, Wlc_ObjFanin0(p, pObj), iFrame, vMemObjs, vValues, ValueA, vRes ); - Vec_IntPush( vRes, (iObj << 10) | iFrame ); + Vec_IntPush( vRes, (iObj << 11) | (iFrame << 1) ); } else assert( 0 ); } Vec_Int_t * Wlc_NtkTrace( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFrame, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues ) { - int iObj = Wlc_ObjId(p, pObj); + int iObj = Wlc_ObjId( p, pObj ); int iNum = Wlc_ObjCopy( p, iObj ); Vec_Int_t * vTrace = Vec_IntAlloc( 10 ); assert( Wlc_ObjType(pObj) == WLC_OBJ_READ ); assert( iObj == Vec_IntEntry(vMemObjs, iNum) ); Wlc_NtkTrace_rec( p, Wlc_ObjFanin0(p, pObj), iFrame, vMemObjs, vValues, Vec_WrdEntry(vValues, 3*(iFrame*Vec_IntSize(vMemObjs) + iNum) + 1), vTrace ); - Vec_IntPush( vTrace, (iObj << 10) | iFrame ); + Vec_IntPush( vTrace, (iObj << 11) | (iFrame << 1) ); return vTrace; } int Wlc_NtkTraceCheckConfict( Wlc_Ntk_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues ) { Wlc_Obj_t * pObjLast, * pObjFirst; - int iFrmLast = Vec_IntEntryLast(vTrace) & 0x3FF; - int iObjLast = Vec_IntEntryLast(vTrace) >> 10; + int iObjLast = Vec_IntEntryLast(vTrace) >> 11; + int iFrmLast =(Vec_IntEntryLast(vTrace) >> 1) & 0x3FF; int iNumLast = Wlc_ObjCopy( p, iObjLast ); int iIndLast = 3*(iFrmLast*Vec_IntSize(vMemObjs) + iNumLast); - int iFrmFirst = Vec_IntEntry(vTrace, 0) & 0x3FF; - int iObjFirst = Vec_IntEntry(vTrace, 0) >> 10; + int iObjFirst = Vec_IntEntry(vTrace, 0) >> 11; + int iFrmFirst =(Vec_IntEntry(vTrace, 0) >> 1) & 0x3FF; int iNumFirst = Wlc_ObjCopy( p, iObjFirst ); int iIndFirst = 3*(iFrmFirst*Vec_IntSize(vMemObjs) + iNumFirst); assert( Vec_IntSize(vTrace) >= 2 ); @@ -621,22 +677,25 @@ int Wlc_NtkTraceCheckConfict( Wlc_Ntk_t * p, Vec_Int_t * vTrace, Vec_Int_t * vMe assert( Wlc_ObjType(pObjFirst) == WLC_OBJ_WRITE || Wlc_ObjIsPi(pObjFirst) ); if ( Wlc_ObjIsPi(pObjFirst) ) return 0; - assert( Vec_WrdEntry(vValues, iIndLast + 1) == Vec_WrdEntry(vValues, iIndFirst + 1) ); + assert( Vec_WrdEntry(vValues, iIndLast + 1) == Vec_WrdEntry(vValues, iIndFirst + 1) ); // equal addr return Vec_WrdEntry(vValues, iIndLast + 2) != Vec_WrdEntry(vValues, iIndFirst + 2); // diff data } Vec_Int_t * Wlc_NtkFindConflict( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues, int nFrames ) { Wlc_Obj_t * pObj; int i, f, Entry; - Vec_Wec_t * vTraces = Vec_WecStart( 100 ); + Vec_Wec_t * vTraces = Vec_WecAlloc( 100 ); Vec_Int_t * vTrace, * vTrace1, * vTrace2; assert( 3 * nFrames * Vec_IntSize(vMemObjs) == Vec_WrdSize(vValues) ); + Wlc_NtkCleanCopy( p ); + Vec_IntForEachEntry( vMemObjs, Entry, i ) + Wlc_ObjSetCopy( p, Entry, i ); for ( f = 0; f < nFrames; f++ ) { Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i ) { if ( Wlc_ObjType(pObj) != WLC_OBJ_READ ) continue; - vTrace = Wlc_NtkTrace( p, pObj, nFrames, vMemObjs, vValues ); + vTrace = Wlc_NtkTrace( p, pObj, f, vMemObjs, vValues ); if ( Wlc_NtkTraceCheckConfict( p, vTrace, vMemObjs, vValues ) ) { Vec_WecFree( vTraces ); @@ -652,20 +711,26 @@ Vec_Int_t * Wlc_NtkFindConflict( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wrd_t Vec_WecForEachLevelStop( vTraces, vTrace2, f, i ) if ( Vec_IntEntry(vTrace1, 0) == Vec_IntEntry(vTrace2, 0) ) { - int iObj1 = Vec_IntEntryLast(vTrace1); + int iObj1 = Vec_IntEntryLast(vTrace1) >> 11; + int iFrm1 =(Vec_IntEntryLast(vTrace1) >> 1) & 0x3FF; int iNum1 = Wlc_ObjCopy( p, iObj1 ); - int iObj2 = Vec_IntEntryLast(vTrace2); + int iInd1 = 3*(iFrm1*Vec_IntSize(vMemObjs) + iNum1); + + int iObj2 = Vec_IntEntryLast(vTrace2) >> 11; + int iFrm2 =(Vec_IntEntryLast(vTrace2) >> 1) & 0x3FF; int iNum2 = Wlc_ObjCopy( p, iObj2 ); + int iInd2 = 3*(iFrm2*Vec_IntSize(vMemObjs) + iNum2); + assert( iObj1 == Vec_IntEntry(vMemObjs, iNum1) ); assert( iObj2 == Vec_IntEntry(vMemObjs, iNum2) ); - if ( Vec_WrdEntry(vValues, 3*iNum1 + 1) == Vec_WrdEntry(vValues, 3*iNum2 + 1) && // same address - Vec_WrdEntry(vValues, 3*iNum2 + 1) != Vec_WrdEntry(vValues, 3*iNum2 + 1) ) // different data + if ( Vec_WrdEntry(vValues, iInd1 + 1) == Vec_WrdEntry(vValues, iInd2 + 1) && // equal address + Vec_WrdEntry(vValues, iInd1 + 2) != Vec_WrdEntry(vValues, iInd2 + 2) ) // diff data { vTrace = Vec_IntAlloc( 100 ); Vec_IntPush( vTrace, Vec_IntPop(vTrace1) ); - Vec_IntForEachEntry( vTrace1, Entry, i ) + Vec_IntForEachEntryStart( vTrace1, Entry, i, 1 ) Vec_IntPushUnique( vTrace, Entry ); - Vec_IntForEachEntry( vTrace2, Entry, i ) + Vec_IntForEachEntryStart( vTrace2, Entry, i, 1 ) Vec_IntPushUnique( vTrace, Entry ); Vec_WecFree( vTraces ); return vTrace; @@ -674,16 +739,38 @@ Vec_Int_t * Wlc_NtkFindConflict( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wrd_t Vec_WecFree( vTraces ); return NULL; } -Vec_Bit_t * Wlc_NtkCollectMuxValues( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues, int nFrames ) +void Wlc_NtkPrintConflict( Wlc_Ntk_t * p, Vec_Int_t * vTrace ) { - Vec_Bit_t * vBitValues = Vec_BitStart( nFrames * Wlc_NtkObjNum(p) ); - Wlc_Obj_t * pObj; int i, f; - Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i ) - if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX ) - for ( f = 0; f < nFrames; f++ ) - if ( Vec_WrdEntry(vValues, 3*f*Vec_IntSize(vMemObjs) + i) ) - Vec_BitWriteEntry( vBitValues, f*Wlc_NtkObjNum(p) + Wlc_ObjId(p, pObj), 1 ); - return vBitValues; + int Entry, i; + printf( "Memory semantics failure trace:\n" ); + Vec_IntForEachEntry( vTrace, Entry, i ) + printf( "%3d: entry %9d : obj %5d with name %16s in frame %d\n", i, Entry, Entry >> 11, Wlc_ObjName(p, Entry>>11), (Entry >> 1) & 0x3FF ); +} +void Wlc_NtkPrintCex( Wlc_Ntk_t * p, Wlc_Ntk_t * pAbs, Abc_Cex_t * pCex ) +{ + Wlc_Obj_t * pObj; int i, k, f, nBits = pCex ? pCex->nRegs : 0; + if ( pCex == NULL ) + { + printf( "The CEX is NULL.\n" ); + return; + } + for ( f = 0; f <= pCex->iFrame; f++ ) + { + printf( "Frame%02d ", f ); + Wlc_NtkForEachPi( pAbs, pObj, i ) + { + printf( "PI%d:", i ); + //printf( "%d(%d):", nBits, Wlc_ObjRange(pObj) ); + for ( k = 0; k < Wlc_ObjRange(pObj); k++ ) + printf( "%d", Abc_InfoHasBit(pCex->pData, nBits++) ); + printf( " " ); + } + printf( "FF:" ); + for ( k = 0; nBits < pCex->nPis; k++ ) + printf( "%d", Abc_InfoHasBit(pCex->pData, nBits++) ); + printf( "\n" ); + } + } /**Function************************************************************* @@ -700,32 +787,41 @@ Vec_Bit_t * Wlc_NtkCollectMuxValues( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs, Vec_Wr Wlc_Ntk_t * Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p ) { int iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits; - Vec_Int_t * vFirstTotal; + Vec_Int_t * vRefine; Vec_Int_t * vMemObjs = Wlc_NtkCollectMemory( p ); Vec_Int_t * vMemFanins = Wlc_NtkCollectMemFanins( p, vMemObjs ); Vec_Wec_t * vRefines = Vec_WecAlloc( 100 ); Vec_Int_t * vNodeFrames = Vec_IntAlloc( 100 ); -// Wlc_Ntk_t * pNewFull = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL, NULL ); - Wlc_Ntk_t * pNewFull = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames, NULL ); + Wlc_Ntk_t * pNewFull; + + vRefine = Vec_WecPushLevel(vRefines); + Vec_IntPush( vRefine, (11 << 11) | 0 ); + Vec_IntPush( vRefine, (10 << 11) | 0 ); + Vec_IntPush( vRefine, ( 8 << 11) | 0 ); + Vec_IntPush( vRefine, ( 9 << 11) | 0 ); + Wlc_NtkAbsAddToNodeFrames( vNodeFrames, vRefine ); + +// pNewFull = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL ); + pNewFull = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames ); + Vec_WecFree( vRefines ); Vec_IntFree( vNodeFrames ); nDcBits = Wlc_CountDcs( pNewFull->pInits ); - vFirstTotal = Wlc_NtkDeriveFirstTotal( p, vMemObjs, vMemFanins, iFirstMemPi, nDcBits + iFirstMemCi ); printf( "iFirstMemPi = %d iFirstCi = %d iFirstMemCi = %d nDcBits = %d\n", iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits ); + Vec_IntFreeP( &vMemObjs ); Vec_IntFreeP( &vMemFanins ); - Vec_IntFreeP( &vFirstTotal ); return pNewFull; } int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbose ) { abctime clk = Abc_Clock(); - Wlc_Ntk_t * pNewFull, * pNew; Aig_Man_t * pAig; - Gia_Man_t * pAbsFull, * pAbs, * pTemp; - Abc_Cex_t * pCex = NULL; Vec_Wrd_t * vValues = NULL; Vec_Bit_t * vMuxVal = NULL; + Wlc_Ntk_t * pNewFull, * pNew; Aig_Man_t * pAig, * pTempAig; + Gia_Man_t * pAbsFull, * pAbs; + Abc_Cex_t * pCex = NULL; Vec_Wrd_t * vValues = NULL; Vec_Wec_t * vRefines = Vec_WecAlloc( 100 ); Vec_Int_t * vNodeFrames = Vec_IntAlloc( 100 ); Vec_Int_t * vMemObjs, * vMemFanins, * vFirstTotal, * vRefine; @@ -733,15 +829,16 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbo vMemObjs = Wlc_NtkCollectMemory( p ); vMemFanins = Wlc_NtkCollectMemFanins( p, vMemObjs ); - pNewFull = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL, NULL ); + pNewFull = Wlc_NtkAbstractMemory( p, vMemObjs, vMemFanins, &iFirstMemPi, &iFirstCi, &iFirstMemCi, NULL, NULL ); nDcBits = Wlc_CountDcs( pNewFull->pInits ); - vFirstTotal = Wlc_NtkDeriveFirstTotal( p, vMemObjs, vMemFanins, iFirstMemPi, nDcBits + iFirstMemCi ); + vFirstTotal = Wlc_NtkDeriveFirstTotal( p, vMemObjs, vMemFanins, iFirstMemPi, nDcBits + iFirstMemCi, fVerbose ); pAbsFull = Wlc_NtkBitBlast( pNewFull, NULL ); assert( Gia_ManPiNum(pAbsFull) == iFirstCi + nDcBits ); + Wlc_NtkFree( pNewFull ); // perform abstraction - for ( nIters = 1; nIters < 10000; nIters++ ) + for ( nIters = 0; nIters < nIterMax; nIters++ ) { // set up parameters to run PDR Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; @@ -750,64 +847,80 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fPdrVerbose, int fVerbo pPdrPars->fVerbose = fVerbose; // derive specific abstraction - pNew = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames, vMuxVal ); + pNew = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames ); pAbs = Wlc_NtkBitBlast( pNew, NULL ); - Wlc_NtkFree( pNew ); // simplify the AIG - pAbs = Gia_ManSeqStructSweep( pTemp = pAbs, 1, 1, 0 ); - Gia_ManStop( pTemp ); + //pAbs = Gia_ManSeqStructSweep( pGiaTemp = pAbs, 1, 1, 0 ); + //Gia_ManStop( pGiaTemp ); - // try to prove abstracted GIA by converting it to AIG and calling PDR + // roll in the constraints pAig = Gia_ManToAigSimple( pAbs ); Gia_ManStop( pAbs ); + pAig->nConstrs = 1; + pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0 ); + Aig_ManStop( pTempAig ); + pAbs = Gia_ManFromAigSimple( pAig ); + Aig_ManStop( pAig ); + //Gia_AigerWrite( pAbs, "mem_abs.aig", 0, 0 ); + + // try to prove abstracted GIA by converting it to AIG and calling PDR + pAig = Gia_ManToAigSimple( pAbs ); RetValue = Pdr_ManSolve( pAig, pPdrPars ); pCex = pAig->pSeqModel; pAig->pSeqModel = NULL; Aig_ManStop( pAig ); + if ( fVerbose ) + printf( "\nITERATIONS %d:\n", nIters ); + if ( fVerbose ) + Wlc_NtkPrintCex( p, pNew, pCex ); + Wlc_NtkFree( pNew ); + // check if proved or undecided if ( pCex == NULL ) { assert( RetValue ); + Gia_ManStop( pAbs ); break; } // analyze counter-example - Vec_BitFreeP( &vMuxVal ); - vValues = Wlc_NtkConvertCex( p, vFirstTotal, pAbs, pCex ); - vMuxVal = Wlc_NtkCollectMuxValues( p, vMemObjs, vValues, pCex->iFrame + 1 ); + vValues = Wlc_NtkConvertCex( vFirstTotal, pAbsFull, pCex, fVerbose ); + Gia_ManStop( pAbs ); vRefine = Wlc_NtkFindConflict( p, vMemObjs, vValues, pCex->iFrame + 1 ); Vec_WrdFree( vValues ); - Abc_CexFree( pCex ); // return CEX in the future - if ( vRefine == NULL ) + if ( vRefine == NULL ) // cannot refine break; + Abc_CexFreeP( &pCex ); // save refinement for the future + if ( fVerbose ) + Wlc_NtkPrintConflict( p, vRefine ); Vec_WecPushLevel( vRefines ); Vec_IntAppend( Vec_WecEntryLast(vRefines), vRefine ); Wlc_NtkAbsAddToNodeFrames( vNodeFrames, vRefine ); Vec_IntFree( vRefine ); } // cleanup - Wlc_NtkFree( pNew ); + Gia_ManStop( pAbsFull ); Vec_WecFree( vRefines ); Vec_IntFreeP( &vMemObjs ); Vec_IntFreeP( &vMemFanins ); Vec_IntFreeP( &vFirstTotal ); Vec_IntFreeP( &vNodeFrames ); - Vec_BitFreeP( &vMuxVal ); // report the result if ( fVerbose ) printf( "\n" ); printf( "Abstraction " ); - if ( RetValue == 0 ) - printf( "resulted in a real CEX" ); + if ( RetValue == 0 && pCex ) + printf( "resulted in a real CEX in frame %d", pCex->iFrame ); else if ( RetValue == 1 ) printf( "is successfully proved" ); else printf( "timed out" ); printf( " after %d iterations. ", nIters ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + Abc_CexFreeP( &pCex ); // return CEX in the future return RetValue; } diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index b65558e6..b3b87f9e 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -334,6 +334,8 @@ int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p ) Vec_IntWriteEntry( &p->vLevels, i, LevelMax - Wlc_ObjLevelId(p, i) ); Wlc_NtkForEachCi( p, pObj, i ) Vec_IntWriteEntry( &p->vLevels, Wlc_ObjId(p, pObj), 0 ); + //Wlc_NtkForEachObj( p, pObj, i ) + // printf( "%d -> %d\n", i, Wlc_ObjLevelId(p, i) ); return LevelMax; } @@ -624,36 +626,36 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fTwoSides, int fVerbose ) void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { printf( "%8d : ", Wlc_ObjId(p, pObj) ); - printf( "%3d%s", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " ); + printf( "%6d%s = ", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " ); if ( pObj->Type == WLC_OBJ_PI ) { - printf( " PI\n" ); + printf( "PI\n" ); return; } if ( pObj->Type == WLC_OBJ_FO ) { - printf( " FO\n" ); + printf( "FO\n" ); return; } - if ( pObj->Type == WLC_OBJ_CONST ) - printf( " " ); - else + if ( pObj->Type != WLC_OBJ_CONST ) { - printf( " = %3d%s %5s ", Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin0(p, pObj)) ? "s" : " ", Wlc_Names[(int)pObj->Type] ); + printf( "%6d%s %5s ", Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin0(p, pObj)) ? "s" : " ", Wlc_Names[(int)pObj->Type] ); if ( Wlc_ObjFaninNum(pObj) > 1 ) - printf( "%3d%s ", Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin1(p, pObj)) ? "s" : " " ); + printf( "%6d%s ", Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin1(p, pObj)) ? "s" : " " ); else - printf( " " ); + printf( " " ); if ( Wlc_ObjFaninNum(pObj) > 2 ) - printf( "%3d%s ", Wlc_ObjRange(Wlc_ObjFanin2(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin2(p, pObj)) ? "s" : " " ); + printf( "%6d%s ", Wlc_ObjRange(Wlc_ObjFanin2(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin2(p, pObj)) ? "s" : " " ); else - printf( " " ); + printf( " " ); } + else + printf( " " ); printf( " : " ); printf( "%-12s", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) ); if ( pObj->Type == WLC_OBJ_CONST ) { - printf( " = %d\'%sh", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s":"" ); + printf( " = %d\'%sh", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s":"" ); if ( pObj->fXConst ) { int k; @@ -723,6 +725,12 @@ void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose printf( "%2d : %-8s %6d\n", i, Wlc_Names[i], p->nObjs[i] ); } } +void Wlc_NtkPrintObjects( Wlc_Ntk_t * p ) +{ + Wlc_Obj_t * pObj; int i; + Wlc_NtkForEachObj( p, pObj, i ) + Wlc_NtkPrintNode( p, pObj ); +} /**Function************************************************************* @@ -928,7 +936,8 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq ) } if ( p->pSpec ) pNew->pSpec = Abc_UtilStrsav( p->pSpec ); - Wlc_NtkTransferNames( pNew, p ); + if ( Wlc_NtkHasNameId(p) ) + Wlc_NtkTransferNames( pNew, p ); if ( Vec_IntSize(&p->vPoPairs) ) Vec_IntAppend( &pNew->vPoPairs, &p->vPoPairs ); return pNew; |