From f65983c2c0810cfb933f696952325a81d2378987 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 28 Feb 2008 08:01:00 -0800 Subject: Version abc80228 --- src/base/abc/abc.h | 4 +- src/base/abci/abc.c | 247 ++++++++++++++++++++++++++++++----------------- src/base/abci/abcDar.c | 75 +++++++------- src/base/abci/abcDelay.c | 73 +++++++++++--- src/base/abci/abcIf.c | 2 + src/base/abci/abcPrint.c | 13 ++- 6 files changed, 265 insertions(+), 149 deletions(-) (limited to 'src/base') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index fdff8b39..86cc7e62 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -567,6 +567,8 @@ extern void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, extern void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst ); extern void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj ); extern void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj ); +/*=== abcDelay.c ==========================================================*/ +extern float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib ); /*=== abcDfs.c ==========================================================*/ extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll ); extern Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes ); @@ -733,7 +735,7 @@ extern bool Abc_NodeIsBuf( Abc_Obj_t * pNode ); extern bool Abc_NodeIsInv( Abc_Obj_t * pNode ); extern void Abc_NodeComplement( Abc_Obj_t * pNode ); /*=== abcPrint.c ==========================================================*/ -extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest ); +extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib ); extern void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk ); extern void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ); extern void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 492d1910..99da9201 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30,6 +30,7 @@ #include "aig.h" #include "dar.h" #include "mfs.h" +#include "fra.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -442,6 +443,8 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int fFactor; int fSaveBest; + int fDumpResult; + int fUseLutLib; int c; pNtk = Abc_FrameReadNtk(pAbc); @@ -451,8 +454,10 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) // set the defaults fFactor = 0; fSaveBest = 0; + fDumpResult = 0; + fUseLutLib = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "fbh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "fbdlh" ) ) != EOF ) { switch ( c ) { @@ -462,6 +467,12 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': fSaveBest ^= 1; break; + case 'd': + fDumpResult ^= 1; + break; + case 'l': + fUseLutLib ^= 1; + break; case 'h': goto usage; default: @@ -474,14 +485,16 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" ); return 1; } - Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest ); + Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib ); return 0; usage: - fprintf( pErr, "usage: print_stats [-fbh]\n" ); + fprintf( pErr, "usage: print_stats [-fbdlh]\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" ); + fprintf( pErr, "\t-d : toggles dumping network into file \"_dump.blif\" [default = %s]\n", fDumpResult? "yes": "no" ); + fprintf( pErr, "\t-l : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fSaveBest? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -567,7 +580,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 ); + Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0 ); return 0; usage: @@ -672,7 +685,7 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fPrintSccs = 0; + fPrintSccs = 1; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF ) { @@ -6829,7 +6842,8 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk;//, * pNtkRes; + Abc_Ntk_t * pNtk; +// Abc_Ntk_t * pNtkRes; int c; int fBmc; int nFrames; @@ -6849,14 +6863,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); // extern void Abc_NtkDarTestBlif( char * pFileName ); - extern void Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); +// extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); -// printf( "This command is temporarily disabled.\n" ); -// return 0; + printf( "This command is temporarily disabled.\n" ); + return 0; // set defaults fVeryVerbose = 0; @@ -7032,8 +7046,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkDarTestBlif( argv[globalUtilOptind] ); */ - Abc_NtkDarPartition( pNtk ); - +// Abc_NtkDarPartition( pNtk ); +/* + pNtkRes = Abc_NtkDarPartition( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); +*/ return 0; usage: fprintf( pErr, "usage: test [-vwh]\n" ); @@ -10825,6 +10848,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get LUT size from the library pPars->nLutSize = pPars->pLutLib->LutMax; + // if variable pin delay, force truth table computation + if ( pPars->pLutLib->fVarPinDelays ) + pPars->fTruth = 1; } if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE ) @@ -11646,6 +11672,7 @@ usage: fprintf( pErr, "\t-h : print the command usage\n"); return 1; } + /**Function************************************************************* Synopsis [] @@ -11665,12 +11692,14 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) int fForward; int fBackward; int fVerbose; - int fComputeInit; + int fComputeInit, fGuaranteeInit, fBlockConst; + int fFastButConservative; int maxDelay; - extern Abc_Ntk_t* Abc_FlowRetime_MinReg( Abc_Ntk_t * pNtk, int fVerbose, int fComputeInit, + 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 maxDelay, int fFastButConservative); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -11678,13 +11707,16 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fForward = 0; + fFastButConservative = 0; fBackward = 0; fComputeInit = 1; + fGuaranteeInit = 0; fVerbose = 0; + fBlockConst = 0; nMaxIters = 999; maxDelay = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MDfbivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MDfcgbkivh" ) ) != EOF ) { switch ( c ) { @@ -11709,16 +11741,25 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) globalUtilOptind++; if ( maxDelay < 0 ) goto usage; - break; + break; case 'f': fForward ^= 1; break; + case 'c': + fFastButConservative ^= 1; + break; case 'i': fComputeInit ^= 1; break; case 'b': fBackward ^= 1; break; + case 'g': + fGuaranteeInit ^= 1; + break; + case 'k': + fBlockConst ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -11741,6 +11782,12 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } + if ( fGuaranteeInit && !fComputeInit ) + { + fprintf( pErr, "Initial state guarantee (-g) requires initial state computation (-i).\n" ); + return 1; + } + if ( !Abc_NtkLatchNum(pNtk) ) { fprintf( pErr, "The network has no latches. Retiming is not performed.\n" ); @@ -11754,7 +11801,10 @@ int Abc_CommandFlowRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) } // perform the retiming - pNtkRes = Abc_FlowRetime_MinReg( pNtk, fVerbose, fComputeInit, fForward, fBackward, nMaxIters, maxDelay ); + pNtkRes = Abc_FlowRetime_MinReg( pNtk, fVerbose, fComputeInit, + fGuaranteeInit, fBlockConst, + fForward, fBackward, + nMaxIters, maxDelay, fFastButConservative ); if (pNtkRes != pNtk) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -11767,6 +11817,9 @@ usage: fprintf( pErr, "\t-M num : the maximum number of iterations [default = %d]\n", nMaxIters ); fprintf( pErr, "\t-D num : the maximum delay [default = none]\n" ); fprintf( pErr, "\t-i : enables init state computation [default = %s]\n", fComputeInit? "yes": "no" ); + fprintf( pErr, "\t-k : blocks retiming over const nodes [default = %s]\n", fBlockConst? "yes": "no" ); + fprintf( pErr, "\t-g : guarantees init state computation [default = %s]\n", fGuaranteeInit? "yes": "no" ); + fprintf( pErr, "\t-c : very fast (but conserv.) delay constraints [default = %s]\n", fFastButConservative? "yes": "no" ); fprintf( pErr, "\t-f : enables forward-only retiming [default = %s]\n", fForward? "yes": "no" ); fprintf( pErr, "\t-b : enables backward-only retiming [default = %s]\n", fBackward? "yes": "no" ); fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" ); @@ -12044,38 +12097,30 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; + Fra_Ssw_t Pars, * pPars = &Pars; int c; - int nFramesP; - int nFramesK; - int nMaxImps; - int nMaxLevs; - int fUseImps; - int fRewrite; - int fFraiging; - int fLatchCorr; - int fWriteImps; - int fUse1Hot; - int fVerbose; - extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nFramesP = 0; - nFramesK = 1; - nMaxImps = 5000; - nMaxLevs = 0; - fUseImps = 0; - fRewrite = 0; - fFraiging = 0; - fLatchCorr = 0; - fWriteImps = 0; - fUse1Hot = 0; - fVerbose = 0; + pPars->nPartSize = 0; + pPars->nOverSize = 0; + pPars->nFramesP = 0; + pPars->nFramesK = 1; + pPars->nMaxImps = 5000; + pPars->nMaxLevs = 0; + pPars->fUseImps = 0; + pPars->fRewrite = 0; + pPars->fFraiging = 0; + pPars->fLatchCorr = 0; + pPars->fWriteImps = 0; + pPars->fUse1Hot = 0; + pPars->fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PFILirfletvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILirfletvh" ) ) != EOF ) { switch ( c ) { @@ -12085,9 +12130,31 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); goto usage; } - nFramesP = atoi(argv[globalUtilOptind]); + pPars->nPartSize = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFramesP < 0 ) + if ( pPars->nPartSize < 2 ) + goto usage; + break; + case 'Q': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-Q\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nOverSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nOverSize < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesP = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesP < 0 ) goto usage; break; case 'F': @@ -12096,9 +12163,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nFramesK = atoi(argv[globalUtilOptind]); + pPars->nFramesK = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFramesK <= 0 ) + if ( pPars->nFramesK <= 0 ) goto usage; break; case 'I': @@ -12107,9 +12174,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); goto usage; } - nMaxImps = atoi(argv[globalUtilOptind]); + pPars->nMaxImps = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nMaxImps <= 0 ) + if ( pPars->nMaxImps <= 0 ) goto usage; break; case 'L': @@ -12118,31 +12185,31 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); goto usage; } - nMaxLevs = atoi(argv[globalUtilOptind]); + pPars->nMaxLevs = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nMaxLevs <= 0 ) + if ( pPars->nMaxLevs <= 0 ) goto usage; break; case 'i': - fUseImps ^= 1; + pPars->fUseImps ^= 1; break; case 'r': - fRewrite ^= 1; + pPars->fRewrite ^= 1; break; case 'f': - fFraiging ^= 1; + pPars->fFraiging ^= 1; break; case 'l': - fLatchCorr ^= 1; + pPars->fLatchCorr ^= 1; break; case 'e': - fWriteImps ^= 1; + pPars->fWriteImps ^= 1; break; case 't': - fUse1Hot ^= 1; + pPars->fUse1Hot ^= 1; break; case 'v': - fVerbose ^= 1; + pPars->fVerbose ^= 1; break; case 'h': goto usage; @@ -12169,20 +12236,20 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } - if ( nFramesK > 1 && fUse1Hot ) + if ( pPars->nFramesK > 1 && pPars->fUse1Hot ) { printf( "Currrently can only use one-hotness for simple induction (K=1).\n" ); return 0; } - if ( nFramesP && fUse1Hot ) + if ( pPars->nFramesP && pPars->fUse1Hot ) { printf( "Currrently can only use one-hotness without prefix.\n" ); return 0; } // get the new network - pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fFraiging, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose ); + pNtkRes = Abc_NtkDarSeqSweep( pNtk, pPars ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -12193,19 +12260,21 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrfetvh]\n" ); + fprintf( pErr, "usage: ssweep [-PQNFL num] [-lrfetvh]\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); - fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP ); - fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK ); - fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", nMaxImps ); - fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", nMaxLevs ); - fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", fUseImps? "yes": "no" ); - fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" ); - fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" ); - fprintf( pErr, "\t-f : toggle fraiging (combinational SAT sweeping) [default = %s]\n", fFraiging? "yes": "no" ); - fprintf( pErr, "\t-e : toggle writing implications as assertions [default = %s]\n", fWriteImps? "yes": "no" ); - fprintf( pErr, "\t-t : toggle using one-hotness conditions [default = %s]\n", fUse1Hot? "yes": "no" ); - fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + 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 ); + fprintf( pErr, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP ); + fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK ); + fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs ); +// fprintf( pErr, "\t-I num : max number of implications to consider [default = %d]\n", pPars->nMaxImps ); +// fprintf( pErr, "\t-i : toggle using implications [default = %s]\n", pPars->fUseImps? "yes": "no" ); + fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); + fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", pPars->fRewrite? "yes": "no" ); + fprintf( pErr, "\t-f : toggle fraiging (combinational SAT sweeping) [default = %s]\n", pPars->fFraiging? "yes": "no" ); + fprintf( pErr, "\t-e : toggle writing implications as assertions [default = %s]\n", pPars->fWriteImps? "yes": "no" ); + fprintf( pErr, "\t-t : toggle using one-hotness conditions [default = %s]\n", pPars->fUse1Hot? "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"); return 1; } @@ -12331,29 +12400,29 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; - int fLatchSweep; - int fAutoSweep; + int fLatchConst; + int fLatchEqual; int fVerbose; - extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fLatchSweep = 0; - fAutoSweep = 0; + fLatchConst = 1; + fLatchEqual = 1; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "lavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cevh" ) ) != EOF ) { switch ( c ) { - case 'l': - fLatchSweep ^= 1; + case 'c': + fLatchConst ^= 1; break; - case 'a': - fAutoSweep ^= 1; + case 'e': + fLatchEqual ^= 1; break; case 'v': fVerbose ^= 1; @@ -12380,7 +12449,7 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } // modify the current network - pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchSweep, fVerbose ); + pNtkRes = Abc_NtkDarLatchSweep( pNtk, fLatchConst, fLatchEqual, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential cleanup has failed.\n" ); @@ -12391,13 +12460,11 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: scleanup [-lvh]\n" ); - fprintf( pErr, "\t performs sequential cleanup\n" ); - fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" ); - fprintf( pErr, "\t - removes stuck-at and identical latches (latch sweep)\n" ); -// fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" ); - fprintf( pErr, "\t-l : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" ); -// fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" ); + fprintf( pErr, "usage: scleanup [-cevh]\n" ); + fprintf( pErr, "\t performs sequential cleanup of the current network\n" ); + fprintf( pErr, "\t by removing nodes and latches that do not feed into POs\n" ); + fprintf( pErr, "\t-c : sweep stuck-at latches detected by ternary simulation [default = %s]\n", fLatchConst? "yes": "no" ); + fprintf( pErr, "\t-e : merge equal latches (same data inputs and init states) [default = %s]\n", fLatchEqual? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -13901,7 +13968,7 @@ usage: fprintf( pErr, "\t perform bounded model checking\n" ); fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit ); - fprintf( pErr, "\t-r : toggle initialization of the first frame [default = %s]\n", fRewrite? "yes": "no" ); + fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 119a2a97..6f5138c8 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -263,6 +263,25 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_NtkAddDummyBoxNames( pNtkNew ); else { + { + int i, k, iFlop, Counter = 0; + FILE * pFile; + pFile = fopen( "out.txt", "w" ); + fprintf( pFile, "The total of %d registers were removed (out of %d):\n", + Abc_NtkLatchNum(pNtkOld)-Vec_IntSize(pMan->vFlopNums), Abc_NtkLatchNum(pNtkOld) ); + for ( i = 0; i < Abc_NtkLatchNum(pNtkOld); i++ ) + { + Vec_IntForEachEntry( pMan->vFlopNums, iFlop, k ) + { + if ( i == iFlop ) + break; + } + if ( k == Vec_IntSize(pMan->vFlopNums) ) + fprintf( pFile, "%6d (%6d) : %s\n", ++Counter, i, Abc_ObjName( Abc_ObjFanout0(Abc_NtkBox(pNtkOld, i)) ) ); + } + fclose( pFile ); + //printf( "\n" ); + } assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) ); nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) ); Abc_NtkForEachLatch( pNtkNew, pObjNew, i ) @@ -1034,7 +1053,7 @@ PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int nMaxImps, int nMaxLevs, int fRewrite, int fFraiging, int fUseImps, int fLatchCorr, int fWriteImps, int fUse1Hot, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars ) { Fraig_Params_t Params; Abc_Ntk_t * pNtkAig, * pNtkFraig; @@ -1046,21 +1065,23 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in // so fraiging does not reduce the number of functions represented by nodes Fraig_ParamsSetDefault( &Params ); Params.nBTLimit = 100000; - if ( fFraiging ) + if ( pPars->fFraiging && pPars->nPartSize == 0 ) + { pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 ); - else - pNtkFraig = Abc_NtkDup( pNtk ); -if ( fVerbose ) +if ( pPars->fVerbose ) { PRT( "Initial fraiging time", clock() - clk ); } + } + else + pNtkFraig = Abc_NtkDup( pNtk ); pMan = Abc_NtkToDar( pNtkFraig, 1 ); Abc_NtkDelete( pNtkFraig ); if ( pMan == NULL ) return NULL; - pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose, NULL ); + pMan = Fra_FraigInduction( pTemp = pMan, pPars ); Aig_ManStop( pTemp ); if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) @@ -1283,7 +1304,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbose ) +Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan; @@ -1291,13 +1312,10 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbos if ( pMan == NULL ) return NULL; Aig_ManSeqCleanup( pMan ); - if ( fLatchSweep ) - { - if ( pMan->nRegs ) - pMan = Aig_ManReduceLaches( pMan, fVerbose ); - if ( pMan->nRegs ) - pMan = Aig_ManConstReduce( pMan, fVerbose ); - } + if ( fLatchConst && pMan->nRegs ) + pMan = Aig_ManConstReduce( pMan, fVerbose ); + if ( fLatchEqual && pMan->nRegs ) + pMan = Aig_ManReduceLaches( pMan, fVerbose ); pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); Aig_ManStop( pMan ); return pNtkAig; @@ -1557,41 +1575,16 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose ***********************************************************************/ void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose ) { +// extern Vec_Ptr_t * Aig_ManRegPartitionLinear( Aig_Man_t * pAig, int nPartSize ); Aig_Man_t * pMan; pMan = Abc_NtkToDar( pNtk, 1 ); if ( pMan == NULL ) return; Aig_ManComputeSccs( pMan ); +// Aig_ManRegPartitionLinear( pMan, 1000 ); Aig_ManStop( pMan ); } -/**Function************************************************************* - - Synopsis [Performs partitioning.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDarPartition( Abc_Ntk_t * pNtk ) -{ - extern void Aig_ManRegPartitionRun( Aig_Man_t * pAig ); - Aig_Man_t * pMan; - - // convert to the AIG manager - assert( Abc_NtkIsStrash(pNtk) ); - pMan = Abc_NtkToDar( pNtk, 1 ); - if ( pMan == NULL ) - return; - - Aig_ManRegPartitionRun( pMan ); - Aig_ManStop( pMan ); -} - - #include "ntl.h" diff --git a/src/base/abci/abcDelay.c b/src/base/abci/abcDelay.c index 7317b41b..bb654b73 100644 --- a/src/base/abci/abcDelay.c +++ b/src/base/abci/abcDelay.c @@ -74,7 +74,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD pPinPerm[best_i] = temp; } // verify - assert( pPinPerm[0] < Abc_ObjFaninNum(pNode) ); + assert( Abc_ObjFaninNum(pNode) == 0 || pPinPerm[0] < Abc_ObjFaninNum(pNode) ); for ( i = 1; i < Abc_ObjFaninNum(pNode); i++ ) { assert( pPinPerm[i] < Abc_ObjFaninNum(pNode) ); @@ -96,6 +96,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib ) { extern void * Abc_FrameReadLibLut(); + int fUseSorting = 0; int pPinPerm[32]; float pPinDelays[32]; If_Lib_t * pLutLib; @@ -144,10 +145,19 @@ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib ) else { pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)]; - Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); - Abc_ObjForEachFanin( pNode, pFanin, k ) - if ( tArrival < Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] ) - tArrival = Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k]; + if ( fUseSorting ) + { + Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); + Abc_ObjForEachFanin( pNode, pFanin, k ) + if ( tArrival < Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k] ) + tArrival = Abc_ObjArrival(Abc_ObjFanin(pNode,pPinPerm[k])) + pDelays[k]; + } + else + { + Abc_ObjForEachFanin( pNode, pFanin, k ) + if ( tArrival < Abc_ObjArrival(pFanin) + pDelays[k] ) + tArrival = Abc_ObjArrival(pFanin) + pDelays[k]; + } } if ( Abc_ObjFaninNum(pNode) == 0 ) tArrival = 0.0; @@ -188,12 +198,24 @@ float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib ) else { pDelays = pLutLib->pLutDelays[Abc_ObjFaninNum(pNode)]; - Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); - Abc_ObjForEachFanin( pNode, pFanin, k ) + if ( fUseSorting ) { - tRequired = Abc_ObjRequired(pNode) - pDelays[k]; - if ( Abc_ObjRequired(Abc_ObjFanin(pNode,pPinPerm[k])) > tRequired ) - Abc_ObjSetRequired( Abc_ObjFanin(pNode,pPinPerm[k]), tRequired ); + Abc_NtkDelayTraceSortPins( pNode, pPinPerm, pPinDelays ); + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + tRequired = Abc_ObjRequired(pNode) - pDelays[k]; + if ( Abc_ObjRequired(Abc_ObjFanin(pNode,pPinPerm[k])) > tRequired ) + Abc_ObjSetRequired( Abc_ObjFanin(pNode,pPinPerm[k]), tRequired ); + } + } + else + { + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + tRequired = Abc_ObjRequired(pNode) - pDelays[k]; + if ( Abc_ObjRequired(pFanin) > tRequired ) + Abc_ObjSetRequired( pFanin, tRequired ); + } } } // set slack for this object @@ -265,8 +287,17 @@ unsigned Abc_NtkDelayTraceTCEdges( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, float tD void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose ) { Abc_Obj_t * pNode; + If_Lib_t * pLutLib; int i, Nodes, * pCounters; float tArrival, tDelta, nSteps, Num; + // get the library + pLutLib = fUseLutLib? Abc_FrameReadLibLut() : NULL; + if ( pLutLib && pLutLib->LutMax < Abc_NtkGetFaninMax(pNtk) ) + { + printf( "The max LUT size (%d) is less than the max fanin count (%d).\n", + pLutLib->LutMax, Abc_NtkGetFaninMax(pNtk) ); + return; + } // decide how many steps nSteps = fUseLutLib ? 20 : Abc_NtkLevel(pNtk); pCounters = ALLOC( int, nSteps + 1 ); @@ -277,6 +308,8 @@ void Abc_NtkDelayTracePrint( Abc_Ntk_t * pNtk, int fUseLutLib, int fVerbose ) // count how many nodes have slack in the corresponding intervals Abc_NtkForEachNode( pNtk, pNode, i ) { + if ( Abc_ObjFaninNum(pNode) == 0 ) + continue; Num = Abc_ObjSlack(pNode) / tDelta; assert( Num >=0 && Num <= nSteps ); pCounters[(int)Num]++; @@ -356,15 +389,20 @@ int Abc_AigCheckTfi( Abc_Obj_t * pNew, Abc_Obj_t * pOld ) SeeAlso [] ***********************************************************************/ -void Abc_NtkSpeedupNode_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +int Abc_NtkSpeedupNode_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) { if ( Abc_NodeIsTravIdCurrent(pNode) ) - return; + return 1; + if ( Abc_ObjIsCi(pNode) ) + return 0; assert( Abc_ObjIsNode(pNode) ); Abc_NodeSetTravIdCurrent( pNode ); - Abc_NtkSpeedupNode_rec( Abc_ObjFanin0(pNode), vNodes ); - Abc_NtkSpeedupNode_rec( Abc_ObjFanin1(pNode), vNodes ); + if ( !Abc_NtkSpeedupNode_rec( Abc_ObjFanin0(pNode), vNodes ) ) + return 0; + if ( !Abc_NtkSpeedupNode_rec( Abc_ObjFanin1(pNode), vNodes ) ) + return 0; Vec_PtrPush( vNodes, pNode ); + return 1; } /**Function************************************************************* @@ -405,7 +443,12 @@ void Abc_NtkSpeedupNode( Abc_Ntk_t * pNtk, Abc_Ntk_t * pAig, Abc_Obj_t * pNode, } // traverse from the root node pAnd = pNode->pCopy; - Abc_NtkSpeedupNode_rec( Abc_ObjRegular(pAnd), vNodes ); + if ( !Abc_NtkSpeedupNode_rec( Abc_ObjRegular(pAnd), vNodes ) ) + { +// printf( "Bad node!!!\n" ); + Vec_PtrFree( vNodes ); + return; + } // derive cofactors nCofs = (1 << Vec_PtrSize(vTimes)); diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index 5d24398b..742a3a02 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -252,6 +252,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t // create a new node pNodeNew = Abc_NtkCreateNode( pNtkNew ); pCutBest = If_ObjCutBest( pIfObj ); + if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays ) + If_CutRotatePins( pIfMan, pCutBest ); if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv ) { If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i ) diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 5d35f329..239b155c 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -111,12 +111,20 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest ) +void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib ) { int Num; if ( fSaveBest ) Abc_NtkCompareAndSaveBest( pNtk ); + if ( fDumpResult ) + { + char Buffer[1000] = {0}; + char * pNameGen = pNtk->pSpec? Extra_FileNameGeneric( pNtk->pSpec ) : "nameless_"; + sprintf( Buffer, "%s_dump.blif", pNameGen ); + Io_Write( pNtk, Buffer, IO_FILE_BLIF ); + if ( pNtk->pSpec ) free( pNameGen ); + } // if ( Abc_NtkIsStrash(pNtk) ) // Abc_AigCountNext( pNtk->pManFunc ); @@ -181,7 +189,8 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave fprintf( pFile, " lev = %3d", Abc_AigLevel(pNtk) ); else fprintf( pFile, " lev = %3d", Abc_NtkLevel(pNtk) ); - + if ( fUseLutLib && Abc_FrameReadLibLut() ) + fprintf( pFile, " delay = %5.2f", Abc_NtkDelayTraceLut(pNtk, 1) ); fprintf( pFile, "\n" ); // Abc_NtkCrossCut( pNtk ); -- cgit v1.2.3