summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/aig/aigDup.c3
-rw-r--r--src/aig/fra/fraSec.c5
-rw-r--r--src/aig/kit/kit.h16
-rw-r--r--src/aig/kit/kitPla.c298
-rw-r--r--src/aig/kit/module.make1
-rw-r--r--src/aig/ntl/ntl.h13
-rw-r--r--src/aig/ntl/ntlCheck.c2
-rw-r--r--src/aig/ntl/ntlExtract.c296
-rw-r--r--src/aig/ntl/ntlFraig.c289
-rw-r--r--src/aig/ntl/ntlInsert.c22
-rw-r--r--src/aig/ntl/ntlMan.c22
-rw-r--r--src/aig/ntl/ntlObj.c4
-rw-r--r--src/aig/ntl/ntlReadBlif.c12
-rw-r--r--src/aig/ntl/ntlSweep.c31
-rw-r--r--src/aig/ntl/ntlTable.c26
-rw-r--r--src/aig/ntl/ntlUtil.c264
-rw-r--r--src/aig/ntl/ntlWriteBlif.c4
-rw-r--r--src/aig/nwk/nwk.h4
-rw-r--r--src/aig/nwk/nwkMap.c2
-rw-r--r--src/aig/nwk/nwkStrash.c2
-rw-r--r--src/aig/nwk/nwkUtil.c91
-rw-r--r--src/base/abci/abc.c239
-rw-r--r--src/base/abci/abcAbc8.c2
23 files changed, 952 insertions, 696 deletions
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index aaaa287f..3829ee22 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -638,7 +638,10 @@ Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p )
if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Repres(p, pObj), Aig_ObjChild1Repres(p, pObj) );
else if ( Aig_ObjIsPi(pObj) )
+ {
pObj->pData = Aig_ObjCreatePi(pNew);
+ pObj->pData = Aig_ObjGetRepres( p, pObj );
+ }
else if ( Aig_ObjIsPo(pObj) )
pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Repres(p, pObj) );
else if ( Aig_ObjIsConst1(pObj) )
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 012c7651..99d4bc89 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -44,7 +44,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging
{
Fra_Ssw_t Pars, * pPars = &Pars;
Fra_Sml_t * pSml;
- Aig_Man_t * pNew, * pTemp;
+ Aig_Man_t * pNew = NULL, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
int fLatchCorr = 0;
@@ -235,7 +235,8 @@ PRT( "Time", clock() - clkTotal );
Ioa_WriteAiger( pNew, pFileName, 0, 0 );
printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
}
- Aig_ManStop( pNew );
+ if ( pNew )
+ Aig_ManStop( pNew );
return RetValue;
}
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 23e3ce8d..7607d17c 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -160,6 +160,11 @@ static inline unsigned Kit_DsdLitSupport( Kit_DsdNtk_t * pNtk, int Lit )
#define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) \
for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
+#define Kit_PlaForEachCube( pSop, nFanins, pCube ) \
+ for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
+#define Kit_PlaCubeForEachVar( pCube, Value, i ) \
+ for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -540,6 +545,17 @@ extern int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t
//extern Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory );
/*=== kitIsop.c ==========================================================*/
extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth );
+/*=== kitPla.c ==========================================================*/
+extern int Kit_PlaIsConst0( char * pSop );
+extern int Kit_PlaGetVarNum( char * pSop );
+extern int Kit_PlaGetCubeNum( char * pSop );
+extern int Kit_PlaIsComplement( char * pSop );
+extern void Kit_PlaComplement( char * pSop );
+extern char * Kit_PlaStart( void * p, int nCubes, int nVars );
+extern char * Kit_PlaCreateFromIsop( void * p, int nVars, Vec_Int_t * vCover );
+extern void Kit_PlaToIsop( char * pSop, Vec_Int_t * vCover );
+extern char * Kit_PlaStoreSop( void * p, char * pSop );
+extern char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover );
/*=== kitSop.c ==========================================================*/
extern void Kit_SopCreate( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
extern void Kit_SopCreateInverse( Kit_Sop_t * cResult, Vec_Int_t * vInput, int nVars, Vec_Int_t * vMemory );
diff --git a/src/aig/kit/kitPla.c b/src/aig/kit/kitPla.c
new file mode 100644
index 00000000..be8f594a
--- /dev/null
+++ b/src/aig/kit/kitPla.c
@@ -0,0 +1,298 @@
+/**CFile****************************************************************
+
+ FileName [kitPla.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Computation kit.]
+
+ Synopsis [Manipulating SOP in the form of a C-string.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - Dec 6, 2006.]
+
+ Revision [$Id: kitPla.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "kit.h"
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the cover is constant 0.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_PlaIsConst0( char * pSop )
+{
+ return pSop[0] == ' ' && pSop[1] == '0';
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the number of variables in the cover.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_PlaGetVarNum( char * pSop )
+{
+ char * pCur;
+ for ( pCur = pSop; *pCur != '\n'; pCur++ );
+ return pCur - pSop - 2;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the number of cubes in the cover.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_PlaGetCubeNum( char * pSop )
+{
+ char * pCur;
+ int nCubes = 0;
+ if ( pSop == NULL )
+ return 0;
+ for ( pCur = pSop; *pCur; pCur++ )
+ nCubes += (*pCur == '\n');
+ return nCubes;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_PlaIsComplement( char * pSop )
+{
+ char * pCur;
+ for ( pCur = pSop; *pCur; pCur++ )
+ if ( *pCur == '\n' )
+ return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
+ assert( 0 );
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_PlaComplement( char * pSop )
+{
+ char * pCur;
+ for ( pCur = pSop; *pCur; pCur++ )
+ if ( *pCur == '\n' )
+ {
+ if ( *(pCur - 1) == '0' )
+ *(pCur - 1) = '1';
+ else if ( *(pCur - 1) == '1' )
+ *(pCur - 1) = '0';
+ else if ( *(pCur - 1) == 'x' )
+ *(pCur - 1) = 'n';
+ else if ( *(pCur - 1) == 'n' )
+ *(pCur - 1) = 'x';
+ else
+ assert( 0 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the constant 1 cover with the given number of variables and cubes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Kit_PlaStart( void * p, int nCubes, int nVars )
+{
+ Aig_MmFlex_t * pMan = p;
+ char * pSopCover, * pCube;
+ int i, Length;
+
+ Length = nCubes * (nVars + 3);
+ pSopCover = Aig_MmFlexEntryFetch( pMan, Length + 1 );
+ memset( pSopCover, '-', Length );
+ pSopCover[Length] = 0;
+
+ for ( i = 0; i < nCubes; i++ )
+ {
+ pCube = pSopCover + i * (nVars + 3);
+ pCube[nVars + 0] = ' ';
+ pCube[nVars + 1] = '1';
+ pCube[nVars + 2] = '\n';
+ }
+ return pSopCover;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the cover from the ISOP computed from TT.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Kit_PlaCreateFromIsop( void * p, int nVars, Vec_Int_t * vCover )
+{
+ Aig_MmFlex_t * pMan = p;
+ char * pSop, * pCube;
+ int i, k, Entry, Literal;
+ assert( Vec_IntSize(vCover) > 0 );
+ if ( Vec_IntSize(vCover) == 0 )
+ return NULL;
+ // start the cover
+ pSop = Kit_PlaStart( pMan, Vec_IntSize(vCover), nVars );
+ // create cubes
+ Vec_IntForEachEntry( vCover, Entry, i )
+ {
+ pCube = pSop + i * (nVars + 3);
+ for ( k = 0; k < nVars; k++ )
+ {
+ Literal = 3 & (Entry >> (k << 1));
+ if ( Literal == 1 )
+ pCube[k] = '0';
+ else if ( Literal == 2 )
+ pCube[k] = '1';
+ else if ( Literal != 0 )
+ assert( 0 );
+ }
+ }
+ return pSop;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the cover from the ISOP computed from TT.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_PlaToIsop( char * pSop, Vec_Int_t * vCover )
+{
+ char * pCube;
+ int k, nVars, Entry;
+ nVars = Kit_PlaGetVarNum( pSop );
+ assert( nVars > 0 );
+ // create cubes
+ Vec_IntClear( vCover );
+ for ( pCube = pSop; *pCube; pCube += nVars + 3 )
+ {
+ Entry = 0;
+ for ( k = nVars - 1; k >= 0; k-- )
+ if ( pCube[k] == '0' )
+ Entry = (Entry << 2) | 1;
+ else if ( pCube[k] == '1' )
+ Entry = (Entry << 2) | 2;
+ else if ( pCube[k] == '-' )
+ Entry = (Entry << 2);
+ else
+ assert( 0 );
+ Vec_IntPush( vCover, Entry );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Allocates memory and copies the SOP into it.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Kit_PlaStoreSop( void * p, char * pSop )
+{
+ Aig_MmFlex_t * pMan = p;
+ char * pStore;
+ pStore = Aig_MmFlexEntryFetch( pMan, strlen(pSop) + 1 );
+ strcpy( pStore, pSop );
+ return pStore;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms truth table into the SOP.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Kit_PlaFromTruth( void * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover )
+{
+ Aig_MmFlex_t * pMan = p;
+ char * pSop;
+ int RetValue;
+ if ( Kit_TruthIsConst0(pTruth, nVars) )
+ return Kit_PlaStoreSop( pMan, " 0\n" );
+ if ( Kit_TruthIsConst1(pTruth, nVars) )
+ return Kit_PlaStoreSop( pMan, " 1\n" );
+ RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 ); // 1 );
+ assert( RetValue == 0 || RetValue == 1 );
+ pSop = Kit_PlaCreateFromIsop( pMan, nVars, vCover );
+ if ( RetValue )
+ Kit_PlaComplement( pSop );
+ return pSop;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/kit/module.make b/src/aig/kit/module.make
index ea62381b..a592aeec 100644
--- a/src/aig/kit/module.make
+++ b/src/aig/kit/module.make
@@ -6,5 +6,6 @@ SRC += src/aig/kit/kitAig.c \
src/aig/kit/kitGraph.c \
src/aig/kit/kitHop.c \
src/aig/kit/kitIsop.c \
+ src/aig/kit/kitPla.c \
src/aig/kit/kitSop.c \
src/aig/kit/kitTruth.c
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 6b6424c0..4f00cbda 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -123,7 +123,6 @@ 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 attribute
char pName[0]; // the name of this net
};
@@ -235,10 +234,9 @@ extern void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2,
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, int fSeq );
+extern Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p );
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 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 );
@@ -275,15 +273,16 @@ extern Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int
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_ManStoreSop( Aig_MmFlex_t * pMan, 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 );
+extern int Ntl_ManSweep( Ntl_Man_t * p, 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 int Ntl_ModelClearNetDriver( 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 ==========================================================*/
@@ -295,13 +294,13 @@ 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 );
+extern void Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
+extern void Ntl_ManTransformInitValues( Ntl_Man_t * p );
#ifdef __cplusplus
}
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index 9fd4af9f..c5c62433 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.c
@@ -158,7 +158,7 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
continue;
// add the constant 0 driver
pNode = Ntl_ModelCreateNode( pModel, 0 );
- pNode->pSop = Ntl_ManStoreSop( pModel->pMan, " 0\n" );
+ pNode->pSop = Ntl_ManStoreSop( pModel->pMan->pMemSops, " 0\n" );
Ntl_ModelSetNetDriver( pNode, pNet );
// add the net to those for which the warning will be printed
Vec_PtrPush( vNets, pNet );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index b3d099c9..d474b4dd 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -26,257 +26,12 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-#define Ntl_SopForEachCube( pSop, nFanins, pCube ) \
- for ( pCube = (pSop); *pCube; pCube += (nFanins) + 3 )
-#define Ntl_CubeForEachVar( pCube, Value, i ) \
- for ( i = 0; (pCube[i] != ' ') && (Value = pCube[i]); i++ )
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis [Checks if the cover is constant 0.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ntl_SopIsConst0( char * pSop )
-{
- return pSop[0] == ' ' && pSop[1] == '0';
-}
-
-/**Function*************************************************************
-
- Synopsis [Reads the number of variables in the cover.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ntl_SopGetVarNum( char * pSop )
-{
- char * pCur;
- for ( pCur = pSop; *pCur != '\n'; pCur++ );
- return pCur - pSop - 2;
-}
-
-/**Function*************************************************************
-
- Synopsis [Reads the number of cubes in the cover.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ntl_SopGetCubeNum( char * pSop )
-{
- char * pCur;
- int nCubes = 0;
- if ( pSop == NULL )
- return 0;
- for ( pCur = pSop; *pCur; pCur++ )
- nCubes += (*pCur == '\n');
- return nCubes;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ntl_SopIsComplement( char * pSop )
-{
- char * pCur;
- for ( pCur = pSop; *pCur; pCur++ )
- if ( *pCur == '\n' )
- return (int)(*(pCur - 1) == '0' || *(pCur - 1) == 'n');
- assert( 0 );
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ntl_SopComplement( char * pSop )
-{
- char * pCur;
- for ( pCur = pSop; *pCur; pCur++ )
- if ( *pCur == '\n' )
- {
- if ( *(pCur - 1) == '0' )
- *(pCur - 1) = '1';
- else if ( *(pCur - 1) == '1' )
- *(pCur - 1) = '0';
- else if ( *(pCur - 1) == 'x' )
- *(pCur - 1) = 'n';
- else if ( *(pCur - 1) == 'n' )
- *(pCur - 1) = 'x';
- else
- assert( 0 );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the constant 1 cover with the given number of variables and cubes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Ntl_SopStart( Aig_MmFlex_t * pMan, int nCubes, int nVars )
-{
- char * pSopCover, * pCube;
- int i, Length;
-
- Length = nCubes * (nVars + 3);
- pSopCover = Aig_MmFlexEntryFetch( pMan, Length + 1 );
- memset( pSopCover, '-', Length );
- pSopCover[Length] = 0;
-
- for ( i = 0; i < nCubes; i++ )
- {
- pCube = pSopCover + i * (nVars + 3);
- pCube[nVars + 0] = ' ';
- pCube[nVars + 1] = '1';
- pCube[nVars + 2] = '\n';
- }
- return pSopCover;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the cover from the ISOP computed from TT.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Ntl_SopCreateFromIsop( Aig_MmFlex_t * pMan, int nVars, Vec_Int_t * vCover )
-{
- char * pSop, * pCube;
- int i, k, Entry, Literal;
- assert( Vec_IntSize(vCover) > 0 );
- if ( Vec_IntSize(vCover) == 0 )
- return NULL;
- // start the cover
- pSop = Ntl_SopStart( pMan, Vec_IntSize(vCover), nVars );
- // create cubes
- Vec_IntForEachEntry( vCover, Entry, i )
- {
- pCube = pSop + i * (nVars + 3);
- for ( k = 0; k < nVars; k++ )
- {
- Literal = 3 & (Entry >> (k << 1));
- if ( Literal == 1 )
- pCube[k] = '0';
- else if ( Literal == 2 )
- pCube[k] = '1';
- else if ( Literal != 0 )
- assert( 0 );
- }
- }
- return pSop;
-}
-
-/**Function*************************************************************
-
- Synopsis [Creates the cover from the ISOP computed from TT.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ntl_SopToIsop( char * pSop, Vec_Int_t * vCover )
-{
- char * pCube;
- int k, nVars, Entry;
- nVars = Ntl_SopGetVarNum( pSop );
- assert( nVars > 0 );
- // create cubes
- Vec_IntClear( vCover );
- for ( pCube = pSop; *pCube; pCube += nVars + 3 )
- {
- Entry = 0;
- for ( k = nVars - 1; k >= 0; k-- )
- if ( pCube[k] == '0' )
- Entry = (Entry << 2) | 1;
- else if ( pCube[k] == '1' )
- Entry = (Entry << 2) | 2;
- else if ( pCube[k] == '-' )
- Entry = (Entry << 2);
- else
- assert( 0 );
- Vec_IntPush( vCover, Entry );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Transforms truth table into the SOP.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-char * Ntl_SopFromTruth( Ntl_Man_t * p, unsigned * pTruth, int nVars, Vec_Int_t * vCover )
-{
- char * pSop;
- int RetValue;
- if ( Kit_TruthIsConst0(pTruth, nVars) )
- return Ntl_ManStoreSop( p, " 0\n" );
- if ( Kit_TruthIsConst1(pTruth, nVars) )
- return Ntl_ManStoreSop( p, " 1\n" );
- RetValue = Kit_TruthIsop( pTruth, nVars, vCover, 0 ); // 1 );
- assert( RetValue == 0 || RetValue == 1 );
- pSop = Ntl_SopCreateFromIsop( p->pMemSops, nVars, vCover );
- if ( RetValue )
- Ntl_SopComplement( pSop );
- return pSop;
-}
-
-
-
-/**Function*************************************************************
-
Synopsis [Strashes one logic node using its SOP.]
Description []
@@ -293,14 +48,14 @@ Aig_Obj_t * Ntl_ConvertSopToAigInternal( Aig_Man_t * pMan, Ntl_Obj_t * pNode, ch
int i, Value, nFanins;
char * pCube;
// get the number of variables
- nFanins = Ntl_SopGetVarNum(pSop);
+ nFanins = Kit_PlaGetVarNum(pSop);
// go through the cubes of the node's SOP
pSum = Aig_ManConst0(pMan);
- Ntl_SopForEachCube( pSop, nFanins, pCube )
+ Kit_PlaForEachCube( pSop, nFanins, pCube )
{
// create the AND of literals
pAnd = Aig_ManConst1(pMan);
- Ntl_CubeForEachVar( pCube, Value, i )
+ Kit_PlaCubeForEachVar( pCube, Value, i )
{
pNet = Ntl_ObjFanin( pNode, i );
if ( Value == '1' )
@@ -312,7 +67,7 @@ Aig_Obj_t * Ntl_ConvertSopToAigInternal( Aig_Man_t * pMan, Ntl_Obj_t * pNode, ch
pSum = Aig_Or( pMan, pSum, pAnd );
}
// decide whether to complement the result
- if ( Ntl_SopIsComplement(pSop) )
+ if ( Kit_PlaIsComplement(pSop) )
pSum = Aig_Not(pSum);
return pSum;
}
@@ -366,10 +121,10 @@ Aig_Obj_t * Ntl_ManBuildNodeAig( Ntl_Obj_t * pNode )
Aig_Man_t * pMan = pNode->pModel->pMan->pAig;
int fUseFactor = 1;
// consider the constant node
- if ( Ntl_SopGetVarNum(pNode->pSop) == 0 )
- return Aig_NotCond( Aig_ManConst1(pMan), Ntl_SopIsConst0(pNode->pSop) );
+ if ( Kit_PlaGetVarNum(pNode->pSop) == 0 )
+ return Aig_NotCond( Aig_ManConst1(pMan), Kit_PlaIsConst0(pNode->pSop) );
// decide when to use factoring
- if ( fUseFactor && Ntl_SopGetVarNum(pNode->pSop) > 2 && Ntl_SopGetCubeNum(pNode->pSop) > 1 )
+ if ( fUseFactor && Kit_PlaGetVarNum(pNode->pSop) > 2 && Kit_PlaGetCubeNum(pNode->pSop) > 1 )
{
Dec_Graph_t * pFForm;
Dec_Node_t * pFFNode;
@@ -437,13 +192,10 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
pNetFanin->pCopy = Aig_ObjCreatePi( p->pAig );
Aig_ObjSetLevel( pNetFanin->pCopy, LevelMax + 1 );
}
-//printf( "Creating fake PO with ID = %d.\n", Aig_ManPo(p->pAig, Vec_IntEntryLast(p->vBox1Cos))->Id );
}
Vec_PtrPush( p->vNodes, pObj );
if ( Ntl_ObjIsNode(pObj) )
pNet->pCopy = Ntl_ManBuildNodeAig( pObj );
- if ( pNet->fCompl )
- pNet->pCopy = Aig_Not(pNet->pCopy);
pNet->nVisits = 2;
return 1;
}
@@ -517,9 +269,6 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
if ( !Ntl_ManExtract_rec( p, pNet ) )
{
printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
- Vec_PtrClear( p->vCis );
- Vec_PtrClear( p->vCos );
- Vec_PtrClear( p->vNodes );
return 0;
}
Vec_PtrPush( p->vCos, pNet );
@@ -532,9 +281,6 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
if ( !Ntl_ManExtract_rec( p, pNet ) )
{
printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
- Vec_PtrClear( p->vCis );
- Vec_PtrClear( p->vCos );
- Vec_PtrClear( p->vNodes );
return 0;
}
Vec_PtrPush( p->vCos, pNet );
@@ -555,8 +301,6 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
return pAig;
}
-
-
/**Function*************************************************************
Synopsis [Collects the nodes in a topological order.]
@@ -641,8 +385,6 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
}
if ( Ntl_ObjIsNode(pObj) )
pNet->pCopy = Ntl_ManBuildNodeAig( pObj );
- if ( pNet->fCompl )
- pNet->pCopy = Aig_Not(pNet->pCopy);
pNet->nVisits = 2;
return 1;
}
@@ -659,7 +401,7 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
+Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p )
{
Aig_Man_t * pAig;
Ntl_Mod_t * pRoot;
@@ -695,8 +437,6 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
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" );
@@ -724,10 +464,7 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
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 );
+ Aig_ObjCreatePo( p->pAig, pNet->pCopy );
}
// cleanup the AIG
Aig_ManCleanup( p->pAig );
@@ -788,10 +525,9 @@ Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p )
/**Function*************************************************************
- Synopsis [Performs DFS.]
+ Synopsis [Derives AIG for SEC.]
- Description [Checks for combinational loops. Collects PI/PO nets.
- Collects nodes in the topological order.]
+ Description [Uses CIs/COs collected in the internal arrays.]
SideEffects []
@@ -988,18 +724,20 @@ Nwk_Obj_t * Ntl_ManExtractNwk_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, Nwk_Man_t *
Nwk_ObjAddFanin( pNode, pFaninNet->pCopy );
}
if ( Ntl_ObjFaninNum(pNet->pDriver) == 0 )
- pNode->pFunc = Hop_NotCond( Hop_ManConst1(pNtk->pManHop), Ntl_SopIsConst0(pNet->pDriver->pSop) );
+ pNode->pFunc = Hop_NotCond( Hop_ManConst1(pNtk->pManHop), Kit_PlaIsConst0(pNet->pDriver->pSop) );
else
{
- Ntl_SopToIsop( pNet->pDriver->pSop, vCover );
+ Kit_PlaToIsop( pNet->pDriver->pSop, vCover );
pNode->pFunc = Kit_CoverToHop( pNtk->pManHop, vCover, Ntl_ObjFaninNum(pNet->pDriver), vMemory );
+ if ( Kit_PlaIsComplement(pNet->pDriver->pSop) )
+ pNode->pFunc = Hop_Not(pNode->pFunc);
}
return pNet->pCopy = pNode;
}
/**Function*************************************************************
- Synopsis [Extracts logic newtork out of the netlist.]
+ Synopsis [Extracts logic network out of the netlist.]
Description []
@@ -1054,7 +792,6 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig )
pNet = Ntl_ObjFanin0(pObj);
pNet->pCopy = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory );
pNode = Nwk_ManCreateCo( pNtk );
- pNode->fCompl = pNet->fCompl;
Nwk_ObjAddFanin( pNode, pNet->pCopy );
}
}
@@ -1112,7 +849,6 @@ Nwk_Man_t * Ntl_ManReadNwk( char * pFileName, Aig_Man_t * pAig, Tim_Man_t * pMan
return pNtk;
}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 98f14d3d..117f3275 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -48,8 +48,13 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
Aig_Obj_t * pObj, * pObjCol, * pObjColRepr, * pCorresp;
int i;
+ // remember pointers to the nets of pNew
+ Aig_ManForEachObj( pAig, pObj, i )
+ pObj->pNext = pObj->pData;
+
// map the AIG managers
Aig_ManForEachObj( pAig, pObj, i )
+ {
if ( Aig_ObjIsConst1(pObj) )
pObj->pData = Aig_ManConst1(pAigCol);
else if ( !Aig_ObjIsPo(pObj) )
@@ -58,6 +63,7 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
pObjCol = Aig_Regular(pNet->pCopy);
pObj->pData = pObjCol;
}
+ }
// create mapping from the collapsed manager into the original manager
// (each node in the collapsed manager may have more than one equivalent node
@@ -98,12 +104,84 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
pReprs[pCorresp->Id] = pObj;
}
free( pMapBack );
+
+ // recall pointers to the nets of pNew
+ Aig_ManForEachObj( pAig, pObj, i )
+ pObj->pData = pObj->pNext, pObj->pNext = NULL;
return pReprs;
}
/**Function*************************************************************
- Synopsis [Returns AIG with WB after fraiging.]
+ Synopsis [Uses equivalences in the AID to reduce the design.]
+
+ Description [The AIG (pAig) was extracted from the netlist and still
+ points to it (pObj->pData is the pointer to the nets in the netlist).
+ Equivalences have been computed for the collapsed AIG and transfered
+ to this AIG (pAig). This procedure reduces the corresponding nets.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
+{
+ Aig_Obj_t * pObj, * pObjRepr;
+ Ntl_Net_t * pNet, * pNetRepr;
+ Ntl_Mod_t * pRoot;
+ Ntl_Obj_t * pNode;
+ int i, fCompl, Counter = 0;
+ assert( pAig->pReprs );
+ pRoot = Ntl_ManRootModel( p );
+
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ pObjRepr = Aig_ObjRepr( pAig, pObj );
+ if ( pObjRepr == NULL )
+ continue;
+ assert( pObj != pObjRepr );
+ pNet = pObj->pData;
+ pNetRepr = pObjRepr->pData;
+ if ( pNetRepr == NULL )
+ {
+ // this is the constant node
+ assert( Aig_ObjIsConst1(pObjRepr) );
+ pNode = Ntl_ModelCreateNode( pRoot, 0 );
+ pNode->pSop = Ntl_ManStoreSop( p->pMemSops, " 1\n" );
+ if ( (pNetRepr = Ntl_ModelFindNet( pRoot, "Const1" )) )
+ {
+ printf( "Ntl_ManReduce(): Internal error: Intermediate net name is not unique.\n" );
+ return;
+ }
+ pNetRepr = Ntl_ModelFindOrCreateNet( pRoot, "Const1" );
+ if ( !Ntl_ModelSetNetDriver( pNode, pNetRepr ) )
+ {
+ printf( "Ntl_ManReduce(): Internal error: Net has more than one fanin.\n" );
+ return;
+ }
+ pObjRepr->pData = pNetRepr;
+ pNetRepr->pCopy = Aig_ManConst1(pAig);
+ }
+ // get the complemented attributes of the nets
+ fCompl = Aig_IsComplement(pNet->pCopy) ^ Aig_Regular(pNet->pCopy)->fPhase ^
+ Aig_IsComplement(pNetRepr->pCopy) ^ Aig_Regular(pNetRepr->pCopy)->fPhase;
+ // create interter/buffer driven by the representative net
+ pNode = Ntl_ModelCreateNode( pRoot, 1 );
+ pNode->pSop = fCompl? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
+ Ntl_ObjSetFanin( pNode, pNetRepr, 0 );
+ // make the new node drive the equivalent net (pNet)
+ if ( !Ntl_ModelClearNetDriver( pNet->pDriver, pNet ) )
+ printf( "Ntl_ManReduce(): Internal error! Net already has no driver.\n" );
+ if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+ printf( "Ntl_ManReduce(): Internal error! Net already has a driver.\n" );
+ Counter++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finalizes the transformation.]
Description []
@@ -112,43 +190,68 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
SeeAlso []
***********************************************************************/
-Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
+Ntl_Man_t * Ntl_ManFinalize( Ntl_Man_t * pNew, Aig_Man_t * pAig, Aig_Man_t * pAigCol, int fVerbose )
{
- Ntl_Man_t * pNew;
- Aig_Man_t * pAigCol, * pTemp;
+ int fUseExtraSweep = 1;
+ Ntl_Man_t * pSwept;
+ Aig_Man_t * pTemp;
assert( pAig->pReprs == NULL );
+ assert( pAigCol->pReprs != NULL );
- // create a new netlist whose nodes are in 1-to-1 relationship with AIG
- pNew = Ntl_ManInsertAig( p, pAig );
- if ( pNew == NULL )
+ // transfer equivalence classes to the original AIG
+ pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
+ pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
+if ( fVerbose )
+ printf( "Equivalences: Collapsed = %5d. Extracted = %5d.\n", Aig_ManCountReprs(pAigCol), Aig_ManCountReprs(pAig) );
+
+ // implement equivalence classes and remove dangling nodes
+ Ntl_ManReduce( pNew, pAig );
+ Ntl_ManSweep( pNew, fVerbose );
+
+ // perform one more sweep
+ if ( fUseExtraSweep )
{
- printf( "Ntk_ManFraig(): Inserting AIG has failed.\n" );
- return NULL;
+ pTemp = Ntl_ManExtract( pNew );
+ pSwept = Ntl_ManInsertAig( pNew, pTemp );
+ Aig_ManStop( pTemp );
+ Ntl_ManSweep( pSwept, fVerbose );
+ return pSwept;
}
+ return Ntl_ManDup(pNew);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns AIG with WB after fraiging.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
+{
+ Ntl_Man_t * pNew, * pAux;
+ Aig_Man_t * pAig, * pAigCol, * pTemp;
// collapse the AIG
- pAigCol = Ntl_ManCollapse( pNew, 0 );
+ pAig = Ntl_ManExtract( p );
+ pNew = Ntl_ManInsertAig( p, pAig );
+ pAigCol = Ntl_ManCollapse( pNew );
+
// perform fraiging for the given design
- if ( nPartSize == 0 )
- nPartSize = Aig_ManPoNum(pAigCol);
+ nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol);
pTemp = Aig_ManFraigPartitioned( pAigCol, nPartSize, nConfLimit, nLevelMax, fVerbose );
Aig_ManStop( pTemp );
- // transfer equivalence classes to the original AIG
- pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
- pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
- // cleanup
+ // finalize the transformatoin
+ pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
+ Ntl_ManFree( pAux );
+ Aig_ManStop( pAig );
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;
+ return pNew;
}
/**Function*************************************************************
@@ -162,44 +265,30 @@ Aig_Man_t * Ntl_ManFraig( Ntl_Man_t * p, Aig_Man_t * pAig, int nPartSize, int nC
SeeAlso []
***********************************************************************/
-Aig_Man_t * Ntl_ManScl( Ntl_Man_t * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
+Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVerbose )
{
- Ntl_Man_t * pNew;
- Aig_Man_t * pAigCol, * pTemp;
- assert( pAig->pReprs == NULL );
+ Ntl_Man_t * pNew, * pAux;
+ Aig_Man_t * pAig, * pAigCol, * pTemp;
+
+ // transform the design
+ Ntl_ManTransformInitValues( p );
- // 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
+ pAig = Ntl_ManExtract( p );
+ pNew = Ntl_ManInsertAig( p, pAig );
+ pAigCol = Ntl_ManCollapse( pNew );
+
+ // perform SCL 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
+ // finalize the transformatoin
+ pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
+ Ntl_ManFree( pAux );
+ Aig_ManStop( pAig );
Aig_ManStop( pAigCol );
- Ntl_ManFree( pNew );
-
- // derive the new AIG
- pTemp = Aig_ManDupRepresDfs( pAig );
-printf( "Intermediate:\n" );
-Aig_ManPrintStats( pTemp );
- // duplicate the timing manager
- if ( pAig->pManTime )
- pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
- // reset levels
- Aig_ManChoiceLevel( pTemp );
- return pTemp;
+ return pNew;
}
/**Function*************************************************************
@@ -213,46 +302,30 @@ Aig_ManPrintStats( pTemp );
SeeAlso []
***********************************************************************/
-Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, int fVerbose )
+Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
{
- Ntl_Man_t * pNew;
- Aig_Man_t * pAigCol, * pTemp;
- assert( pAig->pReprs == NULL );
+ Ntl_Man_t * pNew, * pAux;
+ Aig_Man_t * pAig, * pAigCol, * pTemp;
- // 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;
- }
+ // transform the design
+ Ntl_ManTransformInitValues( p );
// collapse the AIG
- pAigCol = Ntl_ManCollapse( pNew, 1 );
- // perform fraiging for the given design
+ pAig = Ntl_ManExtract( p );
+ pNew = Ntl_ManInsertAig( p, pAig );
+ pAigCol = Ntl_ManCollapse( pNew );
+
+ // perform SCL for the given design
pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p));
pTemp = Fra_FraigLatchCorrespondence( pAigCol, 0, nConfMax, 0, fVerbose, NULL );
-//printf( "Reprs = %d.\n", Aig_ManCountReprs(pAigCol) );
Aig_ManStop( pTemp );
- // transfer equivalence classes to the original AIG
- pAig->pReprs = Ntl_ManFraigDeriveClasses( pAig, pNew, pAigCol );
- pAig->nReprsAlloc = Aig_ManObjNumMax(pAig);
-//printf( "Reprs = %d.\n", Aig_ManCountReprs(pAig) );
- // cleanup
+ // finalize the transformatoin
+ pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
+ Ntl_ManFree( pAux );
+ Aig_ManStop( pAig );
Aig_ManStop( pAigCol );
- Ntl_ManFree( pNew );
-
- // derive the new AIG
- pTemp = Aig_ManDupRepresDfs( pAig );
-//printf( "Intermediate LCORR:\n" );
-//Aig_ManPrintStats( pTemp );
- // duplicate the timing manager
- if ( pAig->pManTime )
- pTemp->pManTime = Tim_ManDup( pAig->pManTime, 0 );
- // reset levels
- Aig_ManChoiceLevel( pTemp );
- return pTemp;
+ return pNew;
}
/**Function*************************************************************
@@ -266,42 +339,30 @@ Aig_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, Aig_Man_t * pAig, int nConfMax, int fVe
SeeAlso []
***********************************************************************/
-Aig_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars )
+Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
{
- Ntl_Man_t * pNew;
- Aig_Man_t * pAigCol, * pTemp;
- assert( pAig->pReprs == NULL );
+ Ntl_Man_t * pNew, * pAux;
+ Aig_Man_t * pAig, * pAigCol, * pTemp;
- // 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;
- }
+ // transform the design
+ Ntl_ManTransformInitValues( p );
// collapse the AIG
- pAigCol = Ntl_ManCollapse( pNew, 1 );
- // perform fraiging for the given design
+ pAig = Ntl_ManExtract( p );
+ pNew = Ntl_ManInsertAig( p, pAig );
+ pAigCol = Ntl_ManCollapse( pNew );
+
+ // perform SCL 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
+ // finalize the transformatoin
+ pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose );
+ Ntl_ManFree( pAux );
+ Aig_ManStop( pAig );
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;
+ return pNew;
}
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 77fb606a..3e9f82d6 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -68,7 +68,7 @@ Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t
Vec_PtrForEachEntry( vMapping, pLut, i )
{
pNode = Ntl_ModelCreateNode( pRoot, pLut->nFanins );
- pNode->pSop = Ntl_SopFromTruth( p, pLut->pTruth, pLut->nFanins, vCover );
+ pNode->pSop = Kit_PlaFromTruth( p->pMemSops, pLut->pTruth, pLut->nFanins, vCover );
if ( !Kit_TruthIsConst0(pLut->pTruth, pLut->nFanins) && !Kit_TruthIsConst1(pLut->pTruth, pLut->nFanins) )
{
for ( k = 0; k < pLut->nFanins; k++ )
@@ -108,7 +108,7 @@ Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t
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" );
+ pNode->pSop = Aig_IsComplement(pNetCo->pCopy)? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
assert( pNetCo->pDriver == NULL );
@@ -158,7 +158,7 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
if ( Aig_ManConst1(pAig)->nRefs > 0 )
{
pNode = Ntl_ModelCreateNode( pRoot, 0 );
- pNode->pSop = Ntl_ManStoreSop( p, " 1\n" );
+ pNode->pSop = Ntl_ManStoreSop( p->pMemSops, " 1\n" );
if ( (pNet = Ntl_ModelFindNet( pRoot, "Const1" )) )
{
printf( "Ntl_ManInsertAig(): Internal error: Intermediate net name is not unique.\n" );
@@ -188,13 +188,13 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
Ntl_ObjSetFanin( pNode, Aig_ObjFanin0(pObj)->pData, 0 );
Ntl_ObjSetFanin( pNode, Aig_ObjFanin1(pObj)->pData, 1 );
if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
- pNode->pSop = Ntl_ManStoreSop( p, "00 1\n" );
+ pNode->pSop = Ntl_ManStoreSop( p->pMemSops, "00 1\n" );
else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) )
- pNode->pSop = Ntl_ManStoreSop( p, "01 1\n" );
+ pNode->pSop = Ntl_ManStoreSop( p->pMemSops, "01 1\n" );
else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
- pNode->pSop = Ntl_ManStoreSop( p, "10 1\n" );
+ pNode->pSop = Ntl_ManStoreSop( p->pMemSops, "10 1\n" );
else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
- pNode->pSop = Ntl_ManStoreSop( p, "11 1\n" );
+ pNode->pSop = Ntl_ManStoreSop( p->pMemSops, "11 1\n" );
sprintf( Buffer, "and%0*d", nDigits, Counter++ );
if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
{
@@ -224,7 +224,7 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
// get the net driving the driver
pNet = pFanin->pData;
pNode = Ntl_ModelCreateNode( pRoot, 1 );
- pNode->pSop = Aig_ObjFaninC0(pObj)? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+ pNode->pSop = Aig_ObjFaninC0(pObj)? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
assert( pNetCo->pDriver == NULL );
@@ -288,7 +288,7 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
if ( Hop_IsComplement(pObj->pFunc) )
Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
- pNode->pSop = Ntl_SopFromTruth( p, pTruth, Nwk_ObjFaninNum(pObj), vCover );
+ pNode->pSop = Kit_PlaFromTruth( p->pMemSops, pTruth, Nwk_ObjFaninNum(pObj), vCover );
if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
{
Nwk_ObjForEachFanin( pObj, pFanin, k )
@@ -332,9 +332,9 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
pObj = Nwk_ManCo( pNtk, i );
pFanin = Nwk_ObjFanin0( pObj );
// get the net driving the driver
- pNet = pFanin->pCopy; //Vec_PtrEntry( vCopies, Aig_Regular(pNetCo->pCopy)->Id );
+ pNet = pFanin->pCopy;
pNode = Ntl_ModelCreateNode( pRoot, 1 );
- pNode->pSop = pObj->fCompl /*Aig_IsComplement(pNetCo->pCopy)*/? Ntl_ManStoreSop( p, "0 1\n" ) : Ntl_ManStoreSop( p, "1 1\n" );
+ pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
Ntl_ObjSetFanin( pNode, pNet, 0 );
// update the CO driver net
assert( pNetCo->pDriver == NULL );
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index 82131091..b4b63905 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -326,16 +326,27 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
Ntl_Obj_t * pObj;
int i, k;
pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+ Ntl_ModelForEachObj( pModelOld, pObj, i )
+ {
+ if ( Ntl_ObjIsNode(pObj) )
+ pObj->pCopy = NULL;
+ else
+ pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
+ }
Ntl_ModelForEachNet( pModelOld, pNet, i )
+ {
if ( pNet->fMark )
+ {
pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+ ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy;
+ }
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 );
@@ -369,11 +380,16 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
Ntl_Obj_t * pObj;
int i, k;
pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+ Ntl_ModelForEachObj( pModelOld, pObj, i )
+ pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
Ntl_ModelForEachNet( pModelOld, pNet, i )
+ {
pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+ ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy;
+ assert( pNet->pDriver->pCopy != NULL );
+ }
Ntl_ModelForEachObj( pModelOld, pObj, i )
{
- pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
Ntl_ObjForEachFanin( pObj, pNet, k )
Ntl_ObjSetFanin( pObj->pCopy, pNet->pCopy, k );
Ntl_ObjForEachFanout( pObj, pNet, k )
@@ -381,7 +397,7 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
if ( Ntl_ObjIsLatch(pObj) )
((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
if ( Ntl_ObjIsNode(pObj) )
- ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew, pObj->pSop );
+ ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew->pMemSops, pObj->pSop );
}
pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;
diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c
index 68b5cfe8..c86ab47b 100644
--- a/src/aig/ntl/ntlObj.c
+++ b/src/aig/ntl/ntlObj.c
@@ -245,10 +245,10 @@ char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName )
SeeAlso []
***********************************************************************/
-char * Ntl_ManStoreSop( Ntl_Man_t * p, char * pSop )
+char * Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop )
{
char * pStore;
- pStore = Aig_MmFlexEntryFetch( p->pMemSops, strlen(pSop) + 1 );
+ pStore = Aig_MmFlexEntryFetch( pMan, strlen(pSop) + 1 );
strcpy( pStore, pSop );
return pStore;
}
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index dd74f9ba..23bb6d76 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -1048,7 +1048,7 @@ static char * Ioa_ReadParseTableBlif( Ioa_ReadMod_t * p, char * pTable, int nFan
// get the tokens
Ioa_ReadSplitIntoTokens( vTokens, pTable, '.' );
if ( Vec_PtrSize(vTokens) == 0 )
- return Ntl_ManStoreSop( p->pMan->pDesign, " 0\n" );
+ return Ntl_ManStoreSop( p->pMan->pDesign->pMemSops, " 0\n" );
if ( Vec_PtrSize(vTokens) == 1 )
{
pOutput = Vec_PtrEntry( vTokens, 0 );
@@ -1057,7 +1057,7 @@ static char * Ioa_ReadParseTableBlif( Ioa_ReadMod_t * p, char * pTable, int nFan
sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Ioa_ReadGetLine(p->pMan, pOutput), pOutput );
return NULL;
}
- return Ntl_ManStoreSop( p->pMan->pDesign, (pOutput[0] == '0') ? " 0\n" : " 1\n" );
+ return Ntl_ManStoreSop( p->pMan->pDesign->pMemSops, (pOutput[0] == '0') ? " 0\n" : " 1\n" );
}
pProduct = Vec_PtrEntry( vTokens, 0 );
if ( Vec_PtrSize(vTokens) % 2 == 1 )
@@ -1123,12 +1123,6 @@ static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine )
// parse the regular name line
assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") );
pNameOut = Vec_PtrEntryLast( vTokens );
-/*
- if ( strcmp( pNameOut, "18434" ) == 0 )
- {
- int x = 0;
- }
-*/
pNetOut = Ntl_ModelFindOrCreateNet( p->pNtk, pNameOut );
// create fanins
pNode = Ntl_ModelCreateNode( p->pNtk, Vec_PtrSize(vTokens) - 2 );
@@ -1147,7 +1141,7 @@ static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine )
pNode->pSop = Ioa_ReadParseTableBlif( p, pNameOut + strlen(pNameOut), pNode->nFanins );
if ( pNode->pSop == NULL )
return 0;
- pNode->pSop = Ntl_ManStoreSop( p->pNtk->pMan, pNode->pSop );
+ pNode->pSop = Ntl_ManStoreSop( p->pNtk->pMan->pMemSops, pNode->pSop );
return 1;
}
diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c
index 3b9cd61f..000b8f0a 100644
--- a/src/aig/ntl/ntlSweep.c
+++ b/src/aig/ntl/ntlSweep.c
@@ -90,31 +90,23 @@ void Ntl_ManSweepMark( Ntl_Man_t * p )
SeeAlso []
***********************************************************************/
-Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose )
+int Ntl_ManSweep( Ntl_Man_t * p, 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;
- }
+ int Counter = 0;
// remember the number of objects
- pRoot = Ntl_ManRootModel( pNew );
+ pRoot = Ntl_ManRootModel( p );
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 );
+ Ntl_ManSweepMark( p );
// remove the useless objects and their nets
Ntl_ModelForEachObj( pRoot, pObj, i )
@@ -126,20 +118,22 @@ Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose )
}
// remove the fanout nets
Ntl_ObjForEachFanout( pObj, pNet, k )
- Ntl_ModelDeleteNet( pRoot, Ntl_ObjFanout0(pObj) );
+ if ( pNet != NULL )
+ Ntl_ModelDeleteNet( pRoot, pNet );
// remove the object
if ( Ntl_ObjIsNode(pObj) && Ntl_ObjFaninNum(pObj) == 1 )
pRoot->nObjs[NTL_OBJ_LUT1]--;
- else
+ else
pRoot->nObjs[pObj->Type]--;
Vec_PtrWriteEntry( pRoot->vObjs, pObj->Id, NULL );
- pObj->Id = NTL_OBJ_NONE;
+ pObj->Type = NTL_OBJ_NONE;
+ Counter++;
}
// print detailed statistics of sweeping
if ( fVerbose )
{
- printf( "Sweep:" );
+ printf( "Swept away:" );
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] );
@@ -153,9 +147,10 @@ Ntl_Man_t * Ntl_ManSweep( Ntl_Man_t * p, Aig_Man_t * pAig, int fVerbose )
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;
+ if ( !Ntl_ManCheck( p ) )
+ printf( "Ntl_ManSweep: The check has failed for design %s.\n", p->pName );
+ return Counter;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index 07794492..c3acc0b1 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -219,7 +219,7 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
/**Function*************************************************************
- Synopsis [Finds or creates the net.]
+ Synopsis [Sets the driver of the net.]
Description []
@@ -241,7 +241,29 @@ int Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
/**Function*************************************************************
- Synopsis [Finds or creates the net.]
+ Synopsis [Clears the driver of the net.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet )
+{
+ if ( pObj->pFanio[pObj->nFanins] == NULL )
+ return 0;
+ if ( pNet->pDriver == NULL )
+ return 0;
+ pObj->pFanio[pObj->nFanins] = NULL;
+ pNet->pDriver = NULL;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of nets.]
Description []
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 626bcbe1..83586e42 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -107,157 +107,6 @@ int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p )
/**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;
- Ntl_Net_t * pNetCo, * pNetFanin;
- Ntl_Obj_t * pObj;
- Ntl_Mod_t * pRoot;
- int i, k, Counter;
- pRoot = Ntl_ManRootModel( p );
- // collect the nets of the root model
- vCoNets = Vec_PtrAlloc( 1000 );
- Ntl_ModelForEachPo( pRoot, pObj, i )
- if ( !Ntl_ObjFanin0(pObj)->fMark )
- {
- Ntl_ObjFanin0(pObj)->fMark = 1;
- Vec_PtrPush( vCoNets, Ntl_ObjFanin0(pObj) );
- }
- Ntl_ModelForEachLatch( pRoot, pObj, i )
- if ( !Ntl_ObjFanin0(pObj)->fMark )
- {
- Ntl_ObjFanin0(pObj)->fMark = 1;
- Vec_PtrPush( vCoNets, Ntl_ObjFanin0(pObj) );
- }
- Ntl_ModelForEachBox( pRoot, pObj, k )
- Ntl_ObjForEachFanin( pObj, pNetCo, i )
- if ( !pNetCo->fMark )
- {
- pNetCo->fMark = 1;
- Vec_PtrPush( vCoNets, pNetCo );
- }
- // check the nets
- Vec_PtrForEachEntry( vCoNets, pNetCo, i )
- {
- if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
- continue;
- if ( Ntl_ObjFaninNum(pNetCo->pDriver) != 1 )
- break;
- pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
- if ( !Ntl_ObjIsNode(pNetFanin->pDriver) )
- break;
- }
- if ( i < Vec_PtrSize(vCoNets) )
- {
- Vec_PtrFree( vCoNets );
- return 0;
- }
-
-
- // remove the buffers/inverters
- Counter = 0;
- Vec_PtrForEachEntry( vCoNets, pNetCo, i )
- {
- pNetCo->fMark = 0;
- if ( !Ntl_ObjIsNode(pNetCo->pDriver) )
- continue;
- // if this net is driven by an interver
- // set the complemented attribute of the CO
- assert( Ntl_ObjFaninNum(pNetCo->pDriver) == 1 );
- pNetCo->fCompl = (int)(pNetCo->pDriver->pSop[0] == '0');
- // remove the driver
- Vec_PtrWriteEntry( pRoot->vObjs, pNetCo->pDriver->Id, NULL );
- // remove the net
- pNetFanin = Ntl_ObjFanin0(pNetCo->pDriver);
- Ntl_ModelDeleteNet( pRoot, pNetFanin );
- // make the CO net point to the new driver
- assert( Ntl_ObjIsNode(pNetFanin->pDriver) );
- pNetCo->pDriver = NULL;
- pNetFanin->pDriver->pFanio[pNetFanin->pDriver->nFanins] = NULL;
- Ntl_ModelSetNetDriver( pNetFanin->pDriver, pNetCo );
- Counter++;
- }
- Vec_PtrFree( vCoNets );
- 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;
-}
-
-/**Function*************************************************************
-
Synopsis [Derives the array of CI names.]
Description []
@@ -362,6 +211,119 @@ int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
return 1;
}
+/**Function*************************************************************
+
+ Synopsis [Convert initial values of registers to be zero.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManSetZeroInitValues( Ntl_Man_t * p )
+{
+ Ntl_Mod_t * pRoot;
+ Ntl_Obj_t * pObj;
+ int i;
+ pRoot = Ntl_ManRootModel(p);
+ Ntl_ModelForEachLatch( pRoot, pObj, i )
+ pObj->LatchId &= ~3;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the netlist to have latches with const-0 init-values.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManAddInverters( Ntl_Obj_t * pObj )
+{
+ char * pStore;
+ Ntl_Mod_t * pRoot = pObj->pModel;
+ Ntl_Man_t * pMan = pRoot->pMan;
+ Ntl_Net_t * pNetLo, * pNetLi, * pNetLoInv, * pNetLiInv;
+ Ntl_Obj_t * pNode;
+ int nLength, RetValue;
+ assert( (pObj->LatchId & 3) == 1 );
+ // get the nets
+ pNetLi = Ntl_ObjFanin0(pObj);
+ pNetLo = Ntl_ObjFanout0(pObj);
+ // get storage for net names
+ nLength = strlen(pNetLi->pName) + strlen(pNetLo->pName) + 10;
+ pStore = Aig_MmFlexEntryFetch( pMan->pMemSops, nLength );
+ // create input interter
+ pNode = Ntl_ModelCreateNode( pRoot, 1 );
+ pNode->pSop = Ntl_ManStoreSop( pMan->pMemSops, "0 1\n" );
+ Ntl_ObjSetFanin( pNode, pNetLi, 0 );
+ // create input net
+ strcpy( pStore, pNetLi->pName );
+ strcat( pStore, "_inv" );
+ if ( Ntl_ModelFindNet( pRoot, pStore ) )
+ {
+ printf( "Ntl_ManTransformInitValues(): Internal error! Cannot create net with LI-name + _inv\n" );
+ return;
+ }
+ pNetLiInv = Ntl_ModelFindOrCreateNet( pRoot, pStore );
+ RetValue = Ntl_ModelSetNetDriver( pNode, pNetLiInv );
+ assert( RetValue );
+ // connect latch to the input net
+ Ntl_ObjSetFanin( pObj, pNetLiInv, 0 );
+ // disconnect latch from the output net
+ RetValue = Ntl_ModelClearNetDriver( pObj, pNetLo );
+ assert( RetValue );
+ // create the output net
+ strcpy( pStore, pNetLo->pName );
+ strcat( pStore, "_inv" );
+ if ( Ntl_ModelFindNet( pRoot, pStore ) )
+ {
+ printf( "Ntl_ManTransformInitValues(): Internal error! Cannot create net with LO-name + _inv\n" );
+ return;
+ }
+ pNetLoInv = Ntl_ModelFindOrCreateNet( pRoot, pStore );
+ RetValue = Ntl_ModelSetNetDriver( pObj, pNetLoInv );
+ assert( RetValue );
+ // create output interter
+ pNode = Ntl_ModelCreateNode( pRoot, 1 );
+ pNode->pSop = Ntl_ManStoreSop( pMan->pMemSops, "0 1\n" );
+ Ntl_ObjSetFanin( pNode, pNetLoInv, 0 );
+ // redirect the old output net
+ RetValue = Ntl_ModelSetNetDriver( pNode, pNetLo );
+ assert( RetValue );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Transforms the netlist to have latches with const-0 init-values.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ntl_ManTransformInitValues( Ntl_Man_t * p )
+{
+ Ntl_Mod_t * pRoot;
+ Ntl_Obj_t * pObj;
+ int i;
+ pRoot = Ntl_ManRootModel(p);
+ Ntl_ModelForEachLatch( pRoot, pObj, i )
+ {
+ if ( (pObj->LatchId & 3) == 1 )
+ Ntl_ManAddInverters( pObj );
+ pObj->LatchId &= ~3;
+ }
+
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index cefa38d3..24fa1370 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -120,7 +120,7 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
if ( Ntl_ObjFanin(pObj, 1) != NULL )
fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName );
else if ( pObj->LatchId >> 2 )
- fprintf( pFile, " clock" ), fClockAdded = 1;
+ fprintf( pFile, " clock99" ), fClockAdded = 1;
fprintf( pFile, " %d", pObj->LatchId & 3 );
fprintf( pFile, "\n" );
}
@@ -135,7 +135,7 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
}
}
if ( fClockAdded )
- fprintf( pFile, ".names clock\n 0\n" );
+ fprintf( pFile, ".names clock99\n 0\n" );
fprintf( pFile, ".end\n\n" );
}
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index 6fc84893..c087cde8 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -85,7 +85,7 @@ struct Nwk_Obj_t_
void * pNext; // temporary pointer
// node information
unsigned Type : 3; // object type
- unsigned fCompl : 1; // complemented attribute
+ unsigned fInvert : 1; // complemented attribute
unsigned MarkA : 1; // temporary mark
unsigned MarkB : 1; // temporary mark
unsigned PioId : 26; // number of this node in the PI/PO list
@@ -123,6 +123,8 @@ static inline Nwk_Obj_t * Nwk_ManCi( Nwk_Man_t * p, int i ) { return Vec_P
static inline Nwk_Obj_t * Nwk_ManCo( Nwk_Man_t * p, int i ) { return Vec_PtrEntry( p->vCos, i ); }
static inline Nwk_Obj_t * Nwk_ManObj( Nwk_Man_t * p, int i ) { return Vec_PtrEntry( p->vObjs, i ); }
+static inline int Nwk_ObjId( Nwk_Obj_t * p ) { return p->Id; }
+static inline int Nwk_ObjPioNum( Nwk_Obj_t * p ) { return p->PioId; }
static inline int Nwk_ObjFaninNum( Nwk_Obj_t * p ) { return p->nFanins; }
static inline int Nwk_ObjFanoutNum( Nwk_Obj_t * p ) { return p->nFanouts; }
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index f5b2b7f8..effffcf7 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -292,7 +292,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
else if ( Aig_ObjIsPo(pObj) )
{
pObjNew = Nwk_ManCreateCo( pNtk );
- pObjNew->fCompl = Aig_ObjFaninC0(pObj);
+ pObjNew->fInvert = Aig_ObjFaninC0(pObj);
Nwk_ObjAddFanin( pObjNew, Aig_ObjFanin0(pObj)->pData );
}
else if ( Aig_ObjIsConst1(pObj) )
diff --git a/src/aig/nwk/nwkStrash.c b/src/aig/nwk/nwkStrash.c
index 8e49a586..a4ce5e39 100644
--- a/src/aig/nwk/nwkStrash.c
+++ b/src/aig/nwk/nwkStrash.c
@@ -119,7 +119,7 @@ Aig_Man_t * Nwk_ManStrash( Nwk_Man_t * pNtk )
}
else if ( Nwk_ObjIsCo(pObj) )
{
- pObjNew = Aig_ObjCreatePo( pMan, Aig_NotCond(Nwk_ObjFanin0(pObj)->pCopy, pObj->fCompl) );
+ pObjNew = Aig_ObjCreatePo( pMan, Aig_NotCond(Nwk_ObjFanin0(pObj)->pCopy, pObj->fInvert) );
Level = Aig_ObjLevel( pObjNew );
Tim_ManSetCoArrival( pMan->pManTime, pObj->PioId, (float)Level );
}
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index 97c95d27..f30f7251 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -19,7 +19,8 @@
***********************************************************************/
#include "nwk.h"
-#include "math.h"
+#include "kit.h"
+#include <math.h>
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -250,9 +251,93 @@ void Nwk_ObjPrint( Nwk_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames )
+void Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames )
{
- printf( "Dumping logic network is currently not supported.\n" );
+ FILE * pFile;
+ Vec_Ptr_t * vNodes;
+ Vec_Int_t * vTruth;
+ Vec_Int_t * vCover;
+ Nwk_Obj_t * pObj, * pFanin;
+ Aig_MmFlex_t * pMem;
+ char * pSop = NULL;
+ unsigned * pTruth;
+ int i, k, nDigits, Counter = 0;
+ if ( Nwk_ManPoNum(pNtk) == 0 )
+ {
+ printf( "Nwk_ManDumpBlif(): Network does not have POs.\n" );
+ return;
+ }
+ // collect nodes in the DFS order
+ nDigits = Aig_Base10Log( Nwk_ManObjNumMax(pNtk) );
+ // write the file
+ pFile = fopen( pFileName, "w" );
+ fprintf( pFile, "# BLIF file written by procedure Nwk_ManDumpBlif()\n" );
+// fprintf( pFile, "# http://www.eecs.berkeley.edu/~alanmi/abc/\n" );
+ fprintf( pFile, ".model %s\n", pNtk->pName );
+ // write PIs
+ fprintf( pFile, ".inputs" );
+ Nwk_ManForEachCi( pNtk, pObj, i )
+ if ( vPiNames )
+ fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, i) );
+ else
+ fprintf( pFile, " n%0*d", nDigits, pObj->Id );
+ fprintf( pFile, "\n" );
+ // write POs
+ fprintf( pFile, ".outputs" );
+ Nwk_ManForEachCo( pNtk, pObj, i )
+ if ( vPoNames )
+ fprintf( pFile, " %s", Vec_PtrEntry(vPoNames, i) );
+ else
+ fprintf( pFile, " n%0*d", nDigits, pObj->Id );
+ fprintf( pFile, "\n" );
+ // write nodes
+ pMem = Aig_MmFlexStart();
+ vTruth = Vec_IntAlloc( 1 << 16 );
+ vCover = Vec_IntAlloc( 1 << 16 );
+ vNodes = Nwk_ManDfs( pNtk );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ if ( !Nwk_ObjIsNode(pObj) )
+ continue;
+ // derive SOP for the AIG
+ pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+ if ( Hop_IsComplement(pObj->pFunc) )
+ Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
+ pSop = Kit_PlaFromTruth( pMem, pTruth, Nwk_ObjFaninNum(pObj), vCover );
+ // write the node
+ fprintf( pFile, ".names" );
+ if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
+ {
+ Nwk_ObjForEachFanin( pObj, pFanin, k )
+ if ( vPiNames && Nwk_ObjIsPi(pFanin) )
+ fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(pFanin)) );
+ else
+ fprintf( pFile, " n%0*d", nDigits, pFanin->Id );
+ }
+ fprintf( pFile, " n%0*d\n", nDigits, pObj->Id );
+ // write the function
+ fprintf( pFile, "%s", pSop );
+ }
+ Vec_IntFree( vCover );
+ Vec_IntFree( vTruth );
+ Vec_PtrFree( vNodes );
+ Aig_MmFlexStop( pMem, 0 );
+ // write POs
+ Nwk_ManForEachCo( pNtk, pObj, i )
+ {
+ fprintf( pFile, ".names" );
+ if ( vPiNames && Nwk_ObjIsPi(Nwk_ObjFanin0(pObj)) )
+ fprintf( pFile, " %s", Vec_PtrEntry(vPiNames, Nwk_ObjPioNum(Nwk_ObjFanin0(pObj))) );
+ else
+ fprintf( pFile, " n%0*d", nDigits, Nwk_ObjFanin0(pObj)->Id );
+ if ( vPoNames )
+ fprintf( pFile, " %s\n", Vec_PtrEntry(vPoNames, Nwk_ObjPioNum(pObj)) );
+ else
+ fprintf( pFile, " n%0*d\n", nDigits, pObj->Id );
+ fprintf( pFile, "%d 1\n", !pObj->fInvert );
+ }
+ fprintf( pFile, ".end\n\n" );
+ fclose( pFile );
}
/**Function*************************************************************
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9ae7f0da..9cc2fd53 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -226,6 +226,7 @@ static int Abc_CommandAbc8Scl ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc8Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Ssw ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Sweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Zero ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Cec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8DSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -470,6 +471,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC8", "*lcorr", Abc_CommandAbc8Lcorr, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*ssw", Abc_CommandAbc8Ssw, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*sw", Abc_CommandAbc8Sweep, 0 );
+ Cmd_CommandAdd( pAbc, "ABC8", "*zero", Abc_CommandAbc8Zero, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*cec", Abc_CommandAbc8Cec, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*dsec", Abc_CommandAbc8DSec, 0 );
@@ -14780,6 +14782,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc8Read(): AIG extraction has failed.\n" );
return 1;
}
+
return 0;
usage:
@@ -14943,7 +14946,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
else
{
pTemp = pAbc->pAbc8Ntl;
- printf( "Writing the original design.\n" );
+ printf( "Writing the unmapped netlist.\n" );
Ioa_WriteBlif( pTemp, pFileName );
}
}
@@ -14979,7 +14982,7 @@ int Abc_CommandAbc8WriteLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Nwk_ManDumpBlif( void * p, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
// set defaults
- fAig = 1;
+ fAig = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
{
@@ -15003,6 +15006,7 @@ int Abc_CommandAbc8WriteLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
pFileName = argv[globalUtilOptind];
// vCiNames = Ntl_ManCollectCiNames( pAbc->pAbc8Ntl );
// vCoNames = Ntl_ManCollectCoNames( pAbc->pAbc8Ntl );
+ // the problem is duplicated CO names...
if ( fAig )
{
if ( pAbc->pAbc8Aig != NULL )
@@ -16169,12 +16173,14 @@ usage:
***********************************************************************/
int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Aig_Man_t * pAigNew;
+ void * pNtlNew;
int c, fVerbose;
int nPartSize;
int nConfLimit;
int nLevelMax;
- extern Aig_Man_t * Ntl_ManFraig( void * p, Aig_Man_t * pAig, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose );
+ extern Aig_Man_t * Ntl_ManExtract( void * p );
+ extern void * Ntl_ManFraig( void * p, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose );
+ extern void Ntl_ManFree( void * p );
// set defaults
nPartSize = 0;
@@ -16234,29 +16240,33 @@ int Abc_CommandAbc8Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc8Fraig(): There is no design to SAT sweep.\n" );
return 1;
}
- if ( pAbc->pAbc8Aig == NULL )
- {
- printf( "Abc_CommandAbc8Fraig(): There is no AIG to SAT sweep.\n" );
- return 1;
- }
// get the input file name
- pAigNew = Ntl_ManFraig( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, nPartSize, nConfLimit, nLevelMax, fVerbose );
- if ( pAigNew == NULL )
+ pNtlNew = Ntl_ManFraig( pAbc->pAbc8Ntl, nPartSize, nConfLimit, nLevelMax, fVerbose );
+ if ( pNtlNew == NULL )
{
printf( "Abc_CommandAbc8Fraig(): Tranformation of the AIG has failed.\n" );
return 1;
}
- if ( pAbc->pAbc8Aig )
- Aig_ManStop( pAbc->pAbc8Aig );
- pAbc->pAbc8Aig = pAigNew;
- Abc_CommandAbc8Sweep( pAbc, 0, NULL );
+ Abc_FrameClearDesign();
+ pAbc->pAbc8Ntl = pNtlNew;
+ if ( pAbc->pAbc8Ntl == NULL )
+ {
+ printf( "Abc_CommandAbc8Fraig(): Reading BLIF has failed.\n" );
+ return 1;
+ }
+ pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+ if ( pAbc->pAbc8Aig == NULL )
+ {
+ printf( "Abc_CommandAbc8Fraig(): AIG extraction has failed.\n" );
+ return 1;
+ }
return 0;
usage:
fprintf( stdout, "usage: *fraig [-P num] [-C num] [-L num] [-vh]\n" );
- fprintf( stdout, "\t performs SAT sweeping with white-boxes\n" );
+ fprintf( stdout, "\t applies SAT sweeping to netlist with white-boxes\n" );
fprintf( stdout, "\t-P num : partition size (0 = partitioning is not used) [default = %d]\n", nPartSize );
fprintf( stdout, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
fprintf( stdout, "\t-L num : limit on node level to fraig (0 = fraig all nodes) [default = %d]\n", nLevelMax );
@@ -16278,12 +16288,13 @@ usage:
***********************************************************************/
int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Aig_Man_t * pAigNew;
+ void * pNtlNew;
int c;
int fLatchConst;
int fLatchEqual;
int fVerbose;
- extern Aig_Man_t * Ntl_ManScl( void * p, Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose );
+ extern Aig_Man_t * Ntl_ManExtract( void * p );
+ extern void * Ntl_ManScl( void * p, int fLatchConst, int fLatchEqual, int fVerbose );
extern int Ntl_ManIsComb( void * p );
// set defaults
@@ -16316,35 +16327,39 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc8Scl(): There is no design to SAT sweep.\n" );
return 1;
}
- if ( pAbc->pAbc8Aig == NULL )
- {
- printf( "Abc_CommandAbc8Scl(): There is no AIG to SAT sweep.\n" );
- return 1;
- }
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
- fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+ fprintf( stdout, "Abc_CommandAbc8Scl(): The network is combinational (run \"*fraig\").\n" );
return 0;
}
// get the input file name
- pAigNew = Ntl_ManScl( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, fLatchConst, fLatchEqual, fVerbose );
- if ( pAigNew == NULL )
+ pNtlNew = Ntl_ManScl( pAbc->pAbc8Ntl, fLatchConst, fLatchEqual, fVerbose );
+ if ( pNtlNew == NULL )
{
printf( "Abc_CommandAbc8Scl(): Tranformation of the AIG has failed.\n" );
return 1;
}
- if ( pAbc->pAbc8Aig )
- Aig_ManStop( pAbc->pAbc8Aig );
- pAbc->pAbc8Aig = pAigNew;
- Abc_CommandAbc8Sweep( pAbc, 0, NULL );
+ Abc_FrameClearDesign();
+ pAbc->pAbc8Ntl = pNtlNew;
+ if ( pAbc->pAbc8Ntl == NULL )
+ {
+ printf( "Abc_CommandAbc8Scl(): Reading BLIF has failed.\n" );
+ return 1;
+ }
+ pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+ if ( pAbc->pAbc8Aig == NULL )
+ {
+ printf( "Abc_CommandAbc8Scl(): AIG extraction has failed.\n" );
+ return 1;
+ }
return 0;
usage:
fprintf( stdout, "usage: *scl [-cevh]\n" );
- fprintf( stdout, "\t performs sequential cleanup of the current network\n" );
+ fprintf( stdout, "\t performs sequential cleanup of the netlist\n" );
fprintf( stdout, "\t by removing nodes and latches that do not feed into POs\n" );
fprintf( stdout, "\t-c : sweep stuck-at latches detected by ternary simulation [default = %s]\n", fLatchConst? "yes": "no" );
fprintf( stdout, "\t-e : merge equal latches (same data inputs and init states) [default = %s]\n", fLatchEqual? "yes": "no" );
@@ -16366,12 +16381,13 @@ usage:
***********************************************************************/
int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Aig_Man_t * pAigNew;
+ void * pNtlNew;
int c;
int nFramesP;
int nConfMax;
int fVerbose;
- extern Aig_Man_t * Ntl_ManLcorr( void * p, Aig_Man_t * pAig, int nConfMax, int fVerbose );
+ extern Aig_Man_t * Ntl_ManExtract( void * p );
+ extern void * Ntl_ManLcorr( void * p, int nConfMax, int fVerbose );
extern int Ntl_ManIsComb( void * p );
// set defaults
@@ -16417,38 +16433,42 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pAbc8Ntl == NULL )
{
- printf( "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
- return 1;
- }
- if ( pAbc->pAbc8Aig == NULL )
- {
- printf( "Abc_CommandAbc8Ssw(): There is no AIG to SAT sweep.\n" );
+ printf( "Abc_CommandAbc8Lcorr(): There is no design to SAT sweep.\n" );
return 1;
}
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
- fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+ fprintf( stdout, "Abc_CommandAbc8Lcorr(): The network is combinational (run \"*fraig\").\n" );
return 0;
}
// get the input file name
- pAigNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, nConfMax, fVerbose );
- if ( pAigNew == NULL )
+ pNtlNew = Ntl_ManLcorr( pAbc->pAbc8Ntl, nConfMax, fVerbose );
+ if ( pNtlNew == NULL )
{
- printf( "Abc_CommandAbc8Ssw(): Tranformation of the AIG has failed.\n" );
+ printf( "Abc_CommandAbc8Lcorr(): Tranformation of the AIG has failed.\n" );
return 1;
}
- if ( pAbc->pAbc8Aig )
- Aig_ManStop( pAbc->pAbc8Aig );
- pAbc->pAbc8Aig = pAigNew;
- Abc_CommandAbc8Sweep( pAbc, 0, NULL );
+ Abc_FrameClearDesign();
+ pAbc->pAbc8Ntl = pNtlNew;
+ if ( pAbc->pAbc8Ntl == NULL )
+ {
+ printf( "Abc_CommandAbc8Lcorr(): Reading BLIF has failed.\n" );
+ return 1;
+ }
+ pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+ if ( pAbc->pAbc8Aig == NULL )
+ {
+ printf( "Abc_CommandAbc8Lcorr(): AIG extraction has failed.\n" );
+ return 1;
+ }
return 0;
usage:
fprintf( stdout, "usage: *lcorr [-C num] [-vh]\n" );
- fprintf( stdout, "\t computes latch correspondence using 1-step induction\n" );
+ fprintf( stdout, "\t computes latch correspondence for the netlist\n" );
// fprintf( stdout, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
fprintf( stdout, "\t-C num : max conflict number when proving latch equivalence [default = %d]\n", nConfMax );
fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -16469,10 +16489,11 @@ usage:
***********************************************************************/
int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Aig_Man_t * pAigNew;
+ void * pNtlNew;
Fra_Ssw_t Pars, * pPars = &Pars;
int c;
- extern Aig_Man_t * Ntl_ManSsw( void * p, Aig_Man_t * pAig, Fra_Ssw_t * pPars );
+ extern Aig_Man_t * Ntl_ManExtract( void * p );
+ extern void * Ntl_ManSsw( void * p, Fra_Ssw_t * pPars );
extern int Ntl_ManIsComb( void * p );
// set defaults
@@ -16593,11 +16614,6 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
return 1;
}
- if ( pAbc->pAbc8Aig == NULL )
- {
- printf( "Abc_CommandAbc8Ssw(): There is no AIG to SAT sweep.\n" );
- return 1;
- }
if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
{
@@ -16618,22 +16634,31 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the input file name
- pAigNew = Ntl_ManSsw( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pPars );
- if ( pAigNew == NULL )
+ pNtlNew = Ntl_ManSsw( pAbc->pAbc8Ntl, pPars );
+ if ( pNtlNew == NULL )
{
printf( "Abc_CommandAbc8Ssw(): Tranformation of the AIG has failed.\n" );
return 1;
}
- if ( pAbc->pAbc8Aig )
- Aig_ManStop( pAbc->pAbc8Aig );
- pAbc->pAbc8Aig = pAigNew;
- Abc_CommandAbc8Sweep( pAbc, 0, NULL );
+ Abc_FrameClearDesign();
+ pAbc->pAbc8Ntl = pNtlNew;
+ if ( pAbc->pAbc8Ntl == NULL )
+ {
+ printf( "Abc_CommandAbc8Ssw(): Reading BLIF has failed.\n" );
+ return 1;
+ }
+ pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+ if ( pAbc->pAbc8Aig == NULL )
+ {
+ printf( "Abc_CommandAbc8Ssw(): AIG extraction has failed.\n" );
+ return 1;
+ }
return 0;
usage:
fprintf( stdout, "usage: *ssw [-PQNFL num] [-lrfetvh]\n" );
- fprintf( stdout, "\t performs sequential sweep using K-step induction\n" );
+ fprintf( stdout, "\t performs sequential sweep using K-step induction on the netlist \n" );
fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
fprintf( stdout, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP );
@@ -16664,11 +16689,10 @@ usage:
***********************************************************************/
int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- void * pNtlNew;
+ int Counter;
int fVerbose;
int c;
- extern void * Ntl_ManSweep( void * p, Aig_Man_t * pAig, int fVerbose );
- extern Aig_Man_t * Ntl_ManExtract( void * p );
+ extern int Ntl_ManSweep( void * p, int fVerbose );
// set defaults
fVerbose = 0;
@@ -16691,34 +16715,75 @@ int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc8Sweep(): There is no design to sweep.\n" );
return 1;
}
- if ( pAbc->pAbc8Aig == NULL )
- {
- printf( "Abc_CommandAbc8Sweep(): There is no AIG to use.\n" );
- return 1;
- }
// sweep the current design
- pNtlNew = Ntl_ManSweep( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, fVerbose );
- if ( pNtlNew == NULL )
+ Counter = Ntl_ManSweep( pAbc->pAbc8Ntl, fVerbose );
+ if ( Counter == 0 )
+ printf( "The netlist is unchanged by sweep.\n" );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: *sw [-h]\n" );
+ fprintf( stdout, "\t performs structural sweep of the netlist\n" );
+ fprintf( stdout, "\t removes dangling nodes, registers, and white-boxes\n" );
+ fprintf( stdout, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc8Zero( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ void * pNtlNew;
+ int fVerbose;
+ int c;
+ extern void Ntl_ManTransformInitValues( void * p );
+
+ // set defaults
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
- printf( "Abc_CommandAbc8Sweep(): Sweeping has failed.\n" );
- return 1;
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
}
- // replace
- Abc_FrameClearDesign();
- pAbc->pAbc8Ntl = pNtlNew;
- pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
- if ( pAbc->pAbc8Aig == NULL )
+ if ( pAbc->pAbc8Ntl == NULL )
{
- printf( "Abc_CommandAbc8Sweep(): AIG extraction has failed.\n" );
+ printf( "Abc_CommandAbc8Zero(): There is no design to convert.\n" );
return 1;
}
+
+ // transform the registers
+ pNtlNew = pAbc->pAbc8Ntl;
+ pAbc->pAbc8Ntl = NULL;
+ Ntl_ManTransformInitValues( pNtlNew );
+
+ // replace the design
+ Abc_FrameClearDesign();
+ pAbc->pAbc8Ntl = pNtlNew;
return 0;
usage:
- fprintf( stdout, "usage: *sw [-h]\n" );
- fprintf( stdout, "\t performs structural sweep of the design\n" );
- fprintf( stdout, "\t removes dangling nodes, registers, and white-boxes\n" );
+ fprintf( stdout, "usage: *zero [-h]\n" );
+ fprintf( stdout, "\t converts registers to have constant-0 initial value\n" );
fprintf( stdout, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
@@ -16746,7 +16811,7 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
int nConfLimit;
int fSmart;
int nPartSize;
- extern Aig_Man_t * Ntl_ManCollapse( void * p, int fSeq );
+ extern Aig_Man_t * Ntl_ManCollapse( void * p );
extern void * Ntl_ManDup( void * pOld );
extern void Ntl_ManFree( void * p );
extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
@@ -16827,14 +16892,14 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// derive AIGs
- pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 );
+ pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl );
pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
if ( pTemp == NULL )
{
printf( "Abc_CommandAbc8Cec(): Inserting the design has failed.\n" );
return 1;
}
- pAig2 = Ntl_ManCollapse( pTemp, 0 );
+ pAig2 = Ntl_ManCollapse( pTemp );
Ntl_ManFree( pTemp );
// perform verification
@@ -16886,7 +16951,7 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFrames = 16;
- fRetimeFirst = 1;
+ fRetimeFirst = 0;
fFraiging = 1;
fVerbose = 0;
fVeryVerbose = 0;
diff --git a/src/base/abci/abcAbc8.c b/src/base/abci/abcAbc8.c
index e918417c..b2359763 100644
--- a/src/base/abci/abcAbc8.c
+++ b/src/base/abci/abcAbc8.c
@@ -129,7 +129,7 @@ Abc_Ntk_t * Abc_NtkFromNtkNew( Abc_Ntk_t * pNtkOld, Nwk_Man_t * pNtk )
Nwk_ManForEachCo( pNtk, pObj, i )
{
pObjNew = Abc_NtkCreatePo( pNtkNew );
- if ( pObj->fCompl )
+ if ( pObj->fInvert )
pFaninNew = Abc_NtkCreateNodeInv( pNtkNew, Nwk_ObjFanin0(pObj)->pCopy );
else
pFaninNew = Nwk_ObjFanin0(pObj)->pCopy;
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-02 10:55:44 +0000