mirror of https://github.com/YosysHQ/abc.git
1523 lines
58 KiB
C
1523 lines
58 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [wlcMem.c]
|
|
|
|
SystemName [ABC: Logic synthesis and verification system.]
|
|
|
|
PackageName [Verilog parser.]
|
|
|
|
Synopsis [Memory abstraction.]
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 1.0. Started - August 22, 2014.]
|
|
|
|
Revision [$Id: wlcMem.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#include "wlc.h"
|
|
#include "sat/bsat/satStore.h"
|
|
#include "proof/pdr/pdr.h"
|
|
#include "proof/pdr/pdrInt.h"
|
|
|
|
ABC_NAMESPACE_IMPL_START
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Memory blasting.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Wlc_NtkMemBlast_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * vFanins )
|
|
{
|
|
Wlc_Obj_t * pObj;
|
|
int i, iFanin;
|
|
if ( Wlc_ObjCopy(p, iObj) )
|
|
return;
|
|
pObj = Wlc_NtkObj( p, iObj );
|
|
Wlc_ObjForEachFanin( pObj, iFanin, i )
|
|
Wlc_NtkMemBlast_rec( pNew, p, iFanin, vFanins );
|
|
if ( pObj->Type == WLC_OBJ_WRITE )
|
|
{
|
|
Vec_Int_t * vTemp = Vec_IntAlloc( 1 );
|
|
Vec_Int_t * vBits = Vec_IntAlloc( 100 );
|
|
Wlc_Obj_t * pMem = Wlc_ObjFanin0(p, pObj);
|
|
Wlc_Obj_t * pAddr = Wlc_ObjFanin1(p, pObj);
|
|
Wlc_Obj_t * pData = Wlc_ObjFanin2(p, pObj);
|
|
int DataW = Wlc_ObjRange(pData);
|
|
int AddrW = Wlc_ObjRange(pAddr);
|
|
int nRegs = 1 << AddrW, iObjNew, iObjDec;
|
|
assert( nRegs * DataW == Wlc_ObjRange(pMem) );
|
|
assert( Wlc_ObjRange(pObj) == Wlc_ObjRange(pMem) );
|
|
// create decoder
|
|
iObjDec = Wlc_ObjAlloc( pNew, WLC_OBJ_DEC, 0, nRegs-1, 0 );
|
|
Vec_IntFill( vTemp, 1, Wlc_ObjCopy(p, Wlc_ObjId(p, pAddr)) );
|
|
Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjDec), vTemp );
|
|
// create decoder bits
|
|
for ( i = 0; i < nRegs; i++ )
|
|
{
|
|
int iObj2 = Wlc_ObjAlloc( pNew, WLC_OBJ_BIT_SELECT, 0, i, i );
|
|
Vec_IntFill( vTemp, 1, iObjDec );
|
|
Vec_IntPushTwo( vTemp, i, i );
|
|
Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObj2), vTemp );
|
|
Vec_IntPush( vBits, iObj2 );
|
|
}
|
|
// create data words
|
|
Vec_IntClear( vFanins );
|
|
for ( i = 0; i < nRegs; i++ )
|
|
{
|
|
int iObj2 = Wlc_ObjAlloc( pNew, WLC_OBJ_BIT_SELECT, 0, i*DataW+DataW-1, i*DataW );
|
|
Vec_IntFill( vTemp, 1, Wlc_ObjCopy(p, Wlc_ObjId(p, pMem)) );
|
|
Vec_IntPushTwo( vTemp, i*DataW+DataW-1, i*DataW );
|
|
Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObj2), vTemp );
|
|
Vec_IntPush( vFanins, iObj2 );
|
|
}
|
|
// create MUXes of data words controlled by decoder bits
|
|
for ( i = 0; i < nRegs; i++ )
|
|
{
|
|
int iObj2 = Wlc_ObjAlloc( pNew, WLC_OBJ_MUX, 0, DataW-1, 0 );
|
|
Vec_IntFill( vTemp, 1, Vec_IntEntry(vBits, i) );
|
|
Vec_IntPushTwo( vTemp, Wlc_ObjCopy(p, Wlc_ObjId(p, pData)), Vec_IntEntry(vFanins, i) );
|
|
Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObj2), vTemp );
|
|
Vec_IntWriteEntry( vFanins, i, iObj2 );
|
|
}
|
|
// concatenate the results
|
|
iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_BIT_CONCAT, 0, nRegs*DataW-1, 0 );
|
|
Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
|
|
Wlc_ObjSetCopy( p, iObj, iObjNew );
|
|
Vec_IntFree( vTemp );
|
|
Vec_IntFree( vBits );
|
|
}
|
|
else if ( pObj->Type == WLC_OBJ_READ )
|
|
{
|
|
Vec_Int_t * vTemp = Vec_IntAlloc( 1 );
|
|
Wlc_Obj_t * pMem = Wlc_ObjFanin0(p, pObj);
|
|
Wlc_Obj_t * pAddr = Wlc_ObjFanin1(p, pObj);
|
|
int DataW = Wlc_ObjRange(pObj);
|
|
int AddrW = Wlc_ObjRange(pAddr);
|
|
int nRegs = 1 << AddrW, iObjNew;
|
|
assert( nRegs * DataW == Wlc_ObjRange(pMem) );
|
|
Vec_IntClear( vFanins );
|
|
Vec_IntPush( vFanins, Wlc_ObjCopy(p, Wlc_ObjId(p, pAddr)) );
|
|
for ( i = 0; i < nRegs; i++ )
|
|
{
|
|
int iObj2 = Wlc_ObjAlloc( pNew, WLC_OBJ_BIT_SELECT, 0, i*DataW+DataW-1, i*DataW );
|
|
Vec_IntFill( vTemp, 1, Wlc_ObjCopy(p, Wlc_ObjId(p, pMem)) );
|
|
Vec_IntPushTwo( vTemp, i*DataW+DataW-1, i*DataW );
|
|
Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObj2), vTemp );
|
|
Vec_IntPush( vFanins, iObj2 );
|
|
}
|
|
iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_MUX, 0, DataW-1, 0 );
|
|
Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
|
|
Wlc_ObjSetCopy( p, iObj, iObjNew );
|
|
Vec_IntFree( vTemp );
|
|
}
|
|
else
|
|
Wlc_ObjDup( pNew, p, iObj, vFanins );
|
|
}
|
|
Wlc_Ntk_t * Wlc_NtkMemBlast( Wlc_Ntk_t * p )
|
|
{
|
|
Wlc_Ntk_t * pNew;
|
|
Wlc_Obj_t * pObj;
|
|
Vec_Int_t * vFanins;
|
|
int i;
|
|
Wlc_NtkCleanCopy( p );
|
|
vFanins = Vec_IntAlloc( 100 );
|
|
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
|
|
pNew->fSmtLib = p->fSmtLib;
|
|
pNew->fAsyncRst = p->fAsyncRst;
|
|
pNew->fMemPorts = p->fMemPorts;
|
|
pNew->fEasyFfs = p->fEasyFfs;
|
|
Wlc_NtkForEachCi( p, pObj, i )
|
|
Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
|
|
Wlc_NtkForEachCo( p, pObj, i )
|
|
Wlc_NtkMemBlast_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
|
|
Wlc_NtkForEachCo( p, pObj, i )
|
|
Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
|
|
if ( p->vInits )
|
|
pNew->vInits = Vec_IntDup( p->vInits );
|
|
if ( p->pInits )
|
|
pNew->pInits = Abc_UtilStrsav( p->pInits );
|
|
Vec_IntFree( vFanins );
|
|
if ( p->pSpec )
|
|
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
|
|
return pNew;
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Collect memory nodes.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Vec_Int_t * Wlc_NtkCollectMemSizes( Wlc_Ntk_t * p )
|
|
{
|
|
Wlc_Obj_t * pObj; int i;
|
|
Vec_Int_t * vMemSizes = Vec_IntAlloc( 10 );
|
|
Wlc_NtkForEachObj( p, pObj, i )
|
|
{
|
|
if ( Wlc_ObjType(pObj) != WLC_OBJ_WRITE && Wlc_ObjType(pObj) != WLC_OBJ_READ )
|
|
continue;
|
|
pObj = Wlc_ObjFanin( p, pObj, 0 );
|
|
Vec_IntPushUnique( vMemSizes, Wlc_ObjRange(pObj) );
|
|
}
|
|
return vMemSizes;
|
|
}
|
|
// remove PIs without fanout, non-driven object and their fanouts
|
|
int Wlc_ObjCheckIsEmpty_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
|
|
{
|
|
int k, iFanin;
|
|
if ( Wlc_ObjType(pObj) == 0 )
|
|
return 1;
|
|
if ( Wlc_ObjIsPi(pObj) )
|
|
return Vec_IntEntry(&p->vRefs, Wlc_ObjId(p, pObj)) == 0;
|
|
else if ( Wlc_ObjIsCi(pObj) )
|
|
return 0;
|
|
Wlc_ObjForEachFanin( pObj, iFanin, k )
|
|
if ( !Wlc_ObjCheckIsEmpty_rec(p, Wlc_NtkObj(p, iFanin)) )
|
|
return 0;
|
|
return 1;
|
|
}
|
|
Vec_Int_t * Wlc_NtkCleanObjects( Wlc_Ntk_t * p, Vec_Int_t * vObjs )
|
|
{
|
|
Wlc_Obj_t * pObj; int i;
|
|
Vec_Int_t * vMemObjs = Vec_IntAlloc( 10 );
|
|
Wlc_NtkSetRefs( p );
|
|
Wlc_NtkForEachObjVec( vObjs, p, pObj, i )
|
|
{
|
|
//printf( "Considering %d (%s)\n", Wlc_ObjId(p, pObj), Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
|
|
if ( !Wlc_ObjCheckIsEmpty_rec(p, pObj) )
|
|
Vec_IntPush( vMemObjs, Wlc_ObjId(p, pObj) );
|
|
}
|
|
return vMemObjs;
|
|
}
|
|
Vec_Int_t * Wlc_NtkCollectMemory( Wlc_Ntk_t * p, int fClean )
|
|
{
|
|
Wlc_Obj_t * pObj; int i;
|
|
Vec_Int_t * vMemSizes = Wlc_NtkCollectMemSizes( p );
|
|
Vec_Int_t * vMemObjs = Vec_IntAlloc( 10 );
|
|
Wlc_NtkForEachObj( p, pObj, i )
|
|
{
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE || Wlc_ObjType(pObj) == WLC_OBJ_READ )
|
|
Vec_IntPush( vMemObjs, i );
|
|
else if ( Vec_IntFind(vMemSizes, Wlc_ObjRange(pObj)) >= 0 )
|
|
Vec_IntPush( vMemObjs, i );
|
|
}
|
|
Vec_IntFree( vMemSizes );
|
|
Vec_IntSort( vMemObjs, 0 );
|
|
//Wlc_NtkPrintNodeArray( p, vMemObjs );
|
|
if ( fClean )
|
|
{
|
|
Vec_Int_t * vTemp;
|
|
vMemObjs = Wlc_NtkCleanObjects( p, vTemp = vMemObjs );
|
|
Vec_IntFree( vTemp );
|
|
}
|
|
return vMemObjs;
|
|
}
|
|
void Wlc_NtkPrintMemory( Wlc_Ntk_t * p )
|
|
{
|
|
Vec_Int_t * vMemory;
|
|
vMemory = Wlc_NtkCollectMemory( p, 1 );
|
|
printf( "Memory subsystem is composed of the following objects:\n" );
|
|
Wlc_NtkPrintNodeArray( p, vMemory );
|
|
Vec_IntFree( vMemory );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Collect fanins of memory subsystem.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Vec_Int_t * Wlc_NtkCollectMemFanins( Wlc_Ntk_t * p, Vec_Int_t * vMemObjs )
|
|
{
|
|
Wlc_Obj_t * pObj; int i, k, iFanin;
|
|
Vec_Int_t * vMemFanins = Vec_IntAlloc( 100 );
|
|
Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
|
|
{
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
|
|
Vec_IntPush( vMemFanins, Wlc_ObjFaninId0(pObj) );
|
|
else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ || Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
|
|
{
|
|
Wlc_ObjForEachFanin( pObj, iFanin, k )
|
|
if ( k > 0 )
|
|
Vec_IntPush( vMemFanins, iFanin );
|
|
}
|
|
}
|
|
return vMemFanins;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Abstract memory nodes.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Wlc_CountDcs( char * pInit )
|
|
{
|
|
int Count = 0;
|
|
for ( ; *pInit; pInit++ )
|
|
Count += (*pInit == 'x' || *pInit == 'X');
|
|
return Count;
|
|
}
|
|
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, 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, int iFanin, Vec_Int_t * vFanins, int fIsFi )
|
|
{
|
|
int iObj = Wlc_ObjAlloc( pNew, WLC_OBJ_BUF, pObj->Signed, pObj->End, pObj->Beg );
|
|
Wlc_Obj_t * pObjNew = Wlc_NtkObj( pNew, iObj );
|
|
Vec_IntFill( vFanins, 1, iFanin );
|
|
Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
|
|
Wlc_ObjSetCo( pNew, pObjNew, fIsFi );
|
|
}
|
|
|
|
void Wlc_NtkAbsAddToNodeFrames( Vec_Int_t * vNodeFrames, Vec_Int_t * vLevel )
|
|
{
|
|
int i, Entry;
|
|
Vec_IntForEachEntry( vLevel, Entry, i )
|
|
Vec_IntPushUnique( vNodeFrames, Entry );
|
|
Vec_IntSort( vNodeFrames, 0 );
|
|
}
|
|
Vec_Int_t * Wlc_NtkAbsCreateFlopOutputs( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vNodeFrames, Vec_Int_t * vFanins )
|
|
{
|
|
Vec_Int_t * vNewObjs = Vec_IntAlloc( 2*Vec_IntSize(vNodeFrames) );
|
|
Wlc_Obj_t * pObj, * pFanin = NULL;
|
|
int i, Entry, iObj, iFrame;
|
|
Vec_IntForEachEntry( vNodeFrames, Entry, i )
|
|
{
|
|
iObj = Entry >> 11;
|
|
iFrame = (Entry >> 1) & 0x3FF;
|
|
pObj = Wlc_NtkObj( p, iObj );
|
|
// address
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
|
|
pFanin = Wlc_ObjFanin0(p, pObj);
|
|
else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ || Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
|
|
pFanin = Wlc_ObjFanin1(p, pObj);
|
|
else assert( 0 );
|
|
Vec_IntPush( vNewObjs, Wlc_NtkDupOneObject(pNew, p, pFanin, WLC_OBJ_FO, vFanins) );
|
|
// data
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
|
|
pFanin = NULL;
|
|
else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
|
|
pFanin = pObj;
|
|
else if ( Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
|
|
pFanin = Wlc_ObjFanin2(p, pObj);
|
|
else assert( 0 );
|
|
Vec_IntPush( vNewObjs, pFanin ? Wlc_NtkDupOneObject(pNew, p, pFanin, WLC_OBJ_FO, vFanins) : 0 );
|
|
}
|
|
assert( Vec_IntSize(vNewObjs) == 2 * Vec_IntSize(vNodeFrames) );
|
|
return vNewObjs;
|
|
}
|
|
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 )
|
|
{
|
|
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], iFrameLast, iFrameThis;
|
|
assert( Vec_IntSize(vNewObjs) == 2 * Vec_IntSize(vNodeFrames) );
|
|
Vec_WecForEachLevel( vConstrs, vTrace, i )
|
|
{
|
|
if ( Vec_IntSize(vTrace) == 0 )
|
|
continue;
|
|
assert( Vec_IntSize(vTrace) >= 2 );
|
|
Vec_IntClear( vLevConstr );
|
|
|
|
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]) );
|
|
pAddrs[1] = Wlc_NtkObj( pNew, Vec_IntEntry(vNewObjs, 2*Index[1]) );
|
|
|
|
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]) );
|
|
Wlc_ObjAddFanins( pNew, pCond, vFanins );
|
|
Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) );
|
|
|
|
// different datas
|
|
pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0));
|
|
Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pDatas[0]), Wlc_ObjId(pNew, pDatas[1]) );
|
|
Wlc_ObjAddFanins( pNew, pCond, vFanins );
|
|
Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) );
|
|
|
|
Vec_IntForEachEntryStartStop( vTrace, Entry, k, 1, Vec_IntSize(vTrace)-1 )
|
|
{
|
|
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]) );
|
|
pCond = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0));
|
|
Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pAddrs[0]), Wlc_ObjId(pNew, pAddrs[1]) );
|
|
Wlc_ObjAddFanins( pNew, pCond, vFanins );
|
|
Vec_IntPush( vLevConstr, Wlc_ObjId(pNew, pCond) );
|
|
}
|
|
}
|
|
|
|
// create last output
|
|
pConstr = Wlc_NtkObj( pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vLevConstr)-1, 0) );
|
|
Wlc_ObjAddFanins( pNew, pConstr, vLevConstr );
|
|
Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pConstr) );
|
|
pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_REDUCT_AND, 0, 0, 0));
|
|
Wlc_ObjAddFanins( pNew, pConstr, vFanins );
|
|
|
|
// save the result
|
|
Vec_IntPush( vBitConstr, Wlc_ObjId(pNew, pConstr) );
|
|
}
|
|
if ( Vec_IntSize(vBitConstr) > 0 )
|
|
{
|
|
// create last output
|
|
pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vBitConstr)-1, 0));
|
|
Wlc_ObjAddFanins( pNew, pConstr, vBitConstr );
|
|
// create last output
|
|
Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pConstr) );
|
|
pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_REDUCT_OR, 0, 0, 0));
|
|
Wlc_ObjAddFanins( pNew, pConstr, vFanins );
|
|
}
|
|
else
|
|
{
|
|
pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, 0, 0));
|
|
Vec_IntFill( vFanins, 1, 0 ); // const0 - always true
|
|
Wlc_ObjAddFanins( pNew, pConstr, vFanins );
|
|
}
|
|
// cleanup
|
|
Vec_IntFree( vBitConstr );
|
|
Vec_IntFree( vLevConstr );
|
|
// 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 )
|
|
{
|
|
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 = 16, nBits = 0;
|
|
|
|
// mark memory nodes
|
|
Wlc_NtkCleanMarks( p );
|
|
Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
|
|
pObj->Mark = 1;
|
|
|
|
// start new network
|
|
Wlc_NtkCleanCopy( p );
|
|
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + 1000 );
|
|
pNew->fSmtLib = p->fSmtLib;
|
|
pNew->fAsyncRst = p->fAsyncRst;
|
|
pNew->fMemPorts = p->fMemPorts;
|
|
pNew->fEasyFfs = p->fEasyFfs;
|
|
pNew->vInits = Vec_IntAlloc( 100 );
|
|
|
|
// duplicate PIs
|
|
Wlc_NtkForEachPi( p, pObj, i )
|
|
if ( !pObj->Mark )
|
|
{
|
|
Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
|
|
nBits += Wlc_ObjRange(pObj);
|
|
}
|
|
|
|
// create new PIs
|
|
*piFirstMemPi = nBits;
|
|
Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
|
|
{
|
|
Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins );
|
|
nBits += Wlc_ObjRange(pObj);
|
|
}
|
|
|
|
// duplicate flop outputs
|
|
*piFirstCi = nBits;
|
|
Wlc_NtkForEachCi( p, pObj, i )
|
|
if ( !Wlc_ObjIsPi(pObj) && !pObj->Mark )
|
|
{
|
|
Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
|
|
Vec_IntPush( pNew->vInits, Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p)) );
|
|
nBits += Wlc_ObjRange(pObj);
|
|
}
|
|
|
|
// create flop for time-frame counter
|
|
pCounter = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_FO, 0, AdderBits-1, 0));
|
|
Vec_IntPush( pNew->vInits, -AdderBits );
|
|
nBits += AdderBits;
|
|
|
|
// create flops for memory objects
|
|
*piFirstMemCi = nBits;
|
|
if ( vMemFanins )
|
|
Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
|
|
Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_FO, vFanins );
|
|
|
|
// create flops for constraint objects
|
|
if ( vConstrs )
|
|
vNewObjs = Wlc_NtkAbsCreateFlopOutputs( pNew, p, vNodeFrames, vFanins );
|
|
|
|
// duplicate objects
|
|
Wlc_NtkForEachObj( p, pObj, i )
|
|
if ( !Wlc_ObjIsCi(pObj) && !pObj->Mark )
|
|
Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
|
|
|
|
if ( Vec_IntSize(&p->vPoPairs) )
|
|
{
|
|
// create miter for the PO pairs
|
|
Vec_IntForEachEntryDouble( &p->vPoPairs, Po0, Po1, i )
|
|
{
|
|
int iCopy0 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po0)));
|
|
int iCopy1 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po1)));
|
|
int iObj = Wlc_ObjAlloc( pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0 );
|
|
Wlc_Obj_t * pObjNew = Wlc_NtkObj( pNew, iObj );
|
|
Vec_IntFillTwo( vFanins, 1, iCopy0, iCopy1 );
|
|
Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
|
|
Wlc_ObjSetCo( pNew, pObjNew, 0 );
|
|
}
|
|
printf( "Memory abstraction created %d miter outputs.\n", Wlc_NtkPoNum(pNew) );
|
|
Wlc_NtkForEachCo( p, pObj, i )
|
|
if ( pObj->fIsFi && !pObj->Mark )
|
|
Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
|
|
|
|
// create constraint output
|
|
if ( vConstrs )
|
|
Wlc_ObjSetCo( pNew, (pConstr = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_BUF, 0, 0, 0))), 0 );
|
|
}
|
|
else
|
|
{
|
|
// duplicate POs
|
|
Wlc_NtkForEachPo( p, pObj, i )
|
|
if ( !pObj->Mark )
|
|
Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
|
|
// create constraint output
|
|
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 )
|
|
Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
|
|
}
|
|
|
|
// create time-frame counter
|
|
pConst = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_CONST, 0, AdderBits-1, 0));
|
|
Vec_IntFill( vFanins, 1, 1 );
|
|
Wlc_ObjAddFanins( pNew, pConst, vFanins );
|
|
|
|
pAdder = Wlc_NtkObj(pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_ARI_ADD, 0, AdderBits-1, 0));
|
|
Vec_IntFillTwo( vFanins, 2, Wlc_ObjId(pNew, pCounter), Wlc_ObjId(pNew, pConst) );
|
|
Wlc_ObjAddFanins( pNew, pAdder, vFanins );
|
|
Wlc_ObjSetCo( pNew, pAdder, 1 );
|
|
|
|
// create new flop inputs
|
|
if ( vMemFanins )
|
|
Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
|
|
Wlc_NtkDupOneBuffer( pNew, p, pObj, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)), vFanins, 1 );
|
|
|
|
// create flop inputs for constraint objects
|
|
if ( vConstrs )
|
|
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 );
|
|
if ( p->pSpec )
|
|
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
|
|
//Wlc_NtkTransferNames( pNew, p );
|
|
Vec_IntFree( vFanins );
|
|
Vec_IntFreeP( &vNewObjs );
|
|
Wlc_NtkCleanMarks( p );
|
|
// derive topological order
|
|
pNew = Wlc_NtkDupDfs( pTemp = pNew, 0, 1 );
|
|
Wlc_NtkFree( pTemp );
|
|
return pNew;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Derives values of memory subsystem objects under the CEX.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
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;
|
|
Wlc_NtkForEachObjVec( vMemObjs, p, pObj, i )
|
|
{
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_MUX )
|
|
{
|
|
//Vec_IntPush( vMemFanins, Wlc_ObjFaninId0(pObj) );
|
|
pFanin = Wlc_ObjFanin0(p, pObj);
|
|
assert( Wlc_ObjRange(pFanin) == 1 );
|
|
Vec_IntWriteEntry( vFirstTotal, 3*i, (iFirstMemCi << 10) | Wlc_ObjRange(pFanin) );
|
|
iFirstMemCi += Wlc_ObjRange(pFanin);
|
|
nMemFanins++;
|
|
}
|
|
else if ( Wlc_ObjType(pObj) == WLC_OBJ_READ || Wlc_ObjType(pObj) == WLC_OBJ_WRITE )
|
|
{
|
|
Wlc_ObjForEachFanin( pObj, iFanin, k )
|
|
if ( k > 0 )
|
|
{
|
|
//Vec_IntPush( vMemFanins, iFanin );
|
|
pFanin = Wlc_NtkObj(p, iFanin);
|
|
Vec_IntWriteEntry( vFirstTotal, 3*i + k, (iFirstMemCi << 10) | Wlc_ObjRange(pFanin) );
|
|
iFirstMemCi += Wlc_ObjRange(pFanin);
|
|
nMemFanins++;
|
|
}
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_READ )
|
|
{
|
|
Vec_IntWriteEntry( vFirstTotal, 3*i + 2, (iFirstMemPi << 10) | Wlc_ObjRange(pObj) );
|
|
iFirstMemPi += Wlc_ObjRange(pObj);
|
|
}
|
|
}
|
|
}
|
|
assert( nMemFanins == Vec_IntSize(vMemFanins) );
|
|
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 outputs have been assigned in the previous timeframe
|
|
// assign primary inputs
|
|
Gia_ManForEachPi( pAbs, pObj, k )
|
|
pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
|
|
// simulate
|
|
Gia_ManForEachAnd( pAbs, pObj, k )
|
|
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
|
|
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
|
|
// transfer to combinational outputs
|
|
Gia_ManForEachCo( pAbs, pObj, k )
|
|
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
|
|
// transfer values to flop outputs
|
|
Gia_ManForEachRiRo( pAbs, pObjRi, pObjRo, k )
|
|
pObjRo->fMark0 = pObjRi->fMark0;
|
|
// at this point PIs and FOs area assigned according to this time-frame
|
|
// collect values
|
|
Vec_IntForEachEntry( vFirstTotal, Entry, k )
|
|
{
|
|
if ( Entry == 0 )
|
|
{
|
|
Vec_WrdWriteEntry( vRes, Vec_IntSize(vFirstTotal)*iFrame + k, ~(word)0 );
|
|
continue;
|
|
}
|
|
First = Entry >> 10;
|
|
assert( First < Gia_ManCiNum(pAbs) );
|
|
nBits = Entry & 0x3FF;
|
|
assert( nBits <= 64 );
|
|
Value = 0;
|
|
for ( b = 0; b < nBits; b++ )
|
|
if ( Gia_ManCi(pAbs, First+b)->fMark0 )
|
|
Value |= ((word)1) << b;
|
|
Vec_WrdWriteEntry( vRes, Vec_IntSize(vFirstTotal)*iFrame + k, Value );
|
|
}
|
|
return iBit;
|
|
}
|
|
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 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 the reason for failure in terms of memory values.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Wlc_NtkTrace_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int iFrame, Vec_Int_t * vMemObjs, Vec_Wrd_t * vValues, word ValueA, Vec_Int_t * vRes )
|
|
{
|
|
int iObj = Wlc_ObjId(p, pObj);
|
|
int iNum = Wlc_ObjCopy( p, iObj );
|
|
assert( iObj == Vec_IntEntry(vMemObjs, iNum) );
|
|
assert( iFrame >= 0 );
|
|
if ( Wlc_ObjIsPi(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);
|
|
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 << 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 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 << 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 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 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 );
|
|
assert( iObjLast == Vec_IntEntry(vMemObjs, iNumLast) );
|
|
assert( iObjFirst == Vec_IntEntry(vMemObjs, iNumFirst) );
|
|
pObjLast = Wlc_NtkObj(p, iObjLast);
|
|
pObjFirst = Wlc_NtkObj(p, iObjFirst);
|
|
assert( Wlc_ObjType(pObjLast) == WLC_OBJ_READ );
|
|
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) ); // 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_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, f, vMemObjs, vValues );
|
|
if ( Wlc_NtkTraceCheckConfict( p, vTrace, vMemObjs, vValues ) )
|
|
{
|
|
Vec_WecFree( vTraces );
|
|
return vTrace;
|
|
}
|
|
Vec_WecPushLevel( vTraces );
|
|
Vec_IntAppend( Vec_WecEntryLast(vTraces), vTrace );
|
|
Vec_IntFree( vTrace );
|
|
}
|
|
}
|
|
// check if there are any common read addresses
|
|
Vec_WecForEachLevel( vTraces, vTrace1, i )
|
|
Vec_WecForEachLevelStop( vTraces, vTrace2, f, i )
|
|
if ( Vec_IntEntry(vTrace1, 0) == Vec_IntEntry(vTrace2, 0) )
|
|
{
|
|
int iObj1 = Vec_IntEntryLast(vTrace1) >> 11;
|
|
int iFrm1 =(Vec_IntEntryLast(vTrace1) >> 1) & 0x3FF;
|
|
int iNum1 = Wlc_ObjCopy( p, iObj1 );
|
|
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, 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_IntForEachEntryStart( vTrace1, Entry, i, 1 )
|
|
Vec_IntPushUnique( vTrace, Entry );
|
|
Vec_IntForEachEntryStart( vTrace2, Entry, i, 1 )
|
|
Vec_IntPushUnique( vTrace, Entry );
|
|
Vec_WecFree( vTraces );
|
|
return vTrace;
|
|
}
|
|
}
|
|
Vec_WecFree( vTraces );
|
|
return NULL;
|
|
}
|
|
void Wlc_NtkPrintConflict( Wlc_Ntk_t * p, Vec_Int_t * vTrace )
|
|
{
|
|
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*************************************************************
|
|
|
|
Synopsis [Perform abstraction.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Wlc_Ntk_t * Wlc_NtkMemAbstractTest( Wlc_Ntk_t * p )
|
|
{
|
|
int iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits;
|
|
Vec_Int_t * vRefine;
|
|
Vec_Int_t * vMemObjs = Wlc_NtkCollectMemory( p, 0 );
|
|
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;
|
|
|
|
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 );
|
|
printf( "iFirstMemPi = %d iFirstCi = %d iFirstMemCi = %d nDcBits = %d\n", iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits );
|
|
|
|
Vec_IntFreeP( &vMemObjs );
|
|
Vec_IntFreeP( &vMemFanins );
|
|
return pNewFull;
|
|
}
|
|
|
|
int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbose, int fVerbose )
|
|
{
|
|
abctime clk = Abc_Clock();
|
|
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;
|
|
int RetValue = -1, iFirstMemPi, iFirstCi, iFirstMemCi, nDcBits, nIters;
|
|
|
|
vMemObjs = Wlc_NtkCollectMemory( p, 0 );
|
|
vMemFanins = Wlc_NtkCollectMemFanins( p, vMemObjs );
|
|
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, fVerbose );
|
|
|
|
pAbsFull = Wlc_NtkBitBlast( pNewFull, NULL );
|
|
assert( Gia_ManPiNum(pAbsFull) == iFirstCi + nDcBits );
|
|
Wlc_NtkFree( pNewFull );
|
|
|
|
// perform abstraction
|
|
for ( nIters = 0; nIters < nIterMax; nIters++ )
|
|
{
|
|
// set up parameters to run PDR
|
|
Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
|
|
Pdr_ManSetDefaultParams( pPdrPars );
|
|
pPdrPars->fUseAbs = 0; // use 'pdr -t' (on-the-fly abstraction)
|
|
pPdrPars->fVerbose = fVerbose;
|
|
|
|
// derive specific abstraction
|
|
pNew = Wlc_NtkAbstractMemory( p, vMemObjs, NULL, &iFirstMemPi, &iFirstCi, &iFirstMemCi, vRefines, vNodeFrames );
|
|
pAbs = Wlc_NtkBitBlast( pNew, NULL );
|
|
// simplify the AIG
|
|
//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, 1 );
|
|
Aig_ManStop( pTempAig );
|
|
pAbs = Gia_ManFromAigSimple( pAig );
|
|
Aig_ManStop( pAig );
|
|
|
|
// 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 );
|
|
|
|
if ( fDumpAbs )
|
|
{
|
|
char * pFileName = "mem_abs.aig";
|
|
Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
|
|
printf( "Iteration %3d: Dumped abstraction in file \"%s\" after finding CEX in frame %d.\n", nIters, pFileName, pCex ? pCex->iFrame : -1 );
|
|
}
|
|
|
|
// check if proved or undecided
|
|
if ( pCex == NULL )
|
|
{
|
|
assert( RetValue );
|
|
Gia_ManStop( pAbs );
|
|
break;
|
|
}
|
|
|
|
// analyze counter-example
|
|
vValues = Wlc_NtkConvertCex( vFirstTotal, pAbsFull, pCex, fVerbose );
|
|
Gia_ManStop( pAbs );
|
|
vRefine = Wlc_NtkFindConflict( p, vMemObjs, vValues, pCex->iFrame + 1 );
|
|
Vec_WrdFree( vValues );
|
|
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
|
|
Gia_ManStop( pAbsFull );
|
|
Vec_WecFree( vRefines );
|
|
Vec_IntFreeP( &vMemObjs );
|
|
Vec_IntFreeP( &vMemFanins );
|
|
Vec_IntFreeP( &vFirstTotal );
|
|
Vec_IntFreeP( &vNodeFrames );
|
|
|
|
// report the result
|
|
if ( fVerbose )
|
|
printf( "\n" );
|
|
printf( "Abstraction " );
|
|
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;
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Collect visited objects.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
int Wlc_NtkExploreMem2_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vCollect, int nFrames )
|
|
{
|
|
int k, iFanin, nVisited = 0;
|
|
if ( pObj->Mark == 0 )
|
|
return 0;
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_PI || (Wlc_ObjType(pObj) == WLC_OBJ_FO && nFrames == 0) )
|
|
{
|
|
Vec_IntPushTwo( vCollect, Wlc_ObjId(p, pObj), nFrames );
|
|
return 1;
|
|
}
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_FO )
|
|
return Wlc_NtkExploreMem2_rec( p, Wlc_ObjFo2Fi(p, pObj), vCollect, nFrames-1 );
|
|
Wlc_ObjForEachFanin( pObj, iFanin, k )
|
|
nVisited += Wlc_NtkExploreMem2_rec( p, Wlc_NtkObj(p, iFanin), vCollect, nFrames );
|
|
Vec_IntPushTwo( vCollect, Wlc_ObjId(p, pObj), nFrames );
|
|
return nVisited + 1;
|
|
}
|
|
void Wlc_NtkExploreMem2( Wlc_Ntk_t * p, int nFrames )
|
|
{
|
|
Wlc_Obj_t * pObj; int i, k, Entry, Frame, nVisited;
|
|
Vec_Int_t * vCollect = Vec_IntStart( 1000 );
|
|
Vec_Int_t * vMemObjsClean = Wlc_NtkCollectMemory( p, 1 );
|
|
Wlc_NtkCleanMarks( p );
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
|
|
pObj->Mark = 1;
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
|
|
{
|
|
if ( Wlc_ObjType(pObj) != WLC_OBJ_READ )
|
|
continue;
|
|
Vec_IntClear( vCollect );
|
|
nVisited = Wlc_NtkExploreMem2_rec( p, pObj, vCollect, nFrames );
|
|
printf( "Obj %6d : ", Wlc_ObjId(p, pObj) );
|
|
printf( "Visit = %6d ", nVisited );
|
|
printf( "Pair = %6d ", Vec_IntSize(vCollect)/2 );
|
|
if ( Vec_IntSize(vCollect)/2 < 10 )
|
|
Vec_IntForEachEntryDouble( vCollect, Entry, Frame, k )
|
|
printf( "%d(%d) ", Entry, Frame );
|
|
printf( "\n" );
|
|
}
|
|
Vec_IntFree( vMemObjsClean );
|
|
Vec_IntFree( vCollect );
|
|
Wlc_NtkCleanMarks( p );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Collect memory flops reachable.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Wlc_NtkExploreMem_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vCollect, int nFrames )
|
|
{
|
|
int k, iFanin;
|
|
if ( pObj->Mark == 0 )
|
|
return;
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_PI || (Wlc_ObjType(pObj) == WLC_OBJ_FO && nFrames == 0) )
|
|
{
|
|
Vec_IntPushUnique( vCollect, Wlc_ObjId(p, pObj) );
|
|
return;
|
|
}
|
|
if ( Wlc_ObjType(pObj) == WLC_OBJ_FO )
|
|
{
|
|
Wlc_NtkExploreMem_rec( p, Wlc_ObjFo2Fi(p, pObj), vCollect, nFrames-1 );
|
|
return;
|
|
}
|
|
Wlc_ObjForEachFanin( pObj, iFanin, k )
|
|
Wlc_NtkExploreMem_rec( p, Wlc_NtkObj(p, iFanin), vCollect, nFrames );
|
|
}
|
|
void Wlc_NtkExploreMem( Wlc_Ntk_t * p, int nFrames )
|
|
{
|
|
Wlc_Obj_t * pObj; int i, k, iObj;
|
|
Vec_Int_t * vCollect = Vec_IntStart( 1000 );
|
|
Vec_Int_t * vMemObjsClean = Wlc_NtkCollectMemory( p, 1 );
|
|
Wlc_NtkCleanMarks( p );
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
|
|
pObj->Mark = 1;
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
|
|
{
|
|
if ( Wlc_ObjType(pObj) != WLC_OBJ_READ )
|
|
continue;
|
|
Vec_IntClear( vCollect );
|
|
Wlc_NtkExploreMem_rec( p, pObj, vCollect, nFrames );
|
|
printf( "Read port %6d : ", Wlc_ObjId(p, pObj) );
|
|
printf( "Inputs = %6d ", Vec_IntSize(vCollect) );
|
|
Vec_IntForEachEntry( vCollect, iObj, k )
|
|
printf( "%d(%s) ", iObj, Wlc_ObjName(p, iObj) );
|
|
printf( "\n" );
|
|
}
|
|
Vec_IntFree( vMemObjsClean );
|
|
Vec_IntFree( vCollect );
|
|
Wlc_NtkCleanMarks( p );
|
|
}
|
|
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [For each READ find reachable CIs.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Vec_Int_t * Wlc_NtkFindReachablePiFo( Wlc_Ntk_t * p, Vec_Int_t * vMemObjsClean, int nFrames )
|
|
{
|
|
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
|
|
Wlc_Obj_t * pObjR, * pObjI, * pObj;
|
|
int i, j, k, f, fFanin;
|
|
Wlc_NtkForEachObj( p, pObj, i )
|
|
pObj->Mark2 = 0;
|
|
// go through read ports
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObjR, i ) if ( Wlc_ObjIsRead(pObjR) )
|
|
{
|
|
// go through memory CIs
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObjI, j ) if ( Wlc_ObjIsCi(pObjI) )
|
|
{
|
|
// propagate bit from CI to READ
|
|
pObjI->Mark2 = 1;
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, k )
|
|
{
|
|
if ( pObj == pObjI )
|
|
continue;
|
|
assert( pObj->Mark2 == 0 );
|
|
Wlc_ObjForEachFanin( pObj, fFanin, f )
|
|
pObj->Mark2 |= Wlc_NtkObj(p, fFanin)->Mark2;
|
|
}
|
|
if ( pObjR->Mark2 )
|
|
Vec_IntPushThree( vRes, Wlc_ObjId(p, pObjR), Wlc_ObjId(p, pObjI), -1 );
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, k )
|
|
pObj->Mark2 = 0;
|
|
}
|
|
}
|
|
Wlc_NtkForEachObj( p, pObj, i )
|
|
assert( pObj->Mark2 == 0 );
|
|
return vRes;
|
|
}
|
|
Vec_Int_t * Wlc_NtkExtractCisForThisRead( Vec_Int_t * vReachReadCi, int iRead )
|
|
{
|
|
int k;
|
|
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
|
|
for ( k = 0; k < Vec_IntSize(vReachReadCi)/3; k++ )
|
|
{
|
|
if ( iRead != Vec_IntEntry( vReachReadCi, 3*k ) )
|
|
continue;
|
|
Vec_IntPush( vRes, Vec_IntEntry( vReachReadCi, 3*k+1 ) );
|
|
Vec_IntPush( vRes, Vec_IntEntry( vReachReadCi, 3*k+2 ) );
|
|
}
|
|
return vRes;
|
|
}
|
|
Vec_Int_t * Wlc_NtkCollectOneType( Wlc_Ntk_t * p, Vec_Int_t * vMemObjsClean, int Type1, int Type2 )
|
|
{
|
|
Wlc_Obj_t * pObj; int i;
|
|
Vec_Int_t * vRes = Vec_IntAlloc( 100 );
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
|
|
if ( Wlc_ObjType(pObj) == Type1 || Wlc_ObjType(pObj) == Type2 )
|
|
Vec_IntPush( vRes, Wlc_ObjId(p, pObj) );
|
|
return vRes;
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Create memory constraints.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
void Wlc_NtkCreateMemoryConstr( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, Vec_Int_t * vMemObjsClean, Vec_Int_t * vReachReadCi )
|
|
{
|
|
Vec_Int_t * vReads = Wlc_NtkCollectOneType( p, vMemObjsClean, WLC_OBJ_READ, -1 );
|
|
Vec_Int_t * vObjCis = Wlc_NtkCollectOneType( p, vMemObjsClean, WLC_OBJ_PI, WLC_OBJ_FO );
|
|
Vec_Int_t * vFanins = Vec_IntAlloc( 10 );
|
|
Wlc_Obj_t * pObjR, * pObj, * pCond;
|
|
int i, k, iObjCi, iObjNew = -1;
|
|
// go through read ports
|
|
Wlc_NtkForEachObjVec( vReads, p, pObjR, i )
|
|
{
|
|
// ABC_READ ( .mem_in(mem_fi1), .addr(raddr), .data(read1) ) ;
|
|
// ABC_WRITE ( .mem_in(mem_fo1), .addr(waddr), .data(data), .mem_out(mem_fi1) ) ;
|
|
// initialize CI related to the read port
|
|
Vec_Int_t * vLocalCis = Wlc_NtkExtractCisForThisRead( vReachReadCi, Wlc_ObjId(p, pObjR) );
|
|
Wlc_NtkForEachObjVec( vObjCis, p, pObj, k )
|
|
Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), -1 );
|
|
Vec_IntForEachEntryDouble( vLocalCis, iObjCi, iObjNew, k )
|
|
Wlc_ObjSetCopy( p, iObjCi, iObjNew );
|
|
Vec_IntFree( vLocalCis );
|
|
// implement the nodes
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, k )
|
|
{
|
|
if ( Wlc_ObjIsRead(pObj) || Wlc_ObjIsCi(pObj) )
|
|
continue;
|
|
Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), -1 );
|
|
if ( Wlc_ObjIsWrite(pObj) )
|
|
{
|
|
if ( Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) == -1 )
|
|
continue;
|
|
if ( Wlc_ObjRange(pObjR) != Wlc_ObjRange(Wlc_ObjFanin2(p, pObj)) )
|
|
continue;
|
|
// create equality
|
|
pCond = Wlc_NtkObj( pNew, Wlc_ObjAlloc(pNew, WLC_OBJ_COMP_EQU, 0, 0, 0) );
|
|
Vec_IntFillTwo( vFanins, 2, Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObjR)), Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObj)) );
|
|
//printf( "%d : ", Wlc_ObjId(p,pObj) ), Vec_IntPrint( vFanins );
|
|
Wlc_ObjAddFanins( pNew, pCond, vFanins );
|
|
// create MUX
|
|
iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pObjR)-1, 0 );
|
|
Vec_IntFill( vFanins, 1, Wlc_ObjId(pNew, pCond) );
|
|
Vec_IntPush( vFanins, Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj)) );
|
|
Vec_IntPush( vFanins, Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) );
|
|
Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
|
|
}
|
|
else if ( Wlc_ObjIsMux(pObj) )
|
|
{
|
|
int iFanin0New = Wlc_ObjCopy(p, Wlc_ObjFaninId1(pObj));
|
|
int iFanin1New = Wlc_ObjCopy(p, Wlc_ObjFaninId2(pObj));
|
|
if ( iFanin0New == -1 || iFanin1New == -1 )
|
|
continue;
|
|
//Wlc_NtkPrintNode( pNew, Wlc_NtkObj(pNew, iFanin0New) );
|
|
assert( Wlc_ObjRange(pObjR) == Wlc_ObjRange(Wlc_NtkObj(pNew, iFanin0New)) );
|
|
assert( Wlc_ObjRange(pObjR) == Wlc_ObjRange(Wlc_NtkObj(pNew, iFanin1New)) );
|
|
iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_MUX, 0, Wlc_ObjRange(pObjR)-1, 0 );
|
|
Vec_IntFill( vFanins, 1, Wlc_ObjCopy(p, Wlc_ObjFaninId0(pObj)) );
|
|
Vec_IntPush( vFanins, iFanin0New );
|
|
Vec_IntPush( vFanins, iFanin1New );
|
|
Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
|
|
}
|
|
else if ( Wlc_ObjIsBuf(pObj) )
|
|
{
|
|
iObjNew = Wlc_ObjCopy( p, Wlc_ObjFaninId0(pObj) );
|
|
if ( iObjNew == -1 )
|
|
continue;
|
|
}
|
|
else assert( 0 );
|
|
Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), iObjNew );
|
|
}
|
|
// extract fanin
|
|
iObjNew = Wlc_ObjCopy( p, Wlc_ObjFaninId0(pObjR) );
|
|
assert( iObjNew != -1 );
|
|
Vec_IntFill( vFanins, 1, iObjNew );
|
|
// add it as buffer fanin
|
|
iObjNew = Wlc_ObjCopy( p, Wlc_ObjId(p, pObjR) );
|
|
assert( Wlc_NtkObj(pNew, iObjNew)->Type == WLC_OBJ_BUF );
|
|
Wlc_ObjAddFanins( pNew, Wlc_NtkObj(pNew, iObjNew), vFanins );
|
|
}
|
|
Wlc_NtkForEachObjVec( vObjCis, p, pObj, k )
|
|
Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), -1 );
|
|
Vec_IntFree( vFanins );
|
|
Vec_IntFree( vReads );
|
|
Vec_IntFree( vObjCis );
|
|
}
|
|
|
|
/**Function*************************************************************
|
|
|
|
Synopsis [Perform abstraction.]
|
|
|
|
Description []
|
|
|
|
SideEffects []
|
|
|
|
SeeAlso []
|
|
|
|
***********************************************************************/
|
|
Wlc_Ntk_t * Wlc_NtkAbstractMem( Wlc_Ntk_t * p, int nFrames, int fVerbose )
|
|
{
|
|
Vec_Int_t * vMemObjsAll = Wlc_NtkCollectMemory( p, 0 );
|
|
Vec_Int_t * vMemObjsClean = Wlc_NtkCollectMemory( p, 1 );
|
|
Vec_Int_t * vReachReadCi = Wlc_NtkFindReachablePiFo( p, vMemObjsClean, nFrames );
|
|
Wlc_Ntk_t * pNew, * pTemp;
|
|
Wlc_Obj_t * pObj;
|
|
Vec_Int_t * vFanins = Vec_IntAlloc( 100 );
|
|
int i, Po0, Po1, iObjNew;
|
|
|
|
assert( nFrames == 0 );
|
|
|
|
// mark memory nodes
|
|
Wlc_NtkCleanMarks( p );
|
|
Wlc_NtkForEachObjVec( vMemObjsAll, p, pObj, i )
|
|
pObj->Mark = 1;
|
|
|
|
// start new network
|
|
Wlc_NtkCleanCopy( p );
|
|
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc + Vec_IntSize(vMemObjsClean) * nFrames * 10 );
|
|
pNew->fSmtLib = p->fSmtLib;
|
|
pNew->fAsyncRst = p->fAsyncRst;
|
|
pNew->fMemPorts = p->fMemPorts;
|
|
pNew->fEasyFfs = p->fEasyFfs;
|
|
pNew->vInits = Vec_IntAlloc( 100 );
|
|
|
|
// duplicate PIs
|
|
Wlc_NtkForEachPi( p, pObj, i )
|
|
if ( !pObj->Mark )
|
|
Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
|
|
|
|
// create new PIs
|
|
assert( Vec_IntSize(vReachReadCi) % 3 == 0 );
|
|
for ( i = 0; i < Vec_IntSize(vReachReadCi)/3; i++ )
|
|
{
|
|
pObj = Wlc_NtkObj( p, Vec_IntEntry( vReachReadCi, 3*i ) );
|
|
assert( Wlc_ObjIsRead(pObj) );
|
|
iObjNew = Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_PI, vFanins );
|
|
Vec_IntWriteEntry( vReachReadCi, 3*i+2, iObjNew );
|
|
}
|
|
//Vec_IntPrint( vReachReadCi );
|
|
|
|
// duplicate flop outputs
|
|
Wlc_NtkForEachCi( p, pObj, i )
|
|
if ( !Wlc_ObjIsPi(pObj) && !pObj->Mark )
|
|
{
|
|
Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
|
|
Vec_IntPush( pNew->vInits, Vec_IntEntry(p->vInits, i-Wlc_NtkPiNum(p)) );
|
|
}
|
|
|
|
/*
|
|
// create flops for memory objects
|
|
Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
|
|
for ( k = 0; k < nFrames; k++ )
|
|
Wlc_NtkDupOneObject( pNew, p, pObj, WLC_OBJ_FO, vFanins );
|
|
*/
|
|
|
|
// create buffers for read ports
|
|
Wlc_NtkForEachObjVec( vMemObjsClean, p, pObj, i )
|
|
{
|
|
if ( !Wlc_ObjIsRead(pObj) )
|
|
continue;
|
|
iObjNew = Wlc_ObjAlloc( pNew, WLC_OBJ_BUF, pObj->Signed, pObj->End, pObj->Beg );
|
|
Wlc_ObjSetCopy( p, Wlc_ObjId(p, pObj), iObjNew );
|
|
}
|
|
|
|
// duplicate objects
|
|
Wlc_NtkForEachObj( p, pObj, i )
|
|
if ( !Wlc_ObjIsCi(pObj) && !pObj->Mark )
|
|
Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
|
|
|
|
// create memory constraints
|
|
Wlc_NtkCreateMemoryConstr( pNew, p, vMemObjsClean, vReachReadCi );
|
|
|
|
// create outpus
|
|
if ( Vec_IntSize(&p->vPoPairs) )
|
|
{
|
|
// create miter for the PO pairs
|
|
Vec_IntForEachEntryDouble( &p->vPoPairs, Po0, Po1, i )
|
|
{
|
|
int iCopy0 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po0)));
|
|
int iCopy1 = Wlc_ObjCopy(p, Wlc_ObjId(p, Wlc_NtkPo(p, Po1)));
|
|
int iObj = Wlc_ObjAlloc( pNew, WLC_OBJ_COMP_NOTEQU, 0, 0, 0 );
|
|
Wlc_Obj_t * pObjNew = Wlc_NtkObj( pNew, iObj );
|
|
Vec_IntFillTwo( vFanins, 1, iCopy0, iCopy1 );
|
|
Wlc_ObjAddFanins( pNew, pObjNew, vFanins );
|
|
Wlc_ObjSetCo( pNew, pObjNew, 0 );
|
|
}
|
|
printf( "Memory abstraction created %d miter outputs.\n", Wlc_NtkPoNum(pNew) );
|
|
Wlc_NtkForEachCo( p, pObj, i )
|
|
if ( pObj->fIsFi && !pObj->Mark )
|
|
Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
|
|
}
|
|
else
|
|
{
|
|
// duplicate POs
|
|
Wlc_NtkForEachPo( p, pObj, i )
|
|
if ( !pObj->Mark )
|
|
Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
|
|
// duplicate FIs
|
|
Wlc_NtkForEachCo( p, pObj, i )
|
|
if ( !Wlc_ObjIsPo(pObj) && !pObj->Mark )
|
|
Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
|
|
}
|
|
|
|
/*
|
|
// create new flop inputs
|
|
Wlc_NtkForEachObjVec( vMemFanins, p, pObj, i )
|
|
for ( k = 0; k < nFrames; k++ )
|
|
Wlc_NtkDupOneBuffer( pNew, p, pObj, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj))-(nFrames-1-k), vFanins, 1 );
|
|
*/
|
|
|
|
// append init states
|
|
pNew->pInits = Wlc_PrsConvertInitValues( pNew );
|
|
if ( p->pSpec )
|
|
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
|
|
if ( Wlc_NtkHasNameId(p) )
|
|
Wlc_NtkTransferNames( pNew, p );
|
|
Vec_IntFree( vFanins );
|
|
Vec_IntFree( vMemObjsAll );
|
|
Vec_IntFree( vMemObjsClean );
|
|
Vec_IntFree( vReachReadCi );
|
|
Wlc_NtkCleanMarks( p );
|
|
// derive topological order
|
|
//printf( "Objects before = %d.\n", Wlc_NtkObjNum(pNew) );
|
|
pNew = Wlc_NtkDupDfs( pTemp = pNew, 0, 1 );
|
|
Wlc_NtkFree( pTemp );
|
|
//printf( "Objects after = %d.\n", Wlc_NtkObjNum(pNew) );
|
|
return pNew;
|
|
}
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
ABC_NAMESPACE_IMPL_END
|
|
|