summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h20
-rw-r--r--src/base/abci/abc.c43
-rw-r--r--src/base/abci/abcDar.c154
-rw-r--r--src/base/abci/abcDsdRes.c80
-rw-r--r--src/base/abci/abcIvy.c2
-rw-r--r--src/base/abci/abcMeasure.c478
-rw-r--r--src/base/abci/abcPart.c26
-rw-r--r--src/base/abci/abcSweep.c28
-rw-r--r--src/base/abci/abcVerify.c117
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/base/abci/xaaaa.c155
-rw-r--r--src/base/io/ioReadAiger.c2
-rw-r--r--src/base/io/ioWriteAiger.c2
-rw-r--r--src/base/io/ioWriteVerilog.c26
-rw-r--r--src/base/main/mainInt.h4
15 files changed, 1091 insertions, 47 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 98942ca3..3b309b43 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -330,7 +330,7 @@ static inline bool Abc_NtkIsComb( Abc_Ntk_t * pNtk ) { return Ab
static inline bool Abc_NtkHasOnlyLatchBoxes(Abc_Ntk_t * pNtk ){ return Abc_NtkLatchNum(pNtk) == Abc_NtkBoxNum(pNtk); }
// creating simple objects
-extern inline Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
+extern Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
static inline Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PI ); }
static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PO ); }
static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk ) { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BI ); }
@@ -417,8 +417,8 @@ static inline Abc_Obj_t * Abc_ObjChild1( Abc_Obj_t * pObj ) { return Ab
static inline Abc_Obj_t * Abc_ObjChildCopy( Abc_Obj_t * pObj, int i ){ return Abc_ObjNotCond( Abc_ObjFanin(pObj,i)->pCopy, Abc_ObjFaninC(pObj,i) ); }
static inline Abc_Obj_t * Abc_ObjChild0Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); }
static inline Abc_Obj_t * Abc_ObjChild1Copy( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ); }
-static inline Abc_Obj_t * Abc_ObjChild0Data( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin0(pObj)->pData, Abc_ObjFaninC0(pObj) ); }
-static inline Abc_Obj_t * Abc_ObjChild1Data( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_ObjFanin1(pObj)->pData, Abc_ObjFaninC1(pObj) ); }
+static inline Abc_Obj_t * Abc_ObjChild0Data( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( (Abc_Obj_t *)Abc_ObjFanin0(pObj)->pData, Abc_ObjFaninC0(pObj) ); }
+static inline Abc_Obj_t * Abc_ObjChild1Data( Abc_Obj_t * pObj ) { return Abc_ObjNotCond( (Abc_Obj_t *)Abc_ObjFanin1(pObj)->pData, Abc_ObjFaninC1(pObj) ); }
static inline Hop_Obj_t * Abc_ObjChild0Equiv( Abc_Obj_t * pObj ) { return Hop_NotCond( Abc_ObjFanin0(pObj)->pEquiv, Abc_ObjFaninC0(pObj) ); }
static inline Hop_Obj_t * Abc_ObjChild1Equiv( Abc_Obj_t * pObj ) { return Hop_NotCond( Abc_ObjFanin1(pObj)->pEquiv, Abc_ObjFaninC1(pObj) ); }
@@ -452,17 +452,17 @@ static inline int Abc_LatchInit( Abc_Obj_t * pLatch ) { assert(Ab
// global BDDs of the nodes
static inline void * Abc_NtkGlobalBdd( Abc_Ntk_t * pNtk ) { return (void *)Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD); }
-static inline DdManager * Abc_NtkGlobalBddMan( Abc_Ntk_t * pNtk ) { return (DdManager *)Vec_AttMan( Abc_NtkGlobalBdd(pNtk) ); }
-static inline DdNode ** Abc_NtkGlobalBddArray( Abc_Ntk_t * pNtk ) { return (DdNode **)Vec_AttArray( Abc_NtkGlobalBdd(pNtk) ); }
-static inline DdNode * Abc_ObjGlobalBdd( Abc_Obj_t * pObj ) { return (DdNode *)Vec_AttEntry( Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id ); }
-static inline void Abc_ObjSetGlobalBdd( Abc_Obj_t * pObj, DdNode * bF ) { Vec_AttWriteEntry( Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id, bF ); }
+static inline DdManager * Abc_NtkGlobalBddMan( Abc_Ntk_t * pNtk ) { return (DdManager *)Vec_AttMan( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) ); }
+static inline DdNode ** Abc_NtkGlobalBddArray( Abc_Ntk_t * pNtk ) { return (DdNode **)Vec_AttArray( (Vec_Att_t *)Abc_NtkGlobalBdd(pNtk) ); }
+static inline DdNode * Abc_ObjGlobalBdd( Abc_Obj_t * pObj ) { return (DdNode *)Vec_AttEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id ); }
+static inline void Abc_ObjSetGlobalBdd( Abc_Obj_t * pObj, DdNode * bF ) { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkGlobalBdd(pObj->pNtk), pObj->Id, bF ); }
// MV variables of the nodes
static inline void * Abc_NtkMvVar( Abc_Ntk_t * pNtk ) { return Vec_PtrEntry(pNtk->vAttrs, VEC_ATTR_MVVAR); }
-static inline void * Abc_NtkMvVarMan( Abc_Ntk_t * pNtk ) { return Abc_NtkMvVar(pNtk)? Vec_AttMan( Abc_NtkMvVar(pNtk) ) : NULL; }
-static inline void * Abc_ObjMvVar( Abc_Obj_t * pObj ) { return Abc_NtkMvVar(pObj->pNtk)? Vec_AttEntry( Abc_NtkMvVar(pObj->pNtk), pObj->Id ) : NULL; }
+static inline void * Abc_NtkMvVarMan( Abc_Ntk_t * pNtk ) { return Abc_NtkMvVar(pNtk)? Vec_AttMan( (Vec_Att_t *)Abc_NtkMvVar(pNtk) ) : NULL; }
+static inline void * Abc_ObjMvVar( Abc_Obj_t * pObj ) { return Abc_NtkMvVar(pObj->pNtk)? Vec_AttEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id ) : NULL; }
static inline int Abc_ObjMvVarNum( Abc_Obj_t * pObj ) { return (Abc_NtkMvVar(pObj->pNtk) && Abc_ObjMvVar(pObj))? *((int*)Abc_ObjMvVar(pObj)) : 2; }
-static inline void Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_AttWriteEntry( Abc_NtkMvVar(pObj->pNtk), pObj->Id, pV ); }
+static inline void Abc_ObjSetMvVar( Abc_Obj_t * pObj, void * pV) { Vec_AttWriteEntry( (Vec_Att_t *)Abc_NtkMvVar(pObj->pNtk), pObj->Id, pV ); }
// outputs the runtime in seconds
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 39d7cb2b..1e0fed0c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -329,6 +329,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Abc_NtkPrint256();
// Kit_TruthCountMintermsPrecomp();
// Kit_DsdPrecompute4Vars();
+
+ Dar_LibStart();
}
/**Function*************************************************************
@@ -344,6 +346,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
***********************************************************************/
void Abc_End()
{
+ Dar_LibStop();
+
Abc_NtkFraigStoreClean();
// Rwt_Man4ExplorePrint();
}
@@ -6034,13 +6038,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_NtkCompareSupports( pNtk );
// Abc_NtkCompareCones( pNtk );
-
+/*
{
extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose );
Vec_Vec_t * vParts;
vParts = Abc_NtkPartitionSmart( pNtk, 1 );
Vec_VecFree( vParts );
}
+*/
+// Abc_Ntk4VarTable( pNtk );
+// Dat_NtkGenerateArrays( pNtk );
return 0;
@@ -7677,7 +7684,8 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
int fUseInv;
int fExdc;
int fVerbose;
- extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
+ int fVeryVerbose;
+ extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -7687,8 +7695,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
fUseInv = 1;
fExdc = 0;
fVerbose = 0;
+ fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "ievh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ievwh" ) ) != EOF )
{
switch ( c )
{
@@ -7701,6 +7710,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
fVerbose ^= 1;
break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -7724,7 +7736,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
// modify the current network
- if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fExdc, fVerbose ) )
+ if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fExdc, fVerbose, fVeryVerbose ) )
{
fprintf( pErr, "Sweeping has failed.\n" );
return 1;
@@ -7732,10 +7744,11 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: fraig_sweep [-evh]\n" );
+ fprintf( pErr, "usage: fraig_sweep [-evwh]\n" );
fprintf( pErr, "\t performs technology-dependent sweep\n" );
fprintf( pErr, "\t-e : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-w : prints equivalence class information [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -8284,7 +8297,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
int c;
extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose );
- extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
+ extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -8375,7 +8388,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( fSweep )
- Abc_NtkFraigSweep( pNtkRes, 0, 0, 0 );
+ Abc_NtkFraigSweep( pNtkRes, 0, 0, 0, 0 );
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -10346,11 +10359,12 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
int nPartSize;
int nConfLimit;
int nInsLimit;
+ int fPartition;
extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );
extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
extern void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose );
-
+ extern void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -10363,8 +10377,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
nPartSize = 0;
nConfLimit = 10000;
nInsLimit = 0;
+ fPartition = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPsvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPpsvh" ) ) != EOF )
{
switch ( c )
{
@@ -10412,6 +10427,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nPartSize < 0 )
goto usage;
break;
+ case 'p':
+ fPartition ^= 1;
+ break;
case 's':
fSat ^= 1;
break;
@@ -10429,7 +10447,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
// perform equivalence checking
- if ( nPartSize )
+ if ( fPartition )
+ Abc_NtkCecFraigPartAuto( pNtk1, pNtk2, nSeconds, fVerbose );
+ else if ( nPartSize )
Abc_NtkCecFraigPart( pNtk1, pNtk2, nSeconds, nPartSize, fVerbose );
else if ( fSat )
Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nInsLimit );
@@ -10445,12 +10465,13 @@ usage:
strcpy( Buffer, "unused" );
else
sprintf( Buffer, "%d", nPartSize );
- fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-P num] [-svh] <file1> <file2>\n" );
+ fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-P num] [-psvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs combinational equivalence checking\n" );
fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
fprintf( pErr, "\t-I num : limit on the number of clause inspections [default = %d]\n", nInsLimit );
fprintf( pErr, "\t-P num : partition size for multi-output networks [default = %s]\n", Buffer );
+ fprintf( pErr, "\t-p : toggle automatic partitioning [default = %s]\n", fPartition? "yes": "no" );
fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
new file mode 100644
index 00000000..0863061b
--- /dev/null
+++ b/src/base/abci/abcDar.c
@@ -0,0 +1,154 @@
+/**CFile****************************************************************
+
+ FileName [abcDar.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [DAG-aware rewriting.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcDar.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
+{
+ Abc_Ntk_t * pNtkAig;
+ Dar_Man_t * pMan;//, * pTemp;
+ assert( Abc_NtkIsStrash(pNtk) );
+ // convert to the AIG manager
+ pMan = Abc_NtkToDar( pNtk );
+ if ( pMan == NULL )
+ return NULL;
+ if ( !Dar_ManCheck( pMan ) )
+ {
+ printf( "Abc_NtkDar: AIG check has failed.\n" );
+ Dar_ManStop( pMan );
+ return NULL;
+ }
+ // perform balance
+ Dar_ManPrintStats( pMan );
+// Dar_ManDumpBlif( pMan, "aig_temp.blif" );
+ pMan->pPars = Dar_ManDefaultParams();
+ Dar_ManRewrite( pMan );
+ Dar_ManPrintStats( pMan );
+ // convert from the AIG manager
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+ if ( pNtkAig == NULL )
+ return NULL;
+ Dar_ManStop( pMan );
+ // make sure everything is okay
+ if ( !Abc_NtkCheck( pNtkAig ) )
+ {
+ printf( "Abc_NtkDar: The network check has failed.\n" );
+ Abc_NtkDelete( pNtkAig );
+ return NULL;
+ }
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the network from the AIG manager into ABC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
+{
+ Dar_Man_t * pMan;
+ Abc_Obj_t * pObj;
+ int i;
+ // create the manager
+ pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) );
+ // transfer the pointers to the basic nodes
+ Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Dar_ManConst1(pMan);
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ pObj->pCopy = (Abc_Obj_t *)Dar_ObjCreatePi(pMan);
+ // perform the conversion of the internal nodes (assumes DFS ordering)
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ pObj->pCopy = (Abc_Obj_t *)Dar_And( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj), (Dar_Obj_t *)Abc_ObjChild1Copy(pObj) );
+ // create the POs
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Dar_ObjCreatePo( pMan, (Dar_Obj_t *)Abc_ObjChild0Copy(pObj) );
+ Dar_ManCleanup( pMan );
+ return pMan;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the network from the AIG manager into ABC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Ntk_t * pNtkNew;
+ Dar_Obj_t * pObj;
+ int i;
+ // perform strashing
+ pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+ // transfer the pointers to the basic nodes
+ Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
+ Dar_ManForEachPi( pMan, pObj, i )
+ pObj->pData = Abc_NtkCi(pNtkNew, i);
+ // rebuild the AIG
+ vNodes = Dar_ManDfs( pMan );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Dar_ObjChild0Copy(pObj), (Abc_Obj_t *)Dar_ObjChild1Copy(pObj) );
+ Vec_PtrFree( vNodes );
+ // connect the PO nodes
+ Dar_ManForEachPo( pMan, pObj, i )
+ Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Dar_ObjChild0Copy(pObj) );
+ if ( !Abc_NtkCheck( pNtkNew ) )
+ fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
+ return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcDsdRes.c b/src/base/abci/abcDsdRes.c
index 50c624d7..83e1c241 100644
--- a/src/base/abci/abcDsdRes.c
+++ b/src/base/abci/abcDsdRes.c
@@ -994,6 +994,73 @@ If_Obj_t * Abc_LutIfManMap_New_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit
/**Function*************************************************************
+ Synopsis [Find the best cofactoring variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+/*
+int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
+{
+ Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
+// Kit_DsdObj_t * pRoot;
+ unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) };
+ unsigned i, * pTruth;
+ int MaxBlock
+ Verbose = 0;
+ int RetValue = 0;
+
+ if ( fVerbose )
+ {
+ printf( "Function: " );
+// Extra_PrintBinary( stdout, pTruth, (1 << nVars) );
+ Extra_PrintHexadecimal( stdout, pTruth, nVars );
+ printf( "\n" );
+ Kit_DsdPrint( stdout, pNtk );
+ }
+ for ( i = 0; i < nVars; i++ )
+ {
+ Kit_TruthCofactor0New( pCofs2[0], pTruth, nVars, i );
+ pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars );
+ pNtk0 = Kit_DsdExpand( pTemp = pNtk0 );
+ Kit_DsdNtkFree( pTemp );
+
+ if ( fVerbose )
+ {
+ printf( "Cof%d0: ", i );
+ Kit_DsdPrint( stdout, pNtk0 );
+ }
+
+ Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i );
+ pNtk1 = Kit_DsdDecompose( pCofs2[1], nVars );
+ pNtk1 = Kit_DsdExpand( pTemp = pNtk1 );
+ Kit_DsdNtkFree( pTemp );
+
+ if ( fVerbose )
+ {
+ printf( "Cof%d1: ", i );
+ Kit_DsdPrint( stdout, pNtk1 );
+ }
+
+ if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
+ RetValue = 1;
+
+ Kit_DsdNtkFree( pNtk0 );
+ Kit_DsdNtkFree( pNtk1 );
+ }
+ if ( fVerbose )
+ printf( "\n" );
+
+ return RetValue;
+
+}
+*/
+/**Function*************************************************************
+
Synopsis [Prepares the mapping manager.]
Description []
@@ -1220,6 +1287,7 @@ clk = clock();
pTruth = Abc_LutCutTruth( p, pCut );
p->timeTruth += clock() - clk;
+
/*
// evaluate the result of decomposition
Result = Kit_DsdEval( pTruth, pCut->nLeaves, 3 );
@@ -1247,6 +1315,18 @@ p->timeEval += clock() - clk;
continue;
}
*/
+
+/*
+ if ( pCut->nLeaves > 6 && pCut->nLeaves < 12 && Kit_DsdNonDsdSizeMax(pDsdNtk) == pCut->nLeaves )
+ {
+// Abc_NtkPrintMeasures( pTruth, pCut->nLeaves );
+// Kit_DsdTestCofs( pDsdNtk, pTruth );
+
+// Abc_NtkPrintOneDecomp( pTruth, pCut->nLeaves );
+ Abc_NtkPrintOneDec( pTruth, pCut->nLeaves );
+ }
+*/
+
if ( p->pPars->fVeryVerbose )
{
// Extra_PrintHexadecimal( stdout, pTruth, pCut->nLeaves ); printf( "\n" );
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index d3779277..b878091b 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -525,6 +525,8 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
{
pParams->fUseRewriting = 0;
+ pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
+ Abc_NtkDelete( pNtkTemp );
Abc_NtkRewrite( pNtk, 0, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
diff --git a/src/base/abci/abcMeasure.c b/src/base/abci/abcMeasure.c
new file mode 100644
index 00000000..6604a0c4
--- /dev/null
+++ b/src/base/abci/abcMeasure.c
@@ -0,0 +1,478 @@
+/**CFile****************************************************************
+
+ FileName [abc_.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintMeasures( unsigned * pTruth, int nVars )
+{
+ unsigned uCofs[10][32];
+ int i, k, nOnes;
+
+ // total pairs
+ nOnes = Kit_TruthCountOnes( uCofs[0], nVars );
+ printf( "Total = %d.\n", nOnes * ((1 << nVars) - nOnes) );
+
+ // print measures for individual variables
+ for ( i = 0; i < nVars; i++ )
+ {
+ Kit_TruthUniqueNew( uCofs[0], pTruth, nVars, i );
+ nOnes = Kit_TruthCountOnes( uCofs[0], nVars );
+ printf( "%7d ", nOnes );
+ }
+ printf( "\n" );
+
+ // consider pairs
+ for ( i = 0; i < nVars; i++ )
+ for ( k = 0; k < nVars; k++ )
+ {
+ if ( i == k )
+ {
+ printf( " " );
+ continue;
+ }
+ Kit_TruthCofactor0New( uCofs[0], pTruth, nVars, i );
+ Kit_TruthCofactor1New( uCofs[1], pTruth, nVars, i );
+
+ Kit_TruthCofactor0New( uCofs[2], uCofs[0], nVars, k ); // 00
+ Kit_TruthCofactor1New( uCofs[3], uCofs[0], nVars, k ); // 01
+ Kit_TruthCofactor0New( uCofs[4], uCofs[1], nVars, k ); // 10
+ Kit_TruthCofactor1New( uCofs[5], uCofs[1], nVars, k ); // 11
+
+ Kit_TruthAndPhase( uCofs[6], uCofs[2], uCofs[5], nVars, 0, 1 ); // 00 & 11'
+ Kit_TruthAndPhase( uCofs[7], uCofs[2], uCofs[5], nVars, 1, 0 ); // 00' & 11
+ Kit_TruthAndPhase( uCofs[8], uCofs[3], uCofs[4], nVars, 0, 1 ); // 01 & 10'
+ Kit_TruthAndPhase( uCofs[9], uCofs[3], uCofs[4], nVars, 1, 0 ); // 01' & 10
+
+ nOnes = Kit_TruthCountOnes( uCofs[6], nVars ) +
+ Kit_TruthCountOnes( uCofs[7], nVars ) +
+ Kit_TruthCountOnes( uCofs[8], nVars ) +
+ Kit_TruthCountOnes( uCofs[9], nVars );
+
+ printf( "%7d ", nOnes );
+ if ( k == nVars - 1 )
+ printf( "\n" );
+ }
+ printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_Ntk4VarObjPrint_rec( Abc_Obj_t * pObj )
+{
+ if ( pObj == Abc_AigConst1(pObj->pNtk) )
+ {
+ printf( "1" );
+ return;
+ }
+ if ( Abc_ObjIsPi(pObj) )
+ {
+ printf( "%c", pObj->Id - 1 + 'a' );
+ return;
+ }
+
+ printf( "(" );
+ Abc_Ntk4VarObjPrint_rec( Abc_ObjFanin0(pObj) );
+ if ( Abc_ObjFaninC0(pObj) )
+ printf( "\'" );
+ Abc_Ntk4VarObjPrint_rec( Abc_ObjFanin1(pObj) );
+ if ( Abc_ObjFaninC1(pObj) )
+ printf( "\'" );
+ printf( ")" );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Abc_Ntk4VarObj( Vec_Ptr_t * vNodes )
+{
+ Abc_Obj_t * pObj;
+ unsigned uTruth0, uTruth1;
+ int i;
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ uTruth0 = (unsigned)(Abc_ObjFanin0(pObj)->pCopy);
+ uTruth1 = (unsigned)(Abc_ObjFanin1(pObj)->pCopy);
+ if ( Abc_ObjFaninC0(pObj) )
+ uTruth0 = ~uTruth0;
+ if ( Abc_ObjFaninC1(pObj) )
+ uTruth1 = ~uTruth1;
+ pObj->pCopy = (void *)(uTruth0 & uTruth1);
+ }
+ return uTruth0 & uTruth1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_Ntk4VarTable( Abc_Ntk_t * pNtk )
+{
+ static unsigned u4VarTruths[4] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00 };
+ static unsigned u4VarTts[222] = {
+ 0x0000, 0x0001, 0x0003, 0x0006, 0x0007, 0x000f, 0x0016, 0x0017, 0x0018, 0x0019,
+ 0x001b, 0x001e, 0x001f, 0x003c, 0x003d, 0x003f, 0x0069, 0x006b, 0x006f, 0x007e,
+ 0x007f, 0x00ff, 0x0116, 0x0117, 0x0118, 0x0119, 0x011a, 0x011b, 0x011e, 0x011f,
+ 0x012c, 0x012d, 0x012f, 0x013c, 0x013d, 0x013e, 0x013f, 0x0168, 0x0169, 0x016a,
+ 0x016b, 0x016e, 0x016f, 0x017e, 0x017f, 0x0180, 0x0181, 0x0182, 0x0183, 0x0186,
+ 0x0187, 0x0189, 0x018b, 0x018f, 0x0196, 0x0197, 0x0198, 0x0199, 0x019a, 0x019b,
+ 0x019e, 0x019f, 0x01a8, 0x01a9, 0x01aa, 0x01ab, 0x01ac, 0x01ad, 0x01ae, 0x01af,
+ 0x01bc, 0x01bd, 0x01be, 0x01bf, 0x01e8, 0x01e9, 0x01ea, 0x01eb, 0x01ee, 0x01ef,
+ 0x01fe, 0x033c, 0x033d, 0x033f, 0x0356, 0x0357, 0x0358, 0x0359, 0x035a, 0x035b,
+ 0x035e, 0x035f, 0x0368, 0x0369, 0x036a, 0x036b, 0x036c, 0x036d, 0x036e, 0x036f,
+ 0x037c, 0x037d, 0x037e, 0x03c0, 0x03c1, 0x03c3, 0x03c5, 0x03c6, 0x03c7, 0x03cf,
+ 0x03d4, 0x03d5, 0x03d6, 0x03d7, 0x03d8, 0x03d9, 0x03db, 0x03dc, 0x03dd, 0x03de,
+ 0x03fc, 0x0660, 0x0661, 0x0662, 0x0663, 0x0666, 0x0667, 0x0669, 0x066b, 0x066f,
+ 0x0672, 0x0673, 0x0676, 0x0678, 0x0679, 0x067a, 0x067b, 0x067e, 0x0690, 0x0691,
+ 0x0693, 0x0696, 0x0697, 0x069f, 0x06b0, 0x06b1, 0x06b2, 0x06b3, 0x06b4, 0x06b5,
+ 0x06b6, 0x06b7, 0x06b9, 0x06bd, 0x06f0, 0x06f1, 0x06f2, 0x06f6, 0x06f9, 0x0776,
+ 0x0778, 0x0779, 0x077a, 0x077e, 0x07b0, 0x07b1, 0x07b4, 0x07b5, 0x07b6, 0x07bc,
+ 0x07e0, 0x07e1, 0x07e2, 0x07e3, 0x07e6, 0x07e9, 0x07f0, 0x07f1, 0x07f2, 0x07f8,
+ 0x0ff0, 0x1668, 0x1669, 0x166a, 0x166b, 0x166e, 0x167e, 0x1681, 0x1683, 0x1686,
+ 0x1687, 0x1689, 0x168b, 0x168e, 0x1696, 0x1697, 0x1698, 0x1699, 0x169a, 0x169b,
+ 0x169e, 0x16a9, 0x16ac, 0x16ad, 0x16bc, 0x16e9, 0x177e, 0x178e, 0x1796, 0x1798,
+ 0x179a, 0x17ac, 0x17e8, 0x18e7, 0x19e1, 0x19e3, 0x19e6, 0x1bd8, 0x1be4, 0x1ee1,
+ 0x3cc3, 0x6996
+ };
+ int Counters[222] = {0};
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pObj;
+ unsigned uTruth;
+ int i, k, Count = 0;
+
+ unsigned short * puCanons = NULL;
+ unsigned char * puMap = NULL;
+ Extra_Truth4VarNPN( &puCanons, NULL, NULL, &puMap );
+
+ // set elementary truth tables
+ assert( Abc_NtkPiNum(pNtk) == 4 );
+ Abc_AigConst1(pNtk)->pCopy = (void *)0xFFFFFFFF;
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ pObj->pCopy = (void *)u4VarTruths[i];
+
+ // create truth tables
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ {
+ vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+ if ( Vec_PtrSize(vNodes) == 0 )
+ uTruth = (unsigned)Abc_ObjFanin0(pObj)->pCopy;
+ else
+ uTruth = Abc_Ntk4VarObj( vNodes );
+
+ if ( (uTruth & 0xFFFF) < (~uTruth & 0xFFFF) )
+ uTruth = uTruth & 0xFFFF;
+ else
+ uTruth = ~uTruth & 0xFFFF;
+
+ for ( k = 0; k < 222; k++ )
+ if ( u4VarTts[k] == uTruth )
+ break;
+ if ( k == 222 )
+ continue;
+/*
+// if ( uTruth == 1725 )
+ if ( k == 96 )
+ {
+ printf( "%d : ", Vec_PtrSize(vNodes) );
+ Abc_Ntk4VarObjPrint_rec( Abc_ObjFanin0(pObj) );
+ printf( "\n" );
+ }
+*/
+ Counters[k]++;
+
+// Counters[ puMap[uTruth & 0xFFFF] ]++;
+ Vec_PtrFree( vNodes );
+ }
+ free( puCanons );
+ free( puMap );
+
+ Count = 0;
+ for ( k = 0; k < 222; k++ )
+ {
+ printf( "%d/%x/%d ", k, u4VarTts[k], Counters[k] );
+ Count += Counters[k];
+ }
+ printf( " Total = %d\n", Count );
+}
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if there are no more than 2 unique cofactors.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkPrintOneDecompCheckCofList( unsigned * uCofs, int nCofs )
+{
+ int i, Ind = -1;
+ assert( nCofs > 2 );
+ for ( i = 1; i < nCofs; i++ )
+ {
+ if ( uCofs[i] == uCofs[0] )
+ continue;
+ if ( Ind == -1 )
+ {
+ Ind = i;
+ continue;
+ }
+ if ( uCofs[i] == uCofs[Ind] )
+ continue;
+ return 0;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks all cofactors with the given mask.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkPrintOneDecompCheck( unsigned * uCofs, int nCofs, unsigned uMask )
+{
+ unsigned pCofs[32][32];
+ int nCofNums[32] = {0};
+ int uMasks[32];
+ int nGroups = 0;
+ int i, k;
+ for ( i = 0; i < nCofs; i++ )
+ {
+ // find group of this cof
+ for ( k = 0; k < nGroups; k++ )
+ if ( (int)(i & uMask) == uMasks[k] )
+ break;
+ if ( k == nGroups )
+ {
+ uMasks[k] = (i & uMask);
+ nGroups++;
+ }
+ // save cof in the group
+ pCofs[k][ nCofNums[k]++ ] = uCofs[i];
+ assert( nCofNums[k] <= 32 );
+ assert( nGroups <= 32 );
+ }
+ // check the groups
+ for ( i = 0; i < nGroups; i++ )
+ if ( !Abc_NtkPrintOneDecompCheckCofList(pCofs[i], nCofNums[i]) )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintOneDecomp_rec( unsigned * uCofs, int nCofs, int nVars, unsigned uMask, int * pBestSize, unsigned * puBestMask )
+{
+ unsigned uMaskNew;
+ int v, last, Counter = 0;
+ // find the last variable in the mask
+ for ( v = 0; v < nVars; v++ )
+ if ( uMask & (1<<v) )
+ {
+ last = v;
+ Counter++;
+ }
+ if ( Counter > 3 )
+ return;
+ // try adding one variable after the last
+ for ( v = last + 1; v < nVars; v++ )
+ {
+ uMaskNew = uMask | (1 << v);
+ if ( !Abc_NtkPrintOneDecompCheck( uCofs, nCofs, uMaskNew ) )
+ continue;
+ if ( *pBestSize < Counter + 1 )
+ {
+ *pBestSize = Counter + 1;
+ *puBestMask = uMaskNew;
+ }
+ // try other masks
+ Abc_NtkPrintOneDecomp_rec( uCofs, nCofs, nVars, uMaskNew, pBestSize, puBestMask );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintOneDecomp( unsigned * pTruth, int nVars )
+{
+ int BoundSet = 6;
+ unsigned uCofs[64], uMask, uBestMask = 0;
+ int i, nCofs, nMints, nMintShift, BestSize = 1;
+
+ assert( nVars > BoundSet );
+ assert( nVars <= BoundSet + 5 ); // at most 5 variable cofactors
+
+ // collect the cofactors
+ nCofs = (1 << BoundSet);
+ nMints = (1 << (nVars-BoundSet));
+ nMintShift = 0;
+ uMask = Kit_CubeMask( nMints );
+ for ( i = 0; i < nCofs; i++ )
+ {
+ uCofs[i] = (pTruth[nMintShift/32] >> (nMintShift % 32)) & uMask;
+ nMintShift += nMints;
+ }
+
+ // try removing variables
+ for ( i = 0; i < BoundSet; i++ )
+ Abc_NtkPrintOneDecomp_rec( uCofs, nCofs, nVars, (1 << i), &BestSize, &uBestMask );
+
+ printf( "Best size = %d ", BestSize );
+ printf( "Best mask = " );
+ Extra_PrintBinary( stdout, &uBestMask, nVars );
+ printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintOneDec( unsigned * pTruth, int nVars )
+{
+ unsigned uCof[(1<<11)], * pOut = uCof, * pIn = pTruth, * pTemp;
+ int nDiffs[16];
+ int Order[16];
+ int i, fChange, Temp, Counter;
+
+ // find the ordering
+ for ( i = 0; i < nVars; i++ )
+ {
+ Kit_TruthUniqueNew( uCof, pTruth, nVars, i );
+ nDiffs[i] = Kit_TruthCountOnes( uCof, nVars );
+ Order[i] = i;
+ }
+
+ // permute truth table to least active variable first
+ Counter = 0;
+ do {
+ fChange = 0;
+ for ( i = 0; i < nVars-1; i++ )
+ {
+ if ( nDiffs[i] <= nDiffs[i+1] )
+ continue;
+ fChange = 1;
+ Counter++;
+
+ Temp = nDiffs[i];
+ nDiffs[i] = nDiffs[i+1];
+ nDiffs[i+1] = Temp;
+
+ Temp = Order[i];
+ Order[i] = Order[i+1];
+ Order[i+1] = Temp;
+
+ Extra_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
+ pTemp = pIn; pIn = pOut; pOut = pTemp;
+ }
+ } while ( fChange );
+
+ // swap if it was moved an even number of times
+ if ( Counter & 1 )
+ Extra_TruthCopy( pOut, pIn, nVars );
+
+ // call the decomposition
+ Abc_NtkPrintOneDecomp( pTruth, nVars );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 14e33c36..748868de 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -74,9 +74,9 @@ Vec_Ptr_t * Abc_NtkPartitionCollectSupps( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Int_t * vOne )
+int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vPartsAll, int nPartSizeLimit, Vec_Int_t * vOne )
{
- Vec_Int_t * vPartSupp;
+ Vec_Int_t * vPartSupp, * vPart;
double Attract, Repulse, Cost, CostBest;
int i, nCommon, iBest;
iBest = -1;
@@ -84,6 +84,11 @@ int Abc_NtkPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Int_t * vOne )
Vec_PtrForEachEntry( vPartSuppsAll, vPartSupp, i )
{
nCommon = Vec_IntTwoCountCommon( vPartSupp, vOne );
+ if ( nCommon == 0 )
+ continue;
+ vPart = Vec_PtrEntry( vPartsAll, i );
+ if ( nPartSizeLimit > 0 && Vec_IntSize(vPart) > nPartSizeLimit )
+ continue;
if ( nCommon == Vec_IntSize(vOne) )
return i;
Attract = 1.0 * nCommon / Vec_IntSize(vOne);
@@ -143,17 +148,20 @@ void Abc_NtkPartitionPrint( Abc_Ntk_t * pNtk, Vec_Ptr_t * vPartsAll, Vec_Ptr_t *
SeeAlso []
***********************************************************************/
-void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
+void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll, int nPartSizeLimit )
{
Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
int i, iPart;
+ if ( nPartSizeLimit == 0 )
+ nPartSizeLimit = 200;
+
// pack smaller partitions into larger blocks
iPart = 0;
vPart = vPartSupp = NULL;
Vec_PtrForEachEntry( vPartSuppsAll, vOne, i )
{
- if ( Vec_IntSize(vOne) < 200 )
+ if ( Vec_IntSize(vOne) < nPartSizeLimit )
{
if ( vPartSupp == NULL )
{
@@ -169,7 +177,7 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
Vec_IntFree( vTemp );
Vec_IntFree( Vec_PtrEntry(vPartsAll, i) );
}
- if ( Vec_IntSize(vPartSupp) < 200 )
+ if ( Vec_IntSize(vPartSupp) < nPartSizeLimit )
continue;
}
else
@@ -212,7 +220,7 @@ void Abc_NtkPartitionCompact( Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vPartSuppsAll )
SeeAlso []
***********************************************************************/
-Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int fVerbose )
+Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose )
{
Vec_Ptr_t * vSupps, * vPartsAll, * vPartsAll2, * vPartSuppsAll, * vPartPtr;
Vec_Int_t * vOne, * vPart, * vPartSupp, * vTemp;
@@ -235,7 +243,7 @@ clk = clock();
// get the output number
iOut = Vec_IntPop(vOne);
// find closely matching part
- iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vOne );
+ iPart = Abc_NtkPartitionSmartFindPart( vPartSuppsAll, vPartsAll, nPartSizeLimit, vOne );
if ( iPart == -1 )
{
// create new partition
@@ -280,7 +288,7 @@ clk = clock();
// compact small partitions
// Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
- Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll );
+ Abc_NtkPartitionCompact( vPartsAll, vPartSuppsAll, nPartSizeLimit );
if ( fVerbose )
Abc_NtkPartitionPrint( pNtk, vPartsAll, vPartSuppsAll );
if ( fVerbose )
@@ -668,7 +676,7 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams )
// perform partitioning
assert( Abc_NtkIsStrash(pNtk) );
// vParts = Abc_NtkPartitionNaive( pNtk, 20 );
- vParts = Abc_NtkPartitionSmart( pNtk, 0 );
+ vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 );
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 43ddb4fd..c4ec68f3 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -26,7 +26,7 @@
////////////////////////////////////////////////////////////////////////
static void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
-static stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose );
+static stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose, int fVeryVerbose );
static void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose );
static void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
static void Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
@@ -54,7 +54,7 @@ static void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pF
SeeAlso []
***********************************************************************/
-bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
+bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose )
{
Fraig_Params_t Params;
Abc_Ntk_t * pNtkAig;
@@ -100,9 +100,11 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
else
Abc_NtkFraigSweepUsingExdc( pMan, pNtk );
}
+ // assign levels to the nodes of the network
+ Abc_NtkLevel( pNtk );
// collect the classes of equivalent nets
- tEquiv = Abc_NtkFraigEquiv( pNtk, fUseInv, fVerbose );
+ tEquiv = Abc_NtkFraigEquiv( pNtk, fUseInv, fVerbose, fVeryVerbose );
// transform the network into the equivalent one
Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose );
@@ -113,7 +115,11 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
Abc_NtkDelete( pNtkAig );
// cleanup the dangling nodes
- Abc_NtkCleanup( pNtk, fVerbose );
+ if ( Abc_NtkHasMapping(pNtk) )
+ Abc_NtkCleanup( pNtk, fVerbose );
+ else
+ Abc_NtkSweep( pNtk, fVerbose );
+
// check
if ( !Abc_NtkCheck( pNtk ) )
{
@@ -175,7 +181,7 @@ void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
+stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose, int fVeryVerbose )
{
Abc_Obj_t * pList, * pNode, * pNodeAig;
Fraig_Node_t * gNode;
@@ -225,22 +231,22 @@ stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
// count nodes in the non-trival classes
for ( pNode = pList; pNode; pNode = pNode->pNext )
Counter++;
-/*
- if ( fVerbose )
+
+ if ( fVeryVerbose )
{
printf( "Class %2d : {", c );
for ( pNode = pList; pNode; pNode = pNode->pNext )
{
pNode->pCopy = NULL;
printf( " %s", Abc_ObjName(pNode) );
- if ( pNode->fPhase ) printf( "(*)" );
+ printf( "(%c)", pNode->fPhase? '-' : '+' );
+ printf( "(%d)", pNode->Level );
}
printf( " }\n" );
c++;
}
-*/
}
- if ( fVerbose )
+ if ( fVerbose || fVeryVerbose )
{
printf( "Sweeping stats for network \"%s\":\n", pNtk->pName );
printf( "Internal nodes = %d. Different functions (up to compl) = %d.\n", Abc_NtkNodeNum(pNtk), stmm_count(tStrash2Net) );
@@ -268,8 +274,6 @@ void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv,
Abc_Obj_t * pList;
if ( stmm_count(tEquiv) == 0 )
return;
- // assign levels to the nodes of the network
- Abc_NtkLevel( pNtk );
// merge nodes in the classes
if ( Abc_NtkHasMapping( pNtk ) )
{
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index d4b15d59..a4c67a8b 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -313,6 +313,123 @@ void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, in
/**Function*************************************************************
+ Synopsis [Verifies sequential equivalence by fraiging followed by SAT.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
+{
+ extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
+ extern Vec_Vec_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose );
+ extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
+ extern void * Abc_FrameGetGlobalFrame();
+
+ Vec_Vec_t * vParts;
+ Vec_Ptr_t * vOne;
+ Prove_Params_t Params, * pParams = &Params;
+ Abc_Ntk_t * pMiter, * pMiterPart;
+ int i, RetValue, Status, nOutputs;
+
+ // solve the CNF using the SAT solver
+ Prove_ParamsSetDefault( pParams );
+ pParams->nItersMax = 5;
+ // pParams->fVerbose = 1;
+
+ // get the miter of the two networks
+ pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1 );
+ if ( pMiter == NULL )
+ {
+ printf( "Miter computation has failed.\n" );
+ return;
+ }
+ RetValue = Abc_NtkMiterIsConstant( pMiter );
+ if ( RetValue == 0 )
+ {
+ printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
+ // report the error
+ pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
+ Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
+ FREE( pMiter->pModel );
+ Abc_NtkDelete( pMiter );
+ return;
+ }
+ if ( RetValue == 1 )
+ {
+ printf( "Networks are equivalent after structural hashing.\n" );
+ Abc_NtkDelete( pMiter );
+ return;
+ }
+
+ Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
+
+ // partition the outputs
+ vParts = Abc_NtkPartitionSmart( pMiter, 50, 0 );
+
+ // fraig each partition
+ Status = 1;
+ nOutputs = 0;
+ Vec_VecForEachLevel( vParts, vOne, i )
+ {
+ // get this part of the miter
+ pMiterPart = Abc_NtkCreateConeArray( pMiter, vOne, 0 );
+ Abc_NtkCombinePos( pMiterPart, 0 );
+ // check the miter for being constant
+ RetValue = Abc_NtkMiterIsConstant( pMiterPart );
+ if ( RetValue == 0 )
+ {
+ printf( "Networks are NOT EQUIVALENT after partitioning.\n" );
+ Abc_NtkDelete( pMiterPart );
+ break;
+ }
+ if ( RetValue == 1 )
+ {
+ Abc_NtkDelete( pMiterPart );
+ continue;
+ }
+ // solve the problem
+ RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
+ if ( RetValue == -1 )
+ {
+ printf( "Networks are undecided (resource limits is reached).\r" );
+ Status = -1;
+ }
+ else if ( RetValue == 0 )
+ {
+ int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiterPart, pMiterPart->pModel );
+ if ( pSimInfo[0] != 1 )
+ printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
+ else
+ printf( "Networks are NOT EQUIVALENT. \n" );
+ free( pSimInfo );
+ Status = 0;
+ Abc_NtkDelete( pMiterPart );
+ break;
+ }
+ else
+ {
+ printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) );
+ nOutputs += Vec_PtrSize(vOne);
+ }
+ Abc_NtkDelete( pMiterPart );
+ }
+ Vec_VecFree( vParts );
+
+ Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
+
+ if ( Status == 1 )
+ printf( "Networks are equivalent. \n" );
+ else if ( Status == -1 )
+ printf( "Timed out after verifying %d outputs (out of %d).\n", nOutputs, Abc_NtkCoNum(pNtk1) );
+ Abc_NtkDelete( pMiter );
+}
+
+/**Function*************************************************************
+
Synopsis [Verifies sequential equivalence by brute-force SAT.]
Description []
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 5d5bccb8..9bc51dbe 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -7,6 +7,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcClpBdd.c \
src/base/abci/abcClpSop.c \
src/base/abci/abcCut.c \
+ src/base/abci/abcDar.c \
src/base/abci/abcDebug.c \
src/base/abci/abcDress.c \
src/base/abci/abcDsd.c \
diff --git a/src/base/abci/xaaaa.c b/src/base/abci/xaaaa.c
new file mode 100644
index 00000000..ea39ad02
--- /dev/null
+++ b/src/base/abci/xaaaa.c
@@ -0,0 +1,155 @@
+/**CFile****************************************************************
+
+ FileName [abc_.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintMeasures( unsigned * pTruth, int nVars )
+{
+ unsigned uCofs[10][32];
+ int i, k, nOnes;
+
+ // total pairs
+ nOnes = Kit_TruthCountOnes( uCofs[0], nVars );
+ printf( "Total = %d.\n", nOnes * ((1 << nVars) - nOnes) );
+
+ // print measures for individual variables
+ for ( i = 0; i < nVars; i++ )
+ {
+ Kit_TruthUniqueNew( uCofs[0], pTruth, nVars, i );
+ nOnes = Kit_TruthCountOnes( uCofs[0], nVars );
+ printf( "%7d ", nOnes );
+ }
+ printf( "\n" );
+
+ // consider pairs
+ for ( i = 0; i < nVars; i++ )
+ for ( k = 0; k < nVars; k++ )
+ {
+ if ( i == k )
+ {
+ printf( " " );
+ continue;
+ }
+ Kit_TruthCofactor0New( uCofs[0], pTruth, nVars, i );
+ Kit_TruthCofactor1New( uCofs[1], pTruth, nVars, i );
+
+ Kit_TruthCofactor0New( uCofs[2], uCofs[0], nVars, k ); // 00
+ Kit_TruthCofactor1New( uCofs[3], uCofs[0], nVars, k ); // 01
+ Kit_TruthCofactor0New( uCofs[4], uCofs[1], nVars, k ); // 10
+ Kit_TruthCofactor1New( uCofs[5], uCofs[1], nVars, k ); // 11
+
+ Kit_TruthAndPhase( uCofs[6], uCofs[2], uCofs[5], nVars, 0, 1 ); // 00 & 11'
+ Kit_TruthAndPhase( uCofs[7], uCofs[2], uCofs[5], nVars, 1, 0 ); // 00' & 11
+ Kit_TruthAndPhase( uCofs[8], uCofs[3], uCofs[4], nVars, 0, 1 ); // 01 & 10'
+ Kit_TruthAndPhase( uCofs[9], uCofs[3], uCofs[4], nVars, 1, 0 ); // 01' & 10
+
+ nOnes = Kit_TruthCountOnes( uCofs[6], nVars ) +
+ Kit_TruthCountOnes( uCofs[7], nVars ) +
+ Kit_TruthCountOnes( uCofs[8], nVars ) +
+ Kit_TruthCountOnes( uCofs[9], nVars );
+
+ printf( "%7d ", nOnes );
+ if ( k == nVars - 1 )
+ printf( "\n" );
+ }
+ printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_Ntk4VarTable( Abc_Ntk_t * pNtk )
+{
+ static u4VarTts[222] = {
+ 0x0000, 0x0001, 0x0003, 0x0006, 0x0007, 0x000f, 0x0016, 0x0017, 0x0018, 0x0019,
+ 0x001b, 0x001e, 0x001f, 0x003c, 0x003d, 0x003f, 0x0069, 0x006b, 0x006f, 0x007e,
+ 0x007f, 0x00ff, 0x0116, 0x0117, 0x0118, 0x0119, 0x011a, 0x011b, 0x011e, 0x011f,
+ 0x012c, 0x012d, 0x012f, 0x013c, 0x013d, 0x013e, 0x013f, 0x0168, 0x0169, 0x016a,
+ 0x016b, 0x016e, 0x016f, 0x017e, 0x017f, 0x0180, 0x0181, 0x0182, 0x0183, 0x0186,
+ 0x0187, 0x0189, 0x018b, 0x018f, 0x0196, 0x0197, 0x0198, 0x0199, 0x019a, 0x019b,
+ 0x019e, 0x019f, 0x01a8, 0x01a9, 0x01aa, 0x01ab, 0x01ac, 0x01ad, 0x01ae, 0x01af,
+ 0x01bc, 0x01bd, 0x01be, 0x01bf, 0x01e8, 0x01e9, 0x01ea, 0x01eb, 0x01ee, 0x01ef,
+ 0x01fe, 0x033c, 0x033d, 0x033f, 0x0356, 0x0357, 0x0358, 0x0359, 0x035a, 0x035b,
+ 0x035e, 0x035f, 0x0368, 0x0369, 0x036a, 0x036b, 0x036c, 0x036d, 0x036e, 0x036f,
+ 0x037c, 0x037d, 0x037e, 0x03c0, 0x03c1, 0x03c3, 0x03c5, 0x03c6, 0x03c7, 0x03cf,
+ 0x03d4, 0x03d5, 0x03d6, 0x03d7, 0x03d8, 0x03d9, 0x03db, 0x03dc, 0x03dd, 0x03de,
+ 0x03fc, 0x0660, 0x0661, 0x0662, 0x0663, 0x0666, 0x0667, 0x0669, 0x066b, 0x066f,
+ 0x0672, 0x0673, 0x0676, 0x0678, 0x0679, 0x067a, 0x067b, 0x067e, 0x0690, 0x0691,
+ 0x0693, 0x0696, 0x0697, 0x069f, 0x06b0, 0x06b1, 0x06b2, 0x06b3, 0x06b4, 0x06b5,
+ 0x06b6, 0x06b7, 0x06b9, 0x06bd, 0x06f0, 0x06f1, 0x06f2, 0x06f6, 0x06f9, 0x0776,
+ 0x0778, 0x0779, 0x077a, 0x077e, 0x07b0, 0x07b1, 0x07b4, 0x07b5, 0x07b6, 0x07bc,
+ 0x07e0, 0x07e1, 0x07e2, 0x07e3, 0x07e6, 0x07e9, 0x07f0, 0x07f1, 0x07f2, 0x07f8,
+ 0x0ff0, 0x1668, 0x1669, 0x166a, 0x166b, 0x166e, 0x167e, 0x1681, 0x1683, 0x1686,
+ 0x1687, 0x1689, 0x168b, 0x168e, 0x1696, 0x1697, 0x1698, 0x1699, 0x169a, 0x169b,
+ 0x169e, 0x16a9, 0x16ac, 0x16ad, 0x16bc, 0x16e9, 0x177e, 0x178e, 0x1796, 0x1798,
+ 0x179a, 0x17ac, 0x17e8, 0x18e7, 0x19e1, 0x19e3, 0x19e6, 0x1bd8, 0x1be4, 0x1ee1,
+ 0x3cc3, 0x6996
+ };
+ int Counters[222];
+
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pObj;
+ int i;
+
+ // set elementary truth tables
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ pObj
+
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ {
+ vNodes = Abc_NtkDfsNodes( pNtk, &pObj, i );
+ Vec_PtrFree( vNodes );
+ }
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 48738903..a54a00fe 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -25,7 +25,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static unsigned Io_ReadAigerDecode( char ** ppPos );
+unsigned Io_ReadAigerDecode( char ** ppPos );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index a1ff4456..7c9da184 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -129,7 +129,7 @@ static unsigned Io_ObjMakeLit( int Var, int fCompl ) { return (V
static unsigned Io_ObjAigerNum( Abc_Obj_t * pObj ) { return (unsigned)pObj->pCopy; }
static void Io_ObjSetAigerNum( Abc_Obj_t * pObj, unsigned Num ) { pObj->pCopy = (void *)Num; }
-static int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
+int Io_WriteAigerEncode( char * pBuffer, int Pos, unsigned x );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index bf5182fb..a02d53fd 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -213,17 +213,33 @@ void Io_WriteVerilogPis( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
***********************************************************************/
void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
{
- Abc_Obj_t * pTerm, * pNet;
+ Abc_Obj_t * pTerm, * pNet, * pSkip;
int LineLength;
int AddedLength;
int NameCounter;
int i;
+ int nskip;
+
+ pSkip = 0;
+ nskip = 0;
LineLength = Start;
NameCounter = 0;
Abc_NtkForEachPo( pNtk, pTerm, i )
{
pNet = Abc_ObjFanin0(pTerm);
+
+ if ( Abc_ObjIsPi(Abc_ObjFanin0(pNet)) )
+ {
+ // Skip this output since it is a feedthrough -- the same
+ // name will appear as an input and an output which other
+ // tools reading verilog do not like.
+
+ nskip++;
+ pSkip = pNet; // save an example of skipped net
+ continue;
+ }
+
// get the line length after this name is written
AddedLength = strlen(Io_WriteVerilogGetName(Abc_ObjName(pNet))) + 2;
if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
@@ -237,6 +253,14 @@ void Io_WriteVerilogPos( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
LineLength += AddedLength;
NameCounter++;
}
+
+ if (nskip != 0)
+ {
+ assert (pSkip);
+ printf( "Io_WriteVerilogPos(): Omitted %d feedthrough nets from output list of module (e.g. %s).\n", nskip, Abc_ObjName(pSkip) );
+ return;
+ }
+
}
/**Function*************************************************************
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index 13c71759..8c316970 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -18,8 +18,8 @@
***********************************************************************/
-#ifndef __Abc_INT_H__
-#define __Abc_INT_H__
+#ifndef __MAIN_INT_H__
+#define __MAIN_INT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-31 11:18:53 +0000