summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2009-03-10 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2009-03-10 08:01:00 -0700
commit32314347bae6ddcd841a268e797ec4da45726abb (patch)
treee2e5fd1711f04a06d0da2b8003bc02cb9a5dd446 /src/base/abci
parentc03f9b516bed2c06ec2bfc78617eba5fc9a11c32 (diff)
downloadabc-32314347bae6ddcd841a268e797ec4da45726abb.tar.gz
abc-32314347bae6ddcd841a268e797ec4da45726abb.tar.bz2
abc-32314347bae6ddcd841a268e797ec4da45726abb.zip
Version abc90310
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c1295
-rw-r--r--src/base/abci/abcDar.c122
-rw-r--r--src/base/abci/abcDsd.c3
-rw-r--r--src/base/abci/abcLutmin.c209
-rw-r--r--src/base/abci/module.make1
5 files changed, 1140 insertions, 490 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e7187a9f..1164c3da 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -82,6 +82,7 @@ static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandEliminate ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLutpack ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandLutmin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -151,14 +152,13 @@ static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandNFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSimSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMatch ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandQbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -217,7 +217,6 @@ static int Abc_CommandExtWin ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandInsWin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCec2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -258,6 +257,7 @@ static int Abc_CommandAbc8Bidec ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc8Strash ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Lutpack ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Lutmin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Balance ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Speedup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc8Merge ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -279,6 +279,7 @@ static int Abc_CommandAbc9Read ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc9Write ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Ps ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PFan ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9PSig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Status ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Show ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Hash ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -287,13 +288,18 @@ static int Abc_CommandAbc9Cof ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandAbc9Trim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Dfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sim ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Equiv ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Times ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Frames ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Miter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Scl ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Srm ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Embed ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9If ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbcTestNew ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -391,6 +397,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "eliminate", Abc_CommandEliminate, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "lutpack", Abc_CommandLutpack, 1 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "lutmin", Abc_CommandLutmin, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs", Abc_CommandMfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "trace", Abc_CommandTrace, 0 );
@@ -460,10 +467,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "isat", Abc_CommandISat, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "ifraig", Abc_CommandIFraig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dfraig", Abc_CommandDFraig, 1 );
- Cmd_CommandAdd( pAbc, "New AIG", "nfraig", Abc_CommandNFraig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "csweep", Abc_CommandCSweep, 1 );
// Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 );
- Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 );
+// Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "qbf", Abc_CommandQbf, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 );
@@ -520,7 +526,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "inswin", Abc_CommandInsWin, 1 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
- Cmd_CommandAdd( pAbc, "Verification", "cec2", Abc_CommandCec2, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dsec", Abc_CommandDSec, 0 );
@@ -582,6 +587,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "AIG", "&w", Abc_CommandAbc9Write, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&ps", Abc_CommandAbc9Ps, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&pfan", Abc_CommandAbc9PFan, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&psig", Abc_CommandAbc9PSig, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&status", Abc_CommandAbc9Status, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&show", Abc_CommandAbc9Show, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&hash", Abc_CommandAbc9Hash, 0 );
@@ -590,13 +596,18 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "AIG", "&trim", Abc_CommandAbc9Trim, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&dfs", Abc_CommandAbc9Dfs, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&sim", Abc_CommandAbc9Sim, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&equiv", Abc_CommandAbc9Equiv, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&times", Abc_CommandAbc9Times, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&frames", Abc_CommandAbc9Frames, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&miter", Abc_CommandAbc9Miter, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&scl", Abc_CommandAbc9Scl, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&sat", Abc_CommandAbc9Sat, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&fraig", Abc_CommandAbc9Fraig, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&srm", Abc_CommandAbc9Srm, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&cec", Abc_CommandAbc9Cec, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&force", Abc_CommandAbc9Force, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&embed", Abc_CommandAbc9Embed, 0 );
+ Cmd_CommandAdd( pAbc, "AIG", "&if", Abc_CommandAbc9If, 0 );
Cmd_CommandAdd( pAbc, "AIG", "&test", Abc_CommandAbc9Test, 0 );
Cmd_CommandAdd( pAbc, "Various", "testnew", Abc_CommandAbcTestNew, 0 );
@@ -634,6 +645,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
extern void Gia_SortTest();
// Gia_SortTest();
}
+ {
+ void For_ManFileExperiment();
+// For_ManFileExperiment();
+ }
}
@@ -3694,6 +3709,85 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandLutmin( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c;
+ int nLutSize;
+ int fVerbose;
+ extern Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nLutSize = 6;
+ fVerbose = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Kvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nLutSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nLutSize > 1 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ // modify the current network
+ pNtkRes = Abc_NtkLutmin( pNtk, nLutSize, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "The command has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: lutmin [-K <num>] [-vh]\n" );
+ fprintf( pErr, "\t perform FPGA mapping while minimizing the LUT count\n" );
+ fprintf( pErr, "\t as described in the paper T. Sasao and A. Mishchenko:\n" );
+ fprintf( pErr, "\t \"On the number of LUTs to implement logic functions\".\n" );
+ fprintf( pErr, "\t-K <num> : the LUT size to use for the mapping (2 <= num) [default = %d]\n", nLutSize );
+ fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -5369,12 +5463,6 @@ int Abc_CommandDemiter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( !Abc_NodeIsExorType(Abc_ObjFanin0(Abc_NtkPo(pNtk,0))) )
- {
- fprintf( pErr, "The miter's PO is not an EXOR.\n" );
- return 1;
- }
-
// get the new network
if ( fSeq )
{
@@ -5391,6 +5479,11 @@ int Abc_CommandDemiter( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "The network is not a single-output miter.\n" );
return 1;
}
+ if ( !Abc_NodeIsExorType(Abc_ObjFanin0(Abc_NtkPo(pNtk,0))) )
+ {
+ fprintf( pErr, "The miter's PO is not an EXOR.\n" );
+ return 1;
+ }
if ( !Abc_NtkDemiter( pNtk ) )
{
fprintf( pErr, "Demitering has failed.\n" );
@@ -8163,6 +8256,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk );
extern void Amap_LibertyTest( char * pFileName );
+ extern void Bbl_ManTest( Abc_Ntk_t * pNtk );
+ extern void Bbl_ManSimpleDemo();
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -8379,6 +8474,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_NtkDarTest( pNtk );
+ Bbl_ManTest( pNtk );
+// Bbl_ManSimpleDemo();
return 0;
usage:
fprintf( pErr, "usage: test [-h] <file_name>\n" );
@@ -10076,152 +10173,6 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandNFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
- Cec_ParCsw_t Pars, * p = &Pars;
- FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk, * pNtkRes;
- int c;
- extern Abc_Ntk_t * Abc_NtkDarSatSweep( Abc_Ntk_t * pNtk, Cec_ParCsw_t * pPars );
-
- pNtk = Abc_FrameReadNtk(pAbc);
- pOut = Abc_FrameReadOut(pAbc);
- pErr = Abc_FrameReadErr(pAbc);
-
- // set defaults
- Cec_ManCswSetDefaultParams( p );
- Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WRCNZLrfvh" ) ) != EOF )
- {
- switch ( c )
- {
- case 'W':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
- goto usage;
- }
- p->nWords = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( p->nWords < 0 )
- goto usage;
- break;
- case 'R':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
- goto usage;
- }
- p->nRounds = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( p->nRounds < 0 )
- goto usage;
- break;
- case 'C':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
- goto usage;
- }
- p->nBTLimit = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( p->nBTLimit < 0 )
- goto usage;
- break;
- case 'N':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
- goto usage;
- }
- p->nSatVarMax = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( p->nSatVarMax < 0 )
- goto usage;
- break;
- case 'Z':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-Z\" should be followed by an integer.\n" );
- goto usage;
- }
- p->nCallsRecycle = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( p->nCallsRecycle < 0 )
- goto usage;
- break;
- case 'L':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
- goto usage;
- }
- p->nLevelMax = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( p->nLevelMax < 0 )
- goto usage;
- break;
- case 'r':
- p->fRewriting ^= 1;
- break;
- case 'f':
- p->fFirstStop ^= 1;
- break;
- case 'v':
- p->fVerbose ^= 1;
- break;
- case 'h':
- goto usage;
- default:
- goto usage;
- }
- }
- if ( pNtk == NULL )
- {
- fprintf( pErr, "Empty network.\n" );
- return 1;
- }
- if ( !Abc_NtkIsStrash(pNtk) )
- {
- fprintf( pErr, "This command works only for strashed networks.\n" );
- return 1;
- }
- pNtkRes = Abc_NtkDarSatSweep( pNtk, p );
- if ( pNtkRes == NULL )
- {
- fprintf( pErr, "Command has failed.\n" );
- return 0;
- }
- // replace the current network
- Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
- return 0;
-usage:
- fprintf( pErr, "usage: nfraig [-WRCNZL num] [-rfvh]\n" );
- fprintf( pErr, "\t performs fraiging using a new method\n" );
- fprintf( pErr, "\t-W num : lthe number of simulation words [default = %d]\n", p->nWords );
- fprintf( pErr, "\t-R num : the number of simulation rounds [default = %d]\n", p->nRounds );
- fprintf( pErr, "\t-C num : limit on conflicts at a node [default = %d]\n", p->nBTLimit );
- fprintf( pErr, "\t-N num : the min number of SAT vars before recycling [default = %d]\n", p->nSatVarMax );
- fprintf( pErr, "\t-Z num : the min number of SAT calls before recycling [default = %d]\n", p->nCallsRecycle );
- fprintf( pErr, "\t-L num : the maximum level of the nodes to be swept [default = %d]\n", p->nLevelMax );
- fprintf( pErr, "\t-r : toggle the use of AIG rewriting [default = %s]\n", p->fRewriting? "yes": "no" );
- fprintf( pErr, "\t-f : stop after one output is disproved [default = %s]\n", p->fFirstStop? "yes": "no" );
- fprintf( pErr, "\t-v : enable verbose printout [default = %s]\n", p->fVerbose? "yes": "no" );
- fprintf( pErr, "\t-h : print the command usage\n");
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -12792,6 +12743,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
+/*
+ if ( pPars->fSeqMap )
+ {
+ fprintf( pErr, "Sequential mapping is currently disabled.\n" );
+ return 1;
+ }
+*/
if ( pPars->fSeqMap && pPars->nLatches == 0 )
{
@@ -12825,12 +12783,6 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( pPars->fSeqMap )
- {
- fprintf( pErr, "Sequential mapping is currently disabled.\n" );
- return 1;
- }
-
// enable truth table computation if choices are selected
if ( (c = Abc_NtkGetChoiceNum( pNtk )) )
{
@@ -15828,6 +15780,7 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
int nConfLimit;
int nInsLimit;
int fPartition;
+ int fIgnoreNames;
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 );
@@ -15846,8 +15799,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
nConfLimit = 10000;
nInsLimit = 0;
fPartition = 0;
+ fIgnoreNames = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPpsvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPpsnvh" ) ) != EOF )
{
switch ( c )
{
@@ -15901,6 +15855,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
fSat ^= 1;
break;
+ case 'n':
+ fIgnoreNames ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -15913,6 +15870,12 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
nArgcNew = argc - globalUtilOptind;
if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
return 1;
+
+ if ( fIgnoreNames )
+ {
+ Abc_NtkShortNames( pNtk1 );
+ Abc_NtkShortNames( pNtk2 );
+ }
// perform equivalence checking
if ( fPartition )
@@ -15933,7 +15896,7 @@ usage:
strcpy( Buffer, "unused" );
else
sprintf( Buffer, "%d", nPartSize );
- fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-P num] [-psvh] <file1> <file2>\n" );
+ fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-P num] [-psnvh] <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 );
@@ -15941,6 +15904,7 @@ usage:
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-n : toggle using names to match CIs/COs [default = %s]\n", fIgnoreNames? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
@@ -16115,149 +16079,6 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandCec2( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
- Cec_ParCec_t Pars, * pPars = &Pars;
- FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
- int fDelete1, fDelete2;
- char ** pArgvNew;
- int nArgcNew;
- int fMiter;
- int c;
-
- extern int Abc_NtkDarCec2( Abc_Ntk_t * pNtk0, Abc_Ntk_t * pNtk1, Cec_ParCec_t * pPars );
-
- pNtk = Abc_FrameReadNtk(pAbc);
- pOut = Abc_FrameReadOut(pAbc);
- pErr = Abc_FrameReadErr(pAbc);
-
- // set defaults
- fMiter = 0;
- Cec_ManCecSetDefaultParams( pPars );
- Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "BMImfrsvh" ) ) != EOF )
- {
- switch ( c )
- {
- case 'B':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
- goto usage;
- }
- pPars->nBTLimitBeg = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( pPars->nBTLimitBeg < 0 )
- goto usage;
- break;
- case 'M':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
- goto usage;
- }
- pPars->nBTlimitMulti = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( pPars->nBTlimitMulti < 0 )
- goto usage;
- break;
- case 'I':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
- goto usage;
- }
- pPars->nIters = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( pPars->nIters < 0 )
- goto usage;
- break;
- case 'm':
- fMiter ^= 1;
- break;
- case 'f':
- pPars->fFirstStop ^= 1;
- break;
- case 'r':
- pPars->fRewriting ^= 1;
- break;
- case 's':
- pPars->fSatSweeping ^= 1;
- break;
- case 'v':
- pPars->fVerbose ^= 1;
- break;
- default:
- goto usage;
- }
- }
-
- pArgvNew = argv + globalUtilOptind;
- nArgcNew = argc - globalUtilOptind;
- if ( fMiter )
- {
- if ( pNtk == NULL )
- {
- fprintf( pErr, "Empty network.\n" );
- return 1;
- }
- if ( Abc_NtkIsStrash(pNtk) )
- {
- pNtk1 = pNtk;
- fDelete1 = 0;
- }
- else
- {
- pNtk1 = Abc_NtkStrash( pNtk, 0, 1, 0 );
- fDelete1 = 1;
- }
- pNtk2 = NULL;
- fDelete2 = 0;
- }
- else
- {
- if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
- return 1;
- }
-
- // perform equivalence checking
- Abc_NtkDarCec2( pNtk1, pNtk2, pPars );
-
- if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
- if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
- return 0;
-
-usage:
- fprintf( pErr, "usage: cec2 [-BMI num] [-frsvh] <file1> <file2>\n" );
- fprintf( pErr, "\t performs combinational equivalence checking\n" );
- fprintf( pErr, "\t-B num : staring limit on the number of conflicts [default = %d]\n", pPars->nBTLimitBeg );
- fprintf( pErr, "\t-M num : multiple of the above limit [default = %d]\n", pPars->nBTlimitMulti );
- fprintf( pErr, "\t-I num : the number of iterations [default = %d]\n", pPars->nIters );
- fprintf( pErr, "\t-m : toggle working on two networks or a miter [default = %s]\n", fMiter? "miter": "two networks" );
- fprintf( pErr, "\t-f : toggle stopping after first mismatch [default = %s]\n", pPars->fFirstStop? "yes": "no" );
- fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
- fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", pPars->fSatSweeping? "SAT only": "FRAIG + SAT" );
- fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
- fprintf( pErr, "\t-h : print the command usage\n");
- fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
- fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
- fprintf( pErr, "\t if no files are given, uses the current network and its spec\n");
- fprintf( pErr, "\t if one file is given, uses the current network and the file\n");
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -22157,6 +21978,56 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9PSig( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ int c;
+ int fSetReset = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'r':
+ fSetReset ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pAig == NULL )
+ {
+ printf( "Abc_CommandAbc9PSigs(): There is no AIG.\n" );
+ return 1;
+ }
+ if ( Gia_ManRegNum(pAbc->pAig) == 0 )
+ {
+ printf( "Abc_CommandAbc9PSigs(): Works only for sequential circuits.\n" );
+ return 1;
+ }
+ Gia_ManDetectSeqSignals( pAbc->pAig, fSetReset );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: &psig [-rh]\n" );
+ fprintf( stdout, "\t prints enable/set/reset statistics\n" );
+ fprintf( stdout, "\t-r : toggle printing set/reset signals [default = %s]\n", fSetReset? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Status( Abc_Frame_t * pAbc, int argc, char ** argv )
{
int c;
@@ -22336,9 +22207,9 @@ usage:
int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
- int c, iVar = 0;
+ int c, iVar = 0, nLimFan = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Vh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "VLh" ) ) != EOF )
{
switch ( c )
{
@@ -22353,6 +22224,17 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( iVar < 0 )
goto usage;
break;
+ case 'L':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nLimFan = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nLimFan < 0 )
+ goto usage;
+ break;
case 'h':
goto usage;
default:
@@ -22364,7 +22246,7 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Cof(): There is no AIG.\n" );
return 1;
}
- pAbc->pAig = Gia_ManDupCofactored( pTemp = pAbc->pAig, iVar );
+ pAbc->pAig = Gia_ManDupCofactored( pTemp = pAbc->pAig, iVar, nLimFan );
if ( pAbc->pAig == NULL )
{
pAbc->pAig = pTemp;
@@ -22375,9 +22257,10 @@ int Abc_CommandAbc9Cof( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( stdout, "usage: &cof [-V num] [-h]\n" );
+ fprintf( stdout, "usage: &cof [-VL num] [-h]\n" );
fprintf( stdout, "\t performs cofactoring w.r.t. a variable\n" );
fprintf( stdout, "\t-V num : the zero-based ID of the variable to cofactor [default = %d]\n", iVar );
+ fprintf( stdout, "\t-L num : cofactor w.r.t. variables whose fanout is higher [default = %d]\n", nLimFan );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
@@ -22397,11 +22280,19 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c;
+ int fTrimCis = 1;
+ int fTrimCos = 1;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ioh" ) ) != EOF )
{
switch ( c )
{
+ case 'i':
+ fTrimCis ^= 1;
+ break;
+ case 'o':
+ fTrimCos ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -22413,13 +22304,15 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Trim(): There is no AIG.\n" );
return 1;
}
- pAbc->pAig = Gia_ManDupTrimmed( pTemp = pAbc->pAig );
+ pAbc->pAig = Gia_ManDupTrimmed( pTemp = pAbc->pAig, fTrimCis, fTrimCos );
Gia_ManStop( pTemp );
return 0;
usage:
- fprintf( stdout, "usage: &trim [-h]\n" );
+ fprintf( stdout, "usage: &trim [-ioh]\n" );
fprintf( stdout, "\t removes PIs without fanout and PO driven by constants\n" );
+ fprintf( stdout, "\t-i : toggle removing PIs [default = %s]\n", fTrimCis? "yes": "no" );
+ fprintf( stdout, "\t-o : toggle removing POs [default = %s]\n", fTrimCos? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
@@ -22563,6 +22456,104 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Equiv( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Cec_ParSim_t Pars, * pPars = &Pars;
+ int c;
+ Cec_ManSimSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WRTsmfdvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'W':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-W\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nWords = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nWords < 0 )
+ goto usage;
+ break;
+ case 'R':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-R\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nRounds = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nRounds < 0 )
+ goto usage;
+ break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->TimeLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->TimeLimit < 0 )
+ goto usage;
+ break;
+ case 's':
+ pPars->fSeqSimulate ^= 1;
+ break;
+ case 'm':
+ pPars->fCheckMiter ^= 1;
+ break;
+ case 'f':
+ pPars->fFirstStop ^= 1;
+ break;
+ case 'd':
+ pPars->fDoubleOuts ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pAig == NULL )
+ {
+ printf( "Abc_CommandAbc9Equiv(): There is no AIG.\n" );
+ return 1;
+ }
+ Cec_ManSimulation( pAbc->pAig, pPars );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: &equiv [-WRT <num>] [-smfdvh]\n" );
+ fprintf( stdout, "\t computes candidate equivalence classes\n" );
+ fprintf( stdout, "\t-W num : the number of words to simulate [default = %d]\n", pPars->nWords );
+ fprintf( stdout, "\t-R num : the number of rounds to simulate [default = %d]\n", pPars->nRounds );
+ fprintf( stdout, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
+ fprintf( stdout, "\t-s : toggle seq vs. comb simulation [default = %s]\n", pPars->fSeqSimulate? "yes": "no" );
+ fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
+ fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
+ fprintf( stdout, "\t-d : toggle using two POs intead of XOR [default = %s]\n", pPars->fDoubleOuts? "yes": "no" );
+ fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Times( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
@@ -22685,6 +22676,119 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pFile;
+ Gia_Man_t * pAux;
+ Gia_Man_t * pSecond;
+ char * FileName, * pTemp;
+ char ** pArgvNew;
+ int nArgcNew;
+ int c;
+ int fXorOuts = 1;
+ int fComb = 1;
+ int fTrans = 0;
+ int fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "xctvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'x':
+ fXorOuts ^= 1;
+ break;
+ case 'c':
+ fComb ^= 1;
+ break;
+ case 't':
+ fTrans ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( fTrans )
+ {
+ if ( (Gia_ManPoNum(pAbc->pAig) & 1) == 1 )
+ {
+ printf( "Abc_CommandAbc9Miter(): The number of outputs should be even.\n" );
+ return 0;
+ }
+ pAbc->pAig = Gia_ManTransformMiter( pAux = pAbc->pAig );
+ Gia_ManStop( pAux );
+ printf( "Abc_CommandAbc9Miter(): Miter is transformed by merging POs pair-wise.\n" );
+ return 0;
+ }
+
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
+ if ( nArgcNew != 1 )
+ {
+ printf( "File name is not given on the command line.\n" );
+ return 1;
+ }
+
+ // get the input file name
+ FileName = pArgvNew[0];
+ // fix the wrong symbol
+ for ( pTemp = FileName; *pTemp; pTemp++ )
+ if ( *pTemp == '>' )
+ *pTemp = '\\';
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+ if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
+ fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+ fprintf( pAbc->Err, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+ pSecond = Gia_ReadAiger( FileName, 0 );
+ if ( pSecond == NULL )
+ {
+ printf( "Reading AIGER has failed.\n" );
+ return 0;
+ }
+ // compute the miter
+ pAbc->pAig = Gia_ManMiter( pAux = pAbc->pAig, pSecond, fXorOuts, fComb, fVerbose );
+ Gia_ManStop( pSecond );
+ if ( pAbc->pAig == NULL )
+ {
+ printf( "Miter construction has failed.\n" );
+ pAbc->pAig = pAux;
+ }
+ else
+ Gia_ManStop( pAux );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: &miter [-xctvh] <file>\n" );
+ fprintf( stdout, "\t creates miter of two designs (current AIG vs. <file>)\n" );
+ fprintf( stdout, "\t-x : toggle creating XOR of output pairs [default = %s]\n", fXorOuts? "yes": "no" );
+ fprintf( stdout, "\t-c : toggle creating combinational miter [default = %s]\n", fComb? "yes": "no" );
+ fprintf( stdout, "\t-t : toggle XORing pair-wise POs of the miter [default = %s]\n", fTrans? "yes": "no" );
+ fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ fprintf( stdout, "\t<file> : AIGER file with the design to miter\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
@@ -22747,7 +22851,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Cec_ManSatSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "CSNfvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CSNmfvh" ) ) != EOF )
{
switch ( c )
{
@@ -22784,6 +22888,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nCallsRecycle < 0 )
goto usage;
break;
+ case 'm':
+ pPars->fCheckMiter ^= 1;
+ break;
case 'f':
pPars->fFirstStop ^= 1;
break;
@@ -22804,12 +22911,13 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( stdout, "usage: &sat [-CSN <num>] [-fvh]\n" );
+ fprintf( stdout, "usage: &sat [-CSN <num>] [-mfvh]\n" );
fprintf( stdout, "\t performs SAT solving for the combinational outputs\n" );
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
- fprintf( stdout, "\t-N num : the max number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
- fprintf( stdout, "\t-f : toggle stopping when an output is satisfiable [default = %s]\n", pPars->fFirstStop? "yes": "no" );
+ fprintf( stdout, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
+ fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
+ fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
@@ -22828,12 +22936,12 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Cec_ParCsw_t ParsCsw, * pPars = &ParsCsw;
+ Cec_ParFra_t ParsFra, * pPars = &ParsFra;
Gia_Man_t * pTemp;
int c;
- Cec_ManCswSetDefaultParams( pPars );
+ Cec_ManFraSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCSNrmwvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCrmfdwvh" ) ) != EOF )
{
switch ( c )
{
@@ -22903,34 +23011,18 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nBTLimit < 0 )
goto usage;
break;
- case 'S':
- if ( globalUtilOptind >= argc )
- {
- fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" );
- goto usage;
- }
- pPars->nSatVarMax = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( pPars->nSatVarMax < 0 )
- goto usage;
- break;
- case 'N':
- if ( globalUtilOptind >= argc )
- {
- fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
- goto usage;
- }
- pPars->nCallsRecycle = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( pPars->nCallsRecycle < 0 )
- goto usage;
- break;
case 'r':
pPars->fRewriting ^= 1;
break;
case 'm':
+ pPars->fCheckMiter ^= 1;
+ break;
+ case 'f':
pPars->fFirstStop ^= 1;
break;
+ case 'd':
+ pPars->fDoubleOuts ^= 1;
+ break;
case 'w':
pPars->fVeryVerbose ^= 1;
break;
@@ -22946,12 +23038,16 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "Abc_CommandAbc9Fraig(): There is no AIG.\n" );
return 1;
}
- pAbc->pAig = Cec_ManSatSweeping( pTemp = pAbc->pAig, pPars );
- Gia_ManStop( pTemp );
+ pTemp = Cec_ManSatSweeping( pAbc->pAig, pPars );
+ if ( pTemp )
+ {
+ Gia_ManStop( pAbc->pAig );
+ pAbc->pAig = pTemp;
+ }
return 0;
usage:
- fprintf( stdout, "usage: &fraig [-WRILDCSN <num>] [-rmwvh]\n" );
+ fprintf( stdout, "usage: &fraig [-WRILDC <num>] [-rmfdwvh]\n" );
fprintf( stdout, "\t performs combinational SAT sweeping\n" );
fprintf( stdout, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
fprintf( stdout, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
@@ -22959,10 +23055,10 @@ usage:
fprintf( stdout, "\t-L num : the max number of levels of nodes to consider [default = %d]\n", pPars->nLevelMax );
fprintf( stdout, "\t-D num : the max number of steps of speculative reduction [default = %d]\n", pPars->nDepthMax );
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
- fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
- fprintf( stdout, "\t-N num : the max number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
fprintf( stdout, "\t-r : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
- fprintf( stdout, "\t-m : toggle stopping when an output is satisfiable [default = %s]\n", pPars->fFirstStop? "yes": "no" );
+ fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
+ fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
+ fprintf( stdout, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDoubleOuts? "yes": "no" );
fprintf( stdout, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
@@ -22980,14 +23076,196 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Gia_Man_t * pTemp;
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pAig == NULL )
+ {
+ printf( "Abc_CommandAbc9Srm(): There is no AIG.\n" );
+ return 1;
+ }
+ pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig );
+ Gia_ManStop( pTemp );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: &srm [-vh]\n" );
+ fprintf( stdout, "\t testing various procedures\n" );
+ fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Cec_ParCec_t ParsCec, * pPars = &ParsCec;
+ FILE * pFile;
+ Gia_Man_t * pSecond, * pMiter;
+ char * FileName, * pTemp;
+ char ** pArgvNew;
+ int c, nArgcNew, fMiter = 0;
+ Cec_ManCecSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "CTmvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBTLimit < 0 )
+ goto usage;
+ break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->TimeLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->TimeLimit < 0 )
+ goto usage;
+ break;
+ case 'm':
+ fMiter ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( fMiter )
+ {
+ printf( "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
+ Cec_ManVerify( pAbc->pAig, pPars );
+ return 0;
+ }
+
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
+ if ( nArgcNew != 1 )
+ {
+ printf( "File name is not given on the command line.\n" );
+ return 1;
+ }
+
+ // get the input file name
+ FileName = pArgvNew[0];
+ // fix the wrong symbol
+ for ( pTemp = FileName; *pTemp; pTemp++ )
+ if ( *pTemp == '>' )
+ *pTemp = '\\';
+ if ( (pFile = fopen( FileName, "r" )) == NULL )
+ {
+ fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+ if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) )
+ fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+ fprintf( pAbc->Err, "\n" );
+ return 1;
+ }
+ fclose( pFile );
+ pSecond = Gia_ReadAiger( FileName, 0 );
+ if ( pSecond == NULL )
+ {
+ printf( "Reading AIGER has failed.\n" );
+ return 0;
+ }
+ // compute the miter
+ pMiter = Gia_ManMiter( pAbc->pAig, pSecond, 0, 1, pPars->fVerbose );
+ if ( pMiter )
+ {
+ Cec_ManVerify( pMiter, pPars );
+ Gia_ManStop( pMiter );
+ }
+ Gia_ManStop( pSecond );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: &cec [-CT num] [-mvh]\n" );
+ fprintf( stdout, "\t new combinational equivalence checker\n" );
+ fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+ fprintf( stdout, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
+ fprintf( stdout, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
+ fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9Force( Abc_Frame_t * pAbc, int argc, char ** argv )
{
+ int nIters = 20;
+ int fClustered = 1;
+ int fVerbose = 1;
int c;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Icvh" ) ) != EOF )
{
switch ( c )
{
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-I\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nIters < 0 )
+ goto usage;
+ break;
+ case 'c':
+ fClustered ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -22996,17 +23274,20 @@ int Abc_CommandAbc9Force( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pAig == NULL )
{
- printf( "Abc_CommandAbc9Test(): There is no AIG.\n" );
+ printf( "Abc_CommandAbc9Force(): There is no AIG.\n" );
return 1;
}
- For_ManExperiment( pAbc->pAig );
+ For_ManExperiment( pAbc->pAig, nIters, fClustered, fVerbose );
return 0;
usage:
- fprintf( stdout, "usage: &force [-h]\n" );
- fprintf( stdout, "\t one-dimensional placement algorithm FORCE introduced by\n" );
- fprintf( stdout, "\t F. A. Aloul, I. L. Markov, and K. A. Sakallah (GLSVLSI’03).\n" );
- fprintf( stdout, "\t-h : print the command usage\n");
+ fprintf( stdout, "usage: &force [-I <num>] [-cvh]\n" );
+ fprintf( stdout, "\t one-dimensional placement algorithm FORCE introduced by\n" );
+ fprintf( stdout, "\t F. A. Aloul, I. L. Markov, and K. A. Sakallah (GLSVLSI’03).\n" );
+ fprintf( stdout, "\t-I num : the number of refinement iterations [default = %d]\n", nIters );
+ fprintf( stdout, "\t-c : toggle clustered representation [default = %s]\n", fClustered? "yes":"no");
+ fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes":"no");
+ fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
@@ -23023,13 +23304,19 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Embed( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- int nDims = 30;
- int fCluster = 0;
- int fDump = 0;
- int fVerbose = 0;
+ Emb_Par_t Pars, * pPars = &Pars;
int c;
+ pPars->nDims = 30;
+ pPars->nIters = 10;
+ pPars->nSols = 2;
+ pPars->fRefine = 0;
+ pPars->fCluster = 0;
+ pPars->fDump = 0;
+ pPars->fDumpLarge = 0;
+ pPars->fShowImage = 0;
+ pPars->fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Ddcvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "DIrcdlsvh" ) ) != EOF )
{
switch ( c )
{
@@ -23039,19 +23326,39 @@ int Abc_CommandAbc9Embed( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
- nDims = atoi(argv[globalUtilOptind]);
+ pPars->nDims = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
- if ( nDims < 0 )
+ if ( pPars->nDims < 0 )
goto usage;
break;
+ case 'I':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nIters < 0 )
+ goto usage;
+ break;
+ case 'r':
+ pPars->fRefine ^= 1;
+ break;
case 'c':
- fCluster ^= 1;
+ pPars->fCluster ^= 1;
break;
case 'd':
- fDump ^= 1;
+ pPars->fDump ^= 1;
+ break;
+ case 'l':
+ pPars->fDumpLarge ^= 1;
+ break;
+ case 's':
+ pPars->fShowImage ^= 1;
break;
case 'v':
- fVerbose ^= 1;
+ pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
@@ -23061,24 +23368,247 @@ int Abc_CommandAbc9Embed( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pAig == NULL )
{
- printf( "Abc_CommandAbc9Test(): There is no AIG.\n" );
+ printf( "Abc_CommandAbc9Embed(): There is no AIG.\n" );
return 1;
}
- Gia_ManSolveProblem( pAbc->pAig, nDims, 2, fCluster, fDump, fVerbose );
+ Gia_ManSolveProblem( pAbc->pAig, pPars );
return 0;
usage:
- fprintf( stdout, "usage: &embed [-D num] [-dcvh]\n" );
+ fprintf( stdout, "usage: &embed [-DI <num>] [-rdlscvh]\n" );
fprintf( stdout, "\t fast placement based on high-dimensional embedding from\n" );
fprintf( stdout, "\t D. Harel and Y. Koren, \"Graph drawing by high-dimensional\n" );
fprintf( stdout, "\t embedding\", J. Graph Algs & Apps, 2004, Vol 8(2), pp. 195-217\n" );
- fprintf( stdout, "\t-D num : the number of dimensions for embedding [default = %d]\n", nDims );
- fprintf( stdout, "\t-d : toggle dumping placement into a Gnuplot file [default = %s]\n", fDump? "yes":"no");
- fprintf( stdout, "\t-c : toggle clustered representation [default = %s]\n", fCluster? "yes":"no");
- fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes":"no");
+ fprintf( stdout, "\t-D num : the number of dimensions for embedding [default = %d]\n", pPars->nDims );
+ fprintf( stdout, "\t-I num : the number of refinement iterations [default = %d]\n", pPars->nIters );
+ fprintf( stdout, "\t-r : toggle the use of refinement [default = %s]\n", pPars->fRefine? "yes":"no");
+ fprintf( stdout, "\t-c : toggle clustered representation [default = %s]\n", pPars->fCluster? "yes":"no");
+ fprintf( stdout, "\t-d : toggle dumping placement into a Gnuplot file [default = %s]\n", pPars->fDump? "yes":"no");
+ fprintf( stdout, "\t-l : toggle dumping Gnuplot for large placement [default = %s]\n", pPars->fDumpLarge? "yes":"no");
+ fprintf( stdout, "\t-s : toggle showing image if Gnuplot is installed [default = %s]\n", pPars->fShowImage? "yes":"no");
+ fprintf( stdout, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ char Buffer[200];
+ char LutSize[200];
+ If_Par_t Pars, * pPars = &Pars;
+ int c;
+ extern void Gia_ManSetIfParsDefault( If_Par_t * pPars );
+ extern int Gia_MappingIf( Gia_Man_t * p, If_Par_t * pPars );
+ if ( pAbc->pAbc8Lib == NULL )
+ {
+ printf( "LUT library is not given. Using default 6-LUT library.\n" );
+ pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
+ }
+ // set defaults
+ Gia_ManSetIfParsDefault( pPars );
+ pPars->pLutLib = pAbc->pAbc8Lib;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEqaflepmrstbvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ pPars->nLutSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLutSize < 0 )
+ goto usage;
+ // if the LUT size is specified, disable library
+ pPars->pLutLib = NULL;
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-C\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ pPars->nCutsMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nCutsMax < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-F\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ pPars->nFlowIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nFlowIters < 0 )
+ goto usage;
+ break;
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-A\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ pPars->nAreaIters = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nAreaIters < 0 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-D\" should be followed by a floating point number.\n" );
+ goto usage;
+ }
+ pPars->DelayTarget = (float)atof(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->DelayTarget <= 0.0 )
+ goto usage;
+ break;
+ case 'E':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-E\" should be followed by a floating point number.\n" );
+ goto usage;
+ }
+ pPars->Epsilon = (float)atof(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->Epsilon < 0.0 || pPars->Epsilon > 1.0 )
+ goto usage;
+ break;
+ case 'q':
+ pPars->fPreprocess ^= 1;
+ break;
+ case 'a':
+ pPars->fArea ^= 1;
+ break;
+ case 'r':
+ pPars->fExpRed ^= 1;
+ break;
+ case 'f':
+ pPars->fFancy ^= 1;
+ break;
+ case 'l':
+ pPars->fLatchPaths ^= 1;
+ break;
+ case 'e':
+ pPars->fEdge ^= 1;
+ break;
+ case 'p':
+ pPars->fPower ^= 1;
+ break;
+ case 'm':
+ pPars->fCutMin ^= 1;
+ break;
+ case 's':
+ pPars->fSeqMap ^= 1;
+ break;
+ case 't':
+ pPars->fLiftLeaves ^= 1;
+ break;
+ case 'b':
+ pPars->fBidec ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pAig == NULL )
+ {
+ printf( "Abc_CommandAbc9If(): There is no AIG to map.\n" );
+ return 1;
+ }
+
+ if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE )
+ {
+ fprintf( stdout, "Incorrect LUT size (%d).\n", pPars->nLutSize );
+ return 1;
+ }
+
+ if ( pPars->nCutsMax < 1 || pPars->nCutsMax >= (1<<12) )
+ {
+ fprintf( stdout, "Incorrect number of cuts.\n" );
+ return 1;
+ }
+/*
+ // enable truth table computation if choices are selected
+ if ( (c = Aig_ManChoiceNum( pAbc->pAbc8Aig )) )
+ {
+ printf( "Performing LUT mapping with %d choices.\n", c );
+ pPars->fExpRed = 0;
+ }
+*/
+ // enable truth table computation if cut minimization is selected
+ if ( pPars->fCutMin )
+ {
+ pPars->fTruth = 1;
+ pPars->fExpRed = 0;
+ }
+
+ // complain if truth tables are requested but the cut size is too large
+ if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
+ {
+ fprintf( stdout, "Truth tables cannot be computed for LUT larger than %d inputs.\n", IF_MAX_FUNC_LUTSIZE );
+ return 1;
+ }
+
+ if ( !Gia_MappingIf( pAbc->pAig, pPars ) )
+ {
+ printf( "Abc_CommandAbc9If(): Mapping of the AIG has failed.\n" );
+ return 1;
+ }
+ return 0;
+
+usage:
+ if ( pPars->DelayTarget == -1 )
+ sprintf( Buffer, "best possible" );
+ else
+ sprintf( Buffer, "%.2f", pPars->DelayTarget );
+ if ( pPars->nLutSize == -1 )
+ sprintf( LutSize, "library" );
+ else
+ sprintf( LutSize, "%d", pPars->nLutSize );
+ fprintf( stdout, "usage: &if [-KCFA num] [-DE float] [-qarlepmbvh]\n" );
+ fprintf( stdout, "\t performs FPGA technology mapping of the network\n" );
+ fprintf( stdout, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
+ fprintf( stdout, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
+ fprintf( stdout, "\t-F num : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters );
+ fprintf( stdout, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters );
+ fprintf( stdout, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );
+ fprintf( stdout, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->Epsilon );
+ fprintf( stdout, "\t-q : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
+ fprintf( stdout, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
+// fprintf( stdout, "\t-f : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
+ fprintf( stdout, "\t-r : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
+ fprintf( stdout, "\t-l : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
+ fprintf( stdout, "\t-e : uses edge-based cut selection heuristics [default = %s]\n", pPars->fEdge? "yes": "no" );
+ fprintf( stdout, "\t-p : uses power-aware cut selection heuristics [default = %s]\n", pPars->fPower? "yes": "no" );
+ fprintf( stdout, "\t-m : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
+// fprintf( stdout, "\t-s : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" );
+// fprintf( stdout, "\t-t : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
+ fprintf( stdout, "\t-b : toggles deriving local AIGs using bi-decomposition [default = %s]\n", pPars->fBidec? "yes": "no" );
+ fprintf( stdout, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : prints the command usage\n");
+ return 1;
+}
/**Function*************************************************************
@@ -23093,14 +23623,18 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- int c;
+ Gia_Man_t * pTemp = NULL;
+ int c, fVerbose = 0;
extern void Gia_SatSolveTest( Gia_Man_t * p );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
+ case 'v':
+ fVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -23116,19 +23650,18 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ManReduceConst( pAbc->pAig, 1 );
// Sat_ManTest( pAbc->pAig, Gia_ManCo(pAbc->pAig, 0), 0 );
// Gia_ManTestDistance( pAbc->pAig );
-// For_ManExperiment( pAbc->pAig );
- Gia_ManSolveProblem( pAbc->pAig, 30, 2, 1, 0, 1 );
// Gia_SatSolveTest( pAbc->pAig );
+// For_ManExperiment( pAbc->pAig, 20, 1, 1 );
return 0;
usage:
- fprintf( stdout, "usage: &test [-h]\n" );
+ fprintf( stdout, "usage: &test [-vh]\n" );
fprintf( stdout, "\t testing various procedures\n" );
+ fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
-
/**Function*************************************************************
Synopsis []
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index dbd461c4..ca33667f 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -702,35 +702,6 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarSatSweep( Abc_Ntk_t * pNtk, Cec_ParCsw_t * pPars )
-{
-/*
- extern Aig_Man_t * Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars );
- Abc_Ntk_t * pNtkAig;
- Aig_Man_t * pMan, * pTemp;
- pMan = Abc_NtkToDar( pNtk, 0, 0 );
- if ( pMan == NULL )
- return NULL;
- pMan = Cec_ManSatSweep( pTemp = pMan, pPars );
- Aig_ManStop( pTemp );
- pNtkAig = Abc_NtkFromDar( pNtk, pMan );
- Aig_ManStop( pMan );
- return pNtkAig;
- */
- return NULL;
-}
-
-/**Function*************************************************************
-
- Synopsis [Gives the current ABC network to AIG manager for processing.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
@@ -1184,7 +1155,17 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPa
Aig_Man_t * pMan, * pMan1, * pMan2;
Abc_Ntk_t * pMiter;
int RetValue, clkTotal = clock();
-
+/*
+ {
+ extern void Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose );
+ Aig_Man_t * pAig0 = Abc_NtkToDar( pNtk1, 0, 0 );
+ Aig_Man_t * pAig1 = Abc_NtkToDar( pNtk2, 0, 0 );
+ Cec_ManVerifyTwoAigs( pAig0, pAig1, 1 );
+ Aig_ManStop( pAig0 );
+ Aig_ManStop( pAig1 );
+ return 1;
+ }
+*/
// cannot partition if it is already a miter
if ( pNtk2 == NULL && fPartition == 1 )
{
@@ -1285,82 +1266,6 @@ ABC_PRT( "Time", clock() - clkTotal );
SeeAlso []
***********************************************************************/
-int Abc_NtkDarCec2( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Cec_ParCec_t * pPars )
-{
- Aig_Man_t * pMan1, * pMan2 = NULL;
- int RetValue, clkTotal = clock();
- if ( pNtk2 )
- {
- if ( Abc_NtkPiNum(pNtk1) != Abc_NtkPiNum(pNtk2) )
- {
- printf( "Networks have different number of PIs.\n" );
- return -1;
- }
- if ( Abc_NtkPoNum(pNtk1) != Abc_NtkPoNum(pNtk2) )
- {
- printf( "Networks have different number of POs.\n" );
- return -1;
- }
- }
- if ( pNtk1 )
- {
- pMan1 = Abc_NtkToDar( pNtk1, 0, 0 );
- if ( pMan1 == NULL )
- {
- printf( "Converting into AIG has failed.\n" );
- return -1;
- }
- }
- if ( pNtk2 )
- {
- pMan2 = Abc_NtkToDar( pNtk2, 0, 0 );
- if ( pMan2 == NULL )
- {
- Aig_ManStop( pMan1 );
- printf( "Converting into AIG has failed.\n" );
- return -1;
- }
- }
- // perform verification
-// RetValue = Cec_Solve( pMan1, pMan2, pPars );
- RetValue = -1;
- // transfer model if given
- pNtk1->pModel = pMan1->pData, pMan1->pData = NULL;
- Aig_ManStop( pMan1 );
- if ( pMan2 )
- Aig_ManStop( pMan2 );
-
- // report the miter
- if ( RetValue == 1 )
- {
- printf( "Networks are equivalent. " );
-ABC_PRT( "Time", clock() - clkTotal );
- }
- else if ( RetValue == 0 )
- {
- printf( "Networks are NOT EQUIVALENT. " );
-ABC_PRT( "Time", clock() - clkTotal );
- }
- else
- {
- printf( "Networks are UNDECIDED. " );
-ABC_PRT( "Time", clock() - clkTotal );
- }
- fflush( stdout );
- return RetValue;
-}
-
-/**Function*************************************************************
-
- Synopsis [Gives the current ABC network to AIG manager for processing.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars )
{
Fraig_Params_t Params;
@@ -1797,8 +1702,8 @@ int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
Aig_ManStop( pPart1 );
Aig_ManStop( pMan );
return 1;
-}
-
+}
+
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
@@ -1826,6 +1731,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
Abc_NtkMakeComb( pNtkComb, 1 );
// solve it using combinational equivalence checking
Prove_ParamsSetDefault( pParams );
+ pParams->fVerbose = 1;
RetValue = Abc_NtkIvyProve( &pNtkComb, pParams );
// transfer model if given
// pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL;
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 7f3d2071..796a51a4 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -161,7 +161,8 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
int i, nNodesDsd;
// save the CI nodes in the DSD nodes
- Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)(ABC_PTRINT_T)Abc_NtkCreateNodeConst1(pNtkNew) );
+ Abc_AigConst1(pNtk)->pCopy = pNodeNew = Abc_NtkCreateNodeConst1(pNtkNew);
+ Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)(ABC_PTRINT_T)pNodeNew );
Abc_NtkForEachCi( pNtk, pNode, i )
{
pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c
new file mode 100644
index 00000000..6906e2c4
--- /dev/null
+++ b/src/base/abci/abcLutmin.c
@@ -0,0 +1,209 @@
+/**CFile****************************************************************
+
+ FileName [abcLutmin.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Minimization of the number of LUTs.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcLutmin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Converts the node to MUXes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkCreateNodeLut( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc, Abc_Obj_t * pNode, int nLutSize )
+{
+ DdNode * bFuncNew;
+ Abc_Obj_t * pNodeNew;
+ int i, nStart = ABC_MIN( 0, Abc_ObjFaninNum(pNode) - nLutSize );
+ // create a new node
+ pNodeNew = Abc_NtkCreateNode( pNtkNew );
+ // add the fanins in the order, in which they appear in the reordered manager
+ for ( i = nStart; i < Abc_ObjFaninNum(pNode); i++ )
+ Abc_ObjAddFanin( pNodeNew, Abc_ObjFanin(pNode, i)->pCopy );
+ // transfer the function
+ bFuncNew = Extra_bddMove( dd, bFunc, nStart ); Cudd_Ref( bFuncNew );
+ assert( Cudd_SupportSize(dd, bFuncNew) <= nLutSize );
+ pNodeNew->pData = Extra_TransferLevelByLevel( dd, pNtkNew->pManFunc, bFuncNew ); Cudd_Ref( pNodeNew->pData );
+ Cudd_RecursiveDeref( dd, bFuncNew );
+ return pNodeNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the node to MUXes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeBddToMuxesLut_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node, Abc_Obj_t * pNode, int nLutSize )
+{
+ Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
+ assert( !Cudd_IsComplement(bFunc) );
+ if ( bFunc == b1 )
+ return Abc_NtkCreateNodeConst1(pNtkNew);
+ if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
+ return pNodeNew;
+ if ( dd->perm[bFunc->index] >= Abc_ObjFaninNum(pNode) - nLutSize )
+ {
+ pNodeNew = Abc_NtkCreateNodeLut( pNtkNew, dd, bFunc, pNode, nLutSize );
+ st_insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew );
+ return pNodeNew;
+ }
+ // solve for the children nodes
+ pNodeNew0 = Abc_NodeBddToMuxesLut_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node, pNode, nLutSize );
+ if ( Cudd_IsComplement(cuddE(bFunc)) )
+ pNodeNew0 = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew0 );
+ pNodeNew1 = Abc_NodeBddToMuxesLut_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node, pNode, nLutSize );
+ if ( !st_lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) )
+ assert( 0 );
+ // create the MUX node
+ pNodeNew = Abc_NtkCreateNodeMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
+ st_insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew );
+ return pNodeNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the node to MUXes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeBddToMuxesLut( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, int nLutSize )
+{
+ DdManager * dd = pNodeOld->pNtk->pManFunc;
+ DdNode * bFunc = pNodeOld->pData;
+ Abc_Obj_t * pFaninOld, * pNodeNew;
+ st_table * tBdd2Node;
+ int i;
+ // create the table mapping BDD nodes into the ABC nodes
+ tBdd2Node = st_init_table( st_ptrcmp, st_ptrhash );
+ // add the constant and the elementary vars
+ Abc_ObjForEachFanin( pNodeOld, pFaninOld, i )
+ st_insert( tBdd2Node, (char *)Cudd_bddIthVar(dd, i), (char *)pFaninOld->pCopy );
+ // create the new nodes recursively
+ pNodeNew = Abc_NodeBddToMuxesLut_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node, pNodeOld, nLutSize );
+ st_free_table( tBdd2Node );
+ if ( Cudd_IsComplement(bFunc) )
+ pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew );
+ return pNodeNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkLutminConstruct( Abc_Ntk_t * pNtkClp, Abc_Ntk_t * pNtkDec, int nLutSize )
+{
+ Abc_Obj_t * pObj, * pDriver;
+ int i;
+ Abc_NtkForEachCo( pNtkClp, pObj, i )
+ {
+ pDriver = Abc_ObjFanin0( pObj );
+ if ( !Abc_ObjIsNode(pDriver) )
+ continue;
+ if ( Abc_ObjFaninNum(pDriver) == 0 )
+ pDriver->pCopy = Abc_NtkDupObj( pNtkDec, pDriver, 0 );
+ else
+ pDriver->pCopy = Abc_NodeBddToMuxesLut( pNtkDec, pDriver, nLutSize );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkLutmin( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose )
+{
+ extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
+ Abc_Ntk_t * pNtkDec, * pNtkClp, * pTemp;
+ // collapse the network and reorder BDDs
+ if ( Abc_NtkIsStrash(pNtk) )
+ pTemp = Abc_NtkDup( pNtk );
+ else
+ pTemp = Abc_NtkStrash( pNtk, 0, 1, 0 );
+ pNtkClp = Abc_NtkCollapse( pTemp, 10000, 0, 1, 0 );
+ Abc_NtkDelete( pTemp );
+ if ( pNtkClp == NULL )
+ return NULL;
+ if ( !Abc_NtkIsBddLogic(pNtkClp) )
+ Abc_NtkToBdd( pNtkClp );
+ Abc_NtkBddReorder( pNtkClp, fVerbose );
+ // decompose one output at a time
+ pNtkDec = Abc_NtkStartFrom( pNtkClp, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+ // make sure the new manager has enough inputs
+ Cudd_bddIthVar( pNtkDec->pManFunc, nLutSize );
+ // put the results into the new network (save new CO drivers in old CO drivers)
+ Abc_NtkLutminConstruct( pNtkClp, pNtkDec, nLutSize );
+ // finalize the new network
+ Abc_NtkFinalize( pNtkClp, pNtkDec );
+ Abc_NtkDelete( pNtkClp );
+ // make the network minimum base
+ Abc_NtkMinimumBase( pNtkDec );
+ // fix the problem with complemented and duplicated CO edges
+ Abc_NtkLogicMakeSimpleCos( pNtkDec, 0 );
+ // make sure everything is okay
+ if ( !Abc_NtkCheck( pNtkDec ) )
+ {
+ printf( "Abc_NtkLutmin: The network check has failed.\n" );
+ return 0;
+ }
+ return pNtkDec;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index e520dcce..9214bb52 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -24,6 +24,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcIf.c \
src/base/abci/abcIvy.c \
src/base/abci/abcLut.c \
+ src/base/abci/abcLutmin.c \
src/base/abci/abcMap.c \
src/base/abci/abcMerge.c \
src/base/abci/abcMini.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-19 22:44:37 +0000