diff options
Diffstat (limited to 'src')
34 files changed, 3919 insertions, 139 deletions
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] <name>\n" ); + fprintf( pErr, "usage: split [-O num] [-ah] <name>\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] <file1> <file2>\n" ); + fprintf( pErr, "usage: sec [-sh] [-F num] <file1> <file2>\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 \ diff --git a/src/map/mapper/mapperCanon.c b/src/map/mapper/mapperCanon.c index 4937fd0e..2b0f261f 100644 --- a/src/map/mapper/mapperCanon.c +++ b/src/map/mapper/mapperCanon.c @@ -170,13 +170,26 @@ void Map_CanonComputePhase6( unsigned uTruths[][2], int nVars, unsigned uTruth[] int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char * puPhases, unsigned uTruthRes[] ) { unsigned uTruth0, uTruth1; - unsigned uCanon0, uCanon1, uCanonBest; + unsigned uCanon0, uCanon1, uCanonBest, uPhaseBest; int i, Limit; - if ( nVarsMax != 5 || nVarsReal < 5 ) + if ( nVarsMax == 6 ) return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes ); + if ( nVarsReal < 5 ) + { +// return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes ); + + uTruth0 = uTruth[0] & 0xFFFF; + assert( p->pCounters[uTruth0] > 0 ); + uTruthRes[0] = (p->uCanons[uTruth0] << 16) | p->uCanons[uTruth0]; + uTruthRes[1] = uTruthRes[0]; + puPhases[0] = p->uPhases[uTruth0][0]; + return 1; + } + assert( nVarsMax == 5 ); + assert( nVarsReal == 5 ); uTruth0 = uTruth[0] & 0xFFFF; uTruth1 = (uTruth[0] >> 16); if ( uTruth1 == 0 ) @@ -202,7 +215,7 @@ int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned u } uCanon0 = p->uCanons[uTruth0]; uCanon1 = p->uCanons[uTruth1]; - if ( uCanon0 && uCanon1 && uCanon0 > uCanon1 ) // using nCanon1 as the main one + if ( uCanon0 >= uCanon1 ) // using nCanon1 as the main one { assert( p->pCounters[uTruth1] > 0 ); uCanonBest = 0xFFFF; @@ -210,16 +223,17 @@ int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned u { uCanon0 = Extra_TruthPolarize( uTruth0, p->uPhases[uTruth1][i], 4 ); if ( uCanonBest > uCanon0 ) + { uCanonBest = uCanon0; + uPhaseBest = p->uPhases[uTruth1][i]; + } } uTruthRes[0] = (uCanon1 << 16) | uCanonBest; uTruthRes[1] = uTruthRes[0]; - Limit = (p->pCounters[uTruth1] > 4)? 4 : p->pCounters[uTruth1]; - for ( i = 0; i < Limit; i++ ) - puPhases[i] = p->uPhases[uTruth1][i]; - return Limit; + puPhases[0] = uPhaseBest; + return 1; } - else if ( uCanon0 && uCanon1 && uCanon0 < uCanon1 ) + else if ( uCanon0 < uCanon1 ) { assert( p->pCounters[uTruth0] > 0 ); uCanonBest = 0xFFFF; @@ -227,22 +241,27 @@ int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned u { uCanon1 = Extra_TruthPolarize( uTruth1, p->uPhases[uTruth0][i], 4 ); if ( uCanonBest > uCanon1 ) + { uCanonBest = uCanon1; + uPhaseBest = p->uPhases[uTruth0][i]; + } } uTruthRes[0] = (uCanon0 << 16) | uCanonBest; uTruthRes[1] = uTruthRes[0]; - Limit = (p->pCounters[uTruth0] > 4)? 4 : p->pCounters[uTruth0]; - for ( i = 0; i < Limit; i++ ) - { - puPhases[i] = p->uPhases[uTruth0][i]; - puPhases[i] |= (1 << 4); - } - return Limit; + puPhases[0] = uPhaseBest | (1 << 4); + return 1; } else + { + assert( 0 ); return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes ); + } } + + + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/mapper/mapperCore.c b/src/map/mapper/mapperCore.c index 16cbfd5c..a43bcdc1 100644 --- a/src/map/mapper/mapperCore.c +++ b/src/map/mapper/mapperCore.c @@ -69,7 +69,7 @@ int Map_Mapping( Map_Man_t * p ) Map_MappingTruths( p ); p->timeTruth = clock() - clk; ////////////////////////////////////////////////////////////////////// -//PRT( "Truths", clock() - clk ); +PRT( "Truths", clock() - clk ); ////////////////////////////////////////////////////////////////////// // compute the minimum-delay mapping diff --git a/src/map/mapper/mapperCreate.c b/src/map/mapper/mapperCreate.c index dc056f34..738d099c 100644 --- a/src/map/mapper/mapperCreate.c +++ b/src/map/mapper/mapperCreate.c @@ -197,7 +197,7 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose ) assert( p->nVarsMax > 0 ); if ( p->nVarsMax == 5 ) - Extra_Truth4VarN( &p->uCanons, &p->uPhases, &p->pCounters, 16 ); + Extra_Truth4VarN( &p->uCanons, &p->uPhases, &p->pCounters, 8 ); // start various data structures Map_TableCreate( p ); diff --git a/src/map/mapper/mapperCut.c b/src/map/mapper/mapperCut.c index 0c3a0910..b5ce4018 100644 --- a/src/map/mapper/mapperCut.c +++ b/src/map/mapper/mapperCut.c @@ -692,6 +692,7 @@ int Map_MappingCountAllCuts( Map_Man_t * pMan ) Map_Cut_t * pCut; int i, nCuts; // int nCuts55 = 0, nCuts5x = 0, nCuts4x = 0, nCuts3x = 0; +// int pCounts[7] = {0}; nCuts = 0; for ( i = 0; i < pMan->nBins; i++ ) for ( pNode = pMan->pBins[i]; pNode; pNode = pNode->pNext ) @@ -708,9 +709,14 @@ int Map_MappingCountAllCuts( Map_Man_t * pMan ) nCuts4x++; else if ( Map_CutRegular(pCut->pOne)->nLeaves == 3 || Map_CutRegular(pCut->pTwo)->nLeaves == 3 ) nCuts3x++; -*/ +*/ +// pCounts[ Map_CutRegular(pCut->pOne)->nLeaves ]++; +// pCounts[ Map_CutRegular(pCut->pTwo)->nLeaves ]++; } // printf( "Total cuts = %6d. 55 = %6d. 5x = %6d. 4x = %6d. 3x = %6d.\n", nCuts, nCuts55, nCuts5x, nCuts4x, nCuts3x ); + +// printf( "Total cuts = %6d. 6= %6d. 5= %6d. 4= %6d. 3= %6d. 2= %6d. 1= %6d.\n", +// nCuts, pCounts[6], pCounts[5], pCounts[4], pCounts[3], pCounts[2], pCounts[1] ); return nCuts; } diff --git a/src/map/mapper/mapperTruth.c b/src/map/mapper/mapperTruth.c index 54fc0391..7eabf4df 100644 --- a/src/map/mapper/mapperTruth.c +++ b/src/map/mapper/mapperTruth.c @@ -93,8 +93,13 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut ) // unsigned uCanon1, uCanon2; unsigned uTruth[2], uCanon[2]; unsigned char uPhases[16]; - int fUseFast = 1; + unsigned * uCanon2; + char * pPhases2; + int fUseFast = 0; + int fUseRec = 1; + extern int Map_CanonCompute( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes ); + // generally speaking, 1-input cut can be matched into a wire! if ( pCut->nLeaves == 1 ) return; @@ -112,6 +117,21 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut ) // compute the canonical form for the positive phase if ( fUseFast ) Map_CanonComputeFast( p, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon ); + else if ( fUseRec ) + { +// Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon ); + Extra_TruthCanonFastN( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 ); +/* + if ( uCanon[0] != uCanon2[0] || uPhases[0] != pPhases2[0] ) + { + int k = 0; + Map_CanonCompute( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 ); + } +*/ + uCanon[0] = uCanon2[0]; + uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0]; + uPhases[0] = pPhases2[0]; + } else Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon ); pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon ); @@ -125,6 +145,21 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut ) uTruth[1] = ~uTruth[1]; if ( fUseFast ) Map_CanonComputeFast( p, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon ); + else if ( fUseRec ) + { +// Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon ); + Extra_TruthCanonFastN( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 ); +/* + if ( uCanon[0] != uCanon2[0] || uPhases[0] != pPhases2[0] ) + { + int k = 0; + Map_CanonCompute( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 ); + } +*/ + uCanon[0] = uCanon2[0]; + uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0]; + uPhases[0] = pPhases2[0]; + } else Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon ); pCut->M[0].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon ); @@ -243,6 +278,25 @@ void Map_CutsCollect_rec( Map_Cut_t * pCut, Map_NodeVec_t * vVisited ) Map_NodeVecPush( vVisited, (Map_Node_t *)pCut ); } +/* + { + unsigned * uCanon2; + char * pPhases2; + + Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon ); + Map_CanonCompute( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 ); + if ( uCanon2[0] != uCanon[0] ) + { + int v = 0; + Map_CanonCompute( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 ); + Map_CanonComputeFast( p, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon ); + } +// else +// { +// printf( "Correct.\n" ); +// } + } +*/ //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h index 92e631ad..d298a204 100644 --- a/src/misc/extra/extra.h +++ b/src/misc/extra/extra.h @@ -216,6 +216,10 @@ extern unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars ); extern void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap ); extern void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int nPhasesMax ); /* permutation mapping */ +extern unsigned short Extra_TruthPerm4One( unsigned uTruth, int Phase ); +extern unsigned Extra_TruthPerm5One( unsigned uTruth, int Phase ); +extern void Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes ); +/* precomputing tables for permutation mapping */ extern void ** Extra_ArrayAlloc( int nCols, int nRows, int Size ); extern unsigned short ** Extra_TruthPerm43(); extern unsigned ** Extra_TruthPerm53(); @@ -223,6 +227,11 @@ extern unsigned ** Extra_TruthPerm54(); /* for independence from CUDD */ extern unsigned int Cudd_PrimeCopy( unsigned int p ); +/*=== extraUtilCanon.c ========================================================*/ + +/* fast computation of N-canoninical form up to 6 inputs */ +extern int Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes ); + /*=== extraUtilProgress.c ================================================================*/ typedef struct ProgressBarStruct ProgressBar; diff --git a/src/misc/extra/extraUtilCanon.c b/src/misc/extra/extraUtilCanon.c new file mode 100644 index 00000000..9d4e5b5d --- /dev/null +++ b/src/misc/extra/extraUtilCanon.c @@ -0,0 +1,699 @@ +/**CFile**************************************************************** + + FileName [extraUtilMisc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [extra] + + Synopsis [Computing canonical forms of Boolean functions using truth tables.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: extraUtilMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "extra.h" + +/*---------------------------------------------------------------------------*/ +/* Constant declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Stucture declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Type declarations */ +/*---------------------------------------------------------------------------*/ + +/*---------------------------------------------------------------------------*/ +/* Variable declarations */ +/*---------------------------------------------------------------------------*/ + +static unsigned s_Truths3[256]; +static char s_Phases3[256][9]; + +/*---------------------------------------------------------------------------*/ +/* Macro declarations */ +/*---------------------------------------------------------------------------*/ + + +/**AutomaticStart*************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Static function prototypes */ +/*---------------------------------------------------------------------------*/ + +static int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, char ** ppfRes, int Flag ); + +/**AutomaticEnd***************************************************************/ + +/*---------------------------------------------------------------------------*/ +/* Definition of exported functions */ +/*---------------------------------------------------------------------------*/ + +/**Function******************************************************************** + + Synopsis [Computes the N-canonical form of the Boolean function up to 6 inputs.] + + Description [The N-canonical form is defined as the truth table with + the minimum integer value. This function exhaustively enumerates + through the complete set of 2^N phase assignments. + Returns pointers to the static storage to the truth table and phases. + This data should be used before the function is called again.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes ) +{ + static unsigned uTruthStore6[2]; + int RetValue; + assert( nVarsMax <= 6 ); + assert( nVarsReal <= nVarsMax ); + RetValue = Extra_TruthCanonN_rec( nVarsReal <= 3? 3: nVarsReal, (unsigned char *)pt, pptRes, ppfRes, 0 ); + if ( nVarsMax == 6 && nVarsReal < nVarsMax ) + { + uTruthStore6[0] = **pptRes; + uTruthStore6[1] = **pptRes; + *pptRes = uTruthStore6; + } + return RetValue; +} + +/*---------------------------------------------------------------------------*/ +/* Definition of internal functions */ +/*---------------------------------------------------------------------------*/ + +/**Function************************************************************* + + Synopsis [Recursive implementation of the above.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, char ** ppfRes, int Flag ) +{ + static unsigned uTruthStore[7][2][2]; + static char uPhaseStore[7][2][64]; + + unsigned char * pt0, * pt1; + unsigned * ptRes0, * ptRes1, * ptRes; + unsigned uInit0, uInit1, uTruth0, uTruth1, uTemp; + char * pfRes0, * pfRes1, * pfRes; + int nf0, nf1, nfRes, i, nVarsN; + + // table lookup for three vars + if ( nVars == 3 ) + { + *pptRes = &s_Truths3[*pt]; + *ppfRes = s_Phases3[*pt]+1; + return s_Phases3[*pt][0]; + } + + // number of vars for the next call + nVarsN = nVars-1; + // truth table for the next call + pt0 = pt; + pt1 = pt + (1 << nVarsN) / 8; + // 5-var truth tables for this call + uInit0 = *((unsigned *)pt0); + uInit1 = *((unsigned *)pt1); + if ( nVarsN == 3 ) + { + uInit0 &= 0xFF; + uInit1 &= 0xFF; + uInit0 = (uInit0 << 24) | (uInit0 << 16) | (uInit0 << 8) | uInit0; + uInit1 = (uInit1 << 24) | (uInit1 << 16) | (uInit1 << 8) | uInit1; + } + else if ( nVarsN == 4 ) + { + uInit0 &= 0xFFFF; + uInit1 &= 0xFFFF; + uInit0 = (uInit0 << 16) | uInit0; + uInit1 = (uInit1 << 16) | uInit1; + } + + // storage for truth tables and phases + ptRes = uTruthStore[nVars][Flag]; + pfRes = uPhaseStore[nVars][Flag]; + + // solve trivial cases + if ( uInit1 == 0 ) + { + nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 ); + uTruth1 = uInit1; + uTruth0 = *ptRes0; + nfRes = 0; + for ( i = 0; i < nf0; i++ ) + pfRes[nfRes++] = pfRes0[i]; + goto finish; + } + if ( uInit0 == 0 ) + { + nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 ); + uTruth1 = uInit0; + uTruth0 = *ptRes1; + nfRes = 0; + for ( i = 0; i < nf1; i++ ) + pfRes[nfRes++] = pfRes1[i] | (1<<nVarsN); + goto finish; + } + + if ( uInit1 == 0xFFFFFFFF ) + { + nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 ); + uTruth1 = *ptRes0; + uTruth0 = uInit1; + nfRes = 0; + for ( i = 0; i < nf0; i++ ) + pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN); + goto finish; + } + if ( uInit0 == 0xFFFFFFFF ) + { + nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 ); + uTruth1 = *ptRes1; + uTruth0 = uInit0; + nfRes = 0; + for ( i = 0; i < nf1; i++ ) + pfRes[nfRes++] = pfRes1[i]; + goto finish; + } + + // solve the problem for cofactors + nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 ); + nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 ); + + // combine the result + if ( *ptRes1 < *ptRes0 ) + { + uTruth0 = 0xFFFFFFFF; + nfRes = 0; + for ( i = 0; i < nf1; i++ ) + { + uTemp = Extra_TruthPolarize( uInit0, pfRes1[i], nVarsN ); + if ( uTruth0 > uTemp ) + { + nfRes = 0; + uTruth0 = uTemp; + pfRes[nfRes++] = pfRes1[i]; + } + else if ( uTruth0 == uTemp ) + pfRes[nfRes++] = pfRes1[i]; + } + uTruth1 = *ptRes1; + } + else if ( *ptRes1 > *ptRes0 ) + { + uTruth0 = 0xFFFFFFFF; + nfRes = 0; + for ( i = 0; i < nf0; i++ ) + { + uTemp = Extra_TruthPolarize( uInit1, pfRes0[i], nVarsN ); + if ( uTruth0 > uTemp ) + { + nfRes = 0; + uTruth0 = uTemp; + pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN); + } + else if ( uTruth0 == uTemp ) + pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN); + } + uTruth1 = *ptRes0; + } + else + { + assert( nf0 == nf1 ); + nfRes = 0; + for ( i = 0; i < nf1; i++ ) + pfRes[nfRes++] = pfRes1[i]; + for ( i = 0; i < nf0; i++ ) + pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN); + uTruth0 = Extra_TruthPolarize( uInit0, pfRes1[0], nVarsN ); + uTruth1 = *ptRes0; + } + +finish : + if ( nVarsN == 3 ) + { + uTruth0 &= 0xFF; + uTruth1 &= 0xFF; + uTemp = (uTruth1 << 8) | uTruth0; + *ptRes = (uTemp << 16) | uTemp; + } + else if ( nVarsN == 4 ) + { + uTruth0 &= 0xFFFF; + uTruth1 &= 0xFFFF; + *ptRes = (uTruth1 << 16) | uTruth0; + } + else if ( nVarsN == 5 ) + { + *(ptRes+0) = uTruth0; + *(ptRes+1) = uTruth1; + } + + *pptRes = ptRes; + *ppfRes = pfRes; + return nfRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Map_Var3Print() +{ + extern void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters ); + + unsigned * uCanons; + char ** uPhases; + char * pCounters; + int i, k; + + Extra_Truth3VarN( &uCanons, &uPhases, &pCounters ); + + for ( i = 0; i < 256; i++ ) + { + if ( i % 8 == 0 ) + printf( "\n" ); + Extra_PrintHex( stdout, uCanons[i], 5 ); + printf( ", " ); + } + printf( "\n" ); + + for ( i = 0; i < 256; i++ ) + { + printf( "%3d */ { %2d, ", i, pCounters[i] ); + for ( k = 0; k < pCounters[i]; k++ ) + printf( "%s%d", k? ", ":"", uPhases[i][k] ); + printf( " }\n" ); + } + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Map_Var3Test() +{ + extern void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters ); + + unsigned * uCanons; + char ** uPhases; + char * pCounters; + int i; + unsigned * ptRes; + char * pfRes; + unsigned uTruth; + int Count; + + Extra_Truth3VarN( &uCanons, &uPhases, &pCounters ); + + for ( i = 0; i < 256; i++ ) + { + uTruth = i; + Count = Extra_TruthCanonFastN( 5, 3, &uTruth, &ptRes, &pfRes ); + if ( *ptRes != uCanons[i] || Count != pCounters[i] ) + { + int k = 0; + } + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Map_Var4Test() +{ + extern void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int PhaseMax ); + + unsigned short * uCanons; + char ** uPhases; + char * pCounters; + int i, k; + unsigned * ptRes; + char * pfRes; + unsigned uTruth; + int Count; + + Extra_Truth4VarN( &uCanons, &uPhases, &pCounters, 16 ); + + for ( i = 0; i < 256*256; i++ ) + { + uTruth = i; + Count = Extra_TruthCanonFastN( 5, 4, &uTruth, &ptRes, &pfRes ); + if ( (*ptRes & 0xFFFF) != uCanons[i] || Count != pCounters[i] ) + { + int k = 0; + } + for ( k = 0; k < Count; k++ ) + if ( uPhases[i][k] != pfRes[k] ) + { + int v = 0; + } + } +} + +/*---------------------------------------------------------------------------*/ +/* Definition of static Functions */ +/*---------------------------------------------------------------------------*/ + +static unsigned s_Truths3[256] = +{ + 0x00000000, 0x01010101, 0x01010101, 0x03030303, 0x01010101, 0x05050505, 0x06060606, 0x07070707, + 0x01010101, 0x06060606, 0x05050505, 0x07070707, 0x03030303, 0x07070707, 0x07070707, 0x0f0f0f0f, + 0x01010101, 0x11111111, 0x12121212, 0x13131313, 0x14141414, 0x15151515, 0x16161616, 0x17171717, + 0x18181818, 0x19191919, 0x1a1a1a1a, 0x1b1b1b1b, 0x1c1c1c1c, 0x1d1d1d1d, 0x1e1e1e1e, 0x1f1f1f1f, + 0x01010101, 0x12121212, 0x11111111, 0x13131313, 0x18181818, 0x1a1a1a1a, 0x19191919, 0x1b1b1b1b, + 0x14141414, 0x16161616, 0x15151515, 0x17171717, 0x1c1c1c1c, 0x1e1e1e1e, 0x1d1d1d1d, 0x1f1f1f1f, + 0x03030303, 0x13131313, 0x13131313, 0x33333333, 0x1c1c1c1c, 0x35353535, 0x36363636, 0x37373737, + 0x1c1c1c1c, 0x36363636, 0x35353535, 0x37373737, 0x3c3c3c3c, 0x3d3d3d3d, 0x3d3d3d3d, 0x3f3f3f3f, + 0x01010101, 0x14141414, 0x18181818, 0x1c1c1c1c, 0x11111111, 0x15151515, 0x19191919, 0x1d1d1d1d, + 0x12121212, 0x16161616, 0x1a1a1a1a, 0x1e1e1e1e, 0x13131313, 0x17171717, 0x1b1b1b1b, 0x1f1f1f1f, + 0x05050505, 0x15151515, 0x1a1a1a1a, 0x35353535, 0x15151515, 0x55555555, 0x56565656, 0x57575757, + 0x1a1a1a1a, 0x56565656, 0x5a5a5a5a, 0x5b5b5b5b, 0x35353535, 0x57575757, 0x5b5b5b5b, 0x5f5f5f5f, + 0x06060606, 0x16161616, 0x19191919, 0x36363636, 0x19191919, 0x56565656, 0x66666666, 0x67676767, + 0x16161616, 0x69696969, 0x56565656, 0x6b6b6b6b, 0x36363636, 0x6b6b6b6b, 0x67676767, 0x6f6f6f6f, + 0x07070707, 0x17171717, 0x1b1b1b1b, 0x37373737, 0x1d1d1d1d, 0x57575757, 0x67676767, 0x77777777, + 0x1e1e1e1e, 0x6b6b6b6b, 0x5b5b5b5b, 0x7b7b7b7b, 0x3d3d3d3d, 0x7d7d7d7d, 0x7e7e7e7e, 0x7f7f7f7f, + 0x01010101, 0x18181818, 0x14141414, 0x1c1c1c1c, 0x12121212, 0x1a1a1a1a, 0x16161616, 0x1e1e1e1e, + 0x11111111, 0x19191919, 0x15151515, 0x1d1d1d1d, 0x13131313, 0x1b1b1b1b, 0x17171717, 0x1f1f1f1f, + 0x06060606, 0x19191919, 0x16161616, 0x36363636, 0x16161616, 0x56565656, 0x69696969, 0x6b6b6b6b, + 0x19191919, 0x66666666, 0x56565656, 0x67676767, 0x36363636, 0x67676767, 0x6b6b6b6b, 0x6f6f6f6f, + 0x05050505, 0x1a1a1a1a, 0x15151515, 0x35353535, 0x1a1a1a1a, 0x5a5a5a5a, 0x56565656, 0x5b5b5b5b, + 0x15151515, 0x56565656, 0x55555555, 0x57575757, 0x35353535, 0x5b5b5b5b, 0x57575757, 0x5f5f5f5f, + 0x07070707, 0x1b1b1b1b, 0x17171717, 0x37373737, 0x1e1e1e1e, 0x5b5b5b5b, 0x6b6b6b6b, 0x7b7b7b7b, + 0x1d1d1d1d, 0x67676767, 0x57575757, 0x77777777, 0x3d3d3d3d, 0x7e7e7e7e, 0x7d7d7d7d, 0x7f7f7f7f, + 0x03030303, 0x1c1c1c1c, 0x1c1c1c1c, 0x3c3c3c3c, 0x13131313, 0x35353535, 0x36363636, 0x3d3d3d3d, + 0x13131313, 0x36363636, 0x35353535, 0x3d3d3d3d, 0x33333333, 0x37373737, 0x37373737, 0x3f3f3f3f, + 0x07070707, 0x1d1d1d1d, 0x1e1e1e1e, 0x3d3d3d3d, 0x17171717, 0x57575757, 0x6b6b6b6b, 0x7d7d7d7d, + 0x1b1b1b1b, 0x67676767, 0x5b5b5b5b, 0x7e7e7e7e, 0x37373737, 0x77777777, 0x7b7b7b7b, 0x7f7f7f7f, + 0x07070707, 0x1e1e1e1e, 0x1d1d1d1d, 0x3d3d3d3d, 0x1b1b1b1b, 0x5b5b5b5b, 0x67676767, 0x7e7e7e7e, + 0x17171717, 0x6b6b6b6b, 0x57575757, 0x7d7d7d7d, 0x37373737, 0x7b7b7b7b, 0x77777777, 0x7f7f7f7f, + 0x0f0f0f0f, 0x1f1f1f1f, 0x1f1f1f1f, 0x3f3f3f3f, 0x1f1f1f1f, 0x5f5f5f5f, 0x6f6f6f6f, 0x7f7f7f7f, + 0x1f1f1f1f, 0x6f6f6f6f, 0x5f5f5f5f, 0x7f7f7f7f, 0x3f3f3f3f, 0x7f7f7f7f, 0x7f7f7f7f, 0xffffffff +}; + +static char s_Phases3[256][9] = +{ +/* 0 */ { 8, 0, 1, 2, 3, 4, 5, 6, 7 }, +/* 1 */ { 1, 0 }, +/* 2 */ { 1, 1 }, +/* 3 */ { 2, 0, 1 }, +/* 4 */ { 1, 2 }, +/* 5 */ { 2, 0, 2 }, +/* 6 */ { 2, 0, 3 }, +/* 7 */ { 1, 0 }, +/* 8 */ { 1, 3 }, +/* 9 */ { 2, 1, 2 }, +/* 10 */ { 2, 1, 3 }, +/* 11 */ { 1, 1 }, +/* 12 */ { 2, 2, 3 }, +/* 13 */ { 1, 2 }, +/* 14 */ { 1, 3 }, +/* 15 */ { 4, 0, 1, 2, 3 }, +/* 16 */ { 1, 4 }, +/* 17 */ { 2, 0, 4 }, +/* 18 */ { 2, 0, 5 }, +/* 19 */ { 1, 0 }, +/* 20 */ { 2, 0, 6 }, +/* 21 */ { 1, 0 }, +/* 22 */ { 1, 0 }, +/* 23 */ { 1, 0 }, +/* 24 */ { 2, 0, 7 }, +/* 25 */ { 1, 0 }, +/* 26 */ { 1, 0 }, +/* 27 */ { 1, 0 }, +/* 28 */ { 1, 0 }, +/* 29 */ { 1, 0 }, +/* 30 */ { 1, 0 }, +/* 31 */ { 1, 0 }, +/* 32 */ { 1, 5 }, +/* 33 */ { 2, 1, 4 }, +/* 34 */ { 2, 1, 5 }, +/* 35 */ { 1, 1 }, +/* 36 */ { 2, 1, 6 }, +/* 37 */ { 1, 1 }, +/* 38 */ { 1, 1 }, +/* 39 */ { 1, 1 }, +/* 40 */ { 2, 1, 7 }, +/* 41 */ { 1, 1 }, +/* 42 */ { 1, 1 }, +/* 43 */ { 1, 1 }, +/* 44 */ { 1, 1 }, +/* 45 */ { 1, 1 }, +/* 46 */ { 1, 1 }, +/* 47 */ { 1, 1 }, +/* 48 */ { 2, 4, 5 }, +/* 49 */ { 1, 4 }, +/* 50 */ { 1, 5 }, +/* 51 */ { 4, 0, 1, 4, 5 }, +/* 52 */ { 1, 6 }, +/* 53 */ { 1, 0 }, +/* 54 */ { 1, 0 }, +/* 55 */ { 1, 0 }, +/* 56 */ { 1, 7 }, +/* 57 */ { 1, 1 }, +/* 58 */ { 1, 1 }, +/* 59 */ { 1, 1 }, +/* 60 */ { 4, 0, 1, 6, 7 }, +/* 61 */ { 1, 0 }, +/* 62 */ { 1, 1 }, +/* 63 */ { 2, 0, 1 }, +/* 64 */ { 1, 6 }, +/* 65 */ { 2, 2, 4 }, +/* 66 */ { 2, 2, 5 }, +/* 67 */ { 1, 2 }, +/* 68 */ { 2, 2, 6 }, +/* 69 */ { 1, 2 }, +/* 70 */ { 1, 2 }, +/* 71 */ { 1, 2 }, +/* 72 */ { 2, 2, 7 }, +/* 73 */ { 1, 2 }, +/* 74 */ { 1, 2 }, +/* 75 */ { 1, 2 }, +/* 76 */ { 1, 2 }, +/* 77 */ { 1, 2 }, +/* 78 */ { 1, 2 }, +/* 79 */ { 1, 2 }, +/* 80 */ { 2, 4, 6 }, +/* 81 */ { 1, 4 }, +/* 82 */ { 1, 5 }, +/* 83 */ { 1, 4 }, +/* 84 */ { 1, 6 }, +/* 85 */ { 4, 0, 2, 4, 6 }, +/* 86 */ { 1, 0 }, +/* 87 */ { 1, 0 }, +/* 88 */ { 1, 7 }, +/* 89 */ { 1, 2 }, +/* 90 */ { 4, 0, 2, 5, 7 }, +/* 91 */ { 1, 0 }, +/* 92 */ { 1, 6 }, +/* 93 */ { 1, 2 }, +/* 94 */ { 1, 2 }, +/* 95 */ { 2, 0, 2 }, +/* 96 */ { 2, 4, 7 }, +/* 97 */ { 1, 4 }, +/* 98 */ { 1, 5 }, +/* 99 */ { 1, 4 }, +/* 100 */ { 1, 6 }, +/* 101 */ { 1, 4 }, +/* 102 */ { 4, 0, 3, 4, 7 }, +/* 103 */ { 1, 0 }, +/* 104 */ { 1, 7 }, +/* 105 */ { 4, 0, 3, 5, 6 }, +/* 106 */ { 1, 7 }, +/* 107 */ { 1, 0 }, +/* 108 */ { 1, 7 }, +/* 109 */ { 1, 3 }, +/* 110 */ { 1, 3 }, +/* 111 */ { 2, 0, 3 }, +/* 112 */ { 1, 4 }, +/* 113 */ { 1, 4 }, +/* 114 */ { 1, 5 }, +/* 115 */ { 1, 4 }, +/* 116 */ { 1, 6 }, +/* 117 */ { 1, 4 }, +/* 118 */ { 1, 4 }, +/* 119 */ { 2, 0, 4 }, +/* 120 */ { 1, 7 }, +/* 121 */ { 1, 5 }, +/* 122 */ { 1, 5 }, +/* 123 */ { 2, 0, 5 }, +/* 124 */ { 1, 6 }, +/* 125 */ { 2, 0, 6 }, +/* 126 */ { 2, 0, 7 }, +/* 127 */ { 1, 0 }, +/* 128 */ { 1, 7 }, +/* 129 */ { 2, 3, 4 }, +/* 130 */ { 2, 3, 5 }, +/* 131 */ { 1, 3 }, +/* 132 */ { 2, 3, 6 }, +/* 133 */ { 1, 3 }, +/* 134 */ { 1, 3 }, +/* 135 */ { 1, 3 }, +/* 136 */ { 2, 3, 7 }, +/* 137 */ { 1, 3 }, +/* 138 */ { 1, 3 }, +/* 139 */ { 1, 3 }, +/* 140 */ { 1, 3 }, +/* 141 */ { 1, 3 }, +/* 142 */ { 1, 3 }, +/* 143 */ { 1, 3 }, +/* 144 */ { 2, 5, 6 }, +/* 145 */ { 1, 4 }, +/* 146 */ { 1, 5 }, +/* 147 */ { 1, 5 }, +/* 148 */ { 1, 6 }, +/* 149 */ { 1, 6 }, +/* 150 */ { 4, 1, 2, 4, 7 }, +/* 151 */ { 1, 1 }, +/* 152 */ { 1, 7 }, +/* 153 */ { 4, 1, 2, 5, 6 }, +/* 154 */ { 1, 5 }, +/* 155 */ { 1, 1 }, +/* 156 */ { 1, 6 }, +/* 157 */ { 1, 2 }, +/* 158 */ { 1, 2 }, +/* 159 */ { 2, 1, 2 }, +/* 160 */ { 2, 5, 7 }, +/* 161 */ { 1, 4 }, +/* 162 */ { 1, 5 }, +/* 163 */ { 1, 5 }, +/* 164 */ { 1, 6 }, +/* 165 */ { 4, 1, 3, 4, 6 }, +/* 166 */ { 1, 3 }, +/* 167 */ { 1, 1 }, +/* 168 */ { 1, 7 }, +/* 169 */ { 1, 1 }, +/* 170 */ { 4, 1, 3, 5, 7 }, +/* 171 */ { 1, 1 }, +/* 172 */ { 1, 7 }, +/* 173 */ { 1, 3 }, +/* 174 */ { 1, 3 }, +/* 175 */ { 2, 1, 3 }, +/* 176 */ { 1, 5 }, +/* 177 */ { 1, 4 }, +/* 178 */ { 1, 5 }, +/* 179 */ { 1, 5 }, +/* 180 */ { 1, 6 }, +/* 181 */ { 1, 4 }, +/* 182 */ { 1, 4 }, +/* 183 */ { 2, 1, 4 }, +/* 184 */ { 1, 7 }, +/* 185 */ { 1, 5 }, +/* 186 */ { 1, 5 }, +/* 187 */ { 2, 1, 5 }, +/* 188 */ { 1, 7 }, +/* 189 */ { 2, 1, 6 }, +/* 190 */ { 2, 1, 7 }, +/* 191 */ { 1, 1 }, +/* 192 */ { 2, 6, 7 }, +/* 193 */ { 1, 4 }, +/* 194 */ { 1, 5 }, +/* 195 */ { 4, 2, 3, 4, 5 }, +/* 196 */ { 1, 6 }, +/* 197 */ { 1, 2 }, +/* 198 */ { 1, 3 }, +/* 199 */ { 1, 2 }, +/* 200 */ { 1, 7 }, +/* 201 */ { 1, 2 }, +/* 202 */ { 1, 3 }, +/* 203 */ { 1, 3 }, +/* 204 */ { 4, 2, 3, 6, 7 }, +/* 205 */ { 1, 2 }, +/* 206 */ { 1, 3 }, +/* 207 */ { 2, 2, 3 }, +/* 208 */ { 1, 6 }, +/* 209 */ { 1, 4 }, +/* 210 */ { 1, 5 }, +/* 211 */ { 1, 4 }, +/* 212 */ { 1, 6 }, +/* 213 */ { 1, 6 }, +/* 214 */ { 1, 7 }, +/* 215 */ { 2, 2, 4 }, +/* 216 */ { 1, 7 }, +/* 217 */ { 1, 6 }, +/* 218 */ { 1, 7 }, +/* 219 */ { 2, 2, 5 }, +/* 220 */ { 1, 6 }, +/* 221 */ { 2, 2, 6 }, +/* 222 */ { 2, 2, 7 }, +/* 223 */ { 1, 2 }, +/* 224 */ { 1, 7 }, +/* 225 */ { 1, 4 }, +/* 226 */ { 1, 5 }, +/* 227 */ { 1, 5 }, +/* 228 */ { 1, 6 }, +/* 229 */ { 1, 6 }, +/* 230 */ { 1, 7 }, +/* 231 */ { 2, 3, 4 }, +/* 232 */ { 1, 7 }, +/* 233 */ { 1, 6 }, +/* 234 */ { 1, 7 }, +/* 235 */ { 2, 3, 5 }, +/* 236 */ { 1, 7 }, +/* 237 */ { 2, 3, 6 }, +/* 238 */ { 2, 3, 7 }, +/* 239 */ { 1, 3 }, +/* 240 */ { 4, 4, 5, 6, 7 }, +/* 241 */ { 1, 4 }, +/* 242 */ { 1, 5 }, +/* 243 */ { 2, 4, 5 }, +/* 244 */ { 1, 6 }, +/* 245 */ { 2, 4, 6 }, +/* 246 */ { 2, 4, 7 }, +/* 247 */ { 1, 4 }, +/* 248 */ { 1, 7 }, +/* 249 */ { 2, 5, 6 }, +/* 250 */ { 2, 5, 7 }, +/* 251 */ { 1, 5 }, +/* 252 */ { 2, 6, 7 }, +/* 253 */ { 1, 6 }, +/* 254 */ { 1, 7 }, +/* 255 */ { 8, 0, 1, 2, 3, 4, 5, 6, 7 } +}; + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/misc/extra/extraUtilMisc.c b/src/misc/extra/extraUtilMisc.c index 2767498b..a12fbce4 100644 --- a/src/misc/extra/extraUtilMisc.c +++ b/src/misc/extra/extraUtilMisc.c @@ -429,8 +429,6 @@ unsigned Extra_TruthPolarize( unsigned uTruth, int Polarity, int nVars ) uCof1 >>= Shift; uTruth = uCof0 | uCof1; } - if ( nVars < 5 ) - uTruth &= ((~0) >> (32-nMints)); return uTruth; } @@ -752,6 +750,74 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p SeeAlso [] ***********************************************************************/ +void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters ) +{ + int nPhasesMax = 8; + unsigned * uCanons; + unsigned uTruth, uPhase, uTruth32; + char ** uPhases, * pCounters; + int nFuncs, nClasses, i; + + nFuncs = (1 << 8); + uCanons = ALLOC( unsigned, nFuncs ); + memset( uCanons, 0, sizeof(unsigned) * nFuncs ); + pCounters = ALLOC( char, nFuncs ); + memset( pCounters, 0, sizeof(char) * nFuncs ); + uPhases = (char **)Extra_ArrayAlloc( nFuncs, nPhasesMax, sizeof(char) ); + nClasses = 0; + for ( uTruth = 0; uTruth < (unsigned)nFuncs; uTruth++ ) + { + // skip already assigned + uTruth32 = ((uTruth << 24) | (uTruth << 16) | (uTruth << 8) | uTruth); + if ( uCanons[uTruth] ) + { + assert( uTruth32 > uCanons[uTruth] ); + continue; + } + nClasses++; + for ( i = 0; i < 8; i++ ) + { + uPhase = Extra_TruthPolarize( uTruth, i, 3 ); + if ( uCanons[uPhase] == 0 && (uTruth || i==0) ) + { + uCanons[uPhase] = uTruth32; + uPhases[uPhase][0] = i; + pCounters[uPhase] = 1; + } + else + { + assert( uCanons[uPhase] == uTruth32 ); + if ( pCounters[uPhase] < nPhasesMax ) + uPhases[uPhase][ pCounters[uPhase]++ ] = i; + } + } + } + if ( puCanons ) + *puCanons = uCanons; + else + free( uCanons ); + if ( puPhases ) + *puPhases = uPhases; + else + free( uPhases ); + if ( ppCounters ) + *ppCounters = pCounters; + else + free( pCounters ); + printf( "The number of 3N-classes = %d.\n", nClasses ); +} + +/**Function************************************************************* + + Synopsis [Computes NPN canonical forms for 4-variable functions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int nPhasesMax ) { unsigned short * uCanons; @@ -778,7 +844,7 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp for ( i = 0; i < 16; i++ ) { uPhase = Extra_TruthPolarize( uTruth, i, 4 ); - if ( uCanons[uPhase] == 0 ) + if ( uCanons[uPhase] == 0 && (uTruth || i==0) ) { uCanons[uPhase] = uTruth; uPhases[uPhase][0] = i; @@ -804,6 +870,7 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp *ppCounters = pCounters; else free( pCounters ); + printf( "The number of 4N-classes = %d.\n", nClasses ); } /**Function************************************************************* @@ -1005,6 +1072,208 @@ unsigned Extra_TruthPerm5One( unsigned uTruth, int Phase ) /**Function************************************************************* + Synopsis [Computes a phase of the 3-var function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes ) +{ + // cases + static unsigned Cases[64] = { + 0, // 000000 - skip + 0, // 000001 - skip + 0xCCCCCCCC, // 000010 - single var + 0, // 000011 - skip + 0xF0F0F0F0, // 000100 - single var + 1, // 000101 + 1, // 000110 + 0, // 000111 - skip + 0xFF00FF00, // 001000 - single var + 1, // 001001 + 1, // 001010 + 1, // 001011 + 1, // 001100 + 1, // 001101 + 1, // 001110 + 0, // 001111 - skip + 0xFFFF0000, // 010000 - skip + 1, // 010001 + 1, // 010010 + 1, // 010011 + 1, // 010100 + 1, // 010101 + 1, // 010110 + 1, // 010111 - four var + 1, // 011000 + 1, // 011001 + 1, // 011010 + 1, // 011011 - four var + 1, // 011100 + 1, // 011101 - four var + 1, // 011110 - four var + 0, // 011111 - skip + 0xFFFFFFFF, // 100000 - single var + 1, // 100001 + 1, // 100010 + 1, // 100011 + 1, // 100100 + 1, // 100101 + 1, // 100110 + 1, // 100111 + 1, // 101000 + 1, // 101001 + 1, // 101010 + 1, // 101011 + 1, // 101100 + 1, // 101101 + 1, // 101110 + 1, // 101111 + 1, // 110000 + 1, // 110001 + 1, // 110010 + 1, // 110011 + 1, // 110100 + 1, // 110101 + 1, // 110110 + 1, // 110111 + 1, // 111000 + 1, // 111001 + 1, // 111010 + 1, // 111011 + 1, // 111100 + 1, // 111101 + 1, // 111110 + 0 // 111111 - skip + }; + // permutations + static int Perms[64][6] = { + { 0, 0, 0, 0, 0, 0 }, // 000000 - skip + { 0, 0, 0, 0, 0, 0 }, // 000001 - skip + { 0, 0, 0, 0, 0, 0 }, // 000010 - single var + { 0, 0, 0, 0, 0, 0 }, // 000011 - skip + { 0, 0, 0, 0, 0, 0 }, // 000100 - single var + { 0, 2, 1, 3, 4, 5 }, // 000101 + { 2, 0, 1, 3, 4, 5 }, // 000110 + { 0, 0, 0, 0, 0, 0 }, // 000111 - skip + { 0, 0, 0, 0, 0, 0 }, // 001000 - single var + { 0, 2, 3, 1, 4, 5 }, // 001001 + { 2, 0, 3, 1, 4, 5 }, // 001010 + { 0, 1, 3, 2, 4, 5 }, // 001011 + { 2, 3, 0, 1, 4, 5 }, // 001100 + { 0, 3, 1, 2, 4, 5 }, // 001101 + { 3, 0, 1, 2, 4, 5 }, // 001110 + { 0, 0, 0, 0, 0, 0 }, // 001111 - skip + { 0, 0, 0, 0, 0, 0 }, // 010000 - skip + { 0, 4, 2, 3, 1, 5 }, // 010001 + { 4, 0, 2, 3, 1, 5 }, // 010010 + { 0, 1, 3, 4, 2, 5 }, // 010011 + { 2, 3, 0, 4, 1, 5 }, // 010100 + { 0, 3, 1, 4, 2, 5 }, // 010101 + { 3, 0, 1, 4, 2, 5 }, // 010110 + { 0, 1, 2, 4, 3, 5 }, // 010111 - four var + { 2, 3, 4, 0, 1, 5 }, // 011000 + { 0, 3, 4, 1, 2, 5 }, // 011001 + { 3, 0, 4, 1, 2, 5 }, // 011010 + { 0, 1, 4, 2, 3, 5 }, // 011011 - four var + { 3, 4, 0, 1, 2, 5 }, // 011100 + { 0, 4, 1, 2, 3, 5 }, // 011101 - four var + { 4, 0, 1, 2, 3, 5 }, // 011110 - four var + { 0, 0, 0, 0, 0, 0 }, // 011111 - skip + { 0, 0, 0, 0, 0, 0 }, // 100000 - single var + { 0, 2, 3, 4, 5, 1 }, // 100001 + { 2, 0, 3, 4, 5, 1 }, // 100010 + { 0, 1, 3, 4, 5, 2 }, // 100011 + { 2, 3, 0, 4, 5, 1 }, // 100100 + { 0, 3, 1, 4, 5, 2 }, // 100101 + { 3, 0, 1, 4, 5, 2 }, // 100110 + { 0, 1, 2, 4, 5, 3 }, // 100111 + { 2, 3, 4, 0, 5, 1 }, // 101000 + { 0, 3, 4, 1, 5, 2 }, // 101001 + { 3, 0, 4, 1, 5, 2 }, // 101010 + { 0, 1, 4, 2, 5, 3 }, // 101011 + { 3, 4, 0, 1, 5, 2 }, // 101100 + { 0, 4, 1, 2, 5, 3 }, // 101101 + { 4, 0, 1, 2, 5, 3 }, // 101110 + { 0, 1, 2, 3, 5, 4 }, // 101111 + { 2, 3, 4, 5, 0, 1 }, // 110000 + { 0, 3, 4, 5, 1, 2 }, // 110001 + { 3, 0, 4, 5, 1, 2 }, // 110010 + { 0, 1, 4, 5, 2, 3 }, // 110011 + { 3, 4, 0, 5, 1, 2 }, // 110100 + { 0, 4, 1, 5, 2, 3 }, // 110101 + { 4, 0, 1, 5, 2, 3 }, // 110110 + { 0, 1, 2, 5, 3, 4 }, // 110111 + { 3, 4, 5, 0, 1, 2 }, // 111000 + { 0, 4, 5, 1, 2, 3 }, // 111001 + { 4, 0, 5, 1, 2, 3 }, // 111010 + { 0, 1, 5, 2, 3, 4 }, // 111011 + { 4, 5, 0, 1, 2, 3 }, // 111100 + { 0, 5, 1, 2, 3, 4 }, // 111101 + { 5, 0, 1, 2, 3, 4 }, // 111110 + { 0, 0, 0, 0, 0, 0 } // 111111 - skip + }; + int i, k, iRes; + assert( Phase >= 0 && Phase < 64 ); + if ( Cases[Phase] == 0 ) + { + uTruthRes[0] = uTruth[0]; + uTruthRes[1] = uTruth[1]; + return; + } + if ( Cases[Phase] > 1 ) + { + if ( Phase == 32 ) + { + uTruthRes[0] = 0x00000000; + uTruthRes[1] = 0xFFFFFFFF; + } + else + { + uTruthRes[0] = Cases[Phase]; + uTruthRes[1] = Cases[Phase]; + } + return; + } + uTruthRes[0] = 0; + uTruthRes[1] = 0; + for ( i = 0; i < 64; i++ ) + { + if ( i < 32 ) + { + if ( uTruth[0] & (1 << i) ) + { + for ( iRes = 0, k = 0; k < 6; k++ ) + if ( i & (1 << Perms[Phase][k]) ) + iRes |= (1 << k); + if ( iRes < 32 ) + uTruthRes[0] |= (1 << iRes); + else + uTruthRes[1] |= (1 << (iRes-32)); + } + } + else + { + if ( uTruth[1] & (1 << (i-32)) ) + { + for ( iRes = 0, k = 0; k < 6; k++ ) + if ( i & (1 << Perms[Phase][k]) ) + iRes |= (1 << k); + if ( iRes < 32 ) + uTruthRes[0] |= (1 << iRes); + else + uTruthRes[1] |= (1 << (iRes-32)); + } + } + } +} + +/**Function************************************************************* + Synopsis [Allocated lookup table for truth table permutation.] Description [] @@ -1085,6 +1354,33 @@ unsigned ** Extra_TruthPerm54() /**Function************************************************************* + Synopsis [Allocated lookup table for truth table permutation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned ** Extra_TruthPerm63() +{ + unsigned ** pTable; + unsigned uTruth[2]; + int i, k; + pTable = (unsigned **)Extra_ArrayAlloc( 256, 64, 8 ); + for ( i = 0; i < 256; i++ ) + { + uTruth[0] = (i << 24) | (i << 16) | (i << 8) | i; + uTruth[1] = uTruth[0]; + for ( k = 0; k < 64; k++ ) + Extra_TruthPerm6One( uTruth, k, &pTable[i][k] ); + } + return pTable; +} + +/**Function************************************************************* + Synopsis [Returns the smallest prime larger than the number.] Description [] diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make index bfc9d0ad..3098a23c 100644 --- a/src/misc/extra/module.make +++ b/src/misc/extra/module.make @@ -1,5 +1,6 @@ SRC += src/misc/extra/extraUtilBdd.c \ src/misc/extra/extraUtilBitMatrix.c \ + src/misc/extra/extraUtilCanon.c \ src/misc/extra/extraUtilFile.c \ src/misc/extra/extraUtilMemory.c \ src/misc/extra/extraUtilMisc.c \ diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index effebc68..919b7e5a 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -50,6 +50,8 @@ struct Vec_Int_t_ #define Vec_IntForEachEntry( vVec, Entry, i ) \ for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ ) +#define Vec_IntForEachEntryStart( vVec, Entry, i, Start ) \ + for ( i = Start; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h new file mode 100644 index 00000000..0b4c4535 --- /dev/null +++ b/src/opt/cut/cut.h @@ -0,0 +1,108 @@ +/**CFile**************************************************************** + + FileName [cut.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [K-feasible cut computation package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: .h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CUT_H__ +#define __CUT_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Cut_ManStruct_t_ Cut_Man_t; +typedef struct Cut_CutStruct_t_ Cut_Cut_t; +typedef struct Cut_ParamsStruct_t_ Cut_Params_t; + +struct Cut_ParamsStruct_t_ +{ + int nVarsMax; // the max cut size ("k" of the k-feasible cuts) + int nKeepMax; // the max number of cuts kept at a node + int nIdsMax; // the max number of IDs of cut objects + int fTruth; // compute truth tables + int fHash; // hash cuts to detect unique + int fFilter; // filter dominated cuts + int fSeq; // compute sequential cuts + int fDrop; // drop cuts on the fly + int fVerbose; // the verbosiness flag +}; + +struct Cut_CutStruct_t_ +{ + unsigned uTruth : 16; // truth table for 4-input cuts + unsigned uPhase : 7; // the phase when mapping into a canonical form + unsigned fSimul : 1; // the value of cut's output at 000.. pattern + unsigned fCompl : 1; // the cut is complemented + unsigned fSeq : 1; // the cut is sequential + unsigned nVarsMax : 3; // the max number of vars [4-6] + unsigned nLeaves : 3; // the number of leaves [4-6] + Cut_Cut_t * pNext; // the next cut in the list + void * pData; // the user data + int pLeaves[0]; // the array of leaves +}; + +static inline unsigned * Cut_CutReadTruth( Cut_Cut_t * p ) { if ( p->nVarsMax == 4 ) return (unsigned *)p; return (unsigned *)(p->pLeaves + p->nVarsMax + p->fSeq); } +static inline unsigned Cut_CutReadPhase( Cut_Cut_t * p ) { return p->uPhase; } +static inline int Cut_CutReadLeaveNum( Cut_Cut_t * p ) { return p->nLeaves; } +static inline int * Cut_CutReadLeaves( Cut_Cut_t * p ) { return p->pLeaves; } +static inline void * Cut_CutReadData( Cut_Cut_t * p ) { return p->pData; } + +static inline void * Cut_CutWriteData( Cut_Cut_t * p, void * pData ) { p->pData = pData; } +static inline void Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth ) { + if ( p->nVarsMax == 4 ) { p->uTruth = *puTruth; return; } + p->pLeaves[p->nVarsMax + p->fSeq] = (int)puTruth[0]; + if ( p->nVarsMax == 6 ) p->pLeaves[p->nVarsMax + p->fSeq + 1] = (int)puTruth[1]; +} + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== cutMan.c ==========================================================*/ +extern Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams ); +extern void Cut_ManStop( Cut_Man_t * p ); +extern void Cut_ManPrintStats( Cut_Man_t * p ); +extern void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts ); +/*=== cutNode.c ==========================================================*/ +extern void Cut_NodeSetTriv( Cut_Man_t * p, int Node ); +extern Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 ); +extern Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes ); +extern Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node ); +extern void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList ); +extern void Cut_NodeFreeCuts( Cut_Man_t * p, int Node ); +extern void Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node ); +extern void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h new file mode 100644 index 00000000..da54a188 --- /dev/null +++ b/src/opt/cut/cutInt.h @@ -0,0 +1,107 @@ +/**CFile**************************************************************** + + FileName [cutInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [K-feasible cut computation package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cutInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CUT_INT_H__ +#define __CUT_INT_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include "extra.h" +#include "vec.h" +#include "cut.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Cut_HashTableStruct_t_ Cut_HashTable_t; + +struct Cut_ManStruct_t_ +{ + // user preferences + Cut_Params_t * pParams; // computation parameters + Vec_Int_t * vFanCounts; // the array of fanout counters + // storage for cuts + Vec_Ptr_t * vCuts; // cuts by ID + Vec_Ptr_t * vCutsNew; // cuts by ID + Cut_HashTable_t * tTable; // cuts by their leaves (and root) + // memory management + Extra_MmFixed_t * pMmCuts; + int EntrySize; + // temporary variables + Cut_Cut_t * pReady; + Vec_Ptr_t * vTemp; + int fCompl0; + int fCompl1; + int fSimul; + // precomputations + unsigned uTruthVars[6][2]; + unsigned short ** pPerms43; + unsigned ** pPerms53; + unsigned ** pPerms54; + // statistics + int nCutsCur; + int nCutsAlloc; + int nCutsDealloc; + int nCutsPeak; + int nCutsTriv; + int nCutsNode; + // runtime + int timeMerge; + int timeUnion; + int timeTruth; + int timeFilter; + int timeHash; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== cutMerge.c ==========================================================*/ +extern Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ); +/*=== cutNode.c ==========================================================*/ +extern Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p ); +/*=== cutTable.c ==========================================================*/ +extern Cut_HashTable_t * Cut_TableStart( int Size ); +extern void Cut_TableStop( Cut_HashTable_t * pTable ); +extern int Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t * pCut, int fStore ); +extern void Cut_TableClear( Cut_HashTable_t * pTable ); +extern int Cut_TableReadTime( Cut_HashTable_t * pTable ); +/*=== cutTruth.c ==========================================================*/ +extern void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ); + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + diff --git a/src/opt/cut/cutList.h b/src/opt/cut/cutList.h new file mode 100644 index 00000000..eb008ef9 --- /dev/null +++ b/src/opt/cut/cutList.h @@ -0,0 +1,115 @@ +/**CFile**************************************************************** + + FileName [cutList.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Implementation of layered listed list of cuts.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cutList.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CUT_LIST_H__ +#define __CUT_LIST_H__ + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Cut_ListStruct_t_ Cut_List_t; +struct Cut_ListStruct_t_ +{ + Cut_Cut_t * pHead[7]; + Cut_Cut_t ** ppTail[7]; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cut_ListStart( Cut_List_t * p ) +{ + int i; + for ( i = 1; i <= 6; i++ ) + { + p->pHead[i] = 0; + p->ppTail[i] = &p->pHead[i]; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cut_ListAdd( Cut_List_t * p, Cut_Cut_t * pCut ) +{ + assert( pCut->nLeaves > 0 && pCut->nLeaves < 7 ); + *p->ppTail[pCut->nLeaves] = pCut; + p->ppTail[pCut->nLeaves] = &pCut->pNext; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Cut_Cut_t * Cut_ListFinish( Cut_List_t * p ) +{ + int i; + for ( i = 1; i < 6; i++ ) + *p->ppTail[i] = p->pHead[i+1]; + *p->ppTail[6] = NULL; + return p->pHead[1]; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + +#endif + diff --git a/src/opt/cut/cutMan.c b/src/opt/cut/cutMan.c new file mode 100644 index 00000000..a96f8173 --- /dev/null +++ b/src/opt/cut/cutMan.c @@ -0,0 +1,174 @@ +/**CFile**************************************************************** + + FileName [cutMan.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [K-feasible cut computation package.] + + Synopsis [Cut manager.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cutMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cutInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the cut manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams ) +{ + Cut_Man_t * p; + int clk = clock(); + assert( pParams->nVarsMax >= 4 && pParams->nVarsMax <= 6 ); + p = ALLOC( Cut_Man_t, 1 ); + memset( p, 0, sizeof(Cut_Man_t) ); + // set and correct parameters + p->pParams = pParams; + if ( p->pParams->fSeq ) + p->pParams->fHash = 1; + // space for cuts + p->vCuts = Vec_PtrAlloc( pParams->nIdsMax ); + Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL ); + if ( pParams->fSeq ) + { + p->vCutsNew = Vec_PtrAlloc( pParams->nIdsMax ); + Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL ); + } + // hash tables + if ( pParams->fHash ) + p->tTable = Cut_TableStart( p->pParams->nKeepMax ); + // entry size + p->EntrySize = sizeof(Cut_Cut_t) + (pParams->nVarsMax + pParams->fSeq) * sizeof(int); + if ( pParams->nVarsMax == 5 ) + p->EntrySize += sizeof(unsigned); + else if ( pParams->nVarsMax == 6 ) + p->EntrySize += 2 * sizeof(unsigned); + // memory for cuts + p->pMmCuts = Extra_MmFixedStart( p->EntrySize ); + // precomputations +// if ( pParams->fTruth && pParams->nVarsMax == 4 ) +// p->pPerms43 = Extra_TruthPerm43(); +// else if ( pParams->fTruth ) +// { +// p->pPerms53 = Extra_TruthPerm53(); +// p->pPerms54 = Extra_TruthPerm54(); +// } + p->uTruthVars[0][1] = p->uTruthVars[0][0] = 0xAAAAAAAA; // 1010 1010 1010 1010 1010 1010 1010 1010 + p->uTruthVars[1][1] = p->uTruthVars[1][0] = 0xCCCCCCCC; // 1010 1010 1010 1010 1010 1010 1010 1010 + p->uTruthVars[2][1] = p->uTruthVars[2][0] = 0xF0F0F0F0; // 1111 0000 1111 0000 1111 0000 1111 0000 + p->uTruthVars[3][1] = p->uTruthVars[3][0] = 0xFF00FF00; // 1111 1111 0000 0000 1111 1111 0000 0000 + p->uTruthVars[4][1] = p->uTruthVars[4][0] = 0xFFFF0000; // 1111 1111 1111 1111 0000 0000 0000 0000 + p->uTruthVars[5][0] = 0x00000000; + p->uTruthVars[5][1] = 0xFFFFFFFF; + p->vTemp = Vec_PtrAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the cut manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_ManStop( Cut_Man_t * p ) +{ + Cut_Cut_t * pCut; + int i; + Vec_PtrForEachEntry( p->vCuts, pCut, i ) + { + if ( pCut != NULL ) + { + int k = 0; + } + } + + if ( p->vCutsNew ) Vec_PtrFree( p->vCutsNew ); + if ( p->vCuts ) Vec_PtrFree( p->vCuts ); + if ( p->vFanCounts ) Vec_IntFree( p->vFanCounts ); + if ( p->pPerms43 ) free( p->pPerms43 ); + if ( p->pPerms53 ) free( p->pPerms53 ); + if ( p->pPerms54 ) free( p->pPerms54 ); + if ( p->vTemp ) Vec_PtrFree( p->vTemp ); + if ( p->tTable ) Cut_TableStop( p->tTable ); + Extra_MmFixedStop( p->pMmCuts, 0 ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_ManPrintStats( Cut_Man_t * p ) +{ + printf( "Cut computation statistics:\n" ); + printf( "Current cuts = %8d. (Trivial = %d.)\n", p->nCutsCur-p->nCutsTriv, p->nCutsTriv ); + printf( "Peak cuts = %8d.\n", p->nCutsPeak ); + printf( "Total allocated = %8d.\n", p->nCutsAlloc ); + printf( "Total deallocated = %8d.\n", p->nCutsDealloc ); + printf( "The cut size = %3d bytes.\n", p->EntrySize ); + printf( "Peak memory = %.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) ); + PRT( "Merge ", p->timeMerge ); + PRT( "Union ", p->timeUnion ); + PRT( "Hash ", Cut_TableReadTime(p->tTable) ); + PRT( "Filter", p->timeFilter ); + PRT( "Truth ", p->timeTruth ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts ) +{ + p->vFanCounts = vFanCounts; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/cut/cutMerge.c b/src/opt/cut/cutMerge.c new file mode 100644 index 00000000..ba1afce4 --- /dev/null +++ b/src/opt/cut/cutMerge.c @@ -0,0 +1,656 @@ +/**CFile**************************************************************** + + FileName [cutMerge.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [K-feasible cut computation package.] + + Synopsis [Procedure to merge two cuts.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cutMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cutInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Merges two cuts.] + + Description [This procedure works.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ + static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}}; + Cut_Cut_t * pRes; + int * pRow; + int nLeaves0, nLeaves1, Limit; + int i, k, Count, nNodes; + + assert( pCut0->nLeaves >= pCut1->nLeaves ); + + // the case of the largest cut sizes + Limit = p->pParams->nVarsMax; + nLeaves0 = pCut0->nLeaves; + nLeaves1 = pCut1->nLeaves; + if ( nLeaves0 == Limit && nLeaves1 == Limit ) + { + for ( i = 0; i < nLeaves0; i++ ) + if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] ) + return NULL; + pRes = Cut_CutAlloc( p ); + for ( i = 0; i < nLeaves0; i++ ) + pRes->pLeaves[i] = pCut0->pLeaves[i]; + pRes->nLeaves = nLeaves0; + return pRes; + } + // the case when one of the cuts is the largest + if ( nLeaves0 == Limit ) + { + for ( i = 0; i < nLeaves1; i++ ) + { + for ( k = nLeaves0 - 1; k >= 0; k-- ) + if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] ) + break; + if ( k == -1 ) // did not find + return NULL; + } + pRes = Cut_CutAlloc( p ); + for ( i = 0; i < nLeaves0; i++ ) + pRes->pLeaves[i] = pCut0->pLeaves[i]; + pRes->nLeaves = nLeaves0; + return pRes; + } + // other cases + nNodes = nLeaves0; + for ( i = 0; i < nLeaves1; i++ ) + { + for ( k = nLeaves0 - 1; k >= 0; k-- ) + { + if ( pCut0->pLeaves[k] > pCut1->pLeaves[i] ) + continue; + if ( pCut0->pLeaves[k] < pCut1->pLeaves[i] ) + { + pRow = M[k+1]; + if ( pRow[0] == 0 ) + pRow[0] = pCut1->pLeaves[i], pRow[1] = 0; + else if ( pRow[1] == 0 ) + pRow[1] = pCut1->pLeaves[i], pRow[2] = 0; + else if ( pRow[2] == 0 ) + pRow[2] = pCut1->pLeaves[i]; + else + assert( 0 ); + if ( ++nNodes > Limit ) + { + for ( i = 0; i <= nLeaves0; i++ ) + M[i][0] = 0; + return NULL; + } + } + break; + } + if ( k == -1 ) + { + pRow = M[0]; + if ( pRow[0] == 0 ) + pRow[0] = pCut1->pLeaves[i], pRow[1] = 0; + else if ( pRow[1] == 0 ) + pRow[1] = pCut1->pLeaves[i], pRow[2] = 0; + else if ( pRow[2] == 0 ) + pRow[2] = pCut1->pLeaves[i]; + else + assert( 0 ); + if ( ++nNodes > Limit ) + { + for ( i = 0; i <= nLeaves0; i++ ) + M[i][0] = 0; + return NULL; + } + continue; + } + } + + pRes = Cut_CutAlloc( p ); + for ( Count = 0, i = 0; i <= nLeaves0; i++ ) + { + if ( i > 0 ) + pRes->pLeaves[Count++] = pCut0->pLeaves[i-1]; + pRow = M[i]; + if ( pRow[0] ) + { + pRes->pLeaves[Count++] = pRow[0]; + if ( pRow[1] ) + { + pRes->pLeaves[Count++] = pRow[1]; + if ( pRow[2] ) + pRes->pLeaves[Count++] = pRow[2]; + } + pRow[0] = 0; + } + } + assert( Count == nNodes ); + pRes->nLeaves = nNodes; + return pRes; +} + +/**Function************************************************************* + + Synopsis [Merges two cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_CutMergeTwo2( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ + Cut_Cut_t * pRes; + int * pLeaves; + int Limit, nLeaves0, nLeaves1; + int i, k, c; + + assert( pCut0->nLeaves >= pCut1->nLeaves ); + + // consider two cuts + nLeaves0 = pCut0->nLeaves; + nLeaves1 = pCut1->nLeaves; + + // the case of the largest cut sizes + Limit = p->pParams->nVarsMax; + if ( nLeaves0 == Limit && nLeaves1 == Limit ) + { + for ( i = 0; i < nLeaves0; i++ ) + if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] ) + return NULL; + pRes = Cut_CutAlloc( p ); + for ( i = 0; i < nLeaves0; i++ ) + pRes->pLeaves[i] = pCut0->pLeaves[i]; + pRes->nLeaves = pCut0->nLeaves; + return pRes; + } + // the case when one of the cuts is the largest + if ( nLeaves0 == Limit ) + { + for ( i = 0; i < nLeaves1; i++ ) + { + for ( k = nLeaves0 - 1; k >= 0; k-- ) + if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] ) + break; + if ( k == -1 ) // did not find + return NULL; + } + pRes = Cut_CutAlloc( p ); + for ( i = 0; i < nLeaves0; i++ ) + pRes->pLeaves[i] = pCut0->pLeaves[i]; + pRes->nLeaves = pCut0->nLeaves; + return pRes; + } + + // prepare the cut + if ( p->pReady == NULL ) + p->pReady = Cut_CutAlloc( p ); + pLeaves = p->pReady->pLeaves; + + // compare two cuts with different numbers + i = k = 0; + for ( c = 0; c < Limit; c++ ) + { + if ( k == nLeaves1 ) + { + if ( i == nLeaves0 ) + { + p->pReady->nLeaves = c; + pRes = p->pReady; p->pReady = NULL; + return pRes; + } + pLeaves[c] = pCut0->pLeaves[i++]; + continue; + } + if ( i == nLeaves0 ) + { + if ( k == nLeaves1 ) + { + p->pReady->nLeaves = c; + pRes = p->pReady; p->pReady = NULL; + return pRes; + } + pLeaves[c] = pCut1->pLeaves[k++]; + continue; + } + if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] ) + { + pLeaves[c] = pCut0->pLeaves[i++]; + continue; + } + if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] ) + { + pLeaves[c] = pCut1->pLeaves[k++]; + continue; + } + pLeaves[c] = pCut0->pLeaves[i++]; + k++; + } + if ( i < nLeaves0 || k < nLeaves1 ) + return NULL; + p->pReady->nLeaves = c; + pRes = p->pReady; p->pReady = NULL; + return pRes; +} + + +/**Function************************************************************* + + Synopsis [Merges two cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_CutMergeTwo3( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ + Cut_Cut_t * pRes; + int * pLeaves; + int Limit, nLeaves0, nLeaves1; + int i, k, c; + + assert( pCut0->nLeaves >= pCut1->nLeaves ); + + // prepare the cut + if ( p->pReady == NULL ) + p->pReady = Cut_CutAlloc( p ); + pLeaves = p->pReady->pLeaves; + + // consider two cuts + Limit = p->pParams->nVarsMax; + nLeaves0 = pCut0->nLeaves; + nLeaves1 = pCut1->nLeaves; + if ( nLeaves0 == Limit ) + { // the case when one of the cuts is the largest + if ( nLeaves1 == Limit ) + { // the case when both cuts are the largest + for ( i = 0; i < nLeaves0; i++ ) + { + pLeaves[i] = pCut0->pLeaves[i]; + if ( pLeaves[i] != pCut1->pLeaves[i] ) + return NULL; + } + } + else + { + for ( i = k = 0; i < nLeaves0; i++ ) + { + pLeaves[i] = pCut0->pLeaves[i]; + if ( k == (int)nLeaves1 ) + continue; + if ( pLeaves[i] < pCut1->pLeaves[k] ) + continue; + if ( pLeaves[i] == pCut1->pLeaves[k++] ) + continue; + return NULL; + } + if ( k < nLeaves1 ) + return NULL; + } + p->pReady->nLeaves = nLeaves0; + pRes = p->pReady; p->pReady = NULL; + return pRes; + } + + // compare two cuts with different numbers + i = k = 0; + for ( c = 0; c < Limit; c++ ) + { + if ( k == nLeaves1 ) + { + if ( i == nLeaves0 ) + { + p->pReady->nLeaves = c; + pRes = p->pReady; p->pReady = NULL; + return pRes; + } + pLeaves[c] = pCut0->pLeaves[i++]; + continue; + } + if ( i == nLeaves0 ) + { + if ( k == nLeaves1 ) + { + p->pReady->nLeaves = c; + pRes = p->pReady; p->pReady = NULL; + return pRes; + } + pLeaves[c] = pCut1->pLeaves[k++]; + continue; + } + if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] ) + { + pLeaves[c] = pCut0->pLeaves[i++]; + continue; + } + if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] ) + { + pLeaves[c] = pCut1->pLeaves[k++]; + continue; + } + pLeaves[c] = pCut0->pLeaves[i++]; + k++; + } + if ( i < nLeaves0 || k < nLeaves1 ) + return NULL; + p->pReady->nLeaves = c; + pRes = p->pReady; p->pReady = NULL; + return pRes; +} + +/**Function************************************************************* + + Synopsis [Merges two cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_CutMergeTwo4( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ + Cut_Cut_t * pRes; + int * pLeaves; + int i, k, min, NodeTemp, Limit, nTotal; + + assert( pCut0->nLeaves >= pCut1->nLeaves ); + + // prepare the cut + if ( p->pReady == NULL ) + p->pReady = Cut_CutAlloc( p ); + pLeaves = p->pReady->pLeaves; + + // consider two cuts + Limit = p->pParams->nVarsMax; + if ( pCut0->nLeaves == (unsigned)Limit ) + { // the case when one of the cuts is the largest + if ( pCut1->nLeaves == (unsigned)Limit ) + { // the case when both cuts are the largest + for ( i = 0; i < (int)pCut0->nLeaves; i++ ) + { + pLeaves[i] = pCut0->pLeaves[i]; + if ( pLeaves[i] != pCut1->pLeaves[i] ) + return NULL; + } + } + else + { + for ( i = k = 0; i < (int)pCut0->nLeaves; i++ ) + { + pLeaves[i] = pCut0->pLeaves[i]; + if ( k == (int)pCut1->nLeaves ) + continue; + if ( pLeaves[i] < pCut1->pLeaves[k] ) + continue; + if ( pLeaves[i] == pCut1->pLeaves[k++] ) + continue; + return NULL; + } + if ( k < (int)pCut1->nLeaves ) + return NULL; + } + p->pReady->nLeaves = pCut0->nLeaves; + pRes = p->pReady; p->pReady = NULL; + return pRes; + } + + // count the number of unique entries in pCut1 + nTotal = pCut0->nLeaves; + for ( i = 0; i < (int)pCut1->nLeaves; i++ ) + { + // try to find this entry among the leaves of pCut0 + for ( k = 0; k < (int)pCut0->nLeaves; k++ ) + if ( pCut1->pLeaves[i] == pCut0->pLeaves[k] ) + break; + if ( k < (int)pCut0->nLeaves ) // found + continue; + // we found a new entry to add + if ( nTotal == Limit ) + return NULL; + pLeaves[nTotal++] = pCut1->pLeaves[i]; + } + // we know that the feasible cut exists + + // add the starting entries + for ( k = 0; k < (int)pCut0->nLeaves; k++ ) + pLeaves[k] = pCut0->pLeaves[k]; + + // selection-sort the entries + for ( i = 0; i < nTotal - 1; i++ ) + { + min = i; + for ( k = i+1; k < nTotal; k++ ) + if ( pLeaves[k] < pLeaves[min] ) + min = k; + NodeTemp = pLeaves[i]; + pLeaves[i] = pLeaves[min]; + pLeaves[min] = NodeTemp; + } + p->pReady->nLeaves = nTotal; + pRes = p->pReady; p->pReady = NULL; + return pRes; +} + +/**Function************************************************************* + + Synopsis [Merges two cuts.] + + Description [This procedure works.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_CutMergeTwo5( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ + static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}}; + Cut_Cut_t * pRes; + int * pRow; + unsigned uSign0, uSign1; + int i, k, nNodes, Count; + unsigned Limit = p->pParams->nVarsMax; + + assert( pCut0->nLeaves >= pCut1->nLeaves ); + + // the case of the largest cut sizes + if ( pCut0->nLeaves == Limit && pCut1->nLeaves == Limit ) + { + for ( i = 0; i < (int)pCut0->nLeaves; i++ ) + if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] ) + return NULL; + pRes = Cut_CutAlloc( p ); + for ( i = 0; i < (int)pCut0->nLeaves; i++ ) + pRes->pLeaves[i] = pCut0->pLeaves[i]; + pRes->nLeaves = pCut0->nLeaves; + return pRes; + } + // the case when one of the cuts is the largest + if ( pCut0->nLeaves == Limit ) + { + if ( !p->pParams->fTruth ) + { + for ( i = 0; i < (int)pCut1->nLeaves; i++ ) + { + for ( k = pCut0->nLeaves - 1; k >= 0; k-- ) + if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] ) + break; + if ( k == -1 ) // did not find + return NULL; + } + pRes = Cut_CutAlloc( p ); + } + else + { + uSign1 = 0; + for ( i = 0; i < (int)pCut1->nLeaves; i++ ) + { + for ( k = pCut0->nLeaves - 1; k >= 0; k-- ) + if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] ) + { + uSign1 |= (1 << i); + break; + } + if ( k == -1 ) // did not find + return NULL; + } + pRes = Cut_CutAlloc( p ); + pRes->uTruth = (uSign1 << 8); + } + for ( i = 0; i < (int)pCut0->nLeaves; i++ ) + pRes->pLeaves[i] = pCut0->pLeaves[i]; + pRes->nLeaves = pCut0->nLeaves; + return pRes; + } + // other cases + nNodes = pCut0->nLeaves; + for ( i = 0; i < (int)pCut1->nLeaves; i++ ) + { + for ( k = pCut0->nLeaves - 1; k >= 0; k-- ) + { + if ( pCut0->pLeaves[k] > pCut1->pLeaves[i] ) + continue; + if ( pCut0->pLeaves[k] < pCut1->pLeaves[i] ) + { + pRow = M[k+1]; + if ( pRow[0] == 0 ) + pRow[0] = pCut1->pLeaves[i], pRow[1] = 0; + else if ( pRow[1] == 0 ) + pRow[1] = pCut1->pLeaves[i], pRow[2] = 0; + else if ( pRow[2] == 0 ) + pRow[2] = pCut1->pLeaves[i]; + else + assert( 0 ); + if ( ++nNodes > (int)Limit ) + { + for ( i = 0; i <= (int)pCut0->nLeaves; i++ ) + M[i][0] = 0; + return NULL; + } + } + break; + } + if ( k == -1 ) + { + pRow = M[0]; + if ( pRow[0] == 0 ) + pRow[0] = pCut1->pLeaves[i], pRow[1] = 0; + else if ( pRow[1] == 0 ) + pRow[1] = pCut1->pLeaves[i], pRow[2] = 0; + else if ( pRow[2] == 0 ) + pRow[2] = pCut1->pLeaves[i]; + else + assert( 0 ); + if ( ++nNodes > (int)Limit ) + { + for ( i = 0; i <= (int)pCut0->nLeaves; i++ ) + M[i][0] = 0; + return NULL; + } + continue; + } + } + + pRes = Cut_CutAlloc( p ); + if ( !p->pParams->fTruth ) + { + for ( Count = 0, i = 0; i <= (int)pCut0->nLeaves; i++ ) + { + if ( i > 0 ) + pRes->pLeaves[Count++] = pCut0->pLeaves[i-1]; + pRow = M[i]; + if ( pRow[0] ) + { + pRes->pLeaves[Count++] = pRow[0]; + if ( pRow[1] ) + { + pRes->pLeaves[Count++] = pRow[1]; + if ( pRow[2] ) + pRes->pLeaves[Count++] = pRow[2]; + } + pRow[0] = 0; + } + } + assert( Count == nNodes ); + pRes->nLeaves = nNodes; +/* + // make sure that the cut is correct + { + for ( i = 1; i < (int)pRes->nLeaves; i++ ) + if ( pRes->pLeaves[i-1] >= pRes->pLeaves[i] ) + { + int v = 0; + } + } +*/ + return pRes; + } + + uSign0 = uSign1 = 0; + for ( Count = 0, i = 0; i <= (int)pCut0->nLeaves; i++ ) + { + if ( i > 0 ) + { + uSign0 |= (1 << Count); + pRes->pLeaves[Count++] = pCut1->pLeaves[i-1]; + } + pRow = M[i]; + if ( pRow[0] ) + { + uSign1 |= (1 << Count); + pRes->pLeaves[Count++] = pRow[0]; + if ( pRow[1] ) + { + uSign1 |= (1 << Count); + pRes->pLeaves[Count++] = pRow[1]; + if ( pRow[2] ) + { + uSign1 |= (1 << Count); + pRes->pLeaves[Count++] = pRow[2]; + } + } + pRow[0] = 0; + } + } + assert( Count == nNodes ); + pRes->nLeaves = nNodes; + pRes->uTruth = (uSign1 << 8) | uSign0; + return pRes; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c new file mode 100644 index 00000000..6ce3b983 --- /dev/null +++ b/src/opt/cut/cutNode.c @@ -0,0 +1,623 @@ +/**CFile**************************************************************** + + FileName [cutNode.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [K-feasible cut computation package.] + + Synopsis [Procedures to compute cuts for a node.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cutNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cutInt.h" +#include "cutList.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node ); +static inline void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut ); +static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList ); + +static void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ); +static void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList ); + +// iterator through all the cuts of the list +#define Cut_ListForEachCut( pList, pCut ) \ + for ( pCut = pList; \ + pCut; \ + pCut = pCut->pNext ) +#define Cut_ListForEachCutStop( pList, pCut, pStop ) \ + for ( pCut = pList; \ + pCut != pStop; \ + pCut = pCut->pNext ) +#define Cut_ListForEachCutSafe( pList, pCut, pCut2 ) \ + for ( pCut = pList, \ + pCut2 = pCut? pCut->pNext: NULL; \ + pCut; \ + pCut = pCut2, \ + pCut2 = pCut? pCut->pNext: NULL ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the pointer to the linked list of cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node ) +{ + return Vec_PtrEntry( p->vCuts, Node ); +} + +/**Function************************************************************* + + Synopsis [Returns the pointer to the linked list of cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList ) +{ + Vec_PtrWriteEntry( p->vCuts, Node, pList ); +} + +/**Function************************************************************* + + Synopsis [Sets the trivial cut for the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_NodeSetTriv( Cut_Man_t * p, int Node ) +{ + assert( Cut_NodeReadCuts(p, Node) == NULL ); + Cut_NodeWriteCuts( p, Node, Cut_CutCreateTriv(p, Node) ); +} + +/**Function************************************************************* + + Synopsis [Deallocates the cuts at the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_NodeFreeCuts( Cut_Man_t * p, int Node ) +{ + Cut_Cut_t * pList, * pCut, * pCut2; + pList = Cut_NodeReadCuts( p, Node ); + if ( pList == NULL ) + return; + Cut_ListForEachCutSafe( pList, pCut, pCut2 ) + Cut_CutRecycle( p, pCut ); + Cut_NodeWriteCuts( p, Node, NULL ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node ) +{ +} + +/**Function************************************************************* + + Synopsis [Computes the cuts by merging cuts at two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 ) +{ + Cut_List_t SuperList; + Cut_Cut_t * pList0, * pList1, * pStop0, * pStop1, * pTemp0, * pTemp1; + int i, Limit = p->pParams->nVarsMax; + int clk = clock(); + assert( p->pParams->nVarsMax <= 6 ); + // start the new list + Cut_ListStart( &SuperList ); + // get the cut lists of children + pList0 = Cut_NodeReadCuts( p, Node0 ); + pList1 = Cut_NodeReadCuts( p, Node1 ); + assert( pList0 && pList1 ); + // get the simultation bit of the node + p->fSimul = (fCompl0 ^ pList0->fSimul) & (fCompl1 ^ pList1->fSimul); + // set temporary variables + p->fCompl0 = fCompl0; + p->fCompl1 = fCompl1; + // find the point in the list where the max-var cuts begin + Cut_ListForEachCut( pList0, pStop0 ) + if ( pStop0->nLeaves == (unsigned)Limit ) + break; + Cut_ListForEachCut( pList1, pStop1 ) + if ( pStop1->nLeaves == (unsigned)Limit ) + break; + // start with the elementary cut + pTemp0 = Cut_CutCreateTriv( p, Node ); + Cut_ListAdd( &SuperList, pTemp0 ); + p->nCutsNode = 1; + // small by small + Cut_ListForEachCutStop( pList0, pTemp0, pStop0 ) + Cut_ListForEachCutStop( pList1, pTemp1, pStop1 ) + if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) ) + goto finish; + // all by large + Cut_ListForEachCut( pList0, pTemp0 ) + Cut_ListForEachCut( pStop1, pTemp1 ) + if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) ) + goto finish; + // all by large + Cut_ListForEachCut( pList1, pTemp1 ) + Cut_ListForEachCut( pStop0, pTemp0 ) + if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) ) + goto finish; + // large by large + Cut_ListForEachCut( pStop0, pTemp0 ) + Cut_ListForEachCut( pStop1, pTemp1 ) + { + assert( pTemp0->nLeaves == (unsigned)Limit && pTemp1->nLeaves == (unsigned)Limit ); + for ( i = 0; i < Limit; i++ ) + if ( pTemp0->pLeaves[i] != pTemp1->pLeaves[i] ) + break; + if ( i < Limit ) + continue; + if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) ) + goto finish; + } +finish : + // set the list at the node + assert( Cut_NodeReadCuts(p, Node) == NULL ); + pList0 = Cut_ListFinish( &SuperList ); + Cut_NodeWriteCuts( p, Node, pList0 ); + // clear the hash table + if ( p->pParams->fHash && !p->pParams->fSeq ) + Cut_TableClear( p->tTable ); + // consider dropping the fanins cuts + if ( p->pParams->fDrop ) + { + Cut_NodeTryDroppingCuts( p, Node0 ); + Cut_NodeTryDroppingCuts( p, Node1 ); + } +p->timeMerge += clock() - clk; + // filter the cuts +clk = clock(); + if ( p->pParams->fFilter ) + Cut_CutFilter( p, pList0 ); +p->timeFilter += clock() - clk; + return pList0; +} + +/**Function************************************************************* + + Synopsis [Processes two cuts.] + + Description [Returns 1 if the limit has been reached.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList ) +{ + Cut_Cut_t * pCut; + // merge the cuts + if ( pCut0->nLeaves >= pCut1->nLeaves ) + pCut = Cut_CutMergeTwo( p, pCut0, pCut1 ); + else + pCut = Cut_CutMergeTwo( p, pCut1, pCut0 ); + if ( pCut == NULL ) + return 0; + assert( pCut->nLeaves > 1 ); + // add the root if sequential + if ( p->pParams->fSeq ) + pCut->pLeaves[pCut->nLeaves] = Root; + // check the lookup table + if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) ) + { + Cut_CutRecycle( p, pCut ); + return 0; + } + // compute the truth table + if ( p->pParams->fTruth ) + Cut_TruthCompute( p, pCut, pCut0, pCut1 ); + // add to the list + Cut_ListAdd( pSuperList, pCut ); + // return status (0 if okay; 1 if exceeded the limit) + return ++p->nCutsNode == p->pParams->nKeepMax; +} + +/**Function************************************************************* + + Synopsis [Computes the cuts by unioning cuts at a choice node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes ) +{ + Cut_List_t SuperList; + Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop; + int i, k, Node, Root, Limit = p->pParams->nVarsMax; + int clk = clock(); + + assert( p->pParams->nVarsMax <= 6 ); + + // start the new list + Cut_ListStart( &SuperList ); + + // remember the root node to save the resulting cuts + Root = Vec_IntEntry( vNodes, 0 ); + p->nCutsNode = 1; + + // collect small cuts first + Vec_PtrClear( p->vTemp ); + Vec_IntForEachEntry( vNodes, Node, i ) + { + // get the cuts of this node + pList = Cut_NodeReadCuts( p, Node ); + Cut_NodeWriteCuts( p, Node, NULL ); + assert( pList ); + // remember the starting point + pListStart = pList->pNext; + // save or recycle the elementary cut + if ( i == 0 ) + Cut_ListAdd( &SuperList, pList ), pTop = pList; + else + Cut_CutRecycle( p, pList ); + // save all the cuts that are smaller than the limit + Cut_ListForEachCutSafe( pListStart, pCut, pCut2 ) + { + if ( pCut->nLeaves == (unsigned)Limit ) + { + Vec_PtrPush( p->vTemp, pCut ); + break; + } + // check hash tables + if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) ) + { + Cut_CutRecycle( p, pCut ); + continue; + } + // set the complemented bit by comparing the first cut with the current cut + pCut->fCompl = pTop->fSimul ^ pCut->fSimul; + // add to the list + Cut_ListAdd( &SuperList, pCut ); + if ( ++p->nCutsNode == p->pParams->nKeepMax ) + { + // recycle the rest of the cuts of this node + Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 ) + Cut_CutRecycle( p, pCut ); + // recycle all cuts of other nodes + Vec_IntForEachEntryStart( vNodes, Node, k, i+1 ) + Cut_NodeFreeCuts( p, Node ); + // recycle the saved cuts of other nodes + Vec_PtrForEachEntry( p->vTemp, pList, k ) + Cut_ListForEachCutSafe( pList, pCut, pCut2 ) + Cut_CutRecycle( p, pCut ); + goto finish; + } + } + } + // collect larger cuts next + Vec_PtrForEachEntry( p->vTemp, pList, i ) + { + Cut_ListForEachCutSafe( pList, pCut, pCut2 ) + { + if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) ) + { + Cut_CutRecycle( p, pCut ); + continue; + } + // set the complemented bit + pCut->fCompl = pTop->fSimul ^ pCut->fSimul; + // add to the list + Cut_ListAdd( &SuperList, pCut ); + if ( ++p->nCutsNode == p->pParams->nKeepMax ) + { + // recycle the rest of the cuts + Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 ) + Cut_CutRecycle( p, pCut ); + // recycle the saved cuts of other nodes + Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 ) + Cut_ListForEachCutSafe( pList, pCut, pCut2 ) + Cut_CutRecycle( p, pCut ); + goto finish; + } + } + } +finish : + // set the cuts at the node + assert( Cut_NodeReadCuts(p, Root) == NULL ); + pList = Cut_ListFinish( &SuperList ); + Cut_NodeWriteCuts( p, Root, pList ); + // clear the hash table + if ( p->pParams->fHash && !p->pParams->fSeq ) + Cut_TableClear( p->tTable ); +p->timeUnion += clock() - clk; + // filter the cuts +clk = clock(); + if ( p->pParams->fFilter ) + Cut_CutFilter( p, pList ); +p->timeFilter += clock() - clk; + return pList; +} + +/**Function************************************************************* + + Synopsis [Start the cut computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p ) +{ + Cut_Cut_t * pCut; + // cut allocation + pCut = (Cut_Cut_t *)Extra_MmFixedEntryFetch( p->pMmCuts ); + memset( pCut, 0, sizeof(Cut_Cut_t) ); + pCut->nVarsMax = p->pParams->nVarsMax; + pCut->fSeq = p->pParams->fSeq; + pCut->fSimul = p->fSimul; + // statistics + p->nCutsAlloc++; + p->nCutsCur++; + if ( p->nCutsPeak < p->nCutsAlloc - p->nCutsDealloc ) + p->nCutsPeak = p->nCutsAlloc - p->nCutsDealloc; + return pCut; +} + +/**Function************************************************************* + + Synopsis [Start the cut computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node ) +{ + Cut_Cut_t * pCut; + pCut = Cut_CutAlloc( p ); + pCut->nLeaves = 1; + pCut->pLeaves[0] = Node; + if ( p->pParams->fTruth ) + Cut_CutWriteTruth( pCut, p->uTruthVars[0] ); + p->nCutsTriv++; + return pCut; +} + +/**Function************************************************************* + + Synopsis [Start the cut computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut ) +{ + p->nCutsDealloc++; + p->nCutsCur--; + if ( pCut->nLeaves == 1 ) + p->nCutsTriv--; + Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut ); +} + + +/**Function************************************************************* + + Synopsis [Consider dropping cuts if they are useless by now.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node ) +{ + int nFanouts; + assert( p->vFanCounts ); + nFanouts = Vec_IntEntry( p->vFanCounts, Node ); + assert( nFanouts > 0 ); + if ( --nFanouts == 0 ) + Cut_NodeFreeCuts( p, Node ); + Vec_IntWriteEntry( p->vFanCounts, Node, nFanouts ); +} + +/**Function************************************************************* + + Synopsis [Print the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_CutPrint( Cut_Cut_t * pCut ) +{ + int i; + assert( pCut->nLeaves > 1 ); + printf( "%d : {", pCut->nLeaves ); + for ( i = 0; i < (int)pCut->nLeaves; i++ ) + printf( " %d", pCut->pLeaves[i] ); + printf( " }" ); +} + +/**Function************************************************************* + + Synopsis [Consider dropping cuts if they are useless by now.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ + printf( "\n" ); + printf( "%d : %5d %5d %5d %5d %5d\n", + pCut0->nLeaves, + pCut0->nLeaves > 0 ? pCut0->pLeaves[0] : -1, + pCut0->nLeaves > 1 ? pCut0->pLeaves[1] : -1, + pCut0->nLeaves > 2 ? pCut0->pLeaves[2] : -1, + pCut0->nLeaves > 3 ? pCut0->pLeaves[3] : -1, + pCut0->nLeaves > 4 ? pCut0->pLeaves[4] : -1 + ); + printf( "%d : %5d %5d %5d %5d %5d\n", + pCut1->nLeaves, + pCut1->nLeaves > 0 ? pCut1->pLeaves[0] : -1, + pCut1->nLeaves > 1 ? pCut1->pLeaves[1] : -1, + pCut1->nLeaves > 2 ? pCut1->pLeaves[2] : -1, + pCut1->nLeaves > 3 ? pCut1->pLeaves[3] : -1, + pCut1->nLeaves > 4 ? pCut1->pLeaves[4] : -1 + ); + if ( pCut == NULL ) + printf( "Cannot merge\n" ); + else + printf( "%d : %5d %5d %5d %5d %5d\n", + pCut->nLeaves, + pCut->nLeaves > 0 ? pCut->pLeaves[0] : -1, + pCut->nLeaves > 1 ? pCut->pLeaves[1] : -1, + pCut->nLeaves > 2 ? pCut->pLeaves[2] : -1, + pCut->nLeaves > 3 ? pCut->pLeaves[3] : -1, + pCut->nLeaves > 4 ? pCut->pLeaves[4] : -1 + ); +} + + +/**Function************************************************************* + + Synopsis [Filter the cuts using dominance.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList ) +{ + Cut_Cut_t * pListR, ** ppListR = &pListR; + Cut_Cut_t * pCut, * pCut2, * pDom, * pPrev; + int i, k; + // save the first cut + *ppListR = pList, ppListR = &pList->pNext; + // try to filter out other cuts + pPrev = pList; + Cut_ListForEachCutSafe( pList->pNext, pCut, pCut2 ) + { + assert( pCut->nLeaves > 1 ); + // go through all the previous cuts up to pCut + Cut_ListForEachCutStop( pList->pNext, pDom, pCut ) + { + if ( pDom->nLeaves >= pCut->nLeaves ) + continue; + // check if every node in pDom is contained in pCut + for ( i = 0; i < (int)pDom->nLeaves; i++ ) + { + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + if ( pDom->pLeaves[i] == pCut->pLeaves[k] ) + break; + if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut + break; + } + if ( i == (int)pDom->nLeaves ) // every node in pDom is contained in pCut + break; + } + if ( pDom != pCut ) // pDom is contained in pCut - recycle pCut + { + // make sure cuts are connected after removing + pPrev->pNext = pCut->pNext; +/* + // report + printf( "Recycling cut: " ); + Cut_CutPrint( pCut ); + printf( "\n" ); + printf( "As contained in: " ); + Cut_CutPrint( pDom ); + printf( "\n" ); +*/ + // recycle the cut + Cut_CutRecycle( p, pCut ); + } + else // pDom is NOT contained in pCut - save pCut + { + *ppListR = pCut, ppListR = &pCut->pNext; + pPrev = pCut; + } + } + *ppListR = NULL; +} + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/cut/cutSeq.c b/src/opt/cut/cutSeq.c new file mode 100644 index 00000000..869bd7b3 --- /dev/null +++ b/src/opt/cut/cutSeq.c @@ -0,0 +1,47 @@ +/**CFile**************************************************************** + + FileName [cutSeq.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [K-feasible cut computation package.] + + Synopsis [Sequential cut computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cutSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cutInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/cut/cutTable.c b/src/opt/cut/cutTable.c new file mode 100644 index 00000000..5dfaca7b --- /dev/null +++ b/src/opt/cut/cutTable.c @@ -0,0 +1,253 @@ +/**CFile**************************************************************** + + FileName [cutTable.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [K-feasible cut computation package.] + + Synopsis [Hashing cuts to prevent duplication.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cutTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cutInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct Cut_HashTableStruct_t_ +{ + int nBins; + Cut_Cut_t ** pBins; + int nEntries; + int * pPlaces; + int nPlaces; + int timeLookup; +}; + +// iterator through all the cuts of the list +#define Cut_TableListForEachCut( pList, pCut ) \ + for ( pCut = pList; \ + pCut; \ + pCut = pCut->pData ) +#define Cut_TableListForEachCutSafe( pList, pCut, pCut2 ) \ + for ( pCut = pList, \ + pCut2 = pCut? pCut->pData: NULL; \ + pCut; \ + pCut = pCut2, \ + pCut2 = pCut? pCut->pData: NULL ) + +// primes used to compute the hash key +static int s_HashPrimes[10] = { 109, 499, 557, 619, 631, 709, 797, 881, 907, 991 }; + +// hashing function +static inline unsigned Cut_HashKey( Cut_Cut_t * pCut ) +{ + unsigned i, uRes = pCut->nLeaves * s_HashPrimes[9]; + for ( i = 0; i < pCut->nLeaves + pCut->fSeq; i++ ) + uRes += s_HashPrimes[i] * pCut->pLeaves[i]; + return uRes; +} + +// hashing function +static inline int Cut_CompareTwo( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 ) +{ + unsigned i; + if ( pCut1->nLeaves != pCut2->nLeaves ) + return 1; + for ( i = 0; i < pCut1->nLeaves; i++ ) + if ( pCut1->pLeaves[i] != pCut2->pLeaves[i] ) + return 1; + return 0; +} + +static void Cut_TableResize( Cut_HashTable_t * pTable ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_HashTable_t * Cut_TableStart( int Size ) +{ + Cut_HashTable_t * pTable; + pTable = ALLOC( Cut_HashTable_t, 1 ); + memset( pTable, 0, sizeof(Cut_HashTable_t) ); + // allocate the table + pTable->nBins = Cudd_PrimeCopy( Size ); + pTable->pBins = ALLOC( Cut_Cut_t *, pTable->nBins ); + memset( pTable->pBins, 0, sizeof(Cut_Cut_t *) * pTable->nBins ); + pTable->pPlaces = ALLOC( int, pTable->nBins ); + return pTable; +} + +/**Function************************************************************* + + Synopsis [Stops the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_TableStop( Cut_HashTable_t * pTable ) +{ + FREE( pTable->pPlaces ); + free( pTable->pBins ); + free( pTable ); +} + +/**Function************************************************************* + + Synopsis [Check the existence of a cut in the lookup table] + + Description [Returns 1 if the entry is found.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t * pCut, int fStore ) +{ + Cut_Cut_t * pEnt; + unsigned Key; + int clk = clock(); + + Key = Cut_HashKey(pCut) % pTable->nBins; + Cut_TableListForEachCut( pTable->pBins[Key], pEnt ) + { + if ( !Cut_CompareTwo( pEnt, pCut ) ) + { +pTable->timeLookup += clock() - clk; + return 1; + } + } + if ( pTable->nEntries > 2 * pTable->nBins ) + { + Cut_TableResize( pTable ); + Key = Cut_HashKey(pCut) % pTable->nBins; + } + // remember the place + if ( fStore && pTable->pBins[Key] == NULL ) + pTable->pPlaces[ pTable->nPlaces++ ] = Key; + // add the cut to the table + pCut->pData = pTable->pBins[Key]; + pTable->pBins[Key] = pCut; + pTable->nEntries++; +pTable->timeLookup += clock() - clk; + return 0; +} + + +/**Function************************************************************* + + Synopsis [Stops the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_TableClear( Cut_HashTable_t * pTable ) +{ + int i; + assert( pTable->nPlaces <= pTable->nBins ); + for ( i = 0; i < pTable->nPlaces; i++ ) + { + assert( pTable->pBins[ pTable->pPlaces[i] ] ); + pTable->pBins[ pTable->pPlaces[i] ] = NULL; + } + pTable->nPlaces = 0; + pTable->nEntries = 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_TableResize( Cut_HashTable_t * pTable ) +{ + Cut_Cut_t ** pBinsNew; + Cut_Cut_t * pEnt, * pEnt2; + int nBinsNew, Counter, i, clk; + unsigned Key; + +clk = clock(); + // get the new table size + nBinsNew = Cudd_PrimeCopy( 3 * pTable->nBins ); + // allocate a new array + pBinsNew = ALLOC( Cut_Cut_t *, nBinsNew ); + memset( pBinsNew, 0, sizeof(Cut_Cut_t *) * nBinsNew ); + // rehash the entries from the old table + Counter = 0; + for ( i = 0; i < pTable->nBins; i++ ) + Cut_TableListForEachCutSafe( pTable->pBins[i], pEnt, pEnt2 ) + { + Key = Cut_HashKey(pEnt) % nBinsNew; + pEnt->pData = pBinsNew[Key]; + pBinsNew[Key] = pEnt; + Counter++; + } + assert( Counter == pTable->nEntries ); +// printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew ); +// PRT( "Time", clock() - clk ); + // replace the table and the parameters + free( pTable->pBins ); + pTable->pBins = pBinsNew; + pTable->nBins = nBinsNew; +} + +/**Function************************************************************* + + Synopsis [Stops the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cut_TableReadTime( Cut_HashTable_t * pTable ) +{ + if ( pTable == NULL ) + return 0; + return pTable->timeLookup; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/cut/cutTruth.c b/src/opt/cut/cutTruth.c new file mode 100644 index 00000000..efacd456 --- /dev/null +++ b/src/opt/cut/cutTruth.c @@ -0,0 +1,322 @@ +/**CFile**************************************************************** + + FileName [cutTruth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [K-feasible cut computation package.] + + Synopsis [Incremental truth table computation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cutTruth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cutInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Cut_TruthCompute4( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ); +static void Cut_TruthCompute5( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ); +static void Cut_TruthCompute6( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs truth table computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 ) +{ + unsigned uPhase = 0; + int i, k; + for ( i = k = 0; i < (int)pCut->nLeaves; i++ ) + { + if ( k == (int)pCut1->nLeaves ) + break; + if ( pCut->pLeaves[i] < pCut1->pLeaves[k] ) + continue; + assert( pCut->pLeaves[i] == pCut1->pLeaves[k] ); + uPhase |= (1 << i); + k++; + } + return uPhase; +} + +/**Function************************************************************* + + Synopsis [Performs truth table computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ +int clk = clock(); + if ( pCut->nVarsMax == 4 ) + Cut_TruthCompute4( p, pCut, pCut0, pCut1 ); + else if ( pCut->nVarsMax == 5 ) + Cut_TruthCompute5( p, pCut, pCut0, pCut1 ); + else // if ( pCut->nVarsMax == 6 ) + Cut_TruthCompute6( p, pCut, pCut0, pCut1 ); +p->timeTruth += clock() - clk; +} + +/**Function************************************************************* + + Synopsis [Performs truth table computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_TruthCompute4( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ + unsigned * puTruthCut0, * puTruthCut1; + unsigned uTruth0, uTruth1, uPhase; + + puTruthCut0 = Cut_CutReadTruth(pCut0); + puTruthCut1 = Cut_CutReadTruth(pCut1); + + uPhase = Cut_TruthPhase( pCut, pCut0 ); + uTruth0 = Extra_TruthPerm4One( *puTruthCut0, uPhase ); + uTruth0 = p->fCompl0? ~uTruth0: uTruth0; + + uPhase = Cut_TruthPhase( pCut, pCut1 ); + uTruth1 = Extra_TruthPerm4One( *puTruthCut1, uPhase ); + uTruth1 = p->fCompl1? ~uTruth1: uTruth1; + + uTruth1 = uTruth0 & uTruth1; + if ( pCut->fCompl ) + uTruth1 = ~uTruth1; + if ( pCut->nVarsMax == 4 ) + uTruth1 &= 0xFFFF; + Cut_CutWriteTruth( pCut, &uTruth1 ); +} + +/**Function************************************************************* + + Synopsis [Performs truth table computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_TruthCompute5( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ + unsigned * puTruthCut0, * puTruthCut1; + unsigned uTruth0, uTruth1, uPhase; + + puTruthCut0 = Cut_CutReadTruth(pCut0); + puTruthCut1 = Cut_CutReadTruth(pCut1); + + uPhase = Cut_TruthPhase( pCut, pCut0 ); + uTruth0 = Extra_TruthPerm5One( *puTruthCut0, uPhase ); + uTruth0 = p->fCompl0? ~uTruth0: uTruth0; + + uPhase = Cut_TruthPhase( pCut, pCut1 ); + uTruth1 = Extra_TruthPerm5One( *puTruthCut1, uPhase ); + uTruth1 = p->fCompl1? ~uTruth1: uTruth1; + + uTruth1 = uTruth0 & uTruth1; + if ( pCut->fCompl ) + uTruth1 = ~uTruth1; + Cut_CutWriteTruth( pCut, &uTruth1 ); +} + +/**Function************************************************************* + + Synopsis [Performs truth table computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_TruthCompute6( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ + unsigned * puTruthCut0, * puTruthCut1; + unsigned uTruth0[2], uTruth1[2], uPhase; + + puTruthCut0 = Cut_CutReadTruth(pCut0); + puTruthCut1 = Cut_CutReadTruth(pCut1); + + uPhase = Cut_TruthPhase( pCut, pCut0 ); + Extra_TruthPerm6One( puTruthCut0, uPhase, uTruth0 ); + uTruth0[0] = p->fCompl0? ~uTruth0[0]: uTruth0[0]; + uTruth0[1] = p->fCompl0? ~uTruth0[1]: uTruth0[1]; + + uPhase = Cut_TruthPhase( pCut, pCut1 ); + Extra_TruthPerm6One( puTruthCut1, uPhase, uTruth1 ); + uTruth1[0] = p->fCompl1? ~uTruth1[0]: uTruth1[0]; + uTruth1[1] = p->fCompl1? ~uTruth1[1]: uTruth1[1]; + + uTruth1[0] = uTruth0[0] & uTruth1[0]; + uTruth1[1] = uTruth0[1] & uTruth1[1]; + if ( pCut->fCompl ) + { + uTruth1[0] = ~uTruth0[0]; + uTruth1[1] = ~uTruth0[1]; + } + Cut_CutWriteTruth( pCut, uTruth1 ); +} + + + + + + +/**Function************************************************************* + + Synopsis [Performs truth table computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cut_TruthComputeOld( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 ) +{ + unsigned uTruth0, uTruth1, uPhase; + int clk = clock(); + + assert( pCut->nVarsMax < 6 ); + + // assign the truth table + if ( pCut0->nLeaves == pCut->nLeaves ) + uTruth0 = *Cut_CutReadTruth(pCut0); + else + { + assert( pCut0->nLeaves < pCut->nLeaves ); + uPhase = Cut_TruthPhase( pCut, pCut0 ); + if ( pCut->nVarsMax == 4 ) + { + assert( pCut0->nLeaves < 4 ); + assert( uPhase < 16 ); + uTruth0 = p->pPerms43[pCut0->uTruth & 0xFF][uPhase]; + } + else + { + assert( pCut->nVarsMax == 5 ); + assert( pCut0->nLeaves < 5 ); + assert( uPhase < 32 ); + if ( pCut0->nLeaves == 4 ) + { +// Count4++; +/* + if ( uPhase == 31-16 ) // 01111 + uTruth0 = pCut0->uTruth; + else if ( uPhase == 31-8 ) // 10111 + uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][0]; + else if ( uPhase == 31-4 ) // 11011 + uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][1]; + else if ( uPhase == 31-2 ) // 11101 + uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][2]; + else if ( uPhase == 31-1 ) // 11110 + uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][3]; + else + assert( 0 ); +*/ + uTruth0 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut0), uPhase ); + } + else + { +// Count5++; +// uTruth0 = p->pPerms53[pCut0->uTruth & 0xFF][uPhase]; + uTruth0 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut0), uPhase ); + } + } + } + uTruth0 = p->fCompl0? ~uTruth0: uTruth0; + + // assign the truth table + if ( pCut1->nLeaves == pCut->nLeaves ) + uTruth0 = *Cut_CutReadTruth(pCut1); + else + { + assert( pCut1->nLeaves < pCut->nLeaves ); + uPhase = Cut_TruthPhase( pCut, pCut1 ); + if ( pCut->nVarsMax == 4 ) + { + assert( pCut1->nLeaves < 4 ); + assert( uPhase < 16 ); + uTruth1 = p->pPerms43[pCut1->uTruth & 0xFF][uPhase]; + } + else + { + assert( pCut->nVarsMax == 5 ); + assert( pCut1->nLeaves < 5 ); + assert( uPhase < 32 ); + if ( pCut1->nLeaves == 4 ) + { +// Count4++; +/* + if ( uPhase == 31-16 ) // 01111 + uTruth1 = pCut1->uTruth; + else if ( uPhase == 31-8 ) // 10111 + uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][0]; + else if ( uPhase == 31-4 ) // 11011 + uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][1]; + else if ( uPhase == 31-2 ) // 11101 + uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][2]; + else if ( uPhase == 31-1 ) // 11110 + uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][3]; + else + assert( 0 ); +*/ + uTruth1 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut1), uPhase ); + } + else + { +// Count5++; +// uTruth1 = p->pPerms53[pCut1->uTruth & 0xFF][uPhase]; + uTruth1 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut1), uPhase ); + } + } + } + uTruth1 = p->fCompl1? ~uTruth1: uTruth1; + uTruth1 = uTruth0 & uTruth1; + if ( pCut->fCompl ) + uTruth1 = ~uTruth1; + if ( pCut->nVarsMax == 4 ) + uTruth1 &= 0xFFFF; + Cut_CutWriteTruth( pCut, &uTruth1 ); +p->timeTruth += clock() - clk; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/cut/module.make b/src/opt/cut/module.make new file mode 100644 index 00000000..1175b3f2 --- /dev/null +++ b/src/opt/cut/module.make @@ -0,0 +1,6 @@ +SRC += src/opt/cut/cutMan.c \ + src/opt/cut/cutMerge.c \ + src/opt/cut/cutNode.c \ + src/opt/cut/cutSeq.c \ + src/opt/cut/cutTable.c \ + src/opt/cut/cutTruth.c diff --git a/src/opt/fxu/module.make b/src/opt/fxu/module.make index 331712d1..dd8acd40 100644 --- a/src/opt/fxu/module.make +++ b/src/opt/fxu/module.make @@ -1,12 +1,12 @@ -SRC += fxu.c \ - fxuCreate.c \ - fxuHeapD.c \ - fxuHeapS.c \ - fxuList.c \ - fxuMatrix.c \ - fxuPair.c \ - fxuPrint.c \ - fxuReduce.c \ - fxuSelect.c \ - fxuSingle.c \ - fxuUpdate.c +SRC += src/opt/fxu/fxu.c \ + src/opt/fxu/fxuCreate.c \ + src/opt/fxu/fxuHeapD.c \ + src/opt/fxu/fxuHeapS.c \ + src/opt/fxu/fxuList.c \ + src/opt/fxu/fxuMatrix.c \ + src/opt/fxu/fxuPair.c \ + src/opt/fxu/fxuPrint.c \ + src/opt/fxu/fxuReduce.c \ + src/opt/fxu/fxuSelect.c \ + src/opt/fxu/fxuSingle.c \ + src/opt/fxu/fxuUpdate.c diff --git a/src/opt/rwr/module.make b/src/opt/rwr/module.make index e97eb33e..fc72630f 100644 --- a/src/opt/rwr/module.make +++ b/src/opt/rwr/module.make @@ -1,6 +1,7 @@ -SRC += rwrCut.c \ - rwrEva.c \ - rwrExp.c \ - rwrLib.c \ - rwrMan.c \ - rwrUtil.c +SRC += src/opt/rwr/rwrCut.c \ + src/opt/rwr/rwrEva.c \ + src/opt/rwr/rwrExp.c \ + src/opt/rwr/rwrLib.c \ + src/opt/rwr/rwrMan.c \ + src/opt/rwr/rwrPrint.c \ + src/opt/rwr/rwrUtil.c diff --git a/src/opt/rwr/rwrCut.c b/src/opt/rwr/rwrCut.c index 209d6ee6..be512963 100644 --- a/src/opt/rwr/rwrCut.c +++ b/src/opt/rwr/rwrCut.c @@ -245,6 +245,8 @@ Rwr_Cut_t * Rwr_CutCreateTriv( Rwr_Man_t * p, Abc_Obj_t * pNode ) } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/sim/module.make b/src/sat/sim/module.make index 8f1b4ded..ac887acf 100644 --- a/src/sat/sim/module.make +++ b/src/sat/sim/module.make @@ -1,6 +1,6 @@ -SRC += simMan.c \ - simSat.c \ - simSupp.c \ - simSym.c \ - simUnate.c \ - simUtils.c +SRC += src/sat/sim/simMan.c \ + src/sat/sim/simSat.c \ + src/sat/sim/simSupp.c \ + src/sat/sim/simSym.c \ + src/sat/sim/simUnate.c \ + src/sat/sim/simUtils.c |