summaryrefslogtreecommitdiffstats
path: root/src/base/wlc
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/wlc')
-rw-r--r--src/base/wlc/module.make3
-rw-r--r--src/base/wlc/wlc.h58
-rw-r--r--src/base/wlc/wlcAbc.c181
-rw-r--r--src/base/wlc/wlcAbs.c701
-rw-r--r--src/base/wlc/wlcAbs2.c410
-rw-r--r--src/base/wlc/wlcBlast.c51
-rw-r--r--src/base/wlc/wlcCom.c949
-rw-r--r--src/base/wlc/wlcNtk.c570
-rw-r--r--src/base/wlc/wlcReadSmt.c336
-rw-r--r--src/base/wlc/wlcReadVer.c5
-rw-r--r--src/base/wlc/wlcShow.c337
-rw-r--r--src/base/wlc/wlcSim.c22
-rw-r--r--src/base/wlc/wlcUif.c290
-rw-r--r--src/base/wlc/wlcWriteVer.c2
14 files changed, 3473 insertions, 442 deletions
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index 5a95a63f..c4330264 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -1,4 +1,5 @@
SRC += src/base/wlc/wlcAbs.c \
+ src/base/wlc/wlcAbs2.c \
src/base/wlc/wlcAbc.c \
src/base/wlc/wlcBlast.c \
src/base/wlc/wlcCom.c \
@@ -7,6 +8,8 @@ SRC += src/base/wlc/wlcAbs.c \
src/base/wlc/wlcReadSmt.c \
src/base/wlc/wlcReadVer.c \
src/base/wlc/wlcSim.c \
+ src/base/wlc/wlcShow.c \
src/base/wlc/wlcStdin.c \
+ src/base/wlc/wlcUif.c \
src/base/wlc/wlcWin.c \
src/base/wlc/wlcWriteVer.c
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 1df3e5e9..686d9f00 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -140,6 +140,7 @@ struct Wlc_Ntk_t_
int nObjs[WLC_OBJ_NUMBER]; // counter of objects of each type
int nAnds[WLC_OBJ_NUMBER]; // counter of AND gates after blasting
int fSmtLib; // the network comes from an SMT-LIB file
+ int nAssert; // the number of asserts
// memory for objects
Wlc_Obj_t * pObjs;
int iObj;
@@ -156,6 +157,23 @@ struct Wlc_Ntk_t_
Vec_Int_t vTravIds; // trav IDs of the objects
Vec_Int_t vCopies; // object first bits
Vec_Int_t vBits; // object mapping into AIG nodes
+ Vec_Int_t vLevels; // object levels
+ Vec_Int_t vRefs; // object reference counters
+};
+
+typedef struct Wlc_Par_t_ Wlc_Par_t;
+struct Wlc_Par_t_
+{
+ int nBitsAdd; // adder bit-width
+ int nBitsMul; // multiplier bit-widht
+ int nBitsMux; // MUX bit-width
+ int nBitsFlop; // flop bit-width
+ int nIterMax; // the max number of iterations
+ int fXorOutput; // XOR outputs of word-level miter
+ int fCheckClauses; // Check clauses in the reloaded trace
+ int fPushClauses; // Push clauses in the reloaded trace
+ int fVerbose; // verbose output
+ int fPdrVerbose; // verbose output
};
static inline int Wlc_NtkObjNum( Wlc_Ntk_t * p ) { return p->iObj - 1; }
@@ -205,6 +223,8 @@ static inline int Wlc_ObjSign( Wlc_Obj_t * p )
static inline int * Wlc_ObjConstValue( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_CONST); return Wlc_ObjFanins(p); }
static inline int Wlc_ObjTableId( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_TABLE); return p->Fanins[1]; }
static inline word * Wlc_ObjTable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return (word *)Vec_PtrEntry( p->vTables, Wlc_ObjTableId(pObj) ); }
+static inline int Wlc_ObjLevelId( Wlc_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vLevels, iObj ); }
+static inline int Wlc_ObjLevel( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return Wlc_ObjLevelId( p, Wlc_ObjId(p, pObj) ); }
static inline void Wlc_NtkCleanCopy( Wlc_Ntk_t * p ) { Vec_IntFill( &p->vCopies, p->nObjsAlloc, 0 ); }
static inline int Wlc_NtkHasCopy( Wlc_Ntk_t * p ) { return Vec_IntSize( &p->vCopies ) > 0; }
@@ -217,7 +237,8 @@ static inline int Wlc_NtkHasNameId( Wlc_Ntk_t * p )
static inline void Wlc_ObjSetNameId( Wlc_Ntk_t * p, int iObj, int i ) { Vec_IntWriteEntry( &p->vNameIds, iObj, i ); }
static inline int Wlc_ObjNameId( Wlc_Ntk_t * p, int iObj ) { return Vec_IntEntry( &p->vNameIds, iObj ); }
-static inline Wlc_Obj_t * Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkCoNum(p) - Wlc_NtkCiNum(p) + Wlc_ObjCiId(pObj)); }
+static inline Wlc_Obj_t * Wlc_ObjFo2Fi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { assert( pObj->Type == WLC_OBJ_FO ); return Wlc_NtkCo(p, Wlc_NtkPoNum(p) + Wlc_ObjCiId(pObj) - Wlc_NtkPiNum(p)); }
+static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId ) { return iCoId < Wlc_NtkPoNum(p) ? Wlc_NtkPo(p, iCoId) : Wlc_NtkCi(p, Wlc_NtkPiNum(p) + iCoId - Wlc_NtkPoNum(p)); }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
@@ -229,6 +250,8 @@ static inline Wlc_Obj_t * Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
#define Wlc_NtkForEachObj( p, pObj, i ) \
for ( i = 1; (i < Wlc_NtkObjNumMax(p)) && (((pObj) = Wlc_NtkObj(p, i)), 1); i++ )
+#define Wlc_NtkForEachObjReverse( p, pObj, i ) \
+ for ( i = Wlc_NtkObjNumMax(p) - 1; (i > 0) && (((pObj) = Wlc_NtkObj(p, i)), 1); i-- )
#define Wlc_NtkForEachObjVec( vVec, p, pObj, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && (((pObj) = Wlc_NtkObj(p, Vec_IntEntry(vVec, i))), 1); i++ )
#define Wlc_NtkForEachPi( p, pPi, i ) \
@@ -255,16 +278,17 @@ static inline Wlc_Obj_t * Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
////////////////////////////////////////////////////////////////////////
/*=== wlcAbs.c ========================================================*/
-extern int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 );
-extern Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
-extern Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
-extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
-extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
+extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
+extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
+/*=== wlcAbs2.c ========================================================*/
+extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
/*=== wlcBlast.c ========================================================*/
extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nRange, int fGiaSimple, int fAddOutputs, int fBooth );
/*=== wlcCom.c ========================================================*/
extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
/*=== wlcNtk.c ========================================================*/
+extern void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars );
+extern char * Wlc_ObjTypeName( Wlc_Obj_t * p );
extern Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc );
extern int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
extern int Wlc_ObjCreate( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg, Vec_Int_t * vFanins );
@@ -274,13 +298,25 @@ extern char * Wlc_ObjName( Wlc_Ntk_t * p, int iObj );
extern void Wlc_ObjUpdateType( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int Type );
extern void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins );
extern void Wlc_NtkFree( Wlc_Ntk_t * p );
+extern int Wlc_NtkCreateLevels( Wlc_Ntk_t * p );
+extern int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p );
+extern int Wlc_NtkCountRealPis( Wlc_Ntk_t * p );
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 fVerbose );
-extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p );
+extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose );
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 );
+extern Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops );
+extern void Wlc_NtkCleanMarks( Wlc_Ntk_t * p );
+extern void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis );
+extern void Wlc_NtkProfileCones( Wlc_Ntk_t * p );
extern Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p );
+extern void Wlc_NtkShortNames( Wlc_Ntk_t * p );
+extern int Wlc_NtkDcFlopNum( Wlc_Ntk_t * p );
+extern void Wlc_NtkSetRefs( Wlc_Ntk_t * p );
+extern int Wlc_NtkCountObjBits( Wlc_Ntk_t * p, Vec_Int_t * vPisNew );
/*=== wlcReadSmt.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit, int fOldParser, int fPrintTree );
extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName, int fOldParser, int fPrintTree );
@@ -291,6 +327,12 @@ extern void Wlc_NtkDeleteSim( Vec_Ptr_t * p );
extern int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
/*=== wlcReadVer.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr );
+/*=== wlcUif.c ========================================================*/
+extern int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 );
+extern Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p );
+extern Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p );
+extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes );
+extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
/*=== wlcWin.c =============================================================*/
extern void Wlc_WinProfileArith( Wlc_Ntk_t * p );
/*=== wlcWriteVer.c ========================================================*/
diff --git a/src/base/wlc/wlcAbc.c b/src/base/wlc/wlcAbc.c
index 0bf27f7b..1836f4ed 100644
--- a/src/base/wlc/wlcAbc.c
+++ b/src/base/wlc/wlcAbc.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
+void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
{
Wlc_Obj_t * pObj;
int i, k, nNum, nRange, nBits = 0;
@@ -53,7 +53,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
nRange = Wlc_ObjRange(pObj);
for ( k = 0; k < nRange; k++ )
{
- nNum = Vec_IntEntry(vInv, nBits + k);
+ nNum = Vec_IntEntry(vCounts, nBits + k);
if ( nNum )
break;
}
@@ -65,7 +65,7 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
for ( k = 0; k < nRange; k++ )
{
- nNum = Vec_IntEntry( vInv, nBits + k );
+ nNum = Vec_IntEntry( vCounts, nBits + k );
if ( nNum == 0 )
continue;
printf( " [%d] -> %d", k, nNum );
@@ -73,8 +73,8 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
printf( "\n");
nBits += nRange;
}
- //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
- assert( Vec_IntSize(vInv) == nBits );
+ //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+ assert( Vec_IntSize(vCounts) == nBits );
}
/**Function*************************************************************
@@ -88,8 +88,14 @@ void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose )
+Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
{
+ extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
+ extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );
+
+ Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
+ Vec_Str_t * vSop = Pdr_InvPrintStr( vInv, vCounts );
+
Wlc_Obj_t * pObj;
int i, k, nNum, nRange, nBits = 0;
Abc_Ntk_t * pMainNtk = NULL;
@@ -98,46 +104,69 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
// start the network
pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
// duplicate the name and the spec
- pMainNtk->pName = Extra_UtilStrsav(pNtk->pName);
+ pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv");
// create primary inputs
- Wlc_NtkForEachCi( pNtk, pObj, i )
+ if ( pNtk == NULL )
{
- if ( pObj->Type != WLC_OBJ_FO )
- continue;
- nRange = Wlc_ObjRange(pObj);
- for ( k = 0; k < nRange; k++ )
+ int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) );
+ Vec_IntForEachEntry( vCounts, Entry, i )
{
- nNum = Vec_IntEntry(vInv, nBits + k);
- if ( nNum )
- break;
+ if ( Entry == 0 )
+ continue;
+ pMainObj = Abc_NtkCreatePi( pMainNtk );
+ sprintf( Buffer, "pi%d", i );
+ Abc_ObjAssignName( pMainObj, Buffer, NULL );
}
- if ( k == nRange )
+ if ( Abc_NtkPiNum(pMainNtk) != nInputs )
{
- nBits += nRange;
- continue;
+ printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" );
+ Abc_NtkDelete( pMainNtk );
+ return NULL;
}
- //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
- for ( k = 0; k < nRange; k++ )
+ }
+ else
+ {
+ Wlc_NtkForEachCi( pNtk, pObj, i )
{
- nNum = Vec_IntEntry( vInv, nBits + k );
- if ( nNum == 0 )
+ if ( pObj->Type != WLC_OBJ_FO )
continue;
- //printf( " [%d] -> %d", k, nNum );
- pMainObj = Abc_NtkCreatePi( pMainNtk );
- sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
- Abc_ObjAssignName( pMainObj, Buffer, NULL );
+ nRange = Wlc_ObjRange(pObj);
+ for ( k = 0; k < nRange; k++ )
+ {
+ nNum = Vec_IntEntry(vCounts, nBits + k);
+ if ( nNum )
+ break;
+ }
+ if ( k == nRange )
+ {
+ nBits += nRange;
+ continue;
+ }
+ //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
+ for ( k = 0; k < nRange; k++ )
+ {
+ nNum = Vec_IntEntry( vCounts, nBits + k );
+ if ( nNum == 0 )
+ continue;
+ //printf( " [%d] -> %d", k, nNum );
+ pMainObj = Abc_NtkCreatePi( pMainNtk );
+ sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
+ Abc_ObjAssignName( pMainObj, Buffer, NULL );
+ }
+ //printf( "\n");
+ nBits += nRange;
}
- //printf( "\n");
- nBits += nRange;
}
- //printf( "%d %d\n", Vec_IntSize(vInv), nBits );
- assert( Vec_IntSize(vInv) == nBits );
+ //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
+ assert( pNtk == NULL || Vec_IntSize(vCounts) == nBits );
// create node
pMainObj = Abc_NtkCreateNode( pMainNtk );
Abc_NtkForEachPi( pMainNtk, pMainTemp, i )
Abc_ObjAddFanin( pMainObj, pMainTemp );
pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );
+ Vec_IntFree( vCounts );
+ Vec_StrFree( vSop );
// create PO
pMainTemp = Abc_NtkCreatePo( pMainNtk );
Abc_ObjAddFanin( pMainTemp, pMainObj );
@@ -145,6 +174,98 @@ Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop,
return pMainNtk;
}
+/**Function*************************************************************
+
+ Synopsis [Translate current network into an invariant.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia )
+{
+ int nRegs = Gia_ManRegNum(pGia);
+ Vec_Int_t * vRes = NULL;
+ if ( Abc_NtkPoNum(pNtk) != 1 )
+ printf( "The number of outputs is other than 1.\n" );
+ else if ( Abc_NtkNodeNum(pNtk) != 1 )
+ printf( "The number of internal nodes is other than 1.\n" );
+ else
+ {
+ Abc_Nam_t * pNames = NULL;
+ Abc_Obj_t * pFanin, * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
+ char * pName, * pCube, * pSop = (char *)pNode->pData;
+ Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) );
+ int i, k, Value, nLits, Counter = 0;
+ if ( pGia->vNamesIn )
+ {
+ // hash the names
+ pNames = Abc_NamStart( 100, 16 );
+ Vec_PtrForEachEntry( char *, pGia->vNamesIn, pName, i )
+ {
+ Value = Abc_NamStrFindOrAdd( pNames, pName, NULL );
+ assert( Value == i+1 );
+ //printf( "%s(%d) ", pName, i );
+ }
+ //printf( "\n" );
+ }
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+ assert( Abc_ObjIsCi(pFanin) );
+ pName = Abc_ObjName(pFanin);
+ if ( pNames )
+ {
+ Value = Abc_NamStrFind(pNames, pName) - 1 - Gia_ManPiNum(pGia);
+ if ( Value < 0 )
+ {
+ if ( Counter++ == 0 )
+ printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i );
+ Value = i;
+ }
+ }
+ else
+ {
+ for ( k = (int)strlen(pName)-1; k >= 0; k-- )
+ if ( pName[k] < '0' || pName[k] > '9' )
+ break;
+ if ( k == (int)strlen(pName)-1 )
+ {
+ if ( Counter++ == 0 )
+ printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i );
+ Value = i;
+ }
+ else
+ Value = atoi(pName + k + 1);
+ }
+ Vec_IntPush( vFanins, Value );
+ }
+ if ( Counter )
+ printf( "Cannot read names for %d inputs of the invariant.\n", Counter );
+ if ( pNames )
+ Abc_NamStop( pNames );
+ assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) );
+ vRes = Vec_IntAlloc( 1000 );
+ Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) );
+ Abc_SopForEachCube( pSop, Abc_ObjFaninNum(pNode), pCube )
+ {
+ nLits = 0;
+ Abc_CubeForEachVar( pCube, Value, k )
+ if ( Value != '-' )
+ nLits++;
+ Vec_IntPush( vRes, nLits );
+ Abc_CubeForEachVar( pCube, Value, k )
+ if ( Value != '-' )
+ Vec_IntPush( vRes, Abc_Var2Lit(Vec_IntEntry(vFanins, k), (int)Value == '0') );
+ }
+ Vec_IntPush( vRes, nRegs );
+ Vec_IntFree( vFanins );
+ }
+ return vRes;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 73ff7328..e33424f7 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -8,7 +8,7 @@
Synopsis [Abstraction for word-level networks.]
- Author [Alan Mishchenko]
+ Author [Yen-Sheng Ho, Alan Mishchenko]
Affiliation [UC Berkeley]
@@ -19,6 +19,10 @@
***********************************************************************/
#include "wlc.h"
+#include "proof/pdr/pdr.h"
+#include "proof/pdr/pdrInt.h"
+#include "aig/gia/giaAig.h"
+#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
@@ -26,161 +30,330 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
+extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap );
+extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis [Check if two objects have the same input/output signatures.]
+ Synopsis [Mark operators that meet the abstraction criteria.]
- Description []
+ Description [This procedure returns the array of objects (vLeaves) that
+ should be abstracted because of their high bit-width. It uses input array (vUnmark)
+ to not abstract those objects that have been refined in the previous rounds.]
SideEffects []
SeeAlso []
***********************************************************************/
-int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 )
+static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
{
- Wlc_Obj_t * pFanin, * pFanin2; int k;
- if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) )
- return 0;
- if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) )
- return 0;
- if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) )
- return 0;
- for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
+ Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+ Wlc_Obj_t * pObj; int i, Count[4] = {0};
+ Wlc_NtkForEachObj( p, pObj, i )
{
- pFanin = Wlc_ObjFanin(p, pObj, k);
- pFanin2 = Wlc_ObjFanin(p, pObj2, k);
- if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) )
- return 0;
- if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) )
- return 0;
+ if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away
+ continue;
+ if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[0]++;
+ continue;
+ }
+ if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[1]++;
+ continue;
+ }
+ if ( pObj->Type == WLC_OBJ_MUX )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[2]++;
+ continue;
+ }
+ if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[3]++;
+ continue;
+ }
}
- return 1;
+ if ( fVerbose )
+ printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
+ return vLeaves;
}
/**Function*************************************************************
- Synopsis [Collect IDs of the multipliers.]
+ Synopsis [Marks nodes to be included in the abstracted network.]
- Description []
+ Description [Marks all objects that will be included in the abstracted model.
+ Stops at the objects (vLeaves) that are abstracted away. Returns three arrays:
+ a subset of original PIs (vPisOld), a subset of pseudo-PIs (vPisNew) and the
+ set of flops present as flops in the abstracted network.]
SideEffects []
SeeAlso []
***********************************************************************/
-Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p )
+static void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
{
- Wlc_Obj_t * pObj; int i;
- Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
+ int i, iFanin;
+ if ( pObj->Mark )
+ return;
+ pObj->Mark = 1;
+ if ( Vec_BitEntry(vLeaves, Wlc_ObjId(p, pObj)) )
+ {
+ assert( !Wlc_ObjIsPi(pObj) );
+ Vec_IntPush( vPisNew, Wlc_ObjId(p, pObj) );
+ return;
+ }
+ if ( Wlc_ObjIsCi(pObj) )
+ {
+ if ( Wlc_ObjIsPi(pObj) )
+ Vec_IntPush( vPisOld, Wlc_ObjId(p, pObj) );
+ else
+ Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) );
+ return;
+ }
+ Wlc_ObjForEachFanin( pObj, iFanin, i )
+ Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vPisOld, vPisNew, vFlops );
+}
+static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+{
+ Wlc_Obj_t * pObj;
+ int i, Count = 0;
+ Wlc_NtkCleanMarks( p );
+ Wlc_NtkForEachCo( p, pObj, i )
+ Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops );
+
+/*
+ Vec_IntClear(vFlops);
+ Wlc_NtkForEachCi( p, pObj, i ) {
+ if ( !Wlc_ObjIsPi(pObj) ) {
+ Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) );
+ pObj->Mark = 1;
+ }
+ }
+*/
+
+ Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+ Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops );
Wlc_NtkForEachObj( p, pObj, i )
- if ( pObj->Type == WLC_OBJ_ARI_MULTI )
- Vec_IntPush( vBoxIds, i );
- if ( Vec_IntSize( vBoxIds ) > 0 )
- return vBoxIds;
- Vec_IntFree( vBoxIds );
- return NULL;
+ Count += pObj->Mark;
+// printf( "Collected %d old PIs, %d new PIs, %d flops, and %d other objects.\n",
+// Vec_IntSize(vPisOld), Vec_IntSize(vPisNew), Vec_IntSize(vFlops),
+// Count - Vec_IntSize(vPisOld) - Vec_IntSize(vPisNew) - Vec_IntSize(vFlops) );
+ Vec_IntSort( vPisOld, 0 );
+ Vec_IntSort( vPisNew, 0 );
+ Vec_IntSort( vFlops, 0 );
+ Wlc_NtkCleanMarks( p );
}
/**Function*************************************************************
- Synopsis [Returns all pairs of uifable multipliers.]
+ Synopsis [Derive word-level abstracted model based on the parameter values.]
- Description []
+ Description [Retuns the word-level abstracted network and the set of pseudo-PIs
+ (vPisNew), which were created during abstraction. If the abstraction is
+ satisfiable, some of the pseudo-PIs will be un-abstracted. These pseudo-PIs
+ and their MFFC cones will be listed in the array (vUnmark), which will
+ force the abstraction to not stop at these pseudo-PIs in the future.]
SideEffects []
SeeAlso []
***********************************************************************/
-Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p )
+static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, Vec_Int_t ** pvFlops, int fVerbose )
{
- Vec_Int_t * vMultis = Wlc_NtkCollectMultipliers( p );
- Vec_Int_t * vPairs = Vec_IntAlloc( 2 );
- Wlc_Obj_t * pObj, * pObj2; int i, k;
- // iterate through unique pairs
- Wlc_NtkForEachObjVec( vMultis, p, pObj, i )
- Wlc_NtkForEachObjVec( vMultis, p, pObj2, k )
- {
- if ( k == i )
- break;
- if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) )
- {
- Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) );
- Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) );
- }
- }
- Vec_IntFree( vMultis );
- if ( Vec_IntSize( vPairs ) > 0 )
- return vPairs;
- Vec_IntFree( vPairs );
- return NULL;
+ Wlc_Ntk_t * pNtkNew = NULL;
+ Vec_Int_t * vPisOld = Vec_IntAlloc( 100 );
+ Vec_Int_t * vPisNew = Vec_IntAlloc( 100 );
+ Vec_Int_t * vFlops = Vec_IntAlloc( 100 );
+ Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars, vUnmark, fVerbose );
+ Wlc_NtkAbsMarkNodes( p, vLeaves, vPisOld, vPisNew, vFlops );
+ Vec_BitFree( vLeaves );
+ pNtkNew = Wlc_NtkDupDfsAbs( p, vPisOld, vPisNew, vFlops );
+ Vec_IntFree( vPisOld );
+ if ( pvFlops )
+ *pvFlops = vFlops;
+ else
+ Vec_IntFree( vFlops );
+ if ( pvPisNew )
+ *pvPisNew = vPisNew;
+ else
+ Vec_IntFree( vPisNew );
+ return pNtkNew;
}
+/**Function*************************************************************
+
+ Synopsis [Find what objects need to be un-abstracted.]
+
+ Description [Returns a subset of pseudo-PIs (vPisNew), which will be
+ prevented from being abstracted in the future rounds of abstraction.
+ The AIG manager (pGia) is a bit-level view of the abstracted model.
+ The counter-example (pCex) is used to find waht PPIs to refine.]
+
+ SideEffects []
+ SeeAlso []
+
+***********************************************************************/
+static Vec_Int_t * Wlc_NtkAbsRefinement( Wlc_Ntk_t * p, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vPisNew )
+{
+ Vec_Int_t * vRefine = Vec_IntAlloc( 100 );
+ Abc_Cex_t * pCexCare;
+ Wlc_Obj_t * pObj;
+ // count the number of bit-level PPIs and map them into word-level objects they were derived from
+ int f, i, b, nRealPis, nPpiBits = 0;
+ Vec_Int_t * vMap = Vec_IntStartFull( pCex->nPis );
+ Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+ for ( b = 0; b < Wlc_ObjRange(pObj); b++ )
+ Vec_IntWriteEntry( vMap, nPpiBits++, Wlc_ObjId(p, pObj) );
+ // since PPIs are ordered last, the previous bits are real PIs
+ nRealPis = pCex->nPis - nPpiBits;
+ // find the care-set
+ pCexCare = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, 1, 0, 0 );
+ assert( pCexCare->nPis == pCex->nPis );
+ // detect care PPIs
+ for ( f = 0; f <= pCexCare->iFrame; f++ )
+ for ( i = nRealPis; i < pCexCare->nPis; i++ )
+ if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
+ Vec_IntPushUniqueOrder( vRefine, Vec_IntEntry(vMap, i-nRealPis) );
+ Abc_CexFree( pCexCare );
+ Vec_IntFree( vMap );
+ if ( Vec_IntSize(vRefine) == 0 )// real CEX
+ Vec_IntFreeP( &vRefine );
+ return vRefine;
+}
/**Function*************************************************************
- Synopsis [Abstracts nodes by replacing their outputs with new PIs.]
+ Synopsis [Mark MFFC cones of the un-abstracted objects.]
- Description [If array is NULL, abstract all multipliers.]
+ Description [The MFFC cones of the objects in vRefine are traversed
+ and all their nodes are marked in vUnmark.]
SideEffects []
SeeAlso []
***********************************************************************/
-Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
+static int Wlc_NtkNodeDeref_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
{
- Vec_Int_t * vNodes = vNodesInit;
- Wlc_Ntk_t * pNew;
- Wlc_Obj_t * pObj;
- int i, k, iObj, iFanin;
- // get multipliers if not given
- if ( vNodes == NULL )
- vNodes = Wlc_NtkCollectMultipliers( p );
- if ( vNodes == NULL )
- return NULL;
- // mark nodes
- Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
- pObj->Mark = 1;
- // iterate through the nodes in the DFS order
- Wlc_NtkCleanCopy( p );
- Wlc_NtkForEachObj( p, pObj, i )
+ int i, Fanin, Counter = 1;
+ if ( Wlc_ObjIsCi(pNode) )
+ return 0;
+ Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+ Wlc_ObjForEachFanin( pNode, Fanin, i )
{
- if ( i == Vec_IntSize(&p->vCopies) )
- break;
- if ( pObj->Mark ) {
- // clean
- pObj->Mark = 0;
- // add fresh PI with the same number of bits
- iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 );
- }
- else {
- // update fanins
- Wlc_ObjForEachFanin( pObj, iFanin, k )
- Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
- // node to remain
- iObj = i;
- }
- Wlc_ObjSetCopy( p, i, iObj );
+ Vec_IntAddToEntry( &p->vRefs, Fanin, -1 );
+ if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+ Counter += Wlc_NtkNodeDeref_rec( p, Wlc_NtkObj(p, Fanin), vUnmark );
}
- // POs do not change in this procedure
- if ( vNodes != vNodesInit )
- Vec_IntFree( vNodes );
- // reconstruct topological order
- pNew = Wlc_NtkDupDfs( p );
- Wlc_NtkTransferNames( pNew, p );
- return pNew;
+ return Counter;
+}
+static int Wlc_NtkNodeRef_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode )
+{
+ int i, Fanin, Counter = 1;
+ if ( Wlc_ObjIsCi(pNode) )
+ return 0;
+ Wlc_ObjForEachFanin( pNode, Fanin, i )
+ {
+ if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+ Counter += Wlc_NtkNodeRef_rec( p, Wlc_NtkObj(p, Fanin) );
+ Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
+ }
+ return Counter;
+}
+static int Wlc_NtkMarkMffc( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
+{
+ int Count1, Count2;
+ // if this is a flop output, compute MFFC of the corresponding flop input
+ while ( Wlc_ObjIsCi(pNode) )
+ {
+ Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+ pNode = Wlc_ObjFo2Fi(p, pNode);
+ }
+ assert( !Wlc_ObjIsCi(pNode) );
+ // dereference the node (and set the bits in vUnmark)
+ Count1 = Wlc_NtkNodeDeref_rec( p, pNode, vUnmark );
+ // reference it back
+ Count2 = Wlc_NtkNodeRef_rec( p, pNode );
+ assert( Count1 == Count2 );
+ return Count1;
+}
+static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark )
+{
+ Wlc_Obj_t * pObj; int i, nNodes = 0;
+ if ( Vec_IntSize(&p->vRefs) == 0 )
+ Wlc_NtkSetRefs( p );
+ Wlc_NtkForEachObjVec( vRefine, p, pObj, i )
+ nNodes += Wlc_NtkMarkMffc( p, pObj, vUnmark );
+ return nNodes;
}
/**Function*************************************************************
- Synopsis [Adds UIF constraints to node pairs and updates POs.]
+ Synopsis [Computes the map for remapping flop IDs used in the clauses.]
+
+ Description [Takes the original network (Wlc_Ntk_t) and the array of word-level
+ flops used in the old abstraction (vFfOld) and those used in the new abstraction
+ (vFfNew). Returns the integer map, which remaps every binary flop found
+ in the old abstraction into a binary flop found in the new abstraction.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkFlopsRemap( Wlc_Ntk_t * p, Vec_Int_t * vFfOld, Vec_Int_t * vFfNew )
+{
+ Vec_Int_t * vMap = Vec_IntAlloc( 1000 ); // the resulting map
+ Vec_Int_t * vMapFfNew2Bit1 = Vec_IntAlloc( 1000 ); // first binary bit of each new word-level flop
+ int i, b, iFfOld, iFfNew, iBit1New, nBits = 0;
+ // map object IDs of old flops into their flop indexes
+ Vec_Int_t * vMapFfObj2FfId = Vec_IntStartFull( Wlc_NtkObjNumMax(p) );
+ Vec_IntForEachEntry( vFfNew, iFfNew, i )
+ Vec_IntWriteEntry( vMapFfObj2FfId, iFfNew, i );
+ // map each new flop index into its first bit
+ Vec_IntForEachEntry( vFfNew, iFfNew, i )
+ {
+ Wlc_Obj_t * pObj = Wlc_NtkObj( p, iFfNew );
+ int nRange = Wlc_ObjRange( pObj );
+ Vec_IntPush( vMapFfNew2Bit1, nBits );
+ nBits += nRange;
+ }
+ assert( Vec_IntSize(vMapFfNew2Bit1) == Vec_IntSize(vFfNew) );
+ // remap old binary flops into new binary flops
+ Vec_IntForEachEntry( vFfOld, iFfOld, i )
+ {
+ Wlc_Obj_t * pObj = Wlc_NtkObj( p, iFfOld );
+ int nRange = Wlc_ObjRange( pObj );
+ iFfNew = Vec_IntEntry( vMapFfObj2FfId, iFfOld );
+ assert( iFfNew >= 0 ); // every old flop should be present in the new abstraction
+ // find the first bit of this new flop
+ iBit1New = Vec_IntEntry( vMapFfNew2Bit1, iFfNew );
+ for ( b = 0; b < nRange; b++ )
+ Vec_IntPush( vMap, iBit1New + b );
+ }
+ Vec_IntFree( vMapFfNew2Bit1 );
+ Vec_IntFree( vMapFfObj2FfId );
+ return vMap;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs PDR with word-level abstraction.]
Description []
@@ -189,98 +362,266 @@ Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
SeeAlso []
***********************************************************************/
-Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
+int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
- Vec_Int_t * vPairs = vPairsInit;
- Wlc_Ntk_t * pNew;
- Wlc_Obj_t * pObj, * pObj2;
- Vec_Int_t * vUifConstrs, * vCompares, * vFanins;
- int i, k, iObj, iObj2, iObjNew, iObjNew2;
- int iFanin, iFanin2, iFaninNew;
- // get multiplier pairs if not given
- if ( vPairs == NULL )
- vPairs = Wlc_NtkFindUifableMultiplierPairs( p );
- if ( vPairs == NULL )
- return NULL;
- // sanity checks
- assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 );
- // iterate through node pairs
- vFanins = Vec_IntAlloc( 100 );
- vCompares = Vec_IntAlloc( 100 );
- vUifConstrs = Vec_IntAlloc( 100 );
- Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i )
+ abctime clk = Abc_Clock();
+ abctime pdrClk;
+ Pdr_Man_t * pPdr;
+ Vec_Vec_t * vClauses = NULL;
+ Vec_Int_t * vFfOld = NULL, * vFfNew = NULL, * vMap = NULL;
+ int nIters, nNodes, nDcFlops, RetValue = -1, nGiaFfNumOld = -1;
+ // start the bitmap to mark objects that cannot be abstracted because of refinement
+ // currently, this bitmap is empty because abstraction begins without refinement
+ Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+ // set up parameters to run PDR
+ Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
+ Pdr_ManSetDefaultParams( pPdrPars );
+ pPdrPars->fVerbose = pPars->fPdrVerbose;
+ pPdrPars->fVeryVerbose = 0;
+
+ // perform refinement iterations
+ for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{
- // get two nodes
- pObj = Wlc_NtkObj( p, iObj );
- pObj2 = Wlc_NtkObj( p, iObj2 );
- assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) );
- // create fanin comparator nodes
- Vec_IntClear( vCompares );
- Wlc_ObjForEachFanin( pObj, iFanin, k )
+ Aig_Man_t * pAig;
+ Abc_Cex_t * pCex;
+ Vec_Int_t * vPisNew, * vRefine;
+ Gia_Man_t * pGia, * pTemp;
+ Wlc_Ntk_t * pAbs;
+
+ if ( pPars->fVerbose )
+ printf( "\nIteration %d:\n", nIters );
+
+ // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+ pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose );
+ pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
+
+ // map old flops into new flops
+ if ( vFfOld )
{
- iFanin2 = Wlc_ObjFaninId( pObj2, k );
- Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 );
- iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins );
- Vec_IntPush( vCompares, iFaninNew );
- // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to
- // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
- pObj = Wlc_NtkObj( p, iObj );
+ assert( nGiaFfNumOld >= 0 );
+ vMap = Wlc_NtkFlopsRemap( p, vFfOld, vFfNew );
+ //Vec_IntPrint( vMap );
+ // if reset flop was added in the previous iteration, it will be added again in this iteration
+ // remap the last flop (reset flop) into the last flop (reset flop) of the current AIG
+ if ( Vec_IntSize(vMap) + 1 == nGiaFfNumOld )
+ Vec_IntPush( vMap, Gia_ManRegNum(pGia)-1 );
+ assert( Vec_IntSize(vMap) == nGiaFfNumOld );
+ Vec_IntFreeP( &vFfOld );
}
- // concatenate fanin comparators
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares );
- // create reduction-OR node
- Vec_IntFill( vFanins, 1, iObjNew );
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins );
- // craete output comparator node
- Vec_IntFillTwo( vFanins, 2, iObj, iObj2 );
- iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins );
- // create implication node (iObjNew is already complemented above)
- Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 );
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins );
- // save the constraint
- Vec_IntPush( vUifConstrs, iObjNew );
- }
- // derive the AND of the UIF contraints
- assert( Vec_IntSize(vUifConstrs) > 0 );
- if ( Vec_IntSize(vUifConstrs) == 1 )
- iObjNew = Vec_IntEntry( vUifConstrs, 0 );
- else
- {
- // concatenate
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs );
- // create reduction-AND node
- Vec_IntFill( vFanins, 1, iObjNew );
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins );
+ ABC_SWAP( Vec_Int_t *, vFfOld, vFfNew );
+ nGiaFfNumOld = Gia_ManRegNum(pGia);
+
+ // if the abstraction has flops with DC-init state,
+ // new PIs were introduced by bit-blasting at the end of the PI list
+ // here we move these variables to be *before* PPIs, because
+ // PPIs are supposed to be at the end of the PI list for refinement
+ nDcFlops = Wlc_NtkDcFlopNum(pAbs);
+ if ( nDcFlops > 0 ) // DC-init flops are present
+ {
+ pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
+ Gia_ManStop( pTemp );
+ }
+ // if the word-level outputs have to be XORs, this is a place to do it
+ if ( pPars->fXorOutput )
+ {
+ pGia = Gia_ManTransformMiter2( pTemp = pGia );
+ Gia_ManStop( pTemp );
+ }
+ if ( pPars->fVerbose )
+ {
+ printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) );
+ Gia_ManPrintStats( pGia, NULL );
+ }
+ Wlc_NtkFree( pAbs );
+
+ // try to prove abstracted GIA by converting it to AIG and calling PDR
+ pAig = Gia_ManToAigSimple( pGia );
+
+ pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
+ pdrClk = Abc_Clock();
+
+ if ( vClauses ) {
+ assert( Vec_VecSize( vClauses) >= 2 );
+ IPdr_ManRestore( pPdr, vClauses, vMap );
+ }
+ Vec_IntFreeP( &vMap );
+
+ RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
+ pPdr->tTotal += Abc_Clock() - pdrClk;
+
+ pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
+
+ // consider outcomes
+ if ( pCex == NULL )
+ {
+ assert( RetValue ); // proved or undecided
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ Pdr_ManStop( pPdr );
+ Aig_ManStop( pAig );
+ break;
+ }
+
+ // perform refinement
+ vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ if ( vRefine == NULL ) // real CEX
+ {
+ Abc_CexFree( pCex ); // return CEX in the future
+ Pdr_ManStop( pPdr );
+ Aig_ManStop( pAig );
+ break;
+ }
+
+ // spurious CEX, continue solving
+ vClauses = IPdr_ManSaveClauses( pPdr, 0 );
+
+ Pdr_ManStop( pPdr );
+
+ // update the set of objects to be un-abstracted
+ nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
+ if ( pPars->fVerbose )
+ printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+ Vec_IntFree( vRefine );
+ Abc_CexFree( pCex );
+ Aig_ManStop( pAig );
}
- // update each PO to point to the new node
- Wlc_NtkForEachPo( p, pObj, i )
+
+ Vec_IntFreeP( &vFfOld );
+ Vec_BitFree( vUnmark );
+ // report the result
+ if ( pPars->fVerbose )
+ printf( "\n" );
+ printf( "Abstraction " );
+ if ( RetValue == 0 )
+ printf( "resulted in a real CEX" );
+ else if ( RetValue == 1 )
+ printf( "is successfully proved" );
+ else
+ printf( "timed out" );
+ printf( " after %d iterations. ", nIters );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs abstraction.]
+
+ Description [Derives initial abstraction based on user-specified
+ parameter values, which tell what is the smallest bit-width of a
+ primitive that is being abstracted away. Currently only add/sub,
+ mul/div, mux, and flop are supported with individual parameters.
+ The second step is to refine the initial abstraction until the
+ point when the property is proved.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+ abctime clk = Abc_Clock();
+ int nIters, nNodes, nDcFlops, RetValue = -1;
+ // start the bitmap to mark objects that cannot be abstracted because of refinement
+ // currently, this bitmap is empty because abstraction begins without refinement
+ Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+ // set up parameters to run PDR
+ Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
+ Pdr_ManSetDefaultParams( pPdrPars );
+ //pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
+ //pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
+ //pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
+ //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
+ pPdrPars->fVerbose = pPars->fPdrVerbose;
+ pPdrPars->fVeryVerbose = 0;
+ // perform refinement iterations
+ for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{
- iObj = Wlc_ObjId(p, pObj);
- Vec_IntFillTwo( vFanins, 2, iObj, iObjNew );
- iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins );
- // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to
- // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
- pObj = Wlc_NtkObj( p, iObj );
- // update PO/CO arrays
- assert( Vec_IntEntry(&p->vPos, i) == iObj );
- assert( Vec_IntEntry(&p->vCos, i) == iObj );
- Vec_IntWriteEntry( &p->vPos, i, iObjNew );
- Vec_IntWriteEntry( &p->vCos, i, iObjNew );
- // transfer the PO attribute
- Wlc_NtkObj(p, iObjNew)->fIsPo = 1;
- assert( pObj->fIsPo );
- pObj->fIsPo = 0;
+ Aig_Man_t * pAig;
+ Abc_Cex_t * pCex;
+ Vec_Int_t * vPisNew, * vRefine;
+ Gia_Man_t * pGia, * pTemp;
+ Wlc_Ntk_t * pAbs;
+
+ if ( pPars->fVerbose )
+ printf( "\nIteration %d:\n", nIters );
+
+ // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+ pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, NULL, pPars->fVerbose );
+ pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
+
+ // if the abstraction has flops with DC-init state,
+ // new PIs were introduced by bit-blasting at the end of the PI list
+ // here we move these variables to be *before* PPIs, because
+ // PPIs are supposed to be at the end of the PI list for refinement
+ nDcFlops = Wlc_NtkDcFlopNum(pAbs);
+ if ( nDcFlops > 0 ) // DC-init flops are present
+ {
+ pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
+ Gia_ManStop( pTemp );
+ }
+ // if the word-level outputs have to be XORs, this is a place to do it
+ if ( pPars->fXorOutput )
+ {
+ pGia = Gia_ManTransformMiter2( pTemp = pGia );
+ Gia_ManStop( pTemp );
+ }
+ if ( pPars->fVerbose )
+ {
+ printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) );
+ Gia_ManPrintStats( pGia, NULL );
+ }
+ Wlc_NtkFree( pAbs );
+
+ // try to prove abstracted GIA by converting it to AIG and calling PDR
+ pAig = Gia_ManToAigSimple( pGia );
+ RetValue = Pdr_ManSolve( pAig, pPdrPars );
+ pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
+ Aig_ManStop( pAig );
+
+ // consider outcomes
+ if ( pCex == NULL )
+ {
+ assert( RetValue ); // proved or undecided
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ break;
+ }
+
+ // perform refinement
+ vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ if ( vRefine == NULL ) // real CEX
+ {
+ Abc_CexFree( pCex ); // return CEX in the future
+ break;
+ }
+
+ // update the set of objects to be un-abstracted
+ nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
+ if ( pPars->fVerbose )
+ printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+ Vec_IntFree( vRefine );
+ Abc_CexFree( pCex );
}
- // cleanup
- Vec_IntFree( vUifConstrs );
- Vec_IntFree( vCompares );
- Vec_IntFree( vFanins );
- if ( vPairs != vPairsInit )
- Vec_IntFree( vPairs );
- // reconstruct topological order
- pNew = Wlc_NtkDupDfs( p );
- Wlc_NtkTransferNames( pNew, p );
- return pNew;
+ Vec_BitFree( vUnmark );
+ // report the result
+ if ( pPars->fVerbose )
+ printf( "\n" );
+ printf( "Abstraction " );
+ if ( RetValue == 0 )
+ printf( "resulted in a real CEX" );
+ else if ( RetValue == 1 )
+ printf( "is successfully proved" );
+ else
+ printf( "timed out" );
+ printf( " after %d iterations. ", nIters );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return RetValue;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/wlc/wlcAbs2.c b/src/base/wlc/wlcAbs2.c
new file mode 100644
index 00000000..9bccdf62
--- /dev/null
+++ b/src/base/wlc/wlcAbs2.c
@@ -0,0 +1,410 @@
+/**CFile****************************************************************
+
+ FileName [wlcAbs2.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Verilog parser.]
+
+ Synopsis [Abstraction for word-level networks.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - August 22, 2014.]
+
+ Revision [$Id: wlcAbs2.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+#include "proof/pdr/pdr.h"
+#include "aig/gia/giaAig.h"
+#include "sat/bmc/bmc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Mark operators that meet the abstraction criteria.]
+
+ Description [This procedure returns the array of objects (vLeaves) that
+ should be abstracted because of their high bit-width. It uses input array (vUnmark)
+ to not abstract those objects that have been refined in the previous rounds.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
+{
+ Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+ Wlc_Obj_t * pObj; int i, Count[4] = {0};
+ Wlc_NtkForEachObj( p, pObj, i )
+ {
+ if ( vUnmark && Vec_BitEntry(vUnmark, i) ) // not allow this object to be abstracted away
+ continue;
+ if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[0]++;
+ continue;
+ }
+ if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[1]++;
+ continue;
+ }
+ if ( pObj->Type == WLC_OBJ_MUX )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[2]++;
+ continue;
+ }
+ if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+ {
+ if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[3]++;
+ continue;
+ }
+ }
+ if ( fVerbose )
+ printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
+ return vLeaves;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks nodes to be included in the abstracted network.]
+
+ Description [Marks all objects that will be included in the abstracted model.
+ Stops at the objects (vLeaves) that are abstracted away. Returns three arrays:
+ a subset of original PIs (vPisOld), a subset of pseudo-PIs (vPisNew) and the
+ set of flops present as flops in the abstracted network.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+{
+ int i, iFanin;
+ if ( pObj->Mark )
+ return;
+ pObj->Mark = 1;
+ if ( Vec_BitEntry(vLeaves, Wlc_ObjId(p, pObj)) )
+ {
+ assert( !Wlc_ObjIsPi(pObj) );
+ Vec_IntPush( vPisNew, Wlc_ObjId(p, pObj) );
+ return;
+ }
+ if ( Wlc_ObjIsCi(pObj) )
+ {
+ if ( Wlc_ObjIsPi(pObj) )
+ Vec_IntPush( vPisOld, Wlc_ObjId(p, pObj) );
+ else
+ Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) );
+ return;
+ }
+ Wlc_ObjForEachFanin( pObj, iFanin, i )
+ Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vPisOld, vPisNew, vFlops );
+}
+static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+{
+ Wlc_Obj_t * pObj;
+ int i, Count = 0;
+ Wlc_NtkCleanMarks( p );
+ Wlc_NtkForEachCo( p, pObj, i )
+ Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops );
+ Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+ Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops );
+ Wlc_NtkForEachObj( p, pObj, i )
+ Count += pObj->Mark;
+// printf( "Collected %d old PIs, %d new PIs, %d flops, and %d other objects.\n",
+// Vec_IntSize(vPisOld), Vec_IntSize(vPisNew), Vec_IntSize(vFlops),
+// Count - Vec_IntSize(vPisOld) - Vec_IntSize(vPisNew) - Vec_IntSize(vFlops) );
+ Vec_IntSort( vPisOld, 0 );
+ Vec_IntSort( vPisNew, 0 );
+ Vec_IntSort( vFlops, 0 );
+ Wlc_NtkCleanMarks( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derive word-level abstracted model based on the parameter values.]
+
+ Description [Retuns the word-level abstracted network and the set of pseudo-PIs
+ (vPisNew), which were created during abstraction. If the abstraction is
+ satisfiable, some of the pseudo-PIs will be un-abstracted. These pseudo-PIs
+ and their MFFC cones will be listed in the array (vUnmark), which will
+ force the abstraction to not stop at these pseudo-PIs in the future.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, Vec_Int_t ** pvPisNew, int fVerbose )
+{
+ Wlc_Ntk_t * pNtkNew = NULL;
+ Vec_Int_t * vPisOld = Vec_IntAlloc( 100 );
+ Vec_Int_t * vPisNew = Vec_IntAlloc( 100 );
+ Vec_Int_t * vFlops = Vec_IntAlloc( 100 );
+ Vec_Bit_t * vLeaves = Wlc_NtkAbsMarkOpers( p, pPars, vUnmark, fVerbose );
+ Wlc_NtkAbsMarkNodes( p, vLeaves, vPisOld, vPisNew, vFlops );
+ Vec_BitFree( vLeaves );
+ pNtkNew = Wlc_NtkDupDfsAbs( p, vPisOld, vPisNew, vFlops );
+ Vec_IntFree( vPisOld );
+ Vec_IntFree( vFlops );
+ if ( pvPisNew )
+ *pvPisNew = vPisNew;
+ else
+ Vec_IntFree( vPisNew );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Find what objects need to be un-abstracted.]
+
+ Description [Returns a subset of pseudo-PIs (vPisNew), which will be
+ prevented from being abstracted in the future rounds of abstraction.
+ The AIG manager (pGia) is a bit-level view of the abstracted model.
+ The counter-example (pCex) is used to find waht PPIs to refine.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static Vec_Int_t * Wlc_NtkAbsRefinement( Wlc_Ntk_t * p, Gia_Man_t * pGia, Abc_Cex_t * pCex, Vec_Int_t * vPisNew )
+{
+ Vec_Int_t * vRefine = Vec_IntAlloc( 100 );
+ Abc_Cex_t * pCexCare;
+ Wlc_Obj_t * pObj;
+ // count the number of bit-level PPIs and map them into word-level objects they were derived from
+ int f, i, b, nRealPis, nPpiBits = 0;
+ Vec_Int_t * vMap = Vec_IntStartFull( pCex->nPis );
+ Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+ for ( b = 0; b < Wlc_ObjRange(pObj); b++ )
+ Vec_IntWriteEntry( vMap, nPpiBits++, Wlc_ObjId(p, pObj) );
+ // since PPIs are ordered last, the previous bits are real PIs
+ nRealPis = pCex->nPis - nPpiBits;
+ // find the care-set
+ pCexCare = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, 1, 0, 0 );
+ assert( pCexCare->nPis == pCex->nPis );
+ // detect care PPIs
+ for ( f = 0; f <= pCexCare->iFrame; f++ )
+ for ( i = nRealPis; i < pCexCare->nPis; i++ )
+ if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
+ Vec_IntPushUniqueOrder( vRefine, Vec_IntEntry(vMap, i-nRealPis) );
+ Abc_CexFree( pCexCare );
+ Vec_IntFree( vMap );
+ if ( Vec_IntSize(vRefine) == 0 )// real CEX
+ Vec_IntFreeP( &vRefine );
+ return vRefine;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Mark MFFC cones of the un-abstracted objects.]
+
+ Description [The MFFC cones of the objects in vRefine are traversed
+ and all their nodes are marked in vUnmark.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static int Wlc_NtkNodeDeref_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
+{
+ int i, Fanin, Counter = 1;
+ if ( Wlc_ObjIsCi(pNode) )
+ return 0;
+ Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+ Wlc_ObjForEachFanin( pNode, Fanin, i )
+ {
+ Vec_IntAddToEntry( &p->vRefs, Fanin, -1 );
+ if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+ Counter += Wlc_NtkNodeDeref_rec( p, Wlc_NtkObj(p, Fanin), vUnmark );
+ }
+ return Counter;
+}
+static int Wlc_NtkNodeRef_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pNode )
+{
+ int i, Fanin, Counter = 1;
+ if ( Wlc_ObjIsCi(pNode) )
+ return 0;
+ Wlc_ObjForEachFanin( pNode, Fanin, i )
+ {
+ if ( Vec_IntEntry(&p->vRefs, Fanin) == 0 )
+ Counter += Wlc_NtkNodeRef_rec( p, Wlc_NtkObj(p, Fanin) );
+ Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
+ }
+ return Counter;
+}
+static int Wlc_NtkMarkMffc( Wlc_Ntk_t * p, Wlc_Obj_t * pNode, Vec_Bit_t * vUnmark )
+{
+ int Count1, Count2;
+ // if this is a flop output, compute MFFC of the corresponding flop input
+ while ( Wlc_ObjIsCi(pNode) )
+ {
+ Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pNode), 1 );
+ pNode = Wlc_ObjFo2Fi(p, pNode);
+ }
+ assert( !Wlc_ObjIsCi(pNode) );
+ // dereference the node (and set the bits in vUnmark)
+ Count1 = Wlc_NtkNodeDeref_rec( p, pNode, vUnmark );
+ // reference it back
+ Count2 = Wlc_NtkNodeRef_rec( p, pNode );
+ assert( Count1 == Count2 );
+ return Count1;
+}
+static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark )
+{
+ Wlc_Obj_t * pObj; int i, nNodes = 0;
+ if ( Vec_IntSize(&p->vRefs) == 0 )
+ Wlc_NtkSetRefs( p );
+ Wlc_NtkForEachObjVec( vRefine, p, pObj, i )
+ nNodes += Wlc_NtkMarkMffc( p, pObj, vUnmark );
+ return nNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs abstraction.]
+
+ Description [Derives initial abstraction based on user-specified
+ parameter values, which tell what is the smallest bit-width of a
+ primitive that is being abstracted away. Currently only add/sub,
+ mul/div, mux, and flop are supported with individual parameters.
+ The second step is to refine the initial abstraction until the
+ point when the property is proved.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+ abctime clk = Abc_Clock();
+ int nIters, nNodes, nDcFlops, RetValue = -1;
+ // start the bitmap to mark objects that cannot be abstracted because of refinement
+ // currently, this bitmap is empty because abstraction begins without refinement
+ Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+ // set up parameters to run PDR
+ Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
+ Pdr_ManSetDefaultParams( pPdrPars );
+ pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
+ pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
+ pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
+ //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
+ pPdrPars->fVerbose = pPars->fPdrVerbose;
+ // perform refinement iterations
+ for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
+ {
+ Aig_Man_t * pAig;
+ Abc_Cex_t * pCex;
+ Vec_Int_t * vPisNew, * vRefine;
+ Gia_Man_t * pGia, * pTemp;
+ Wlc_Ntk_t * pAbs;
+
+ if ( pPars->fVerbose )
+ printf( "\nIteration %d:\n", nIters );
+
+ // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+ pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
+ pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
+
+ // if the abstraction has flops with DC-init state,
+ // new PIs were introduced by bit-blasting at the end of the PI list
+ // here we move these variables to be *before* PPIs, because
+ // PPIs are supposed to be at the end of the PI list for refinement
+ nDcFlops = Wlc_NtkDcFlopNum(pAbs);
+ if ( nDcFlops > 0 ) // DC-init flops are present
+ {
+ pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
+ Gia_ManStop( pTemp );
+ }
+ // if the word-level outputs have to be XORs, this is a place to do it
+ if ( pPars->fXorOutput )
+ {
+ pGia = Gia_ManTransformMiter2( pTemp = pGia );
+ Gia_ManStop( pTemp );
+ }
+ if ( pPars->fVerbose )
+ {
+ printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) );
+ Gia_ManPrintStats( pGia, NULL );
+ }
+ Wlc_NtkFree( pAbs );
+
+ // try to prove abstracted GIA by converting it to AIG and calling PDR
+ pAig = Gia_ManToAigSimple( pGia );
+ RetValue = Pdr_ManSolve( pAig, pPdrPars );
+ pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
+ Aig_ManStop( pAig );
+
+ // consider outcomes
+ if ( pCex == NULL )
+ {
+ assert( RetValue ); // proved or undecided
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ break;
+ }
+
+ // perform refinement
+ vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+ Gia_ManStop( pGia );
+ Vec_IntFree( vPisNew );
+ if ( vRefine == NULL ) // real CEX
+ {
+ Abc_CexFree( pCex ); // return CEX in the future
+ break;
+ }
+
+ // update the set of objects to be un-abstracted
+ nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
+ if ( pPars->fVerbose )
+ printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+ Vec_IntFree( vRefine );
+ Abc_CexFree( pCex );
+ }
+ Vec_BitFree( vUnmark );
+ // report the result
+ if ( pPars->fVerbose )
+ printf( "\n" );
+ printf( "Abstraction " );
+ if ( RetValue == 0 )
+ printf( "resulted in a real CEX" );
+ else if ( RetValue == 1 )
+ printf( "is successfully proved" );
+ else
+ printf( "timed out" );
+ printf( " after %d iterations. ", nIters );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index ec3b040d..f4de8ee6 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -643,6 +643,41 @@ void Wlc_IntInsert( Vec_Int_t * vProd, Vec_Int_t * vLevel, int Node, int Level )
Vec_IntInsert( vProd, i + 1, Node );
Vec_IntInsert( vLevel, i + 1, Level );
}
+void Wlc_BlastPrintMatrix( Gia_Man_t * p, Vec_Wec_t * vProds )
+{
+ int fVerbose = 0;
+ Vec_Int_t * vSupp = Vec_IntAlloc( 100 );
+ Vec_Wrd_t * vTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vLevel; word Truth;
+ int i, k, iLit;
+ Vec_WecForEachLevel( vProds, vLevel, i )
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(iLit))) )
+ Vec_IntPushUnique( vSupp, Abc_Lit2Var(iLit) );
+ printf( "Booth partial products: %d pps, %d unique, %d nodes.\n",
+ Vec_WecSizeSize(vProds), Vec_IntSize(vSupp), Gia_ManAndNum(p) );
+ Vec_IntPrint( vSupp );
+
+ if ( fVerbose )
+ Vec_WecForEachLevel( vProds, vLevel, i )
+ Vec_IntForEachEntry( vLevel, iLit, k )
+ {
+ printf( "Obj = %4d : ", Abc_Lit2Var(iLit) );
+ printf( "Compl = %d ", Abc_LitIsCompl(iLit) );
+ printf( "Rank = %2d ", i );
+ Truth = Gia_ObjComputeTruth6Cis( p, iLit, vSupp, vTemp );
+ Extra_PrintHex( stdout, (unsigned*)&Truth, Vec_IntSize(vSupp) );
+ if ( Vec_IntSize(vSupp) == 4 ) printf( " " );
+ if ( Vec_IntSize(vSupp) == 3 ) printf( " " );
+ if ( Vec_IntSize(vSupp) <= 2 ) printf( " " );
+ printf( " " );
+ Vec_IntPrint( vSupp );
+ if ( k == Vec_IntSize(vLevel)-1 )
+ printf( "\n" );
+ }
+ Vec_IntFree( vSupp );
+ Vec_WrdFree( vTemp );
+}
void Wlc_BlastReduceMatrix( Gia_Man_t * pNew, Vec_Wec_t * vProds, Vec_Wec_t * vLevels, Vec_Int_t * vRes )
{
Vec_Int_t * vLevel, * vProd;
@@ -812,6 +847,7 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
Vec_WecPush( vLevels, k, 0 );
}
//Vec_WecPrint( vProds, 0 );
+ //Wlc_BlastPrintMatrix( pNew, vProds );
//printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) );
Wlc_BlastReduceMatrix( pNew, vProds, vLevels, vRes );
@@ -836,6 +872,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
int fVerbose = 0;
int fUseOldMultiplierBlasting = 0;
+ int fSkipBitRange = 0;
Tim_Man_t * pManTime = NULL;
Gia_Man_t * pTemp, * pNew, * pExtra = NULL;
Wlc_Obj_t * pObj;
@@ -1381,7 +1418,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
}
else
{
- pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 1 );
+ pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 0 );
Gia_ManDupRemapLiterals( vBits, pTemp );
Gia_ManStop( pTemp );
}
@@ -1412,7 +1449,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
nRange = Wlc_ObjRange( pObj );
- if ( nRange == 1 )
+ if ( fSkipBitRange && nRange == 1 )
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) );
else
for ( k = 0; k < nRange; k++ )
@@ -1439,7 +1476,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
nRange = Wlc_ObjRange( pObj );
- if ( nRange == 1 )
+ if ( fSkipBitRange && nRange == 1 )
Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsav(pName) );
else
for ( k = 0; k < nRange; k++ )
@@ -1462,7 +1499,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
nRange = Wlc_ObjRange( pObj );
- if ( nRange == 1 )
+ if ( fSkipBitRange && nRange == 1 )
Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
else
for ( k = 0; k < nRange; k++ )
@@ -1477,7 +1514,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
nRange = Wlc_ObjRange( pObj );
- if ( nRange == 1 )
+ if ( fSkipBitRange && nRange == 1 )
Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
else
for ( k = 0; k < nRange; k++ )
@@ -1496,7 +1533,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
nRange = Wlc_ObjRange( pObj );
- if ( nRange == 1 )
+ if ( fSkipBitRange && nRange == 1 )
Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
else
for ( k = 0; k < nRange; k++ )
@@ -1509,7 +1546,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) );
}
- pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
+ //pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
// dump the miter parts
if ( 0 )
{
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index f3eb6dd7..df736e70 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -28,22 +28,31 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPsInv ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandGetInv ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPdrAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShow ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandInvPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvPrint ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvPut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInvMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; }
static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc)); }
static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; }
static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcInv; }
-static inline Vec_Int_t * Wlc_AbcGetCnf( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcCnf; }
-static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcStr; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -62,14 +71,25 @@ static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc )
******************************************************************************/
void Wlc_Init( Abc_Frame_t * pAbc )
{
- Cmd_CommandAdd( pAbc, "Word level", "%read", Abc_CommandReadWlc, 0 );
- Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 );
- Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 );
- Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 );
- Cmd_CommandAdd( pAbc, "Word level", "%psinv", Abc_CommandPsInv, 0 );
- Cmd_CommandAdd( pAbc, "Word level", "%getinv", Abc_CommandGetInv, 0 );
- Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 );
- Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%read", Abc_CommandReadWlc, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%cone", Abc_CommandCone, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%abs", Abc_CommandAbs, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%pdra", Abc_CommandPdrAbs, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%abs2", Abc_CommandAbs2, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%short_names", Abc_CommandShortNames, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%show", Abc_CommandShow, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 );
+
+ Cmd_CommandAdd( pAbc, "Word level", "inv_ps", Abc_CommandInvPs, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "inv_print", Abc_CommandInvPrint, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "inv_check", Abc_CommandInvCheck, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "inv_get", Abc_CommandInvGet, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "inv_put", Abc_CommandInvPut, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "inv_min", Abc_CommandInvMin, 0 );
}
/**Function********************************************************************
@@ -275,15 +295,20 @@ usage:
int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int fShowCones = 0;
int fShowMulti = 0;
int fShowAdder = 0;
int fDistrib = 0;
+ int fTwoSides = 0;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "madvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "cmadtvh" ) ) != EOF )
{
switch ( c )
{
+ case 'c':
+ fShowCones ^= 1;
+ break;
case 'm':
fShowMulti ^= 1;
break;
@@ -293,6 +318,9 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDistrib ^= 1;
break;
+ case 't':
+ fTwoSides ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -307,18 +335,110 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Abc_CommandPs(): There is no current design.\n" );
return 0;
}
- Wlc_NtkPrintStats( pNtk, fDistrib, fVerbose );
+ Wlc_NtkPrintStats( pNtk, fDistrib, fTwoSides, fVerbose );
+ if ( fShowCones )
+ Wlc_NtkProfileCones( pNtk );
if ( fShowMulti )
Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_MULTI );
if ( fShowAdder )
Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_ADD );
return 0;
usage:
- Abc_Print( -2, "usage: %%ps [-madvh]\n" );
+ Abc_Print( -2, "usage: %%ps [-cmadtvh]\n" );
Abc_Print( -2, "\t prints statistics\n" );
- Abc_Print( -2, "\t-m : toggle printing multipliers [default = %s]\n", fShowMulti? "yes": "no" );
- Abc_Print( -2, "\t-a : toggle printing adders [default = %s]\n", fShowAdder? "yes": "no" );
- Abc_Print( -2, "\t-d : toggle printing distrubition [default = %s]\n", fDistrib? "yes": "no" );
+ 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" );
+ Abc_Print( -2, "\t-a : toggle printing adders [default = %s]\n", fShowAdder? "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-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int c, iOutput = -1, Range = 1, fAllPis = 0, fSeq = 0, fVerbose = 0;
+ char * pName;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ORisvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'O':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ iOutput = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( iOutput < 0 )
+ goto usage;
+ break;
+ case 'R':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Range = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Range < 0 )
+ goto usage;
+ break;
+ case 'i':
+ fAllPis ^= 1;
+ break;
+ case 's':
+ fSeq ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
+ return 0;
+ }
+ if ( iOutput < 0 || iOutput >= Wlc_NtkCoNum(pNtk) )
+ {
+ Abc_Print( 1, "Abc_CommandCone(): Illegal output index (%d) (should be 0 <= num < %d).\n", iOutput, Wlc_NtkCoNum(pNtk) );
+ return 0;
+ }
+ printf( "Extracting output %d as a %s word-level network.\n", iOutput, fSeq ? "sequential" : "combinational" );
+ pName = Wlc_NtkNewName( pNtk, iOutput, fSeq );
+ Wlc_NtkMarkCone( pNtk, iOutput, Range, fSeq, fAllPis );
+ pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq );
+ ABC_FREE( pNtk->pName );
+ pNtk->pName = Abc_UtilStrsav( pName );
+ Wlc_AbcUpdateNtk( pAbc, pNtk );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%cone [-OR num] [-isvh]\n" );
+ Abc_Print( -2, "\t extracts logic cone of one or more word-level outputs\n" );
+ Abc_Print( -2, "\t-O num : zero-based index of the first word-level output to extract [default = %d]\n", iOutput );
+ Abc_Print( -2, "\t-R num : total number of word-level outputs to extract [default = %d]\n", Range );
+ Abc_Print( -2, "\t-i : toggle using support composed of all primary inputs [default = %s]\n", fAllPis? "yes": "no" );
+ Abc_Print( -2, "\t-s : toggle performing extracting sequential cones [default = %s]\n", fSeq? "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;
@@ -335,6 +455,357 @@ usage:
SeeAlso []
******************************************************************************/
+int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ Wlc_Par_t Pars, * pPars = &Pars;
+ int c;
+ Wlc_ManSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsAdd < 0 )
+ goto usage;
+ break;
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsMul = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsMul < 0 )
+ goto usage;
+ break;
+ case 'X':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsMux = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsMux < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsFlop < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nIterMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nIterMax < 0 )
+ goto usage;
+ break;
+ case 'x':
+ pPars->fXorOutput ^= 1;
+ break;
+ case 'c':
+ pPars->fCheckClauses ^= 1;
+ break;
+ case 'p':
+ pPars->fPushClauses ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'w':
+ pPars->fPdrVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
+ return 0;
+ }
+ Wlc_NtkPdrAbs( pNtk, pPars );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" );
+ Abc_Print( -2, "\t abstraction for word-level networks\n" );
+ Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
+ Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
+ Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
+ Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
+ Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
+ Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
+ Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" );
+ Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ Wlc_Par_t Pars, * pPars = &Pars;
+ int c;
+ Wlc_ManSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsAdd < 0 )
+ goto usage;
+ break;
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsMul = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsMul < 0 )
+ goto usage;
+ break;
+ case 'X':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsMux = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsMux < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsFlop < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nIterMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nIterMax < 0 )
+ goto usage;
+ break;
+ case 'x':
+ pPars->fXorOutput ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'w':
+ pPars->fPdrVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
+ return 0;
+ }
+ Wlc_NtkAbsCore( pNtk, pPars );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%abs [-AMXFI num] [-xvwh]\n" );
+ Abc_Print( -2, "\t abstraction for word-level networks\n" );
+ Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
+ Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
+ Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
+ Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
+ Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
+ Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandAbs2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ Wlc_Par_t Pars, * pPars = &Pars;
+ int c;
+ Wlc_ManSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsAdd < 0 )
+ goto usage;
+ break;
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsMul = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsMul < 0 )
+ goto usage;
+ break;
+ case 'X':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsMux = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsMux < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBitsFlop < 0 )
+ goto usage;
+ break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nIterMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nIterMax < 0 )
+ goto usage;
+ break;
+ case 'x':
+ pPars->fXorOutput ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'w':
+ pPars->fPdrVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
+ return 0;
+ }
+ Wlc_NtkAbsCore2( pNtk, pPars );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%abs2 [-AMXFI num] [-xvwh]\n" );
+ Abc_Print( -2, "\t abstraction for word-level networks\n" );
+ Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
+ Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
+ Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
+ Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
+ Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
+ Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
@@ -440,10 +911,200 @@ usage:
SeeAlso []
******************************************************************************/
-int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+ return 0;
+ }
+ Wlc_WinProfileArith( pNtk );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%profile [-vh]\n" );
+ Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\n" );
+ 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;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+ return 0;
+ }
+ Wlc_NtkShortNames( pNtk );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%short_names [-vh]\n" );
+ Abc_Print( -2, "\t derives short names for all objects of the network\n" );
+ 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;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold );
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int c, fVerbose = 0;
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( -1, "Empty network.\n" );
+ return 1;
+ }
+ Wlc_NtkShow( pNtk, NULL );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: %%show [-h]\n" );
+ Abc_Print( -2, " visualizes the network structure using DOT and GSVIEW\n" );
+#ifdef WIN32
+ Abc_Print( -2, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
+ Abc_Print( -2, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
+#endif
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
+ return 0;
+ }
+ // transform
+ //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
+ //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
+ //Wlc_AbcUpdateNtk( pAbc, pNtk );
+ //Wlc_GenerateSmtStdout( pAbc );
+ //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
+ pNtk = Wlc_NtkDupSingleNodes( pNtk );
+ Wlc_AbcUpdateNtk( pAbc, pNtk );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%test [-vh]\n" );
+ Abc_Print( -2, "\t experiments with word-level networks\n" );
+ 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;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandInvPs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
extern void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose );
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ Vec_Int_t * vCounts;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@@ -461,24 +1122,66 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pNtk == NULL )
{
- Abc_Print( 1, "Abc_CommandPsInv(): There is no current design.\n" );
+ Abc_Print( 1, "Abc_CommandInvPs(): There is no current design.\n" );
return 0;
}
- if ( Wlc_AbcGetNtk(pAbc) == NULL )
+ if ( Wlc_AbcGetInv(pAbc) == NULL )
{
- Abc_Print( 1, "Abc_CommandPsInv(): There is no saved invariant.\n" );
+ Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
return 0;
}
+ vCounts = Pdr_InvCounts( Wlc_AbcGetInv(pAbc) );
+ Wlc_NtkPrintInvStats( pNtk, vCounts, fVerbose );
+ Vec_IntFree( vCounts );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: inv_ps [-vh]\n" );
+ Abc_Print( -2, "\t prints statistics for inductive invariant\n" );
+ Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
+ 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;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose );
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
if ( Wlc_AbcGetInv(pAbc) == NULL )
{
- Abc_Print( 1, "Abc_CommandPsInv(): Invariant is not available.\n" );
+ Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
return 0;
}
- Wlc_NtkPrintInvStats( pNtk, Wlc_AbcGetInv(pAbc), fVerbose );
+ Pdr_InvPrint( Wlc_AbcGetInv(pAbc), fVerbose );
return 0;
- usage:
- Abc_Print( -2, "usage: %%psinv [-vh]\n" );
- Abc_Print( -2, "\t prints statistics for inductive invariant\n" );
+usage:
+ Abc_Print( -2, "usage: inv_print [-vh]\n" );
+ Abc_Print( -2, "\t prints the current inductive invariant\n" );
Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
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");
@@ -496,12 +1199,11 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv )
SeeAlso []
******************************************************************************/
-int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose );
- Abc_Ntk_t * pMainNtk;
- Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
- int c, fVerbose = 0;
+ abctime clk = Abc_Clock();
+ extern int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose );
+ int c, nFailed, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
@@ -516,28 +1218,81 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
- if ( pNtk == NULL )
+ if ( pAbc->pGia == NULL )
{
- Abc_Print( 1, "Abc_CommandGetInv(): There is no current design.\n" );
+ Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
return 0;
}
- if ( Wlc_AbcGetNtk(pAbc) == NULL )
+ if ( Wlc_AbcGetInv(pAbc) == NULL )
{
- Abc_Print( 1, "Abc_CommandGetInv(): There is no saved invariant.\n" );
+ Abc_Print( 1, "Abc_CommandInvMin(): There is no saved invariant.\n" );
return 0;
}
+ if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(Wlc_AbcGetInv(pAbc)) )
+ {
+ Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
+ return 0;
+ }
+ nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc), fVerbose );
+ if ( nFailed )
+ printf( "Invariant verification failed for %d clauses (out of %d). ", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) );
+ else
+ printf( "Invariant verification succeeded. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: inv_check [-vh]\n" );
+ Abc_Print( -2, "\t checks that the invariant is indeed an inductive invariant\n" );
+ Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" );
+ 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;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv );
+ Abc_Ntk_t * pMainNtk;
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
if ( Wlc_AbcGetInv(pAbc) == NULL )
{
- Abc_Print( 1, "Abc_CommandGetInv(): Invariant is not available.\n" );
+ Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" );
return 0;
}
// derive the network
- pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), Wlc_AbcGetStr(pAbc), fVerbose );
+ pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) );
// replace the current network
- Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
+ if ( pMainNtk )
+ Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
return 0;
- usage:
- Abc_Print( -2, "usage: %%getinv [-vh]\n" );
+usage:
+ Abc_Print( -2, "usage: inv_get [-vh]\n" );
Abc_Print( -2, "\t places invariant found by PDR as the current network in the main-space\n" );
Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -556,34 +1311,45 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
SeeAlso []
******************************************************************************/
-int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia );
+ Vec_Int_t * vInv = NULL;
+ Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
- case 'v':
- fVerbose ^= 1;
- break;
- case 'h':
- goto usage;
- default:
- goto usage;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
}
}
if ( pNtk == NULL )
{
- Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+ Abc_Print( 1, "Abc_CommandInvPut(): There is no current design.\n" );
return 0;
}
- Wlc_WinProfileArith( pNtk );
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandInvPut(): There is no current AIG.\n" );
+ return 0;
+ }
+ // derive the network
+ vInv = Wlc_NtkGetPut( pNtk, pAbc->pGia );
+ if ( vInv )
+ Abc_FrameSetInv( vInv );
return 0;
usage:
- Abc_Print( -2, "usage: %%profile [-vh]\n" );
- Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\n" );
+ Abc_Print( -2, "usage: inv_put [-vh]\n" );
+ Abc_Print( -2, "\t inputs the current network in the main-space as an invariant\n" );
+ Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" );
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;
@@ -600,42 +1366,57 @@ usage:
SeeAlso []
******************************************************************************/
-int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
- Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
- int c, fVerbose = 0;
+ extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose );
+ extern Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose );
+ Vec_Int_t * vInv, * vInv2;
+ int c, fLits = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "lvh" ) ) != EOF )
{
switch ( c )
{
- case 'v':
- fVerbose ^= 1;
- break;
- case 'h':
- goto usage;
- default:
- goto usage;
+ case 'l':
+ fLits ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
}
}
- if ( pNtk == NULL )
+ if ( pAbc->pGia == NULL )
{
- Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
+ Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
return 0;
}
- // transform
- //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
- //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
- //Wlc_AbcUpdateNtk( pAbc, pNtk );
- //Wlc_GenerateSmtStdout( pAbc );
- //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
- pNtk = Wlc_NtkDupSingleNodes( pNtk );
- Wlc_AbcUpdateNtk( pAbc, pNtk );
+ if ( Wlc_AbcGetInv(pAbc) == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandInvMin(): Invariant is not available.\n" );
+ return 0;
+ }
+ vInv = Wlc_AbcGetInv(pAbc);
+ if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(vInv) )
+ {
+ Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
+ return 0;
+ }
+ if ( fLits )
+ vInv2 = Pdr_InvMinimizeLits( pAbc->pGia, vInv, fVerbose );
+ else
+ vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv, fVerbose );
+ if ( vInv2 )
+ Abc_FrameSetInv( vInv2 );
return 0;
usage:
- Abc_Print( -2, "usage: %%test [-vh]\n" );
- Abc_Print( -2, "\t experiments with word-level networks\n" );
+ Abc_Print( -2, "usage: inv_min [-lvh]\n" );
+ Abc_Print( -2, "\t performs minimization of the current invariant\n" );
+ Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" );
+ Abc_Print( -2, "\t-l : toggle minimizing literals rather than clauses [default = %s]\n", fLits? "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/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 6f396771..c8fc15a7 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -88,12 +88,40 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
NULL // 54: unused
};
+char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
+{
+ memset( pPars, 0, sizeof(Wlc_Par_t) );
+ pPars->nBitsAdd = ABC_INFINITY; // adder bit-width
+ pPars->nBitsMul = ABC_INFINITY; // multiplier bit-widht
+ pPars->nBitsMux = ABC_INFINITY; // MUX bit-width
+ pPars->nBitsFlop = ABC_INFINITY; // flop bit-width
+ pPars->nIterMax = 1000; // the max number of iterations
+ pPars->fXorOutput = 1; // XOR outputs of word-level miter
+ pPars->fCheckClauses = 1; // Check clauses in the reloaded trace
+ pPars->fPushClauses = 0; // Push clauses in the reloaded trace
+ pPars->fVerbose = 0; // verbose output`
+ pPars->fPdrVerbose = 0; // show verbose PDR output
+}
+
+/**Function*************************************************************
+
Synopsis [Working with models.]
Description []
@@ -195,14 +223,14 @@ void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins )
{
assert( pObj->nFanins == 0 );
pObj->nFanins = Vec_IntSize(vFanins);
- if ( Wlc_ObjHasArray(pObj) )
- pObj->pFanins[0] = (int *)Mem_FlexEntryFetch( p->pMemFanin, Vec_IntSize(vFanins) * sizeof(int) );
- memcpy( Wlc_ObjFanins(pObj), Vec_IntArray(vFanins), sizeof(int) * Vec_IntSize(vFanins) );
// special treatment of CONST, SELECT and TABLE
if ( pObj->Type == WLC_OBJ_CONST )
pObj->nFanins = 0;
else if ( pObj->Type == WLC_OBJ_BIT_SELECT || pObj->Type == WLC_OBJ_TABLE )
pObj->nFanins = 1;
+ if ( Wlc_ObjHasArray(pObj) )
+ pObj->pFanins[0] = (int *)Mem_FlexEntryFetch( p->pMemFanin, Vec_IntSize(vFanins) * sizeof(int) );
+ memcpy( Wlc_ObjFanins(pObj), Vec_IntArray(vFanins), sizeof(int) * Vec_IntSize(vFanins) );
}
void Wlc_NtkFree( Wlc_Ntk_t * p )
{
@@ -224,6 +252,8 @@ void Wlc_NtkFree( Wlc_Ntk_t * p )
ABC_FREE( p->vValues.pArray );
ABC_FREE( p->vCopies.pArray );
ABC_FREE( p->vBits.pArray );
+ ABC_FREE( p->vLevels.pArray );
+ ABC_FREE( p->vRefs.pArray );
ABC_FREE( p->pInits );
ABC_FREE( p->pObjs );
ABC_FREE( p->pName );
@@ -246,6 +276,91 @@ int Wlc_NtkMemUsage( Wlc_Ntk_t * p )
/**Function*************************************************************
+ Synopsis [Assigns object levels.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkCreateLevels( Wlc_Ntk_t * p )
+{
+ Wlc_Obj_t * pObj;
+ int i, k, iFanin, Level, LevelMax = 0;
+ Vec_IntFill( &p->vLevels, Wlc_NtkObjNumMax(p), 0 );
+ Wlc_NtkForEachObj( p, pObj, i )
+ {
+ Level = 0;
+ Wlc_ObjForEachFanin( pObj, iFanin, k )
+ Level = Abc_MaxInt( Level, Wlc_ObjLevelId(p, iFanin) + 1 );
+ Vec_IntWriteEntry( &p->vLevels, i, Level );
+ LevelMax = Abc_MaxInt( LevelMax, Level );
+ }
+ return LevelMax;
+}
+int Wlc_NtkCreateLevelsRev( Wlc_Ntk_t * p )
+{
+ Wlc_Obj_t * pObj;
+ int i, k, iFanin, Level, LevelMax = 0;
+ Vec_IntFill( &p->vLevels, Wlc_NtkObjNumMax(p), 0 );
+ Wlc_NtkForEachObjReverse( p, pObj, i )
+ {
+ if ( Wlc_ObjIsCi(pObj) )
+ continue;
+ Level = Wlc_ObjLevel(p, pObj) + 1;
+ Wlc_ObjForEachFanin( pObj, iFanin, k )
+ Vec_IntUpdateEntry( &p->vLevels, iFanin, Level );
+ LevelMax = Abc_MaxInt( LevelMax, Level );
+ }
+ // reverse the values
+ Wlc_NtkForEachObj( p, pObj, i )
+ Vec_IntWriteEntry( &p->vLevels, i, LevelMax - Wlc_ObjLevelId(p, i) );
+ Wlc_NtkForEachCi( p, pObj, i )
+ Vec_IntWriteEntry( &p->vLevels, Wlc_ObjId(p, pObj), 0 );
+ return LevelMax;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects statistics for each side of the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_NtkCollectStats( Wlc_Ntk_t * p, int nObjs[2][WLC_OBJ_NUMBER] )
+{
+ Wlc_Obj_t * pObj;
+ int n, i;
+ if ( Wlc_NtkPoNum(p) != 2 )
+ return;
+ for ( n = 0; n < 2; n++ )
+ {
+ Wlc_NtkMarkCone( p, n, 1, 1, 0 );
+ Wlc_NtkForEachObj( p, pObj, i )
+ if ( pObj->Mark )
+ nObjs[n][pObj->Type]++;
+ }
+ Wlc_NtkCleanMarks( p );
+}
+int Wlc_NtkCountRealPis( Wlc_Ntk_t * p )
+{
+ Wlc_Obj_t * pObj;
+ int i, Count = 0;
+ Wlc_NtkMarkCone( p, -1, -1, 1, 0 );
+ Wlc_NtkForEachPi( p, pObj, i )
+ Count += pObj->Mark;
+ Wlc_NtkCleanMarks( p );
+ return Count;
+}
+
+/**Function*************************************************************
+
Synopsis [Prints distribution of operator types.]
Description []
@@ -298,13 +413,18 @@ void Wlc_NtkPrintDistribSortOne( Vec_Ptr_t * vTypes, Vec_Ptr_t * vOccurs, int Ty
Vec_WrdReverseOrder( vType );
Vec_WrdReverseOrder( vOccur );
}
-void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
+void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fTwoSides, int fVerbose )
{
+ int nObjs[2][WLC_OBJ_NUMBER] = {{0}}; // counter of objects of each type
Wlc_Obj_t * pObj, * pObjRange = NULL; int nCountRange = 0;
Vec_Ptr_t * vTypes, * vOccurs;
Vec_Int_t * vAnds = Vec_IntStart( WLC_OBJ_NUMBER );
word Sign;
int i, k, s, s0, s1;
+ if ( Wlc_NtkPoNum(p) != 2 )
+ fTwoSides = 0;
+ if ( fTwoSides )
+ Wlc_NtkCollectStats( p, nObjs );
// allocate statistics arrays
vTypes = Vec_PtrStart( WLC_OBJ_NUMBER );
vOccurs = Vec_PtrStart( WLC_OBJ_NUMBER );
@@ -409,11 +529,11 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
else if ( pObj->Type == WLC_OBJ_REDUCT_XOR )
Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_XOR, 3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 );
else if ( pObj->Type == WLC_OBJ_REDUCT_NAND )
- Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NAND, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
+ Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NAND, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
else if ( pObj->Type == WLC_OBJ_REDUCT_NOR )
- Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NOR, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
+ Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NOR, Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 1 );
else if ( pObj->Type == WLC_OBJ_REDUCT_NXOR )
- Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NXOR, 3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 );
+ Vec_IntAddToEntry( vAnds, WLC_OBJ_REDUCT_NXOR, 3 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) - 3 );
else if ( pObj->Type == WLC_OBJ_ARI_ADD )
Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_ADD, 9 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) );
else if ( pObj->Type == WLC_OBJ_ARI_SUB )
@@ -435,28 +555,41 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
else if ( pObj->Type == WLC_OBJ_ARI_SQUARE )
Vec_IntAddToEntry( vAnds, WLC_OBJ_ARI_SQUARE, 5 * Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)) * Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)) );
}
- if ( nCountRange )
+ if ( nCountRange && Vec_IntSize(&p->vNameIds) > 0 )
{
printf( "Warning: %d objects of the design have non-zero-based ranges.\n", nCountRange );
printf( "In particular, object %6d with name \"%s\" has range %d=[%d:%d]\n", Wlc_ObjId(p, pObjRange),
Abc_NamStr(p->pManName, Wlc_ObjNameId(p, Wlc_ObjId(p, pObjRange))), Wlc_ObjRange(pObjRange), pObjRange->End, pObjRange->Beg );
}
// print by occurrence
- printf( "ID : name occurrence and2 (occurrence)<output_range>=<input_range>.<input_range> ...\n" );
+ printf( "ID : name occurrence%s and2 (occurrence)<output_range>=<input_range>.<input_range> ...\n", fTwoSides ? " Left Share Right":"" );
for ( i = 0; i < WLC_OBJ_NUMBER; i++ )
{
Vec_Wrd_t * vType = (Vec_Wrd_t *)Vec_PtrEntry( vTypes, i );
Vec_Wrd_t * vOccur = (Vec_Wrd_t *)Vec_PtrEntry( vOccurs, i );
if ( p->nObjs[i] == 0 )
continue;
- printf( "%2d : %-8s %6d%8d ", i, Wlc_Names[i], p->nObjs[i], Vec_IntEntry(vAnds, i) );
+ printf( "%2d : %-8s %6d", i, Wlc_Names[i], p->nObjs[i] );
+ if ( fTwoSides )
+ {
+ int nTotal = i == WLC_OBJ_PI ? Wlc_NtkCountRealPis(p) : p->nObjs[i];
+ printf( " " );
+ printf( "%6d", nObjs[0][i] );
+ printf( "%6d", nObjs[0][i]+nObjs[1][i]-nTotal );
+ printf( "%6d", nObjs[1][i] );
+ }
+ printf( "%8d ", Vec_IntEntry(vAnds, i) );
// sort by occurence
Wlc_NtkPrintDistribSortOne( vTypes, vOccurs, i );
Vec_WrdForEachEntry( vType, Sign, k )
{
Wlc_NtkPrintDistribFromSign( Sign, &s, &s0, &s1 );
if ( ((k % 6) == 5 && s1) || ((k % 8) == 7 && !s1) )
+ {
printf( "\n " );
+ if ( fTwoSides )
+ printf( " " );
+ }
printf( "(%d)", (int)Vec_WrdEntry( vOccur, k ) );
printf( "%s%d", Abc_LitIsCompl(s)?"-":"", Abc_Lit2Var(s) );
if ( s0 )
@@ -535,19 +668,19 @@ void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type )
Wlc_NtkPrintNode( p, pObj );
}
}
-void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose )
+void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose )
{
int i;
printf( "%-20s : ", p->pName );
- printf( "PI = %4d ", Wlc_NtkPiNum(p) );
+ printf( "PI = %4d ", Wlc_NtkCountRealPis(p) ); //Wlc_NtkPiNum(p) );
printf( "PO = %4d ", Wlc_NtkPoNum(p) );
printf( "FF = %4d ", Wlc_NtkFfNum(p) );
- printf( "Obj = %6d ", Wlc_NtkObjNum(p) );
+ printf( "Obj = %6d ", Wlc_NtkObjNum(p) - Wlc_NtkPiNum(p) - Wlc_NtkPoNum(p) - Wlc_NtkFfNum(p) );
printf( "Mem = %.3f MB", 1.0*Wlc_NtkMemUsage(p)/(1<<20) );
printf( "\n" );
if ( fDistrib )
{
- Wlc_NtkPrintDistrib( p, fVerbose );
+ Wlc_NtkPrintDistrib( p, fTwoSides, fVerbose );
return;
}
if ( !fVerbose )
@@ -566,6 +699,80 @@ void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose )
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
+{
+ int i;
+ assert( !Wlc_NtkHasCopy(pNew) && Wlc_NtkHasCopy(p) );
+ assert( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(p) );
+ assert( pNew->pManName == NULL && p->pManName != NULL );
+ Wlc_NtkCleanNameId( pNew );
+ for ( i = 0; i < p->nObjsAlloc; i++ )
+ if ( Wlc_ObjCopy(p, i) && i < Vec_IntSize(&p->vNameIds) && Wlc_ObjNameId(p, i) )
+ Wlc_ObjSetNameId( pNew, Wlc_ObjCopy(p, i), Wlc_ObjNameId(p, i) );
+ pNew->pManName = p->pManName;
+ p->pManName = NULL;
+ Vec_IntErase( &p->vNameIds );
+ // transfer table
+ pNew->pMemTable = p->pMemTable; p->pMemTable = NULL;
+ pNew->vTables = p->vTables; p->vTables = NULL;
+}
+char * Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq )
+{
+ static char pBuffer[1000];
+ sprintf( pBuffer, "%s_o%d_%s", p->pName, iCoId, fSeq ? "seq": "comb" );
+ return pBuffer;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reduce init vector.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Wlc_ReduceMarkedInitVec( Wlc_Ntk_t * p, Vec_Int_t * vInit )
+{
+ Vec_Int_t * vInitNew = Vec_IntDup( vInit );
+ Wlc_Obj_t * pObj; int i, k = 0;
+ assert( Vec_IntSize(vInit) == Wlc_NtkCiNum(p) - Wlc_NtkPiNum(p) );
+ Wlc_NtkForEachCi( p, pObj, i )
+ if ( !Wlc_ObjIsPi(pObj) && pObj->Mark )
+ Vec_IntWriteEntry( vInitNew, k++, Vec_IntEntry(vInit, i - Wlc_NtkPiNum(p)) );
+ Vec_IntShrink( vInitNew, k );
+ return vInitNew;
+}
+char * Wlc_ReduceMarkedInitStr( Wlc_Ntk_t * p, char * pInit )
+{
+ char * pInitNew = Abc_UtilStrsav( pInit );
+ Wlc_Obj_t * pObj; int i, b, nBits = 0, k = 0;
+ Wlc_NtkForEachCi( p, pObj, i )
+ {
+ if ( !Wlc_ObjIsPi(pObj) && pObj->Mark )
+ for ( b = 0; b < Wlc_ObjRange(pObj); b++ )
+ pInitNew[k++] = pInitNew[nBits+b];
+ if ( !Wlc_ObjIsPi(pObj) )
+ nBits += Wlc_ObjRange(pObj);
+ }
+ pInitNew[k] = '\0';
+ assert( nBits == (int)strlen(pInit) );
+ return pInitNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Duplicates the network in a topological order.]
Description []
@@ -623,47 +830,214 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v
Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins );
Wlc_ObjDup( pNew, p, iObj, vFanins );
}
-Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p )
+Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
{
Wlc_Ntk_t * pNew;
Wlc_Obj_t * pObj;
Vec_Int_t * vFanins;
int i;
- Wlc_NtkCleanCopy( p );
vFanins = Vec_IntAlloc( 100 );
+ Wlc_NtkCleanCopy( p );
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
pNew->fSmtLib = p->fSmtLib;
Wlc_NtkForEachCi( p, pObj, i )
- Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+ if ( !fMarked || pObj->Mark )
+ {
+ unsigned Type = pObj->Type;
+ if ( !fSeq ) pObj->Type = WLC_OBJ_PI;
+ Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+ pObj->Type = Type;
+ }
Wlc_NtkForEachCo( p, pObj, i )
- Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+ if ( !fMarked || pObj->Mark )
+ Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
Wlc_NtkForEachCo( p, pObj, i )
- Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+ if ( !fMarked || pObj->Mark )
+ Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), fSeq ? pObj->fIsFi : 0 );
+ Vec_IntFree( vFanins );
+ if ( fSeq )
+ {
+ if ( fMarked )
+ {
+ if ( p->vInits )
+ pNew->vInits = Wlc_ReduceMarkedInitVec( p, p->vInits );
+ if ( p->pInits )
+ pNew->pInits = Wlc_ReduceMarkedInitStr( p, p->pInits );
+ }
+ else
+ {
+ if ( p->vInits )
+ pNew->vInits = Vec_IntDup( p->vInits );
+ if ( p->pInits )
+ pNew->pInits = Abc_UtilStrsav( p->pInits );
+ }
+ }
+ if ( p->pSpec )
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ Wlc_NtkTransferNames( pNew, p );
+ return pNew;
+}
+Wlc_Ntk_t * Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
+{
+ Wlc_Ntk_t * pNew;
+ Wlc_Obj_t * pObj;
+ Vec_Int_t * vFanins;
+ int i;
+ Wlc_NtkCleanCopy( p );
+ pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
+ pNew->fSmtLib = p->fSmtLib;
+
+ // duplicate marked PIs
+ vFanins = Vec_IntAlloc( 100 );
+ Wlc_NtkForEachObjVec( vPisOld, p, pObj, i )
+ {
+ assert( Wlc_ObjIsPi(pObj) );
+ Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+ }
+ // duplicate additional PIs
+ Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+ {
+ unsigned Type = pObj->Type;
+ int nFanins = Wlc_ObjFaninNum(pObj);
+ assert( !Wlc_ObjIsPi(pObj) );
+ pObj->Type = WLC_OBJ_PI;
+ pObj->nFanins = 0;
+ Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+ pObj->Type = Type;
+ pObj->nFanins = (unsigned)nFanins;
+ }
+ // duplicate flop outputs
+ Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+ {
+ assert( !Wlc_ObjIsPi(pObj) && Wlc_ObjIsCi(pObj) );
+ Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+ }
+
+ // duplicate logic cones of primary outputs
+ Wlc_NtkForEachPo( p, pObj, i )
+ Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+ // duplidate logic cone of flop inputs
+ Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+ Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj)), vFanins );
+
+ // duplicate POs
+ Wlc_NtkForEachPo( p, pObj, i )
+ Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), 0 );
+ // duplicate flop inputs
+ Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+ Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, Wlc_ObjFo2Fi(p, pObj)), 1 );
+ Vec_IntFree( vFanins );
+
+ // mark flop outputs
+ Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
+ pObj->Mark = 1;
if ( p->vInits )
- pNew->vInits = Vec_IntDup( p->vInits );
+ pNew->vInits = Wlc_ReduceMarkedInitVec( p, p->vInits );
if ( p->pInits )
- pNew->pInits = Abc_UtilStrsav( p->pInits );
- Vec_IntFree( vFanins );
+ pNew->pInits = Wlc_ReduceMarkedInitStr( p, p->pInits );
+ Wlc_NtkCleanMarks( p );
+
if ( p->pSpec )
- pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+ //Wlc_NtkTransferNames( pNew, p );
return pNew;
}
-void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p )
+
+/**Function*************************************************************
+
+ Synopsis [Select the cone of the given output.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_NtkCleanMarks( Wlc_Ntk_t * p )
{
+ Wlc_Obj_t * pObj;
int i;
- assert( !Wlc_NtkHasCopy(pNew) && Wlc_NtkHasCopy(p) );
- assert( !Wlc_NtkHasNameId(pNew) && Wlc_NtkHasNameId(p) );
- assert( pNew->pManName == NULL && p->pManName != NULL );
- Wlc_NtkCleanNameId( pNew );
- for ( i = 0; i < p->nObjsAlloc; i++ )
- if ( Wlc_ObjCopy(p, i) && i < Vec_IntSize(&p->vNameIds) && Wlc_ObjNameId(p, i) )
- Wlc_ObjSetNameId( pNew, Wlc_ObjCopy(p, i), Wlc_ObjNameId(p, i) );
- pNew->pManName = p->pManName;
- p->pManName = NULL;
- Vec_IntErase( &p->vNameIds );
- // transfer table
- pNew->pMemTable = p->pMemTable; p->pMemTable = NULL;
- pNew->vTables = p->vTables; p->vTables = NULL;
+ Wlc_NtkForEachObj( p, pObj, i )
+ pObj->Mark = 0;
+}
+int Wlc_NtkCountMarked( Wlc_Ntk_t * p, int * pnPis, int * pnFos, int * pnAdders, int * pnMults )
+{
+ Wlc_Obj_t * pObj;
+ int i, nNodes = 0;
+ *pnPis = *pnFos = *pnAdders = *pnMults = 0;
+ Wlc_NtkForEachObj( p, pObj, i )
+ {
+ if ( !pObj->Mark )
+ continue;
+ if ( Wlc_ObjIsPi(pObj) )
+ (*pnPis)++;
+ else if ( Wlc_ObjIsCi(pObj) )
+ (*pnFos)++;
+ else if ( pObj->Mark )
+ {
+ nNodes++;
+ if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB )
+ (*pnAdders)++;
+ else if ( pObj->Type == WLC_OBJ_ARI_MULTI )
+ (*pnMults)++;
+ }
+ }
+ return nNodes;
+}
+void Wlc_NtkMarkCone_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFlops )
+{
+ int i, iFanin;
+ if ( pObj->Mark )
+ return;
+ pObj->Mark = 1;
+ if ( Wlc_ObjIsCi(pObj) )
+ {
+ if ( !Wlc_ObjIsPi(pObj) )
+ Vec_IntPush( vFlops, Wlc_ObjCiId(pObj) );
+ return;
+ }
+ Wlc_ObjForEachFanin( pObj, iFanin, i )
+ Wlc_NtkMarkCone_rec( p, Wlc_NtkObj(p, iFanin), vFlops );
+}
+void Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis )
+{
+ Vec_Int_t * vFlops;
+ Wlc_Obj_t * pObj;
+ int i, CiId, CoId;
+ Wlc_NtkCleanMarks( p );
+ if ( fAllPis )
+ Wlc_NtkForEachPi( p, pObj, i )
+ pObj->Mark = 1;
+ vFlops = Vec_IntAlloc( 100 );
+ Wlc_NtkForEachCo( p, pObj, i )
+ if ( iCoId == -1 || (i >= iCoId && i < iCoId + Range) )
+ Wlc_NtkMarkCone_rec( p, pObj, vFlops );
+ if ( fSeq )
+ Vec_IntForEachEntry( vFlops, CiId, i )
+ {
+ CoId = Wlc_NtkPoNum(p) + CiId - Wlc_NtkPiNum(p);
+ Wlc_NtkMarkCone_rec( p, Wlc_NtkCo(p, CoId), vFlops );
+ }
+ Vec_IntFree( vFlops );
+}
+void Wlc_NtkProfileCones( Wlc_Ntk_t * p )
+{
+ Wlc_Obj_t * pObj;
+ int i, nPis, nFos, nNodes, nAdders, nMults;
+ Wlc_NtkForEachCo( p, pObj, i )
+ {
+ Wlc_NtkMarkCone( p, i, 1, 0, 0 );
+ nNodes = Wlc_NtkCountMarked( p, &nPis, &nFos, &nAdders, &nMults );
+ printf( "Cone %5d : ", i );
+ printf( "PI = %4d ", nPis );
+ printf( "FO = %4d ", nFos );
+ printf( "Node = %6d ", nNodes );
+ printf( "Add/Sub = %4d ", nAdders );
+ printf( "Mult = %4d ", nMults );
+ printf( "\n" );
+ }
+ Wlc_NtkCleanMarks( p );
}
/**Function*************************************************************
@@ -723,6 +1097,128 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p )
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis [Creates short names for all objects.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_NtkShortNames( Wlc_Ntk_t * p )
+{
+ Wlc_Obj_t * pObj;
+ char pBuffer[100];
+ int nDigits, NameId, fFound, i;
+ int nFlops = Wlc_NtkCoNum(p) - Wlc_NtkPoNum(p);
+ nDigits = Abc_Base10Log( nFlops );
+ Wlc_NtkForEachCo( p, pObj, i )
+ {
+ if ( Wlc_ObjIsPo(pObj) )
+ continue;
+ sprintf( pBuffer, "%s%0*d", "fi", nDigits, i - Wlc_NtkPoNum(p) );
+ NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
+ Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
+ }
+ Wlc_NtkForEachCi( p, pObj, i )
+ {
+ if ( Wlc_ObjIsPi(pObj) )
+ continue;
+ sprintf( pBuffer, "%s%0*d", "fo", nDigits, i - Wlc_NtkPiNum(p) );
+ NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
+ Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
+ }
+ nDigits = Abc_Base10Log( Wlc_NtkPoNum(p) );
+ Wlc_NtkForEachPo( p, pObj, i )
+ {
+ sprintf( pBuffer, "%s%0*d", "po", nDigits, i );
+ NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
+ Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
+ }
+ nDigits = Abc_Base10Log( Wlc_NtkPiNum(p) );
+ Wlc_NtkForEachPi( p, pObj, i )
+ {
+ sprintf( pBuffer, "%s%0*d", "pi", nDigits, i );
+ NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
+ Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
+ }
+ nDigits = Abc_Base10Log( Wlc_NtkObjNum(p) );
+ Wlc_NtkForEachObj( p, pObj, i )
+ {
+ if ( Wlc_ObjIsCi(pObj) || Wlc_ObjIsCo(pObj) )
+ continue;
+ sprintf( pBuffer, "%s%0*d", "n", nDigits, i );
+ NameId = Abc_NamStrFindOrAdd( p->pManName, pBuffer, &fFound );
+ Wlc_ObjSetNameId( p, Wlc_ObjId(p, pObj), NameId );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Count the number of flops initialized to DC value.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkDcFlopNum( Wlc_Ntk_t * p )
+{
+ int i, nFlops, Count = 0;
+ if ( p->pInits == NULL )
+ return 0;
+ nFlops = strlen(p->pInits);
+ for ( i = 0; i < nFlops; i++ )
+ Count += (p->pInits[i] == 'x' || p->pInits[i] == 'X');
+ return Count;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Create references.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_NtkSetRefs( Wlc_Ntk_t * p )
+{
+ Wlc_Obj_t * pObj; int i, k, Fanin;
+ Vec_IntFill( &p->vRefs, Wlc_NtkObjNumMax(p), 0 );
+ Wlc_NtkForEachObj( p, pObj, i )
+ Wlc_ObjForEachFanin( pObj, Fanin, k )
+ Vec_IntAddToEntry( &p->vRefs, Fanin, 1 );
+ Wlc_NtkForEachCo( p, pObj, i )
+ Vec_IntAddToEntry( &p->vRefs, Wlc_ObjId(p, pObj), 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [This procedure simply count the number of PPI bits.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkCountObjBits( Wlc_Ntk_t * p, Vec_Int_t * vPisNew )
+{
+ Wlc_Obj_t * pObj;
+ int i, Count = 0;
+ Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+ Count += Wlc_ObjRange(pObj);
+ return Count;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index d07a54c4..69a01ab0 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -48,6 +48,9 @@ struct Smt_Prs_t_
char ErrorStr[1000];
};
+//#define SMT_GLO_SUFFIX "_glb"
+#define SMT_GLO_SUFFIX ""
+
// parser name types
typedef enum {
SMT_PRS_NONE = 0,
@@ -219,6 +222,8 @@ static inline int Smt_StrToType( char * pName, int * pfSigned )
Type = WLC_OBJ_ARI_REM, *pfSigned = 1; // 40: arithmetic remainder
else if ( !strcmp(pName, "bvsmod") )
Type = WLC_OBJ_ARI_MODULUS, *pfSigned = 1; // 40: arithmetic modulus
+ else if ( !strcmp(pName, "=") )
+ Type = WLC_OBJ_COMP_EQU; // 40: arithmetic modulus
// else if ( !strcmp(pName, "") )
// Type = WLC_OBJ_ARI_POWER; // 41: arithmetic power
else if ( !strcmp(pName, "bvneg") )
@@ -255,6 +260,8 @@ static inline int Smt_PrsReadType( Smt_Prs_t * p, int iSig, int * pfSigned, int
}
}
+static inline int Smt_StrType( char * str ) { return Smt_StrToType(str, NULL); }
+
/**Function*************************************************************
Synopsis []
@@ -274,20 +281,27 @@ static inline int Smt_PrsCreateNodeOld( Wlc_Ntk_t * pNtk, int Type, int fSigned,
assert( Type > 0 );
assert( Range >= 0 );
assert( fSigned >= 0 );
- Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
- if ( fSigned )
- Wlc_NtkObj(pNtk, iObj)->Signed = fSigned;
- if ( Type == WLC_OBJ_SHIFT_RA )
- Wlc_NtkObj(pNtk, iObj)->Signed = 1;
+
+ // add node's name
if ( pName == NULL )
{
sprintf( Buffer, "_n%d_", iObj );
pName = Buffer;
}
- // add node's name
NameId = Abc_NamStrFindOrAdd( pNtk->pManName, pName, &fFound );
assert( !fFound );
assert( iObj == NameId );
+
+ Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), vFanins );
+ if ( fSigned )
+ {
+ Wlc_NtkObj(pNtk, iObj)->Signed = fSigned;
+// if ( Vec_IntSize(vFanins) > 0 )
+// Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 0))->Signed = fSigned;
+// if ( Vec_IntSize(vFanins) > 1 )
+// Wlc_NtkObj(pNtk, Vec_IntEntry(vFanins, 1))->Signed = fSigned;
+ }
+
return iObj;
}
static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, int Range, Vec_Int_t * vFanins, char * pName )
@@ -302,8 +316,7 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in
assert( Range >= 0 );
assert( fSigned >= 0 );
- // allow more than 2 fanins for specific operators
- // if (Vec_IntSize(vFanins)<=2 || Type == WLC_OBJ_BIT_CONCAT || Type == WLC_OBJ_MUX )
+ //if (Vec_IntSize(vFanins)<=2 || Type == WLC_OBJ_BIT_CONCAT || Type == WLC_OBJ_MUX )
// explicitely secify allowed multi operators
if (Vec_IntSize(vFanins)<=2 ||
!( Type == WLC_OBJ_BIT_AND || // 16:`` bitwise AND
@@ -362,17 +375,17 @@ FINISHED_WITH_FANINS:
Vec_IntFree(v2Fanins);
- // to deal with long shifts create extra bit select (ROTATE as well ??)
+ //added to deal with long shifts create extra bit select (ROTATE as well ??)
// this is a temporary hack
- // basically we keep only 32 bits.
- // bits 0 - 30 are kept same as original
- // bit 31 will be the reduction or of all bits from 31 to Range-1
+ // basically we keep only 32 bits.
+ // bit[31] will be the copy of original MSB (sign bit, just in case) UPDATE: assume it is unsigned first????
+ // bit[31] will be the reduction or of any bits from [31] to Range
if (Type == WLC_OBJ_SHIFT_R || Type == WLC_OBJ_SHIFT_RA || Type == WLC_OBJ_SHIFT_L)
{
- int iFanin1 = Vec_IntEntry(vFanins,1);
- int range1 = Wlc_ObjRange( Wlc_NtkObj(pNtk, iFanin1) );
- int iObj1, iObj2, iObj3;
+ int range1, iObj1, iObj2, iObj3;
assert(Vec_IntSize(vFanins)>=2);
+ iFanin1 = Vec_IntEntry(vFanins,1);
+ range1 = Wlc_ObjRange( Wlc_NtkObj(pNtk, iFanin1) );
if (range1>32)
{
Vec_Int_t * newFanins = Vec_IntAlloc(10);
@@ -389,6 +402,8 @@ FINISHED_WITH_FANINS:
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj1), newFanins );
+ //printf("obj1: %d\n",iObj1);
+
// bit select of larger bits
Vec_IntPop(newFanins);
Vec_IntPop(newFanins);
@@ -402,6 +417,7 @@ FINISHED_WITH_FANINS:
assert( iObj2 == NameId );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj2), newFanins );
+ //printf("obj2: %d\n",iObj2);
// reduction or
Vec_IntPop( newFanins );
@@ -416,6 +432,7 @@ FINISHED_WITH_FANINS:
assert( iObj3 == NameId );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj3), newFanins );
+ //printf("obj3: %d\n",iObj3);
// concat all together
Vec_IntWriteEntry( newFanins, 0, iObj3 );
@@ -429,6 +446,7 @@ FINISHED_WITH_FANINS:
assert( iObj == NameId );
Wlc_ObjAddFanins( pNtk, Wlc_NtkObj(pNtk, iObj), newFanins );
+ //printf("obj: %d\n",iObj);
// pushing the new node
Vec_IntWriteEntry(vFanins, 1, iObj);
@@ -461,34 +479,22 @@ FINISHED_WITH_FANINS:
return iObj;
}
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
static inline char * Smt_GetHexFromDecimalString(char * pStr)
{
int i,k=0, nDigits = strlen(pStr);
int digit, carry = 0;
- int metNonZeroBit;
- int nBits;
- char * hex;
+ int metNonZeroBit = 0;
Vec_Int_t * decimal = Vec_IntAlloc(nDigits);
Vec_Int_t * rev;
+ int nBits;
+ char * hex;
for (i=0;i<nDigits;i++)
Vec_IntPush(decimal,pStr[i]-'0');
- // firstly fill-in the reversed vector
+ // firstly fillin the reversed vector
rev = Vec_IntAlloc(10);
- metNonZeroBit = 0;
while(k<nDigits)
{
digit = Vec_IntEntry(decimal,k);
@@ -501,7 +507,7 @@ static inline char * Smt_GetHexFromDecimalString(char * pStr)
break;
else
{
- Vec_IntPush(rev,carry);
+ Vec_IntPush(rev,carry);
carry = 0;
k = 0;
metNonZeroBit = 0;
@@ -564,12 +570,17 @@ static inline char * Smt_GetHexFromDecimalString(char * pStr)
default: assert(0);
}
hex[nBits/4-1-k] = letter;
+ //if (k<Vec_IntSize(rev))
+ // Vec_IntPush(vFanins,Vec_IntEntry(rev,k));
+ //else
+ // Vec_IntPush(vFanins,0);
}
hex[nBits/4] = '\0';
Vec_IntFree(rev);
return hex;
-}
+}
+
static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits, char * pName )
{
int i, nDigits, iObj;
@@ -578,6 +589,25 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits
{
if ( pStr[0] >= '0' && pStr[0] <= '9' )
{
+ // added: sanity check for large constants
+ /*
+ Vec_Int_t * temp = Vec_IntAlloc(10);
+ int fullBits = -1;
+ Smt_GetBinaryFromDecimalString(pStr,temp,&fullBits);
+ Vec_IntFree(temp);
+ assert(fullBits < 32);*/
+
+ char * pHex = Smt_GetHexFromDecimalString(pStr);
+
+ if ( nBits == -1 )
+ nBits = strlen(pHex)*4;
+
+ //printf("nbits: %d\n",nBits);
+
+ Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 );
+ nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pHex );
+ ABC_FREE( pHex );
+
/*
int w, nWords, Number = atoi( pStr );
if ( nBits == -1 )
@@ -589,15 +619,6 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits
for ( w = 0; w < nWords; w++ )
Vec_IntPush( vFanins, w ? 0 : Number );
*/
-
- // convert decimal to hex to parse large constants
- char * pHex = Smt_GetHexFromDecimalString(pStr);
-
- if ( nBits == -1 )
- nBits = strlen(pHex)*4;
-
- Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 );
- nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pHex );
}
else
{
@@ -616,7 +637,10 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits
if ( pStr[2+i] == '1' )
Abc_InfoSetBit( (unsigned *)Vec_IntArray(vFanins), nBits-1-i );
else if ( pStr[2+i] != '0' )
+ {
+ Vec_IntFree( vFanins );
return 0;
+ }
}
else if ( pStr[1] == 'x' ) // hexadecimal
{
@@ -625,9 +649,16 @@ static inline int Smt_PrsBuildConstant( Wlc_Ntk_t * pNtk, char * pStr, int nBits
Vec_IntFill( vFanins, Abc_BitWordNum(nBits), 0 );
nDigits = Abc_TtReadHexNumber( (word *)Vec_IntArray(vFanins), pStr+2 );
if ( nDigits != (nBits + 3)/4 )
+ {
+ Vec_IntFree( vFanins );
return 0;
+ }
+ }
+ else
+ {
+ Vec_IntFree( vFanins );
+ return 0;
}
- else return 0;
// create constant node
iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_CONST, 0, nBits, vFanins, pName );
Vec_IntFree( vFanins );
@@ -648,12 +679,6 @@ int Smt_PrsBuildNode( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int RangeOut,
// s3087
int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
assert( fFound );
- // create buffer if the name of the fanin has different name
- if ( pName && strcmp(pStr, pName) )
- {
- Vec_IntFill( &p->vTempFans, 1, iObj );
- iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, RangeOut, &p->vTempFans, pName );
- }
return iObj;
}
}
@@ -804,13 +829,6 @@ Wlc_Ntk_t * Smt_PrsBuild( Smt_Prs_t * p )
// skip ()
Fan = Vec_IntEntry(vFans, 2);
assert( !Smt_EntryIsName(Fan) );
- vFans2 = Smt_VecEntryNode(p, vFans, 2);
- if ( Vec_IntSize(vFans2) > 0 )
- {
- printf( "File parsing error: Uninterpreted functions are not supported.\n" );
- Wlc_NtkFree( pNtk ); pNtk = NULL;
- goto finish;
- }
// check type (Bool or BitVec)
Fan = Vec_IntEntry(vFans, 3);
if ( Smt_EntryIsName(Fan) )
@@ -1006,6 +1024,14 @@ char * Smt_PrsGenName( Smt_Prs_t * p )
}
int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev, char * pName )
{
+ char suffix[100];
+ sprintf(suffix,"_as%d",pNtk->nAssert);
+
+ //char * prepStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode));
+ //printf("prestr: %s\n",prepStr);
+
+ //printf("inode: %d %d\n",iNode,Smt_EntryIsName(iNode));
+
if ( Smt_EntryIsName(iNode) )
{
char * pStr = Abc_NamStr(p->pStrs, Abc_Lit2Var(iNode));
@@ -1018,7 +1044,27 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
return Smt_PrsBuildConstant( pNtk, pStr, -1, pName ? pName : Smt_PrsGenName(p) );
else
{
- int fFound, iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
+ int fFound, iObj;
+ // look either for global DECLARE-FUN variable or local LET
+ char * pStr_glb = (char *)malloc(strlen(pStr) + 4 +1); //glb
+ char * pStr_loc = (char *)malloc(strlen(pStr) + strlen(suffix) +1);
+ strcpy(pStr_glb,pStr);
+ strcat(pStr_glb,SMT_GLO_SUFFIX);
+ strcpy(pStr_loc,pStr);
+ strcat(pStr_loc,suffix);
+
+ fFound = Abc_NamStrFind( pNtk->pManName, pStr_glb );
+
+ if (fFound)
+ pStr = pStr_glb;
+ else
+ {
+ assert( Abc_NamStrFind( pNtk->pManName, pStr_loc ));
+ pStr = pStr_loc;
+ }
+ // FIXME: delete memory of pStr
+
+ iObj = Abc_NamStrFindOrAdd( pNtk->pManName, pStr, &fFound );
assert( fFound );
// create buffer if the name of the fanin has different name
if ( pName && strcmp(Wlc_ObjName(pNtk, iObj), pName) )
@@ -1026,9 +1072,11 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
Vec_IntFill( &p->vTempFans, 1, iObj );
iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, Wlc_ObjRange(Wlc_NtkObj(pNtk, iObj)), &p->vTempFans, pName );
}
+ ABC_FREE( pStr_glb );
+ ABC_FREE( pStr_loc );
return iObj;
}
- }
+ }
else
{
Vec_Int_t * vRoots, * vRoots1, * vFans3;
@@ -1039,7 +1087,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
if ( Smt_EntryIsName(iRoot0) )
{
char * pName2, * pStr0 = Abc_NamStr(p->pStrs, Abc_Lit2Var(iRoot0));
- if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET )
+ if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET || Abc_Lit2Var(iRoot0) == SMT_PRS_DEFINE_FUN) //added define-fun is similar to let
{
// let ((s35550 (bvor s48 s35549)))
assert( Vec_IntSize(vRoots) == 3 );
@@ -1051,6 +1099,7 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
// iterate through the parts
Vec_IntForEachEntry( vRoots1, Fan, k )
{
+ char * temp;
// s35550 (bvor s48 s35549)
assert( !Smt_EntryIsName(Fan) );
vFans3 = Smt_EntryNode(p, Fan);
@@ -1059,11 +1108,26 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
Fan3 = Vec_IntEntry(vFans3, 0);
assert( Smt_EntryIsName(Fan3) );
pName2 = Smt_EntryName(p, Fan3);
+ // create a local name with suffix
+ if ( Abc_Lit2Var(iRoot0) == SMT_PRS_LET )
+ {
+ temp = (char *)malloc(strlen(pName2) + strlen(suffix) + 1);
+ strcpy(temp, pName2);
+ strcat(temp,suffix);
+ }
+ else
+ { temp = (char *)malloc(strlen(pName2) + 4 + 1);
+ strcpy(temp, pName2);
+ strcat(temp,SMT_GLO_SUFFIX);
+ }
+ // FIXME: need to delete memory of pName2
+ pName2 = temp;
// get function
Fan3 = Vec_IntEntry(vFans3, 1);
//assert( !Smt_EntryIsName(Fan3) );
// solve the problem
iObj = Smt_PrsBuild2_rec( pNtk, p, Fan3, -1, pName2 ); // NULL ); //pName2 );
+ ABC_FREE( temp );
if ( iObj == 0 )
return 0;
// create buffer
@@ -1133,7 +1197,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
int iObj = Abc_NamStrFind( pNtk->pManName, pStr0 );
if ( iObj )
return iObj;
-
Type0 = Smt_StrToType( pStr0, &fSigned );
if ( Type0 == 0 )
return 0;
@@ -1151,7 +1214,6 @@ int Smt_PrsBuild2_rec( Wlc_Ntk_t * pNtk, Smt_Prs_t * p, int iNode, int iObjPrev,
}
Vec_IntPush( vFanins, iObj );
}
-
// find range
Range = 0;
if ( Type0 >= WLC_OBJ_LOGIC_NOT && Type0 <= WLC_OBJ_REDUCT_XOR )
@@ -1197,7 +1259,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
Wlc_Ntk_t * pNtk;
Vec_Int_t * vFansRoot, * vFans, * vFans2;
Vec_Int_t * vAsserts = Vec_IntAlloc(100);
- int i, Root, Fan, iObj, NameId, Range, Status, nBits = 0;
+ int i, Root, Fan, iObj, NameId, Range, nBits = 0;
char * pName, * pRange;
// start network and create primary inputs
pNtk = Wlc_NtkAlloc( p->pName, 1000 );
@@ -1214,22 +1276,22 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
// create variables
if ( Abc_Lit2Var(Fan) == SMT_PRS_DECLARE_FUN )
{
+ char * pName_glb;
assert( Vec_IntSize(vFans) == 4 );
assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DECLARE_FUN) );
// get name
Fan = Vec_IntEntry(vFans, 1);
assert( Smt_EntryIsName(Fan) );
pName = Smt_EntryName(p, Fan);
+ // added: giving a global suffix
+ pName_glb = (char *) malloc(strlen(pName) + 4 + 1);
+ strcpy(pName_glb,pName);
+ strcat(pName_glb,SMT_GLO_SUFFIX);
+ // FIXME: delete memory of pName
+ pName = pName_glb;
// skip ()
Fan = Vec_IntEntry(vFans, 2);
assert( !Smt_EntryIsName(Fan) );
- vFans2 = Smt_VecEntryNode(p, vFans, 2);
- if ( Vec_IntSize(vFans2) > 0 )
- {
- printf( "File parsing error: Uninterpreted functions are not supported.\n" );
- Wlc_NtkFree( pNtk ); pNtk = NULL;
- goto finish;
- }
// check type (Bool or BitVec)
Fan = Vec_IntEntry(vFans, 3);
if ( Smt_EntryIsName(Fan) )
@@ -1259,9 +1321,11 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
Vec_IntPush( &pNtk->vValues, nBits );
Vec_IntPush( &pNtk->vValues, Range );
nBits += Range;
+ ABC_FREE( pName_glb );
}
// create constants
- else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN )
+ /*
+ else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN ) // added: we parse DEFINE_FUN in LET
{
assert( Vec_IntSize(vFans) == 5 );
assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) );
@@ -1269,6 +1333,14 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
Fan = Vec_IntEntry(vFans, 1);
assert( Smt_EntryIsName(Fan) );
pName = Smt_EntryName(p, Fan);
+
+ // added: giving a global suffix
+ char * pName_glb = (char *) malloc(strlen(pName) + 4 + 1);
+ strcpy(pName_glb,pName);
+ strcat(pName_glb,SMT_GLO_SUFFIX);
+ // FIXME: delete memory of pName
+ pName = pName_glb;
+
// skip ()
Fan = Vec_IntEntry(vFans, 2);
assert( !Smt_EntryIsName(Fan) );
@@ -1278,13 +1350,17 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
{
// (define-fun s_2 () Bool false)
assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
- iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), -1, pName );
- if ( iObj == 0 )
- {
- Wlc_NtkFree( pNtk ); pNtk = NULL;
- goto finish;
- }
- continue;
+ Range = 1;
+ pValue = Smt_VecEntryName(p, vFans, 4);
+
+ //printf("value: %s\n",pValue);
+
+ if ( !strcmp("false", pValue) )
+ pValue = "#b0";
+ else if ( !strcmp("true", pValue) )
+ pValue = "#b1";
+ else assert( 0 );
+ Status = Smt_PrsBuildConstant( pNtk, pValue, Range, pName );
}
else
{
@@ -1292,6 +1368,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
// (define-fun s1 () (_ BitVec 8) (bvneg #x7f))
// get range
Fan = Vec_IntEntry(vFans, 3);
+
assert( !Smt_EntryIsName(Fan) );
vFans2 = Smt_VecEntryNode(p, vFans, 3);
assert( Vec_IntSize(vFans2) == 3 );
@@ -1299,11 +1376,24 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
// get range
Fan = Vec_IntEntry(vFans2, 2);
+
assert( Smt_EntryIsName(Fan) );
pRange = Smt_EntryName(p, Fan);
Range = atoi(pRange);
+
+ // added: can parse functions too
+ Vec_Int_t * vFans3 = Smt_VecEntryNode(p, vFans, 4);
+ Fan = Vec_IntEntry(vFans3, 0);
+
// get constant
- Fan = Vec_IntEntry(vFans, 4);
+ //Fan = Vec_IntEntry(vFans, 4);
+
+ //printf("fan3: %s\n",Fan);
+ //printf("fan0: %s\n",Smt_VecEntryName(p, vFans3, 0));
+ //printf("fan1: %s\n",Smt_VecEntryName(p, vFans3, 1));
+ //printf("fan2: %s\n",Smt_VecEntryName(p, vFans3, 2));
+ //printf("fan3: %s\n",Smt_VecEntryName(p, vFans3, 3));
+
Status = Smt_PrsBuildNode( pNtk, p, Fan, Range, pName );
}
if ( !Status )
@@ -1312,6 +1402,57 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
goto finish;
}
}
+ */
+ // added: new way to parse define-fun
+ // create constants
+ else if ( Abc_Lit2Var(Fan) == SMT_PRS_DEFINE_FUN )
+ {
+ char * pName_glb;
+ // (define-fun def_16001 () Bool (or def_15999 def_16000))
+ // (define-fun def_15990 () (_ BitVec 24) (concat def_15988 def_15989))
+ assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_DEFINE_FUN) );
+ assert( Vec_IntSize(vFans) == 5 ); // const or definition
+
+ // get name
+ Fan = Vec_IntEntry(vFans, 1);
+ assert( Smt_EntryIsName(Fan) );
+ pName = Smt_EntryName(p, Fan);
+ // added: giving a global suffix
+ pName_glb = (char *) malloc(strlen(pName) + 4 + 1);
+ strcpy(pName_glb,pName);
+ strcat(pName_glb,SMT_GLO_SUFFIX);
+ // FIXME: delete memory of pName
+ pName = pName_glb;
+
+ //get range
+ Fan = Vec_IntEntry(vFans, 3);
+ if ( Smt_EntryIsName(Fan) )
+ {
+ // (define-fun s_2 () Bool false)
+ assert( !strcmp("Bool", Smt_VecEntryName(p, vFans, 3)) );
+ Range = 1;
+ }
+ else
+ {
+ // (define-fun s702 () (_ BitVec 4) #xe)
+ // (define-fun s1 () (_ BitVec 8) (bvneg #x7f))
+ assert( !Smt_EntryIsName(Fan) );
+ vFans2 = Smt_VecEntryNode(p, vFans, 3);
+ assert( Vec_IntSize(vFans2) == 3 );
+ assert( !strcmp("_", Smt_VecEntryName(p, vFans2, 0)) );
+ assert( !strcmp("BitVec", Smt_VecEntryName(p, vFans2, 1)) );
+ // get range
+ Fan = Vec_IntEntry(vFans2, 2);
+ assert( Smt_EntryIsName(Fan) );
+ pRange = Smt_EntryName(p, Fan);
+ Range = atoi(pRange);
+ }
+
+ iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 4), Range, pName );
+ assert( iObj );
+ ABC_FREE( pName_glb );
+ }
+
// collect assertion outputs
else if ( Abc_Lit2Var(Fan) == SMT_PRS_ASSERT )
{
@@ -1321,6 +1462,7 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
//(assert (not (= s0 #x00)))
assert( Vec_IntSize(vFans) == 2 );
assert( Smt_VecEntryIsType(vFans, 0, SMT_PRS_ASSERT) );
+ pNtk->nAssert++; // added
iObj = Smt_PrsBuild2_rec( pNtk, p, Vec_IntEntry(vFans, 1), -1, NULL );
if ( iObj == 0 )
{
@@ -1336,6 +1478,9 @@ Wlc_Ntk_t * Smt_PrsBuild2( Smt_Prs_t * p )
// build AND of asserts
if ( Vec_IntSize(vAsserts) == 1 )
iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BUF, 0, 1, vAsserts, "miter" );
+ // added: 0 asserts
+ else if ( Vec_IntSize(vAsserts) == 0 )
+ iObj = Smt_PrsBuildConstant( pNtk, "#b1", 1, "miter" );
else
{
iObj = Smt_PrsCreateNode( pNtk, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vAsserts), vAsserts, NULL );
@@ -1413,18 +1558,35 @@ static inline char * Smt_PrsLoadFile( char * pFileName, char ** ppLimit )
static inline int Smt_PrsRemoveComments( char * pBuffer, char * pLimit )
{
char * pTemp; int nCount1 = 0, nCount2 = 0, fHaveBar = 0;
+ int backslash = 0;
for ( pTemp = pBuffer; pTemp < pLimit; pTemp++ )
{
if ( *pTemp == '(' )
- nCount1++;
+ { if ( !fHaveBar ) nCount1++; }
else if ( *pTemp == ')' )
- nCount2++;
+ { if ( !fHaveBar ) nCount2++; }
else if ( *pTemp == '|' )
fHaveBar ^= 1;
else if ( *pTemp == ';' && !fHaveBar )
while ( *pTemp && *pTemp != '\n' )
*pTemp++ = ' ';
+ // added: hack to remove quotes
+ else if ( *pTemp == '\"' && *(pTemp-1) != '\\' && !fHaveBar )
+ {
+ *pTemp++ = ' ';
+ while ( *pTemp && (*pTemp != '\"' || backslash))
+ {
+ if (*pTemp == '\\')
+ backslash = 1;
+ else
+ backslash = 0;
+ *pTemp++ = ' ';
+ }
+ // remove the last quote symbol
+ *pTemp = ' ';
+ }
}
+
if ( nCount1 != nCount2 )
printf( "The input SMTLIB file has different number of opening and closing parentheses (%d and %d).\n", nCount1, nCount2 );
else if ( nCount1 == 0 )
@@ -1486,6 +1648,7 @@ static inline void Smt_PrsSkipNonSpaces( Smt_Prs_t * p )
}
void Smt_PrsReadLines( Smt_Prs_t * p )
{
+ int fFirstTime = 1;
assert( Vec_IntSize(&p->vStack) == 0 );
//assert( Vec_WecSize(&p->vDepth) == 0 );
assert( Vec_WecSize(&p->vObjs) == 0 );
@@ -1499,6 +1662,16 @@ void Smt_PrsReadLines( Smt_Prs_t * p )
for ( p->pCur = p->pBuffer; p->pCur < p->pLimit; p->pCur++ )
{
Smt_PrsSkipSpaces( p );
+ if ( fFirstTime && *p->pCur == '|' )
+ {
+ fFirstTime = 0;
+ *p->pCur = ' ';
+ while ( *p->pCur && *p->pCur != '|' )
+ *p->pCur++ = ' ';
+ if ( *p->pCur == '|' )
+ *p->pCur = ' ';
+ continue;
+ }
if ( *p->pCur == '(' )
{
// add new node at this depth
@@ -1524,12 +1697,13 @@ void Smt_PrsReadLines( Smt_Prs_t * p )
{
// remove strange characters (this can lead to name clashes)
int iToken;
+ /* commented out for SMT comp
char * pTemp;
if ( *pStart == '?' )
*pStart = '_';
for ( pTemp = pStart; pTemp < p->pCur; pTemp++ )
if ( *pTemp == '.' )
- *pTemp = '_';
+ *pTemp = '_';*/
// create and save token for this string
iToken = Abc_NamStrFindOrAddLim( p->pStrs, pStart, p->pCur--, NULL );
Vec_IntPush( Vec_WecEntry(&p->vObjs, Vec_IntEntryLast(&p->vStack)), Abc_Var2Lit(iToken, 1) );
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index fa3efacd..e4a65ecf 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
// Word-level Verilog file parser
-#define WLV_PRS_MAX_LINE 1000
+#define WLV_PRS_MAX_LINE 10000
typedef struct Wlc_Prs_t_ Wlc_Prs_t;
struct Wlc_Prs_t_
@@ -1265,8 +1265,7 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr )
if ( !Wlc_PrsDerive( p ) )
goto finish;
// derive topological order
- pNtk = Wlc_NtkDupDfs( p->pNtk );
- Wlc_NtkTransferNames( pNtk, p->pNtk );
+ pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 );
pNtk->pSpec = Abc_UtilStrsav( pFileName );
finish:
Wlc_PrsPrintErrorMessage( p );
diff --git a/src/base/wlc/wlcShow.c b/src/base/wlc/wlcShow.c
new file mode 100644
index 00000000..1601d602
--- /dev/null
+++ b/src/base/wlc/wlcShow.c
@@ -0,0 +1,337 @@
+/**CFile****************************************************************
+
+ FileName [wlcShow.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Verilog parser.]
+
+ Synopsis [Parses several flavors of word-level Verilog.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - August 22, 2014.]
+
+ Revision [$Id: wlcShow.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+ Synopsis [Writes the graph structure of WLC for DOT.]
+
+ Description [Useful for graph visualization using tools such as GraphViz:
+ http://www.graphviz.org/]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_NtkDumpDot( Wlc_Ntk_t * p, char * pFileName, Vec_Int_t * vBold )
+{
+ FILE * pFile;
+ Wlc_Obj_t * pNode;
+ int LevelMax, Prev, Level, i;
+
+ if ( Wlc_NtkObjNum(p) > 2000 )
+ {
+ fprintf( stdout, "Cannot visualize WLC with more than %d nodes.\n", 2000 );
+ return;
+ }
+ if ( (pFile = fopen( pFileName, "w" )) == NULL )
+ {
+ fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName );
+ return;
+ }
+
+ // mark the nodes
+ if ( vBold )
+ Wlc_NtkForEachObjVec( vBold, p, pNode, i )
+ pNode->Mark = 1;
+
+ // compute levels
+ LevelMax = 1 + Wlc_NtkCreateLevelsRev( p );
+
+ // write the DOT header
+ fprintf( pFile, "# %s\n", "WLC structure generated by ABC" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "digraph WLC {\n" );
+ fprintf( pFile, "size = \"7.5,10\";\n" );
+// fprintf( pFile, "ranksep = 0.5;\n" );
+// fprintf( pFile, "nodesep = 0.5;\n" );
+ fprintf( pFile, "center = true;\n" );
+// fprintf( pFile, "orientation = landscape;\n" );
+// fprintf( pFile, "edge [fontsize = 10];\n" );
+// fprintf( pFile, "edge [dir = none];\n" );
+ fprintf( pFile, "edge [dir = back];\n" );
+ fprintf( pFile, "\n" );
+
+ // labels on the left of the picture
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " node [shape = plaintext];\n" );
+ fprintf( pFile, " edge [style = invis];\n" );
+ fprintf( pFile, " LevelTitle1 [label=\"\"];\n" );
+ fprintf( pFile, " LevelTitle2 [label=\"\"];\n" );
+ // generate node names with labels
+ for ( Level = LevelMax; Level >= 0; Level-- )
+ {
+ // the visible node name
+ fprintf( pFile, " Level%d", Level );
+ fprintf( pFile, " [label = " );
+ // label name
+ fprintf( pFile, "\"" );
+ fprintf( pFile, "\"" );
+ fprintf( pFile, "];\n" );
+ }
+
+ // genetate the sequence of visible/invisible nodes to mark levels
+ fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" );
+ for ( Level = LevelMax; Level >= 0; Level-- )
+ {
+ // the visible node name
+ fprintf( pFile, " Level%d", Level );
+ // the connector
+ if ( Level != 0 )
+ fprintf( pFile, " ->" );
+ else
+ fprintf( pFile, ";" );
+ }
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate title box on top
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ fprintf( pFile, " LevelTitle1;\n" );
+ fprintf( pFile, " title1 [shape=plaintext,\n" );
+ fprintf( pFile, " fontsize=20,\n" );
+ fprintf( pFile, " fontname = \"Times-Roman\",\n" );
+ fprintf( pFile, " label=\"" );
+ fprintf( pFile, "%s", "WLC structure generated by ABC" );
+ fprintf( pFile, "\\n" );
+ fprintf( pFile, "Benchmark \\\"%s\\\". ", p->pName );
+// fprintf( pFile, "Time was %s. ", Extra_TimeStamp() );
+ fprintf( pFile, "\"\n" );
+ fprintf( pFile, " ];\n" );
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate statistics box
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ fprintf( pFile, " LevelTitle2;\n" );
+ fprintf( pFile, " title2 [shape=plaintext,\n" );
+ fprintf( pFile, " fontsize=18,\n" );
+ fprintf( pFile, " fontname = \"Times-Roman\",\n" );
+ fprintf( pFile, " label=\"" );
+ fprintf( pFile, "The word-level network contains %d nodes and spans %d levels.", Wlc_NtkObjNum(p)-Wlc_NtkCiNum(p), LevelMax-1 );
+ fprintf( pFile, "\\n" );
+ fprintf( pFile, "\"\n" );
+ fprintf( pFile, " ];\n" );
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate the COs
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ // the labeling node of this level
+ fprintf( pFile, " Level%d;\n", LevelMax );
+ // generate the CO nodes
+ Wlc_NtkForEachCo( p, pNode, i )
+ {
+ pNode = Wlc_ObjCo2PoFo(p, i);
+ fprintf( pFile, " NodePo%d [label = \"%s_in %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) );
+ fprintf( pFile, ", shape = %s", i < Wlc_NtkPoNum(p) ? "invtriangle" : "box" );
+ fprintf( pFile, ", color = coral, fillcolor = coral" );
+ fprintf( pFile, "];\n" );
+ }
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate nodes of each rank
+ for ( Level = LevelMax - 1; Level > 0; Level-- )
+ {
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ // the labeling node of this level
+ fprintf( pFile, " Level%d;\n", Level );
+ Wlc_NtkForEachObj( p, pNode, i )
+ {
+ if ( (int)Wlc_ObjLevel(p, pNode) != Level )
+ continue;
+
+ if ( pNode->Type == WLC_OBJ_CONST )
+ {
+ fprintf( pFile, " Node%d [label = \"0x", i );
+ Abc_TtPrintHexArrayRev( pFile, (word *)Wlc_ObjConstValue(pNode), (Wlc_ObjRange(pNode) + 3) / 4 );
+ fprintf( pFile, "\"" );
+ }
+ else if ( pNode->Type == WLC_OBJ_BUF || pNode->Type == WLC_OBJ_MUX )
+ fprintf( pFile, " Node%d [label = \"%d\"", i, Wlc_ObjRange(pNode) );
+ else if ( pNode->Type >= WLC_OBJ_LOGIC_NOT && pNode->Type <= WLC_OBJ_COMP_MOREEQU )
+ fprintf( pFile, " Node%d [label = \"%s\"", i, Wlc_ObjTypeName(pNode) );
+ else
+ fprintf( pFile, " Node%d [label = \"%s %d\"", i, Wlc_ObjTypeName(pNode), Wlc_ObjRange(pNode) );
+
+ if ( pNode->Type == WLC_OBJ_ARI_MULTI )
+ fprintf( pFile, ", shape = doublecircle" );
+ else if ( pNode->Type >= WLC_OBJ_COMP_EQU && pNode->Type <= WLC_OBJ_COMP_MOREEQU )
+ fprintf( pFile, ", shape = diamond" );
+ else if ( pNode->Type == WLC_OBJ_BIT_SELECT || pNode->Type == WLC_OBJ_BIT_CONCAT )
+ fprintf( pFile, ", shape = box" );
+ else if ( pNode->Type == WLC_OBJ_BUF || pNode->Type == WLC_OBJ_BIT_ZEROPAD || pNode->Type == WLC_OBJ_BIT_SIGNEXT )
+ fprintf( pFile, ", shape = triangle" );
+ else if ( pNode->Type == WLC_OBJ_MUX )
+ fprintf( pFile, ", shape = trapezium" );
+ else
+ fprintf( pFile, ", shape = ellipse" );
+
+ if ( vBold ? pNode->Mark : ((pNode->Type >= WLC_OBJ_ARI_ADD && pNode->Type <= WLC_OBJ_ARI_SQUARE) || pNode->Type == WLC_OBJ_BIT_NOT) )
+ fprintf( pFile, ", style = filled" );
+ fprintf( pFile, "];\n" );
+ }
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+ }
+
+ // generate the CI nodes
+ fprintf( pFile, "{\n" );
+ fprintf( pFile, " rank = same;\n" );
+ // the labeling node of this level
+ fprintf( pFile, " Level%d;\n", 0 );
+ // generate the CI nodes
+ Wlc_NtkForEachCi( p, pNode, i )
+ {
+ fprintf( pFile, " Node%d [label = \"%s %d\"", Wlc_ObjId(p, pNode), Wlc_ObjName(p, Wlc_ObjId(p, pNode)), Wlc_ObjRange(pNode) );
+ fprintf( pFile, ", shape = %s", i < Wlc_NtkPiNum(p) ? "triangle" : "box" );
+ fprintf( pFile, ", color = coral, fillcolor = coral" );
+ fprintf( pFile, "];\n" );
+ }
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+
+ // generate invisible edges from the square down
+ fprintf( pFile, "title1 -> title2 [style = invis];\n" );
+ Wlc_NtkForEachCo( p, pNode, i )
+ {
+ pNode = Wlc_ObjCo2PoFo( p, i );
+ fprintf( pFile, "title2 -> NodePo%d [style = invis];\n", Wlc_ObjId(p, pNode) );
+ }
+ // generate invisible edges among the COs
+ Prev = -1;
+ Wlc_NtkForEachCo( p, pNode, i )
+ {
+ pNode = Wlc_ObjCo2PoFo( p, i );
+ if ( i > 0 )
+ fprintf( pFile, "NodePo%d -> NodePo%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) );
+ Prev = Wlc_ObjId(p, pNode);
+ }
+ // generate invisible edges among the CIs
+ Prev = -1;
+ Wlc_NtkForEachCi( p, pNode, i )
+ {
+ if ( i > 0 )
+ fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Wlc_ObjId(p, pNode) );
+ Prev = Wlc_ObjId(p, pNode);
+ }
+
+ // generate edges
+ Wlc_NtkForEachCo( p, pNode, i )
+ {
+ fprintf( pFile, "NodePo%d", Wlc_ObjId(p, Wlc_ObjCo2PoFo(p, i)) );
+ fprintf( pFile, " -> " );
+ fprintf( pFile, "Node%d", Wlc_ObjId(p, pNode) );
+ fprintf( pFile, " [" );
+ fprintf( pFile, "style = %s", pNode->Signed? "dotted" : "solid" );
+ fprintf( pFile, "]" );
+ fprintf( pFile, ";\n" );
+ }
+ Wlc_NtkForEachObj( p, pNode, i )
+ {
+ int k, iFanin;
+ if ( Wlc_ObjIsCi(pNode) )
+ continue;
+ // generate the edge from this node to the next
+ Wlc_ObjForEachFanin( pNode, iFanin, k )
+ {
+ fprintf( pFile, "Node%d", i );
+ fprintf( pFile, " -> " );
+ fprintf( pFile, "Node%d", iFanin );
+ fprintf( pFile, " [" );
+ fprintf( pFile, "style = %s", Wlc_NtkObj(p, iFanin)->Signed? "dotted" : "solid" );
+ if ( pNode->Type == WLC_OBJ_MUX && k == 0 )
+ fprintf( pFile, ", style = %s", "bold" );
+ fprintf( pFile, "]" );
+ fprintf( pFile, ";\n" );
+ }
+ }
+ fprintf( pFile, "}" );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+
+ // unmark nodes
+ if ( vBold )
+ Wlc_NtkCleanMarks( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold )
+{
+ extern void Abc_ShowFile( char * FileNameDot );
+ FILE * pFile;
+ char FileNameDot[200];
+ sprintf( FileNameDot, "%s", Extra_FileNameGenericAppend(p->pName, ".dot") );
+ // check that the file can be opened
+ if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+ {
+ fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+ return;
+ }
+ fclose( pFile );
+ // generate the file
+ Wlc_NtkDumpDot( p, FileNameDot, vBold );
+ // visualize the file
+ Abc_ShowFile( FileNameDot );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wlc/wlcSim.c b/src/base/wlc/wlcSim.c
index 20ac8c61..e2fcd1f8 100644
--- a/src/base/wlc/wlcSim.c
+++ b/src/base/wlc/wlcSim.c
@@ -43,13 +43,13 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
static inline word * Wlc_ObjSim( Gia_Man_t * p, int iObj )
{
- return Vec_WrdEntryP( p->vSims, p->iPatsPi * iObj );
+ return Vec_WrdEntryP( p->vSims, p->nSimWords * iObj );
}
static inline void Wlc_ObjSimPi( Gia_Man_t * p, int iObj )
{
int w;
word * pSim = Wlc_ObjSim( p, iObj );
- for ( w = 0; w < p->iPatsPi; w++ )
+ for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = Gia_ManRandomW( 0 );
}
static inline void Wlc_ObjSimRo( Gia_Man_t * p, int iObj )
@@ -57,7 +57,7 @@ static inline void Wlc_ObjSimRo( Gia_Man_t * p, int iObj )
int w;
word * pSimRo = Wlc_ObjSim( p, iObj );
word * pSimRi = Wlc_ObjSim( p, Gia_ObjRoToRiId(p, iObj) );
- for ( w = 0; w < p->iPatsPi; w++ )
+ for ( w = 0; w < p->nSimWords; w++ )
pSimRo[w] = pSimRi[w];
}
static inline void Wlc_ObjSimCo( Gia_Man_t * p, int iObj )
@@ -67,10 +67,10 @@ static inline void Wlc_ObjSimCo( Gia_Man_t * p, int iObj )
word * pSimCo = Wlc_ObjSim( p, iObj );
word * pSimDri = Wlc_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
if ( Gia_ObjFaninC0(pObj) )
- for ( w = 0; w < p->iPatsPi; w++ )
+ for ( w = 0; w < p->nSimWords; w++ )
pSimCo[w] = ~pSimDri[w];
else
- for ( w = 0; w < p->iPatsPi; w++ )
+ for ( w = 0; w < p->nSimWords; w++ )
pSimCo[w] = pSimDri[w];
}
static inline void Wlc_ObjSimAnd( Gia_Man_t * p, int iObj )
@@ -81,16 +81,16 @@ static inline void Wlc_ObjSimAnd( Gia_Man_t * p, int iObj )
word * pSim0 = Wlc_ObjSim( p, Gia_ObjFaninId0(pObj, iObj) );
word * pSim1 = Wlc_ObjSim( p, Gia_ObjFaninId1(pObj, iObj) );
if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
- for ( w = 0; w < p->iPatsPi; w++ )
+ for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = ~pSim0[w] & ~pSim1[w];
else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
- for ( w = 0; w < p->iPatsPi; w++ )
+ for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = ~pSim0[w] & pSim1[w];
else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
- for ( w = 0; w < p->iPatsPi; w++ )
+ for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = pSim0[w] & ~pSim1[w];
else
- for ( w = 0; w < p->iPatsPi; w++ )
+ for ( w = 0; w < p->nSimWords; w++ )
pSim[w] = pSim0[w] & pSim1[w];
}
@@ -135,7 +135,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int
// allocate simulation info for one timeframe
Vec_WrdFreeP( &pGia->vSims );
pGia->vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * nWords );
- pGia->iPatsPi = nWords;
+ pGia->nSimWords = nWords;
// allocate resulting simulation info
vRes = Vec_PtrAlloc( Vec_IntSize(vNodes) );
Wlc_NtkForEachObjVec( vNodes, p, pWlcObj, i )
@@ -188,7 +188,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int
printf( "Replaced %d dangling internal bits with constant 0.\n", Counter );
}
Vec_WrdFreeP( &pGia->vSims );
- pGia->iPatsPi = 0;
+ pGia->nSimWords = 0;
Gia_ManStop( pGia );
return vRes;
}
diff --git a/src/base/wlc/wlcUif.c b/src/base/wlc/wlcUif.c
new file mode 100644
index 00000000..78451c17
--- /dev/null
+++ b/src/base/wlc/wlcUif.c
@@ -0,0 +1,290 @@
+/**CFile****************************************************************
+
+ FileName [wlcUif.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Verilog parser.]
+
+ Synopsis [Abstraction for word-level networks.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - August 22, 2014.]
+
+ Revision [$Id: wlcUif.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Check if two objects have the same input/output signatures.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_NtkPairIsUifable( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Wlc_Obj_t * pObj2 )
+{
+ Wlc_Obj_t * pFanin, * pFanin2; int k;
+ if ( Wlc_ObjRange(pObj) != Wlc_ObjRange(pObj2) )
+ return 0;
+ if ( Wlc_ObjIsSigned(pObj) != Wlc_ObjIsSigned(pObj2) )
+ return 0;
+ if ( Wlc_ObjFaninNum(pObj) != Wlc_ObjFaninNum(pObj2) )
+ return 0;
+ for ( k = 0; k < Wlc_ObjFaninNum(pObj); k++ )
+ {
+ pFanin = Wlc_ObjFanin(p, pObj, k);
+ pFanin2 = Wlc_ObjFanin(p, pObj2, k);
+ if ( Wlc_ObjRange(pFanin) != Wlc_ObjRange(pFanin2) )
+ return 0;
+ if ( Wlc_ObjIsSigned(pFanin) != Wlc_ObjIsSigned(pFanin2) )
+ return 0;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect IDs of the multipliers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkCollectMultipliers( Wlc_Ntk_t * p )
+{
+ Wlc_Obj_t * pObj; int i;
+ Vec_Int_t * vBoxIds = Vec_IntAlloc( 100 );
+ Wlc_NtkForEachObj( p, pObj, i )
+ if ( pObj->Type == WLC_OBJ_ARI_MULTI )
+ Vec_IntPush( vBoxIds, i );
+ if ( Vec_IntSize( vBoxIds ) > 0 )
+ return vBoxIds;
+ Vec_IntFree( vBoxIds );
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns all pairs of uifable multipliers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Wlc_NtkFindUifableMultiplierPairs( Wlc_Ntk_t * p )
+{
+ Vec_Int_t * vMultis = Wlc_NtkCollectMultipliers( p );
+ Vec_Int_t * vPairs = Vec_IntAlloc( 2 );
+ Wlc_Obj_t * pObj, * pObj2; int i, k;
+ // iterate through unique pairs
+ Wlc_NtkForEachObjVec( vMultis, p, pObj, i )
+ Wlc_NtkForEachObjVec( vMultis, p, pObj2, k )
+ {
+ if ( k == i )
+ break;
+ if ( Wlc_NtkPairIsUifable( p, pObj, pObj2 ) )
+ {
+ Vec_IntPush( vPairs, Wlc_ObjId(p, pObj) );
+ Vec_IntPush( vPairs, Wlc_ObjId(p, pObj2) );
+ }
+ }
+ Vec_IntFree( vMultis );
+ if ( Vec_IntSize( vPairs ) > 0 )
+ return vPairs;
+ Vec_IntFree( vPairs );
+ return NULL;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Abstracts nodes by replacing their outputs with new PIs.]
+
+ Description [If array is NULL, abstract all multipliers.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
+{
+ Vec_Int_t * vNodes = vNodesInit;
+ Wlc_Ntk_t * pNew;
+ Wlc_Obj_t * pObj;
+ int i, k, iObj, iFanin;
+ // get multipliers if not given
+ if ( vNodes == NULL )
+ vNodes = Wlc_NtkCollectMultipliers( p );
+ if ( vNodes == NULL )
+ return NULL;
+ // mark nodes
+ Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
+ pObj->Mark = 1;
+ // iterate through the nodes in the DFS order
+ Wlc_NtkCleanCopy( p );
+ Wlc_NtkForEachObj( p, pObj, i )
+ {
+ if ( i == Vec_IntSize(&p->vCopies) )
+ break;
+ if ( pObj->Mark ) {
+ // clean
+ pObj->Mark = 0;
+ // add fresh PI with the same number of bits
+ iObj = Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 );
+ }
+ else {
+ // update fanins
+ Wlc_ObjForEachFanin( pObj, iFanin, k )
+ Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
+ // node to remain
+ iObj = i;
+ }
+ Wlc_ObjSetCopy( p, i, iObj );
+ }
+ // POs do not change in this procedure
+ if ( vNodes != vNodesInit )
+ Vec_IntFree( vNodes );
+ // reconstruct topological order
+ pNew = Wlc_NtkDupDfs( p, 0, 1 );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds UIF constraints to node pairs and updates POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
+{
+ Vec_Int_t * vPairs = vPairsInit;
+ Wlc_Ntk_t * pNew;
+ Wlc_Obj_t * pObj, * pObj2;
+ Vec_Int_t * vUifConstrs, * vCompares, * vFanins;
+ int i, k, iObj, iObj2, iObjNew, iObjNew2;
+ int iFanin, iFanin2, iFaninNew;
+ // get multiplier pairs if not given
+ if ( vPairs == NULL )
+ vPairs = Wlc_NtkFindUifableMultiplierPairs( p );
+ if ( vPairs == NULL )
+ return NULL;
+ // sanity checks
+ assert( Vec_IntSize(vPairs) > 0 && Vec_IntSize(vPairs) % 2 == 0 );
+ // iterate through node pairs
+ vFanins = Vec_IntAlloc( 100 );
+ vCompares = Vec_IntAlloc( 100 );
+ vUifConstrs = Vec_IntAlloc( 100 );
+ Vec_IntForEachEntryDouble( vPairs, iObj, iObj2, i )
+ {
+ // get two nodes
+ pObj = Wlc_NtkObj( p, iObj );
+ pObj2 = Wlc_NtkObj( p, iObj2 );
+ assert( Wlc_NtkPairIsUifable(p, pObj, pObj2) );
+ // create fanin comparator nodes
+ Vec_IntClear( vCompares );
+ Wlc_ObjForEachFanin( pObj, iFanin, k )
+ {
+ iFanin2 = Wlc_ObjFaninId( pObj2, k );
+ Vec_IntFillTwo( vFanins, 2, iFanin, iFanin2 );
+ iFaninNew = Wlc_ObjCreate( p, WLC_OBJ_COMP_NOTEQU, 0, 0, 0, vFanins );
+ Vec_IntPush( vCompares, iFaninNew );
+ // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to
+ // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
+ pObj = Wlc_NtkObj( p, iObj );
+ }
+ // concatenate fanin comparators
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vCompares) - 1, 0, vCompares );
+ // create reduction-OR node
+ Vec_IntFill( vFanins, 1, iObjNew );
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_OR, 0, 0, 0, vFanins );
+ // craete output comparator node
+ Vec_IntFillTwo( vFanins, 2, iObj, iObj2 );
+ iObjNew2 = Wlc_ObjCreate( p, WLC_OBJ_COMP_EQU, 0, 0, 0, vFanins );
+ // create implication node (iObjNew is already complemented above)
+ Vec_IntFillTwo( vFanins, 2, iObjNew, iObjNew2 );
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_OR, 0, 0, 0, vFanins );
+ // save the constraint
+ Vec_IntPush( vUifConstrs, iObjNew );
+ }
+ // derive the AND of the UIF contraints
+ assert( Vec_IntSize(vUifConstrs) > 0 );
+ if ( Vec_IntSize(vUifConstrs) == 1 )
+ iObjNew = Vec_IntEntry( vUifConstrs, 0 );
+ else
+ {
+ // concatenate
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_BIT_CONCAT, 0, Vec_IntSize(vUifConstrs) - 1, 0, vUifConstrs );
+ // create reduction-AND node
+ Vec_IntFill( vFanins, 1, iObjNew );
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_REDUCT_AND, 0, 0, 0, vFanins );
+ }
+ // update each PO to point to the new node
+ Wlc_NtkForEachPo( p, pObj, i )
+ {
+ iObj = Wlc_ObjId(p, pObj);
+ Vec_IntFillTwo( vFanins, 2, iObj, iObjNew );
+ iObjNew = Wlc_ObjCreate( p, WLC_OBJ_LOGIC_AND, 0, 0, 0, vFanins );
+ // note that a pointer to Wlc_Obj_t (for example, pObj) can be invalidated after a call to
+ // Wlc_ObjCreate() due to a possible realloc of the internal array of objects...
+ pObj = Wlc_NtkObj( p, iObj );
+ // update PO/CO arrays
+ assert( Vec_IntEntry(&p->vPos, i) == iObj );
+ assert( Vec_IntEntry(&p->vCos, i) == iObj );
+ Vec_IntWriteEntry( &p->vPos, i, iObjNew );
+ Vec_IntWriteEntry( &p->vCos, i, iObjNew );
+ // transfer the PO attribute
+ Wlc_NtkObj(p, iObjNew)->fIsPo = 1;
+ assert( pObj->fIsPo );
+ pObj->fIsPo = 0;
+ }
+ // cleanup
+ Vec_IntFree( vUifConstrs );
+ Vec_IntFree( vCompares );
+ Vec_IntFree( vFanins );
+ if ( vPairs != vPairsInit )
+ Vec_IntFree( vPairs );
+ // reconstruct topological order
+ pNew = Wlc_NtkDupDfs( p, 0, 1 );
+ return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/wlc/wlcWriteVer.c b/src/base/wlc/wlcWriteVer.c
index cf0e528f..c4dee094 100644
--- a/src/base/wlc/wlcWriteVer.c
+++ b/src/base/wlc/wlcWriteVer.c
@@ -409,7 +409,7 @@ void Wlc_WriteVerInt( FILE * pFile, Wlc_Ntk_t * p, int fNoFlops )
fprintf( pFile, " reg%d (", i );
fprintf( pFile, " .q( %s ),", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
fprintf( pFile, " .qbar()," );
- fprintf( pFile, " .d( %s ),", Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFoToFi(p, pObj))) );
+ fprintf( pFile, " .d( %s ),", Wlc_ObjName(p, Wlc_ObjId(p, Wlc_ObjFo2Fi(p, pObj))) );
fprintf( pFile, " .clk( %s ),", "1\'b0" );
fprintf( pFile, " .arst( %s ),", "1\'b0" );
if ( p->vInits )
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-28 09:21:11 +0000