summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h1
-rw-r--r--src/base/abci/abc.c130
-rw-r--r--src/base/abci/abcEco.c58
-rw-r--r--src/base/abci/abcMap.c16
-rw-r--r--src/base/abci/abcPrint.c79
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/base/cmd/cmdHist.c8
-rw-r--r--src/base/main/abcapis.h105
-rw-r--r--src/base/main/abcapis_old.h84
-rw-r--r--src/base/main/main.h8
-rw-r--r--src/base/main/mainFrame.c2
-rw-r--r--src/base/wlc/wlcStdin.c2
12 files changed, 471 insertions, 23 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 6c0d96d1..fad0b804 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -825,6 +825,7 @@ extern ABC_DLL void Abc_NtkDontCareFree( Odc_Man_t * p );
extern ABC_DLL int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth );
/*=== abcPrint.c ==========================================================*/
extern ABC_DLL float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk );
+extern ABC_DLL float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose );
extern ABC_DLL void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch, int fSkipBuf, int fSkipSmall, int fPrintMem );
extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintFlops );
extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2efa041c..7fc45f48 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -122,6 +122,7 @@ static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandMfs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfs3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandGlitch ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPowerdown ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAddBuffs ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -316,6 +317,7 @@ static int Abc_CommandPSat ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEco ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmc3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -772,6 +774,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "mfs2", Abc_CommandMfs2, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs3", Abc_CommandMfs3, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "trace", Abc_CommandTrace, 0 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "glitch", Abc_CommandGlitch, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "powerdown", Abc_CommandPowerdown, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "addbuffs", Abc_CommandAddBuffs, 1 );
@@ -966,6 +969,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "eco", Abc_CommandEco, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc", Abc_CommandBmc, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc2", Abc_CommandBmc2, 0 );
Cmd_CommandAdd( pAbc, "Verification", "bmc3", Abc_CommandBmc3, 1 );
@@ -5718,6 +5722,88 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandGlitch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+ int nPats = 4000;
+ int Prob = 8;
+ int fVerbose = 1;
+ int c;
+
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NPvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nPats = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nPats < 1 )
+ goto usage;
+ break;
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Prob = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Prob < 1 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( -1, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ Abc_Print( -1, "This command can only be applied to a mapped logic network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsMappedLogic(pNtk) || Abc_NtkGetFaninMax(pNtk) <= 6 )
+ Abc_Print( 1, "Glitching adds %7.2f %% of signal transitions, compared to switching.\n", Abc_NtkMfsTotalGlitching(pNtk, nPats, Prob, fVerbose) );
+ else
+ printf( "Currently computes glitching only for K-LUT networks with K <= 6.\n" );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: glitch [-NP <num>] [-vh]\n" );
+ Abc_Print( -2, "\t comparing glitching activity to switching activity\n" );
+ Abc_Print( -2, "\t-N <num> : the number of random patterns to use (0 < num < 1000000) [default = %d]\n", nPats );
+ Abc_Print( -2, "\t-P <num> : once in how many cycles an input changes its value [default = %d]\n", Prob );
+ Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandSpeedup( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk, * pNtkRes;
@@ -23865,6 +23951,50 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandEco( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Abc_NtkEco( char * pFileNames[3] );
+ char * pFileNames[3] = {NULL}; int c;
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( globalUtilOptind + 3 != argc )
+ {
+ Abc_Print( -1, "Expecting three file names on the command line.\n" );
+ return 1;
+ }
+ for ( c = 0; c < 3; c++ )
+ pFileNames[c] = argv[globalUtilOptind+c];
+ Abc_NtkEco( pFileNames );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: eco [-h]\n" );
+ Abc_Print( -2, "\t performs experimental ECO computation\n" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
diff --git a/src/base/abci/abcEco.c b/src/base/abci/abcEco.c
new file mode 100644
index 00000000..70a76729
--- /dev/null
+++ b/src/base/abci/abcEco.c
@@ -0,0 +1,58 @@
+/**CFile****************************************************************
+
+ FileName [abcEco.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Experimental procedures.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcEco.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "base/main/main.h"
+#include "map/mio/mio.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkEco( char * pFileNames[3] )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 4e588e2d..f758d0f0 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -923,9 +923,9 @@ void Abc_NtkPrintMiniMapping( int * pArray )
SeeAlso []
***********************************************************************/
-int * Abc_NtkOutputMiniMapping( void * pAbc0 )
+int * Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc )
{
- Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+ //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
Abc_Ntk_t * pNtk;
Vec_Int_t * vMapping;
int * pArray;
@@ -977,9 +977,9 @@ void Abc_NtkTestMiniMapping( Abc_Ntk_t * p )
SeeAlso []
***********************************************************************/
-void Abc_NtkSetCiArrivalTime( void * pAbc0, int iCi, float Rise, float Fall )
+void Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall )
{
- Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+ //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
if ( pAbc == NULL )
@@ -1001,9 +1001,9 @@ void Abc_NtkSetCiArrivalTime( void * pAbc0, int iCi, float Rise, float Fall )
pNode = Abc_NtkCi( pNtk, iCi );
Abc_NtkTimeSetArrival( pNtk, Abc_ObjId(pNode), Rise, Fall );
}
-void Abc_NtkSetCoRequiredTime( void * pAbc0, int iCo, float Rise, float Fall )
+void Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall )
{
- Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+ //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
if ( pAbc == NULL )\
@@ -1037,9 +1037,9 @@ void Abc_NtkSetCoRequiredTime( void * pAbc0, int iCo, float Rise, float Fall )
SeeAlso []
***********************************************************************/
-void Abc_NtkSetAndGateDelay( void * pAbc0, float Delay )
+void Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay )
{
- Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+ //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
Abc_Ntk_t * pNtk;
if ( pAbc == NULL )
{
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 2129782f..ea91619c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -351,9 +351,8 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
Abc_Print( 1," power =%7.2f", Abc_NtkMfsTotalSwitching(pNtk) );
if ( fGlitch )
{
- extern float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk );
if ( Abc_NtkIsLogic(pNtk) && Abc_NtkGetFaninMax(pNtk) <= 6 )
- Abc_Print( 1," glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk) );
+ Abc_Print( 1," glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk, 4000, 8, 0) );
else
printf( "\nCurrently computes glitching only for K-LUT networks with K <= 6." );
}
@@ -1744,7 +1743,7 @@ extern Gli_Man_t * Gli_ManAlloc( int nObjs, int nRegs, int nFanioPairs );
extern void Gli_ManStop( Gli_Man_t * p );
extern int Gli_ManCreateCi( Gli_Man_t * p, int nFanouts );
extern int Gli_ManCreateCo( Gli_Man_t * p, int iFanin );
-extern int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, unsigned * puTruth );
+extern int Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, word * pGateTruth );
extern void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose );
extern int Gli_ObjNumSwitches( Gli_Man_t * p, int iNode );
@@ -1761,13 +1760,14 @@ extern int Gli_ObjNumGlitches( Gli_Man_t * p, int iNode );
SeeAlso []
***********************************************************************/
-float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
+float Abc_NtkMfsTotalGlitchingLut( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose )
{
int nSwitches, nGlitches;
Gli_Man_t * p;
Vec_Ptr_t * vNodes;
Vec_Int_t * vFanins, * vTruth;
Abc_Obj_t * pObj, * pFanin;
+ Vec_Wrd_t * vTruths; word * pTruth;
unsigned * puTruth;
int i, k;
assert( Abc_NtkIsLogic(pNtk) );
@@ -1781,6 +1781,7 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
vNodes = Abc_NtkDfs( pNtk, 0 );
vFanins = Vec_IntAlloc( 6 );
vTruth = Vec_IntAlloc( 1 << 12 );
+ vTruths = Vec_WrdStart( Abc_NtkObjNumMax(pNtk) );
// derive network for glitch computation
p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk),
@@ -1795,7 +1796,9 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
Abc_ObjForEachFanin( pObj, pFanin, k )
Vec_IntPush( vFanins, pFanin->iTemp );
puTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNtk->pManFunc, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj), vTruth, 0 );
- pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), puTruth );
+ pTruth = Vec_WrdEntryP( vTruths, Abc_ObjId(pObj) );
+ *pTruth = ((word)puTruth[Abc_ObjFaninNum(pObj) == 6] << 32) | (word)puTruth[0];
+ pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), pTruth );
}
Abc_NtkForEachCo( pNtk, pObj, i )
Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp );
@@ -1816,6 +1819,72 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
Vec_PtrFree( vNodes );
Vec_IntFree( vTruth );
Vec_IntFree( vFanins );
+ Vec_WrdFree( vTruths );
+ return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the percentable of increased power due to glitching.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose )
+{
+ int nSwitches, nGlitches;
+ Gli_Man_t * p;
+ Vec_Ptr_t * vNodes;
+ Vec_Int_t * vFanins;
+ Abc_Obj_t * pObj, * pFanin;
+ int i, k, nFaninMax = Abc_NtkGetFaninMax(pNtk);
+ if ( !Abc_NtkIsMappedLogic(pNtk) )
+ return Abc_NtkMfsTotalGlitchingLut( pNtk, nPats, Prob, fVerbose );
+ assert( Abc_NtkIsMappedLogic(pNtk) );
+ if ( nFaninMax > 16 )
+ {
+ printf( "Abc_NtkMfsTotalGlitching() This procedure works only for mapped networks with LUTs size up to 6 inputs.\n" );
+ return -1.0;
+ }
+ vNodes = Abc_NtkDfs( pNtk, 0 );
+ vFanins = Vec_IntAlloc( 6 );
+
+ // derive network for glitch computation
+ p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk),
+ Abc_NtkLatchNum(pNtk), Abc_NtkGetTotalFanins(pNtk) + Abc_NtkCoNum(pNtk) );
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ pObj->iTemp = -1;
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ pObj->iTemp = Gli_ManCreateCi( p, Abc_ObjFanoutNum(pObj) );
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+ {
+ Vec_IntClear( vFanins );
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Vec_IntPush( vFanins, pFanin->iTemp );
+ pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), Mio_GateReadTruthP((Mio_Gate_t *)pObj->pData) );
+ }
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp );
+
+ // compute glitching
+ Gli_ManSwitchesAndGlitches( p, nPats, 1.0/Prob, fVerbose );
+
+ // compute the ratio
+ nSwitches = nGlitches = 0;
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ if ( pObj->iTemp >= 0 )
+ {
+ nSwitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumSwitches(p, pObj->iTemp);
+ nGlitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumGlitches(p, pObj->iTemp);
+ }
+
+ Gli_ManStop( p );
+ Vec_PtrFree( vNodes );
+ Vec_IntFree( vFanins );
return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0;
}
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index b97f526f..abf56716 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -17,6 +17,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDress2.c \
src/base/abci/abcDress3.c \
src/base/abci/abcDsd.c \
+ src/base/abci/abcEco.c \
src/base/abci/abcExact.c \
src/base/abci/abcExtract.c \
src/base/abci/abcFraig.c \
diff --git a/src/base/cmd/cmdHist.c b/src/base/cmd/cmdHist.c
index d1ff0a9d..36e546a7 100644
--- a/src/base/cmd/cmdHist.c
+++ b/src/base/cmd/cmdHist.c
@@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+#define ABC_USE_HISTORY 1
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -99,7 +101,7 @@ void Cmd_HistoryAddCommand( Abc_Frame_t * p, const char * command )
***********************************************************************/
void Cmd_HistoryRead( Abc_Frame_t * p )
{
-#if defined(WIN32)
+#if defined(WIN32) && defined(ABC_USE_HISTORY)
char Buffer[ABC_MAX_STR];
FILE * pFile;
assert( Vec_PtrSize(p->aHistory) == 0 );
@@ -130,7 +132,7 @@ void Cmd_HistoryRead( Abc_Frame_t * p )
***********************************************************************/
void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
{
-#if defined(WIN32)
+#if defined(WIN32) && defined(ABC_USE_HISTORY)
FILE * pFile;
char * pStr;
int i;
@@ -160,7 +162,7 @@ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
***********************************************************************/
void Cmd_HistoryPrint( Abc_Frame_t * p, int Limit )
{
-#if defined(WIN32)
+#if defined(WIN32) && defined(ABC_USE_HISTORY)
char * pStr;
int i;
Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit );
diff --git a/src/base/main/abcapis.h b/src/base/main/abcapis.h
new file mode 100644
index 00000000..8c188b67
--- /dev/null
+++ b/src/base/main/abcapis.h
@@ -0,0 +1,105 @@
+/**CFile****************************************************************
+
+ FileName [abcapis.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Include this file in the external code calling ABC.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 29, 2012.]
+
+ Revision [$Id: abcapis.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef MINI_AIG__abc_apis_h
+#define MINI_AIG__abc_apis_h
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+typedef struct Abc_Frame_t_ Abc_Frame_t;
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef WIN32
+ #ifdef WIN32_NO_DLL
+ #define ABC_DLLEXPORT
+ #define ABC_DLLIMPORT
+ #else
+ #define ABC_DLLEXPORT __declspec(dllexport)
+ #define ABC_DLLIMPORT __declspec(dllimport)
+ #endif
+#else /* defined(WIN32) */
+#define ABC_DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL ABC_DLLIMPORT
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// procedures to start and stop the ABC framework
+extern ABC_DLL void Abc_Start();
+extern ABC_DLL void Abc_Stop();
+
+// procedures to get the ABC framework (pAbc) and execute commands in it
+extern ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame();
+extern ABC_DLL int Cmd_CommandExecute( Abc_Frame_t * pAbc, const char * pCommandLine );
+
+// procedures to input/output 'mini AIG'
+extern ABC_DLL void Abc_NtkInputMiniAig( Abc_Frame_t * pAbc, void * pMiniAig );
+extern ABC_DLL void * Abc_NtkOutputMiniAig( Abc_Frame_t * pAbc );
+extern ABC_DLL void Abc_FrameGiaInputMiniAig( Abc_Frame_t * pAbc, void * p );
+extern ABC_DLL void * Abc_FrameGiaOutputMiniAig( Abc_Frame_t * pAbc );
+extern ABC_DLL void Abc_NtkSetFlopNum( Abc_Frame_t * pAbc, int nFlops );
+
+// procedures to input/output 'mini LUT'
+extern ABC_DLL void Abc_FrameGiaInputMiniLut( Abc_Frame_t * pAbc, void * pMiniLut );
+extern ABC_DLL void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc );
+
+// procedures to set CI/CO arrival/required times
+extern ABC_DLL void Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall );
+extern ABC_DLL void Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall );
+
+// procedure to set AND-gate delay to tech-independent synthesis and mapping
+extern ABC_DLL void Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay );
+
+// procedures to return the mapped network
+extern ABC_DLL int * Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc );
+extern ABC_DLL void Abc_NtkPrintMiniMapping( int * pArray );
+
+// procedures to access verifization status and a counter-example
+extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * pAbc );
+extern ABC_DLL void * Abc_FrameReadCex( Abc_Frame_t * pAbc );
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/main/abcapis_old.h b/src/base/main/abcapis_old.h
new file mode 100644
index 00000000..b2703bea
--- /dev/null
+++ b/src/base/main/abcapis_old.h
@@ -0,0 +1,84 @@
+/**CFile****************************************************************
+
+ FileName [abcapis.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Include this file in the external code calling ABC.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - September 29, 2012.]
+
+ Revision [$Id: abcapis.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef MINI_AIG__abc_apis_old_h
+#define MINI_AIG__abc_apis_old_h
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// procedures to start and stop the ABC framework
+extern void Abc_Start();
+extern void Abc_Stop();
+
+// procedures to get the ABC framework (pAbc) and execute commands in it
+extern void * Abc_FrameGetGlobalFrame();
+extern int Cmd_CommandExecute( void * pAbc, char * pCommandLine );
+
+// procedures to input/output 'mini AIG'
+extern void Abc_NtkInputMiniAig( void * pAbc, void * pMiniAig );
+extern void * Abc_NtkOutputMiniAig( void * pAbc );
+extern void Abc_FrameGiaInputMiniAig( void * pAbc, void * p );
+extern void * Abc_FrameGiaOutputMiniAig( void * pAbc );
+extern void Abc_NtkSetFlopNum( void * pAbc, int nFlops );
+
+// procedures to input/output 'mini LUT'
+extern void Abc_FrameGiaInputMiniLut( void * pAbc, void * pMiniLut );
+extern void * Abc_FrameGiaOutputMiniLut( void * pAbc );
+
+// procedures to set CI/CO arrival/required times
+extern void Abc_NtkSetCiArrivalTime( void * pAbc, int iCi, float Rise, float Fall );
+extern void Abc_NtkSetCoRequiredTime( void * pAbc, int iCo, float Rise, float Fall );
+
+// procedure to set AND-gate delay to tech-independent synthesis and mapping
+extern void Abc_NtkSetAndGateDelay( void * pAbc, float Delay );
+
+// procedures to return the mapped network
+extern int * Abc_NtkOutputMiniMapping( void * pAbc );
+extern void Abc_NtkPrintMiniMapping( int * pArray );
+
+// procedures to access verifization status and a counter-example
+extern int Abc_FrameReadProbStatus( void * pAbc );
+extern void * Abc_FrameReadCex( void * pAbc );
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 89353fa6..a59a9a40 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -34,10 +34,8 @@
#include "misc/vec/vec.h"
#include "misc/st/st.h"
-ABC_NAMESPACE_HEADER_START
-// the framework containing all data
-typedef struct Abc_Frame_t_ Abc_Frame_t;
-ABC_NAMESPACE_HEADER_END
+// the framework containing all data is defined here
+#include "abcapis.h"
#include "base/cmd/cmd.h"
#include "base/io/ioAbc.h"
@@ -116,7 +114,7 @@ extern ABC_DLL void Abc_FrameSetBridgeMode();
extern ABC_DLL int Abc_FrameReadBmcFrames( Abc_Frame_t * p );
extern ABC_DLL int Abc_FrameReadProbStatus( Abc_Frame_t * p );
-extern ABC_DLL Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p );
+extern ABC_DLL void * Abc_FrameReadCex( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p );
extern ABC_DLL Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p );
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p );
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 9647d020..cd4ff2c7 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -69,7 +69,7 @@ char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagRe
int Abc_FrameReadBmcFrames( Abc_Frame_t * p ) { return s_GlobalFrame->nFrames; }
int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFrame->Status; }
-Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; }
+void * Abc_FrameReadCex( Abc_Frame_t * p ) { return s_GlobalFrame->pCex; }
Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p ) { return s_GlobalFrame->vCexVec; }
Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p ) { return s_GlobalFrame->vStatuses; }
Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p ) { return s_GlobalFrame->vPoEquivs; }
diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c
index 49c25ad0..3b747cc5 100644
--- a/src/base/wlc/wlcStdin.c
+++ b/src/base/wlc/wlcStdin.c
@@ -239,7 +239,7 @@ int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd )
return 0;
}
// report value of this variable
- Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, Abc_FrameReadCex(pAbc), pName, 16 );
+ Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, (Abc_Cex_t *)Abc_FrameReadCex(pAbc), pName, 16 );
Vec_StrFree( vInput );
fflush( stdout );
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-06 12:06:32 +0000