From d01b1a0eee0ff49d18d8235f533fbb214c61d28a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 22 Aug 2005 08:01:00 -0700 Subject: Version abc50822 --- src/base/abc/abc.c | 282 +++++++++++++++++++++++++++++++++-------------- src/base/abc/abc.h | 2 +- src/base/abc/abcAig.c | 2 +- src/base/abc/abcCut.c | 157 ++++++++++++++++++++++++++ src/base/abc/abcDfs.c | 14 ++- src/base/abc/abcFpga.c | 2 +- src/base/abc/abcFraig.c | 2 +- src/base/abc/abcMap.c | 2 +- src/base/abc/abcSeq.c | 2 +- src/base/abc/module.make | 1 + 10 files changed, 373 insertions(+), 93 deletions(-) create mode 100644 src/base/abc/abcCut.c (limited to 'src/base') diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c index dfe2f4d4..7f4ee12f 100644 --- a/src/base/abc/abc.c +++ b/src/base/abc/abc.c @@ -23,6 +23,7 @@ #include "ft.h" #include "fraig.h" #include "fxu.h" +#include "cut.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -58,6 +59,7 @@ static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSplit ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -126,6 +128,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); Cmd_CommandAdd( pAbc, "Various", "split", Abc_CommandSplit, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); + Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Abc_CommandFraigTrust, 1 ); @@ -149,6 +152,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Ft_FactorStartMan(); // Rwt_Man4ExploreStart(); +// Map_Var3Print(); +// Map_Var4Test(); } /**Function************************************************************* @@ -929,14 +934,14 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) fMulti = 0; fSimple = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "tfmcsh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "TFmcsh" ) ) != EOF ) { switch ( c ) { - case 't': + case 'T': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-t\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); goto usage; } nThresh = atoi(argv[util_optind]); @@ -944,10 +949,10 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nThresh < 0 ) goto usage; break; - case 'f': + case 'F': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-f\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } nFaninMax = atoi(argv[util_optind]); @@ -994,10 +999,10 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: renode [-t num] [-f num] [-cmsh]\n" ); + fprintf( pErr, "usage: renode [-T num] [-F num] [-cmsh]\n" ); fprintf( pErr, "\t transforms an AIG into a logic network by creating larger nodes\n" ); - fprintf( pErr, "\t-t num : the threshold for AIG node duplication [default = %d]\n", nThresh ); - fprintf( pErr, "\t-f num : the maximum fanin size after renoding [default = %d]\n", nFaninMax ); + fprintf( pErr, "\t-T num : the threshold for AIG node duplication [default = %d]\n", nThresh ); + fprintf( pErr, "\t-F num : the maximum fanin size after renoding [default = %d]\n", nFaninMax ); fprintf( pErr, "\t-c : performs renoding to derive the CNF [default = %s]\n", fCnf? "yes": "no" ); fprintf( pErr, "\t-m : creates multi-input AND graph [default = %s]\n", fMulti? "yes": "no" ); fprintf( pErr, "\t-s : creates a simple AIG (no renoding) [default = %s]\n", fSimple? "yes": "no" ); @@ -1099,14 +1104,14 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) p->fUseCompl = 1; p->fVerbose = 0; util_getopt_reset(); - while ( (c = util_getopt(argc, argv, "lnsdzcvh")) != EOF ) + while ( (c = util_getopt(argc, argv, "LNsdzcvh")) != EOF ) { switch (c) { - case 'l': + case 'L': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-l\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); goto usage; } p->nPairsMax = atoi(argv[util_optind]); @@ -1114,10 +1119,10 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( p->nPairsMax < 0 ) goto usage; break; - case 'n': + case 'N': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } p->nNodesExt = atoi(argv[util_optind]); @@ -1168,10 +1173,10 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: fx [-n num] [-l num] [-sdzcvh]\n"); + fprintf( pErr, "usage: fx [-N num] [-L num] [-sdzcvh]\n"); fprintf( pErr, "\t performs unate fast extract on the current network\n"); - fprintf( pErr, "\t-n num : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt ); - fprintf( pErr, "\t-l num : the maximum number of cube pairs to consider [default = %d]\n", p->nPairsMax ); + fprintf( pErr, "\t-N num : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt ); + fprintf( pErr, "\t-L num : the maximum number of cube pairs to consider [default = %d]\n", p->nPairsMax ); fprintf( pErr, "\t-s : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" ); fprintf( pErr, "\t-d : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" ); fprintf( pErr, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" ); @@ -1423,14 +1428,14 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) fUseDcs = 0; fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ncdvh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "NCdvh" ) ) != EOF ) { switch ( c ) { - case 'n': + case 'N': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } nNodeSizeMax = atoi(argv[util_optind]); @@ -1438,10 +1443,10 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nNodeSizeMax < 0 ) goto usage; break; - case 'c': + case 'C': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-c\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } nConeSizeMax = atoi(argv[util_optind]); @@ -1487,10 +1492,10 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: refactor [-n num] [-c num] [-dvh]\n" ); + fprintf( pErr, "usage: refactor [-N num] [-C num] [-dvh]\n" ); fprintf( pErr, "\t performs technology-independent refactoring of the AIG\n" ); - fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax ); - fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", nConeSizeMax ); + fprintf( pErr, "\t-N num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax ); + fprintf( pErr, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax ); fprintf( pErr, "\t-d : toggle use of don't-cares [default = %s]\n", fUseDcs? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -1663,14 +1668,14 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) fInitial = 0; nFrames = 5; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "fih" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "Fih" ) ) != EOF ) { switch ( c ) { - case 'f': + case 'F': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } nFrames = atoi(argv[util_optind]); @@ -1713,9 +1718,9 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: frames [-f num] [-ih]\n" ); + fprintf( pErr, "usage: frames [-F num] [-ih]\n" ); fprintf( pErr, "\t unrolls the network for a number of time frames\n" ); - fprintf( pErr, "\t-f num : the number of frames to unroll [default = %d]\n", nFrames ); + fprintf( pErr, "\t-F num : the number of frames to unroll [default = %d]\n", nFrames ); fprintf( pErr, "\t-i : toggles initializing the first frame [default = %s]\n", fInitial? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -2015,14 +2020,14 @@ int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv ) fUseAllCis = 0; Output = -1; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "oah" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "Oah" ) ) != EOF ) { switch ( c ) { - case 'o': + case 'O': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-o\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-O\" should be followed by an integer.\n" ); goto usage; } Output = atoi(argv[util_optind]); @@ -2092,11 +2097,11 @@ int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: split [-o num] [-ah] \n" ); + fprintf( pErr, "usage: split [-O num] [-ah] \n" ); fprintf( pErr, "\t replaces the current network by the logic cone of one output\n" ); fprintf( pErr, "\t-a : toggle writing all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" ); fprintf( pErr, "\t-h : print the command usage\n"); - fprintf( pErr, "\t-o num : (optional) the 0-based number of the output\n"); + fprintf( pErr, "\t-O num : (optional) the 0-based number of the output\n"); fprintf( pErr, "\tname : (optional) the name of the output\n"); return 1; } @@ -2151,6 +2156,121 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Cut_Params_t Params, * pParams = &Params; + Cut_Man_t * pCutMan; + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ); + + pNtk = Abc_FrameReadNet(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + pParams->nVarsMax = 5; // the max cut size ("k" of the k-feasible cuts) + pParams->nKeepMax = 250; // the max number of cuts kept at a node + pParams->fTruth = 1; // compute truth tables + pParams->fHash = 0; // hash cuts to detect unique + pParams->fFilter = 0; // filter dominated cuts + pParams->fSeq = 0; // compute sequential cuts + pParams->fDrop = 0; // drop cuts on the fly + pParams->fVerbose = 0; // the verbosiness flag + util_getopt_reset(); + while ( ( c = util_getopt( argc, argv, "KMtrfsdvh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + pParams->nVarsMax = atoi(argv[util_optind]); + util_optind++; + if ( pParams->nVarsMax < 0 ) + goto usage; + break; + case 'M': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pParams->nKeepMax = atoi(argv[util_optind]); + util_optind++; + if ( pParams->nKeepMax < 0 ) + goto usage; + break; + case 't': + pParams->fTruth ^= 1; + break; + case 'r': + pParams->fHash ^= 1; + break; + case 'f': + pParams->fFilter ^= 1; + break; + case 's': + pParams->fSeq ^= 1; + break; + case 'd': + pParams->fDrop ^= 1; + break; + case 'v': + pParams->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsAig(pNtk) ) + { + fprintf( pErr, "Cut computation is available only for AIGs.\n" ); + return 1; + } + pCutMan = Abc_NtkCuts( pNtk, pParams ); + Cut_ManPrintStats( pCutMan ); + Cut_ManStop( pCutMan ); + return 0; + +usage: + fprintf( pErr, "usage: cut [-K num] [-M num] [-trfsdvh]\n" ); + fprintf( pErr, "\t computes k-feasible cuts for the AIG\n" ); + fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n", pParams->nVarsMax ); + fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n", pParams->nKeepMax ); + fprintf( pErr, "\t-t : toggle truth table computation [default = %s]\n", pParams->fTruth? "yes": "no" ); + fprintf( pErr, "\t-r : toggle reduction by hashing [default = %s]\n", pParams->fHash? "yes": "no" ); + fprintf( pErr, "\t-f : toggle filtering by dominance [default = %s]\n", pParams->fFilter? "yes": "no" ); + fprintf( pErr, "\t-s : toggle sequential cut computation [default = %s]\n", pParams->fSeq? "yes": "no" ); + fprintf( pErr, "\t-d : toggle dropping when fanouts are done [default = %s]\n", pParams->fDrop? "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; +} + @@ -2168,7 +2288,7 @@ usage: int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { char Buffer[100]; - Fraig_Params_t Params; + Fraig_Params_t Params, * pParams = &Params; FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int fAllNodes; @@ -2180,17 +2300,17 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fAllNodes = 0; - Params.nPatsRand = 2048; // the number of words of random simulation info - Params.nPatsDyna = 2048; // the number of words of dynamic simulation info - Params.nBTLimit = 99; // the max number of backtracks to perform - Params.fFuncRed = 1; // performs only one level hashing - Params.fFeedBack = 1; // enables solver feedback - Params.fDist1Pats = 1; // enables distance-1 patterns - Params.fDoSparse = 0; // performs equiv tests for sparse functions - Params.fChoicing = 0; // enables recording structural choices - Params.fTryProve = 0; // tries to solve the final miter - Params.fVerbose = 0; // the verbosiness flag - Params.fVerboseP = 0; // the verbosiness flag + pParams->nPatsRand = 2048; // the number of words of random simulation info + pParams->nPatsDyna = 2048; // the number of words of dynamic simulation info + pParams->nBTLimit = 99; // the max number of backtracks to perform + pParams->fFuncRed = 1; // performs only one level hashing + pParams->fFeedBack = 1; // enables solver feedback + pParams->fDist1Pats = 1; // enables distance-1 patterns + pParams->fDoSparse = 0; // performs equiv tests for sparse functions + pParams->fChoicing = 0; // enables recording structural choices + pParams->fTryProve = 0; // tries to solve the final miter + pParams->fVerbose = 0; // the verbosiness flag + pParams->fVerboseP = 0; // the verbosiness flag util_getopt_reset(); while ( ( c = util_getopt( argc, argv, "RDBrscpvah" ) ) != EOF ) { @@ -2200,51 +2320,51 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'R': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-r\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" ); goto usage; } - Params.nPatsRand = atoi(argv[util_optind]); + pParams->nPatsRand = atoi(argv[util_optind]); util_optind++; - if ( Params.nPatsRand < 0 ) + if ( pParams->nPatsRand < 0 ) goto usage; break; case 'D': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-d\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" ); goto usage; } - Params.nPatsDyna = atoi(argv[util_optind]); + pParams->nPatsDyna = atoi(argv[util_optind]); util_optind++; - if ( Params.nPatsDyna < 0 ) + if ( pParams->nPatsDyna < 0 ) goto usage; break; case 'B': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-b\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" ); goto usage; } - Params.nBTLimit = atoi(argv[util_optind]); + pParams->nBTLimit = atoi(argv[util_optind]); util_optind++; - if ( Params.nBTLimit < 0 ) + if ( pParams->nBTLimit < 0 ) goto usage; break; case 'r': - Params.fFuncRed ^= 1; + pParams->fFuncRed ^= 1; break; case 's': - Params.fDoSparse ^= 1; + pParams->fDoSparse ^= 1; break; case 'c': - Params.fChoicing ^= 1; + pParams->fChoicing ^= 1; break; case 'p': - Params.fTryProve ^= 1; + pParams->fTryProve ^= 1; break; case 'v': - Params.fVerbose ^= 1; + pParams->fVerbose ^= 1; break; case 'a': fAllNodes ^= 1; @@ -2268,7 +2388,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) } // report the proof - Params.fVerboseP = Params.fTryProve; + pParams->fVerboseP = pParams->fTryProve; // get the new network if ( Abc_NtkIsAig(pNtk) ) @@ -2285,7 +2405,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( Params.fTryProve ) // report the result + if ( pParams->fTryProve ) // report the result Abc_NtkMiterReport( pNtkRes ); // replace the current network @@ -2293,17 +2413,17 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - sprintf( Buffer, "%d", Params.nBTLimit ); + sprintf( Buffer, "%d", pParams->nBTLimit ); fprintf( pErr, "usage: fraig [-R num] [-D num] [-B num] [-rscpvah]\n" ); fprintf( pErr, "\t transforms a logic network into a functionally reduced AIG\n" ); - fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n", Params.nPatsRand ); - fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", Params.nPatsDyna ); - fprintf( pErr, "\t-B num : number of backtracks for one SAT problem [default = %s]\n", Params.nBTLimit==-1? "infinity" : Buffer ); - fprintf( pErr, "\t-r : toggle functional reduction [default = %s]\n", Params.fFuncRed? "yes": "no" ); - fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", Params.fDoSparse? "yes": "no" ); - fprintf( pErr, "\t-c : toggle accumulation of choices [default = %s]\n", Params.fChoicing? "yes": "no" ); - fprintf( pErr, "\t-p : toggle proving the final miter [default = %s]\n", Params.fTryProve? "yes": "no" ); - fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", Params.fVerbose? "yes": "no" ); + fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsRand ); + fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna ); + fprintf( pErr, "\t-B num : number of backtracks for one SAT problem [default = %s]\n", pParams->nBTLimit==-1? "infinity" : Buffer ); + fprintf( pErr, "\t-r : toggle functional reduction [default = %s]\n", pParams->fFuncRed? "yes": "no" ); + fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", pParams->fDoSparse? "yes": "no" ); + fprintf( pErr, "\t-c : toggle accumulation of choices [default = %s]\n", pParams->fChoicing? "yes": "no" ); + fprintf( pErr, "\t-p : toggle proving the final miter [default = %s]\n", pParams->fTryProve? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" ); fprintf( pErr, "\t-a : toggle between all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "dfs" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -2657,14 +2777,14 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) fSweep = 1; fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "dasvh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "Dasvh" ) ) != EOF ) { switch ( c ) { - case 'd': + case 'D': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-d\" should be followed by a floating point number.\n" ); + fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" ); goto usage; } DelayTarget = (float)atof(argv[util_optind]); @@ -2743,9 +2863,9 @@ usage: sprintf( Buffer, "not used" ); else sprintf( Buffer, "%.3f", DelayTarget ); - fprintf( pErr, "usage: map [-d num] [-asvh]\n" ); + fprintf( pErr, "usage: map [-D num] [-asvh]\n" ); fprintf( pErr, "\t performs standard cell mapping of the current network\n" ); - fprintf( pErr, "\t-d num : sets the global required times [default = %s]\n", Buffer ); + fprintf( pErr, "\t-D num : 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-s : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); @@ -3299,14 +3419,14 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) nFrames = 3; fSat = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "fsh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "Fsh" ) ) != EOF ) { switch ( c ) { - case 'f': + case 'F': if ( util_optind >= argc ) { - fprintf( pErr, "Command line switch \"-t\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } nFrames = atoi(argv[util_optind]); @@ -3338,11 +3458,11 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: sec [-sh] [-f num] \n" ); + fprintf( pErr, "usage: sec [-sh] [-F num] \n" ); fprintf( pErr, "\t performs bounded sequential equivalence checking\n" ); fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" ); fprintf( pErr, "\t-h : print the command usage\n"); - fprintf( pErr, "\t-f num : the number of time frames to use [default = %d]\n", nFrames ); + fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames ); 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"); diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 18923f26..3bf419c5 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -426,7 +426,7 @@ extern Abc_Obj_t * Abc_NodeClone( Abc_Obj_t * pNode ); 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 ); extern Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk ); -extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll ); +extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos ); extern Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi ); extern int Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk ); extern bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 25237868..b7bcde83 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -156,7 +156,7 @@ Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew ) Abc_NtkForEachLatch( pMan->pNtkAig, pObj, i ) pObj->pCopy = Abc_NtkLatch( pManNew->pNtkAig, i ); // copy internal nodes - vNodes = Abc_AigDfs( pMan->pNtkAig, 1 ); + vNodes = Abc_AigDfs( pMan->pNtkAig, 1, 0 ); Vec_PtrForEachEntry( vNodes, pObj, i ) { if ( !Abc_NodeIsAigAnd(pObj) ) diff --git a/src/base/abc/abcCut.c b/src/base/abc/abcCut.c new file mode 100644 index 00000000..424d7561 --- /dev/null +++ b/src/base/abc/abcCut.c @@ -0,0 +1,157 @@ +/**CFile**************************************************************** + + FileName [abcCut.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Interface to cut computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "cut.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes the cuts for the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) +{ + Cut_Man_t * p; + Abc_Obj_t * pObj, * pDriver, * pNode; + Vec_Ptr_t * vNodes; + Vec_Int_t * vChoices; + int i; + int clk = clock(); + + assert( Abc_NtkIsAig(pNtk) ); + + // start the manager + pParams->nIdsMax = Abc_NtkObjNumMax( pNtk ); + p = Cut_ManStart( pParams ); + if ( pParams->fDrop ) + Cut_ManSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) ); + // set cuts for PIs + Abc_NtkForEachCi( pNtk, pObj, i ) + if ( Abc_ObjFanoutNum(pObj) > 0 ) + Cut_NodeSetTriv( p, pObj->Id ); + // compute cuts for internal nodes + vNodes = Abc_AigDfs( pNtk, 0, 1 ); + vChoices = Vec_IntAlloc( 100 ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // when we reached a CO, it is time to deallocate the cuts + if ( Abc_ObjIsCo(pObj) ) + { + if ( pParams->fDrop ) + Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) ); + continue; + } + // skip constant node, it has no cuts + if ( Abc_NodeIsConst(pObj) ) + continue; + // compute the cuts to the internal node + Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj), + Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + // add cuts due to choices + if ( Abc_NodeIsAigChoice(pObj) ) + { + Vec_IntClear( vChoices ); + for ( pNode = pObj; pNode; pNode = pNode->pData ) + Vec_IntPush( vChoices, pNode->Id ); + Cut_NodeUnionCuts( p, vChoices ); + } + } + if ( !pParams->fSeq ) + { + Vec_PtrFree( vNodes ); + Vec_IntFree( vChoices ); +PRT( "Total", clock() - clk ); + return p; + } + assert( 0 ); + + // compute sequential cuts + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + { + pDriver = Abc_ObjFanin0(pObj); + if ( !Abc_ObjIsNode(pDriver) ) + continue; + if ( Abc_NodeIsTravIdCurrent(pDriver) ) + continue; + Abc_NodeSetTravIdCurrent(pDriver); + Cut_NodeSetComputedAsNew( p, pDriver->Id ); + } + // compute as long as new cuts appear + + + return p; +} + +/**Function************************************************************* + + Synopsis [Creates the array of fanout counters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vFanNums; + Abc_Obj_t * pObj;//, * pFanout; + int i;//, k, nFanouts; + vFanNums = Vec_IntAlloc( 0 ); + Vec_IntFill( vFanNums, Abc_NtkObjNumMax(pNtk), -1 ); + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) ) + { + Vec_IntWriteEntry( vFanNums, i, Abc_ObjFanoutNum(pObj) ); +/* + // get the number of non-CO fanouts + nFanouts = 0; + Abc_ObjForEachFanout( pObj, pFanout, k ) + if ( !Abc_ObjIsCo(pFanout) ) + nFanouts++; + Vec_IntWriteEntry( vFanNums, i, nFanouts ); +*/ + } + return vFanNums; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index 40fbf799..e5f1bde9 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -141,8 +141,8 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) Synopsis [Returns the reverse DFS ordered array of logic nodes.] - Description [Collects only the internal nodes, leaving CIs and CO. - However it marks with the current TravId both CIs and COs.] + Description [Collects only the internal nodes, leaving out CIs/COs. + However it marks both CIs and COs with the current TravId.] SideEffects [] @@ -210,15 +210,15 @@ void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) Synopsis [Returns the DFS ordered array of logic nodes.] - Description [Collects only the internal nodes, leaving CIs and CO. - However it marks with the current TravId both CIs and COs.] + Description [Collects only the internal nodes, leaving out CIs/COs. + However it marks both CIs and COs with the current TravId.] SideEffects [] SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll ) +Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos ) { Vec_Ptr_t * vNodes; Abc_Obj_t * pNode; @@ -231,8 +231,10 @@ Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll ) // go through the PO nodes and call for each of them Abc_NtkForEachCo( pNtk, pNode, i ) { - Abc_NodeSetTravIdCurrent( pNode ); Abc_AigDfs_rec( Abc_ObjFanin0(pNode), vNodes ); + Abc_NodeSetTravIdCurrent( pNode ); + if ( fCollectCos ) + Vec_PtrPush( vNodes, pNode ); } // collect dangling nodes if asked to if ( fCollectAll ) diff --git a/src/base/abc/abcFpga.c b/src/base/abc/abcFpga.c index 1ced34d2..b83c376a 100644 --- a/src/base/abc/abcFpga.c +++ b/src/base/abc/abcFpga.c @@ -121,7 +121,7 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose ) pNode->pCopy = (Abc_Obj_t *)Fpga_ManReadInputs(pMan)[i]; // load the AIG into the mapper - vNodes = Abc_AigDfs( pNtk, 0 ); + vNodes = Abc_AigDfs( pNtk, 0, 0 ); pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); Vec_PtrForEachEntry( vNodes, pNode, i ) { diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c index 3f5304a7..c0eb1c0a 100644 --- a/src/base/abc/abcFraig.c +++ b/src/base/abc/abcFraig.c @@ -104,7 +104,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA pConst1 = Abc_AigConst1( pNtk->pManFunc ); // perform strashing - vNodes = Abc_AigDfs( pNtk, fAllNodes ); + vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 ); pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); Vec_PtrForEachEntry( vNodes, pNode, i ) { diff --git a/src/base/abc/abcMap.c b/src/base/abc/abcMap.c index 78f2faaa..15e5c6af 100644 --- a/src/base/abc/abcMap.c +++ b/src/base/abc/abcMap.c @@ -147,7 +147,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i pNode->pCopy = (Abc_Obj_t *)Map_ManReadInputs(pMan)[i]; // load the AIG into the mapper - vNodes = Abc_AigDfs( pNtk, 0 ); + vNodes = Abc_AigDfs( pNtk, 0, 0 ); pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); Vec_PtrForEachEntry( vNodes, pNode, i ) { diff --git a/src/base/abc/abcSeq.c b/src/base/abc/abcSeq.c index e0685bf7..2fcbf670 100644 --- a/src/base/abc/abcSeq.c +++ b/src/base/abc/abcSeq.c @@ -87,7 +87,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) } // copy internal nodes - vNodes = Abc_AigDfs( pNtk, 1 ); + vNodes = Abc_AigDfs( pNtk, 1, 0 ); Vec_PtrForEachEntry( vNodes, pObj, i ) if ( Abc_ObjFaninNum(pObj) == 2 ) pObj->pCopy = Abc_AigAnd( pManNew, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); diff --git a/src/base/abc/module.make b/src/base/abc/module.make index b05cf03b..bd390002 100644 --- a/src/base/abc/module.make +++ b/src/base/abc/module.make @@ -4,6 +4,7 @@ SRC += src/base/abc/abc.c \ src/base/abc/abcCheck.c \ src/base/abc/abcCollapse.c \ src/base/abc/abcCreate.c \ + src/base/abc/abcCut.c \ src/base/abc/abcDfs.c \ src/base/abc/abcDsd.c \ src/base/abc/abcFanio.c \ -- cgit v1.2.3