diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abc/abc.h | 1 | ||||
-rw-r--r-- | src/base/abc/abcNtk.c | 10 | ||||
-rw-r--r-- | src/base/abci/abc.c | 299 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 37 | ||||
-rw-r--r-- | src/base/abci/abcPrint.c | 10 |
5 files changed, 275 insertions, 82 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 11161698..e6f8b8f2 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -199,6 +199,7 @@ struct Abc_Ntk_t_ int * pModel; // counter-example (for miters) void * pSeqModel; // counter-example (for sequential miters) Abc_Ntk_t * pExdc; // the EXDC network (if given) + void * pManExdc; // the EXDC network (if given) void * pData; // misc Abc_Ntk_t * pCopy; Hop_Man_t * pHaig; // history AIG diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index d78a3a6a..85cb1569 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -23,6 +23,8 @@ #include "main.h" #include "mio.h" +#include "aig.h" + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -346,6 +348,8 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) // duplicate the EXDC Ntk if ( pNtk->pExdc ) pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc ); + if ( pNtk->pManExdc ) + pNtkNew->pManExdc = Aig_ManDup( pNtk->pManExdc, 0 ); if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" ); pNtk->pCopy = pNtkNew; @@ -431,6 +435,7 @@ Abc_Ntk_t * Abc_NtkDouble( Abc_Ntk_t * pNtk ) Abc_ObjAssignName( Abc_NtkCo(pNtkNew, i), "1_", Abc_ObjName(pObj) ); Abc_ObjAssignName( Abc_NtkCo(pNtkNew, Abc_NtkCoNum(pNtk) + i), "2_", Abc_ObjName(pObj) ); } + Abc_NtkOrderCisCos( pNtkNew ); // perform the final check if ( !Abc_NtkCheck( pNtkNew ) ) @@ -936,6 +941,11 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) // free EXDC Ntk if ( pNtk->pExdc ) Abc_NtkDelete( pNtk->pExdc ); + if ( pNtk->pManExdc ) + { + Aig_ManStop( pNtk->pManExdc ); + pNtk->pManExdc = NULL; + } // dereference the BDDs if ( Abc_NtkHasBdd(pNtk) ) { diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f0905155..338f38fc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -29,6 +29,7 @@ #include "lpk.h" #include "aig.h" #include "dar.h" +#include "mfs.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -66,8 +67,9 @@ static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandEliminate ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLutpack ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -244,8 +246,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "eliminate", Abc_CommandEliminate, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 ); - Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "lutpack", Abc_CommandLutpack, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "mfs", Abc_CommandMfs, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); @@ -650,17 +653,23 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; + int fPrintSccs; + extern void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fPrintSccs = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF ) { switch ( c ) { + case 's': + fPrintSccs ^= 1; + break; case 'h': goto usage; default: @@ -675,11 +684,14 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv ) } // print the nodes Abc_NtkPrintLatch( pOut, pNtk ); + if ( fPrintSccs ) + Abc_NtkPrintSccs( pNtk, 0 ); return 0; usage: - fprintf( pErr, "usage: print_latch [-h]\n" ); + fprintf( pErr, "usage: print_latch [-sh]\n" ); fprintf( pErr, "\t prints information about latches\n" ); + fprintf( pErr, "\t-s : toggles printing SCCs of registers [default = %s]\n", fPrintSccs? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -2946,6 +2958,158 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + Lpk_Par_t Pars, * pPars = &Pars; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + memset( pPars, 0, sizeof(Lpk_Par_t) ); + pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure + pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC + pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars) + pPars->nGrowthLevel = 0; // (L) the maximum number of increased levels + pPars->fSatur = 1; + pPars->fZeroCost = 0; + pPars->fFirst = 0; + pPars->fOldAlgo = 0; + pPars->fVerbose = 0; + pPars->fVeryVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfovwh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLutsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLutsMax < 2 || pPars->nLutsMax > 8 ) + goto usage; + break; + case 'Q': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-Q\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nLutsOver = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nLutsOver < 0 || pPars->nLutsOver > 8 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nVarsShared = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 4 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nGrowthLevel = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) + goto usage; + break; + case 's': + pPars->fSatur ^= 1; + break; + case 'z': + pPars->fZeroCost ^= 1; + break; + case 'f': + pPars->fFirst ^= 1; + break; + case 'o': + pPars->fOldAlgo ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->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; + } + if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 3 ) + { + fprintf( pErr, "The number of shared variables (%d) is not in the range 0 <= S <= 3.\n", pPars->nVarsShared ); + return 1; + } + + // modify the current network + if ( !Lpk_Resynthesize( pNtk, pPars ) ) + { + fprintf( pErr, "Resynthesis has failed.\n" ); + return 1; + } + return 0; + +usage: + fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfovwh]\n" ); + fprintf( pErr, "\t performs \"rewriting\" for LUT networks;\n" ); + fprintf( pErr, "\t determines LUT size as the max fanin count of a node;\n" ); + fprintf( pErr, "\t if the network is not LUT-mapped, packs it into 6-LUTs\n" ); + fprintf( pErr, "\t (there is another command for resynthesis after LUT mapping, \"imfs\")\n" ); + fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax ); + fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver ); + fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared ); + fprintf( pErr, "\t-L <num> : max level increase after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); + fprintf( pErr, "\t-s : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" ); + fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" ); + fprintf( pErr, "\t-f : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" ); + fprintf( pErr, "\t-o : toggle using old implementation [default = %s]\n", pPars->fOldAlgo? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); + fprintf( pErr, "\t-w : toggle detailed printout of decomposed functions [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -3078,65 +3242,52 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; - Lpk_Par_t Pars, * pPars = &Pars; + Mfs_Par_t Pars, * pPars = &Pars; int c; - + +// printf( "Implementation of this command is not finished.\n" ); +// return 1; + pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - memset( pPars, 0, sizeof(Lpk_Par_t) ); - pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure - pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC - pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars) - pPars->nGrowthLevel = 0; // (L) the maximum number of increased levels - pPars->fSatur = 1; - pPars->fZeroCost = 0; - pPars->fFirst = 0; - pPars->fOldAlgo = 0; + pPars->nWinTfoLevs = 2; + pPars->nFanoutsMax = 10; + pPars->nGrowthLevel = 0; + pPars->fArea = 0; pPars->fVerbose = 0; pPars->fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfovwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFLavwh" ) ) != EOF ) { switch ( c ) { - case 'N': - if ( globalUtilOptind >= argc ) - { - fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nLutsMax = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nLutsMax < 2 || pPars->nLutsMax > 8 ) - goto usage; - break; - case 'Q': + case 'W': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-Q\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" ); goto usage; } - pPars->nLutsOver = atoi(argv[globalUtilOptind]); + pPars->nWinTfoLevs = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nLutsOver < 0 || pPars->nLutsOver > 8 ) + if ( pPars->nWinTfoLevs < 1 || pPars->nWinTfoLevs > 99 ) goto usage; break; - case 'S': + case 'F': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - pPars->nVarsShared = atoi(argv[globalUtilOptind]); + pPars->nFanoutsMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 4 ) + if ( pPars->nFanoutsMax < 1 ) goto usage; break; case 'L': @@ -3150,17 +3301,8 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY ) goto usage; break; - case 's': - pPars->fSatur ^= 1; - break; - case 'z': - pPars->fZeroCost ^= 1; - break; - case 'f': - pPars->fFirst ^= 1; - break; - case 'o': - pPars->fOldAlgo ^= 1; + case 'a': + pPars->fArea ^= 1; break; case 'v': pPars->fVerbose ^= 1; @@ -3185,14 +3327,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "This command can only be applied to a logic network.\n" ); return 1; } - if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 3 ) - { - fprintf( pErr, "The number of shared variables (%d) is not in the range 0 <= S <= 3.\n", pPars->nVarsShared ); - return 1; - } // modify the current network - if ( !Lpk_Resynthesize( pNtk, pPars ) ) + if ( !Abc_NtkMfs( pNtk, pPars ) ) { fprintf( pErr, "Resynthesis has failed.\n" ); return 1; @@ -3200,26 +3337,18 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfovwh]\n" ); - fprintf( pErr, "\t performs \"rewriting\" for LUT networks;\n" ); - fprintf( pErr, "\t determines LUT size as the max fanin count of a node;\n" ); - fprintf( pErr, "\t if the network is not LUT-mapped, packs it into 6-LUTs\n" ); - fprintf( pErr, "\t (there is another command for resynthesis after LUT mapping, \"imfs\")\n" ); - fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax ); - fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver ); - fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared ); - fprintf( pErr, "\t-L <num> : max level increase after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); - fprintf( pErr, "\t-s : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" ); - fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" ); - fprintf( pErr, "\t-f : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" ); - fprintf( pErr, "\t-o : toggle using old implementation [default = %s]\n", pPars->fOldAlgo? "yes": "no" ); + fprintf( pErr, "usage: mfs [-W <num>] [-F <num>] [-L <num>] [-vh]\n" ); + fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" ); + fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= NM <= 100) [default = %d]\n", pPars->nWinTfoLevs ); + fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= n) [default = %d]\n", pPars->nFanoutsMax ); + fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); +// fprintf( pErr, "\t-a : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); - fprintf( pErr, "\t-w : toggle detailed printout of decomposed functions [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); +// fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } - /**Function************************************************************* Synopsis [] @@ -11552,10 +11681,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) 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 fUseImps, int fLatchCorr, int fWriteImps, 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 ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -11568,11 +11699,13 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) nMaxLevs = 0; fUseImps = 0; fRewrite = 0; + fFraiging = 0; fLatchCorr = 0; fWriteImps = 0; + fUse1Hot = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PFILirlevh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PFILirfletvh" ) ) != EOF ) { switch ( c ) { @@ -11626,12 +11759,18 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRewrite ^= 1; break; + case 'f': + fFraiging ^= 1; + break; case 'l': fLatchCorr ^= 1; break; case 'e': fWriteImps ^= 1; break; + case 't': + fUse1Hot ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -11660,8 +11799,20 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } + if ( nFramesK > 1 && fUse1Hot ) + { + printf( "Currrently can only use one-hotness for simple induction (K=1).\n" ); + return 0; + } + + if ( nFramesP && 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, fUseImps, fLatchCorr, fWriteImps, fVerbose ); + pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fFraiging, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -11672,7 +11823,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrevh]\n" ); + fprintf( pErr, "usage: ssweep [-P num] [-F num] [-I num] [-ilrfetvh]\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 ); @@ -11681,7 +11832,9 @@ usage: 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-h : print the command usage\n"); return 1; @@ -13376,7 +13529,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: bmc [-F num] [-C num] [-rvh]\n" ); fprintf( pErr, "\t perform bounded model checking\n" ); - fprintf( pErr, "\t-F num : number of time frames [default = %d]\n", nFrames ); + 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-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 1563bdfe..2a15c3a4 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -184,6 +184,11 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) ); Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); } + if ( pMan->pManExdc ) + { + pNtkNew->pManExdc = pMan->pManExdc; + pMan->pManExdc = NULL; + } if ( !Abc_NtkCheck( pNtkNew ) ) fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); return pNtkNew; @@ -1022,7 +1027,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 fUseImps, int fLatchCorr, int fWriteImps, int fVerbose ) +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 ) { Fraig_Params_t Params; Abc_Ntk_t * pNtkAig, * pNtkFraig; @@ -1034,8 +1039,10 @@ 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; -// pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 ); - pNtkFraig = Abc_NtkDup( pNtk ); + if ( fFraiging ) + pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 ); + else + pNtkFraig = Abc_NtkDup( pNtk ); if ( fVerbose ) { PRT( "Initial fraiging time", clock() - clk ); @@ -1046,7 +1053,7 @@ PRT( "Initial fraiging time", clock() - clk ); if ( pMan == NULL ) return NULL; - pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fVerbose, NULL ); + pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, nMaxImps, nMaxLevs, fRewrite, fUseImps, fLatchCorr, fWriteImps, fUse1Hot, fVerbose, NULL ); Aig_ManStop( pTemp ); if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) @@ -1530,6 +1537,28 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose return pNtkAig; } +/**Function************************************************************* + + Synopsis [Interplates two networks.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintSccs( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return; + Aig_ManComputeSccs( pMan ); + Aig_ManStop( pMan ); +} + + #include "ntl.h" diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 4003a6d6..6135d009 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -322,11 +322,11 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ) Counter2++; } } - fprintf( pFile, "%-15s: ", pNtk->pName ); - fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n", - Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] ); - fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 ); - fprintf( pFile, "Self-feed latches = %2d.\n", -1 ); //Abc_NtkCountSelfFeedLatches(pNtk) ); +// fprintf( pFile, "%-15s: ", pNtk->pName ); + fprintf( pFile, "Total latches = %5d. Init0 = %d. Init1 = %d. InitDC = %d. Const data = %d.\n", + Abc_NtkLatchNum(pNtk), InitNums[1], InitNums[2], InitNums[3], Counter0 ); +// fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 ); +// fprintf( pFile, "Self-feed latches = %2d.\n", -1 ); //Abc_NtkCountSelfFeedLatches(pNtk) ); } /**Function************************************************************* |