summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2009-01-18 08:01:00 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2009-01-18 08:01:00 -0800
commitf936cc0680c98ffe51b3a1716c996072d5dbf76c (patch)
tree784a2a809fb6b972ec6a8e2758ab758ca590d01a /src/base/abci
parentc9ad5880cc61787dec6d018111b63023407ce0e6 (diff)
downloadabc-f936cc0680c98ffe51b3a1716c996072d5dbf76c.tar.gz
abc-f936cc0680c98ffe51b3a1716c996072d5dbf76c.tar.bz2
abc-f936cc0680c98ffe51b3a1716c996072d5dbf76c.zip
Version abc90118
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c1478
-rw-r--r--src/base/abci/abc.zipbin62408 -> 0 bytes
-rw-r--r--src/base/abci/abcBidec.c33
-rw-r--r--src/base/abci/abcCut.c75
-rw-r--r--src/base/abci/abcDar.c726
-rw-r--r--src/base/abci/abcDelay.c297
-rw-r--r--src/base/abci/abcIf.c58
-rw-r--r--src/base/abci/abcMap.c6
-rw-r--r--src/base/abci/abcMerge.c352
-rw-r--r--src/base/abci/abcPrint.c82
-rw-r--r--src/base/abci/abcStrash.c8
-rw-r--r--src/base/abci/module.make1
12 files changed, 2953 insertions, 163 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2ad8dc75..7aad2eb2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -38,6 +38,8 @@
#include "dch.h"
#include "ssw.h"
#include "cgt.h"
+#include "amap.h"
+#include "cec.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -82,6 +84,8 @@ static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPowerdown ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -136,7 +140,7 @@ static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandDCompress2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDC2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDChoice ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDch ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDrwsat ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -147,6 +151,9 @@ static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandDFraig ( 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_CommandQbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -170,6 +177,7 @@ static int Abc_CommandRecPs ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandRecUse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAmap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnmap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAttach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSuperChoice ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -202,8 +210,11 @@ static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandDarPhase ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSynch ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandClockGate ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExtWin ( Abc_Frame_t * pAbc, int argc, char ** argv );
+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 );
@@ -314,8 +325,9 @@ void Abc_FrameClearDesign()
***********************************************************************/
void Abc_Init( Abc_Frame_t * pAbc )
{
-// Abc_NtkBddImplicationTest();
-// Ply_LutPairTest();
+// Amap_LibParseTest( "at\\syn\\libraries\\LIBS\\BRDCM\\tsmc13_5.ff.genlib" );
+// Amap_LibParseTest( "at\\syn\\libraries\\LIBS\\GS60\\GS60_W_30_1.7_CORE.genlib" );
+// Amap_LibParseTest( "at\\syn\\libraries\\LIBS\\TYPICAL\\typical.genlib" );
Cmd_CommandAdd( pAbc, "Printing", "print_stats", Abc_CommandPrintStats, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_exdc", Abc_CommandPrintExdc, 0 );
@@ -356,6 +368,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "mfs", Abc_CommandMfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "trace", Abc_CommandTrace, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "powerdown", Abc_CommandPowerdown, 1 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "merge", Abc_CommandMerge, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 );
@@ -410,7 +424,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "irw", Abc_CommandIRewrite, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "drw", Abc_CommandDRewrite, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "drf", Abc_CommandDRefactor, 1 );
- Cmd_CommandAdd( pAbc, "New AIG", "dcompress2", Abc_CommandDCompress2, 1 );
+ Cmd_CommandAdd( pAbc, "New AIG", "dc2", Abc_CommandDC2, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dchoice", Abc_CommandDChoice, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dch", Abc_CommandDch, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "drwsat", Abc_CommandDrwsat, 1 );
@@ -443,6 +457,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Choicing", "rec_use", Abc_CommandRecUse, 1 );
Cmd_CommandAdd( pAbc, "SC mapping", "map", Abc_CommandMap, 1 );
+ Cmd_CommandAdd( pAbc, "SC mapping", "amap", Abc_CommandAmap, 1 );
Cmd_CommandAdd( pAbc, "SC mapping", "unmap", Abc_CommandUnmap, 1 );
Cmd_CommandAdd( pAbc, "SC mapping", "attach", Abc_CommandAttach, 1 );
Cmd_CommandAdd( pAbc, "SC mapping", "sc", Abc_CommandSuperChoice, 1 );
@@ -473,12 +488,18 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "phase", Abc_CommandDarPhase, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "synch", Abc_CommandSynch, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "clockgate", Abc_CommandClockGate, 1 );
+ Cmd_CommandAdd( pAbc, "Sequential", "extwin", Abc_CommandExtWin, 1 );
+ 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 );
Cmd_CommandAdd( pAbc, "Verification", "dprove", Abc_CommandDProve, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "absec", Abc_CommandAbSec, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "simsec", Abc_CommandSimSec, 0 );
+ Cmd_CommandAdd( pAbc, "Verification", "match", Abc_CommandMatch, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "psat", Abc_CommandPSat, 0 );
@@ -553,6 +574,12 @@ void Abc_Init( Abc_Frame_t * pAbc )
// extern void Aig_ManRandomTest1();
// Aig_ManRandomTest1();
}
+// malloc(1001);
+ {
+ extern void Extra_MemTest();
+// Extra_MemTest();
+ }
+
}
/**Function*************************************************************
@@ -589,6 +616,10 @@ void Abc_End()
extern void Dar_LibStop();
Dar_LibStop();
}
+ {
+ extern void Aig_RManQuit();
+ Aig_RManQuit();
+ }
Abc_NtkFraigStoreClean();
// Rwt_Man4ExplorePrint();
@@ -616,6 +647,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
int fUseLutLib;
int fPrintTime;
int fPrintMuxes;
+ int fPower;
int c;
pNtk = Abc_FrameReadNtk(pAbc);
@@ -629,8 +661,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
fUseLutLib = 0;
fPrintTime = 0;
fPrintMuxes = 0;
+ fPower = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmph" ) ) != EOF )
{
switch ( c )
{
@@ -652,6 +685,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fPrintMuxes ^= 1;
break;
+ case 'p':
+ fPower ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -669,7 +705,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( Abc_FrameReadErr(pAbc), "Cannot print LUT delay for a non-logic network.\n" );
return 1;
}
- Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes );
+ Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes, fPower );
if ( fPrintTime )
{
pAbc->TimeTotal += pAbc->TimeCommand;
@@ -680,7 +716,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: print_stats [-fbdltmh]\n" );
+ fprintf( pErr, "usage: print_stats [-fbdltmph]\n" );
fprintf( pErr, "\t prints the network statistics\n" );
fprintf( pErr, "\t-f : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
fprintf( pErr, "\t-b : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" );
@@ -688,6 +724,7 @@ usage:
fprintf( pErr, "\t-l : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fSaveBest? "yes": "no" );
fprintf( pErr, "\t-t : toggles printing runtime statistics [default = %s]\n", fPrintTime? "yes": "no" );
fprintf( pErr, "\t-m : toggles printing MUX statistics [default = %s]\n", fPrintMuxes? "yes": "no" );
+ fprintf( pErr, "\t-p : toggles printing power dissipation due to switching [default = %s]\n", fPower? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -773,7 +810,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
printf( "EXDC network statistics: \n" );
- Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0, 0 );
+ Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0, 0, 0 );
return 0;
usage:
@@ -3683,7 +3720,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Abc_NtkMfsParsDefault( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraestvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraestpvwh" ) ) != EOF )
{
switch ( c )
{
@@ -3768,6 +3805,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
pPars->fOneHotness ^= 1;
break;
+ case 'p':
+ pPars->fPower ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -3801,7 +3841,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: mfs [-WFDMLC <num>] [-raestvh]\n" );
+ fprintf( pErr, "usage: mfs [-WFDMLC <num>] [-raestpvh]\n" );
fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" );
fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
@@ -3814,6 +3854,7 @@ usage:
fprintf( pErr, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
fprintf( pErr, "\t-s : toggle evaluation of edge swapping [default = %s]\n", pPars->fSwapEdge? "yes": "no" );
fprintf( pErr, "\t-t : toggle using artificial one-hotness conditions [default = %s]\n", pPars->fOneHotness? "yes": "no" );
+ fprintf( pErr, "\t-p : toggle power-aware optimization [default = %s]\n", pPars->fPower? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@@ -4001,6 +4042,252 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandPowerdown( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c;
+ int fUseLutLib;
+ int Percentage;
+ int Degree;
+ int fVerbose;
+ int fVeryVerbose;
+ extern Abc_Ntk_t * Abc_NtkPowerdown( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fUseLutLib = 0;
+ Percentage =10;
+ Degree = 2;
+ fVerbose = 0;
+ fVeryVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PNlvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'P':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Percentage = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Percentage < 1 || Percentage > 100 )
+ goto usage;
+ break;
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Degree = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Degree < 1 || Degree > 5 )
+ goto usage;
+ break;
+ case 'l':
+ fUseLutLib ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ fprintf( pErr, "This command can only be applied to a logic network.\n" );
+ return 1;
+ }
+
+ // modify the current network
+ pNtkRes = Abc_NtkPowerdown( pNtk, fUseLutLib, Percentage, Degree, fVerbose, fVeryVerbose );
+ 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: powerdown [-P num] [-N num] [-vwh]\n" );
+ fprintf( pErr, "\t transforms LUT-mapped network into an AIG with choices;\n" );
+ fprintf( pErr, "\t the choices are added to power down the next round of mapping\n" );
+ fprintf( pErr, "\t-P <num> : switching propability delta defining power critical edges [default = %d%%]\n", Percentage );
+ fprintf( pErr, "\t (e.g. 5% means hot wires switch with probability: 0.45 <= p <= 0.50 (max)\n" );
+ fprintf( pErr, "\t-N <num> : the max critical path degree for resynthesis (0 < num < 6) [default = %d]\n", Degree );
+// fprintf( pErr, "\t-l : toggle using unit- or LUT-library-delay model [default = %s]\n", fUseLutLib? "lib" : "unit" );
+ fprintf( pErr, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-w : toggle printing detailed stats for each node [default = %s]\n", fVeryVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk;
+ Nwk_LMPars_t Pars, * pPars = &Pars;
+ Vec_Int_t * vResult;
+ int c;
+ extern Vec_Int_t * Abc_NtkLutMerge( Abc_Ntk_t * pNtk, Nwk_LMPars_t * pPars );
+ pNtk = Abc_FrameReadNtk(pAbc);
+
+ // set defaults
+ memset( pPars, 0, sizeof(Nwk_LMPars_t) );
+ pPars->nMaxLutSize = 5; // the max LUT size for merging (N=5)
+ pPars->nMaxSuppSize = 5; // the max total support size after merging (S=5)
+ pPars->nMaxDistance = 3; // the max number of nodes separating LUTs
+ pPars->nMaxLevelDiff = 2; // the max difference in levels
+ pPars->nMaxFanout = 100; // the max number of fanouts to traverse
+ pPars->fUseDiffSupp = 0; // enables the use of nodes with different support
+ pPars->fUseTfiTfo = 0; // enables the use of TFO/TFO nodes as candidates
+ pPars->fVeryVerbose = 0; // enables additional verbose output
+ pPars->fVerbose = 1; // enables verbose output
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NSDLFscvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nMaxLutSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nMaxLutSize < 2 )
+ goto usage;
+ break;
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nMaxSuppSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nMaxSuppSize < 2 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nMaxDistance = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nMaxDistance < 2 )
+ goto usage;
+ break;
+ case 'L':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nMaxLevelDiff = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nMaxLevelDiff < 2 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nMaxFanout = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nMaxFanout < 2 )
+ goto usage;
+ break;
+ case 's':
+ pPars->fUseDiffSupp ^= 1;
+ break;
+ case 'c':
+ pPars->fUseTfiTfo ^= 1;
+ break;
+ case 'w':
+ pPars->fVeryVerbose ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL || !Abc_NtkIsLogic(pNtk) )
+ {
+ printf( "Abc_CommandSpeedup(): There is no mapped network to merge LUTs.\n" );
+ return 1;
+ }
+
+ vResult = Abc_NtkLutMerge( pNtk, pPars );
+ Vec_IntFree( vResult );
+ return 0;
+
+usage:
+ fprintf( stdout, "usage: merge [-NSDLF num] [-scwvh]\n" );
+ fprintf( stdout, "\t creates pairs of topologically-related LUTs\n" );
+ fprintf( stdout, "\t-N <num> : the max LUT size for merging (1 < num) [default = %d]\n", pPars->nMaxLutSize );
+ fprintf( stdout, "\t-S <num> : the max total support size after merging (1 < num) [default = %d]\n", pPars->nMaxSuppSize );
+ fprintf( stdout, "\t-D <num> : the max distance in terms of LUTs (0 < num) [default = %d]\n", pPars->nMaxDistance );
+ fprintf( stdout, "\t-L <num> : the max difference in levels (0 <= num) [default = %d]\n", pPars->nMaxLevelDiff );
+ fprintf( stdout, "\t-F <num> : the max number of fanouts to stop traversal (0 < num) [default = %d]\n", pPars->nMaxFanout );
+ fprintf( stdout, "\t-s : toggle the use of nodes without support overlap [default = %s]\n", pPars->fUseDiffSupp? "yes" : "no" );
+ fprintf( stdout, "\t-c : toggle the use of TFI/TFO nodes as candidates [default = %s]\n", pPars->fUseTfiTfo? "yes" : "no" );
+ fprintf( stdout, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+ fprintf( stdout, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( stdout, "\t-h : print the command usage\n");
+ return 1;
+}
/**Function*************************************************************
@@ -4905,7 +5192,7 @@ usage:
fprintf( pErr, "\t-P num : output partition size [default = %s]\n", Buffer );
fprintf( pErr, "\t-c : toggles deriving combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
fprintf( pErr, "\t-i : toggles deriving implication miter (file1 => file2) [default = %s]\n", fImplic? "yes": "no" );
- fprintf( pErr, "\t-m : toggles creating multi-output miters [default = %s]\n", fMulti? "yes": "no" );
+ fprintf( pErr, "\t-m : toggles creating multi-output miter [default = %s]\n", fMulti? "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");
@@ -6943,18 +7230,20 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
memset( pParams, 0, sizeof(Cut_Params_t) );
pParams->nVarsMax = 5; // the max cut size ("k" of the k-feasible cuts)
pParams->nKeepMax = 1000; // the max number of cuts kept at a node
- pParams->fTruth = 0; // compute truth tables
+ pParams->fTruth = 1; // compute truth tables
pParams->fFilter = 1; // filter dominated cuts
pParams->fDrop = 0; // drop cuts on the fly
- pParams->fDag = 0; // compute DAG cuts
+ pParams->fDag = 1; // compute DAG cuts
pParams->fTree = 0; // compute tree cuts
pParams->fGlobal = 0; // compute global cuts
pParams->fLocal = 0; // compute local cuts
pParams->fFancy = 0; // compute something fancy
+ pParams->fRecordAig= 1; // compute something fancy
pParams->fMap = 0; // compute mapping delay
+ pParams->fAdjust = 1; // removes useless fanouts
pParams->fVerbose = 0; // the verbosiness flag
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdxyglzmvoh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdxyglzamjvoh" ) ) != EOF )
{
switch ( c )
{
@@ -7004,9 +7293,15 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'z':
pParams->fFancy ^= 1;
break;
+ case 'a':
+ pParams->fRecordAig ^= 1;
+ break;
case 'm':
pParams->fMap ^= 1;
break;
+ case 'j':
+ pParams->fAdjust ^= 1;
+ break;
case 'v':
pParams->fVerbose ^= 1;
break;
@@ -7056,7 +7351,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdxyzmvh]\n" );
+ fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdxyzamjvh]\n" );
fprintf( pErr, "\t computes k-feasible cuts for the AIG\n" );
fprintf( pErr, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n", CUT_SIZE_MIN, CUT_SIZE_MAX, pParams->nVarsMax );
fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n", pParams->nKeepMax );
@@ -7068,7 +7363,9 @@ usage:
fprintf( pErr, "\t-g : toggle computing only global cuts [default = %s]\n", pParams->fGlobal? "yes": "no" );
fprintf( pErr, "\t-l : toggle computing only local cuts [default = %s]\n", pParams->fLocal? "yes": "no" );
fprintf( pErr, "\t-z : toggle fancy computations [default = %s]\n", pParams->fFancy? "yes": "no" );
+ fprintf( pErr, "\t-a : toggle recording cut functions [default = %s]\n", pParams->fRecordAig?"yes": "no" );
fprintf( pErr, "\t-m : toggle delay-oriented FPGA mapping [default = %s]\n", pParams->fMap? "yes": "no" );
+ fprintf( pErr, "\t-j : toggle removing fanouts due to XOR/MUX [default = %s]\n", pParams->fAdjust? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", pParams->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -7742,7 +8039,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Aig_ProcedureTest();
extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk );
- extern int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -8804,13 +9100,13 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandDC2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
- int fBalance, fVerbose, fUpdateLevel, fFanout, c;
+ int fBalance, fVerbose, fUpdateLevel, fFanout, fPower, c;
- extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkDC2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -8821,8 +9117,9 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
fVerbose = 0;
fUpdateLevel = 0;
fFanout = 1;
+ fPower = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "blfvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "blfpvh" ) ) != EOF )
{
switch ( c )
{
@@ -8835,6 +9132,9 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
fFanout ^= 1;
break;
+ case 'p':
+ fPower ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -8854,7 +9154,7 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "This command works only for strashed networks.\n" );
return 1;
}
- pNtkRes = Abc_NtkDCompress2( pNtk, fBalance, fUpdateLevel, fFanout, fVerbose );
+ pNtkRes = Abc_NtkDC2( pNtk, fBalance, fUpdateLevel, fFanout, fPower, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -8865,11 +9165,12 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: dcompress2 [-blfvh]\n" );
+ fprintf( pErr, "usage: dc2 [-blfpvh]\n" );
fprintf( pErr, "\t performs combinational AIG optimization\n" );
fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
fprintf( pErr, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-f : toggle representing fanouts [default = %s]\n", fFanout? "yes": "no" );
+ fprintf( pErr, "\t-p : toggle power-aware rewriting [default = %s]\n", fPower? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -9053,7 +9354,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fSynthesis ^= 1;
break;
case 'p':
- pPars->fPolarFlip ^= 1;
+ pPars->fPower ^= 1;
break;
case 't':
pPars->fSimulateTfo ^= 1;
@@ -9094,7 +9395,7 @@ usage:
fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( pErr, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
fprintf( pErr, "\t-s : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
- fprintf( pErr, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
+ fprintf( pErr, "\t-p : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" );
fprintf( pErr, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@@ -11166,6 +11467,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk, * pNtkRes;
char Buffer[100];
double DelayTarget;
+ int fAreaOnly;
int fRecovery;
int fSweep;
int fSwitching;
@@ -11180,12 +11482,13 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
DelayTarget =-1;
+ fAreaOnly = 0;
fRecovery = 1;
fSweep = 1;
fSwitching = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Daspvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Darspvh" ) ) != EOF )
{
switch ( c )
{
@@ -11201,6 +11504,9 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
break;
case 'a':
+ fAreaOnly ^= 1;
+ break;
+ case 'r':
fRecovery ^= 1;
break;
case 's':
@@ -11225,6 +11531,9 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
+ if ( fAreaOnly )
+ DelayTarget = 100000.0;
+
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
@@ -11274,10 +11583,11 @@ usage:
sprintf( Buffer, "not used" );
else
sprintf( Buffer, "%.3f", DelayTarget );
- fprintf( pErr, "usage: map [-D float] [-aspvh]\n" );
+ fprintf( pErr, "usage: map [-D float] [-arspvh]\n" );
fprintf( pErr, "\t performs standard cell mapping of the current network\n" );
fprintf( pErr, "\t-D float : sets the global required times [default = %s]\n", Buffer );
- fprintf( pErr, "\t-a : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
+ fprintf( pErr, "\t-a : toggles area-only mapping [default = %s]\n", fAreaOnly? "yes": "no" );
+ fprintf( pErr, "\t-r : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
fprintf( pErr, "\t-s : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" );
fprintf( pErr, "\t-p : optimizes power by minimizing switching [default = %s]\n", fSwitching? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -11285,6 +11595,159 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAmap( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Amap_Par_t Pars, * pPars = &Pars;
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int fSweep;
+ int c;
+ extern Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars );
+ extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose, int fVeryVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fSweep = 0;
+ Amap_ManSetDefaultParams( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FAEmxisvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by a floating point number.\n" );
+ goto usage;
+ }
+ pPars->nIterFlow = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nIterFlow < 0 )
+ goto usage;
+ break;
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-A\" should be followed by a floating point number.\n" );
+ goto usage;
+ }
+ pPars->nIterArea = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nIterArea < 0 )
+ goto usage;
+ break;
+ case 'E':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-E\" should be followed by a floating point number.\n" );
+ goto usage;
+ }
+ pPars->fEpsilon = (float)atof(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->fEpsilon < 0.0 || pPars->fEpsilon > 1.0 )
+ goto usage;
+ break;
+ case 'm':
+ pPars->fUseMuxes ^= 1;
+ break;
+ case 'x':
+ pPars->fUseXors ^= 1;
+ break;
+ case 'i':
+ pPars->fFreeInvs ^= 1;
+ break;
+ case 's':
+ fSweep ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Strashing before mapping has failed.\n" );
+ return 1;
+ }
+ pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 );
+ Abc_NtkDelete( pNtkRes );
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Balancing before mapping has failed.\n" );
+ return 1;
+ }
+ fprintf( pOut, "The network was strashed and balanced before mapping.\n" );
+ // get the new network
+ pNtkRes = Abc_NtkDarAmap( pNtk, pPars );
+ if ( pNtkRes == NULL )
+ {
+ Abc_NtkDelete( pNtk );
+ fprintf( pErr, "Mapping has failed.\n" );
+ return 1;
+ }
+ Abc_NtkDelete( pNtk );
+ }
+ else
+ {
+ // get the new network
+ pNtkRes = Abc_NtkDarAmap( pNtk, pPars );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Mapping has failed.\n" );
+ return 1;
+ }
+ }
+
+ if ( fSweep )
+ Abc_NtkFraigSweep( pNtkRes, 0, 0, 0, 0 );
+
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: amap [-FA <num>] [-E <float>] [-mxisvh]\n" );
+ fprintf( pErr, "\t performs standard cell mapping of the current network\n" );
+ fprintf( pErr, "\t-F num : the number of iterations of area flow [default = %d]\n", pPars->nIterFlow );
+ fprintf( pErr, "\t-A num : the number of iterations of exact area [default = %d]\n", pPars->nIterArea );
+ fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->fEpsilon );
+ fprintf( pErr, "\t-m : toggles using MUX matching [default = %s]\n", pPars->fUseMuxes? "yes": "no" );
+ fprintf( pErr, "\t-x : toggles using XOR matching [default = %s]\n", pPars->fUseXors? "yes": "no" );
+ fprintf( pErr, "\t-i : toggles assuming inverters are free [default = %s]\n", pPars->fFreeInvs? "yes": "no" );
+ fprintf( pErr, "\t-s : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" );
+ fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
@@ -11916,6 +12379,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fExpRed = 1;
pPars->fLatchPaths = 0;
pPars->fEdge = 1;
+ pPars->fPower = 0;
pPars->fCutMin = 0;
pPars->fSeqMap = 0;
pPars->fBidec = 0;
@@ -11930,7 +12394,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pFuncCost = NULL;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstbvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEqaflepmrstbvh" ) ) != EOF )
{
switch ( c )
{
@@ -12001,7 +12465,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->Epsilon < 0.0 || pPars->Epsilon > 1.0 )
goto usage;
break;
- case 'p':
+ case 'q':
pPars->fPreprocess ^= 1;
break;
case 'a':
@@ -12019,6 +12483,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'e':
pPars->fEdge ^= 1;
break;
+ case 'p':
+ pPars->fPower ^= 1;
+ break;
case 'm':
pPars->fCutMin ^= 1;
break;
@@ -12159,7 +12626,7 @@ usage:
sprintf( LutSize, "library" );
else
sprintf( LutSize, "%d", pPars->nLutSize );
- fprintf( pErr, "usage: if [-KCFA num] [-DE float] [-parlemsbvh]\n" );
+ fprintf( pErr, "usage: if [-KCFA num] [-DE float] [-qarlepmsbvh]\n" );
fprintf( pErr, "\t performs FPGA technology mapping of the network\n" );
fprintf( pErr, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
fprintf( pErr, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -12167,12 +12634,13 @@ usage:
fprintf( pErr, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters );
fprintf( pErr, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );
fprintf( pErr, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->Epsilon );
- fprintf( pErr, "\t-p : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
+ fprintf( pErr, "\t-q : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
fprintf( pErr, "\t-a : toggles area-oriented mapping [default = %s]\n", pPars->fArea? "yes": "no" );
// fprintf( pErr, "\t-f : toggles one fancy feature [default = %s]\n", pPars->fFancy? "yes": "no" );
fprintf( pErr, "\t-r : enables expansion/reduction of the best cuts [default = %s]\n", pPars->fExpRed? "yes": "no" );
fprintf( pErr, "\t-l : optimizes latch paths for delay, other paths for area [default = %s]\n", pPars->fLatchPaths? "yes": "no" );
fprintf( pErr, "\t-e : uses edge-based cut selection heuristics [default = %s]\n", pPars->fEdge? "yes": "no" );
+ fprintf( pErr, "\t-p : uses power-aware cut selection heuristics [default = %s]\n", pPars->fPower? "yes": "no" );
fprintf( pErr, "\t-m : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
fprintf( pErr, "\t-s : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" );
// fprintf( pErr, "\t-t : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
@@ -12957,10 +13425,12 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
int fFastButConservative;
int maxDelay;
- extern Abc_Ntk_t* Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose,
- int fComputeInit, int fGuaranteeInit, int fBlockConst,
- int fForward, int fBackward, int nMaxIters,
- int maxDelay, int fFastButConservative);
+ printf( "This command is temporarily disabled.\n" );
+ return 0;
+// extern Abc_Ntk_t* Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose,
+// int fComputeInit, int fGuaranteeInit, int fBlockConst,
+// int fForward, int fBackward, int nMaxIters,
+// int maxDelay, int fFastButConservative);
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -13042,7 +13512,7 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Only one switch \"-f\" or \"-b\" can be selected at a time.\n" );
return 1;
}
-
+
if ( fGuaranteeInit && !fComputeInit )
{
fprintf( pErr, "Initial state guarantee (-g) requires initial state computation (-i).\n" );
@@ -13062,10 +13532,10 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// perform the retiming
- pNtkRes = Abc_FlowRetime_MinReg( pNtk, fVerbose, fComputeInit,
- fGuaranteeInit, fBlockConst,
- fForward, fBackward,
- nMaxIters, maxDelay, fFastButConservative );
+// pNtkRes = Abc_FlowRetime_MinReg( pNtk, fVerbose, fComputeInit,
+// fGuaranteeInit, fBlockConst,
+// fForward, fBackward,
+// nMaxIters, maxDelay, fFastButConservative );
if (pNtkRes != pNtk)
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -13567,7 +14037,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSIVMplfudvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSIVMplfudsvwh" ) ) != EOF )
{
switch ( c )
{
@@ -13696,6 +14166,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
pPars->fDynamic ^= 1;
break;
+ case 's':
+ pPars->fLocalSim ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -13739,7 +14212,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: scorr [-PQFCLNSIVM <num>] [-pludvwh]\n" );
+ fprintf( pErr, "usage: scorr [-PQFCLNSIVM <num>] [-pludsvwh]\n" );
fprintf( pErr, "\t performs sequential sweep using K-step induction\n" );
fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -13756,6 +14229,7 @@ usage:
// fprintf( pErr, "\t-f : toggle filtering using iterative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
fprintf( pErr, "\t-u : toggle using uniqueness constraints [default = %s]\n", pPars->fUniqueness? "yes": "no" );
fprintf( pErr, "\t-d : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" );
+ fprintf( pErr, "\t-s : toggle local simulation in the cone of influence [default = %s]\n", pPars->fLocalSim? "yes": "no" );
fprintf( pErr, "\t-w : toggle printout of flop equivalences [default = %s]\n", pPars->fFlopVerbose? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
@@ -14336,21 +14810,29 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
+ int fNew;
+ int fComb;
int nFrames;
int nWords;
+ int TimeOut;
+ int fMiter;
int fVerbose;
- extern int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose );
+ extern int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fComb, int fMiter, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
+ fNew = 1;
+ fComb = 0;
nFrames = 32;
nWords = 8;
+ TimeOut = 30;
+ fMiter = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "FWvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FWTncmvh" ) ) != EOF )
{
switch ( c )
{
@@ -14376,6 +14858,26 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nWords < 0 )
goto usage;
break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ TimeOut = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( TimeOut < 0 )
+ goto usage;
+ break;
+ case 'n':
+ fNew ^= 1;
+ break;
+ case 'c':
+ fComb ^= 1;
+ break;
+ case 'm':
+ fMiter ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -14390,27 +14892,24 @@ int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
-
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Only works for strashed networks.\n" );
return 1;
}
- if ( !Abc_NtkLatchNum(pNtk) )
- {
- fprintf( pErr, "The network is combinational.\n" );
- return 0;
- }
-
FREE( pNtk->pSeqModel );
- Abc_NtkDarSeqSim( pNtk, nFrames, nWords, fVerbose );
+ Abc_NtkDarSeqSim( pNtk, nFrames, nWords, TimeOut, fNew, fComb, fMiter, fVerbose );
return 0;
usage:
- fprintf( pErr, "usage: sim [-F num] [-W num] [-vh]\n" );
+ fprintf( pErr, "usage: sim [-FWT num] [-ncmvh]\n" );
fprintf( pErr, "\t performs random simulation of the sequentail miter\n" );
fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
fprintf( pErr, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
+ fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut );
+ fprintf( pErr, "\t-n : toggle new vs. old implementation [default = %s]\n", fNew? "new": "old" );
+ fprintf( pErr, "\t-c : toggle comb vs. seq simulaton [default = %s]\n", fComb? "comb": "seq" );
+ fprintf( pErr, "\t-m : toggle miter vs. any circuit [default = %s]\n", fMiter? "miter": "not miter" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -14664,7 +15163,7 @@ int Abc_CommandClockGate( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Cgt_SetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "LNDCVKvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "LNDCVKavwh" ) ) != EOF )
{
switch ( c )
{
@@ -14734,9 +15233,15 @@ int Abc_CommandClockGate( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nFlopsMin <= 0 )
goto usage;
break;
+ case 'a':
+ pPars->fAreaOnly ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
+ case 'w':
+ pPars->fVeryVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -14780,7 +15285,7 @@ int Abc_CommandClockGate( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: clockgate [-LNDCVK <num>] [-vh] <file>\n" );
+ fprintf( pErr, "usage: clockgate [-LNDCVK <num>] [-avwh] <file>\n" );
fprintf( pErr, "\t sequential clock gating with observability don't-cares\n" );
fprintf( pErr, "\t-L num : max level number of a clock gate [default = %d]\n", pPars->nLevelMax );
fprintf( pErr, "\t-N num : max number of candidates for a flop [default = %d]\n", pPars->nCandMax );
@@ -14788,7 +15293,9 @@ usage:
fprintf( pErr, "\t-C num : max number of conflicts at a node [default = %d]\n", pPars->nConfMax );
fprintf( pErr, "\t-V num : min number of vars to recycle SAT solver [default = %d]\n", pPars->nVarsMin );
fprintf( pErr, "\t-K num : min number of flops to recycle SAT solver [default = %d]\n", pPars->nFlopsMin );
+ fprintf( pErr, "\t-a : toggle minimizing area-only [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-w : toggle even more detailed output [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tfile : (optional) constraints for primary inputs and register outputs\n");
return 1;
@@ -14805,6 +15312,226 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandExtWin( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtkRes, * pNtk;
+ int c;
+ int nObjId;
+ int nDist;
+ int fVerbose;
+
+ extern Abc_Ntk_t * Abc_NtkDarExtWin( Abc_Ntk_t * pNtk, int nObjId, int nDist, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nObjId = -1;
+ nDist = 5;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NDvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nObjId = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nObjId <= 0 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nDist = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nDist <= 0 )
+ 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;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Only works for structrally hashed networks.\n" );
+ return 1;
+ }
+
+ if ( argc != globalUtilOptind )
+ {
+ fprintf( pErr, "Not enough command-line arguments.\n" );
+ return 1;
+ }
+ // modify the current network
+ pNtkRes = Abc_NtkDarExtWin( pNtk, nObjId, nDist, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Extracting sequential window has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: extwin [-ND <num>] [-vh]\n" );
+ fprintf( pErr, "\t extracts sequential window from the AIG\n" );
+ fprintf( pErr, "\t-N num : the ID of the object to use as the center [default = %d]\n", nObjId );
+ fprintf( pErr, "\t-D num : the \"radius\" of the window [default = %d]\n", nDist );
+ fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandInsWin( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtkRes, * pNtk, * pNtkCare;
+ int c;
+ int nObjId;
+ int nDist;
+ int fVerbose;
+
+ extern Abc_Ntk_t * Abc_NtkDarInsWin( Abc_Ntk_t * pNtk, Abc_Ntk_t * pWnd, int nObjId, int nDist, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nObjId = -1;
+ nDist = 5;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NDvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nObjId = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nObjId <= 0 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nDist = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nDist <= 0 )
+ 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;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Only works for structrally hashed networks.\n" );
+ return 1;
+ }
+
+ if ( argc != globalUtilOptind + 1 )
+ {
+ fprintf( pErr, "Not enough command-line arguments.\n" );
+ return 1;
+ }
+ pNtkCare = Io_Read( argv[globalUtilOptind], Io_ReadFileType(argv[globalUtilOptind]), 1 );
+ if ( pNtkCare == NULL )
+ {
+ printf( "Reading care network has failed.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsStrash(pNtkCare) )
+ {
+ Abc_Ntk_t * pNtkTemp;
+ pNtkCare = Abc_NtkStrash( pNtkTemp = pNtkCare, 0, 1, 0 );
+ Abc_NtkDelete( pNtkTemp );
+ }
+ // modify the current network
+ pNtkRes = Abc_NtkDarInsWin( pNtk, pNtkCare, nObjId, nDist, fVerbose );
+ Abc_NtkDelete( pNtkCare );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Inserting sequential window has failed.\n" );
+ return 0;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: inswin [-ND <num>] [-vh] <file>\n" );
+ fprintf( pErr, "\t inserts sequential window into the AIG\n" );
+ fprintf( pErr, "\t-N num : the ID of the object to use as the center [default = %d]\n", nObjId );
+ fprintf( pErr, "\t-D num : the \"radius\" of the window [default = %d]\n", nDist );
+ fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ fprintf( pErr, "\tfile : file with the AIG to be inserted\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char Buffer[16];
@@ -15108,6 +15835,149 @@ 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;
@@ -15558,6 +16428,351 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbSec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
+ int fDelete1, fDelete2;
+ char ** pArgvNew;
+ int nArgcNew;
+ int fMiter, nFrames, fVerbose, c;
+
+ extern int Abc_NtkDarAbSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fMiter = 1;
+ nFrames = 2;
+ fVerbose = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Fmvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFrames < 0 )
+ goto usage;
+ break;
+ case 'm':
+ fMiter ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( fMiter )
+ {
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+ return 0;
+ }
+ Abc_NtkDarAbSec( pNtk, NULL, nFrames, fVerbose );
+ }
+ else
+ {
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
+ if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
+ return 1;
+ if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
+ {
+ if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+ if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+ printf( "The network has no latches. Used combinational command \"cec\".\n" );
+ return 0;
+ }
+ // perform verification
+ Abc_NtkDarAbSec( pNtk1, pNtk2, nFrames, fVerbose );
+ if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+ if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+ }
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: absec [-F num] [-mv] <file1> <file2>\n" );
+ fprintf( pErr, "\t performs SEC by applying CEC to several timeframes\n" );
+ fprintf( pErr, "\t-F num : the total number of timeframes to use [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-m : toggles miter vs. two networks [default = %s]\n", fMiter? "miter": "two networks" );
+ fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ 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_CommandSimSec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Ssw_Pars_t Pars, * pPars = &Pars;
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
+ int fDelete1, fDelete2;
+ char ** pArgvNew;
+ int nArgcNew, c;
+ int fMiter;
+
+ extern int Abc_NtkDarSimSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Ssw_Pars_t * pPars );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fMiter = 1;
+ Ssw_ManSetDefaultParams( pPars );
+ pPars->fPartSigCorr = 1;
+ pPars->fVerbose = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FDcymvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nFramesK = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nFramesK < 0 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nIsleDist = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nIsleDist < 0 )
+ goto usage;
+ break;
+ case 'm':
+ fMiter ^= 1;
+ break;
+ case 'c':
+ pPars->fPartSigCorr ^= 1;
+ break;
+ case 'y':
+ pPars->fDumpSRInit ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( fMiter )
+ {
+// Abc_Ntk_t * pNtkA, * pNtkB;
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+ return 0;
+ }
+ Abc_NtkDarSimSec( pNtk, NULL, pPars );
+/*
+ pNtkA = Abc_NtkDup( pNtk );
+ pNtkB = Abc_NtkDup( pNtk );
+ Abc_NtkDarSimSec( pNtkA, pNtkB, pPars );
+ Abc_NtkDelete( pNtkA );
+ Abc_NtkDelete( pNtkB );
+*/
+ }
+ else
+ {
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
+ if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
+ return 1;
+ if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
+ {
+ if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+ if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+ printf( "The network has no latches. Used combinational command \"cec\".\n" );
+ return 0;
+ }
+ // perform verification
+ Abc_NtkDarSimSec( pNtk1, pNtk2, pPars );
+ if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+ if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+ }
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: simsec [-FD num] [-mcyv] <file1> <file2>\n" );
+ fprintf( pErr, "\t performs SEC using structural similarity\n" );
+ fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pPars->nFramesK );
+ fprintf( pErr, "\t-D num : the distance for extending islands [default = %d]\n", pPars->nIsleDist );
+ fprintf( pErr, "\t-m : toggles miter vs. two networks [default = %s]\n", fMiter? "miter": "two networks" );
+ fprintf( pErr, "\t-c : uses partial vs. full signal correspondence [default = %s]\n", pPars->fPartSigCorr? "partial": "full" );
+ fprintf( pErr, "\t-y : dumps speculatively reduced miter of the classes [default = %s]\n", pPars->fDumpSRInit? "yes": "no" );
+ fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ 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_CommandMatch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtk1, * pNtk2, * pNtkRes;
+ int fDelete1, fDelete2;
+ char ** pArgvNew;
+ int nArgcNew, c;
+ int fMiter;
+ int nDist;
+ int fVerbose;
+
+ extern Abc_Ntk_t * Abc_NtkDarMatch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nDist, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fMiter = 0;
+ nDist = 0;
+ fVerbose = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Dmvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nDist = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nDist < 0 )
+ goto usage;
+ break;
+ case 'm':
+ fMiter ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( fMiter )
+ {
+// Abc_Ntk_t * pNtkA, * pNtkB;
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+ return 0;
+ }
+ pNtkRes = Abc_NtkDarMatch( pNtk, NULL, nDist, fVerbose );
+/*
+ pNtkA = Abc_NtkDup( pNtk );
+ pNtkB = Abc_NtkDup( pNtk );
+ Abc_NtkDarSimSec( pNtkA, pNtkB, pPars );
+ Abc_NtkDelete( pNtkA );
+ Abc_NtkDelete( pNtkB );
+*/
+ }
+ else
+ {
+ pArgvNew = argv + globalUtilOptind;
+ nArgcNew = argc - globalUtilOptind;
+ if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
+ return 1;
+ if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
+ {
+ if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+ if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+ printf( "The network has no latches. Used combinational command \"cec\".\n" );
+ return 0;
+ }
+ // perform verification
+ pNtkRes = Abc_NtkDarMatch( pNtk1, pNtk2, nDist, fVerbose );
+ if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
+ if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
+ }
+ if ( pNtkRes == NULL )
+ {
+ printf( "Matching has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: match [-D num] [-mv] <file1> <file2>\n" );
+ fprintf( pErr, "\t detects structural similarity using simulation\n" );
+ fprintf( pErr, "\t replaces the current network by the miter of differences\n" );
+ fprintf( pErr, "\t-D num : the distance for extending differences [default = %d]\n", nDist );
+ fprintf( pErr, "\t-m : toggles miter vs. two networks [default = %s]\n", fMiter? "miter": "two networks" );
+ fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ 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_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -17133,8 +18348,9 @@ int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
if ( pNtkRes == NULL )
{
- fprintf( pErr, "Target enlargement has failed.\n" );
- return 1;
+ if ( pNtk->pSeqModel == NULL )
+ printf( "Proof-based abstraction has failed.\n" );
+ return 0;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -17297,16 +18513,19 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fMapped;
int fTest;
+ int fAlter;
extern void * Ioa_ReadBlif( char * pFileName, int fCheck );
extern void Ioa_WriteBlif( void * p, char * pFileName );
extern Aig_Man_t * Ntl_ManExtract( void * p );
extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
+ extern void Ntl_ManPrintStats( void * p );
// set defaults
fMapped = 0;
fTest = 0;
+ fAlter = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "mth" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "mtah" ) ) != EOF )
{
switch ( c )
{
@@ -17316,6 +18535,9 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
fTest ^= 1;
break;
+ case 'a':
+ fAlter ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -17334,11 +18556,9 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
-
if ( fTest )
{
extern void Ntl_ManFree( void * p );
- extern void Ntl_ManPrintStats( void * p );
void * pTemp = Ioa_ReadBlif( pFileName, 1 );
if ( pTemp )
{
@@ -17350,11 +18570,26 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
}
Abc_FrameClearDesign();
- pAbc->pAbc8Ntl = Ioa_ReadBlif( pFileName, 1 );
- if ( pAbc->pAbc8Ntl == NULL )
+ if ( !fAlter )
{
- printf( "Abc_CommandAbc8Read(): Reading BLIF has failed.\n" );
- return 1;
+ pAbc->pAbc8Ntl = Ioa_ReadBlif( pFileName, 1 );
+ if ( pAbc->pAbc8Ntl == NULL )
+ {
+ printf( "Abc_CommandAbc8Read(): Reading BLIF has failed.\n" );
+ return 1;
+ }
+ }
+ else
+ {
+ extern void * Nal_ManRead( char * pFileName );
+ pAbc->pAbc8Ntl = NULL;
+// pAbc->pAbc8Ntl = Nal_ManRead( pFileName );
+// Ioa_WriteBlif( pAbc->pAbc8Ntl, "test_boxes.blif" );
+ if ( pAbc->pAbc8Ntl == NULL )
+ {
+ printf( "Abc_CommandAbc8Read(): Reading design has failed.\n" );
+ return 1;
+ }
}
pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
if ( pAbc->pAbc8Aig == NULL )
@@ -17371,10 +18606,11 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( stdout, "usage: *r [-mth]\n" );
+ fprintf( stdout, "usage: *r [-mtah]\n" );
fprintf( stdout, "\t reads the design with whiteboxes\n" );
fprintf( stdout, "\t-m : toggle extracting mapped network [default = %s]\n", fMapped? "yes": "no" );
fprintf( stdout, "\t-t : toggle reading in the test mode [default = %s]\n", fTest? "yes": "no" );
+ fprintf( stdout, "\t-a : toggle reading another file type [default = %s]\n", fAlter? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
@@ -17468,6 +18704,7 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
char * pFileName;
void * pTemp;
int fAig;
+ int fBlif;
int fCollapsed;
int c;
extern void Ioa_WriteBlif( void * p, char * pFileName );
@@ -17479,15 +18716,19 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fAig = 0;
+ fBlif = 1;
fCollapsed = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "ach" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "abch" ) ) != EOF )
{
switch ( c )
{
case 'a':
fAig ^= 1;
break;
+ case 'b':
+ fBlif ^= 1;
+ break;
case 'c':
fCollapsed ^= 1;
break;
@@ -17501,29 +18742,38 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
{
printf( "Abc_CommandAbc8Write(): There is no design to write.\n" );
return 1;
- }
+ }
// create the design to write
pFileName = argv[globalUtilOptind];
if ( fAig )
{
if ( fCollapsed )
{
+ extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
pTemp = Ntl_ManCollapseSeq( pAbc->pAbc8Ntl, 0 );
- Saig_ManDumpBlif( pTemp, pFileName );
+ if ( fBlif )
+ Saig_ManDumpBlif( pTemp, pFileName );
+ else
+ Ioa_WriteAiger( pTemp, pFileName, 0, 0 );
Aig_ManStop( pTemp );
}
else
{
if ( pAbc->pAbc8Aig != NULL )
{
- pTemp = Ntl_ManInsertAig( pAbc->pAbc8Ntl, pAbc->pAbc8Aig );
- if ( pTemp == NULL )
+ if ( fBlif )
{
- printf( "Abc_CommandAbc8Write(): Inserting AIG has failed.\n" );
- return 1;
+ pTemp = Ntl_ManInsertAig( pAbc->pAbc8Ntl, pAbc->pAbc8Aig );
+ if ( pTemp == NULL )
+ {
+ printf( "Abc_CommandAbc8Write(): Inserting AIG has failed.\n" );
+ return 1;
+ }
+ Ioa_WriteBlif( pTemp, pFileName );
+ Ntl_ManFree( pTemp );
}
- Ioa_WriteBlif( pTemp, pFileName );
- Ntl_ManFree( pTemp );
+ else
+ Ioa_WriteAiger( pAbc->pAbc8Aig, pFileName, 0, 0 );
}
else
{
@@ -17547,17 +18797,18 @@ int Abc_CommandAbc8Write( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
{
- pTemp = pAbc->pAbc8Ntl;
printf( "Writing the unmapped netlist.\n" );
+ pTemp = pAbc->pAbc8Ntl;
Ioa_WriteBlif( pTemp, pFileName );
}
}
return 0;
usage:
- fprintf( stdout, "usage: *w [-ach]\n" );
+ fprintf( stdout, "usage: *w [-abch]\n" );
fprintf( stdout, "\t write the design with whiteboxes\n" );
fprintf( stdout, "\t-a : toggle writing mapped network or AIG [default = %s]\n", fAig? "AIG": "mapped" );
+ fprintf( stdout, "\t-b : toggle writing AIG as BLIF or AIGER [default = %s]\n", fBlif? "BLIF": "AIGER" );
fprintf( stdout, "\t-c : toggle writing collapsed sequential AIG [default = %s]\n", fCollapsed? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
@@ -17841,14 +19092,19 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fSaveBest;
int fDumpResult;
+ int fPower;
+ int fShort;
extern void Ntl_ManPrintStats( void * p );
- extern void Nwk_ManPrintStats( void * p, void * pLutLib, int fSaveBest, int fDumpResult, void * pNtl );
+ extern void Nwk_ManPrintStats( void * p, void * pLutLib, int fSaveBest, int fDumpResult, int fPower, void * pNtl );
+ extern void Nwk_ManPrintStatsShort( void * p, void * pAig, void * pNtk );
// set defaults
fSaveBest = 0;
fDumpResult = 0;
+ fPower = 0;
+ fShort = 1;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "bdh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "bdpsh" ) ) != EOF )
{
switch ( c )
{
@@ -17858,6 +19114,12 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDumpResult ^= 1;
break;
+ case 'p':
+ fPower ^= 1;
+ break;
+ case 's':
+ fShort ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -17870,6 +19132,11 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
+ if ( fShort )
+ {
+ Nwk_ManPrintStatsShort( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pAbc->pAbc8Nwk );
+ return 0;
+ }
// get the input file name
if ( pAbc->pAbc8Ntl )
{
@@ -17889,15 +19156,17 @@ int Abc_CommandAbc8Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->pAbc8Lib = If_SetSimpleLutLib( 6 );
}
printf( "MAPPED: " );
- Nwk_ManPrintStats( pAbc->pAbc8Nwk, pAbc->pAbc8Lib, fSaveBest, fDumpResult, pAbc->pAbc8Ntl );
+ Nwk_ManPrintStats( pAbc->pAbc8Nwk, pAbc->pAbc8Lib, fSaveBest, fDumpResult, fPower, pAbc->pAbc8Ntl );
}
return 0;
usage:
- fprintf( stdout, "usage: *ps [-bdh]\n" );
+ fprintf( stdout, "usage: *ps [-bdpsh]\n" );
fprintf( stdout, "\t prints design statistics\n" );
fprintf( stdout, "\t-b : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" );
fprintf( stdout, "\t-d : toggles dumping network into file \"<input_file_name>_dump.blif\" [default = %s]\n", fDumpResult? "yes": "no" );
+ fprintf( stdout, "\t-p : toggles printing power dissipation due to switching [default = %s]\n", fPower? "yes": "no" );
+ fprintf( stdout, "\t-s : toggles short printing mode [default = %s]\n", fShort? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
}
@@ -17979,7 +19248,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
Nwk_ManSetIfParsDefault( pPars );
pPars->pLutLib = pAbc->pAbc8Lib;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstbvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEqaflepmrstbvh" ) ) != EOF )
{
switch ( c )
{
@@ -18039,6 +19308,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
globalUtilOptind++;
if ( pPars->DelayTarget <= 0.0 )
goto usage;
+ break;
case 'E':
if ( globalUtilOptind >= argc )
{
@@ -18050,7 +19320,7 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->Epsilon < 0.0 || pPars->Epsilon > 1.0 )
goto usage;
break;
- case 'p':
+ case 'q':
pPars->fPreprocess ^= 1;
break;
case 'a':
@@ -18068,6 +19338,9 @@ int Abc_CommandAbc8If( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'e':
pPars->fEdge ^= 1;
break;
+ case 'p':
+ pPars->fPower ^= 1;
+ break;
case 'm':
pPars->fCutMin ^= 1;
break;
@@ -18146,7 +19419,7 @@ usage:
sprintf( LutSize, "library" );
else
sprintf( LutSize, "%d", pPars->nLutSize );
- fprintf( stdout, "usage: *if [-KCFA num] [-DE float] [-parlembvh]\n" );
+ 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 );
@@ -18154,12 +19427,13 @@ usage:
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-p : toggles preprocessing using several starting points [default = %s]\n", pPars->fPreprocess? "yes": "no" );
+ 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" );
@@ -18332,7 +19606,7 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fSynthesis ^= 1;
break;
case 'p':
- pPars->fPolarFlip ^= 1;
+ pPars->fPower ^= 1;
break;
case 't':
pPars->fSimulateTfo ^= 1;
@@ -18370,7 +19644,7 @@ usage:
fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
fprintf( stdout, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
fprintf( stdout, "\t-s : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
- fprintf( stdout, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
+ fprintf( stdout, "\t-p : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" );
fprintf( stdout, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
fprintf( stdout, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
@@ -18395,15 +19669,17 @@ int Abc_CommandAbc8DC2( Abc_Frame_t * pAbc, int argc, char ** argv )
int fBalance;
int fUpdateLevel;
int fVerbose;
+ int fPower;
- extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fVerbose );
+ extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose );
// set defaults
fBalance = 1;
fUpdateLevel = 1;
+ fPower = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "blh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "blpvh" ) ) != EOF )
{
switch ( c )
{
@@ -18413,6 +19689,9 @@ int Abc_CommandAbc8DC2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'l':
fUpdateLevel ^= 1;
break;
+ case 'p':
+ fPower ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -18429,7 +19708,7 @@ int Abc_CommandAbc8DC2( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// get the input file name
- pAigNew = Dar_ManCompress2( pAbc->pAbc8Aig, fBalance, fUpdateLevel, 1, fVerbose );
+ pAigNew = Dar_ManCompress2( pAbc->pAbc8Aig, fBalance, fUpdateLevel, 1, fPower, fVerbose );
if ( pAigNew == NULL )
{
printf( "Abc_CommandAbc8DC2(): Tranformation of the AIG has failed.\n" );
@@ -18440,10 +19719,11 @@ int Abc_CommandAbc8DC2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( stdout, "usage: *dc2 [-blvh]\n" );
+ fprintf( stdout, "usage: *dc2 [-blpvh]\n" );
fprintf( stdout, "\t performs AIG-based synthesis without deriving choices\n" );
fprintf( stdout, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
fprintf( stdout, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
+ fprintf( stdout, "\t-p : toggle power-aware rewriting [default = %s]\n", fPower? "yes": "no" );
fprintf( stdout, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
return 1;
@@ -18526,7 +19806,7 @@ int Abc_CommandAbc8Strash( Abc_Frame_t * pAbc, int argc, char ** argv )
{
printf( "Abc_CommandAbc8Strash(): There is no mapped network to strash.\n" );
return 1;
- }
+ }
pAigNew = Nwk_ManStrash( pAbc->pAbc8Nwk );
if ( pAigNew == NULL )
@@ -18566,7 +19846,7 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Mfx_ParsDefault( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraesvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCraespvwh" ) ) != EOF )
{
switch ( c )
{
@@ -18648,6 +19928,9 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
pPars->fSwapEdge ^= 1;
break;
+ case 'p':
+ pPars->fPower ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -18687,7 +19970,7 @@ int Abc_CommandAbc8Mfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( stdout, "usage: *mfs [-WFDMLC <num>] [-raesvh]\n" );
+ fprintf( stdout, "usage: *mfs [-WFDMLC <num>] [-raespvh]\n" );
fprintf( stdout, "\t performs don't-care-based optimization of logic networks\n" );
fprintf( stdout, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
fprintf( stdout, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
@@ -18699,6 +19982,7 @@ usage:
fprintf( stdout, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
fprintf( stdout, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
fprintf( stdout, "\t-s : toggle evaluation of edge swapping [default = %s]\n", pPars->fSwapEdge? "yes": "no" );
+ fprintf( stdout, "\t-p : toggle power-aware optimization [default = %s]\n", pPars->fPower? "yes": "no" );
fprintf( stdout, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( stdout, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( stdout, "\t-h : print the command usage\n");
@@ -19624,7 +20908,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
Ssw_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDVMpldvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDVMpldsvh" ) ) != EOF )
{
switch ( c )
{
@@ -19747,6 +21031,9 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
pPars->fDynamic ^= 1;
break;
+ case 's':
+ pPars->fLocalSim ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -19800,7 +21087,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( stdout, "usage: *scorr [-PQFCLNSDVM <num>] [-pldvh]\n" );
+ fprintf( stdout, "usage: *scorr [-PQFCLNSDVM <num>] [-pldsvh]\n" );
fprintf( stdout, "\t performs sequential sweep using K-step induction\n" );
fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -19815,6 +21102,7 @@ usage:
fprintf( stdout, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
fprintf( stdout, "\t-d : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" );
+ fprintf( stdout, "\t-s : toggle local simulation in the cone of influence [default = %s]\n", pPars->fLocalSim? "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;
diff --git a/src/base/abci/abc.zip b/src/base/abci/abc.zip
deleted file mode 100644
index 34df9a63..00000000
--- a/src/base/abci/abc.zip
+++ /dev/null
Binary files differ
diff --git a/src/base/abci/abcBidec.c b/src/base/abci/abcBidec.c
index bb114578..01146014 100644
--- a/src/base/abci/abcBidec.c
+++ b/src/base/abci/abcBidec.c
@@ -42,7 +42,7 @@ static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCo
SeeAlso []
***********************************************************************/
-Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare )
+Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare, float dProb )
{
unsigned * pTruth;
Bdc_Fun_t * pFunc;
@@ -52,8 +52,33 @@ Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pR
pTruth = Hop_ManConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
if ( Hop_IsComplement(pRoot) )
Extra_TruthNot( pTruth, pTruth, nVars );
- // decompose truth table
- Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
+ // perform power-aware decomposition
+ if ( dProb >= 0.0 )
+ {
+ float Prob = (float)2.0 * dProb * (1.0 - dProb);
+ assert( Prob >= 0.0 && Prob <= 0.5 );
+ if ( Prob >= 0.4 )
+ {
+ Extra_TruthNot( puCare, puCare, nVars );
+ if ( dProb > 0.5 ) // more 1s than 0s
+ Extra_TruthOr( pTruth, pTruth, puCare, nVars );
+ else
+ Extra_TruthSharp( pTruth, pTruth, puCare, nVars );
+ Extra_TruthNot( puCare, puCare, nVars );
+ // decompose truth table
+ Bdc_ManDecompose( p, pTruth, NULL, nVars, NULL, 1000 );
+ }
+ else
+ {
+ // decompose truth table
+ Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
+ }
+ }
+ else
+ {
+ // decompose truth table
+ Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
+ }
// convert back into HOP
Bdc_FuncSetCopy( Bdc_ManFunc( p, 0 ), Hop_ManConst1( pHop ) );
for ( i = 0; i < nVars; i++ )
@@ -104,7 +129,7 @@ void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose )
if ( Abc_ObjFaninNum(pObj) > 15 )
continue;
nNodes1 = Hop_DagSize(pObj->pData);
- pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth, NULL );
+ pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth, NULL, -1.0 );
nNodes2 = Hop_DagSize(pObj->pData);
nGainTotal += nNodes1 - nNodes2;
}
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index d38f62d0..1c7459eb 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -39,6 +39,74 @@ static int Abc_NtkComputeArea( Abc_Ntk_t * pNtk, Cut_Man_t * p );
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkCutsSubtractFanunt( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pObj, * pFan0, * pFan1, * pFanC;
+ int i, Counter = 0;
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ if ( !Abc_NodeIsMuxType(pObj) )
+ continue;
+ pFanC = Abc_NodeRecognizeMux( pObj, &pFan1, &pFan0 );
+ pFanC = Abc_ObjRegular(pFanC);
+ pFan0 = Abc_ObjRegular(pFan0);
+ assert( pFanC->vFanouts.nSize > 1 );
+ pFanC->vFanouts.nSize--;
+ Counter++;
+ if ( Abc_NodeIsExorType(pObj) )
+ {
+ assert( pFan0->vFanouts.nSize > 1 );
+ pFan0->vFanouts.nSize--;
+ Counter++;
+ }
+ }
+ printf("Substracted %d fanouts\n", Counter );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkCutsAddFanunt( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pObj, * pFan0, * pFan1, * pFanC;
+ int i, Counter = 0;
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ if ( !Abc_NodeIsMuxType(pObj) )
+ continue;
+ pFanC = Abc_NodeRecognizeMux( pObj, &pFan1, &pFan0 );
+ pFanC = Abc_ObjRegular(pFanC);
+ pFan0 = Abc_ObjRegular(pFan0);
+ pFanC->vFanouts.nSize++;
+ Counter++;
+ if ( Abc_NodeIsExorType(pObj) )
+ {
+ pFan0->vFanouts.nSize++;
+ Counter++;
+ }
+ }
+ printf("Added %d fanouts\n", Counter );
+}
+
+/**Function*************************************************************
+
Synopsis [Computes the cuts for the network.]
Description []
@@ -61,6 +129,9 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk );
extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
+ if ( pParams->fAdjust )
+ Abc_NtkCutsSubtractFanunt( pNtk );
+
nTotal = nGood = nEqual = 0;
assert( Abc_NtkIsStrash(pNtk) );
@@ -118,7 +189,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
Vec_PtrFree( vNodes );
Vec_IntFree( vChoices );
Cut_ManPrintStats( p );
-PRT( "TOTAL ", clock() - clk );
+PRT( "TOTAL", clock() - clk );
printf( "Area = %d.\n", Abc_NtkComputeArea( pNtk, p ) );
//Abc_NtkPrintCuts( p, pNtk, 0 );
// Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
@@ -126,6 +197,8 @@ PRT( "TOTAL ", clock() - clk );
// temporary printout of stats
if ( nTotal )
printf( "Total cuts = %d. Good cuts = %d. Ratio = %5.2f\n", nTotal, nGood, ((double)nGood)/nTotal );
+ if ( pParams->fAdjust )
+ Abc_NtkCutsAddFanunt( pNtk );
return p;
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index dcc7f4c1..9dc10d84 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -29,6 +29,8 @@
#include "dch.h"
#include "ssw.h"
#include "cgt.h"
+#include "cec.h"
+#include "fsim.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -126,7 +128,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
// remove dangling nodes
- nNodes = Aig_ManCleanup( pMan );
+ nNodes = (Abc_NtkGetChoiceNum(pNtk) == 0)? Aig_ManCleanup( pMan ) : 0;
if ( !fExors && nNodes )
printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
//Aig_ManDumpVerilog( pMan, "test.v" );
@@ -153,6 +155,63 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
Synopsis [Converts the network from the AIG manager into ABC.]
+ Description [Assumes that registers are ordered after PIs/POs.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk )
+{
+ Aig_Man_t * pMan;
+ Abc_Obj_t * pObj, * pPrev, * pFanin;
+ Vec_Ptr_t * vNodes;
+ int i;
+ vNodes = Abc_AigDfs( pNtk, 0, 0 );
+ // create the manager
+ pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
+ pMan->pName = Extra_UtilStrsav( pNtk->pName );
+ if ( Abc_NtkGetChoiceNum(pNtk) )
+ {
+ pMan->pEquivs = ALLOC( Aig_Obj_t *, Abc_NtkObjNum(pNtk) );
+ memset( pMan->pEquivs, 0, sizeof(Aig_Obj_t *) * Abc_NtkObjNum(pNtk) );
+ }
+ // transfer the pointers to the basic nodes
+ Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
+ // perform the conversion of the internal nodes (assumes DFS ordering)
+ Vec_PtrForEachEntry( vNodes, pObj, i )
+ {
+ pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) );
+// printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id );
+ if ( Abc_AigNodeIsChoice( pObj ) )
+ {
+ for ( pPrev = pObj, pFanin = pObj->pData; pFanin; pPrev = pFanin, pFanin = pFanin->pData )
+ Aig_ObjSetEquiv( pMan, (Aig_Obj_t *)pPrev->pCopy, (Aig_Obj_t *)pFanin->pCopy );
+// Aig_ManCreateChoice( pIfMan, (Aig_Obj_t *)pNode->pCopy );
+ }
+ }
+ Vec_PtrFree( vNodes );
+ // create the POs
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
+ // complement the 1-valued registers
+ Aig_ManSetRegNum( pMan, 0 );
+ if ( !Aig_ManCheck( pMan ) )
+ {
+ printf( "Abc_NtkToDar: AIG check has failed.\n" );
+ Aig_ManStop( pMan );
+ return NULL;
+ }
+ return pMan;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts the network from the AIG manager into ABC.]
+
Description []
SideEffects []
@@ -351,6 +410,9 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
assert( pMan->nAsserts == 0 );
// perform strashing
pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+ // duplicate the name and the spec
+// pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
+// pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
// create PIs
Aig_ManForEachPiSeq( pMan, pObj, i )
@@ -771,7 +833,7 @@ clk = clock();
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fVerbose )
+Abc_Ntk_t * Abc_NtkDC2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose )
{
Aig_Man_t * pMan, * pTemp;
Abc_Ntk_t * pNtkAig;
@@ -783,7 +845,7 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel,
// Aig_ManPrintStats( pMan );
clk = clock();
- pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fVerbose );
+ pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fFanout, fPower, fVerbose );
Aig_ManStop( pTemp );
//PRT( "time", clock() - clk );
@@ -832,7 +894,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
***********************************************************************/
Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
{
- extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+ extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
Vec_Ptr_t * vAigs;
Aig_Man_t * pMan, * pTemp;
@@ -845,8 +907,8 @@ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
clk = clock();
if ( pPars->fSynthesis )
{
-// vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fVerbose );
- vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, 0 );
+// vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fVerbose );
+ vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
Aig_ManStop( pMan );
}
else
@@ -1191,6 +1253,81 @@ 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 );
+ // 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. " );
+PRT( "Time", clock() - clkTotal );
+ }
+ else if ( RetValue == 0 )
+ {
+ printf( "Networks are NOT EQUIVALENT. " );
+PRT( "Time", clock() - clkTotal );
+ }
+ else
+ {
+ printf( "Networks are UNDECIDED. " );
+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;
@@ -1282,7 +1419,7 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig )
if ( pRepr == NULL )
{
// printf("Nothing equivalent to flop %s\n", pFlopName);
- p_irrelevant[i] = true;
+// p_irrelevant[i] = true;
continue;
}
@@ -1600,7 +1737,7 @@ PRT( "Time", clock() - clk );
***********************************************************************/
int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
{
- Aig_Man_t * pMan, * pPart0, * pPart1, * pMiter;
+ Aig_Man_t * pMan, * pPart0, * pPart1;//, * pMiter;
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
@@ -1608,7 +1745,8 @@ int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
printf( "Converting network into AIG has failed.\n" );
return 0;
}
- if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
+// if ( !Saig_ManDemiterSimple( pMan, &pPart0, &pPart1 ) )
+ if ( !Saig_ManDemiterSimpleDiff( pMan, &pPart0, &pPart1 ) )
{
printf( "Demitering has failed.\n" );
return 0;
@@ -1617,10 +1755,10 @@ int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk )
Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
// create two-level miter
- pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
- Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
- Aig_ManStop( pMiter );
- printf( "The new miter is written into file \"%s\".\n", "miter01.blif" );
+// pMiter = Saig_ManCreateMiterTwo( pPart0, pPart1, 2 );
+// Aig_ManDumpBlif( pMiter, "miter01.blif", NULL, NULL );
+// Aig_ManStop( pMiter );
+// printf( "The new miter is written into file \"%s\".\n", "miter01.blif" );
Aig_ManStop( pPart0 );
Aig_ManStop( pPart1 );
@@ -1761,7 +1899,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
return 1;
}
- // commented out because something became non-inductive
+ // commented out because sometimes the problem became non-inductive
/*
// preprocess the miter by fraiging it
// (note that for each functional class, fraiging leaves one representative;
@@ -1805,6 +1943,146 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
return RetValue;
}
+
+/**Function*************************************************************
+
+ Synopsis [Performs BDD-based reachability analysis.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkDarAbSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose )
+{
+ Aig_Man_t * pMan1, * pMan2 = NULL;
+ int RetValue;
+ // derive AIG manager
+ pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
+ if ( pMan1 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( Aig_ManRegNum(pMan1) > 0 );
+ // derive AIG manager
+ if ( pNtk2 )
+ {
+ pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
+ if ( pMan2 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( Aig_ManRegNum(pMan2) > 0 );
+ }
+
+ // perform verification
+ RetValue = Ssw_SecSpecialMiter( pMan1, pMan2, nFrames, fVerbose );
+ Aig_ManStop( pMan1 );
+ if ( pMan2 )
+ Aig_ManStop( pMan2 );
+ return RetValue;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkDarSimSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Ssw_Pars_t * pPars )
+{
+ Aig_Man_t * pMan1, * pMan2 = NULL;
+ int RetValue;
+ // derive AIG manager
+ pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
+ if ( pMan1 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( Aig_ManRegNum(pMan1) > 0 );
+ // derive AIG manager
+ if ( pNtk2 )
+ {
+ pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
+ if ( pMan2 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( Aig_ManRegNum(pMan2) > 0 );
+ }
+
+ // perform verification
+ RetValue = Ssw_SecWithSimilarity( pMan1, pMan2, pPars );
+ Aig_ManStop( pMan1 );
+ if ( pMan2 )
+ Aig_ManStop( pMan2 );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarMatch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nDist, int fVerbose )
+{
+ extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan1, * pMan2 = NULL, * pManRes;
+ Vec_Int_t * vPairs;
+ assert( Abc_NtkIsStrash(pNtk1) );
+ // derive AIG manager
+ pMan1 = Abc_NtkToDar( pNtk1, 0, 1 );
+ if ( pMan1 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return NULL;
+ }
+ assert( Aig_ManRegNum(pMan1) > 0 );
+ // derive AIG manager
+ if ( pNtk2 )
+ {
+ pMan2 = Abc_NtkToDar( pNtk2, 0, 1 );
+ if ( pMan2 == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return NULL;
+ }
+ assert( Aig_ManRegNum(pMan2) > 0 );
+ }
+
+ // perform verification
+ vPairs = Saig_StrSimPerformMatching( pMan1, pMan2, nDist, 1, &pManRes );
+ pNtkAig = Abc_NtkFromAigPhase( pManRes );
+ if ( vPairs )
+ Vec_IntFree( vPairs );
+ if ( pManRes )
+ Aig_ManStop( pManRes );
+ Aig_ManStop( pMan1 );
+ if ( pMan2 )
+ Aig_ManStop( pMan2 );
+ return pNtkAig;
+}
+
+
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
@@ -2049,33 +2327,140 @@ Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int
SeeAlso []
***********************************************************************/
-int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
+int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, int fNew, int fComb, int fMiter, int fVerbose )
{
+ extern int Cec_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
+ extern int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose );
Aig_Man_t * pMan;
- Fra_Sml_t * pSml;
Fra_Cex_t * pCex;
- int RetValue, clk = clock();
+ int status, RetValue, clk = clock();
pMan = Abc_NtkToDar( pNtk, 0, 1 );
- pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords );
- if ( pSml->fNonConstOut )
+ if ( fComb || Abc_NtkLatchNum(pNtk) == 0 )
{
- pCex = Fra_SmlGetCounterExample( pSml );
- if ( pCex )
- printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ if ( Cec_ManSimulate( pMan, nWords, nFrames, TimeOut, fMiter, fVerbose ) )
+ {
+ pCex = pMan->pSeqModel;
+ if ( pCex )
+ {
+ printf( "Simulation iterated %d times with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
- FREE( pNtk->pModel );
- FREE( pNtk->pSeqModel );
- pNtk->pSeqModel = pCex;
- RetValue = 1;
+ status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ if ( status == 0 )
+ printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+ }
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pCex;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation iterated %d times with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
+ }
+ else if ( fNew )
+ {
+/*
+ if ( Raig_ManSimulate( pMan, nWords, nFrames, TimeOut, fVerbose ) )
+ {
+ if ( (pCex = pMan->pSeqModel) )
+ {
+ printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ nFrames, nWords, pCex->iPo, pCex->iFrame );
+ status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ if ( status == 0 )
+ printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+ }
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation of %d frames with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
+*/
+ Fsim_ParSim_t Pars, * pPars = &Pars;
+ Fsim_ManSetDefaultParamsSim( pPars );
+ pPars->nWords = nWords;
+ pPars->nIters = nFrames;
+ pPars->TimeLimit = TimeOut;
+ pPars->fCheckMiter = fMiter;
+ pPars->fVerbose = fVerbose;
+ if ( Fsim_ManSimulate( pMan, pPars ) )
+ {
+ if ( (pCex = pMan->pSeqModel) )
+ {
+ printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ nFrames, nWords, pCex->iPo, pCex->iFrame );
+ status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ if ( status == 0 )
+ printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+ }
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation of %d frames with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
}
else
{
- RetValue = 0;
- printf( "Simulation of %d frames with %d words did not assert the outputs. ",
- nFrames, nWords );
+/*
+ Fra_Sml_t * pSml;
+ pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords );
+ if ( pSml->fNonConstOut )
+ {
+ pCex = Fra_SmlGetCounterExample( pSml );
+ if ( pCex )
+ printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ nFrames, nWords, pCex->iPo, pCex->iFrame );
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pCex;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation of %d frames with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
+ Fra_SmlStop( pSml );
+*/
+ if ( Raig_ManSimulate( pMan, nWords, nFrames, TimeOut, fMiter, fVerbose ) )
+ {
+ if ( (pCex = pMan->pSeqModel) )
+ {
+ printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ nFrames, nWords, pCex->iPo, pCex->iFrame );
+ status = Ssw_SmlRunCounterExample( pMan, (Ssw_Cex_t *)pCex );
+ if ( status == 0 )
+ printf( "Abc_NtkDarSeqSim(): Counter-example verification has FAILED.\n" );
+ }
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pCex; pMan->pSeqModel = NULL;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation of %d frames with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
}
PRT( "Time", clock() - clk );
- Fra_SmlStop( pSml );
Aig_ManStop( pMan );
return RetValue;
}
@@ -2200,14 +2585,20 @@ Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConf
return NULL;
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, fVerbose );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fDynamic, fExtend, 0, fVerbose );
+ if ( pTemp->pSeqModel )
+ {
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
+ pNtk->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+ }
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkFromAigPhase( pMan );
- pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
- pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+// pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+// pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
}
@@ -2480,8 +2871,8 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkFromAigPhase( pMan );
- pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
- pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+// pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+// pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
Aig_ManStop( pMan );
return pNtkAig;
}
@@ -2545,8 +2936,8 @@ Abc_Ntk_t * Abc_NtkDarSynch( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nWords, i
if ( pMan == NULL )
return NULL;
pNtkAig = Abc_NtkFromAigPhase( pMan );
- pNtkAig->pName = Extra_UtilStrsav("miter");
- pNtkAig->pSpec = NULL;
+// pNtkAig->pName = Extra_UtilStrsav("miter");
+// pNtkAig->pSpec = NULL;
Aig_ManStop( pMan );
return pNtkAig;
}
@@ -2600,6 +2991,129 @@ Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t
SeeAlso []
***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarExtWin( Abc_Ntk_t * pNtk, int nObjId, int nDist, int fVerbose )
+{
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan1, * pMan;
+ Aig_Obj_t * pObj;
+ pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan1 == NULL )
+ return NULL;
+ if ( nObjId == -1 )
+ {
+ pObj = Saig_ManFindPivot( pMan1 );
+ printf( "Selected object %d as a window pivot.\n", pObj->Id );
+ }
+ else
+ {
+ if ( nObjId >= Aig_ManObjNumMax(pMan1) )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "The ID is too large.\n" );
+ return NULL;
+ }
+ pObj = Aig_ManObj( pMan1, nObjId );
+ if ( pObj == NULL )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "Object with ID %d does not exist.\n", nObjId );
+ return NULL;
+ }
+ if ( !Saig_ObjIsLo(pMan1, pObj) && !Aig_ObjIsNode(pObj) )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "Object with ID %d is not a node or reg output.\n", nObjId );
+ return NULL;
+ }
+ }
+ pMan = Saig_ManWindowExtract( pMan1, pObj, nDist );
+ Aig_ManStop( pMan1 );
+ if ( pMan == NULL )
+ return NULL;
+ pNtkAig = Abc_NtkFromAigPhase( pMan );
+ pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+ pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs phase abstraction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarInsWin( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, int nObjId, int nDist, int fVerbose )
+{
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan1, * pMan2 = NULL, * pMan;
+ Aig_Obj_t * pObj;
+ pMan1 = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan1 == NULL )
+ return NULL;
+ if ( nObjId == -1 )
+ {
+ pObj = Saig_ManFindPivot( pMan1 );
+ printf( "Selected object %d as a window pivot.\n", pObj->Id );
+ }
+ else
+ {
+ if ( nObjId >= Aig_ManObjNumMax(pMan1) )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "The ID is too large.\n" );
+ return NULL;
+ }
+ pObj = Aig_ManObj( pMan1, nObjId );
+ if ( pObj == NULL )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "Object with ID %d does not exist.\n", nObjId );
+ return NULL;
+ }
+ if ( !Saig_ObjIsLo(pMan1, pObj) && !Aig_ObjIsNode(pObj) )
+ {
+ Aig_ManStop( pMan1 );
+ printf( "Object with ID %d is not a node or reg output.\n", nObjId );
+ return NULL;
+ }
+ }
+ if ( pCare )
+ {
+ pMan2 = Abc_NtkToDar( pCare, 0, 0 );
+ if ( pMan2 == NULL )
+ {
+ Aig_ManStop( pMan1 );
+ return NULL;
+ }
+ }
+ pMan = Saig_ManWindowInsert( pMan1, pObj, nDist, pMan2 );
+ Aig_ManStop( pMan1 );
+ if ( pMan2 )
+ Aig_ManStop( pMan2 );
+ if ( pMan == NULL )
+ return NULL;
+ pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs phase abstraction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fInit, int fVerbose )
{
Abc_Ntk_t * pNtkAig;
@@ -2680,6 +3194,112 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
Aig_ManStop( pMan );
}
+#include "amap.h"
+#include "mio.h"
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Amap_ManProduceNetwork( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMapping )
+{
+ extern void * Abc_FrameReadLibGen();
+ Mio_Library_t * pLib = Abc_FrameReadLibGen();
+ Amap_Out_t * pRes;
+ Vec_Ptr_t * vNodesNew;
+ Abc_Ntk_t * pNtkNew;
+ Abc_Obj_t * pNodeNew, * pFaninNew;
+ int i, k, iPis, iPos, nDupGates;
+ // make sure gates exist in the current library
+ Vec_PtrForEachEntry( vMapping, pRes, i )
+ if ( pRes->pName && Mio_LibraryReadGateByName( pLib, pRes->pName ) == NULL )
+ {
+ printf( "Current library does not contain gate \"%s\".\n", pRes->pName );
+ return NULL;
+ }
+ // create the network
+ pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
+ pNtkNew->pManFunc = pLib;
+ iPis = iPos = 0;
+ vNodesNew = Vec_PtrAlloc( Vec_PtrSize(vMapping) );
+ Vec_PtrForEachEntry( vMapping, pRes, i )
+ {
+ if ( pRes->Type == -1 )
+ pNodeNew = Abc_NtkCi( pNtkNew, iPis++ );
+ else if ( pRes->Type == 1 )
+ pNodeNew = Abc_NtkCo( pNtkNew, iPos++ );
+ else
+ {
+ pNodeNew = Abc_NtkCreateNode( pNtkNew );
+ pNodeNew->pData = Mio_LibraryReadGateByName( pLib, pRes->pName );
+ }
+ for ( k = 0; k < pRes->nFans; k++ )
+ {
+ pFaninNew = Vec_PtrEntry( vNodesNew, pRes->pFans[k] );
+ Abc_ObjAddFanin( pNodeNew, pFaninNew );
+ }
+ Vec_PtrPush( vNodesNew, pNodeNew );
+ }
+ Vec_PtrFree( vNodesNew );
+ assert( iPis == Abc_NtkCiNum(pNtkNew) );
+ assert( iPos == Abc_NtkCoNum(pNtkNew) );
+ // decouple the PO driver nodes to reduce the number of levels
+ nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
+// if ( nDupGates && Map_ManReadVerbose(pMan) )
+// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
+ return pNtkNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars )
+{
+ Vec_Ptr_t * vMapping;
+ Abc_Ntk_t * pNtkAig = NULL;
+ Aig_Man_t * pMan;
+ Aig_MmFlex_t * pMem;
+
+ assert( Abc_NtkIsStrash(pNtk) );
+ // convert to the AIG manager
+ pMan = Abc_NtkToDarChoices( pNtk );
+ if ( pMan == NULL )
+ return NULL;
+
+ // perform computation
+ vMapping = Amap_ManTest( pMan, pPars );
+ Aig_ManStop( pMan );
+ if ( vMapping == NULL )
+ return NULL;
+ pMem = Vec_PtrPop( vMapping );
+ pNtkAig = Amap_ManProduceNetwork( pNtk, vMapping );
+ Aig_MmFlexStop( pMem, 0 );
+ Vec_PtrFree( vMapping );
+
+ // make sure everything is okay
+ if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) )
+ {
+ printf( "Abc_NtkDar: The network check has failed.\n" );
+ Abc_NtkDelete( pNtkAig );
+ return NULL;
+ }
+ return pNtkAig;
+}
/**Function*************************************************************
@@ -2694,9 +3314,10 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
***********************************************************************/
void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
{
-// extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
-
- Aig_Man_t * pMan;//, * pTemp;
+ extern void Fsim_ManTest( Aig_Man_t * pAig );
+ extern Vec_Int_t * Saig_StrSimPerformMatching( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose, Aig_Man_t ** ppMiter );
+// Vec_Int_t * vPairs;
+ Aig_Man_t * pMan;//, * pMan2;//, * pTemp;
assert( Abc_NtkIsStrash(pNtk) );
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
@@ -2714,9 +3335,21 @@ Aig_ManPrintStats( pMan );
pTemp = Ssw_SignalCorrespondeceTestPairs( pMan );
Aig_ManStop( pTemp );
*/
- Ssw_SecSpecialMiter( pMan, 1 );
+/*
+// Ssw_SecSpecialMiter( pMan, NULL, 2, 1 );
+ pMan2 = Aig_ManDupSimple(pMan);
+ vPairs = Saig_StrSimPerformMatching( pMan, pMan2, 0, 1, NULL );
+ Vec_IntFree( vPairs );
Aig_ManStop( pMan );
+ Aig_ManStop( pMan2 );
+*/
+
+// Saig_MvManSimulate( pMan, 1 );
+
+ Fsim_ManTest( pMan );
+ Aig_ManStop( pMan );
+
}
/**Function*************************************************************
@@ -2732,6 +3365,8 @@ Aig_ManPrintStats( pMan );
***********************************************************************/
Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
{
+ extern Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter );
+
/*
extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig );
@@ -2760,9 +3395,16 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return NULL;
+/*
+ Aig_ManSetRegNum( pMan, pMan->nRegs );
+ pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, 1 );
+ Aig_ManStop( pTemp );
+ if ( pMan == NULL )
+ return NULL;
+*/
Aig_ManSetRegNum( pMan, pMan->nRegs );
- pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 0, 0, 1 );
+ pMan = Saig_ManDualRail( pTemp = pMan, 1 );
Aig_ManStop( pTemp );
if ( pMan == NULL )
return NULL;
diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c
index 91f175fa..847c7f1b 100644
--- a/src/base/abci/abcDelay.c
+++ b/src/base/abci/abcDelay.c
@@ -20,6 +20,7 @@
#include "abc.h"
#include "if.h"
+#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -652,6 +653,302 @@ Abc_Ntk_t * Abc_NtkSpeedup( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, in
return pNtkNew;
}
+/**Function*************************************************************
+
+ Synopsis [Marks nodes for power-optimization.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkPowerEstimate( Abc_Ntk_t * pNtk, int fProbOne )
+{
+ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+ extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
+ Vec_Int_t * vProbs;
+ Vec_Int_t * vSwitching;
+ float * pProbability;
+ float * pSwitching;
+ Abc_Ntk_t * pNtkStr;
+ Aig_Man_t * pAig;
+ Aig_Obj_t * pObjAig;
+ Abc_Obj_t * pObjAbc, * pObjAbc2;
+ int i;
+ // start the resulting array
+ vProbs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
+ pProbability = (float *)vProbs->pArray;
+ // strash the network
+ pNtkStr = Abc_NtkStrash( pNtk, 0, 1, 0 );
+ Abc_NtkForEachObj( pNtk, pObjAbc, i )
+ if ( Abc_ObjRegular(pObjAbc->pTemp)->Type == ABC_FUNC_NONE )
+ pObjAbc->pTemp = NULL;
+ // map network into an AIG
+ pAig = Abc_NtkToDar( pNtkStr, 0, (int)(Abc_NtkLatchNum(pNtk) > 0) );
+ vSwitching = Saig_ManComputeSwitchProbs( pAig, 48, 16, fProbOne );
+ pSwitching = (float *)vSwitching->pArray;
+ Abc_NtkForEachObj( pNtk, pObjAbc, i )
+ {
+ if ( (pObjAbc2 = Abc_ObjRegular(pObjAbc->pTemp)) && (pObjAig = pObjAbc2->pTemp) )
+ pProbability[pObjAbc->Id] = pSwitching[pObjAig->Id];
+ }
+ Vec_IntFree( vSwitching );
+ Aig_ManStop( pAig );
+ Abc_NtkDelete( pNtkStr );
+ return vProbs;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks nodes for power-optimization.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPowerPrint( Abc_Ntk_t * pNtk, Vec_Int_t * vProbs )
+{
+ Abc_Obj_t * pObj;
+ float * pProb, TotalProb = 0.0, ProbThis, Probs[5] = {0.0};
+ int i, nNodes = 0, nEdges = 0, Counter[5] = {0};
+ pProb = (float *)vProbs->pArray;
+ assert( Vec_IntSize(vProbs) >= Abc_NtkObjNumMax(pNtk) );
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ if ( !Abc_ObjIsNode(pObj) && !Abc_ObjIsPi(pObj) )
+ continue;
+ nNodes++;
+ nEdges += Abc_ObjFanoutNum(pObj);
+ ProbThis = pProb[i] * Abc_ObjFanoutNum(pObj);
+ TotalProb += ProbThis;
+ assert( pProb[i] >= 0.0 && pProb[i] <= 0.5 );
+ if ( pProb[i] >= 0.4 )
+ {
+ Counter[4]++;
+ Probs[4] += ProbThis;
+ }
+ else if ( pProb[i] >= 0.3 )
+ {
+ Counter[3]++;
+ Probs[3] += ProbThis;
+ }
+ else if ( pProb[i] >= 0.2 )
+ {
+ Counter[2]++;
+ Probs[2] += ProbThis;
+ }
+ else if ( pProb[i] >= 0.1 )
+ {
+ Counter[1]++;
+ Probs[1] += ProbThis;
+ }
+ else
+ {
+ Counter[0]++;
+ Probs[0] += ProbThis;
+ }
+ }
+ printf( "Node distribution: " );
+ for ( i = 0; i < 5; i++ )
+ printf( "n%d%d = %6.2f%% ", i, i+1, 100.0 * Counter[i]/nNodes );
+ printf( "\n" );
+ printf( "Power distribution: " );
+ for ( i = 0; i < 5; i++ )
+ printf( "p%d%d = %6.2f%% ", i, i+1, 100.0 * Probs[i]/TotalProb );
+ printf( "\n" );
+ printf( "Total probs = %7.2f. ", TotalProb );
+ printf( "Total edges = %d. ", nEdges );
+ printf( "Average = %7.2f. ", TotalProb / nEdges );
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Determines timing-critical edges of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned Abc_NtkPowerCriticalEdges( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, float Limit, Vec_Int_t * vProbs )
+{
+ Abc_Obj_t * pFanin;
+ float * pProb = (float *)vProbs->pArray;
+ unsigned uResult = 0;
+ int k;
+ Abc_ObjForEachFanin( pNode, pFanin, k )
+ if ( pProb[pFanin->Id] >= Limit )
+ uResult |= (1 << k);
+ return uResult;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds choices to speed up the network by the given percentage.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkPowerdown( Abc_Ntk_t * pNtk, int fUseLutLib, int Percentage, int Degree, int fVerbose, int fVeryVerbose )
+{
+ Abc_Ntk_t * pNtkNew;
+ Vec_Int_t * vProbs;
+ Vec_Ptr_t * vTimeCries, * vTimeFanins;
+ Abc_Obj_t * pNode, * pFanin, * pFanin2;
+ float * pProb, Limit;
+ int i, k, k2, Counter, CounterRes, nTimeCris;
+ unsigned * puPCEdges;
+ // compute the limit
+ Limit = 0.5 - (1.0 * Percentage / 100);
+ // perform computation of switching probability
+ vProbs = Abc_NtkPowerEstimate( pNtk, 0 );
+ pProb = (float *)vProbs->pArray;
+ // compute percentage of wires of each type
+ if ( fVerbose )
+ Abc_NtkPowerPrint( pNtk, vProbs );
+ // mark the power critical nodes and edges
+ puPCEdges = ALLOC( unsigned, Abc_NtkObjNumMax(pNtk) );
+ memset( puPCEdges, 0, sizeof(unsigned) * Abc_NtkObjNumMax(pNtk) );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ if ( pProb[pNode->Id] < Limit )
+ continue;
+ puPCEdges[pNode->Id] = Abc_NtkPowerCriticalEdges( pNtk, pNode, Limit, vProbs );
+ }
+/*
+ if ( fVerbose )
+ {
+ Counter = CounterRes = 0;
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ Counter += Abc_ObjFaninNum(pNode);
+ CounterRes += Extra_WordCountOnes( puPCEdges[pNode->Id] );
+ }
+ printf( "Edges: Total = %7d. Critical = %7d. Ratio = %4.2f\n",
+ Counter, CounterRes, 1.0*CounterRes/Counter );
+ }
+*/
+ // start the resulting network
+ pNtkNew = Abc_NtkStrash( pNtk, 0, 1, 0 );
+
+ // collect nodes to be used for resynthesis
+ Counter = CounterRes = 0;
+ vTimeCries = Vec_PtrAlloc( 16 );
+ vTimeFanins = Vec_PtrAlloc( 16 );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+// if ( pProb[pNode->Id] < Limit )
+// continue;
+ // count the number of non-PI power-critical nodes
+ nTimeCris = 0;
+ Abc_ObjForEachFanin( pNode, pFanin, k )
+ if ( !Abc_ObjIsCi(pFanin) && (puPCEdges[pNode->Id] & (1<<k)) )
+ nTimeCris++;
+ if ( !fVeryVerbose && nTimeCris == 0 )
+ continue;
+ Counter++;
+ // count the total number of power-critical second-generation nodes
+ Vec_PtrClear( vTimeCries );
+ if ( nTimeCris )
+ {
+ Abc_ObjForEachFanin( pNode, pFanin, k )
+ if ( !Abc_ObjIsCi(pFanin) && (puPCEdges[pNode->Id] & (1<<k)) )
+ Abc_ObjForEachFanin( pFanin, pFanin2, k2 )
+ if ( puPCEdges[pFanin->Id] & (1<<k2) )
+ Vec_PtrPushUnique( vTimeCries, pFanin2 );
+ }
+// if ( !fVeryVerbose && (Vec_PtrSize(vTimeCries) == 0 || Vec_PtrSize(vTimeCries) > Degree) )
+ if ( (Vec_PtrSize(vTimeCries) == 0 || Vec_PtrSize(vTimeCries) > Degree) )
+ continue;
+ CounterRes++;
+ // collect second generation nodes
+ Vec_PtrClear( vTimeFanins );
+ Abc_ObjForEachFanin( pNode, pFanin, k )
+ {
+ if ( Abc_ObjIsCi(pFanin) )
+ Vec_PtrPushUnique( vTimeFanins, pFanin );
+ else
+ Abc_ObjForEachFanin( pFanin, pFanin2, k2 )
+ Vec_PtrPushUnique( vTimeFanins, pFanin2 );
+ }
+ // print the results
+ if ( fVeryVerbose )
+ {
+ printf( "%5d Node %5d : %d %2d %2d ", Counter, pNode->Id,
+ nTimeCris, Vec_PtrSize(vTimeCries), Vec_PtrSize(vTimeFanins) );
+ Abc_ObjForEachFanin( pNode, pFanin, k )
+ printf( "%d(%.2f)%s ", pFanin->Id, pProb[pFanin->Id], (puPCEdges[pNode->Id] & (1<<k))? "*":"" );
+ printf( "\n" );
+ }
+ // add the node to choices
+ if ( Vec_PtrSize(vTimeCries) == 0 || Vec_PtrSize(vTimeCries) > Degree )
+ continue;
+ // order the fanins in the increasing order of criticalily
+ if ( Vec_PtrSize(vTimeCries) > 1 )
+ {
+ pFanin = Vec_PtrEntry( vTimeCries, 0 );
+ pFanin2 = Vec_PtrEntry( vTimeCries, 1 );
+// if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) )
+ if ( pProb[pFanin->Id] > pProb[pFanin2->Id] )
+ {
+ Vec_PtrWriteEntry( vTimeCries, 0, pFanin2 );
+ Vec_PtrWriteEntry( vTimeCries, 1, pFanin );
+ }
+ }
+ if ( Vec_PtrSize(vTimeCries) > 2 )
+ {
+ pFanin = Vec_PtrEntry( vTimeCries, 1 );
+ pFanin2 = Vec_PtrEntry( vTimeCries, 2 );
+// if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) )
+ if ( pProb[pFanin->Id] > pProb[pFanin2->Id] )
+ {
+ Vec_PtrWriteEntry( vTimeCries, 1, pFanin2 );
+ Vec_PtrWriteEntry( vTimeCries, 2, pFanin );
+ }
+ pFanin = Vec_PtrEntry( vTimeCries, 0 );
+ pFanin2 = Vec_PtrEntry( vTimeCries, 1 );
+// if ( Abc_ObjSlack(pFanin) < Abc_ObjSlack(pFanin2) )
+ if ( pProb[pFanin->Id] > pProb[pFanin2->Id] )
+ {
+ Vec_PtrWriteEntry( vTimeCries, 0, pFanin2 );
+ Vec_PtrWriteEntry( vTimeCries, 1, pFanin );
+ }
+ }
+ // add choice
+ Abc_NtkSpeedupNode( pNtk, pNtkNew, pNode, vTimeFanins, vTimeCries );
+ }
+ Vec_PtrFree( vTimeCries );
+ Vec_PtrFree( vTimeFanins );
+ free( puPCEdges );
+ if ( fVerbose )
+ printf( "Nodes: Total = %7d. Power-critical = %7d. Workable = %7d. Ratio = %4.2f\n",
+ Abc_NtkNodeNum(pNtk), Counter, CounterRes, 1.0*CounterRes/Counter );
+
+ // remove invalid choice nodes
+ Abc_AigForEachAnd( pNtkNew, pNode, i )
+ if ( pNode->pData )
+ {
+ if ( Abc_ObjFanoutNum(pNode->pData) > 0 )
+ pNode->pData = NULL;
+ }
+
+ // return the result
+ Vec_IntFree( vProbs );
+ return pNtkNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 751e2b2f..c5d9ada7 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -51,6 +51,59 @@ extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
SeeAlso []
***********************************************************************/
+void Abc_NtkIfComputeSwitching( Abc_Ntk_t * pNtk, If_Man_t * pIfMan )
+{
+ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+ extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
+ Vec_Int_t * vSwitching;
+ float * pSwitching;
+ Abc_Obj_t * pObjAbc;
+ Aig_Obj_t * pObjAig;
+ Aig_Man_t * pAig;
+ If_Obj_t * pObjIf;
+ int i, clk = clock();
+ // map IF objects into old network
+ Abc_NtkForEachObj( pNtk, pObjAbc, i )
+ if ( (pObjIf = pObjAbc->pTemp) )
+ pObjIf->pCopy = pObjAbc;
+ // map network into an AIG
+ pAig = Abc_NtkToDar( pNtk, 0, 0 );
+ vSwitching = Saig_ManComputeSwitchProbs( pAig, 48, 16, 0 );
+ pSwitching = (float *)vSwitching->pArray;
+ Abc_NtkForEachObj( pNtk, pObjAbc, i )
+ if ( (pObjAig = pObjAbc->pTemp) )
+ {
+ pObjAbc->dTemp = pSwitching[pObjAig->Id];
+ // J. Anderson and F. N. Najm, “Power-Aware Technology Mapping for LUT-Based FPGAs,”
+ // IEEE Intl. Conf. on Field-Programmable Technology, 2002.
+// pObjAbc->dTemp = (1.55 + 1.05 / (float) Abc_ObjFanoutNum(pObjAbc)) * pSwitching[pObjAig->Id];
+ }
+ Vec_IntFree( vSwitching );
+ Aig_ManStop( pAig );
+ // compute switching for the IF objects
+ assert( pIfMan->vSwitching == NULL );
+ pIfMan->vSwitching = Vec_IntStart( If_ManObjNum(pIfMan) );
+ pSwitching = (float *)pIfMan->vSwitching->pArray;
+ If_ManForEachObj( pIfMan, pObjIf, i )
+ if ( (pObjAbc = pObjIf->pCopy) )
+ pSwitching[i] = pObjAbc->dTemp;
+if ( pIfMan->pPars->fVerbose )
+{
+ PRT( "Computing switching activity", clock() - clk );
+}
+}
+
+/**Function*************************************************************
+
+ Synopsis [Interface with the FPGA mapping package.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
{
Abc_Ntk_t * pNtkNew;
@@ -74,6 +127,8 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
pIfMan = Abc_NtkToIf( pNtk, pPars );
if ( pIfMan == NULL )
return NULL;
+ if ( pPars->fPower )
+ Abc_NtkIfComputeSwitching( pNtk, pIfMan );
if ( !If_ManPerformMapping( pIfMan ) )
{
If_ManStop( pIfMan );
@@ -133,6 +188,7 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
1.0 * Abc_NtkObjNum(pNtk) * pIfMan->nObjBytes / (1<<30), Abc_NtkObjNum(pNtk) );
// create PIs and remember them in the old nodes
+ Abc_NtkCleanCopy( pNtk );
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)If_ManConst1( pIfMan );
Abc_NtkForEachCi( pNtk, pNode, i )
{
@@ -165,7 +221,7 @@ If_Man_t * Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
// set the primary outputs without copying the phase
Abc_NtkForEachCo( pNtk, pNode, i )
- If_ManCreateCo( pIfMan, If_NotCond( (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
+ pNode->pCopy = (Abc_Obj_t *)If_ManCreateCo( pIfMan, If_NotCond( (If_Obj_t *)Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
return pIfMan;
}
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index d0bce990..3a454fc0 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -61,7 +61,7 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
Map_Man_t * pMan;
Vec_Int_t * vSwitching = NULL;
float * pSwitching = NULL;
- int clk;
+ int clk, clkTotal = clock();
assert( Abc_NtkIsStrash(pNtk) );
@@ -115,6 +115,10 @@ clk = clock();
if ( pNtk->pExdc )
pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+if ( fVerbose )
+{
+PRT( "Total runtime", clock() - clkTotal );
+}
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkNew ) )
diff --git a/src/base/abci/abcMerge.c b/src/base/abci/abcMerge.c
new file mode 100644
index 00000000..25a4f02e
--- /dev/null
+++ b/src/base/abci/abcMerge.c
@@ -0,0 +1,352 @@
+/**CFile****************************************************************
+
+ FileName [abcMerge.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [LUT merging algorithm.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "aig.h"
+#include "nwkMerge.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Marks the fanins of the node with the current trav ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkMarkFanins_rec( Abc_Obj_t * pLut, int nLevMin )
+{
+ Abc_Obj_t * pNext;
+ int i;
+ if ( !Abc_ObjIsNode(pLut) )
+ return;
+ if ( Abc_NodeIsTravIdCurrent( pLut ) )
+ return;
+ Abc_NodeSetTravIdCurrent( pLut );
+ if ( Abc_ObjLevel(pLut) < nLevMin )
+ return;
+ Abc_ObjForEachFanin( pLut, pNext, i )
+ Abc_NtkMarkFanins_rec( pNext, nLevMin );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the fanouts of the node with the current trav ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkMarkFanouts_rec( Abc_Obj_t * pLut, int nLevMax, int nFanMax )
+{
+ Abc_Obj_t * pNext;
+ int i;
+ if ( !Abc_ObjIsNode(pLut) )
+ return;
+ if ( Abc_NodeIsTravIdCurrent( pLut ) )
+ return;
+ Abc_NodeSetTravIdCurrent( pLut );
+ if ( Abc_ObjLevel(pLut) > nLevMax )
+ return;
+ if ( Abc_ObjFanoutNum(pLut) > nFanMax )
+ return;
+ Abc_ObjForEachFanout( pLut, pNext, i )
+ Abc_NtkMarkFanouts_rec( pNext, nLevMax, nFanMax );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the circle of nodes around the given set.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkCollectCircle( Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, int nFanMax )
+{
+ Abc_Obj_t * pObj, * pNext;
+ int i, k;
+ Vec_PtrClear( vNext );
+ Vec_PtrForEachEntry( vStart, pObj, i )
+ {
+ Abc_ObjForEachFanin( pObj, pNext, k )
+ {
+ if ( !Abc_ObjIsNode(pNext) )
+ continue;
+ if ( Abc_NodeIsTravIdCurrent( pNext ) )
+ continue;
+ Abc_NodeSetTravIdCurrent( pNext );
+ Vec_PtrPush( vNext, pNext );
+ }
+ Abc_ObjForEachFanout( pObj, pNext, k )
+ {
+ if ( !Abc_ObjIsNode(pNext) )
+ continue;
+ if ( Abc_NodeIsTravIdCurrent( pNext ) )
+ continue;
+ Abc_NodeSetTravIdCurrent( pNext );
+ if ( Abc_ObjFanoutNum(pNext) > nFanMax )
+ continue;
+ Vec_PtrPush( vNext, pNext );
+ }
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects the circle of nodes removes from the given one.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkCollectNonOverlapCands( Abc_Obj_t * pLut, Vec_Ptr_t * vStart, Vec_Ptr_t * vNext, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars )
+{
+ Vec_Ptr_t * vTemp;
+ Abc_Obj_t * pObj;
+ int i, k;
+ Vec_PtrClear( vCands );
+ if ( pPars->nMaxSuppSize - Abc_ObjFaninNum(pLut) <= 1 )
+ return;
+
+ // collect nodes removed by this distance
+ assert( pPars->nMaxDistance > 0 );
+ Vec_PtrClear( vStart );
+ Vec_PtrPush( vStart, pLut );
+ Abc_NtkIncrementTravId( pLut->pNtk );
+ Abc_NodeSetTravIdCurrent( pLut );
+ for ( i = 1; i <= pPars->nMaxDistance; i++ )
+ {
+ Abc_NtkCollectCircle( vStart, vNext, pPars->nMaxFanout );
+ vTemp = vStart;
+ vStart = vNext;
+ vNext = vTemp;
+ // collect the nodes in vStart
+ Vec_PtrForEachEntry( vStart, pObj, k )
+ Vec_PtrPush( vCands, pObj );
+ }
+
+ // mark the TFI/TFO nodes
+ Abc_NtkIncrementTravId( pLut->pNtk );
+ if ( pPars->fUseTfiTfo )
+ Abc_NodeSetTravIdCurrent( pLut );
+ else
+ {
+ Abc_NodeSetTravIdPrevious( pLut );
+ Abc_NtkMarkFanins_rec( pLut, Abc_ObjLevel(pLut) - pPars->nMaxDistance );
+ Abc_NodeSetTravIdPrevious( pLut );
+ Abc_NtkMarkFanouts_rec( pLut, Abc_ObjLevel(pLut) + pPars->nMaxDistance, pPars->nMaxFanout );
+ }
+
+ // collect nodes satisfying the following conditions:
+ // - they are close enough in terms of distance
+ // - they are not in the TFI/TFO of the LUT
+ // - they have no more than the given number of fanins
+ // - they have no more than the given diff in delay
+ k = 0;
+ Vec_PtrForEachEntry( vCands, pObj, i )
+ {
+ if ( Abc_NodeIsTravIdCurrent(pObj) )
+ continue;
+ if ( Abc_ObjFaninNum(pLut) + Abc_ObjFaninNum(pObj) > pPars->nMaxSuppSize )
+ continue;
+ if ( Abc_ObjLevel(pLut) - Abc_ObjLevel(pObj) > pPars->nMaxLevelDiff ||
+ Abc_ObjLevel(pObj) - Abc_ObjLevel(pLut) > pPars->nMaxLevelDiff )
+ continue;
+ Vec_PtrWriteEntry( vCands, k++, pObj );
+ }
+ Vec_PtrShrink( vCands, k );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Count the total number of fanins.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkCountTotalFanins( Abc_Obj_t * pLut, Abc_Obj_t * pCand )
+{
+ Abc_Obj_t * pFanin;
+ int i, nCounter = Abc_ObjFaninNum(pLut);
+ Abc_ObjForEachFanin( pCand, pFanin, i )
+ nCounter += !pFanin->fMarkC;
+ return nCounter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collects overlapping candidates.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkCollectOverlapCands( Abc_Obj_t * pLut, Vec_Ptr_t * vCands, Nwk_LMPars_t * pPars )
+{
+ Abc_Obj_t * pFanin, * pObj;
+ int i, k;
+ // mark fanins of pLut
+ Abc_ObjForEachFanin( pLut, pFanin, i )
+ pFanin->fMarkC = 1;
+ // collect the matching fanouts of each fanin of the node
+ Vec_PtrClear( vCands );
+ Abc_NtkIncrementTravId( pLut->pNtk );
+ Abc_NodeSetTravIdCurrent( pLut );
+ Abc_ObjForEachFanin( pLut, pFanin, i )
+ {
+ if ( !Abc_ObjIsNode(pFanin) )
+ continue;
+ if ( Abc_ObjFanoutNum(pFanin) > pPars->nMaxFanout )
+ continue;
+ Abc_ObjForEachFanout( pFanin, pObj, k )
+ {
+ if ( !Abc_ObjIsNode(pObj) )
+ continue;
+ if ( Abc_NodeIsTravIdCurrent( pObj ) )
+ continue;
+ Abc_NodeSetTravIdCurrent( pObj );
+ // check the difference in delay
+ if ( Abc_ObjLevel(pLut) - Abc_ObjLevel(pObj) > pPars->nMaxLevelDiff ||
+ Abc_ObjLevel(pObj) - Abc_ObjLevel(pLut) > pPars->nMaxLevelDiff )
+ continue;
+ // check the total number of fanins of the node
+ if ( Abc_NtkCountTotalFanins(pLut, pObj) > pPars->nMaxSuppSize )
+ continue;
+ Vec_PtrPush( vCands, pObj );
+ }
+ }
+ // unmark fanins of pLut
+ Abc_ObjForEachFanin( pLut, pFanin, i )
+ pFanin->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs LUT merging with parameters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkLutMerge( Abc_Ntk_t * pNtk, Nwk_LMPars_t * pPars )
+{
+ Nwk_Grf_t * p;
+ Vec_Int_t * vResult;
+ Vec_Ptr_t * vStart, * vNext, * vCands1, * vCands2;
+ Abc_Obj_t * pLut, * pCand;
+ int i, k, nVertsMax, nCands, clk = clock();
+ // count the number of vertices
+ nVertsMax = 0;
+ Abc_NtkForEachNode( pNtk, pLut, i )
+ nVertsMax += (int)(Abc_ObjFaninNum(pLut) <= pPars->nMaxLutSize);
+ p = Nwk_ManGraphAlloc( nVertsMax );
+ // create graph
+ vStart = Vec_PtrAlloc( 1000 );
+ vNext = Vec_PtrAlloc( 1000 );
+ vCands1 = Vec_PtrAlloc( 1000 );
+ vCands2 = Vec_PtrAlloc( 1000 );
+ nCands = 0;
+ Abc_NtkForEachNode( pNtk, pLut, i )
+ {
+ if ( Abc_ObjFaninNum(pLut) > pPars->nMaxLutSize )
+ continue;
+ Abc_NtkCollectOverlapCands( pLut, vCands1, pPars );
+ if ( pPars->fUseDiffSupp )
+ Abc_NtkCollectNonOverlapCands( pLut, vStart, vNext, vCands2, pPars );
+ if ( Vec_PtrSize(vCands1) == 0 && Vec_PtrSize(vCands2) == 0 )
+ continue;
+ nCands += Vec_PtrSize(vCands1) + Vec_PtrSize(vCands2);
+ // save candidates
+ Vec_PtrForEachEntry( vCands1, pCand, k )
+ Nwk_ManGraphHashEdge( p, Abc_ObjId(pLut), Abc_ObjId(pCand) );
+ Vec_PtrForEachEntry( vCands2, pCand, k )
+ Nwk_ManGraphHashEdge( p, Abc_ObjId(pLut), Abc_ObjId(pCand) );
+ // print statistics about this node
+ if ( pPars->fVeryVerbose )
+ printf( "Node %6d : Fanins = %d. Fanouts = %3d. Cand1 = %3d. Cand2 = %3d.\n",
+ Abc_ObjId(pLut), Abc_ObjFaninNum(pLut), Abc_ObjFaninNum(pLut),
+ Vec_PtrSize(vCands1), Vec_PtrSize(vCands2) );
+ }
+ Vec_PtrFree( vStart );
+ Vec_PtrFree( vNext );
+ Vec_PtrFree( vCands1 );
+ Vec_PtrFree( vCands2 );
+ if ( pPars->fVerbose )
+ {
+ printf( "Mergable LUTs = %6d. Total cands = %6d. ", p->nVertsMax, nCands );
+ PRT( "Deriving graph", clock() - clk );
+ }
+ // solve the graph problem
+ clk = clock();
+ Nwk_ManGraphSolve( p );
+ if ( pPars->fVerbose )
+ {
+ printf( "GRAPH: Nodes = %6d. Edges = %6d. Pairs = %6d. ",
+ p->nVerts, p->nEdges, Vec_IntSize(p->vPairs)/2 );
+ PRT( "Solving", clock() - clk );
+ Nwk_ManGraphReportMemoryUsage( p );
+ }
+ vResult = p->vPairs; p->vPairs = NULL;
+/*
+ for ( i = 0; i < vResult->nSize; i += 2 )
+ printf( "(%d,%d) ", vResult->pArray[i], vResult->pArray[i+1] );
+ printf( "\n" );
+*/
+ Nwk_ManGraphFree( p );
+ return vResult;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 23a44eb3..0b1d8fc1 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -22,7 +22,7 @@
#include "dec.h"
#include "main.h"
#include "mio.h"
-//#include "seq.h"
+#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -102,6 +102,49 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
/**Function*************************************************************
+ Synopsis [Marks nodes for power-optimization.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk )
+{
+ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+ extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
+ Vec_Int_t * vSwitching;
+ float * pSwitching;
+ Abc_Ntk_t * pNtkStr;
+ Aig_Man_t * pAig;
+ Aig_Obj_t * pObjAig;
+ Abc_Obj_t * pObjAbc, * pObjAbc2;
+ float Result = (float)0;
+ int i;
+ // strash the network
+ pNtkStr = Abc_NtkStrash( pNtk, 0, 1, 0 );
+ Abc_NtkForEachObj( pNtk, pObjAbc, i )
+ if ( Abc_ObjRegular(pObjAbc->pTemp)->Type == ABC_FUNC_NONE )
+ pObjAbc->pTemp = NULL;
+ // map network into an AIG
+ pAig = Abc_NtkToDar( pNtkStr, 0, (int)(Abc_NtkLatchNum(pNtk) > 0) );
+ vSwitching = Saig_ManComputeSwitchProbs( pAig, 48, 16, 0 );
+ pSwitching = (float *)vSwitching->pArray;
+ Abc_NtkForEachObj( pNtk, pObjAbc, i )
+ {
+ if ( (pObjAbc2 = Abc_ObjRegular(pObjAbc->pTemp)) && (pObjAig = pObjAbc2->pTemp) )
+ Result += Abc_ObjFanoutNum(pObjAbc) * pSwitching[pObjAig->Id];
+ }
+ Vec_IntFree( vSwitching );
+ Aig_ManStop( pAig );
+ Abc_NtkDelete( pNtkStr );
+ return Result;
+}
+
+/**Function*************************************************************
+
Synopsis [Print the vital stats of the network.]
Description []
@@ -111,7 +154,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes )
+void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower )
{
int Num;
if ( fSaveBest )
@@ -192,6 +235,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
fprintf( pFile, " lev = %3d", Abc_NtkLevel(pNtk) );
if ( fUseLutLib && Abc_FrameReadLibLut() )
fprintf( pFile, " delay = %5.2f", Abc_NtkDelayTraceLut(pNtk, 1) );
+ if ( fPower )
+ fprintf( pFile, " power = %7.2f", Abc_NtkMfsTotalSwitching(pNtk) );
fprintf( pFile, "\n" );
// Abc_NtkCrossCut( pNtk );
@@ -898,32 +943,39 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
if ( fUseLibrary && Abc_NtkHasMapping(pNtk) )
{
- stmm_table * tTable;
- stmm_generator * gen;
- char * pName;
- int * pCounter, Counter;
+ Mio_Gate_t ** ppGates;
double Area, AreaTotal;
+ int Counter, nGates, i;
+
+ // clean value of all gates
+ nGates = Mio_LibraryReadGateNum( pNtk->pManFunc );
+ ppGates = Mio_LibraryReadGatesByName( pNtk->pManFunc );
+ for ( i = 0; i < nGates; i++ )
+ Mio_GateSetValue( ppGates[i], 0 );
// count the gates by name
CounterTotal = 0;
- tTable = stmm_init_table(strcmp, stmm_strhash);
Abc_NtkForEachNode( pNtk, pObj, i )
{
if ( i == 0 ) continue;
- if ( !stmm_find_or_add( tTable, Mio_GateReadName(pObj->pData), (char ***)&pCounter ) )
- *pCounter = 0;
- (*pCounter)++;
+ Mio_GateSetValue( pObj->pData, 1 + Mio_GateReadValue(pObj->pData) );
CounterTotal++;
}
// print the gates
AreaTotal = Abc_NtkGetMappedArea(pNtk);
- stmm_foreach_item( tTable, gen, (char **)&pName, (char **)&Counter )
+ for ( i = 0; i < nGates; i++ )
{
- Area = Counter * Mio_GateReadArea(Mio_LibraryReadGateByName(pNtk->pManFunc,pName));
- printf( "%-12s = %8d %10.2f %6.2f %%\n", pName, Counter, Area, 100.0 * Area / AreaTotal );
+ Counter = Mio_GateReadValue( ppGates[i] );
+ if ( Counter == 0 )
+ continue;
+ Area = Counter * Mio_GateReadArea( ppGates[i] );
+ printf( "%-12s Fanin = %2d Instance = %8d Area = %10.2f %6.2f %%\n",
+ Mio_GateReadName( ppGates[i] ),
+ Mio_GateReadInputs( ppGates[i] ),
+ Counter, Area, 100.0 * Area / AreaTotal );
}
- printf( "%-12s = %8d %10.2f %6.2f %%\n", "TOTAL", CounterTotal, AreaTotal, 100.0 );
- stmm_free_table( tTable );
+ printf( "%-12s Instance = %8d Area = %10.2f %6.2f %%\n", "TOTAL",
+ CounterTotal, AreaTotal, 100.0 );
return;
}
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 463846b9..a7c9f609 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -316,7 +316,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
***********************************************************************/
void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, int fAllNodes, int fRecord )
{
- ProgressBar * pProgress;
+// ProgressBar * pProgress;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNodeOld;
int i; //, clk = clock();
@@ -326,13 +326,13 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew, int fAllNod
vNodes = Abc_NtkDfsIter( pNtkOld, fAllNodes );
//printf( "Nodes = %d. ", Vec_PtrSize(vNodes) );
//PRT( "Time", clock() - clk );
- pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
+// pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
Vec_PtrForEachEntry( vNodes, pNodeOld, i )
{
- Extra_ProgressBarUpdate( pProgress, i, NULL );
+// Extra_ProgressBarUpdate( pProgress, i, NULL );
pNodeOld->pCopy = Abc_NodeStrash( pNtkNew, pNodeOld, fRecord );
}
- Extra_ProgressBarStop( pProgress );
+// Extra_ProgressBarStop( pProgress );
Vec_PtrFree( vNodes );
}
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index e83785fe..c872d62e 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -25,6 +25,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcIvy.c \
src/base/abci/abcLut.c \
src/base/abci/abcMap.c \
+ src/base/abci/abcMerge.c \
src/base/abci/abcMini.c \
src/base/abci/abcMiter.c \
src/base/abci/abcMulti.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 00:55:35 +0000