summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abcBlifMv.zipbin6552 -> 0 bytes
-rw-r--r--src/base/abc/abcFanio.c6
-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
-rw-r--r--src/base/cmd/cmd.c67
-rw-r--r--src/base/io/io.c106
-rw-r--r--src/base/io/ioAbc.h5
-rw-r--r--src/base/io/ioReadAiger.c14
-rw-r--r--src/base/io/ioReadBblif.c342
-rw-r--r--src/base/io/ioUtil.c22
-rw-r--r--src/base/io/ioWriteAiger.c6
-rw-r--r--src/base/io/ioWriteBblif.c111
-rw-r--r--src/base/io/module.make2
-rw-r--r--src/base/ver/verCore.c13
-rw-r--r--src/base/ver/verParse.c9
18 files changed, 1829 insertions, 504 deletions
diff --git a/src/base/abc/abcBlifMv.zip b/src/base/abc/abcBlifMv.zip
deleted file mode 100644
index 4a4d080a..00000000
--- a/src/base/abc/abcBlifMv.zip
+++ /dev/null
Binary files differ
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index fb8dcaae..6c75cf3f 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -92,6 +92,12 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
{
printf( "Abc_ObjAddFanin(): Error! Creating net \"%s\" with two fanins.\n", Abc_ObjName(pObj) );
}
+/*
+ if ( Abc_ObjIsCo(pFanin) )
+ {
+ printf( "Abc_ObjAddFanin(): Error! Creating fanout of a CO.\n", Abc_ObjName(pFanin) );
+ }
+*/
}
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 \
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 21853e9a..398415ae 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1737,6 +1737,73 @@ usage:
}
+/**Function*************************************************************
+
+ Synopsis [Computes dimentions of the graph.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Gia_ManGnuplotShow( char * pPlotFileName )
+{
+ FILE * pFile;
+ void * pAbc;
+ char * pProgNameGnuplotWin = "wgnuplot.exe";
+ char * pProgNameGnuplotUnix = "gnuplot";
+ char * pProgNameGnuplot;
+
+ // read in the Capo plotting output
+ if ( (pFile = fopen( pPlotFileName, "r" )) == NULL )
+ {
+ fprintf( stdout, "Cannot open the plot file \"%s\".\n\n", pPlotFileName );
+ return;
+ }
+ fclose( pFile );
+
+ pAbc = Abc_FrameGetGlobalFrame();
+
+ // get the names from the plotting software
+ if ( Cmd_FlagReadByName(pAbc, "gnuplotwin") )
+ pProgNameGnuplotWin = Cmd_FlagReadByName(pAbc, "gnuplotwin");
+ if ( Cmd_FlagReadByName(pAbc, "gnuplotunix") )
+ pProgNameGnuplotUnix = Cmd_FlagReadByName(pAbc, "gnuplotunix");
+
+ // check if Gnuplot is available
+ if ( (pFile = fopen( pProgNameGnuplotWin, "r" )) )
+ pProgNameGnuplot = pProgNameGnuplotWin;
+ else if ( (pFile = fopen( pProgNameGnuplotUnix, "r" )) )
+ pProgNameGnuplot = pProgNameGnuplotUnix;
+ else if ( pFile == NULL )
+ {
+ fprintf( stdout, "Cannot find \"%s\" or \"%s\" in the current directory.\n", pProgNameGnuplotWin, pProgNameGnuplotUnix );
+ return;
+ }
+ fclose( pFile );
+
+ // spawn the viewer
+#ifdef WIN32
+ if ( _spawnl( _P_NOWAIT, pProgNameGnuplot, pProgNameGnuplot, pPlotFileName, NULL ) == -1 )
+ {
+ fprintf( stdout, "Cannot find \"%s\".\n", pProgNameGnuplot );
+ return;
+ }
+#else
+ {
+ char Command[1000];
+ sprintf( Command, "%s %s ", pProgNameGnuplot, pPlotFileName );
+ if ( system( Command ) == -1 )
+ {
+ fprintf( stdout, "Cannot execute \"%s\".\n", Command );
+ return;
+ }
+ }
+#endif
+}
+
/**Function********************************************************************
Synopsis [Calls Capo internally.]
diff --git a/src/base/io/io.c b/src/base/io/io.c
index ee5df414..e8af161e 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -28,6 +28,7 @@
static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadBblif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -45,6 +46,7 @@ static int IoCommandWrite ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteHie ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteBblif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -83,6 +85,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read", IoCommandRead, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_aiger", IoCommandReadAiger, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_baf", IoCommandReadBaf, 1 );
+ Cmd_CommandAdd( pAbc, "I/O", "read_bblif", IoCommandReadBblif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlifMv, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
@@ -100,6 +103,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "write_hie", IoCommandWriteHie, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_aiger", IoCommandWriteAiger, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_baf", IoCommandWriteBaf, 0 );
+ Cmd_CommandAdd( pAbc, "I/O", "write_bblif", IoCommandWriteBblif, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_blif_mv", IoCommandWriteBlifMv, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
@@ -316,6 +320,60 @@ usage:
SeeAlso []
***********************************************************************/
+int IoCommandReadBblif( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk;
+ char * pFileName;
+ int fCheck;
+ int c;
+
+ fCheck = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'c':
+ fCheck ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( argc != globalUtilOptind + 1 )
+ goto usage;
+ // get the input file name
+ pFileName = argv[globalUtilOptind];
+ // read the file using the corresponding file reader
+ pNtk = Io_Read( pFileName, IO_FILE_BBLIF, fCheck );
+ if ( pNtk == NULL )
+ return 1;
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: read_bblif [-ch] <file>\n" );
+ fprintf( pAbc->Err, "\t read the network in a binary BLIF format\n" );
+ fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
+ fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
+ fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
@@ -1329,6 +1387,54 @@ usage:
SeeAlso []
***********************************************************************/
+int IoCommandWriteBblif( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+ char * pFileName;
+ int c;
+
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pNtkCur == NULL )
+ {
+ fprintf( pAbc->Out, "Empty network.\n" );
+ return 0;
+ }
+ if ( argc != globalUtilOptind + 1 )
+ goto usage;
+ // get the output file name
+ pFileName = argv[globalUtilOptind];
+ // call the corresponding file writer
+ Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BBLIF );
+ return 0;
+
+usage:
+ fprintf( pAbc->Err, "usage: write_bblif [-h] <file>\n" );
+ fprintf( pAbc->Err, "\t write the network into a binary BLIF file\n" );
+ fprintf( pAbc->Err, "\t-h : print the help massage\n" );
+ fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bblif)\n" );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
{
char * pFileName;
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index c11168df..bade17df 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -44,6 +44,7 @@ typedef enum {
IO_FILE_NONE = 0,
IO_FILE_AIGER,
IO_FILE_BAF,
+ IO_FILE_BBLIF,
IO_FILE_BLIF,
IO_FILE_BLIFMV,
IO_FILE_BENCH,
@@ -73,6 +74,8 @@ typedef enum {
extern Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck );
/*=== abcReadBaf.c ============================================================*/
extern Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck );
+/*=== abcReadBblif.c ============================================================*/
+extern Abc_Ntk_t * Io_ReadBblif( char * pFileName, int fCheck );
/*=== abcReadBlif.c ===========================================================*/
extern Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck );
/*=== abcReadBlifMv.c =========================================================*/
@@ -91,6 +94,8 @@ extern Abc_Ntk_t * Io_ReadVerilog( char * pFileName, int fCheck );
extern void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact );
/*=== abcWriteBaf.c ===========================================================*/
extern void Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
+/*=== abcWriteBblif.c ===========================================================*/
+extern void Io_WriteBblif( Abc_Ntk_t * pNtk, char * pFileName );
/*=== abcWriteBlif.c ==========================================================*/
extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 2c37e210..c26e4cd5 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -463,19 +463,19 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
}
// read the name of the model if given
- if ( *pCur == 'c' && pCur < pContents + nFileSize )
+ pCur = pSymbols;
+ if ( pCur + 1 < pContents + nFileSize && *pCur == 'c' )
{
- if ( !strncmp( pCur + 2, ".model", 6 ) )
+ pCur++;
+ if ( *pCur == 'n' )
{
- char * pTemp;
- for ( pTemp = pCur + 9; *pTemp && *pTemp != '\n'; pTemp++ );
- *pTemp = 0;
+ pCur++;
+ // read model name
ABC_FREE( pNtkNew->pName );
- pNtkNew->pName = Extra_UtilStrsav( pCur + 9 );
+ pNtkNew->pName = Extra_UtilStrsav( pCur );
}
}
-
// skipping the comments
ABC_FREE( pContents );
Vec_PtrFree( vNodes );
diff --git a/src/base/io/ioReadBblif.c b/src/base/io/ioReadBblif.c
new file mode 100644
index 00000000..84ef1e29
--- /dev/null
+++ b/src/base/io/ioReadBblif.c
@@ -0,0 +1,342 @@
+/**CFile****************************************************************
+
+ FileName [ioReadBblif.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to read AIG in the binary format.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioReadBblif.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ioAbc.h"
+#include "dec.h"
+#include "bblif.h"
+
+// For description of Binary BLIF format, refer to "abc/src/aig/bbl/bblif.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Fnction*************************************************************
+
+ Synopsis [Constructs ABC network from the manager.]
+
+ Description [The ABC network is started, as well as the array vCopy,
+ which will map the new ID of each object in the BBLIF manager into
+ the ponter ot the corresponding object in the ABC. For each internal
+ node, determined by Bbl_ObjIsLut(), the SOP representation is created
+ by retrieving the SOP representation of the BBLIF object. Finally,
+ the objects are connected using fanin/fanout creation, and the dummy
+ names are assigned because ABC requires each CI/CO to have a name.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Bbl_ManToAbc( Bbl_Man_t * p )
+{
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pObjNew;
+ Bbl_Obj_t * pObj, * pFanin;
+ Vec_Ptr_t * vCopy;
+ // start the network
+ pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
+ pNtk->pName = Extra_UtilStrsav( Bbl_ManName(p) );
+ // create objects
+ vCopy = Vec_PtrStart( 1000 );
+ Bbl_ManForEachObj( p, pObj )
+ {
+ if ( Bbl_ObjIsInput(pObj) )
+ pObjNew = Abc_NtkCreatePi( pNtk );
+ else if ( Bbl_ObjIsOutput(pObj) )
+ pObjNew = Abc_NtkCreatePo( pNtk );
+ else if ( Bbl_ObjIsLut(pObj) )
+ pObjNew = Abc_NtkCreateNode( pNtk );
+ else assert( 0 );
+ if ( Bbl_ObjIsLut(pObj) )
+ pObjNew->pData = Abc_SopRegister( pNtk->pManFunc, Bbl_ObjSop(p, pObj) );
+ Vec_PtrSetEntry( vCopy, Bbl_ObjId(pObj), pObjNew );
+ }
+ // connect objects
+ Bbl_ManForEachObj( p, pObj )
+ Bbl_ObjForEachFanin( pObj, pFanin )
+ Abc_ObjAddFanin( Vec_PtrEntry(vCopy, Bbl_ObjId(pObj)), Vec_PtrEntry(vCopy, Bbl_ObjId(pFanin)) );
+ // finalize
+ Vec_PtrFree( vCopy );
+ Abc_NtkAddDummyPiNames( pNtk );
+ Abc_NtkAddDummyPoNames( pNtk );
+ if ( !Abc_NtkCheck( pNtk ) )
+ printf( "Bbl_ManToAbc(): Network check has failed.\n" );
+ return pNtk;
+}
+
+/**Fnction*************************************************************
+
+ Synopsis [Collects internal nodes in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bbl_ManDfs_rec( Bbl_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+ extern void Bbl_ObjMark( Bbl_Obj_t * p );
+ extern int Bbl_ObjIsMarked( Bbl_Obj_t * p );
+ Bbl_Obj_t * pFanin;
+ if ( Bbl_ObjIsMarked(pObj) || Bbl_ObjIsInput(pObj) )
+ return;
+ Bbl_ObjForEachFanin( pObj, pFanin )
+ Bbl_ManDfs_rec( pFanin, vNodes );
+ assert( !Bbl_ObjIsMarked(pObj) ); // checks if acyclic
+ Bbl_ObjMark( pObj );
+ Vec_PtrPush( vNodes, pObj );
+}
+
+/**Fnction*************************************************************
+
+ Synopsis [Collects internal nodes in the DFS order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Bbl_ManDfs( Bbl_Man_t * p )
+{
+ Vec_Ptr_t * vNodes;
+ Bbl_Obj_t * pObj;
+ vNodes = Vec_PtrAlloc( 1000 );
+ Bbl_ManForEachObj( p, pObj )
+ if ( Bbl_ObjIsLut(pObj) )
+ Bbl_ManDfs_rec( pObj, vNodes );
+ return vNodes;
+}
+
+/**Fnction*************************************************************
+
+ Synopsis [Constructs AIG in ABC from the manager.]
+
+ Description [The ABC network is started, as well as the array vCopy,
+ which will map the new ID of each object in the BBLIF manager into
+ the ponter ot the corresponding AIG object in the ABC. For each internal
+ node in a topological oder the AIG representation is created
+ by factoring the SOP representation of the BBLIF object. Finally,
+ the CO objects are created, and the dummy names are assigned because
+ ABC requires each CI/CO to have a name.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Bbl_ManToAig( Bbl_Man_t * p )
+{
+ extern int Bbl_ManFncSize( Bbl_Man_t * p );
+ extern int Bbl_ObjFncHandle( Bbl_Obj_t * p );
+ extern Abc_Obj_t * Dec_GraphToAig( Abc_Ntk_t * pNtk, Dec_Graph_t * pFForm, Vec_Ptr_t * vFaninAigs );
+ int fVerbose = 0;
+ Abc_Ntk_t * pNtk;
+ Abc_Obj_t * pObjNew;
+ Bbl_Obj_t * pObj, * pFanin;
+ Vec_Ptr_t * vCopy, * vNodes, * vFaninAigs;
+ Dec_Graph_t ** pFForms;
+ int i, clk;
+clk = clock();
+ // map SOP handles into factored forms
+ pFForms = ABC_CALLOC( Dec_Graph_t *, Bbl_ManFncSize(p) );
+ Bbl_ManForEachObj( p, pObj )
+ if ( pFForms[Bbl_ObjFncHandle(pObj)] == NULL )
+ pFForms[Bbl_ObjFncHandle(pObj)] = Dec_Factor( Bbl_ObjSop(p, pObj) );
+if ( fVerbose )
+ABC_PRT( "Fct", clock() - clk );
+ // start the network
+ pNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+ pNtk->pName = Extra_UtilStrsav( Bbl_ManName(p) );
+ vCopy = Vec_PtrStart( 1000 );
+ // create CIs
+ Bbl_ManForEachObj( p, pObj )
+ {
+ if ( !Bbl_ObjIsInput(pObj) )
+ continue;
+ Vec_PtrSetEntry( vCopy, Bbl_ObjId(pObj), Abc_NtkCreatePi(pNtk) );
+ }
+clk = clock();
+ // create internal nodes
+ vNodes = Bbl_ManDfs( p );
+ vFaninAigs = Vec_PtrAlloc( 100 );
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ // collect fanin AIGs
+ Vec_PtrClear( vFaninAigs );
+ Bbl_ObjForEachFanin( pObj, pFanin )
+ Vec_PtrPush( vFaninAigs, Vec_PtrEntry( vCopy, Bbl_ObjId(pFanin) ) );
+ // create the new node
+ pObjNew = Dec_GraphToAig( pNtk, pFForms[Bbl_ObjFncHandle(pObj)], vFaninAigs );
+ Vec_PtrSetEntry( vCopy, Bbl_ObjId(pObj), pObjNew );
+ }
+ Vec_PtrFree( vFaninAigs );
+ Vec_PtrFree( vNodes );
+if ( fVerbose )
+ABC_PRT( "AIG", clock() - clk );
+ // create COs
+ Bbl_ManForEachObj( p, pObj )
+ {
+ if ( !Bbl_ObjIsOutput(pObj) )
+ continue;
+ pObjNew = Vec_PtrEntry( vCopy, Bbl_ObjId(Bbl_ObjFaninFirst(pObj)) );
+ Abc_ObjAddFanin( Abc_NtkCreatePo(pNtk), pObjNew );
+ }
+ Abc_AigCleanup( pNtk->pManFunc );
+ // clear factored forms
+ for ( i = Bbl_ManFncSize(p) - 1; i >= 0; i-- )
+ if ( pFForms[i] )
+ Dec_GraphFree( pFForms[i] );
+ ABC_FREE( pFForms );
+ // finalize
+clk = clock();
+ Vec_PtrFree( vCopy );
+ Abc_NtkAddDummyPiNames( pNtk );
+ Abc_NtkAddDummyPoNames( pNtk );
+if ( fVerbose )
+ABC_PRT( "Nam", clock() - clk );
+// if ( !Abc_NtkCheck( pNtk ) )
+// printf( "Bbl_ManToAig(): Network check has failed.\n" );
+ return pNtk;
+}
+
+/**Fnction*************************************************************
+
+ Synopsis [Verifies equivalence for two combinational networks.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bbl_ManVerify( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+{
+ extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
+ Abc_Ntk_t * pAig1, * pAig2;
+ pAig1 = Abc_NtkStrash( pNtk1, 0, 1, 0 );
+ pAig2 = Abc_NtkStrash( pNtk2, 0, 1, 0 );
+ Abc_NtkShortNames( pAig1 );
+ Abc_NtkShortNames( pAig2 );
+ Abc_NtkCecFraig( pAig1, pAig2, 0, 0 );
+ Abc_NtkDelete( pAig1 );
+ Abc_NtkDelete( pAig2 );
+}
+
+/**Fnction*************************************************************
+
+ Synopsis [Performs testing of the new manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bbl_ManTest( Abc_Ntk_t * pNtk )
+{
+ extern Bbl_Man_t * Bbl_ManFromAbc( Abc_Ntk_t * pNtk );
+
+ Abc_Ntk_t * pNtkNew;
+ Bbl_Man_t * p, * pNew;
+ char * pFileName = "test.bblif";
+ int clk, clk1, clk2, clk3, clk4, clk5;
+clk = clock();
+ p = Bbl_ManFromAbc( pNtk );
+ Bbl_ManPrintStats( p );
+clk1 = clock() - clk;
+//Bbl_ManDumpBlif( p, "test_bbl.blif" );
+
+ // write into file and back
+clk = clock();
+ Bbl_ManDumpBinaryBlif( p, pFileName );
+clk2 = clock() - clk;
+
+ // read from file
+clk = clock();
+ pNew = Bbl_ManReadBinaryBlif( pFileName );
+ Bbl_ManStop( p ); p = pNew;
+clk3 = clock() - clk;
+
+ // generate ABC network
+clk = clock();
+ pNtkNew = Bbl_ManToAig( p );
+// pNtkNew = Bbl_ManToAbc( p );
+ Bbl_ManStop( p );
+clk4 = clock() - clk;
+
+ // equivalence check
+clk = clock();
+// Bbl_ManVerify( pNtk, pNtkNew );
+ Abc_NtkDelete( pNtkNew );
+clk5 = clock() - clk;
+
+printf( "Runtime stats:\n" );
+ABC_PRT( "ABC to Man", clk1 );
+ABC_PRT( "Writing ", clk2 );
+ABC_PRT( "Reading ", clk3 );
+ABC_PRT( "Man to ABC", clk4 );
+ABC_PRT( "Verify ", clk5 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Reads the AIG in the binary format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Io_ReadBblif( char * pFileName, int fCheck )
+{
+ Bbl_Man_t * p;
+ Abc_Ntk_t * pNtkNew;
+ // read the file
+ p = Bbl_ManReadBinaryBlif( pFileName );
+ pNtkNew = Bbl_ManToAig( p );
+ Bbl_ManStop( p );
+ // check the result
+ if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
+ {
+ printf( "Io_ReadBaf: The network check has failed.\n" );
+ Abc_NtkDelete( pNtkNew );
+ return NULL;
+ }
+ return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index c67c183d..c00c3008 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -51,6 +51,8 @@ Io_FileType_t Io_ReadFileType( char * pFileName )
return IO_FILE_AIGER;
if ( !strcmp( pExt, "baf" ) )
return IO_FILE_BAF;
+ if ( !strcmp( pExt, "bblif" ) )
+ return IO_FILE_BBLIF;
if ( !strcmp( pExt, "blif" ) )
return IO_FILE_BLIF;
if ( !strcmp( pExt, "bench" ) )
@@ -108,12 +110,14 @@ Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck
}
fclose( pFile );
// read the AIG
- if ( FileType == IO_FILE_AIGER || FileType == IO_FILE_BAF )
+ if ( FileType == IO_FILE_AIGER || FileType == IO_FILE_BAF || FileType == IO_FILE_BBLIF )
{
if ( FileType == IO_FILE_AIGER )
pNtk = Io_ReadAiger( pFileName, fCheck );
- else // if ( FileType == IO_FILE_BAF )
+ else if ( FileType == IO_FILE_BAF )
pNtk = Io_ReadBaf( pFileName, fCheck );
+ else // if ( FileType == IO_FILE_BBLIF )
+ pNtk = Io_ReadBblif( pFileName, fCheck );
if ( pNtk == NULL )
{
fprintf( stdout, "Reading AIG from file has failed.\n" );
@@ -258,7 +262,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
}
if ( FileType == IO_FILE_AIGER )
Io_WriteAiger( pNtk, pFileName, 1, 0 );
- else // if ( FileType == IO_FILE_BAF )
+ else //if ( FileType == IO_FILE_BAF )
Io_WriteBaf( pNtk, pFileName );
return;
}
@@ -278,6 +282,18 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
Io_WriteGml( pNtk, pFileName );
return;
}
+ if ( FileType == IO_FILE_BBLIF )
+ {
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ fprintf( stdout, "Writing Binary BLIF is only possible for logic networks.\n" );
+ return;
+ }
+ if ( !Abc_NtkHasSop(pNtk) )
+ Abc_NtkToSop( pNtk, 0 );
+ Io_WriteBblif( pNtk, pFileName );
+ return;
+ }
/*
if ( FileType == IO_FILE_BLIFMV )
{
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index f1793a59..8957743c 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -726,10 +726,10 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
}
// write the comment
- fprintfBz2Aig( &b, "c\n" );
+ fprintfBz2Aig( &b, "c" );
if ( pNtk->pName && strlen(pNtk->pName) > 0 )
- fprintfBz2Aig( &b, ".model %s\n", pNtk->pName );
- fprintfBz2Aig( &b, "This file was produced by ABC on %s\n", Extra_TimeStamp() );
+ fprintfBz2Aig( &b, "n%s%c", pNtk->pName, '\0' );
+ fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() );
fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
// close the file
diff --git a/src/base/io/ioWriteBblif.c b/src/base/io/ioWriteBblif.c
new file mode 100644
index 00000000..e5bd6503
--- /dev/null
+++ b/src/base/io/ioWriteBblif.c
@@ -0,0 +1,111 @@
+/**CFile****************************************************************
+
+ FileName [ioWriteBblif.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Command processing package.]
+
+ Synopsis [Procedures to write AIG in the binary format.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: ioWriteBblif.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ioAbc.h"
+#include "bblif.h"
+
+// For description of Binary BLIF format, refer to "abc/src/aig/bbl/bblif.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Fnction*************************************************************
+
+ Synopsis [Construct manager from the ABC network.]
+
+ Description [In the ABC network each object has a unique integer ID.
+ This ID is used when we construct objects of the BBLIF manager
+ corresponding to each object of the ABC network. The objects can be
+ added to the manager in any order (although below they are added in the
+ topological order), but by the time fanin/fanout connections are created,
+ corresponding objects are already constructed. In the end the checking
+ procedure is called.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Bbl_Man_t * Bbl_ManFromAbc( Abc_Ntk_t * pNtk )
+{
+ Bbl_Man_t * p;
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pObj, * pFanin;
+ int i, k;
+ assert( Abc_NtkIsSopLogic(pNtk) );
+ // start the data manager
+ p = Bbl_ManStart( Abc_NtkName(pNtk) );
+ // collect internal nodes to be added
+ vNodes = Abc_NtkDfs( pNtk, 0 );
+ // create combinational inputs
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ Bbl_ManCreateObject( p, BBL_OBJ_CI, Abc_ObjId(pObj), 0, NULL );
+ // create internal nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Bbl_ManCreateObject( p, BBL_OBJ_NODE, Abc_ObjId(pObj), Abc_ObjFaninNum(pObj), pObj->pData );
+ // create combinational outputs
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Bbl_ManCreateObject( p, BBL_OBJ_CO, Abc_ObjId(pObj), 1, NULL );
+ // create fanin/fanout connections for internal nodes
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Bbl_ManAddFanin( p, Abc_ObjId(pObj), Abc_ObjId(pFanin) );
+ // create fanin/fanout connections for combinational outputs
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Bbl_ManAddFanin( p, Abc_ObjId(pObj), Abc_ObjId(pFanin) );
+ Vec_PtrFree( vNodes );
+ // sanity check
+ Bbl_ManCheck( p );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Writes the AIG in the binary format.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Io_WriteBblif( Abc_Ntk_t * pNtk, char * pFileName )
+{
+ Bbl_Man_t * p;
+ p = Bbl_ManFromAbc( pNtk );
+//Bbl_ManPrintStats( p );
+//Bbl_ManDumpBlif( p, "test_bbl.blif" );
+ Bbl_ManDumpBinaryBlif( p, pFileName );
+ Bbl_ManStop( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/io/module.make b/src/base/io/module.make
index 6f4e2539..993bd7d2 100644
--- a/src/base/io/module.make
+++ b/src/base/io/module.make
@@ -1,6 +1,7 @@
SRC += src/base/io/io.c \
src/base/io/ioReadAiger.c \
src/base/io/ioReadBaf.c \
+ src/base/io/ioReadBblif.c \
src/base/io/ioReadBench.c \
src/base/io/ioReadBlif.c \
src/base/io/ioReadBlifAig.c \
@@ -13,6 +14,7 @@ SRC += src/base/io/io.c \
src/base/io/ioUtil.c \
src/base/io/ioWriteAiger.c \
src/base/io/ioWriteBaf.c \
+ src/base/io/ioWriteBblif.c \
src/base/io/ioWriteBench.c \
src/base/io/ioWriteBlif.c \
src/base/io/ioWriteBlifMv.c \
diff --git a/src/base/ver/verCore.c b/src/base/ver/verCore.c
index f83747cf..aa213010 100644
--- a/src/base/ver/verCore.c
+++ b/src/base/ver/verCore.c
@@ -623,7 +623,7 @@ void Ver_ParseRemoveSuffixTable( Ver_Man_t * pMan )
***********************************************************************/
int Ver_ParseSignalPrefix( Ver_Man_t * pMan, char ** ppWord, int * pnMsb, int * pnLsb )
{
- char * pWord = *ppWord;
+ char * pWord = *ppWord, * pTemp;
int nMsb, nLsb;
assert( pWord[0] == '[' );
// get the beginning
@@ -654,6 +654,17 @@ int Ver_ParseSignalPrefix( Ver_Man_t * pMan, char ** ppWord, int * pnMsb, int *
}
assert( *pWord == ']' );
pWord++;
+
+ // fix the case when \<name> follows after [] without space
+ if ( *pWord == '\\' )
+ {
+ pWord++;
+ pTemp = pWord;
+ while ( *pTemp && *pTemp != ' ' )
+ pTemp++;
+ if ( *pTemp == ' ' )
+ *pTemp = 0;
+ }
}
assert( nMsb >= 0 && nLsb >= 0 );
// return
diff --git a/src/base/ver/verParse.c b/src/base/ver/verParse.c
index 9462fc8b..c38399f2 100644
--- a/src/base/ver/verParse.c
+++ b/src/base/ver/verParse.c
@@ -101,6 +101,15 @@ char * Ver_ParseGetName( Ver_Man_t * pMan )
pMan->fNameLast = 1;
Ver_StreamPopChar( p );
pWord = Ver_StreamGetWord( p, " \r\n" );
+ Ver_StreamSkipChars( p, " \r\n" );
+ if ( Ver_StreamScanChar(p) == '[' )
+ {
+ char This, * pEnd = pWord + strlen( pWord );
+ while ( (This = Ver_StreamPopChar(p)) != ']' )
+ *pEnd++ = This;
+ *pEnd++ = This;
+ *pEnd = 0;
+ }
}
else
pWord = Ver_StreamGetWord( p, " \t\n\r(),;" );
generated by cgit v1.2.3 (git 2.25.1) at 2025-08-05 02:08:24 +0000