Skip to content

A
abc
Commit 6da56f1f by Alan Mishchenko
Options

Version abc80516

parent 74ff01bf
Showing with 260 additions and 54 deletions
abc.dsp
......@@ -3266,6 +3266,10 @@ SOURCE=.\src\aig\saig\saigInter.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigIoa.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigPhase.c
# End Source File
# Begin Source File
......@@ -3284,6 +3288,10 @@ SOURCE=.\src\aig\saig\saigRetStep.c
SOURCE=.\src\aig\saig\saigScl.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\saig\saigTrans.c
# End Source File
# End Group
# Begin Group "bbr"
......
src/aig/aig/aig.h
......@@ -135,6 +135,7 @@ struct Aig_Man_t_
Vec_Int_t * vLevelR; // the reverse level of the nodes
int nLevelMax; // maximum number of levels
void * pData; // the temporary data
void * pData2; // the temporary data
int nTravIds; // the current traversal ID
int fCatchExor; // enables EXOR nodes
int fAddStrash; // performs additional strashing
......@@ -497,6 +498,7 @@ extern int Aig_ManCleanup( Aig_Man_t * p );
extern int Aig_ManPiCleanup( Aig_Man_t * p );
extern void Aig_ManPrintStats( Aig_Man_t * p );
extern void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew );
extern void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs );
/*=== aigMem.c ==========================================================*/
extern void Aig_ManStartMemory( Aig_Man_t * p );
extern void Aig_ManStopMemory( Aig_Man_t * p );
......@@ -625,6 +627,7 @@ extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
extern void Aig_ManSetPioNumbers( Aig_Man_t * p );
extern void Aig_ManCleanPioNumbers( Aig_Man_t * p );
extern int Aig_ManCountChoices( Aig_Man_t * p );
extern char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix );
extern unsigned Aig_ManRandom( int fReset );
/*=== aigWin.c =========================================================*/
......
src/aig/aig/aigMan.c
......@@ -359,6 +359,25 @@ void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew )
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Sets the number of registers in the AIG manager.]
Description [This procedure should be called after the manager is
fully constructed.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs )
{
p->nRegs = nRegs;
p->nTruePis = Aig_ManPiNum(p) - nRegs;
p->nTruePos = Aig_ManPoNum(p) - nRegs;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/aig/aigUtil.c
......@@ -992,6 +992,28 @@ void Aig_ManPrintControlFanouts( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Returns the composite name of the file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix )
{
static char Buffer[1000];
char * pDot;
strcpy( Buffer, pBase );
if ( (pDot = strrchr( Buffer, '.' )) )
*pDot = 0;
strcat( Buffer, pSuffix );
return Buffer;
}
/**Function*************************************************************
Synopsis [Creates a sequence or random numbers.]
Description []
......
src/aig/fra/fraCore.c
......@@ -411,6 +411,7 @@ p->timeTrav += clock() - clk2;
}
else
{
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
Aig_ManCleanup( p->pManFraig );
pManAigNew = p->pManFraig;
p->pManFraig = NULL;
......
src/aig/fra/fraInd.c
......@@ -616,6 +616,63 @@ finish:
return pManAigNew;
}
/**Function*************************************************************
Synopsis [Outputs a set of pairs of equivalent nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams )
{
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
FILE * pFile;
char * pFilePairs;
Aig_Man_t * pMan, * pNew;
Aig_Obj_t * pObj, * pRepr;
int * pNum2Id;
int i, Counter = 0;
pMan = Saig_ManReadBlif( pFileName );
if ( pMan == NULL )
return 0;
// perform seq SAT sweeping
pNew = Fra_FraigInduction( pMan, pParams );
if ( pNew == NULL )
{
Aig_ManStop( pMan );
return 0;
}
if ( pParams->fVerbose )
{
printf( "Original AIG: " );
Aig_ManPrintStats( pMan );
printf( "Reduced AIG: " );
Aig_ManPrintStats( pNew );
}
Aig_ManStop( pNew );
pNum2Id = pMan->pData;
// write the output file
pFilePairs = Aig_FileNameGenericAppend( pFileName, ".pairs" );
pFile = fopen( pFilePairs, "w" );
Aig_ManForEachObj( pMan, pObj, i )
if ( (pRepr = pMan->pReprs[pObj->Id]) )
{
fprintf( pFile, "%d %d %c\n", pNum2Id[pObj->Id], pNum2Id[pRepr->Id], (Aig_ObjPhase(pObj) ^ Aig_ObjPhase(pRepr))? '-' : '+' );
Counter++;
}
fclose( pFile );
if ( pParams->fVerbose )
{
printf( "Result: %d pairs of seq equiv nodes are written into file \"%s\".\n", Counter, pFilePairs );
}
Aig_ManStop( pMan );
return 1;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/aig/saig/module.make
SRC += src/aig/saig/saigBmc.c \
src/aig/saig/saigCone.c \
src/aig/saig/saigInter.c \
src/aig/saig/saigIoa.c \
src/aig/saig/saigPhase.c \
src/aig/saig/saigRetFwd.c \
src/aig/saig/saigRetMin.c \
src/aig/saig/saigRetStep.c \
src/aig/saig/saigScl.c
src/aig/saig/saigScl.c \
src/aig/saig/saigTrans.c
src/aig/saig/saig.h
......@@ -79,6 +79,9 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) {
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
/*=== saigIoa.c ==========================================================*/
extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
/*=== saigInter.c ==========================================================*/
extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
/*=== saigPhase.c ==========================================================*/
......@@ -92,6 +95,8 @@ extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, in
extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
/*=== saigScl.c ==========================================================*/
extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
/*=== saigTrans.c ==========================================================*/
extern Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit, int fVerbose );
#ifdef __cplusplus
}
......
src/base/abci/abcDar.c
......@@ -1491,6 +1491,7 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchE
if ( pMan->vFlopNums )
Vec_IntFree( pMan->vFlopNums );
pMan->vFlopNums = NULL;
pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
......@@ -2083,6 +2084,38 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
/**Function*************************************************************
Synopsis [Performs phase abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 0 );
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
if ( pMan == NULL )
return NULL;
pMan = Saig_ManTimeframeSimplify( pTemp = pMan, nPrefix, nFrames, fInit, fVerbose );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkFromAigPhase( pMan );
pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Performs BDD-based reachability analysis.]
Description []
......@@ -2107,6 +2140,38 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
}
/**Function*************************************************************
Synopsis [Performs BDD-based reachability analysis.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
{
Aig_Man_t * pMan;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 1 );
pMan->nRegs = Abc_NtkLatchNum(pNtk);
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
if ( pMan == NULL )
return;
Aig_ManSetRegNum( pMan, pMan->nRegs );
Aig_ManPrintStats( pMan );
Saig_ManDumpBlif( pMan, "_temp_.blif" );
Aig_ManStop( pMan );
pMan = Saig_ManReadBlif( "_temp_.blif" );
Aig_ManPrintStats( pMan );
Aig_ManStop( pMan );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/abci/abcMiter.c
......@@ -766,7 +766,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVerbose )
{
char Buffer[1000];
ProgressBar * pProgress;
......
src/base/abci/abcVerify.c
......@@ -478,7 +478,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
}
// create the timeframes
pFrames = Abc_NtkFrames( pMiter, nFrames, 1 );
pFrames = Abc_NtkFrames( pMiter, nFrames, 1, 0 );
Abc_NtkDelete( pMiter );
if ( pFrames == NULL )
{
......@@ -564,7 +564,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
}
// create the timeframes
pFrames = Abc_NtkFrames( pMiter, nFrames, 1 );
pFrames = Abc_NtkFrames( pMiter, nFrames, 1, 0 );
Abc_NtkDelete( pMiter );
if ( pFrames == NULL )
{
......@@ -777,7 +777,7 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
Vec_Ptr_t * vSupp;
int i, k;
// get the timeframes of the network
pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0 );
pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0, 0 );
//Abc_NtkShowAig( pFrames );
// get the PO of the timeframes
......
src/base/main/main.h
......@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: main.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: main.h,v 1.1 2008/05/14 22:13:13 wudenni Exp $]
***********************************************************************/
......@@ -69,47 +69,57 @@ typedef struct Abc_Frame_t_ Abc_Frame_t;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#ifdef WIN32
#define DLLEXPORT __declspec(dllexport)
#define DLLIMPORT __declspec(dllimport)
#else /* defined(WIN32) */
#define DLLIMPORT
#endif /* defined(WIN32) */
#ifndef ABC_DLL
#define ABC_DLL DLLIMPORT
#endif
/*=== main.c ===========================================================*/
extern void Abc_Start();
extern void Abc_Stop();
extern ABC_DLL void Abc_Start();
extern ABC_DLL void Abc_Stop();
/*=== mainFrame.c ===========================================================*/
extern Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p );
extern FILE * Abc_FrameReadOut( Abc_Frame_t * p );
extern FILE * Abc_FrameReadErr( Abc_Frame_t * p );
extern bool Abc_FrameReadMode( Abc_Frame_t * p );
extern bool Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode );
extern void Abc_FrameRestart( Abc_Frame_t * p );
extern bool Abc_FrameShowProgress( Abc_Frame_t * p );
extern void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
extern void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
extern void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
extern void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p );
extern void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
extern void Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
extern Abc_Frame_t * Abc_FrameGetGlobalFrame();
extern Vec_Ptr_t * Abc_FrameReadStore();
extern int Abc_FrameReadStoreSize();
extern void * Abc_FrameReadLibLut();
extern void * Abc_FrameReadLibGen();
extern void * Abc_FrameReadLibSuper();
extern void * Abc_FrameReadLibVer();
extern void * Abc_FrameReadManDd();
extern void * Abc_FrameReadManDec();
extern char * Abc_FrameReadFlag( char * pFlag );
extern bool Abc_FrameIsFlagEnabled( char * pFlag );
extern void Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk );
extern void Abc_FrameSetNtkStoreSize( int nStored );
extern void Abc_FrameSetLibLut( void * pLib );
extern void Abc_FrameSetLibGen( void * pLib );
extern void Abc_FrameSetLibSuper( void * pLib );
extern void Abc_FrameSetLibVer( void * pLib );
extern void Abc_FrameSetFlag( char * pFlag, char * pValue );
extern ABC_DLL Abc_Ntk_t * Abc_FrameReadNtk( Abc_Frame_t * p );
extern ABC_DLL FILE * Abc_FrameReadOut( Abc_Frame_t * p );
extern ABC_DLL FILE * Abc_FrameReadErr( Abc_Frame_t * p );
extern ABC_DLL bool Abc_FrameReadMode( Abc_Frame_t * p );
extern ABC_DLL bool Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode );
extern ABC_DLL void Abc_FrameRestart( Abc_Frame_t * p );
extern ABC_DLL bool Abc_FrameShowProgress( Abc_Frame_t * p );
extern ABC_DLL void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
extern ABC_DLL void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
extern ABC_DLL void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
extern ABC_DLL void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p );
extern ABC_DLL void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
extern ABC_DLL void Abc_FrameSetGlobalFrame( Abc_Frame_t * p );
extern ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame();
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadStore();
extern ABC_DLL int Abc_FrameReadStoreSize();
extern ABC_DLL void * Abc_FrameReadLibLut();
extern ABC_DLL void * Abc_FrameReadLibGen();
extern ABC_DLL void * Abc_FrameReadLibSuper();
extern ABC_DLL void * Abc_FrameReadLibVer();
extern ABC_DLL void * Abc_FrameReadManDd();
extern ABC_DLL void * Abc_FrameReadManDec();
extern ABC_DLL char * Abc_FrameReadFlag( char * pFlag );
extern ABC_DLL bool Abc_FrameIsFlagEnabled( char * pFlag );
extern ABC_DLL void Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk );
extern ABC_DLL void Abc_FrameSetNtkStoreSize( int nStored );
extern ABC_DLL void Abc_FrameSetLibLut( void * pLib );
extern ABC_DLL void Abc_FrameSetLibGen( void * pLib );
extern ABC_DLL void Abc_FrameSetLibSuper( void * pLib );
extern ABC_DLL void Abc_FrameSetLibVer( void * pLib );
extern ABC_DLL void Abc_FrameSetFlag( char * pFlag, char * pValue );
#ifdef __cplusplus
}
......
src/base/main/mainInt.h
......@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mainInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: mainInt.h,v 1.1 2008/05/14 22:13:13 wudenni Exp $]
***********************************************************************/
......@@ -93,21 +93,31 @@ struct Abc_Frame_t_
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
#ifdef WIN32
#define DLLEXPORT __declspec(dllexport)
#define DLLIMPORT __declspec(dllimport)
#else /* defined(WIN32) */
#define DLLIMPORT
#endif /* defined(WIN32) */
#ifndef ABC_DLL
#define ABC_DLL DLLIMPORT
#endif
/*=== mvMain.c ===========================================================*/
extern int main( int argc, char * argv[] );
extern ABC_DLL int main( int argc, char * argv[] );
/*=== mvInit.c ===================================================*/
extern void Abc_FrameInit( Abc_Frame_t * pAbc );
extern void Abc_FrameEnd( Abc_Frame_t * pAbc );
extern ABC_DLL void Abc_FrameInit( Abc_Frame_t * pAbc );
extern ABC_DLL void Abc_FrameEnd( Abc_Frame_t * pAbc );
/*=== mvFrame.c =====================================================*/
extern Abc_Frame_t * Abc_FrameAllocate();
extern void Abc_FrameDeallocate( Abc_Frame_t * p );
extern ABC_DLL Abc_Frame_t * Abc_FrameAllocate();
extern ABC_DLL void Abc_FrameDeallocate( Abc_Frame_t * p );
/*=== mvUtils.c =====================================================*/
extern char * Abc_UtilsGetVersion( Abc_Frame_t * pAbc );
extern char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc );
extern void Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
extern void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
extern void Abc_UtilsSource( Abc_Frame_t * pAbc );
extern ABC_DLL char * Abc_UtilsGetVersion( Abc_Frame_t * pAbc );
extern ABC_DLL char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc );
extern ABC_DLL void Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
extern ABC_DLL void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
extern ABC_DLL void Abc_UtilsSource( Abc_Frame_t * pAbc );
#endif
......
src/misc/vec/vec.h
......@@ -72,6 +72,10 @@ typedef long long sint64;
#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
#endif
#ifndef CALLOC
#define CALLOC(type, num) ((type *) calloc((num), sizeof(type)))
#endif
#ifndef FREE
#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
#endif
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment