From f936cc0680c98ffe51b3a1716c996072d5dbf76c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 18 Jan 2009 08:01:00 -0800 Subject: Version abc90118 --- src/base/abc/abc.h | 18 +- src/base/abc/abcHie.c | 3 - src/base/abci/abc.c | 1984 ++++++++++++++++++++++++++++++++++++-------- src/base/abci/abc.zip | Bin 62408 -> 0 bytes src/base/abci/abcBidec.c | 33 +- src/base/abci/abcCut.c | 75 +- src/base/abci/abcDar.c | 726 +++++++++++++++- src/base/abci/abcDelay.c | 297 +++++++ src/base/abci/abcIf.c | 58 +- src/base/abci/abcMap.c | 6 +- src/base/abci/abcMerge.c | 352 ++++++++ src/base/abci/abcPrint.c | 82 +- src/base/abci/abcStrash.c | 8 +- src/base/abci/module.make | 1 + src/base/cmd/cmd.c | 1 + src/base/cmd/cmd.h | 8 +- src/base/io/io.c | 45 + src/base/io/ioAbc.h | 3 + src/base/io/ioReadAiger.c | 2 +- src/base/io/ioReadBlifMv.c | 3 +- src/base/io/ioUtil.c | 2 + src/base/io/ioWriteBook.c | 985 ++++++++++++++++++++++ src/base/io/io_.c | 48 -- src/base/io/module.make | 1 + src/base/main/main.c | 6 +- src/base/main/main.h | 11 +- src/base/main/mainFrame.c | 2 + src/base/main/mainInt.h | 10 +- 28 files changed, 4280 insertions(+), 490 deletions(-) delete mode 100644 src/base/abci/abc.zip create mode 100644 src/base/abci/abcMerge.c create mode 100644 src/base/io/ioWriteBook.c delete mode 100644 src/base/io/io_.c (limited to 'src/base') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index e4b0ad69..987adaad 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -154,7 +154,12 @@ struct Abc_Obj_t_ // 12 words // miscellaneous void * pData; // the network specific data (SOP, BDD, gate, equiv class, etc) Abc_Obj_t * pNext; // the next pointer in the hash table - Abc_Obj_t * pCopy; // the copy of this object + union { // temporary store for user's data + Abc_Obj_t * pCopy; // the copy of this object + void * pTemp; + int iTemp; + float dTemp; + }; Hop_Obj_t * pEquiv; // pointer to the HAIG node }; @@ -227,14 +232,14 @@ struct Abc_Lib_t_ //#pragma warning( disable : 4273 ) #ifdef WIN32 -#define DLLEXPORT __declspec(dllexport) -#define DLLIMPORT __declspec(dllimport) +#define ABC_DLLEXPORT __declspec(dllexport) +#define ABC_DLLIMPORT __declspec(dllimport) #else /* defined(WIN32) */ -#define DLLIMPORT +#define ABC_DLLIMPORT #endif /* defined(WIN32) */ #ifndef ABC_DLL -#define ABC_DLL DLLIMPORT +#define ABC_DLL ABC_DLLIMPORT #endif // maximum/minimum operators @@ -748,7 +753,8 @@ extern ABC_DLL bool Abc_NodeIsBuf( Abc_Obj_t * pNode ); extern ABC_DLL bool Abc_NodeIsInv( Abc_Obj_t * pNode ); extern ABC_DLL void Abc_NodeComplement( Abc_Obj_t * pNode ); /*=== abcPrint.c ==========================================================*/ -extern ABC_DLL void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes ); +extern ABC_DLL float Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk ); +extern ABC_DLL void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower ); extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcHie.c b/src/base/abc/abcHie.c index 56333a36..19bdc47e 100644 --- a/src/base/abc/abcHie.c +++ b/src/base/abc/abcHie.c @@ -472,9 +472,6 @@ Abc_Ntk_t * Abc_NtkInsertNewLogic( Abc_Ntk_t * pNtkH, Abc_Ntk_t * pNtkL ) Vec_PtrWriteEntry( pDesign->vModules, 0, pNtkNew ); pNtkNew->pDesign = pDesign; -//Abc_NtkPrintStats( stdout, pNtkH, 0 ); -//Abc_NtkPrintStats( stdout, pNtkNew, 0 ); - // check integrity if ( !Abc_NtkCheck( pNtkNew ) ) { 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 ] [-raestvh]\n" ); + fprintf( pErr, "usage: mfs [-WFDMLC ] [-raestpvh]\n" ); fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" ); fprintf( pErr, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs ); fprintf( pErr, "\t-F : 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 : 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 : 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 : the max LUT size for merging (1 < num) [default = %d]\n", pPars->nMaxLutSize ); + fprintf( stdout, "\t-S : the max total support size after merging (1 < num) [default = %d]\n", pPars->nMaxSuppSize ); + fprintf( stdout, "\t-D : the max distance in terms of LUTs (0 < num) [default = %d]\n", pPars->nMaxDistance ); + fprintf( stdout, "\t-L : the max difference in levels (0 <= num) [default = %d]\n", pPars->nMaxLevelDiff ); + fprintf( stdout, "\t-F : 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,7 +11595,6 @@ usage: return 1; } - /**Function************************************************************* Synopsis [] @@ -11297,10 +11606,164 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAmap( Abc_Frame_t * pAbc, int argc, char ** argv ) { + Amap_Par_t Pars, * pPars = &Pars; FILE * pOut, * pErr; - Abc_Ntk_t * pNtk; + 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 ] [-E ] [-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************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; int c; pNtk = Abc_FrameReadNtk(pAbc); @@ -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 ] [-pludvwh]\n" ); + fprintf( pErr, "usage: scorr [-PQFCLNSIVM ] [-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 ] [-vh] \n" ); + fprintf( pErr, "usage: clockgate [-LNDCVK ] [-avwh] \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,115 +15312,335 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandExtWin( Abc_Frame_t * pAbc, int argc, char ** argv ) { - char Buffer[16]; FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtk1, * pNtk2; - int fDelete1, fDelete2; - char ** pArgvNew; - int nArgcNew; + Abc_Ntk_t * pNtkRes, * pNtk; int c; - int fSat; + int nObjId; + int nDist; int fVerbose; - int nSeconds; - int nPartSize; - int nConfLimit; - int nInsLimit; - int fPartition; - extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit ); - extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ); - extern void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose ); - extern void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, 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 - fSat = 0; + nObjId = -1; + nDist = 5; fVerbose = 0; - nSeconds = 20; - nPartSize = 0; - nConfLimit = 10000; - nInsLimit = 0; - fPartition = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPpsvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NDvh" ) ) != EOF ) { switch ( c ) { - case 'T': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); - goto usage; - } - nSeconds = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nSeconds < 0 ) - goto usage; - break; - case 'C': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); - goto usage; - } - nConfLimit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nConfLimit < 0 ) - goto usage; - break; - case 'I': + case 'N': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } - nInsLimit = atoi(argv[globalUtilOptind]); + nObjId = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nInsLimit < 0 ) + if ( nObjId <= 0 ) goto usage; break; - case 'P': + case 'D': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" ); goto usage; } - nPartSize = atoi(argv[globalUtilOptind]); + nDist = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nPartSize < 0 ) + if ( nDist <= 0 ) goto usage; break; - case 'p': - fPartition ^= 1; - break; - case 's': - fSat ^= 1; - break; case 'v': fVerbose ^= 1; break; + case 'h': + goto usage; default: goto usage; } } - - pArgvNew = argv + globalUtilOptind; - nArgcNew = argc - globalUtilOptind; - if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) + 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; + } - // perform equivalence checking - if ( fPartition ) - Abc_NtkCecFraigPartAuto( pNtk1, pNtk2, nSeconds, fVerbose ); - else if ( nPartSize ) - Abc_NtkCecFraigPart( pNtk1, pNtk2, nSeconds, nPartSize, fVerbose ); - else if ( fSat ) - Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nInsLimit ); + 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 ] [-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 ] [-vh] \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]; + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtk1, * pNtk2; + int fDelete1, fDelete2; + char ** pArgvNew; + int nArgcNew; + int c; + int fSat; + int fVerbose; + int nSeconds; + int nPartSize; + int nConfLimit; + int nInsLimit; + int fPartition; + + extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit ); + extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ); + extern void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose ); + extern void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fSat = 0; + fVerbose = 0; + nSeconds = 20; + nPartSize = 0; + nConfLimit = 10000; + nInsLimit = 0; + fPartition = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "TCIPpsvh" ) ) != EOF ) + { + switch ( c ) + { + case 'T': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + nSeconds = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSeconds < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nInsLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nInsLimit < 0 ) + goto usage; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nPartSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nPartSize < 0 ) + goto usage; + break; + case 'p': + fPartition ^= 1; + break; + case 's': + fSat ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + default: + goto usage; + } + } + + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) + return 1; + + // perform equivalence checking + if ( fPartition ) + Abc_NtkCecFraigPartAuto( pNtk1, pNtk2, nSeconds, fVerbose ); + else if ( nPartSize ) + Abc_NtkCecFraigPart( pNtk1, pNtk2, nSeconds, nPartSize, fVerbose ); + else if ( fSat ) + Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nInsLimit ); else Abc_NtkCecFraig( pNtk1, pNtk2, nSeconds, fVerbose ); @@ -15108,47 +15835,190 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) +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; - int fRetime; - int fSat; - int fVerbose; - int nFrames; - int nSeconds; - int nConfLimit; - int nInsLimit; - - extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames ); - extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); - + + 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 - fRetime = 0; // verification after retiming - fSat = 0; - fVerbose = 0; - nFrames = 5; - nSeconds = 20; - nConfLimit = 10000; - nInsLimit = 0; + fMiter = 0; + Cec_ManCecSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsrvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "BMImfrsvh" ) ) != EOF ) { switch ( c ) { - case 'F': + case 'B': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + 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] \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; + Abc_Ntk_t * pNtk, * pNtk1, * pNtk2; + int fDelete1, fDelete2; + char ** pArgvNew; + int nArgcNew; + int c; + int fRetime; + int fSat; + int fVerbose; + int nFrames; + int nSeconds; + int nConfLimit; + int nInsLimit; + + extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames ); + extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); + + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fRetime = 0; // verification after retiming + fSat = 0; + fVerbose = 0; + nFrames = 5; + nSeconds = 20; + nConfLimit = 10000; + nInsLimit = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsrvh" ) ) != 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]); @@ -15325,38 +16195,449 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - - 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 ) + + 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_NtkDarSec( pNtk1, pNtk2, pSecPar ); + + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + return 0; + +usage: + fprintf( pErr, "usage: dsec [-F num] [-T num] [-armfwvh] \n" ); + fprintf( pErr, "\t performs inductive sequential equivalence checking\n" ); + fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax ); + fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit ); + fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" ); + fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" ); + fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" ); + fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" ); + fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" ); + fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "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_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Fra_Sec_t SecPar, * pSecPar = &SecPar; + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + + extern void Fra_SecSetDefaultParams( Fra_Sec_t * p ); + extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Fra_SecSetDefaultParams( pSecPar ); +// pSecPar->TimeLimit = 300; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijwvh" ) ) != EOF ) + { + switch ( c ) + { + case 'c': + pSecPar->fTryComb ^= 1; + break; + case 'b': + pSecPar->fTryBmc ^= 1; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nFramesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nFramesMax < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nBTLimit < 0 ) + goto usage; + break; + case 'G': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nBTLimitGlobal = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nBTLimitGlobal < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nBTLimitInter = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nBTLimitInter < 0 ) + goto usage; + break; + case 'V': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-V\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nBddVarsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nBddVarsMax < 0 ) + goto usage; + break; + case 'B': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nBddMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nBddMax < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + pSecPar->nBddIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pSecPar->nBddIterMax < 0 ) + goto usage; + break; + case 'a': + pSecPar->fPhaseAbstract ^= 1; + break; + case 'r': + pSecPar->fRetimeFirst ^= 1; + break; + case 'm': + pSecPar->fRetimeRegs ^= 1; + break; + case 'f': + pSecPar->fFraiging ^= 1; + break; + case 'i': + pSecPar->fInduction ^= 1; + break; + case 'j': + pSecPar->fInterpolation ^= 1; + break; + case 'w': + pSecPar->fVeryVerbose ^= 1; + break; + case 'v': + pSecPar->fVerbose ^= 1; + break; + default: + goto usage; + } + } + + if ( !Abc_NtkIsStrash(pNtk) ) + { + printf( "This command works only for structrally hashed networks. Run \"st\".\n" ); + return 0; + } + + // perform verification + Abc_NtkDarProve( pNtk, pSecPar ); + + // Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p ) + + return 0; + +usage: + fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijwvh]\n" ); + fprintf( pErr, "\t performs SEC on the sequential miter\n" ); + fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax ); + fprintf( pErr, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit ); + fprintf( pErr, "\t-G num : the global conflict limit during induction [default = %d]\n", pSecPar->nBTLimitGlobal ); + fprintf( pErr, "\t-D num : the conflict limit during interpolation [default = %d]\n", pSecPar->nBTLimitInter ); + fprintf( pErr, "\t-V num : the flop count limit for BDD-based reachablity [default = %d]\n", pSecPar->nBddVarsMax ); + fprintf( pErr, "\t-B num : the BDD size limit in BDD-based reachablity [default = %d]\n", pSecPar->nBddMax ); + fprintf( pErr, "\t-R num : the max number of reachability iterations [default = %d]\n", pSecPar->nBddIterMax ); + fprintf( pErr, "\t-c : toggles using CEC before attempting SEC [default = %s]\n", pSecPar->fTryComb? "yes": "no" ); + fprintf( pErr, "\t-b : toggles using BMC before attempting SEC [default = %s]\n", pSecPar->fTryBmc? "yes": "no" ); + fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" ); + fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" ); + fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" ); + fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" ); + fprintf( pErr, "\t-i : toggles the use of induction [default = %s]\n", pSecPar->fInduction? "yes": "no" ); + fprintf( pErr, "\t-j : toggles the use of interpolation [default = %s]\n", pSecPar->fInterpolation? "yes": "no" ); +// fprintf( pErr, "\t-n : toggles the use of different induction prover [default = %s]\n", pSecPar->fUseNewProver? "yes": "no" ); + fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" ); + fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + 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] \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 ); - printf( "The network has no latches. Used combinational command \"cec\".\n" ); - return 0; } - - // perform verification - Abc_NtkDarSec( pNtk1, pNtk2, pSecPar ); - - if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); - if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); return 0; usage: - fprintf( pErr, "usage: dsec [-F num] [-T num] [-armfwvh] \n" ); - fprintf( pErr, "\t performs inductive sequential equivalence checking\n" ); - fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax ); - fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit ); - fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" ); - fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" ); - fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" ); - fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" ); - fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" ); - fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" ); - fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "usage: simsec [-FD num] [-mcyv] \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"); @@ -15375,175 +16656,109 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandMatch( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Fra_Sec_t SecPar, * pSecPar = &SecPar; FILE * pOut, * pErr; - Abc_Ntk_t * pNtk; - int c; + Abc_Ntk_t * pNtk, * pNtk1, * pNtk2, * pNtkRes; + int fDelete1, fDelete2; + char ** pArgvNew; + int nArgcNew, c; + int fMiter; + int nDist; + int fVerbose; - extern void Fra_SecSetDefaultParams( Fra_Sec_t * p ); - extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ); + 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 - Fra_SecSetDefaultParams( pSecPar ); -// pSecPar->TimeLimit = 300; + fMiter = 0; + nDist = 0; + fVerbose = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Dmvh" ) ) != EOF ) { switch ( c ) { - case 'c': - pSecPar->fTryComb ^= 1; - break; - case 'b': - pSecPar->fTryBmc ^= 1; - break; - case 'F': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); - goto usage; - } - pSecPar->nFramesMax = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pSecPar->nFramesMax < 0 ) - goto usage; - break; - case 'C': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); - goto usage; - } - pSecPar->nBTLimit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pSecPar->nBTLimit < 0 ) - goto usage; - break; - case 'G': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" ); - goto usage; - } - pSecPar->nBTLimitGlobal = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pSecPar->nBTLimitGlobal < 0 ) - goto usage; - break; case 'D': if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" ); goto usage; } - pSecPar->nBTLimitInter = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pSecPar->nBTLimitInter < 0 ) - goto usage; - break; - case 'V': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-V\" should be followed by an integer.\n" ); - goto usage; - } - pSecPar->nBddVarsMax = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pSecPar->nBddVarsMax < 0 ) - goto usage; - break; - case 'B': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" ); - goto usage; - } - pSecPar->nBddMax = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pSecPar->nBddMax < 0 ) - goto usage; - break; - case 'R': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" ); - goto usage; - } - pSecPar->nBddIterMax = atoi(argv[globalUtilOptind]); + nDist = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pSecPar->nBddIterMax < 0 ) + if ( nDist < 0 ) goto usage; break; - case 'a': - pSecPar->fPhaseAbstract ^= 1; - break; - case 'r': - pSecPar->fRetimeFirst ^= 1; - break; case 'm': - pSecPar->fRetimeRegs ^= 1; - break; - case 'f': - pSecPar->fFraiging ^= 1; - break; - case 'i': - pSecPar->fInduction ^= 1; - break; - case 'j': - pSecPar->fInterpolation ^= 1; - break; - case 'w': - pSecPar->fVeryVerbose ^= 1; + fMiter ^= 1; break; case 'v': - pSecPar->fVerbose ^= 1; + fVerbose ^= 1; break; default: goto usage; } } - if ( !Abc_NtkIsStrash(pNtk) ) + if ( fMiter ) { - printf( "This command works only for structrally hashed networks. Run \"st\".\n" ); - return 0; +// 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 ); +*/ } - - // perform verification - Abc_NtkDarProve( pNtk, pSecPar ); - - // Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p ) - + 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: dprove [-FCGDVBR num] [-cbarmfijwvh]\n" ); - fprintf( pErr, "\t performs SEC on the sequential miter\n" ); - fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax ); - fprintf( pErr, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit ); - fprintf( pErr, "\t-G num : the global conflict limit during induction [default = %d]\n", pSecPar->nBTLimitGlobal ); - fprintf( pErr, "\t-D num : the conflict limit during interpolation [default = %d]\n", pSecPar->nBTLimitInter ); - fprintf( pErr, "\t-V num : the flop count limit for BDD-based reachablity [default = %d]\n", pSecPar->nBddVarsMax ); - fprintf( pErr, "\t-B num : the BDD size limit in BDD-based reachablity [default = %d]\n", pSecPar->nBddMax ); - fprintf( pErr, "\t-R num : the max number of reachability iterations [default = %d]\n", pSecPar->nBddIterMax ); - fprintf( pErr, "\t-c : toggles using CEC before attempting SEC [default = %s]\n", pSecPar->fTryComb? "yes": "no" ); - fprintf( pErr, "\t-b : toggles using BMC before attempting SEC [default = %s]\n", pSecPar->fTryBmc? "yes": "no" ); - fprintf( pErr, "\t-a : toggles the use of phase abstraction [default = %s]\n", pSecPar->fPhaseAbstract? "yes": "no" ); - fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" ); - fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" ); - fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" ); - fprintf( pErr, "\t-i : toggles the use of induction [default = %s]\n", pSecPar->fInduction? "yes": "no" ); - fprintf( pErr, "\t-j : toggles the use of interpolation [default = %s]\n", pSecPar->fInterpolation? "yes": "no" ); -// fprintf( pErr, "\t-n : toggles the use of different induction prover [default = %s]\n", pSecPar->fUseNewProver? "yes": "no" ); - fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" ); - fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" ); - fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "usage: match [-D num] [-mv] \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; } @@ -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 \"_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 ] [-raesvh]\n" ); + fprintf( stdout, "usage: *mfs [-WFDMLC ] [-raespvh]\n" ); fprintf( stdout, "\t performs don't-care-based optimization of logic networks\n" ); fprintf( stdout, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs ); fprintf( stdout, "\t-F : 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 ] [-pldvh]\n" ); + fprintf( stdout, "usage: *scorr [-PQFCLNSDVM ] [-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 Binary files a/src/base/abci/abc.zip and /dev/null 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 @@ -37,6 +37,74 @@ static int Abc_NtkComputeArea( Abc_Ntk_t * pNtk, Cut_Man_t * p ); /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**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.] @@ -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" ); @@ -149,6 +151,63 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ) return pMan; } +/**Function************************************************************* + + 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.] @@ -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 @@ -1180,6 +1242,81 @@ PRT( "Time", clock() - clkTotal ); return RetValue; } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + 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.] @@ -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; } @@ -2589,6 +2980,129 @@ Abc_Ntk_t * Abc_NtkDarClockGate( Abc_Ntk_t * pNtk, Abc_Ntk_t * pCare, Cgt_Par_t return pNtkAig; } +/**Function************************************************************* + + Synopsis [Performs phase abstraction.] + + Description [] + + SideEffects [] + + 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.] @@ -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<Id] & (1<Id] & (1< 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< 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 @@ -40,6 +40,59 @@ extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose ); /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Interface with the FPGA mapping package.] + + Description [] + + SideEffects [] + + 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.] @@ -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 /// @@ -100,6 +100,49 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk ) return 0; } +/**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.] @@ -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 \ diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index 4e0a4c95..459d82c9 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -662,6 +662,7 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv ) } } + fflush( pAbc->Out ); status = Cmd_CommandExecute( pAbc, line ); } while ( status == 0 ); diff --git a/src/base/cmd/cmd.h b/src/base/cmd/cmd.h index 9d0b8703..143f57cd 100644 --- a/src/base/cmd/cmd.h +++ b/src/base/cmd/cmd.h @@ -41,14 +41,14 @@ typedef struct MvCommand Abc_Command; // one command typedef struct MvAlias Abc_Alias; // one alias #ifdef WIN32 -#define DLLEXPORT __declspec(dllexport) -#define DLLIMPORT __declspec(dllimport) +#define ABC_DLLEXPORT __declspec(dllexport) +#define ABC_DLLIMPORT __declspec(dllimport) #else /* defined(WIN32) */ -#define DLLIMPORT +#define ABC_DLLIMPORT #endif /* defined(WIN32) */ #ifndef ABC_DLL -#define ABC_DLL DLLIMPORT +#define ABC_DLL ABC_DLLIMPORT #endif //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/io.c b/src/base/io/io.c index 6f326a27..a8941868 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -48,6 +48,7 @@ static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteBook ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -102,6 +103,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_blif_mv", IoCommandWriteBlifMv, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_book", IoCommandWriteBook, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 ); @@ -1477,6 +1479,49 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int IoCommandWriteBook( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + char * pFileName; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + // get the output file name + pFileName = argv[globalUtilOptind]; + // call the corresponding file writer + Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BOOK ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: write_book [-h] [-options]\n" ); + fprintf( pAbc->Err, "\t-h : print the help massage\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aux, .nodes, .nets)\n" ); + fprintf( pAbc->Err, "\t\n" ); + fprintf( pAbc->Err, "\tThis command is developed by Myungchul Kim (University of Michigan).\n" ); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h index e62cc168..842d8995 100644 --- a/src/base/io/ioAbc.h +++ b/src/base/io/ioAbc.h @@ -47,6 +47,7 @@ typedef enum { IO_FILE_BLIF, IO_FILE_BLIFMV, IO_FILE_BENCH, + IO_FILE_BOOK, IO_FILE_CNF, IO_FILE_DOT, IO_FILE_EDIF, @@ -99,6 +100,8 @@ extern void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteBench.c =========================================================*/ extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); extern int Io_WriteBenchLut( Abc_Ntk_t * pNtk, char * FileName ); +/*=== abcWriteBook.c =========================================================*/ +extern void Io_WriteBook( Abc_Ntk_t * pNtk, char * FileName ); /*=== abcWriteCnf.c ===========================================================*/ extern int Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName, int fAllPrimes ); /*=== abcWriteDot.c ===========================================================*/ diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index b8555561..3a6ecd19 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -45,7 +45,7 @@ SeeAlso [] ***********************************************************************/ -unsigned Io_ReadAigerDecode( char ** ppPos ) +static inline unsigned Io_ReadAigerDecode( char ** ppPos ) { unsigned x = 0, i = 0; unsigned char ch; diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c index 880c2b5f..87358ed2 100644 --- a/src/base/io/ioReadBlifMv.c +++ b/src/base/io/ioReadBlifMv.c @@ -130,7 +130,7 @@ Abc_Ntk_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck ) FILE * pFile; Io_MvMan_t * p; Abc_Ntk_t * pNtk; - Abc_Lib_t * pDesign = NULL; + Abc_Lib_t * pDesign = NULL; char * pDesignName; int RetValue, i; @@ -951,6 +951,7 @@ static int Io_MvParseLineLatch( Io_MvMod_t * p, char * pLine ) pNet = Abc_NtkFindOrCreateNet( p->pNtk, Abc_ObjNameSuffix(pNet, "_out") ); // create latch pObj = Io_ReadCreateLatch( p->pNtk, Vec_PtrEntry(vTokens,1), Abc_ObjName(pNet) ); +// Abc_LatchSetInit0( pObj ); Abc_LatchSetInit0( pObj ); } return 1; diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index 119b4d75..60e6adc8 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -338,6 +338,8 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType ) } else if ( FileType == IO_FILE_BENCH ) Io_WriteBench( pNtkTemp, pFileName ); + else if ( FileType == IO_FILE_BOOK ) + Io_WriteBook( pNtkTemp, pFileName ); else if ( FileType == IO_FILE_PLA ) Io_WritePla( pNtkTemp, pFileName ); else if ( FileType == IO_FILE_EQN ) diff --git a/src/base/io/ioWriteBook.c b/src/base/io/ioWriteBook.c new file mode 100644 index 00000000..95405438 --- /dev/null +++ b/src/base/io/ioWriteBook.c @@ -0,0 +1,985 @@ +/**CFile**************************************************************** + + FileName [ioWriteBook.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to write Bookshelf files.] + + Author [Myungchul Kim] + + Affiliation [U of Michigan] + + Date [Ver. 1.0. Started - October 25, 2008.] + + Revision [$Id: ioWriteBook.c,v 1.00 2005/11/10 00:00:00 mckima Exp $] + +***********************************************************************/ + +#include "ioAbc.h" +#include "main.h" +#include "mio.h" +#define NODES 0 +#define PL 1 +#define coreHeight 1 +#define termWidth 1 +#define termHeight 1 + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static unsigned Io_NtkWriteNodes( FILE * pFile, Abc_Ntk_t * pNtk ); +static void Io_NtkWritePiPoNodes( FILE * pFile, Abc_Ntk_t * pNtk ); +static void Io_NtkWriteLatchNode( FILE * pFile, Abc_Obj_t * pLatch, bool NodesOrPl ); +static unsigned Io_NtkWriteIntNode( FILE * pFile, Abc_Obj_t * pNode, bool NodesOrPl ); +static unsigned Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode ); +static void Io_NtkWriteNets( FILE * pFile, Abc_Ntk_t * pNtk ); +static void Io_NtkWriteIntNet( FILE * pFile, Abc_Obj_t * pNode ); +static void Io_NtkBuildLayout( FILE * pFile1, FILE *pFile2, Abc_Ntk_t * pNtk, double aspectRatio, double whiteSpace, unsigned coreCellArea ); +static void Io_NtkWriteScl( FILE * pFile, unsigned numCoreRows, double layoutWidth ); +static void Io_NtkWritePl( FILE * pFile, Abc_Ntk_t * pNtk, unsigned numTerms, double layoutHeight, double layoutWidth ); +static Vec_Ptr_t * Io_NtkOrderingPads( Abc_Ntk_t * pNtk, Vec_Ptr_t * vTerms ); +static Abc_Obj_t * Io_NtkBfsPads( Abc_Ntk_t * pNtk, Abc_Obj_t * pCurrEntry, unsigned numTerms, bool * pOrdered ); +static bool Abc_NodeIsNand2( Abc_Obj_t * pNode ); +static bool Abc_NodeIsNor2( Abc_Obj_t * pNode ); +static bool Abc_NodeIsAnd2( Abc_Obj_t * pNode ); +static bool Abc_NodeIsOr2( Abc_Obj_t * pNode ); +static bool Abc_NodeIsXor2( Abc_Obj_t * pNode ); +static bool Abc_NodeIsXnor2( Abc_Obj_t * pNode ); + +static inline double Abc_Rint( double x ) { return (double)(int)x; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Write the network into a Bookshelf file with the given name.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteBookLogic( Abc_Ntk_t * pNtk, char * FileName ) +{ + Abc_Ntk_t * pNtkTemp; + // derive the netlist + pNtkTemp = Abc_NtkToNetlist(pNtk); + if ( pNtkTemp == NULL ) + { + fprintf( stdout, "Writing BOOK has failed.\n" ); + return; + } + Io_WriteBook( pNtkTemp, FileName ); + Abc_NtkDelete( pNtkTemp ); +} + +/**Function************************************************************* + + Synopsis [Write the network into a BOOK file with the given name.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteBook( Abc_Ntk_t * pNtk, char * FileName ) +{ + + FILE * pFileNodes, * pFileNets, * pFileAux; + FILE * pFileScl, * pFilePl, * pFileWts; + char * FileExt = (char *)calloc(strlen(FileName)+7, sizeof(char)); + unsigned coreCellArea=0; + Abc_Ntk_t * pExdc, * pNtkTemp; + int i; + + assert( Abc_NtkIsNetlist(pNtk) ); + // start writing the files + strcpy(FileExt, FileName); + pFileNodes = fopen( strcat(FileExt,".nodes"), "w" ); + strcpy(FileExt, FileName); + pFileNets = fopen( strcat(FileExt,".nets"), "w" ); + strcpy(FileExt, FileName); + pFileAux = fopen( strcat(FileExt,".aux"), "w" ); + + // write the aux file + if ( (pFileNodes == NULL) || (pFileNets == NULL) || (pFileAux == NULL) ) + { + fprintf( stdout, "Io_WriteBook(): Cannot open the output files.\n" ); + return; + } + fprintf( pFileAux, "RowBasedPlacement : %s.nodes %s.nets %s.scl %s.pl %s.wts", + FileName, FileName, FileName, FileName, FileName ); + fclose( pFileAux ); + + // write the master network + coreCellArea+=Io_NtkWriteNodes( pFileNodes, pNtk ); + Io_NtkWriteNets( pFileNets, pNtk ); + + // write EXDC network if it exists + pExdc = Abc_NtkExdc( pNtk ); + if ( pExdc ) + { + coreCellArea+=Io_NtkWriteNodes( pFileNodes, pNtk ); + Io_NtkWriteNets( pFileNets, pNtk ); + } + + // make sure there is no logic hierarchy + assert( Abc_NtkWhiteboxNum(pNtk) == 0 ); + + // write the hierarchy if present + if ( Abc_NtkBlackboxNum(pNtk) > 0 ) + { + Vec_PtrForEachEntry( pNtk->pDesign->vModules, pNtkTemp, i ) + { + if ( pNtkTemp == pNtk ) + continue; + coreCellArea+=Io_NtkWriteNodes( pFileNodes, pNtkTemp ); + Io_NtkWriteNets( pFileNets, pNtkTemp ); + } + } + fclose( pFileNodes ); + fclose( pFileNets ); + + strcpy(FileExt, FileName); + pFileScl = fopen( strcat(FileExt,".scl"), "w" ); + strcpy(FileExt, FileName); + pFilePl = fopen( strcat(FileExt,".pl"), "w" ); + strcpy(FileExt, FileName); + pFileWts = fopen( strcat(FileExt,".wts"), "w" ); + free(FileExt); + + Io_NtkBuildLayout( pFileScl, pFilePl, pNtk, 1.0, 10, coreCellArea ); + fclose( pFileScl ); + fclose( pFilePl ); + fclose( pFileWts ); +} + +/**Function************************************************************* + + Synopsis [Write the network into a BOOK file with the given name.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Io_NtkWriteNodes( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + ProgressBar * pProgress; + Abc_Obj_t * pLatch, * pNode; + unsigned numTerms, numNodes, coreCellArea=0; + int i; + + assert( Abc_NtkIsNetlist(pNtk) ); + // write the forehead + numTerms=Abc_NtkPiNum(pNtk)+Abc_NtkPoNum(pNtk); + numNodes=numTerms+Abc_NtkNodeNum(pNtk)+Abc_NtkLatchNum(pNtk); + printf("NumNodes : %d\t", numNodes ); + printf("NumTerminals : %d\n", numTerms ); + fprintf( pFile, "UCLA nodes 1.0\n"); + fprintf( pFile, "NumNodes : %d\n", numNodes ); + fprintf( pFile, "NumTerminals : %d\n", numTerms ); + // write the PI/POs + Io_NtkWritePiPoNodes( pFile, pNtk ); + // write the latches + if ( !Abc_NtkIsComb(pNtk) ) + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + Io_NtkWriteLatchNode( pFile, pLatch, NODES ); + coreCellArea+=6*coreHeight; + } + // write each internal node + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + coreCellArea+=Io_NtkWriteIntNode( pFile, pNode, NODES ); + } + Extra_ProgressBarStop( pProgress ); + return coreCellArea; +} + +/**Function************************************************************* + + Synopsis [Writes the primary input nodes into a file] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_NtkWritePiPoNodes( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pTerm, * pNet; + int i; + + Abc_NtkForEachPi( pNtk, pTerm, i ) + { + pNet = Abc_ObjFanout0(pTerm); + fprintf( pFile, "i%s_input\t", Abc_ObjName(pNet) ); + fprintf( pFile, "terminal "); + fprintf( pFile, " %d %d\n", termWidth, termHeight ); + } + + Abc_NtkForEachPo( pNtk, pTerm, i ) + { + pNet = Abc_ObjFanin0(pTerm); + fprintf( pFile, "o%s_output\t", Abc_ObjName(pNet) ); + fprintf( pFile, "terminal "); + fprintf( pFile, " %d %d\n", termWidth, termHeight ); + } +} + +/**Function************************************************************* + + Synopsis [Write the latch nodes into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_NtkWriteLatchNode( FILE * pFile, Abc_Obj_t * pLatch, bool NodesOrPl ) +{ + Abc_Obj_t * pNetLi, * pNetLo; + + pNetLi = Abc_ObjFanin0( Abc_ObjFanin0(pLatch) ); + pNetLo = Abc_ObjFanout0( Abc_ObjFanout0(pLatch) ); + /// write the latch line + fprintf( pFile, "%s_%s_latch\t", Abc_ObjName(pNetLi), Abc_ObjName(pNetLo) ); + if (NodesOrPl == NODES) + fprintf( pFile, " %d %d\n", 6, 1 ); +} + +/**Function************************************************************* + + Synopsis [Write the internal node into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Io_NtkWriteIntNode( FILE * pFile, Abc_Obj_t * pNode, bool NodesOrPl ) +{ + unsigned sizex=0, sizey=coreHeight, isize=0; + //double nx, ny, xstep, ystep; + Abc_Obj_t * pNeti, *pNeto; + int i; + + // write the network after mapping + if ( Abc_NtkHasMapping(pNode->pNtk) ) + sizex=Io_NtkWriteNodeGate( pFile, pNode ); + else + { + Abc_ObjForEachFanin( pNode, pNeti, i ) + fprintf( pFile, "%s_", Abc_ObjName(pNeti) ); + Abc_ObjForEachFanout( pNode, pNeto, i ) + fprintf( pFile, "%s_", Abc_ObjName(pNeto) ); + fprintf( pFile, "name\t" ); + + if(NodesOrPl == NODES) + { + isize=Abc_ObjFaninNum(pNode); + if ( Abc_NodeIsConst0(pNode) || Abc_NodeIsConst1(pNode) ) + sizex=0; + else if ( Abc_NodeIsInv(pNode) ) + sizex=1; + else if ( Abc_NodeIsBuf(pNode) ) + sizex=2; + else + { + assert( Abc_NtkHasSop(pNode->pNtk) ); + if ( Abc_NodeIsNand2(pNode) || Abc_NodeIsNor2(pNode) ) + sizex=2; + else if ( Abc_NodeIsAnd2(pNode) || Abc_NodeIsOr2(pNode) ) + sizex=3; + else if ( Abc_NodeIsXor2(pNode) || Abc_NodeIsXnor2(pNode) ) + sizex=5; + else + { + assert( isize > 2 ); + sizex=isize+Abc_SopGetCubeNum(pNode->pData); + } + } + } + } + if(NodesOrPl == NODES) + { + fprintf( pFile, " %d %d\n", sizex, sizey ); + + // Equally place pins. Size pins needs / isize+#output+1 + isize= isize + Abc_ObjFanoutNum(pNode) + 1; + } + return sizex*sizey; + /* + xstep = sizex / isize; + ystep = sizey / isize; + nx= -0.5 * sizex; + ny= -0.5 * sizey; + + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + nx+= xstep; + ny+= ystep; + if (fabs(nx) < 0.001) + nx= 0; + if (fabs(ny) < 0.001) + ny= 0; + } + Abc_ObjForEachFanout( pNode, pFanout, i ) + { + nx+= xstep; + ny+= ystep; + if (fabs(nx) < 0.001) + nx= 0; + if (fabs(ny) < 0.001) + ny= 0; + } + */ +} + +/**Function************************************************************* + + Synopsis [Writes the internal node after tech mapping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode ) +{ + Mio_Gate_t * pGate = pNode->pData; + Mio_Pin_t * pGatePin; + int i; + // write the node gate + for ( pGatePin = Mio_GateReadPins(pGate), i = 0; pGatePin; pGatePin = Mio_PinReadNext(pGatePin), i++ ) + fprintf( pFile, "%s_", Abc_ObjName( Abc_ObjFanin(pNode,i) ) ); + assert ( i == Abc_ObjFaninNum(pNode) ); + fprintf( pFile, "%s_%s\t", Abc_ObjName( Abc_ObjFanout0(pNode) ), Mio_GateReadName(pGate) ); + return Mio_GateReadArea(pGate); +} + +/**Function************************************************************* + + Synopsis [Write the nets into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_NtkWriteNets( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + ProgressBar * pProgress; + Abc_Obj_t * pNet; + unsigned numPin=0; + int i; + + assert( Abc_NtkIsNetlist(pNtk) ); + // write the head + Abc_NtkForEachNet( pNtk, pNet, i ) + numPin+=Abc_ObjFaninNum(pNet)+Abc_ObjFanoutNum(pNet); + printf( "NumNets : %d\t", Abc_NtkNetNum(pNtk) ); + printf( "NumPins : %d\n\n", numPin ); + fprintf( pFile, "UCLA nets 1.0\n"); + fprintf( pFile, "NumNets : %d\n", Abc_NtkNetNum(pNtk) ); + fprintf( pFile, "NumPins : %d\n", numPin ); + + // write nets + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNetNum(pNtk) ); + Abc_NtkForEachNet( pNtk, pNet, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + Io_NtkWriteIntNet( pFile, pNet ); + } + Extra_ProgressBarStop( pProgress ); +} + +/**Function************************************************************* + + Synopsis [Write the nets into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_NtkWriteIntNet( FILE * pFile, Abc_Obj_t * pNet ) +{ + Abc_Obj_t * pFanin, * pFanout; + Abc_Obj_t * pNeti, * pNeto; + Abc_Obj_t * pNetLi, * pNetLo, * pLatch; + int i, j; + int NetDegree=Abc_ObjFaninNum(pNet)+Abc_ObjFanoutNum(pNet); + + fprintf( pFile, "NetDegree\t:\t\t%d\t\t%s\n", NetDegree, Abc_ObjName(Abc_ObjFanin0(pNet)) ); + + pFanin=Abc_ObjFanin0(pNet); + if ( Abc_ObjIsPi(pFanin) ) + fprintf( pFile, "i%s_input I\n", Abc_ObjName(pNet) ); + else + { + if(!Abc_NtkIsComb(pNet->pNtk) && Abc_ObjFaninNum(pFanin) && Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) ) + { + pLatch=Abc_ObjFanin0(pFanin); + pNetLi=Abc_ObjFanin0(Abc_ObjFanin0(pLatch)); + pNetLo=Abc_ObjFanout0(Abc_ObjFanout0(pLatch)); + fprintf( pFile, "%s_%s_latch I : ", Abc_ObjName(pNetLi), Abc_ObjName(pNetLo) ); + } + else + { + Abc_ObjForEachFanin( pFanin, pNeti, j ) + fprintf( pFile, "%s_", Abc_ObjName(pNeti) ); + Abc_ObjForEachFanout( pFanin, pNeto, j ) + fprintf( pFile, "%s_", Abc_ObjName(pNeto) ); + if ( Abc_NtkHasMapping(pNet->pNtk) ) + fprintf( pFile, "%s : ", Mio_GateReadName(pFanin->pData) ); + else + fprintf( pFile, "name I : " ); + } + // offsets are simlply 0.00 0.00 at the moment + fprintf( pFile, "%.2f %.2f\n", .0, .0 ); + } + + Abc_ObjForEachFanout( pNet, pFanout, i ) + { + if ( Abc_ObjIsPo(pFanout) ) + fprintf( pFile, "o%s_output O\n", Abc_ObjName(pNet) ); + else + { + if(!Abc_NtkIsComb(pNet->pNtk) && Abc_ObjFanoutNum(pFanout) && Abc_ObjIsLatch( Abc_ObjFanout0(pFanout) ) ) + { + pLatch=Abc_ObjFanout0(pFanout); + pNetLi=Abc_ObjFanin0(Abc_ObjFanin0(pLatch)); + pNetLo=Abc_ObjFanout0(Abc_ObjFanout0(pLatch)); + fprintf( pFile, "%s_%s_latch O : ", Abc_ObjName(pNetLi), Abc_ObjName(pNetLo) ); + } + else + { + Abc_ObjForEachFanin( pFanout, pNeti, j ) + fprintf( pFile, "%s_", Abc_ObjName(pNeti) ); + Abc_ObjForEachFanout( pFanout, pNeto, j ) + fprintf( pFile, "%s_", Abc_ObjName(pNeto) ); + if ( Abc_NtkHasMapping(pNet->pNtk) ) + fprintf( pFile, "%s : ", Mio_GateReadName(pFanout->pData) ); + else + fprintf( pFile, "name O : " ); + } + // offsets are simlply 0.00 0.00 at the moment + fprintf( pFile, "%.2f %.2f\n", .0, .0 ); + } + } +} + +/**Function************************************************************* + + Synopsis [Write the network into a BOOK file with the given name.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_NtkBuildLayout( FILE * pFileScl, FILE * pFilePl, Abc_Ntk_t * pNtk, double aspectRatio, double whiteSpace, unsigned coreCellArea ) +{ + unsigned numCoreCells=Abc_NtkNodeNum(pNtk)+Abc_NtkLatchNum(pNtk); + double targetLayoutArea = coreCellArea/(1.0-(whiteSpace/100.0)); + unsigned numCoreRows=(aspectRatio>0.0) ? (Abc_Rint(sqrt(targetLayoutArea/aspectRatio)/coreHeight)) : 0; + unsigned numTerms=Abc_NtkPiNum(pNtk)+Abc_NtkPoNum(pNtk); + unsigned totalWidth=coreCellArea/coreHeight; + double layoutHeight = numCoreRows * coreHeight; + double layoutWidth = Abc_Rint(targetLayoutArea/layoutHeight); + double actualLayoutArea = layoutWidth * layoutHeight; + + printf( "Core cell height(==site height) is %d\n", coreHeight ); + printf( "Total core cell width is %d giving an ave width of %f\n", totalWidth, (double)(totalWidth/numCoreCells)); + printf( "Target Dimensions:\n" ); + printf( " Area : %f\n", targetLayoutArea ); + printf( " WS%% : %f\n", whiteSpace ); + printf( " AR : %f\n", aspectRatio ); + printf( "Actual Dimensions:\n" ); + printf( " Width : %f\n", layoutWidth ); + printf( " Height: %f (%d rows)\n", layoutHeight, numCoreRows); + printf( " Area : %f\n", actualLayoutArea ); + printf( " WS%% : %f\n", 100*(actualLayoutArea-coreCellArea)/actualLayoutArea ); + printf( " AR : %f\n\n", layoutWidth/layoutHeight ); + + Io_NtkWriteScl( pFileScl, numCoreRows, layoutWidth ); + Io_NtkWritePl( pFilePl, pNtk, numTerms, layoutHeight, layoutWidth ); +} + +/**Function************************************************************* + + Synopsis [Write the network into a BOOK file with the given name.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_NtkWriteScl( FILE * pFile, unsigned numCoreRows, double layoutWidth ) +{ + int origin_y=0; + char * rowOrients[2] = {"N", "FS"}; + char symmetry='Y'; + double sitewidth=1.0; + double spacing=1.0; + + int rowId; + // write the forehead + fprintf( pFile, "UCLA scl 1.0\n\n" ); + fprintf( pFile, "Numrows : %d\n\n", numCoreRows ); + + for( rowId=0 ; rowId0 ) + { + pNeighbor = Vec_PtrEntry( vNeighbors, 0 ); + assert( Abc_ObjIsNode(pNeighbor) || Abc_ObjIsTerm(pNeighbor) ); + Vec_PtrRemove( vNeighbors, pNeighbor ); + + if( Abc_NodeIsTravIdCurrent( pNeighbor ) ) + continue; + Abc_NodeSetTravIdCurrent( pNeighbor ); + + if( ((Abc_ObjIsPi(pNeighbor) || Abc_ObjIsPo(pNeighbor))) && !pOrdered[Abc_ObjId(pNeighbor)] ) + { + foundNeighbor=1; + break; + } + if( Abc_ObjFanoutNum( pNeighbor ) ) + { + pNet=Abc_ObjFanout0( pNeighbor ); + if( !Abc_NtkIsComb(pNtk) && Abc_ObjIsLatch(pNet) ) + pNet=Abc_ObjFanout0( Abc_ObjFanout0(pNet) ); + Abc_ObjForEachFanout( pNet, pNode, i ) + if( !Abc_NodeIsTravIdCurrent(pNode) ) + Vec_PtrPush( vNeighbors, pNode ); + } + if( Abc_ObjFaninNum( pNeighbor ) ) + { + if( !Abc_NtkIsComb(pNtk) && Abc_ObjIsLatch(Abc_ObjFanin0(pNeighbor)) ) + pNeighbor=Abc_ObjFanin0( Abc_ObjFanin0(pNeighbor) ); + Abc_ObjForEachFanin( pNeighbor, pNet, i ) + if( !Abc_NodeIsTravIdCurrent(pNode=Abc_ObjFanin0(pNet)) ) + Vec_PtrPush( vNeighbors, pNode ); + } + } + return ( foundNeighbor ) ? pNeighbor : pTerm; +} + +/**Function************************************************************* + + Synopsis [Test is the node is nand2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NodeIsNand2( Abc_Obj_t * pNode ) +{ + Abc_Ntk_t * pNtk = pNode->pNtk; + assert( Abc_NtkIsNetlist(pNtk) ); + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_ObjFaninNum(pNode) != 2 ) + return 0; + if ( Abc_NtkHasSop(pNtk) ) + return ( !strcmp((pNode->pData), "-0 1\n0- 1\n") || + !strcmp((pNode->pData), "0- 1\n-0 1\n") || + !strcmp((pNode->pData), "11 0\n") ); + if ( Abc_NtkHasMapping(pNtk) ) + return pNode->pData == Mio_LibraryReadNand2(Abc_FrameReadLibGen()); + assert( 0 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Test is the node is nand2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NodeIsNor2( Abc_Obj_t * pNode ) +{ + Abc_Ntk_t * pNtk = pNode->pNtk; + assert( Abc_NtkIsNetlist(pNtk) ); + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_ObjFaninNum(pNode) != 2 ) + return 0; + if ( Abc_NtkHasSop(pNtk) ) + return ( !strcmp((pNode->pData), "00 1\n") ); + assert( 0 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Test is the node is and2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NodeIsAnd2( Abc_Obj_t * pNode ) +{ + Abc_Ntk_t * pNtk = pNode->pNtk; + assert( Abc_NtkIsNetlist(pNtk) ); + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_ObjFaninNum(pNode) != 2 ) + return 0; + if ( Abc_NtkHasSop(pNtk) ) + return Abc_SopIsAndType((pNode->pData)); + if ( Abc_NtkHasMapping(pNtk) ) + return pNode->pData == Mio_LibraryReadAnd2(Abc_FrameReadLibGen()); + assert( 0 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Test is the node is or2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NodeIsOr2( Abc_Obj_t * pNode ) +{ + Abc_Ntk_t * pNtk = pNode->pNtk; + assert( Abc_NtkIsNetlist(pNtk) ); + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_ObjFaninNum(pNode) != 2 ) + return 0; + if ( Abc_NtkHasSop(pNtk) ) + return ( Abc_SopIsOrType((pNode->pData)) || + !strcmp((pNode->pData), "01 0\n") || + !strcmp((pNode->pData), "10 0\n") || + !strcmp((pNode->pData), "00 0\n") ); + //off-sets, too + assert( 0 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Test is the node is xor2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NodeIsXor2( Abc_Obj_t * pNode ) +{ + Abc_Ntk_t * pNtk = pNode->pNtk; + assert( Abc_NtkIsNetlist(pNtk) ); + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_ObjFaninNum(pNode) != 2 ) + return 0; + if ( Abc_NtkHasSop(pNtk) ) + return ( !strcmp((pNode->pData), "01 1\n10 1\n") || !strcmp((pNode->pData), "10 1\n01 1\n") ); + assert( 0 ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Test is the node is xnor2.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NodeIsXnor2( Abc_Obj_t * pNode ) +{ + Abc_Ntk_t * pNtk = pNode->pNtk; + assert( Abc_NtkIsNetlist(pNtk) ); + assert( Abc_ObjIsNode(pNode) ); + if ( Abc_ObjFaninNum(pNode) != 2 ) + return 0; + if ( Abc_NtkHasSop(pNtk) ) + return ( !strcmp((pNode->pData), "11 1\n00 1\n") || !strcmp((pNode->pData), "00 1\n11 1\n") ); + assert( 0 ); + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/io/io_.c b/src/base/io/io_.c deleted file mode 100644 index b24d1299..00000000 --- a/src/base/io/io_.c +++ /dev/null @@ -1,48 +0,0 @@ -/**CFile**************************************************************** - - FileName [io_.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Command processing package.] - - Synopsis [Procedure to read network from file.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: io_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "ioAbc.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - - diff --git a/src/base/io/module.make b/src/base/io/module.make index bb35a7fc..6f4e2539 100644 --- a/src/base/io/module.make +++ b/src/base/io/module.make @@ -16,6 +16,7 @@ SRC += src/base/io/io.c \ src/base/io/ioWriteBench.c \ src/base/io/ioWriteBlif.c \ src/base/io/ioWriteBlifMv.c \ + src/base/io/ioWriteBook.c \ src/base/io/ioWriteCnf.c \ src/base/io/ioWriteDot.c \ src/base/io/ioWriteEqn.c \ diff --git a/src/base/main/main.c b/src/base/main/main.c index bfa91ddc..a9d610fd 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -216,14 +216,14 @@ int main( int argc, char * argv[] ) if ( fStatus == -1 || fStatus == -2 ) break; } - } + } // if the memory should be freed, quit packages if ( fStatus < 0 ) { Abc_Stop(); - } - return 0; + } + return 0; usage: Abc_UtilsPrintHello( pAbc ); diff --git a/src/base/main/main.h b/src/base/main/main.h index af0ed24d..159122d2 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -65,15 +65,16 @@ typedef struct Abc_Frame_t_ Abc_Frame_t; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// + #ifdef WIN32 -#define DLLEXPORT __declspec(dllexport) -#define DLLIMPORT __declspec(dllimport) +#define ABC_DLLEXPORT __declspec(dllexport) +#define ABC_DLLIMPORT __declspec(dllimport) #else /* defined(WIN32) */ -#define DLLIMPORT +#define ABC_DLLIMPORT #endif /* defined(WIN32) */ #ifndef ABC_DLL -#define ABC_DLL DLLIMPORT +#define ABC_DLL ABC_DLLIMPORT #endif /*=== main.c ===========================================================*/ @@ -103,6 +104,7 @@ extern ABC_DLL Vec_Ptr_t * Abc_FrameReadStore(); extern ABC_DLL int Abc_FrameReadStoreSize(); extern ABC_DLL void * Abc_FrameReadLibLut(); extern ABC_DLL void * Abc_FrameReadLibGen(); +extern ABC_DLL void * Abc_FrameReadLibGen2(); extern ABC_DLL void * Abc_FrameReadLibSuper(); extern ABC_DLL void * Abc_FrameReadLibVer(); extern ABC_DLL void * Abc_FrameReadManDd(); @@ -114,6 +116,7 @@ extern ABC_DLL void Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_FrameSetNtkStoreSize( int nStored ); extern ABC_DLL void Abc_FrameSetLibLut( void * pLib ); extern ABC_DLL void Abc_FrameSetLibGen( void * pLib ); +extern ABC_DLL void Abc_FrameSetLibGen2( void * pLib ); extern ABC_DLL void Abc_FrameSetLibSuper( void * pLib ); extern ABC_DLL void Abc_FrameSetLibVer( void * pLib ); extern ABC_DLL void Abc_FrameSetFlag( char * pFlag, char * pValue ); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index f02ade1c..23e9184e 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -47,6 +47,7 @@ Vec_Ptr_t * Abc_FrameReadStore() { return s_GlobalFrame->vSt int Abc_FrameReadStoreSize() { return Vec_PtrSize(s_GlobalFrame->vStore); } void * Abc_FrameReadLibLut() { return s_GlobalFrame->pLibLut; } void * Abc_FrameReadLibGen() { return s_GlobalFrame->pLibGen; } +void * Abc_FrameReadLibGen2() { return s_GlobalFrame->pLibGen2; } void * Abc_FrameReadLibSuper() { return s_GlobalFrame->pLibSuper; } void * Abc_FrameReadLibVer() { return s_GlobalFrame->pLibVer; } void * Abc_FrameReadManDd() { if ( s_GlobalFrame->dd == NULL ) s_GlobalFrame->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); return s_GlobalFrame->dd; } @@ -55,6 +56,7 @@ char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagReadByName void Abc_FrameSetLibLut( void * pLib ) { s_GlobalFrame->pLibLut = pLib; } void Abc_FrameSetLibGen( void * pLib ) { s_GlobalFrame->pLibGen = pLib; } +void Abc_FrameSetLibGen2( void * pLib ) { s_GlobalFrame->pLibGen2 = pLib; } void Abc_FrameSetLibSuper( void * pLib ) { s_GlobalFrame->pLibSuper = pLib; } void Abc_FrameSetLibVer( void * pLib ) { s_GlobalFrame->pLibVer = pLib; } void Abc_FrameSetFlag( char * pFlag, char * pValue ) { Cmd_FlagUpdateValue( s_GlobalFrame, pFlag, pValue ); } diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index becbfd6b..cfd945b7 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -71,6 +71,7 @@ struct Abc_Frame_t_ // libraries for mapping void * pLibLut; // the current LUT library void * pLibGen; // the current genlib + void * pLibGen2; // the current genlib void * pLibSuper; // the current supergate library void * pLibVer; // the current Verilog library @@ -97,15 +98,16 @@ struct Abc_Frame_t_ //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// + #ifdef WIN32 -#define DLLEXPORT __declspec(dllexport) -#define DLLIMPORT __declspec(dllimport) +#define ABC_DLLEXPORT __declspec(dllexport) +#define ABC_DLLIMPORT __declspec(dllimport) #else /* defined(WIN32) */ -#define DLLIMPORT +#define ABC_DLLIMPORT #endif /* defined(WIN32) */ #ifndef ABC_DLL -#define ABC_DLL DLLIMPORT +#define ABC_DLL ABC_DLLIMPORT #endif /*=== mvMain.c ===========================================================*/ -- cgit v1.2.3