summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/wlc/wlc.h3
-rw-r--r--src/base/wlc/wlcAbs.c4
-rw-r--r--src/base/wlc/wlcAbs2.c76
-rw-r--r--src/base/wlc/wlcCom.c8
-rw-r--r--src/base/wlc/wlcNtk.c98
-rw-r--r--src/base/wlc/wlcReadVer.c2
6 files changed, 125 insertions, 66 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 0a17cfe6..21ba73a3 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -304,7 +304,8 @@ extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose );
extern void Wlc_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, Vec_Int_t * vPisNew );
+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 );
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 8662e509..ce6b8de9 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -173,7 +173,7 @@ Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * p, Vec_Int_t * vNodesInit )
if ( vNodes != vNodesInit )
Vec_IntFree( vNodes );
// reconstruct topological order
- pNew = Wlc_NtkDupDfs( p, 0, 1, NULL );
+ pNew = Wlc_NtkDupDfs( p, 0, 1 );
return pNew;
}
@@ -277,7 +277,7 @@ Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * p, Vec_Int_t * vPairsInit )
if ( vPairs != vPairsInit )
Vec_IntFree( vPairs );
// reconstruct topological order
- pNew = Wlc_NtkDupDfs( p, 0, 1, NULL );
+ pNew = Wlc_NtkDupDfs( p, 0, 1 );
return pNew;
}
diff --git a/src/base/wlc/wlcAbs2.c b/src/base/wlc/wlcAbs2.c
index 9da59f42..f5a7b46d 100644
--- a/src/base/wlc/wlcAbs2.c
+++ b/src/base/wlc/wlcAbs2.c
@@ -52,11 +52,11 @@ struct Wabs_Par_t_
void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
{
memset( pPars, 0, sizeof(Wlc_Par_t) );
- pPars->nBitsAdd = 16; // adder bit-width
- pPars->nBitsMul = 8; // multiplier bit-widht
- pPars->nBitsMux = 32; // MUX bit-width
- pPars->nBitsFlop = 32; // flop bit-width
- pPars->fVerbose = 0; // verbose output`
+ 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->fVerbose = 0; // verbose output`
}
/**Function*************************************************************
@@ -73,40 +73,41 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
- Wlc_Obj_t * pObj; int i;
+ Wlc_Obj_t * pObj; int i, Count[4] = {0};
Wlc_NtkForEachObj( p, pObj, i )
{
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 );
+ 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 );
+ 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 );
+ 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 );
+ Vec_BitWriteEntry( vLeaves, Wlc_ObjId(p, pObj), 1 ), Count[3]++;
continue;
}
}
+ 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 []
+ Synopsis [Marks nodes to be included in the abstracted network.]
Description []
@@ -115,7 +116,7 @@ Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
SeeAlso []
***********************************************************************/
-void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeaves, Vec_Int_t * vFlops, Vec_Int_t * vPisNew )
+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 )
@@ -123,42 +124,45 @@ void Wlc_NtkAbsMarkNodes_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Bit_t * vLeav
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( vFlops, Wlc_ObjCiId(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, vFlops, vPisNew );
+ Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkObj(p, iFanin), vLeaves, vPisOld, vPisNew, vFlops );
}
-Vec_Int_t * Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves )
+void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops )
{
- Vec_Int_t * vFlops;
- Vec_Int_t * vPisNew;
Wlc_Obj_t * pObj;
- int i, CiId, CoId;
+ int i, Count = 0;
Wlc_NtkCleanMarks( p );
- vFlops = Vec_IntAlloc( 100 );
- vPisNew = Vec_IntAlloc( 100 );
Wlc_NtkForEachCo( p, pObj, i )
- Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vFlops, vPisNew );
- Vec_IntForEachEntry( vFlops, CiId, i )
- {
- CoId = Wlc_NtkPoNum(p) + CiId - Wlc_NtkPiNum(p);
- Wlc_NtkAbsMarkNodes_rec( p, Wlc_NtkCo(p, CoId), vLeaves, vFlops, vPisNew );
- }
- Vec_IntFree( vFlops );
- return vPisNew;
+ 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 []
+ Synopsis [Derive abstraction based on the parameter values.]
Description []
@@ -169,11 +173,17 @@ Vec_Int_t * Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves )
***********************************************************************/
Wlc_Ntk_t * Wlc_NtkAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
+ 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 );
- Vec_Int_t * vPisNew = Wlc_NtkAbsMarkNodes( p, vLeaves );
- Wlc_Ntk_t * pNtkNew = Wlc_NtkDupDfs( p, 1, 1, vPisNew );
- Vec_IntFree( vPisNew );
+ Wlc_NtkAbsMarkNodes( p, vLeaves, vPisOld, vPisNew, vFlops );
Vec_BitFree( vLeaves );
+ pNtkNew = Wlc_NtkDupDfsAbs( p, vPisOld, vPisNew, vFlops );
+ Vec_IntFree( vPisOld );
+ Vec_IntFree( vPisNew );
+ Vec_IntFree( vFlops );
return pNtkNew;
}
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index cc69c636..346a9076 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -423,7 +423,7 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
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, NULL );
+ pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq );
ABC_FREE( pNtk->pName );
pNtk->pName = Abc_UtilStrsav( pName );
Wlc_AbcUpdateNtk( pAbc, pNtk );
@@ -941,6 +941,7 @@ usage:
******************************************************************************/
int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ 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();
@@ -974,9 +975,10 @@ int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
}
nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc), fVerbose );
if ( nFailed )
- printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) );
+ printf( "Invariant verification failed for %d clauses (out of %d). ", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) );
else
- printf( "Invariant verification succeeded.\n" );
+ printf( "Invariant verification succeeded. " );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return 0;
usage:
Abc_Print( -2, "usage: inv_check [-vh]\n" );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 6eab4442..86b0c17e 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -648,7 +648,7 @@ void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fTwoSides, int fVerbose
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 )
@@ -723,7 +723,7 @@ Vec_Int_t * Wlc_ReduceMarkedInitVec( Wlc_Ntk_t * p, Vec_Int_t * vInit )
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) );
+ Vec_IntWriteEntry( vInitNew, k++, Vec_IntEntry(vInit, i - Wlc_NtkPiNum(p)) );
Vec_IntShrink( vInitNew, k );
return vInitNew;
}
@@ -803,7 +803,7 @@ 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, int fMarked, int fSeq, Vec_Int_t * vPisNew )
+Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
{
Wlc_Ntk_t * pNew;
Wlc_Obj_t * pObj;
@@ -813,33 +813,14 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq, Vec_Int_t * vPi
Wlc_NtkCleanCopy( p );
pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
pNew->fSmtLib = p->fSmtLib;
- if ( vPisNew )
- {
- // duplicate marked PIs
- Wlc_NtkForEachPi( p, pObj, i )
- if ( pObj->Mark )
- Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
- // duplicated additional PIs
- Wlc_NtkForEachObjVec( vPisNew, p, pObj, i )
+ Wlc_NtkForEachCi( p, pObj, i )
+ if ( !fMarked || pObj->Mark )
{
unsigned Type = pObj->Type;
- assert( !Wlc_ObjIsPi(pObj) );
- pObj->Type = WLC_OBJ_PI;
+ if ( !fSeq ) pObj->Type = WLC_OBJ_PI;
Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
pObj->Type = Type;
}
- }
- else
- {
- Wlc_NtkForEachCi( p, pObj, i )
- 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 )
if ( !fMarked || pObj->Mark )
Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
@@ -865,7 +846,72 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq, Vec_Int_t * vPi
}
}
if ( p->pSpec )
- pNew->pSpec = Abc_UtilStrsav( 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 = Wlc_ReduceMarkedInitVec( p, p->vInits );
+ if ( p->pInits )
+ pNew->pInits = Wlc_ReduceMarkedInitStr( p, p->pInits );
+ Wlc_NtkCleanMarks( p );
+
+ if ( p->pSpec )
+ pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Wlc_NtkTransferNames( pNew, p );
return pNew;
}
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index f7546b5b..e4a65ecf 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1265,7 +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, 0, 1, NULL );
+ pNtk = Wlc_NtkDupDfs( p->pNtk, 0, 1 );
pNtk->pSpec = Abc_UtilStrsav( pFileName );
finish:
Wlc_PrsPrintErrorMessage( p );
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 18:28:45 +0000