summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c195
-rw-r--r--src/base/abci/abcDar.c53
-rw-r--r--src/base/main/mainInt.h4
3 files changed, 232 insertions, 20 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ac417d14..2ad8dc75 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -37,6 +37,7 @@
#include "int.h"
#include "dch.h"
#include "ssw.h"
+#include "cgt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -200,6 +201,7 @@ static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDarPhase ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSynch ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandClockGate ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -470,6 +472,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "sim", Abc_CommandSim, 0 );
Cmd_CommandAdd( pAbc, "Sequential", "phase", Abc_CommandDarPhase, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "synch", Abc_CommandSynch, 1 );
+ Cmd_CommandAdd( pAbc, "Sequential", "clockgate", Abc_CommandClockGate, 1 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 );
@@ -7941,7 +7944,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
-
+/*
pNtkRes = Abc_NtkDarTestNtk( pNtk );
if ( pNtkRes == NULL )
{
@@ -7950,9 +7953,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+*/
-
-// Abc_NtkDarTest( pNtk );
+ Abc_NtkDarTest( pNtk );
return 0;
usage:
@@ -14634,6 +14637,162 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandClockGate( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Cgt_Par_t Pars, * pPars = &Pars;
+ Abc_Ntk_t * pNtkRes, * pNtk, * pNtkCare;
+ int c;
+
+ extern Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t * pPars );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ Cgt_SetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "LNDCVKvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'L':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLevelMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLevelMax <= 0 )
+ goto usage;
+ break;
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nCandMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nCandMax <= 0 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nOdcMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nOdcMax <= 0 )
+ goto usage;
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nConfMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nConfMax <= 0 )
+ goto usage;
+ break;
+ case 'V':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-V\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nVarsMin = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nVarsMin <= 0 )
+ goto usage;
+ break;
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nFlopsMin = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nFlopsMin <= 0 )
+ goto usage;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( argc == globalUtilOptind + 1 )
+ {
+ pNtkCare = Io_Read( argv[globalUtilOptind], Io_ReadFileType(argv[globalUtilOptind]), 1 );
+ if ( pNtkCare == NULL )
+ {
+ printf( "Reading care network has failed.\n" );
+ return 1;
+ }
+ // modify the current network
+ pNtkRes = Abc_NtkDarClockGate( pNtk, pNtkCare, pPars );
+ Abc_NtkDelete( pNtkCare );
+ }
+ else if ( argc == globalUtilOptind )
+ {
+ pNtkRes = Abc_NtkDarClockGate( pNtk, NULL, pPars );
+ }
+ else
+ {
+ fprintf( pErr, "Wrong number of arguments.\n" );
+ return 0;
+ }
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Clock gating has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: clockgate [-LNDCVK <num>] [-vh] <file>\n" );
+ fprintf( pErr, "\t sequential clock gating with observability don't-cares\n" );
+ fprintf( pErr, "\t-L num : max level number of a clock gate [default = %d]\n", pPars->nLevelMax );
+ fprintf( pErr, "\t-N num : max number of candidates for a flop [default = %d]\n", pPars->nCandMax );
+ fprintf( pErr, "\t-D num : max number of ODC levels to consider [default = %d]\n", pPars->nOdcMax );
+ fprintf( pErr, "\t-C num : max number of conflicts at a node [default = %d]\n", pPars->nConfMax );
+ fprintf( pErr, "\t-V num : min number of vars to recycle SAT solver [default = %d]\n", pPars->nVarsMin );
+ fprintf( pErr, "\t-K num : min number of flops to recycle SAT solver [default = %d]\n", pPars->nFlopsMin );
+ fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ fprintf( pErr, "\tfile : (optional) constraints for primary inputs and register outputs\n");
+ return 1;
+}
/**Function*************************************************************
@@ -16239,11 +16398,11 @@ int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- nFrames = 1000;
+ nFrames = 2000;
nSizeMax = 200000;
- nBTLimit = 10000;
- nBTLimitAll = 10000000;
- nNodeDelta = 1000;
+ nBTLimit = 2000;
+ nBTLimitAll = 2000000;
+ nNodeDelta = 2000;
fRewrite = 0;
fNewAlgo = 0;
fVerbose = 0;
@@ -16896,9 +17055,11 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
int nFramesMax;
int nConfMax;
+ int fDynamic;
+ int fExtend;
int fVerbose;
int c;
- extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -16907,9 +17068,11 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
nFramesMax = 10;
nConfMax = 10000;
- fVerbose = 1;
+ fDynamic = 1;
+ fExtend = 0;
+ fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FCdevh" ) ) != EOF )
{
switch ( c )
{
@@ -16935,6 +17098,12 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nConfMax < 0 )
goto usage;
break;
+ case 'd':
+ fDynamic ^= 1;
+ break;
+ case 'e':
+ fExtend ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -16961,7 +17130,7 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
- pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fVerbose );
+ pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Target enlargement has failed.\n" );
@@ -16971,10 +17140,12 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
- fprintf( pErr, "usage: abs [-FC num] [-vh]\n" );
+ fprintf( pErr, "usage: abs [-FC num] [-devh]\n" );
fprintf( pErr, "\t proof-based abstraction from UNSAT core of the BMC instance\n" );
fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
+ fprintf( pErr, "\t-d : toggle dynamic unrolling of timeframes [default = %s]\n", fDynamic? "yes": "no" );
+ fprintf( pErr, "\t-e : toggle extending abstraction using COI of flops [default = %s]\n", fExtend? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 22f4b45c..dcc7f4c1 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -28,6 +28,7 @@
#include "int.h"
#include "dch.h"
#include "ssw.h"
+#include "cgt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -2189,10 +2190,8 @@ PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fDynamic, int fExtend, int fVerbose )
{
- Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
-
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
assert( Abc_NtkIsStrash(pNtk) );
@@ -2201,7 +2200,7 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fVerbose );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
@@ -2563,6 +2562,44 @@ Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, i
SeeAlso []
***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t * pPars )
+{
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
+ pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan1 == NULL )
+ return NULL;
+ if ( pCare )
+ {
+ pMan2 = Abc_NtkToDar( pCare, 0, 0 );
+ if ( pMan2 == NULL )
+ {
+ Aig_ManStop( pMan1 );
+ return NULL;
+ }
+ }
+ pMan = Cgt_ClockGating( pMan1, pMan2, pPars );
+ Aig_ManStop( pMan1 );
+ if ( pMan2 )
+ Aig_ManStop( pMan2 );
+ if ( pMan == NULL )
+ return NULL;
+ pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**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;
@@ -2677,7 +2714,7 @@ Aig_ManPrintStats( pMan );
pTemp = Ssw_SignalCorrespondeceTestPairs( pMan );
Aig_ManStop( pTemp );
*/
- Ssw_SecSpecialMiter( pMan, 0 );
+ Ssw_SecSpecialMiter( pMan, 1 );
Aig_ManStop( pMan );
}
@@ -2708,6 +2745,8 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
Aig_ManSetRegNum( pMan, pMan->nRegs );
pMan = Ssw_SignalCorrespondeceTestPairs( pTemp = pMan );
Aig_ManStop( pTemp );
+ if ( pMan == NULL )
+ return NULL;
pNtkAig = Abc_NtkFromAigPhase( pMan );
pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
@@ -2715,8 +2754,6 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
Aig_ManStop( pMan );
return pNtkAig;
*/
- Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
-
Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp;
assert( Abc_NtkIsStrash(pNtk) );
@@ -2725,7 +2762,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 1 );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 1 );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index b03a00fa..becbfd6b 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -79,6 +79,10 @@ struct Abc_Frame_t_
void * pAbc8Nwk; // the current mapped network
void * pAbc8Aig; // the current AIG
void * pAbc8Lib; // the current LUT library
+
+ // the addition to keep the best Ntl that can be used to restore
+ void * pAbc8NtlBestDelay; // the best delay, Ntl
+ void * pAbc8NtlBestArea; // the best area
};
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-30 20:51:39 +0000