summaryrefslogtreecommitdiffstats
path: root/src/aig/ntl
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ntl')
-rw-r--r--src/aig/ntl/module.make2
-rw-r--r--src/aig/ntl/ntl.h34
-rw-r--r--src/aig/ntl/ntlCheck.c10
-rw-r--r--src/aig/ntl/ntlCore.c10
-rw-r--r--src/aig/ntl/ntlEc.c317
-rw-r--r--src/aig/ntl/ntlExtract.c219
-rw-r--r--src/aig/ntl/ntlFraig.c164
-rw-r--r--src/aig/ntl/ntlInsert.c90
-rw-r--r--src/aig/ntl/ntlMan.c137
-rw-r--r--src/aig/ntl/ntlObj.c29
-rw-r--r--src/aig/ntl/ntlReadBlif.c6
-rw-r--r--src/aig/ntl/ntlSweep.c165
-rw-r--r--src/aig/ntl/ntlTable.c20
-rw-r--r--src/aig/ntl/ntlUtil.c208
14 files changed, 1328 insertions, 83 deletions
diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make
index d3f2cfdd..7f885a90 100644
--- a/src/aig/ntl/module.make
+++ b/src/aig/ntl/module.make
@@ -1,5 +1,6 @@
SRC += src/aig/ntl/ntlCheck.c \
src/aig/ntl/ntlCore.c \
+ src/aig/ntl/ntlEc.c \
src/aig/ntl/ntlExtract.c \
src/aig/ntl/ntlFraig.c \
src/aig/ntl/ntlInsert.c \
@@ -7,6 +8,7 @@ SRC += src/aig/ntl/ntlCheck.c \
src/aig/ntl/ntlMap.c \
src/aig/ntl/ntlObj.c \
src/aig/ntl/ntlReadBlif.c \
+ src/aig/ntl/ntlSweep.c \
src/aig/ntl/ntlTable.c \
src/aig/ntl/ntlTime.c \
src/aig/ntl/ntlUtil.c \
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 2e109f05..6b6424c0 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -54,8 +54,9 @@ typedef enum {
NTL_OBJ_PO, // 2: primary output
NTL_OBJ_LATCH, // 3: latch node
NTL_OBJ_NODE, // 4: logic node
- NTL_OBJ_BOX, // 5: white box or black box
- NTL_OBJ_VOID // 6: unused object
+ NTL_OBJ_LUT1, // 5: inverter/buffer
+ NTL_OBJ_BOX, // 6: white box or black box
+ NTL_OBJ_VOID // 7: unused object
} Ntl_Type_t;
struct Ntl_Man_t_
@@ -122,7 +123,7 @@ struct Ntl_Net_t_
Ntl_Obj_t * pDriver; // driver of the net
char nVisits; // the number of times the net is visited
char fMark; // temporary mark
- char fCompl; // complemented attribue
+ char fCompl; // complemented attribute
char pName[0]; // the name of this net
};
@@ -148,6 +149,7 @@ static inline Ntl_Mod_t * Ntl_ManRootModel( Ntl_Man_t * p ) { return Vec_P
static inline int Ntl_ModelPiNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PI]; }
static inline int Ntl_ModelPoNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PO]; }
static inline int Ntl_ModelNodeNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_NODE]; }
+static inline int Ntl_ModelLut1Num( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_LUT1]; }
static inline int Ntl_ModelLatchNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_LATCH]; }
static inline int Ntl_ModelBoxNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_BOX]; }
static inline int Ntl_ModelCiNum( Ntl_Mod_t * p ) { return p->nObjs[NTL_OBJ_PI] + p->nObjs[NTL_OBJ_LATCH]; }
@@ -228,27 +230,35 @@ static inline void Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
/*=== ntlCore.c ==========================================================*/
extern int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig );
extern int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig );
+/*=== ntlEc.c ==========================================================*/
+extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 );
+extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
/*=== ntlExtract.c ==========================================================*/
extern Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p );
-extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p );
+extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
+extern Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p );
+extern Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
extern char * Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
/*=== ntlInsert.c ==========================================================*/
-extern int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
-extern int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
-extern int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
+extern Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
+extern Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
+extern Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
/*=== ntlCheck.c ==========================================================*/
extern int Ntl_ManCheck( Ntl_Man_t * pMan );
extern int Ntl_ModelCheck( Ntl_Mod_t * pModel );
extern void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
/*=== ntlMan.c ============================================================*/
extern Ntl_Man_t * Ntl_ManAlloc( char * pFileName );
+extern void Ntl_ManCleanup( Ntl_Man_t * p );
extern Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * p );
extern Ntl_Man_t * Ntl_ManDup( Ntl_Man_t * p );
extern void Ntl_ManFree( Ntl_Man_t * p );
+extern int Ntl_ManIsComb( Ntl_Man_t * p );
extern Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
extern void Ntl_ManPrintStats( Ntl_Man_t * p );
extern Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p );
extern Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
+extern Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
extern Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
extern void Ntl_ModelFree( Ntl_Mod_t * p );
/*=== ntlMap.c ============================================================*/
@@ -263,15 +273,19 @@ extern Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel );
extern Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins );
extern Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts );
extern Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld );
+extern Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName );
extern char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
extern char * Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop );
extern char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
+/*=== ntlSweep.c ==========================================================*/
+extern Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose );
/*=== ntlTable.c ==========================================================*/
extern Ntl_Net_t * Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
extern Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
extern int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
extern int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
extern void Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
+extern int Ntl_ModelCountNets( Ntl_Mod_t * p );
/*=== ntlTime.c ==========================================================*/
extern Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p );
/*=== ntlReadBlif.c ==========================================================*/
@@ -279,9 +293,15 @@ extern Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck );
/*=== ntlWriteBlif.c ==========================================================*/
extern void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
/*=== ntlUtil.c ==========================================================*/
+extern int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
+extern int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
extern int Ntl_ManTransformCoDrivers( Ntl_Man_t * p );
+extern int Ntl_ManReconnectCoDrivers( Ntl_Man_t * p );
extern Vec_Ptr_t * Ntl_ManCollectCiNames( Ntl_Man_t * p );
extern Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p );
+extern void Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
+extern void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
+extern int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
#ifdef __cplusplus
}
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index 5973e967..9fd4af9f 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.c
@@ -31,7 +31,7 @@
/**Function*************************************************************
- Synopsis []
+ Synopsis [Checks one model.]
Description []
@@ -49,12 +49,12 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
{
if ( pNet->pName == NULL )
{
- printf( "Net %d does not have a name\n", i );
+ printf( "Net in bin %d does not have a name\n", i );
fStatus = 0;
}
if ( pNet->pDriver == NULL )
{
- printf( "Net %d (%s) does not have a driver\n", i, pNet->pName );
+ printf( "Net %s does not have a driver\n", pNet->pName );
fStatus = 0;
}
}
@@ -78,7 +78,7 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
/**Function*************************************************************
- Synopsis []
+ Synopsis [Checks the netlist.]
Description []
@@ -131,7 +131,7 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
/**Function*************************************************************
- Synopsis [Reads the verilog file.]
+ Synopsis [Fixed problems with non-driven nets in the model.]
Description []
diff --git a/src/aig/ntl/ntlCore.c b/src/aig/ntl/ntlCore.c
index fb4bb620..a5c40444 100644
--- a/src/aig/ntl/ntlCore.c
+++ b/src/aig/ntl/ntlCore.c
@@ -69,10 +69,13 @@ Aig_Man_t * Ntl_ManPerformSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdate
***********************************************************************/
int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig )
{
+ Ntl_Man_t * pNew;
Vec_Ptr_t * vMapping;
int RetValue;
vMapping = Ntl_MappingFromAig( pAig );
- RetValue = Ntl_ManInsert( p, vMapping, pAig );
+ pNew = Ntl_ManInsertMapping( p, vMapping, pAig );
+ RetValue = (pNew != NULL);
+ Ntl_ManFree( pNew );
Vec_PtrFree( vMapping );
return RetValue;
}
@@ -90,10 +93,13 @@ int Ntl_ManInsertTest( Ntl_Man_t * p, Aig_Man_t * pAig )
***********************************************************************/
int Ntl_ManInsertTestIf( Ntl_Man_t * p, Aig_Man_t * pAig )
{
+ Ntl_Man_t * pNew;
Vec_Ptr_t * vMapping;
int RetValue;
vMapping = Ntl_MappingIf( p, pAig );
- RetValue = Ntl_ManInsert( p, vMapping, pAig );
+ pNew = Ntl_ManInsertMapping( p, vMapping, pAig );
+ RetValue = (pNew != NULL);
+ Ntl_ManFree( pNew );
Vec_PtrFree( vMapping );
return RetValue;
}
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
new file mode 100644
index 00000000..6b7b1a41
--- /dev/null
+++ b/src/aig/ntl/ntlEc.c
@@ -0,0 +1,317 @@
+/**CFile****************************************************************
+
+ FileName [ntlEc.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Equivalence checking procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ntlEc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Adds PIs to both models, so that they have the same PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManCreateMissingInputs( Ntl_Mod_t * p1, Ntl_Mod_t * p2, int fSeq )
+{
+ Ntl_Obj_t * pObj;
+ Ntl_Net_t * pNet;
+ int i;
+ Ntl_ModelForEachPi( p1, pObj, i )
+ {
+ pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
+ if ( pNet == NULL )
+ Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName );
+ }
+ Ntl_ModelForEachPi( p2, pObj, i )
+ {
+ pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName );
+ if ( pNet == NULL )
+ Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName );
+ }
+ if ( !fSeq )
+ {
+ Ntl_ModelForEachLatch( p1, pObj, i )
+ {
+ pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
+ if ( pNet == NULL )
+ Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName );
+ }
+ Ntl_ModelForEachLatch( p2, pObj, i )
+ {
+ pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName );
+ if ( pNet == NULL )
+ Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName );
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates arrays of combinational inputs in the same order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManDeriveCommonCis( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
+{
+ Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1);
+ Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2);
+ Ntl_Obj_t * pObj;
+ Ntl_Net_t * pNet;
+ int i;
+ if ( fSeq )
+ assert( Ntl_ModelPiNum(p1) == Ntl_ModelPiNum(p2) );
+ else
+ assert( Ntl_ModelCiNum(p1) == Ntl_ModelCiNum(p2) );
+ // order the CIs
+ Vec_PtrClear( pMan1->vCis );
+ Vec_PtrClear( pMan2->vCis );
+ Ntl_ModelForEachPi( p1, pObj, i )
+ {
+ pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
+ if ( pNet == NULL )
+ {
+ printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
+ return;
+ }
+ Vec_PtrPush( pMan1->vCis, pObj );
+ Vec_PtrPush( pMan2->vCis, pNet->pDriver );
+ }
+ if ( !fSeq )
+ {
+ Ntl_ModelForEachLatch( p1, pObj, i )
+ {
+ pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
+ if ( pNet == NULL )
+ {
+ printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
+ return;
+ }
+ Vec_PtrPush( pMan1->vCis, pObj );
+ Vec_PtrPush( pMan2->vCis, pNet->pDriver );
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates arrays of combinational outputs in the same order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManDeriveCommonCos( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
+{
+ Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1);
+ Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2);
+ Ntl_Obj_t * pObj;
+ Ntl_Net_t * pNet;
+ int i;
+// if ( fSeq )
+// assert( Ntl_ModelPoNum(p1) == Ntl_ModelPoNum(p2) );
+// else
+// assert( Ntl_ModelCoNum(p1) == Ntl_ModelCoNum(p2) );
+ // remember PO in the corresponding net of the second design
+ Ntl_ModelForEachPo( p2, pObj, i )
+ Ntl_ObjFanin0(pObj)->pCopy = pObj;
+ // order the COs
+ Vec_PtrClear( pMan1->vCos );
+ Vec_PtrClear( pMan2->vCos );
+ Ntl_ModelForEachPo( p1, pObj, i )
+ {
+ pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName );
+ if ( pNet == NULL )
+ {
+ printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n",
+ Ntl_ObjFanin0(pObj)->pName );
+ continue;
+ }
+ Vec_PtrPush( pMan1->vCos, pObj );
+ Vec_PtrPush( pMan2->vCos, pNet->pCopy );
+ }
+ if ( !fSeq )
+ {
+ Ntl_ModelForEachLatch( p2, pObj, i )
+ Ntl_ObjFanin0(pObj)->pCopy = pObj;
+ Ntl_ModelForEachLatch( p1, pObj, i )
+ {
+ pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName );
+ if ( pNet == NULL )
+ {
+ printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n",
+ Ntl_ObjFanin0(pObj)->pName );
+ continue;
+ }
+ Vec_PtrPush( pMan1->vCos, pObj );
+ Vec_PtrPush( pMan2->vCos, pNet->pCopy );
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares AIGs for combinational equivalence checking.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan1, Aig_Man_t ** ppMan2 )
+{
+ Ntl_Man_t * pMan1, * pMan2;
+ Ntl_Mod_t * pModel1, * pModel2;
+ *ppMan1 = NULL;
+ *ppMan2 = NULL;
+ // read the netlists
+ pMan1 = Ioa_ReadBlif( pFileName1, 1 );
+ pMan2 = Ioa_ReadBlif( pFileName2, 1 );
+ if ( !pMan1 || !pMan2 )
+ {
+ if ( pMan1 ) Ntl_ManFree( pMan1 );
+ if ( pMan2 ) Ntl_ManFree( pMan2 );
+ printf( "Ntl_ManPrepareCec(): Reading designs from file has failed.\n" );
+ return;
+ }
+ // make sure they are compatible
+ pModel1 = Ntl_ManRootModel( pMan1 );
+ pModel2 = Ntl_ManRootModel( pMan2 );
+ if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) )
+ {
+ printf( "Warning: The number of inputs in the designs is different (%d and %d).\n",
+ Ntl_ModelCiNum(pModel1), Ntl_ModelCiNum(pModel2) );
+ }
+ if ( Ntl_ModelCoNum(pModel1) != Ntl_ModelCoNum(pModel2) )
+ {
+ printf( "Warning: The number of outputs in the designs is different (%d and %d).\n",
+ Ntl_ModelCoNum(pModel1), Ntl_ModelCoNum(pModel2) );
+ }
+ // normalize inputs/outputs
+ Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 );
+ Ntl_ManDeriveCommonCis( pMan1, pMan2, 0 );
+ Ntl_ManDeriveCommonCos( pMan1, pMan2, 0 );
+ if ( Vec_PtrSize(pMan1->vCos) == 0 )
+ {
+ printf( "Ntl_ManPrepareCec(): There is no identically-named primary outputs to compare.\n" );
+ if ( pMan1 ) Ntl_ManFree( pMan1 );
+ if ( pMan2 ) Ntl_ManFree( pMan2 );
+ return;
+ }
+ // derive AIGs
+ *ppMan1 = Ntl_ManCollapseForCec( pMan1 );
+ *ppMan2 = Ntl_ManCollapseForCec( pMan2 );
+ // cleanup
+ Ntl_ManFree( pMan1 );
+ Ntl_ManFree( pMan2 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares AIGs for sequential equivalence checking.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
+{
+ Aig_Man_t * pAig;
+ Ntl_Man_t * pMan1, * pMan2;
+ Ntl_Mod_t * pModel1, * pModel2;
+ // read the netlists
+ pMan1 = Ioa_ReadBlif( pFileName1, 1 );
+ pMan2 = Ioa_ReadBlif( pFileName2, 1 );
+ if ( !pMan1 || !pMan2 )
+ {
+ if ( pMan1 ) Ntl_ManFree( pMan1 );
+ if ( pMan2 ) Ntl_ManFree( pMan2 );
+ printf( "Ntl_ManPrepareSec(): Reading designs from file has failed.\n" );
+ return NULL;
+ }
+ // make sure they are compatible
+ pModel1 = Ntl_ManRootModel( pMan1 );
+ pModel2 = Ntl_ManRootModel( pMan2 );
+ if ( Ntl_ModelLatchNum(pModel1) == 0 || Ntl_ModelLatchNum(pModel2) == 0 )
+ {
+ if ( pMan1 ) Ntl_ManFree( pMan1 );
+ if ( pMan2 ) Ntl_ManFree( pMan2 );
+ printf( "Ntl_ManPrepareSec(): The designs have no latches. Used combinational command \"*cec\".\n" );
+ return NULL;
+ }
+ if ( Ntl_ModelPiNum(pModel1) != Ntl_ModelPiNum(pModel2) )
+ {
+ printf( "Warning: The number of inputs in the designs is different (%d and %d).\n",
+ Ntl_ModelPiNum(pModel1), Ntl_ModelPiNum(pModel2) );
+ }
+ if ( Ntl_ModelPoNum(pModel1) != Ntl_ModelPoNum(pModel2) )
+ {
+ printf( "Warning: The number of outputs in the designs is different (%d and %d).\n",
+ Ntl_ModelPoNum(pModel1), Ntl_ModelPoNum(pModel2) );
+ }
+ // normalize inputs/outputs
+ Ntl_ManCreateMissingInputs( pModel1, pModel2, 1 );
+ Ntl_ManDeriveCommonCis( pMan1, pMan2, 1 );
+ Ntl_ManDeriveCommonCos( pMan1, pMan2, 1 );
+ if ( Vec_PtrSize(pMan1->vCos) == 0 )
+ {
+ printf( "Ntl_ManPrepareSec(): There is no identically-named primary outputs to compare.\n" );
+ if ( pMan1 ) Ntl_ManFree( pMan1 );
+ if ( pMan2 ) Ntl_ManFree( pMan2 );
+ return NULL;
+ }
+ // derive AIGs
+ pAig = Ntl_ManCollapseForSec( pMan1, pMan2 );
+ // cleanup
+ pMan1->pAig = pMan2->pAig = NULL;
+ Ntl_ManFree( pMan1 );
+ Ntl_ManFree( pMan2 );
+ return pAig;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 848f113a..9c3666ab 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -467,6 +467,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
Ntl_Obj_t * pObj;
Ntl_Net_t * pNet;
int i, nUselessObjects;
+ Ntl_ManCleanup( p );
assert( Vec_PtrSize(p->vCis) == 0 );
assert( Vec_PtrSize(p->vCos) == 0 );
assert( Vec_PtrSize(p->vNodes) == 0 );
@@ -540,7 +541,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
Aig_ObjCreatePo( p->pAig, pNet->pCopy );
}
// report the number of dangling objects
- nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
+ nUselessObjects = Ntl_ModelNodeNum(pRoot) + Ntl_ModelLut1Num(pRoot) + Ntl_ModelBoxNum(pRoot) - Vec_PtrSize(p->vNodes);
if ( nUselessObjects )
printf( "The number of nodes that do not feed into POs = %d.\n", nUselessObjects );
// cleanup the AIG
@@ -658,7 +659,7 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
+Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
{
Aig_Man_t * pAig;
Ntl_Mod_t * pRoot;
@@ -694,6 +695,8 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
assert( Ntl_ObjFanoutNum(pObj) == 1 );
pNet = Ntl_ObjFanout0(pObj);
pNet->pCopy = Aig_ObjCreatePi( p->pAig );
+ if ( fSeq && (pObj->LatchId & 3) == 1 )
+ pNet->pCopy = Aig_Not(pNet->pCopy);
if ( pNet->nVisits )
{
printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" );
@@ -721,6 +724,60 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
return 0;
}
+ if ( fSeq && (pObj->LatchId & 3) == 1 )
+ Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) );
+ else
+ Aig_ObjCreatePo( p->pAig, pNet->pCopy );
+ }
+ // cleanup the AIG
+ Aig_ManCleanup( p->pAig );
+ pAig = p->pAig; p->pAig = NULL;
+ return pAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives AIG for CEC.]
+
+ Description [Uses CIs/COs collected in the internal arrays.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p )
+{
+ Aig_Man_t * pAig;
+ Ntl_Obj_t * pObj;
+ Ntl_Net_t * pNet;
+ int i;
+ // create the manager
+ p->pAig = Aig_ManStart( 10000 );
+ p->pAig->pName = Aig_UtilStrsav( p->pName );
+ p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
+ // set the inputs
+ Ntl_ManForEachCiNet( p, pObj, i )
+ {
+ assert( Ntl_ObjFanoutNum(pObj) == 1 );
+ pNet = Ntl_ObjFanout0(pObj);
+ pNet->pCopy = Aig_ObjCreatePi( p->pAig );
+ if ( pNet->nVisits )
+ {
+ printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" );
+ return 0;
+ }
+ pNet->nVisits = 2;
+ }
+ // derive the outputs
+ Ntl_ManForEachCoNet( p, pObj, i )
+ {
+ pNet = Ntl_ObjFanin0(pObj);
+ if ( !Ntl_ManCollapse_rec( p, pNet ) )
+ {
+ printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" );
+ return 0;
+ }
Aig_ObjCreatePo( p->pAig, pNet->pCopy );
}
// cleanup the AIG
@@ -731,6 +788,164 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
/**Function*************************************************************
+ Synopsis [Performs DFS.]
+
+ Description [Checks for combinational loops. Collects PI/PO nets.
+ Collects nodes in the topological order.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
+{
+ Aig_Man_t * pAig;
+ Aig_Obj_t * pMiter;
+ Ntl_Mod_t * pRoot1, * pRoot2;
+ Ntl_Obj_t * pObj;
+ Ntl_Net_t * pNet;
+ Vec_Ptr_t * vPairs;
+ int i;
+ assert( Vec_PtrSize(p1->vCis) > 0 );
+ assert( Vec_PtrSize(p1->vCos) > 0 );
+ assert( Vec_PtrSize(p1->vCis) == Vec_PtrSize(p2->vCis) );
+ assert( Vec_PtrSize(p1->vCos) == Vec_PtrSize(p2->vCos) );
+
+ // create the manager
+ pAig = p1->pAig = p2->pAig = Aig_ManStart( 10000 );
+ pAig->pName = Aig_UtilStrsav( p1->pName );
+ pAig->pSpec = Aig_UtilStrsav( p1->pSpec );
+ vPairs = Vec_PtrStart( 2 * Vec_PtrSize(p1->vCos) );
+ // placehoder output to be used later for the miter output
+ Aig_ObjCreatePo( pAig, Aig_ManConst1(pAig) );
+
+ /////////////////////////////////////////////////////
+ // primary inputs
+ Ntl_ManForEachCiNet( p1, pObj, i )
+ {
+ assert( Ntl_ObjFanoutNum(pObj) == 1 );
+ pNet = Ntl_ObjFanout0(pObj);
+ pNet->pCopy = Aig_ObjCreatePi( pAig );
+ if ( pNet->nVisits )
+ {
+ printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" );
+ return 0;
+ }
+ pNet->nVisits = 2;
+ }
+ // latch outputs
+ pRoot1 = Ntl_ManRootModel(p1);
+ Ntl_ModelForEachLatch( pRoot1, pObj, i )
+ {
+ assert( Ntl_ObjFanoutNum(pObj) == 1 );
+ pNet = Ntl_ObjFanout0(pObj);
+ pNet->pCopy = Aig_ObjCreatePi( pAig );
+ if ( (pObj->LatchId & 3) == 1 )
+ pNet->pCopy = Aig_Not(pNet->pCopy);
+ if ( pNet->nVisits )
+ {
+ printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" );
+ return 0;
+ }
+ pNet->nVisits = 2;
+ }
+ // derive the outputs
+ Ntl_ManForEachCoNet( p1, pObj, i )
+ {
+ pNet = Ntl_ObjFanin0(pObj);
+ if ( !Ntl_ManCollapse_rec( p1, pNet ) )
+ {
+ printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
+ return 0;
+ }
+// Aig_ObjCreatePo( pAig, pNet->pCopy );
+ Vec_PtrWriteEntry( vPairs, 2 * i, pNet->pCopy );
+ }
+ // visit the nodes starting from latch inputs outputs
+ Ntl_ModelForEachLatch( pRoot1, pObj, i )
+ {
+ pNet = Ntl_ObjFanin0(pObj);
+ if ( !Ntl_ManCollapse_rec( p1, pNet ) )
+ {
+ printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
+ return 0;
+ }
+ if ( (pObj->LatchId & 3) == 1 )
+ Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) );
+ else
+ Aig_ObjCreatePo( pAig, pNet->pCopy );
+ }
+
+ /////////////////////////////////////////////////////
+ // primary inputs
+ Ntl_ManForEachCiNet( p2, pObj, i )
+ {
+ assert( Ntl_ObjFanoutNum(pObj) == 1 );
+ pNet = Ntl_ObjFanout0(pObj);
+ pNet->pCopy = Aig_ManPi( pAig, i );
+ if ( pNet->nVisits )
+ {
+ printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" );
+ return 0;
+ }
+ pNet->nVisits = 2;
+ }
+ // latch outputs
+ pRoot2 = Ntl_ManRootModel(p2);
+ Ntl_ModelForEachLatch( pRoot2, pObj, i )
+ {
+ assert( Ntl_ObjFanoutNum(pObj) == 1 );
+ pNet = Ntl_ObjFanout0(pObj);
+ pNet->pCopy = Aig_ObjCreatePi( pAig );
+ if ( (pObj->LatchId & 3) == 1 )
+ pNet->pCopy = Aig_Not(pNet->pCopy);
+ if ( pNet->nVisits )
+ {
+ printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" );
+ return 0;
+ }
+ pNet->nVisits = 2;
+ }
+ // derive the outputs
+ Ntl_ManForEachCoNet( p2, pObj, i )
+ {
+ pNet = Ntl_ObjFanin0(pObj);
+ if ( !Ntl_ManCollapse_rec( p2, pNet ) )
+ {
+ printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
+ return 0;
+ }
+// Aig_ObjCreatePo( pAig, pNet->pCopy );
+ Vec_PtrWriteEntry( vPairs, 2 * i + 1, pNet->pCopy );
+ }
+ // visit the nodes starting from latch inputs outputs
+ Ntl_ModelForEachLatch( pRoot2, pObj, i )
+ {
+ pNet = Ntl_ObjFanin0(pObj);
+ if ( !Ntl_ManCollapse_rec( p2, pNet ) )
+ {
+ printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
+ return 0;
+ }
+ if ( (pObj->LatchId & 3) == 1 )
+ Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) );
+ else
+ Aig_ObjCreatePo( pAig, pNet->pCopy );
+ }
+
+ /////////////////////////////////////////////////////
+ pMiter = Aig_Miter(pAig, vPairs);
+ Vec_PtrFree( vPairs );
+ Aig_ObjPatchFanin0( pAig, Aig_ManPo(pAig,0), pMiter );
+ pAig->nRegs = Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 );
+ Aig_ManCleanup( pAig );
+ return pAig;
+}
+
+
+/**Function*************************************************************
+
Synopsis [Increments reference counter of the net.]
Description []
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 7153f081..8a172e6c 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "ntl.h"
+#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -30,10 +31,10 @@
/**Function*************************************************************
- Synopsis [Returns AIG with WB after fraiging.]
+ Synopsis [Transfers equivalence class info from pAigCol to pAig.]
- Description [pAig points to the nodes of pNew derived using it.
- pNew points to the nodes of pAigCol derived using it.]
+ Description [pAig points to the nodes of netlist (pNew) derived using it.
+ pNew points to the nodes of the collapsed AIG (pAigCol) derived using it.]
SideEffects []
@@ -59,6 +60,9 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
}
// create mapping from the collapsed manager into the original manager
+ // (each node in the collapsed manager may have more than one equivalent node
+ // in the original manager; this procedure finds the first node in the original
+ // manager that is equivalent to the given node in the collapsed manager)
pMapBack = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAigCol) );
memset( pMapBack, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAigCol) );
Aig_ManForEachObj( pAig, pObj, i )
@@ -115,16 +119,15 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC
assert( pAig->pReprs == NULL );
// create a new netlist whose nodes are in 1-to-1 relationship with AIG
- pNew = Ntl_ManDup( p );
- if ( !Ntl_ManInsertAig( pNew, pAig ) )
+ pNew = Ntl_ManInsertAig( p, pAig );
+ if ( pNew == NULL )
{
- Ntl_ManFree( pNew );
printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
return NULL;
}
// collapse the AIG
- pAigCol = Ntl_ManCollapse( pNew );
+ pAigCol = Ntl_ManCollapse( pNew, 0 );
// perform fraiging for the given design
if ( nPartSize == 0 )
nPartSize = Aig_ManPoNum(pAigCol);
@@ -148,6 +151,153 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC
return pTemp;
}
+/**Function*************************************************************
+
+ Synopsis [Performs sequential cleanup.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManScl( Ntl_Man_t * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
+{
+ Ntl_Man_t * pNew;
+ Aig_Man_t * pAigCol, * pTemp;
+ assert( pAig->pReprs == NULL );
+
+ // create a new netlist whose nodes are in 1-to-1 relationship with AIG
+ pNew = Ntl_ManInsertAig( p, pAig );
+ if ( pNew == NULL )
+ {
+ printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
+ return NULL;
+ }
+
+ // collapse the AIG
+ pAigCol = Ntl_ManCollapse( pNew, 1 );
+ // perform fraiging for the given design
+ pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+ pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
+ Aig_ManStop( pTemp );
+
+ // transfer equivalence classes to the original AIG
+ pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
+ pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
+ // cleanup
+ Aig_ManStop( pAigCol );
+ Ntl_ManFree( pNew );
+
+ // derive the new AIG
+ pTemp = Aig_ManDupRepresDfs( pAig );
+ // duplicate the timing manager
+ if ( pAig->pManTime )
+ pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
+ // reset levels
+ Aig_ManChoiceLevel( pTemp );
+ return pTemp;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns AIG with WB after fraiging.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, int fVerbose )
+{
+ Ntl_Man_t * pNew;
+ Aig_Man_t * pAigCol, * pTemp;
+ assert( pAig->pReprs == NULL );
+
+ // create a new netlist whose nodes are in 1-to-1 relationship with AIG
+ pNew = Ntl_ManInsertAig( p, pAig );
+ if ( pNew == NULL )
+ {
+ printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
+ return NULL;
+ }
+
+ // collapse the AIG
+ pAigCol = Ntl_ManCollapse( pNew, 1 );
+ // perform fraiging for the given design
+ pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+ pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
+ Aig_ManStop( pTemp );
+
+ // transfer equivalence classes to the original AIG
+ pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
+ pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
+ // cleanup
+ Aig_ManStop( pAigCol );
+ Ntl_ManFree( pNew );
+
+ // derive the new AIG
+ pTemp = Aig_ManDupRepresDfs( pAig );
+ // duplicate the timing manager
+ if ( pAig->pManTime )
+ pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
+ // reset levels
+ Aig_ManChoiceLevel( pTemp );
+ return pTemp;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns AIG with WB after fraiging.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars )
+{
+ Ntl_Man_t * pNew;
+ Aig_Man_t * pAigCol, * pTemp;
+ assert( pAig->pReprs == NULL );
+
+ // create a new netlist whose nodes are in 1-to-1 relationship with AIG
+ pNew = Ntl_ManInsertAig( p, pAig );
+ if ( pNew == NULL )
+ {
+ printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
+ return NULL;
+ }
+
+ // collapse the AIG
+ pAigCol = Ntl_ManCollapse( pNew, 1 );
+ // perform fraiging for the given design
+ pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
+ pTemp = Fra_FraigInduction( pAigCol, pPars );
+ Aig_ManStop( pTemp );
+
+ // transfer equivalence classes to the original AIG
+ pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
+ pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
+ // cleanup
+ Aig_ManStop( pAigCol );
+ Ntl_ManFree( pNew );
+
+ // derive the new AIG
+ pTemp = Aig_ManDupRepresDfs( pAig );
+ // duplicate the timing manager
+ if ( pAig->pManTime )
+ pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
+ // reset levels
+ Aig_ManChoiceLevel( pTemp );
+ return pTemp;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 10b83660..77fb606a 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -40,7 +40,7 @@
SeeAlso []
***********************************************************************/
-int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
+Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
{
char Buffer[100];
Vec_Ptr_t * vCopies;
@@ -50,16 +50,14 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
Ntl_Net_t * pNet, * pNetCo;
Ntl_Lut_t * pLut;
int i, k, nDigits;
+ assert( Vec_PtrSize(p->vCis) == Aig_ManPiNum(pAig) );
+ assert( Vec_PtrSize(p->vCos) == Aig_ManPoNum(pAig) );
+ p = Ntl_ManStartFrom( p );
+ pRoot = Ntl_ManRootModel( p );
+ assert( Ntl_ModelNodeNum(pRoot) == 0 );
// map the AIG back onto the design
Ntl_ManForEachCiNet( p, pNet, i )
pNet->pCopy = Aig_ManPi( pAig, i );
- Ntl_ManForEachCoNet( p, pNet, i )
- pNet->pCopy = Aig_ObjChild0( Aig_ManPo( pAig, i ) );
- // remove old nodes
- pRoot = Ntl_ManRootModel( p );
- Ntl_ModelForEachNode( pRoot, pNode, i )
- Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
- pRoot->nObjs[NTL_OBJ_NODE] = 0;
// start mapping of AIG nodes into their copies
vCopies = Vec_PtrStart( Aig_ManObjNumMax(pAig) );
Ntl_ManForEachCiNet( p, pNet, i )
@@ -101,19 +99,19 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
Vec_IntFree( vCover );
// mark CIs and outputs of the registers
Ntl_ManForEachCiNet( p, pNetCo, i )
- pNetCo->nVisits = 101; // using "101" is harmless because nVisits can only be 0, 1 or 2
+ pNetCo->fMark = 1;
// update the CO pointers
Ntl_ManForEachCoNet( p, pNetCo, i )
{
- if ( pNetCo->nVisits == 101 )
+ if ( pNetCo->fMark )
continue;
- pNetCo->nVisits = 101;
+ pNetCo->fMark = 1;
pNet = Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pCopy)->Id );
pNode = Ntl_ModelCreateNode( pRoot, 1 );
pNode->pSop = Aig_IsComplement(pNetCo->pCopy)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
- pNetCo->pDriver = NULL;
+ assert( pNetCo->pDriver == NULL );
if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
{
printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
@@ -121,7 +119,11 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
}
}
Vec_PtrFree( vCopies );
- return 1;
+ // clean CI/CO marks
+ Ntl_ManUnmarkCiCoNets( p );
+ if ( !Ntl_ManCheck( p ) )
+ printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
+ return p;
}
/**Function*************************************************************
@@ -135,7 +137,7 @@ int Ntl_ManInsert( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig )
SeeAlso []
***********************************************************************/
-int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
+Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
{
char Buffer[100];
Ntl_Mod_t * pRoot;
@@ -145,17 +147,13 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
int i, nDigits, Counter;
assert( Vec_PtrSize(p->vCis) == Aig_ManPiNum(pAig) );
assert( Vec_PtrSize(p->vCos) == Aig_ManPoNum(pAig) );
+ p = Ntl_ManStartFrom( p );
+ pRoot = Ntl_ManRootModel( p );
+ assert( Ntl_ModelNodeNum(pRoot) == 0 );
// set the correspondence between the PI/PO nodes
Aig_ManCleanData( pAig );
Ntl_ManForEachCiNet( p, pNet, i )
Aig_ManPi( pAig, i )->pData = pNet;
-// Ntl_ManForEachCoNet( p, pNet, i )
-// Nwk_ManCo( pNtk, i )->pCopy = pNet;
- // remove old nodes
- pRoot = Ntl_ManRootModel( p );
- Ntl_ModelForEachNode( pRoot, pNode, i )
- Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
- pRoot->nObjs[NTL_OBJ_NODE] = 0;
// create constant node if needed
if ( Aig_ManConst1(pAig)->nRefs > 0 )
{
@@ -213,13 +211,13 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
}
// mark CIs and outputs of the registers
Ntl_ManForEachCiNet( p, pNetCo, i )
- pNetCo->nVisits = 101;
+ pNetCo->fMark = 1;
// update the CO pointers
Ntl_ManForEachCoNet( p, pNetCo, i )
{
- if ( pNetCo->nVisits == 101 )
+ if ( pNetCo->fMark )
continue;
- pNetCo->nVisits = 101;
+ pNetCo->fMark = 1;
// get the corresponding PO and its driver
pObj = Aig_ManPo( pAig, i );
pFanin = Aig_ObjFanin0( pObj );
@@ -229,14 +227,18 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
pNode->pSop = Aig_ObjFaninC0(pObj)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
- pNetCo->pDriver = NULL;
+ assert( pNetCo->pDriver == NULL );
if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
{
- printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+ printf( "Ntl_ManInsertAig(): Internal error: PO net has more than one fanin.\n" );
return 0;
}
}
- return 1;
+ // clean CI/CO marks
+ Ntl_ManUnmarkCiCoNets( p );
+ if ( !Ntl_ManCheck( p ) )
+ printf( "Ntl_ManInsertAig: The check has failed for design %s.\n", p->pName );
+ return p;
}
@@ -251,7 +253,7 @@ int Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
SeeAlso []
***********************************************************************/
-int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
+Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
{
char Buffer[100];
Vec_Ptr_t * vObjs;
@@ -265,16 +267,12 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
unsigned * pTruth;
assert( Vec_PtrSize(p->vCis) == Nwk_ManCiNum(pNtk) );
assert( Vec_PtrSize(p->vCos) == Nwk_ManCoNum(pNtk) );
+ p = Ntl_ManStartFrom( p );
+ pRoot = Ntl_ManRootModel( p );
+ assert( Ntl_ModelNodeNum(pRoot) == 0 );
// set the correspondence between the PI/PO nodes
Ntl_ManForEachCiNet( p, pNet, i )
Nwk_ManCi( pNtk, i )->pCopy = pNet;
-// Ntl_ManForEachCoNet( p, pNet, i )
-// Nwk_ManCo( pNtk, i )->pCopy = pNet;
- // remove old nodes
- pRoot = Ntl_ManRootModel( p );
- Ntl_ModelForEachNode( pRoot, pNode, i )
- Vec_PtrWriteEntry( pRoot->vObjs, pNode->Id, NULL );
- pRoot->nObjs[NTL_OBJ_NODE] = 0;
// create a new node for each LUT
vTruth = Vec_IntAlloc( 1 << 16 );
vCover = Vec_IntAlloc( 1 << 16 );
@@ -298,7 +296,7 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
pNet = pFanin->pCopy;
if ( pNet == NULL )
{
- printf( "Ntl_ManInsert(): Internal error: Net not found.\n" );
+ printf( "Ntl_ManInsertNtk(): Internal error: Net not found.\n" );
return 0;
}
Ntl_ObjSetFanin( pNode, pNet, k );
@@ -307,13 +305,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
sprintf( Buffer, "lut%0*d", nDigits, i );
if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
{
- printf( "Ntl_ManInsert(): Internal error: Intermediate net name is not unique.\n" );
+ printf( "Ntl_ManInsertNtk(): Internal error: Intermediate net name is not unique.\n" );
return 0;
}
pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
{
- printf( "Ntl_ManInsert(): Internal error: Net has more than one fanin.\n" );
+ printf( "Ntl_ManInsertNtk(): Internal error: Net has more than one fanin.\n" );
return 0;
}
pObj->pCopy = pNet;
@@ -323,13 +321,13 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
Vec_IntFree( vTruth );
// mark CIs and outputs of the registers
Ntl_ManForEachCiNet( p, pNetCo, i )
- pNetCo->nVisits = 101;
+ pNetCo->fMark = 1;
// update the CO pointers
Ntl_ManForEachCoNet( p, pNetCo, i )
{
- if ( pNetCo->nVisits == 101 )
+ if ( pNetCo->fMark )
continue;
- pNetCo->nVisits = 101;
+ pNetCo->fMark = 1;
// get the corresponding PO and its driver
pObj = Nwk_ManCo( pNtk, i );
pFanin = Nwk_ObjFanin0( pObj );
@@ -339,14 +337,18 @@ int Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pCopy)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
- pNetCo->pDriver = NULL;
+ assert( pNetCo->pDriver == NULL );
if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
{
- printf( "Ntl_ManInsert(): Internal error: PO net has more than one fanin.\n" );
+ printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" );
return 0;
}
}
- return 1;
+ // clean CI/CO marks
+ Ntl_ManUnmarkCiCoNets( p );
+ if ( !Ntl_ManCheck( p ) )
+ printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
+ return p;
}
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 83219df7..82131091 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -61,7 +61,36 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
/**Function*************************************************************
- Synopsis [Duplicates the interface of the top level model.]
+ Synopsis [Cleanups extended representation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManCleanup( Ntl_Man_t * p )
+{
+ Vec_PtrClear( p->vCis );
+ Vec_PtrClear( p->vCos );
+ Vec_PtrClear( p->vNodes );
+ Vec_IntClear( p->vBox1Cos );
+ if ( p->pAig )
+ {
+ Aig_ManStop( p->pAig );
+ p->pAig = NULL;
+ }
+ if ( p->pManTime )
+ {
+ Tim_ManStop( p->pManTime );
+ p->pManTime = NULL;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Duplicates the design without the nodes of the root model.]
Description []
@@ -72,12 +101,36 @@ Ntl_Man_t * Ntl_ManAlloc( char * pFileName )
***********************************************************************/
Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld )
{
- return NULL;
+ Ntl_Man_t * pNew;
+ Ntl_Mod_t * pModel;
+ Ntl_Obj_t * pBox;
+ Ntl_Net_t * pNet;
+ int i, k;
+ pNew = Ntl_ManAlloc( pOld->pSpec );
+ Vec_PtrForEachEntry( pOld->vModels, pModel, i )
+ if ( i == 0 )
+ {
+ Ntl_ManMarkCiCoNets( pOld );
+ pModel->pCopy = Ntl_ModelStartFrom( pNew, pModel );
+ Ntl_ManUnmarkCiCoNets( pOld );
+ }
+ else
+ pModel->pCopy = Ntl_ModelDup( pNew, pModel );
+ Vec_PtrForEachEntry( pOld->vModels, pModel, i )
+ Ntl_ModelForEachBox( pModel, pBox, k )
+ ((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy;
+ Ntl_ManForEachCiNet( pOld, pNet, i )
+ Vec_PtrPush( pNew->vCis, pNet->pCopy );
+ Ntl_ManForEachCoNet( pOld, pNet, i )
+ Vec_PtrPush( pNew->vCos, pNet->pCopy );
+ if ( pOld->pManTime )
+ pNew->pManTime = Tim_ManDup( pOld->pManTime, 0 );
+ return pNew;
}
/**Function*************************************************************
- Synopsis [Duplicates the interface of the top level model.]
+ Synopsis [Duplicates the design.]
Description []
@@ -144,6 +197,22 @@ void Ntl_ManFree( Ntl_Man_t * p )
/**Function*************************************************************
+ Synopsis [Returns 1 if the design is combinational.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ManIsComb( Ntl_Man_t * p )
+{
+ return Ntl_ModelLatchNum(Ntl_ManRootModel(p)) == 0;
+}
+
+/**Function*************************************************************
+
Synopsis [Find the model with the given name.]
Description []
@@ -178,15 +247,18 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
{
Ntl_Mod_t * pRoot;
pRoot = Ntl_ManRootModel( p );
- printf( "%-15s : ", p->pName );
- printf( "pi = %5d ", Ntl_ModelPiNum(pRoot) );
- printf( "po = %5d ", Ntl_ModelPoNum(pRoot) );
- printf( "lat = %5d ", Ntl_ModelLatchNum(pRoot) );
- printf( "node = %5d ", Ntl_ModelNodeNum(pRoot) );
- printf( "box = %4d ", Ntl_ModelBoxNum(pRoot) );
- printf( "mod = %3d", Vec_PtrSize(p->vModels) );
+ printf( "%-15s : ", p->pName );
+ printf( "pi = %5d ", Ntl_ModelPiNum(pRoot) );
+ printf( "po = %5d ", Ntl_ModelPoNum(pRoot) );
+ printf( "lat = %5d ", Ntl_ModelLatchNum(pRoot) );
+ printf( "node = %5d ", Ntl_ModelNodeNum(pRoot) );
+ printf( "inv/buf = %5d ", Ntl_ModelLut1Num(pRoot) );
+ printf( "box = %4d ", Ntl_ModelBoxNum(pRoot) );
+ printf( "mod = %3d ", Vec_PtrSize(p->vModels) );
+ printf( "net = %d", Ntl_ModelCountNets(pRoot) );
printf( "\n" );
fflush( stdout );
+ assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) );
}
/**Function*************************************************************
@@ -237,6 +309,50 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
/**Function*************************************************************
+ Synopsis [Duplicates the model without nodes but with CI/CO nets.]
+
+ Description [The CI/CO nets of the old model should be marked before
+ calling this procedure.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
+{
+ Ntl_Mod_t * pModelNew;
+ Ntl_Net_t * pNet;
+ Ntl_Obj_t * pObj;
+ int i, k;
+ pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+ Ntl_ModelForEachNet( pModelOld, pNet, i )
+ if ( pNet->fMark )
+ pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+ else
+ pNet->pCopy = NULL;
+ Ntl_ModelForEachObj( pModelOld, pObj, i )
+ {
+ if ( Ntl_ObjIsNode(pObj) )
+ continue;
+ pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
+ Ntl_ObjForEachFanin( pObj, pNet, k )
+ if ( pNet->pCopy != NULL )
+ Ntl_ObjSetFanin( pObj->pCopy, pNet->pCopy, k );
+ Ntl_ObjForEachFanout( pObj, pNet, k )
+ if ( pNet->pCopy != NULL )
+ Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k );
+ if ( Ntl_ObjIsLatch(pObj) )
+ ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
+ }
+ pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
+ pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;
+ pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL;
+ return pModelNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Duplicates the model.]
Description []
@@ -286,6 +402,7 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
***********************************************************************/
void Ntl_ModelFree( Ntl_Mod_t * p )
{
+ assert( Ntl_ManCheckNetsAreNotMarked(p) );
if ( p->vRequireds ) Vec_IntFree( p->vRequireds );
if ( p->vArrivals ) Vec_IntFree( p->vArrivals );
if ( p->vDelays ) Vec_IntFree( p->vDelays );
diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c
index ad43623a..68b5cfe8 100644
--- a/src/aig/ntl/ntlObj.c
+++ b/src/aig/ntl/ntlObj.c
@@ -131,7 +131,10 @@ Ntl_Obj_t * Ntl_ModelCreateNode( Ntl_Mod_t * pModel, int nFanins )
p->Type = NTL_OBJ_NODE;
p->nFanins = nFanins;
p->nFanouts = 1;
- pModel->nObjs[NTL_OBJ_NODE]++;
+ if ( nFanins == 1 )
+ pModel->nObjs[NTL_OBJ_LUT1]++;
+ else
+ pModel->nObjs[NTL_OBJ_NODE]++;
return p;
}
@@ -188,6 +191,30 @@ Ntl_Obj_t * Ntl_ModelDupObj( Ntl_Mod_t * pModel, Ntl_Obj_t * pOld )
return pNew;
}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the primary input with the given name.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, char * pName )
+{
+ Ntl_Obj_t * pObj;
+ Ntl_Net_t * pNet;
+ pNet = Ntl_ModelFindOrCreateNet( pModel, pName );
+ if ( pNet->pDriver )
+ return NULL;
+ pObj = Ntl_ModelCreatePi( pModel );
+ Ntl_ModelSetNetDriver( pObj, pNet );
+ return pObj;
+}
+
/**Function*************************************************************
Synopsis [Allocates memory and copies the name into it.]
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index ce3a2051..dd74f9ba 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -109,7 +109,7 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
FILE * pFile;
Ioa_ReadMan_t * p;
Ntl_Man_t * pDesign;
- int nNodes;
+// int nNodes;
// check that the file is available
pFile = fopen( pFileName, "rb" );
@@ -166,8 +166,8 @@ Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
}
// transform the design by removing the CO drivers
- if ( (nNodes = Ntl_ManTransformCoDrivers(pDesign)) )
- printf( "The design was transformed by removing %d buf/inv CO drivers.\n", nNodes );
+// if ( (nNodes = Ntl_ManReconnectCoDrivers(pDesign)) )
+// printf( "The design was transformed by removing %d buf/inv CO drivers.\n", nNodes );
//Ioa_WriteBlif( pDesign, "_temp_.blif" );
return pDesign;
}
diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c
new file mode 100644
index 00000000..3b9cd61f
--- /dev/null
+++ b/src/aig/ntl/ntlSweep.c
@@ -0,0 +1,165 @@
+/**CFile****************************************************************
+
+ FileName [ntlSweep.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Netlist representation.]
+
+ Synopsis [Performs structural sweep of the netlist.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ntlSweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ntl.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Detects logic that does not fanout into POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManSweepMark_rec( Ntl_Man_t * p, Ntl_Obj_t * pObj )
+{
+ Ntl_Net_t * pNet;
+ int i;
+ if ( pObj->fMark )
+ return;
+ pObj->fMark = 1;
+ Ntl_ObjForEachFanin( pObj, pNet, i )
+ Ntl_ManSweepMark_rec( p, pNet->pDriver );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Detects logic that does not fanout into POs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManSweepMark( Ntl_Man_t * p )
+{
+ Ntl_Mod_t * pRoot;
+ Ntl_Obj_t * pObj;
+ int i;
+ // get the root model
+ pRoot = Ntl_ManRootModel( p );
+ // clear net visited flags
+ Ntl_ModelForEachObj( pRoot, pObj, i )
+ assert( pObj->fMark == 0 );
+ // label the primary inputs
+ Ntl_ModelForEachPi( pRoot, pObj, i )
+ pObj->fMark = 1;
+ // start from the primary outputs
+ Ntl_ModelForEachPo( pRoot, pObj, i )
+ Ntl_ManSweepMark_rec( p, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives new netlist by sweeping current netlist with the current AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose )
+{
+ int nObjsOld[NTL_OBJ_VOID];
+ Ntl_Man_t * pNew;
+ Ntl_Mod_t * pRoot;
+ Ntl_Net_t * pNet;
+ Ntl_Obj_t * pObj;
+ int i, k, nNetsOld;
+
+ // insert the AIG into the netlist
+ pNew = Ntl_ManInsertAig( p, pAig );
+ if ( pNew == NULL )
+ {
+ printf( "Ntl_ManSweep(): Inserting AIG has failed.\n" );
+ return NULL;
+ }
+
+ // remember the number of objects
+ pRoot = Ntl_ManRootModel( pNew );
+ for ( i = 0; i < NTL_OBJ_VOID; i++ )
+ nObjsOld[i] = pRoot->nObjs[i];
+ nNetsOld = Ntl_ModelCountNets(pRoot);
+
+ // mark the nets that do not fanout into POs
+ Ntl_ManSweepMark( pNew );
+
+ // remove the useless objects and their nets
+ Ntl_ModelForEachObj( pRoot, pObj, i )
+ {
+ if ( pObj->fMark )
+ {
+ pObj->fMark = 0;
+ continue;
+ }
+ // remove the fanout nets
+ Ntl_ObjForEachFanout( pObj, pNet, k )
+ Ntl_ModelDeleteNet( pRoot, Ntl_ObjFanout0(pObj) );
+ // remove the object
+ if ( Ntl_ObjIsNode(pObj) && Ntl_ObjFaninNum(pObj) == 1 )
+ pRoot->nObjs[NTL_OBJ_LUT1]--;
+ else
+ pRoot->nObjs[pObj->Type]--;
+ Vec_PtrWriteEntry( pRoot->vObjs, pObj->Id, NULL );
+ pObj->Id = NTL_OBJ_NONE;
+ }
+
+ // print detailed statistics of sweeping
+ if ( fVerbose )
+ {
+ printf( "Sweep:" );
+ printf( " Node = %d (%4.1f %%)",
+ nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE],
+ !nObjsOld[NTL_OBJ_NODE]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_NODE] - pRoot->nObjs[NTL_OBJ_NODE]) / nObjsOld[NTL_OBJ_NODE] );
+ printf( " Buf/Inv = %d (%4.1f %%)",
+ nObjsOld[NTL_OBJ_LUT1] - pRoot->nObjs[NTL_OBJ_LUT1],
+ !nObjsOld[NTL_OBJ_LUT1]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_LUT1] - pRoot->nObjs[NTL_OBJ_LUT1]) / nObjsOld[NTL_OBJ_LUT1] );
+ printf( " Lat = %d (%4.1f %%)",
+ nObjsOld[NTL_OBJ_LATCH] - pRoot->nObjs[NTL_OBJ_LATCH],
+ !nObjsOld[NTL_OBJ_LATCH]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_LATCH] - pRoot->nObjs[NTL_OBJ_LATCH]) / nObjsOld[NTL_OBJ_LATCH] );
+ printf( " Box = %d (%4.1f %%)",
+ nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX],
+ !nObjsOld[NTL_OBJ_BOX]? 0.0: 100.0 * (nObjsOld[NTL_OBJ_BOX] - pRoot->nObjs[NTL_OBJ_BOX]) / nObjsOld[NTL_OBJ_BOX] );
+ printf( "\n" );
+// printf( "Also, sweep reduced %d nets.\n", nNetsOld - Ntl_ModelCountNets(pRoot) );
+ }
+ return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index df982481..07794492 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -239,6 +239,26 @@ int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Finds or creates the net.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ModelCountNets( Ntl_Mod_t * p )
+{
+ Ntl_Net_t * pNet;
+ int i, Counter = 0;
+ Ntl_ModelForEachNet( p, pNet, i )
+ Counter++;
+ return Counter;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index b13dd3a7..626bcbe1 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -30,7 +30,28 @@
/**Function*************************************************************
- Synopsis [Returns 1 if netlist was written by ABC with added bufs/invs.]
+ Synopsis [Counts COs that are connected to the internal nodes through invs/bufs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot )
+{
+ Ntl_Obj_t * pObj;
+ int i, Counter = 0;
+ Ntl_ModelForEachNode( pRoot, pObj, i )
+ if ( Ntl_ObjFaninNum(pObj) == 1 )
+ Counter++;
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Connects COs to the internal nodes other than inv/bufs.]
Description [Should be called immediately after reading from file.]
@@ -39,6 +60,63 @@
SeeAlso []
***********************************************************************/
+int Ntl_ManCountSimpleCoDriversOne( Ntl_Net_t * pNetCo )
+{
+ Ntl_Net_t * pNetFanin;
+ // skip the case when the net is not driven by a node
+ if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
+ return 0;
+ // skip the case when the node is not an inv/buf
+ if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
+ return 0;
+ // skip the case when the second-generation driver is not a node
+ pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
+ if ( !Ntl_ObjIsNode(pNetFanin->pDriver) )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts COs that are connected to the internal nodes through invs/bufs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p )
+{
+ Ntl_Net_t * pNetCo;
+ Ntl_Obj_t * pObj;
+ Ntl_Mod_t * pRoot;
+ int i, k, Counter;
+ Counter = 0;
+ pRoot = Ntl_ManRootModel( p );
+ Ntl_ModelForEachPo( pRoot, pObj, i )
+ Counter += Ntl_ManCountSimpleCoDriversOne( Ntl_ObjFanin0(pObj) );
+ Ntl_ModelForEachLatch( pRoot, pObj, i )
+ Counter += Ntl_ManCountSimpleCoDriversOne( Ntl_ObjFanin0(pObj) );
+ Ntl_ModelForEachBox( pRoot, pObj, i )
+ Ntl_ObjForEachFanin( pObj, pNetCo, k )
+ Counter += Ntl_ManCountSimpleCoDriversOne( pNetCo );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes the CO drivers that are bufs/invs.]
+
+ Description [Should be called immediately after reading from file.]
+
+ SideEffects [This procedure does not work because the internal net
+ (pNetFanin) may have other drivers.]
+
+ SeeAlso []
+
+***********************************************************************/
int Ntl_ManTransformCoDrivers( Ntl_Man_t * p )
{
Vec_Ptr_t * vCoNets;
@@ -110,7 +188,71 @@ int Ntl_ManTransformCoDrivers( Ntl_Man_t * p )
Counter++;
}
Vec_PtrFree( vCoNets );
- pRoot->nObjs[NTL_OBJ_NODE] -= Counter;
+ pRoot->nObjs[NTL_OBJ_LUT1] -= Counter;
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Connects COs to the internal nodes other than inv/bufs.]
+
+ Description [Should be called immediately after reading from file.]
+
+ SideEffects [This procedure does not work because the internal net
+ (pNetFanin) may have other drivers.]
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ManReconnectCoDriverOne( Ntl_Net_t * pNetCo )
+{
+ Ntl_Net_t * pNetFanin;
+ // skip the case when the net is not driven by a node
+ if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
+ return 0;
+ // skip the case when the node is not an inv/buf
+ if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
+ return 0;
+ // skip the case when the second-generation driver is not a node
+ pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
+ if ( !Ntl_ObjIsNode(pNetFanin->pDriver) )
+ return 0;
+ // set the complemented attribute of the net
+ pNetCo->fCompl = (int)(pNetCo->pDriver->pSop[0] == '0');
+ // drive the CO net with the second-generation driver
+ pNetCo->pDriver = NULL;
+ pNetFanin->pDriver->pFanio[pNetFanin->pDriver->nFanins] = NULL;
+ if ( !Ntl_ModelSetNetDriver( pNetFanin->pDriver, pNetCo ) )
+ printf( "Ntl_ManReconnectCoDriverOne(): Cannot connect the net.\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Connects COs to the internal nodes other than inv/bufs.]
+
+ Description [Should be called immediately after reading from file.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ManReconnectCoDrivers( Ntl_Man_t * p )
+{
+ Ntl_Net_t * pNetCo;
+ Ntl_Obj_t * pObj;
+ Ntl_Mod_t * pRoot;
+ int i, k, Counter;
+ Counter = 0;
+ pRoot = Ntl_ManRootModel( p );
+ Ntl_ModelForEachPo( pRoot, pObj, i )
+ Counter += Ntl_ManReconnectCoDriverOne( Ntl_ObjFanin0(pObj) );
+ Ntl_ModelForEachLatch( pRoot, pObj, i )
+ Counter += Ntl_ManReconnectCoDriverOne( Ntl_ObjFanin0(pObj) );
+ Ntl_ModelForEachBox( pRoot, pObj, i )
+ Ntl_ObjForEachFanin( pObj, pNetCo, k )
+ Counter += Ntl_ManReconnectCoDriverOne( pNetCo );
return Counter;
}
@@ -158,6 +300,68 @@ Vec_Ptr_t * Ntl_ManCollectCoNames( Ntl_Man_t * p )
return vNames;
}
+/**Function*************************************************************
+
+ Synopsis [Marks the CI/CO nets.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManMarkCiCoNets( Ntl_Man_t * p )
+{
+ Ntl_Net_t * pNet;
+ int i;
+ Ntl_ManForEachCiNet( p, pNet, i )
+ pNet->fMark = 1;
+ Ntl_ManForEachCoNet( p, pNet, i )
+ pNet->fMark = 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Unmarks the CI/CO nets.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p )
+{
+ Ntl_Net_t * pNet;
+ int i;
+ Ntl_ManForEachCiNet( p, pNet, i )
+ pNet->fMark = 0;
+ Ntl_ManForEachCoNet( p, pNet, i )
+ pNet->fMark = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Unmarks the CI/CO nets.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
+{
+ Ntl_Net_t * pNet;
+ int i;
+ Ntl_ModelForEachNet( pModel, pNet, i )
+ assert( pNet->fMark == 0 );
+ return 1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 08:34:16 +0000