luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Memory abstraction.

This commit is contained in:
Alan Mishchenko 2018-04-19 17:05:04 -07:00
parent 098103012d
commit 1c6655578c
4 changed files with 284 additions and 154 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/base/wlc/wlc.h
View File

@ -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 );

11
src/base/wlc/wlcCom.c
View File

@ -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;

391
src/base/wlc/wlcMem.c
View File

@ -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;
// add the constraint as fanin to the output
Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pConstr) );
Wlc_ObjAddFanins( pNew, pConstrOut, vFanins );
}
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_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_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 );
}
}
}
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 * 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 );
// 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 );
Gia_ManStop( 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;
}

35
src/base/wlc/wlcNtk.c
View File

@ -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;