diff options
Diffstat (limited to 'src/base/abci')
32 files changed, 2598 insertions, 234 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ffab5116..26ef2b66 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -64,6 +64,7 @@ static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -82,6 +83,7 @@ static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -115,6 +117,9 @@ static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -167,6 +172,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "resub", Abc_CommandResubstitute, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "rr", Abc_CommandRr, 1 ); // Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 ); @@ -185,6 +191,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 ); Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 ); Cmd_CommandAdd( pAbc, "Various", "espresso", Abc_CommandEspresso, 1 ); + Cmd_CommandAdd( pAbc, "Various", "gen", Abc_CommandGen, 0 ); Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); @@ -218,9 +225,13 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); + Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 ); + // Rwt_Man4ExploreStart(); // Map_Var3Print(); // Map_Var4Test(); + } /**Function************************************************************* @@ -1598,6 +1609,7 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int fBddSizeMax; int fDualRail; + int fReorder; int c; pNtk = Abc_FrameReadNtk(pAbc); @@ -1605,10 +1617,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults + fReorder = 1; fDualRail = 0; fBddSizeMax = 1000000; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Bdh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Brdh" ) ) != EOF ) { switch ( c ) { @@ -1626,6 +1639,9 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': fDualRail ^= 1; break; + case 'r': + fReorder ^= 1; + break; case 'h': goto usage; default: @@ -1647,11 +1663,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( Abc_NtkIsStrash(pNtk) ) - pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, 1 ); + pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 ); else { pNtk = Abc_NtkStrash( pNtk, 0, 0 ); - pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, 1 ); + pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, fReorder, 1 ); Abc_NtkDelete( pNtk ); } if ( pNtkRes == NULL ) @@ -1664,9 +1680,10 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: collapse [-B num] [-dh]\n" ); + fprintf( pErr, "usage: collapse [-B num] [-rdh]\n" ); fprintf( pErr, "\t collapses the network by constructing global BDDs\n" ); fprintf( pErr, "\t-B num : limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax ); + fprintf( pErr, "\t-r : toggles dynamic variable reordering [default = %s]\n", fReorder? "yes": "no" ); fprintf( pErr, "\t-d : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -2759,6 +2776,102 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandRr( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c, Window; + int nFaninLevels; + int nFanoutLevels; + int fUseFanouts; + int fVerbose; + extern int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFanouts, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFaninLevels = 3; + nFanoutLevels = 3; + fUseFanouts = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Wfvh" ) ) != EOF ) + { + switch ( c ) + { + case 'W': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" ); + goto usage; + } + Window = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Window < 0 ) + goto usage; + nFaninLevels = Window / 10; + nFanoutLevels = Window % 10; + break; + case 'f': + fUseFanouts ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" ); + return 1; + } + if ( Abc_NtkGetChoiceNum(pNtk) ) + { + fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" ); + return 1; + } + + // modify the current network + if ( !Abc_NtkRR( pNtk, nFaninLevels, nFanoutLevels, fUseFanouts, fVerbose ) ) + { + fprintf( pErr, "Redundancy removal has failed.\n" ); + return 1; + } + return 0; + +usage: + fprintf( pErr, "usage: rr [-W NM] [-fvh]\n" ); + fprintf( pErr, "\t performs redundancy removal in the current network\n" ); + fprintf( pErr, "\t-W NM : window size as the number of TFI (N) and TFO (M) logic levels [default = %d%d]\n", nFaninLevels, nFanoutLevels ); + fprintf( pErr, "\t-f : toggle RR w.r.t. fanouts [default = %s]\n", fUseFanouts? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -3806,10 +3919,12 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fTruth = 0; // compute truth tables pParams->fFilter = 1; // filter dominated cuts pParams->fDrop = 0; // drop cuts on the fly - pParams->fMulti = 0; // use multi-input AND-gates + pParams->fDag = 0; // compute DAG cuts + pParams->fTree = 0; // compute tree cuts + pParams->fFancy = 0; // compute something fancy pParams->fVerbose = 0; // the verbosiness flag Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdmvoh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdxyzvoh" ) ) != EOF ) { switch ( c ) { @@ -3844,8 +3959,14 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': pParams->fDrop ^= 1; break; - case 'm': - pParams->fMulti ^= 1; + case 'x': + pParams->fDag ^= 1; + break; + case 'y': + pParams->fTree ^= 1; + break; + case 'z': + pParams->fFancy ^= 1; break; case 'v': pParams->fVerbose ^= 1; @@ -3875,6 +3996,11 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", CUT_SIZE_MIN, CUT_SIZE_MAX ); return 1; } + if ( pParams->fDag && pParams->fTree ) + { + fprintf( pErr, "Cannot compute both DAG cuts and tree cuts at the same time.\n" ); + return 1; + } if ( fOracle ) pParams->fRecord = 1; @@ -3891,14 +4017,16 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdmvh]\n" ); + fprintf( pErr, "usage: cut [-K num] [-M num] [-tfdxyzvh]\n" ); fprintf( pErr, "\t computes k-feasible cuts for the AIG\n" ); fprintf( pErr, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n", CUT_SIZE_MIN, CUT_SIZE_MAX, pParams->nVarsMax ); fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n", pParams->nKeepMax ); fprintf( pErr, "\t-t : toggle truth table computation [default = %s]\n", pParams->fTruth? "yes": "no" ); fprintf( pErr, "\t-f : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter? "yes": "no" ); fprintf( pErr, "\t-d : toggle dropping when fanouts are done [default = %s]\n", pParams->fDrop? "yes": "no" ); - fprintf( pErr, "\t-m : toggle computing only factor-cuts [default = %s]\n", pParams->fMulti? "yes": "no" ); + fprintf( pErr, "\t-x : toggle computing only DAG cuts [default = %s]\n", pParams->fDag? "yes": "no" ); + fprintf( pErr, "\t-y : toggle computing only tree cuts [default = %s]\n", pParams->fTree? "yes": "no" ); + fprintf( pErr, "\t-z : toggle fancy computations [default = %s]\n", pParams->fFancy? "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; @@ -4160,6 +4288,99 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int nVars; + int fAdder; + int fSorter; + int fVerbose; + char * FileName; + extern void Abc_GenAdder( char * pFileName, int nVars ); + extern void Abc_GenSorter( char * pFileName, int nVars ); + + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nVars = 8; + fAdder = 0; + fSorter = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Nasvh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nVars < 0 ) + goto usage; + break; + case 'a': + fAdder ^= 1; + break; + case 's': + fSorter ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( argc != globalUtilOptind + 1 ) + { + goto usage; + } + + // get the input file name + FileName = argv[globalUtilOptind]; + if ( fAdder ) + Abc_GenAdder( FileName, nVars ); + else if ( fSorter ) + Abc_GenSorter( FileName, nVars ); + else + printf( "Type of circuit is not specified.\n" ); + return 0; + +usage: + fprintf( pErr, "usage: gen [-N] [-asvh] <file>\n" ); + fprintf( pErr, "\t generates simple circuits\n" ); + fprintf( pErr, "\t-N num : the number of variables [default = %d]\n", nVars ); + fprintf( pErr, "\t-a : toggle ripple-carry adder [default = %s]\n", fAdder? "yes": "no" ); + fprintf( pErr, "\t-s : toggle simple sorter [default = %s]\n", fSorter? "yes": "no" ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\t<file> : output file name\n"); + return 1; +} + /**Function************************************************************* @@ -4175,7 +4396,7 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtkRes; + Abc_Ntk_t * pNtk;//, * pNtkRes; int c; // extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); @@ -4195,25 +4416,27 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } +/* if ( pNtk == NULL ) { fprintf( pErr, "Empty network.\n" ); return 1; } - if ( Abc_NtkIsSeq(pNtk) ) { fprintf( pErr, "Only works for non-sequential networks.\n" ); return 1; } +*/ // Abc_NtkTestEsop( pNtk ); // Abc_NtkTestSop( pNtk ); // printf( "This command is currently not used.\n" ); // run the command // pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); - // pNtkRes = Abc_NtkNewAig( pNtk ); + +/* pNtkRes = NULL; if ( pNtkRes == NULL ) { @@ -4222,6 +4445,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); +*/ + +// if ( Cut_CellIsRunning() ) +// Cut_CellDumpToFile(); +// else +// Cut_CellPrecompute(); + Cut_CellLoad(); + return 0; usage: @@ -6459,6 +6690,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; int RetValue; + int fJFront; int fVerbose; int nConfLimit; int nImpLimit; @@ -6469,11 +6701,12 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults + fJFront = 0; fVerbose = 0; nConfLimit = 100000; nImpLimit = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CIvjh" ) ) != EOF ) { switch ( c ) { @@ -6499,6 +6732,9 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nImpLimit < 0 ) goto usage; break; + case 'j': + fJFront ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -6528,13 +6764,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) clk = clock(); if ( Abc_NtkIsStrash(pNtk) ) { - RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fVerbose ); + RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fJFront, fVerbose ); } else { Abc_Ntk_t * pTemp; pTemp = Abc_NtkStrash( pNtk, 0, 0 ); - RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fVerbose ); + RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fJFront, fVerbose ); pNtk->pModel = pTemp->pModel; pTemp->pModel = NULL; Abc_NtkDelete( pTemp ); } @@ -6544,7 +6780,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) { int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel ); if ( pSimInfo[0] != 1 ) - printf( "ERROR in Abc_NtkMiterProve(): Generated counter example is invalid.\n" ); + printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" ); free( pSimInfo ); } @@ -6559,11 +6795,12 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" ); + fprintf( pErr, "usage: sat [-C num] [-I num] [-jvh]\n" ); fprintf( pErr, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" ); fprintf( pErr, "\t derives CNF from the current network and leave it unchanged\n" ); fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit ); + fprintf( pErr, "\t-j : toggle the use of J-frontier [default = %s]\n", fJFront? "yes": "no" ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -6584,60 +6821,72 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkTemp; - int c; - int RetValue; - int fVerbose; - int fRewrite; - int fFraig; - int nConfLimit; - int nImpLimit; - int clk; + Prove_Params_t Params, * pParams = &Params; + int c, clk, RetValue; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fVerbose = 0; - fRewrite = 1; - fFraig = 1; - nConfLimit = 300000; - nImpLimit = 0; + Prove_ParamsSetDefault( pParams ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CIrfvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NCFLrfvh" ) ) != EOF ) { switch ( c ) { + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pParams->nItersMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pParams->nItersMax < 0 ) + goto usage; + break; case 'C': if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } - nConfLimit = atoi(argv[globalUtilOptind]); + pParams->nMiteringLimitStart = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nConfLimit < 0 ) + if ( pParams->nMiteringLimitStart < 0 ) goto usage; break; - case 'I': + case 'F': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nImpLimit = atoi(argv[globalUtilOptind]); + pParams->nFraigingLimitStart = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nImpLimit < 0 ) + if ( pParams->nFraigingLimitStart < 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + pParams->nMiteringLimitLast = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pParams->nMiteringLimitLast < 0 ) goto usage; break; case 'r': - fRewrite ^= 1; + pParams->fUseRewriting ^= 1; break; case 'f': - fFraig ^= 1; + pParams->fUseFraiging ^= 1; break; case 'v': - fVerbose ^= 1; + pParams->fVerbose ^= 1; break; case 'h': goto usage; @@ -6674,7 +6923,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv ) else pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 ); - RetValue = Abc_NtkMiterProve( &pNtkTemp, nConfLimit, nImpLimit, fRewrite, fFraig, fVerbose ); + RetValue = Abc_NtkMiterProve( &pNtkTemp, pParams ); // verify that the pattern is correct if ( RetValue == 0 ) @@ -6699,19 +6948,143 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: prove [-C num] [-I num] [-rfvh]\n" ); + fprintf( pErr, "usage: prove [-N num] [-C num] [-F num] [-L num] [-rfvh]\n" ); fprintf( pErr, "\t solves combinational miter by rewriting, FRAIGing, and SAT\n" ); fprintf( pErr, "\t replaces the current network by the cone modified by rewriting\n" ); - fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); - fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit ); - fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); - fprintf( pErr, "\t-f : toggle the use of FRAIGing [default = %s]\n", fFraig? "yes": "no" ); - fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-N num : max number of iterations [default = %d]\n", pParams->nItersMax ); + fprintf( pErr, "\t-C num : max starting number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitStart ); + fprintf( pErr, "\t-F num : max starting number of conflicts in fraiging [default = %d]\n", pParams->nFraigingLimitStart ); + fprintf( pErr, "\t-L num : max last-gasp number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitLast ); + fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", pParams->fUseRewriting? "yes": "no" ); + fprintf( pErr, "\t-f : toggle the use of FRAIGing [default = %s]\n", pParams->fUseFraiging? "yes": "no" ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", pParams->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTraceStart( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command is applicable to AIGs.\n" ); + return 1; + } + + Abc_HManStart(); + if ( !Abc_HManPopulate( pNtk ) ) + { + fprintf( pErr, "Failed to start the tracing database.\n" ); + return 1; + } + return 0; + +usage: + fprintf( pErr, "usage: trace_start [-h]\n" ); + fprintf( pErr, "\t starts verification tracing\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTraceCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command is applicable to AIGs.\n" ); + return 1; + } + + if ( !Abc_HManIsRunning(pNtk) ) + { + fprintf( pErr, "The tracing database is not available.\n" ); + return 1; + } + + if ( !Abc_HManVerify( 1, pNtk->Id ) ) + fprintf( pErr, "Verification failed.\n" ); + Abc_HManStop(); + return 0; + +usage: + fprintf( pErr, "usage: trace_check [-h]\n" ); + fprintf( pErr, "\t checks the current network using verification trace\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c index fb818ff3..cc6e8913 100644 --- a/src/base/abci/abcAuto.c +++ b/src/base/abci/abcAuto.c @@ -51,7 +51,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose ) int nOutputs, nInputs, i; // compute the global BDDs - if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL ) + if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL ) return; // get information about the network diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index 919ea3b2..9e9212aa 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -29,6 +29,8 @@ static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate, bool fSelective ); static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate, bool fSelective ); static void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk ); +static Vec_Ptr_t * Abc_NodeBalanceConeExor( Abc_Obj_t * pNode ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -227,6 +229,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ return pNodeOld->pCopy; assert( Abc_ObjIsNode(pNodeOld) ); // get the implication supergate +// Abc_NodeBalanceConeExor( pNodeOld ); vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate, fSelective ); if ( vSuper->nSize == 0 ) { // it means that the supergate contains two nodes in the opposite polarity @@ -260,6 +263,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ assert( pNodeOld->pCopy == NULL ); // mark the old node with the new node pNodeOld->pCopy = vSuper->pArray[0]; + Abc_HManAddProto( pNodeOld->pCopy, pNodeOld ); vSuper->nSize = 0; return pNodeOld->pCopy; } @@ -351,6 +355,65 @@ int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeBalanceConeExor_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst ) +{ + int RetValue1, RetValue2, i; + // check if the node occurs in the same polarity + for ( i = 0; i < vSuper->nSize; i++ ) + if ( vSuper->pArray[i] == pNode ) + return 1; + // if the new node is complemented or a PI, another gate begins + if ( !fFirst && (!pNode->fExor || !Abc_ObjIsNode(pNode)) ) + { + Vec_PtrPush( vSuper, pNode ); + return 0; + } + assert( !Abc_ObjIsComplement(pNode) ); + assert( Abc_ObjIsNode(pNode) ); + assert( pNode->fExor ); + // go through the branches + RetValue1 = Abc_NodeBalanceConeExor_rec( Abc_ObjFanin0(Abc_ObjFanin0(pNode)), vSuper, 0 ); + RetValue2 = Abc_NodeBalanceConeExor_rec( Abc_ObjFanin1(Abc_ObjFanin0(pNode)), vSuper, 0 ); + if ( RetValue1 == -1 || RetValue2 == -1 ) + return -1; + // return 1 if at least one branch has a duplicate + return RetValue1 || RetValue2; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NodeBalanceConeExor( Abc_Obj_t * pNode ) +{ + Vec_Ptr_t * vSuper; + if ( !pNode->fExor ) + return NULL; + vSuper = Vec_PtrAlloc( 10 ); + Abc_NodeBalanceConeExor_rec( pNode, vSuper, 1 ); + printf( "%d ", Vec_PtrSize(vSuper) ); + Vec_PtrFree( vSuper ); + return NULL; +} + /**Function************************************************************* diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c index 84016436..eed18e1b 100644 --- a/src/base/abci/abcClpBdd.c +++ b/src/base/abci/abcClpBdd.c @@ -43,14 +43,14 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose ) +Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose ) { Abc_Ntk_t * pNtkNew; assert( Abc_NtkIsStrash(pNtk) ); // compute the global BDDs - if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0) == NULL ) + if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0, fReorder, fVerbose) == NULL ) return NULL; if ( fVerbose ) printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) ); diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c index 2b1816c4..2752dc69 100644 --- a/src/base/abci/abcCut.c +++ b/src/base/abci/abcCut.c @@ -29,6 +29,9 @@ static void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq ); static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq ); + +extern int nTotal, nGood, nEqual; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -46,6 +49,7 @@ static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq ); ***********************************************************************/ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) { + ProgressBar * pProgress; Cut_Man_t * p; Abc_Obj_t * pObj, * pNode; Vec_Ptr_t * vNodes; @@ -56,6 +60,8 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) extern void Abc_NtkBalanceAttach( Abc_Ntk_t * pNtk ); extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk ); + nTotal = nGood = nEqual = 0; + assert( Abc_NtkIsStrash(pNtk) ); // start the manager pParams->nIdsMax = Abc_NtkObjNumMax( pNtk ); @@ -69,6 +75,7 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) // compute cuts for internal nodes vNodes = Abc_AigDfs( pNtk, 0, 1 ); // collects POs vChoices = Vec_IntAlloc( 100 ); + pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodes) ); Vec_PtrForEachEntry( vNodes, pObj, i ) { // when we reached a CO, it is time to deallocate the cuts @@ -81,8 +88,9 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) // skip constant node, it has no cuts if ( Abc_NodeIsConst(pObj) ) continue; + Extra_ProgressBarUpdate( pProgress, i, NULL ); // compute the cuts to the internal node - Abc_NodeGetCuts( p, pObj, pParams->fMulti ); + Abc_NodeGetCuts( p, pObj, pParams->fDag, pParams->fTree ); // consider dropping the fanins cuts if ( pParams->fDrop ) { @@ -98,11 +106,16 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) Cut_NodeUnionCuts( p, vChoices ); } } + Extra_ProgressBarStop( pProgress ); Vec_PtrFree( vNodes ); Vec_IntFree( vChoices ); PRT( "Total", clock() - clk ); //Abc_NtkPrintCuts_( p, pNtk, 0 ); // Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk ); + + // temporary printout of stats + if ( nTotal ) + printf( "Total cuts = %d. Good cuts = %d. Ratio = %5.2f\n", nTotal, nGood, ((double)nGood)/nTotal ); return p; } @@ -276,14 +289,14 @@ printf( "Converged after %d iterations.\n", nIters ); SeeAlso [] ***********************************************************************/ -void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti ) +void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree ) { void * pList; if ( pList = Abc_NodeReadCuts( p, pObj ) ) return pList; - Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fMulti ); - Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fMulti ); - return Abc_NodeGetCuts( p, pObj, fMulti ); + Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fDag, fTree ); + Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fDag, fTree ); + return Abc_NodeGetCuts( p, pObj, fDag, fTree ); } /**Function************************************************************* @@ -297,14 +310,28 @@ void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti ) SeeAlso [] ***********************************************************************/ -void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti ) +void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree ) { -// int fTriv = (!fMulti) || pObj->fMarkB; - int fTriv = (!fMulti) || (pObj->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pObj)); + Abc_Obj_t * pFanin; + int fDagNode, fTriv, TreeCode = 0; assert( Abc_NtkIsStrash(pObj->pNtk) ); assert( Abc_ObjFaninNum(pObj) == 2 ); + // check if the node is a DAG node + fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj)); + // increment the counter of DAG nodes + if ( fDagNode ) Cut_ManIncrementDagNodes( p ); + // add the trivial cut if the node is a DAG node, or if we compute all cuts + fTriv = fDagNode || !fDag; + // check if fanins are DAG nodes + if ( fTree ) + { + pFanin = Abc_ObjFanin0(pObj); + TreeCode |= (Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin)); + pFanin = Abc_ObjFanin1(pObj); + TreeCode |= ((Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin)) << 1); + } return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj), - Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv ); + Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv, TreeCode ); } /**Function************************************************************* diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index 18a85a04..79d2b729 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool assert( Abc_NtkIsStrash(pNtk) ); // perform FPGA mapping - if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL ) + if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL ) return NULL; if ( fVerbose ) printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) ); diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c index 744169b5..ad43534d 100644 --- a/src/base/abci/abcEspresso.c +++ b/src/base/abci/abcEspresso.c @@ -54,7 +54,13 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose ) if ( Abc_NtkHasMapping(pNtk) ) Abc_NtkUnmap(pNtk); else if ( Abc_NtkHasBdd(pNtk) ) - Abc_NtkBddToSop(pNtk, 0); + { + if ( !Abc_NtkBddToSop(pNtk, 0) ) + { + printf( "Converting to SOPs has failed.\n" ); + return; + } + } // minimize SOPs of all nodes Abc_NtkForEachNode( pNtk, pNode, i ) if ( i ) Abc_NodeEspresso( pNode ); diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index 4aae6ba5..2f54dcee 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -684,7 +684,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) // set the number of networks stored Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 ); } - printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld ); +// printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld ); return 1; } diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c index b377da1d..a8e656ce 100644 --- a/src/base/abci/abcFxu.c +++ b/src/base/abci/abcFxu.c @@ -57,7 +57,13 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p ) if ( Abc_NtkIsMappedLogic(pNtk) ) Abc_NtkUnmap(pNtk); else if ( Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk, 0); + { + if ( !Abc_NtkBddToSop(pNtk, 0) ) + { + printf( "Converting to SOPs has failed.\n" ); + return 0; + } + } else { // to make sure the SOPs are SCC-free // Abc_NtkSopToBdd(pNtk); diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c new file mode 100644 index 00000000..626e5e1e --- /dev/null +++ b/src/base/abci/abcGen.c @@ -0,0 +1,261 @@ +/**CFile**************************************************************** + + FileName [abc_.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +void Abc_WriteLayer( FILE * pFile, int nVars, int fSkip1 ); +void Abc_WriteComp( FILE * pFile ); +void Abc_WriteFullAdder( FILE * pFile ); + +void Abc_GenAdder( char * pFileName, int nVars ); +void Abc_GenSorter( char * pFileName, int nVars ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_GenAdder( char * pFileName, int nVars ) +{ + FILE * pFile; + int i; + + assert( nVars > 0 ); + + pFile = fopen( pFileName, "w" ); + fprintf( pFile, "# %d-bit ripple-carry adder generated by ABC on %s\n", nVars, Extra_TimeStamp() ); + fprintf( pFile, ".model Adder%02d\n", nVars ); + + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nVars; i++ ) + fprintf( pFile, " a%02d", i ); + for ( i = 0; i < nVars; i++ ) + fprintf( pFile, " b%02d", i ); + fprintf( pFile, "\n" ); + + fprintf( pFile, ".outputs" ); + for ( i = 0; i <= nVars; i++ ) + fprintf( pFile, " y%02d", i ); + fprintf( pFile, "\n" ); + + fprintf( pFile, ".names c\n" ); + if ( nVars == 1 ) + fprintf( pFile, ".subckt FA a=a00 b=b00 cin=c s=y00 cout=y01\n" ); + else + { + fprintf( pFile, ".subckt FA a=a00 b=b00 cin=c s=y00 cout=%02d\n", 0 ); + for ( i = 1; i < nVars-1; i++ ) + fprintf( pFile, ".subckt FA a=a%02d b=b%02d cin=%02d s=y%02d cout=%02d\n", i, i, i-1, i, i ); + fprintf( pFile, ".subckt FA a=a%02d b=b%02d cin=%02d s=y%02d cout=y%02d\n", i, i, i-1, i, i+1 ); + } + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); + + Abc_WriteFullAdder( pFile ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_GenSorter( char * pFileName, int nVars ) +{ + FILE * pFile; + int i, k, Counter, nDigits; + + assert( nVars > 1 ); + + pFile = fopen( pFileName, "w" ); + fprintf( pFile, "# %d-bit sorter generated by ABC on %s\n", nVars, Extra_TimeStamp() ); + fprintf( pFile, ".model Sorter%02d\n", nVars ); + + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nVars; i++ ) + fprintf( pFile, " x%02d", i ); + fprintf( pFile, "\n" ); + + fprintf( pFile, ".outputs" ); + for ( i = 0; i < nVars; i++ ) + fprintf( pFile, " y%02d", i ); + fprintf( pFile, "\n" ); + + Counter = 0; + nDigits = Extra_Base10Log( (nVars-2)*nVars ); + if ( nVars == 2 ) + fprintf( pFile, ".subckt Comp a=x00 b=x01 x=y00 y=y01\n" ); + else + { + fprintf( pFile, ".subckt Layer0" ); + for ( k = 0; k < nVars; k++ ) + fprintf( pFile, " x%02d=x%02d", k, k ); + for ( k = 0; k < nVars; k++ ) + fprintf( pFile, " y%02d=%0*d", k, nDigits, Counter++ ); + fprintf( pFile, "\n" ); + Counter -= nVars; + for ( i = 1; i < nVars-2; i++ ) + { + fprintf( pFile, ".subckt Layer%d", (i&1) ); + for ( k = 0; k < nVars; k++ ) + fprintf( pFile, " x%02d=%0*d", k, nDigits, Counter++ ); + for ( k = 0; k < nVars; k++ ) + fprintf( pFile, " y%02d=%0*d", k, nDigits, Counter++ ); + fprintf( pFile, "\n" ); + Counter -= nVars; + } + fprintf( pFile, ".subckt Layer%d", (i&1) ); + for ( k = 0; k < nVars; k++ ) + fprintf( pFile, " x%02d=%0*d", k, nDigits, Counter++ ); + for ( k = 0; k < nVars; k++ ) + fprintf( pFile, " y%02d=y%02d", k, k ); + fprintf( pFile, "\n" ); + } + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); + + Abc_WriteLayer( pFile, nVars, 0 ); + Abc_WriteLayer( pFile, nVars, 1 ); + Abc_WriteComp( pFile ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_WriteLayer( FILE * pFile, int nVars, int fSkip1 ) +{ + int i; + fprintf( pFile, ".model Layer%d\n", fSkip1 ); + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nVars; i++ ) + fprintf( pFile, " x%02d", i ); + fprintf( pFile, "\n" ); + fprintf( pFile, ".outputs" ); + for ( i = 0; i < nVars; i++ ) + fprintf( pFile, " y%02d", i ); + fprintf( pFile, "\n" ); + if ( fSkip1 ) + { + fprintf( pFile, ".names x00 y00\n" ); + fprintf( pFile, "1 1\n" ); + i = 1; + } + else + i = 0; + for ( ; i + 1 < nVars; i += 2 ) + fprintf( pFile, ".subckt Comp a=x%02d b=x%02d x=y%02d y=y%02d\n", i, i+1, i, i+1 ); + if ( i < nVars ) + { + fprintf( pFile, ".names x%02d y%02d\n", i, i ); + fprintf( pFile, "1 1\n" ); + } + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_WriteComp( FILE * pFile ) +{ + fprintf( pFile, ".model Comp\n" ); + fprintf( pFile, ".inputs a b\n" ); + fprintf( pFile, ".outputs x y\n" ); + fprintf( pFile, ".names a b x\n" ); + fprintf( pFile, "11 1\n" ); + fprintf( pFile, ".names a b y\n" ); + fprintf( pFile, "1- 1\n" ); + fprintf( pFile, "-1 1\n" ); + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_WriteFullAdder( FILE * pFile ) +{ + fprintf( pFile, ".model FA\n" ); + fprintf( pFile, ".inputs a b cin\n" ); + fprintf( pFile, ".outputs s cout\n" ); + fprintf( pFile, ".names a b k\n" ); + fprintf( pFile, "10 1\n" ); + fprintf( pFile, "01 1\n" ); + fprintf( pFile, ".names k cin s\n" ); + fprintf( pFile, "10 1\n" ); + fprintf( pFile, "01 1\n" ); + fprintf( pFile, ".names a b cin cout\n" ); + fprintf( pFile, "11- 1\n" ); + fprintf( pFile, "1-1 1\n" ); + fprintf( pFile, "-11 1\n" ); + fprintf( pFile, ".end\n" ); + fprintf( pFile, "\n" ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index 25d9e30f..c579eb84 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -522,7 +522,11 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk ) // duplicate the network pNtkNew2 = Abc_NtkDup( pNtk ); pNtkNew = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1, 0 ); - Abc_NtkBddToSop( pNtkNew, 0 ); + if ( !Abc_NtkBddToSop( pNtkNew, 0 ) ) + { + printf( "Converting to SOPs has failed.\n" ); + return NULL; + } // set the old network to point to the new network Abc_NtkForEachCi( pNtk, pNode, i ) diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index c0658d5e..87ea57f3 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -282,7 +282,129 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt +/**Function************************************************************* + + Synopsis [Derives the AND of two miters.] + + Description [The network should have the same names of PIs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) +{ + char Buffer[100]; + Abc_Ntk_t * pNtkMiter; + Abc_Obj_t * pOutput1, * pOutput2; + Abc_Obj_t * pRoot1, * pRoot2, * pMiter; + + assert( Abc_NtkIsStrash(pNtk1) ); + assert( Abc_NtkIsStrash(pNtk2) ); + assert( 1 == Abc_NtkCoNum(pNtk1) ); + assert( 1 == Abc_NtkCoNum(pNtk2) ); + assert( 0 == Abc_NtkLatchNum(pNtk1) ); + assert( 0 == Abc_NtkLatchNum(pNtk2) ); + assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) ); + + // start the new network + pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); + sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName ); + pNtkMiter->pName = Extra_UtilStrsav(Buffer); + + // perform strashing + Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, 1 ); + Abc_NtkMiterAddOne( pNtk1, pNtkMiter ); + Abc_NtkMiterAddOne( pNtk2, pNtkMiter ); +// Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, 1 ); + pRoot1 = Abc_NtkPo(pNtk1,0); + pRoot2 = Abc_NtkPo(pNtk2,0); + pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot1)->pCopy, Abc_ObjFaninC0(pRoot1) ); + pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot2)->pCopy, Abc_ObjFaninC0(pRoot2) ); + + // create the miter of the two outputs + pMiter = Abc_AigAnd( pNtkMiter->pManFunc, pOutput1, pOutput2 ); + Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pMiter ); + + // make sure that everything is okay + if ( !Abc_NtkCheck( pNtkMiter ) ) + { + printf( "Abc_NtkMiterAnd: The network check has failed.\n" ); + Abc_NtkDelete( pNtkMiter ); + return NULL; + } + return pNtkMiter; +} + + +/**Function************************************************************* + + Synopsis [Derives the cofactor of the miter w.r.t. the set of vars.] + + Description [The array of variable values contains -1/0/1 for each PI. + -1 means this PI remains, 0/1 means this PI is set to 0/1.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues ) +{ + char Buffer[100]; + Abc_Ntk_t * pNtkMiter; + Abc_Obj_t * pRoot, * pOutput1; + int Value, i; + + assert( Abc_NtkIsStrash(pNtk) ); + assert( 1 == Abc_NtkCoNum(pNtk) ); + + // start the new network + pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); + sprintf( Buffer, "%s_miter", pNtk->pName ); + pNtkMiter->pName = Extra_UtilStrsav(Buffer); + + // get the root output + pRoot = Abc_NtkCo( pNtk, 0 ); + + // perform strashing + Abc_NtkMiterPrepare( pNtk, pNtk, pNtkMiter, 1 ); + // set the first cofactor + Vec_IntForEachEntry( vPiValues, Value, i ) + { + if ( Value == -1 ) + continue; + if ( Value == 0 ) + { + Abc_NtkCi(pNtk, i)->pCopy = Abc_ObjNot( Abc_NtkConst1(pNtkMiter) ); + continue; + } + if ( Value == 1 ) + { + Abc_NtkCi(pNtk, i)->pCopy = Abc_NtkConst1(pNtkMiter); + continue; + } + assert( 0 ); + } + // add the first cofactor + Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); + + // save the output + pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) ); + + // create the miter of the two outputs + Abc_ObjAddFanin( Abc_NtkPo(pNtkMiter,0), pOutput1 ); + // make sure that everything is okay + if ( !Abc_NtkCheck( pNtkMiter ) ) + { + printf( "Abc_NtkMiterCofactor: The network check has failed.\n" ); + Abc_NtkDelete( pNtkMiter ); + return NULL; + } + return pNtkMiter; +} /**Function************************************************************* Synopsis [Derives the miter of two cofactors of one output.] diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c index 209fc991..62ae51ed 100644 --- a/src/base/abci/abcNewAig.c +++ b/src/base/abci/abcNewAig.c @@ -65,7 +65,13 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ) assert( !Abc_NtkIsNetlist(pNtk) ); assert( !Abc_NtkIsSeq(pNtk) ); if ( Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk, 0); + { + if ( !Abc_NtkBddToSop(pNtk, 0) ) + { + printf( "Converting to SOPs has failed.\n" ); + return; + } + } // print warning about choice nodes if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index d92da31b..33f432f4 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -27,7 +27,7 @@ static void Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew ); static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew ); static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node ); -static DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax ); +static DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -243,15 +243,14 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * SeeAlso [] ***********************************************************************/ -DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly ) +DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly, int fReorder, int fVerbose ) { - int fReorder = 1; ProgressBar * pProgress; Vec_Ptr_t * vFuncsGlob; Abc_Obj_t * pNode; DdNode * bFunc; DdManager * dd; - int i; + int i, Counter; // start the manager assert( pNtk->pManGlob == NULL ); @@ -269,18 +268,20 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly // collect the global functions of the COs vFuncsGlob = Vec_PtrAlloc( 100 ); + Counter = 0; if ( fLatchOnly ) { // construct the BDDs - pProgress = Extra_ProgressBarStart( stdout, Abc_NtkLatchNum(pNtk) ); + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) ); Abc_NtkForEachLatch( pNtk, pNode, i ) { - Extra_ProgressBarUpdate( pProgress, i, NULL ); - bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax ); +// Extra_ProgressBarUpdate( pProgress, i, NULL ); + bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose ); if ( bFunc == NULL ) { + if ( fVerbose ) printf( "Constructing global BDDs is aborted.\n" ); - Extra_ProgressBarStop( pProgress ); + Vec_PtrFree( vFuncsGlob ); Cudd_Quit( dd ); return NULL; } @@ -292,15 +293,16 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly else { // construct the BDDs - pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); + pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) { - Extra_ProgressBarUpdate( pProgress, i, NULL ); - bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax ); +// Extra_ProgressBarUpdate( pProgress, i, NULL ); + bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose ); if ( bFunc == NULL ) { + if ( fVerbose ) printf( "Constructing global BDDs is aborted.\n" ); - Extra_ProgressBarStop( pProgress ); + Vec_PtrFree( vFuncsGlob ); Cudd_Quit( dd ); return NULL; } @@ -339,12 +341,14 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly SeeAlso [] ***********************************************************************/ -DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax ) +DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax, ProgressBar * pProgress, int * pCounter, int fVerbose ) { DdNode * bFunc, * bFunc0, * bFunc1; assert( !Abc_ObjIsComplement(pNode) ); if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax ) { + Extra_ProgressBarStop( pProgress ); + if ( fVerbose ) printf( "The number of live nodes reached %d.\n", nBddSizeMax ); fflush( stdout ); return NULL; @@ -353,11 +357,11 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize if ( pNode->pCopy ) return (DdNode *)pNode->pCopy; // compute the result for both branches - bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax ); + bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax, pProgress, pCounter, fVerbose ); if ( bFunc0 == NULL ) return NULL; Cudd_Ref( bFunc0 ); - bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax ); + bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax, pProgress, pCounter, fVerbose ); if ( bFunc1 == NULL ) return NULL; Cudd_Ref( bFunc1 ); @@ -370,6 +374,9 @@ DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSize // set the result assert( pNode->pCopy == NULL ); pNode->pCopy = (Abc_Obj_t *)bFunc; + // increment the progress bar + if ( pProgress ) + Extra_ProgressBarUpdate( pProgress, (*pCounter)++, NULL ); return bFunc; } @@ -427,7 +434,7 @@ double Abc_NtkSpacePercentage( Abc_Obj_t * pNode ) Vec_PtrForEachEntry( vNodes, pObj, i ) pObj->pCopy = (Abc_Obj_t *)dd->vars[i]; // build the BDD of the cone - bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000 ); Cudd_Ref( bFunc ); + bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000, NULL, NULL, 1 ); Cudd_Ref( bFunc ); bFunc = Cudd_NotCond( bFunc, pNode != pNodeR ); // count minterms Result = Cudd_CountMinterm( dd, bFunc, dd->size ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index d299a29d..56b70c5b 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -28,6 +28,9 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +//extern int s_TotalNodes = 0; +//extern int s_TotalChanges = 0; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -147,6 +150,11 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) fclose( pTable ); } */ +/* + s_TotalNodes += Abc_NtkNodeNum(pNtk); + printf( "Total nodes = %6d %6.2f Mb Changes = %6d.\n", + s_TotalNodes, s_TotalNodes * 20.0 / (1<<20), s_TotalChanges ); +*/ } /**Function************************************************************* @@ -644,7 +652,13 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary ) // transform logic functions from BDD to SOP if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk, 0); + { + if ( !Abc_NtkBddToSop(pNtk, 0) ) + { + printf( "Converting to SOPs has failed.\n" ); + return; + } + } // get hold of the SOP of the node CountConst = CountBuf = CountInv = CountAnd = CountOr = CountOther = CounterTotal = 0; diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index ae4bb250..c0e904bf 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -20,6 +20,7 @@ #include "abc.h" #include "fraig.h" +#include "math.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -32,10 +33,11 @@ extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails ); static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - + /**Function************************************************************* Synopsis [Attempts to solve the miter using a number of tricks.] @@ -50,106 +52,126 @@ static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fV SeeAlso [] ***********************************************************************/ -int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose ) +int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) { + Prove_Params_t * pParams = pPars; Abc_Ntk_t * pNtk, * pNtkTemp; - int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2; // was 5000 - int nConfs, nImps, nBTLimit, RetValue, nSatFails; - int nIter = 0, clk, timeStart = clock(); + int RetValue, nIter, Counter, clk, timeStart = clock(); // get the starting network pNtk = *ppNtk; assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkPoNum(pNtk) == 1 ); - // set the initial limits - nConfs = !nConfLimit? nConfsStart : ABC_MIN( nConfsStart, nConfLimit ); - nImps = !nImpLimit ? nImpsStart : ABC_MIN( nImpsStart , nImpLimit ); - nBTLimit = nBTLimitStart; - - if ( fVerbose ) - printf( "Global resource limits: ConfsLim = %6d. ImpsLim = %d.\n", nConfLimit, nImpLimit ); + if ( pParams->fVerbose ) + { + printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n", + pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" ); + printf( "Mitering = %d (%3.1f). Rewriting = %d (%3.1f). Fraiging = %d (%3.1f).\n", + pParams->nMiteringLimitStart, pParams->nMiteringLimitMulti, + pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti, + pParams->nFraigingLimitStart, pParams->nFraigingLimitMulti ); + printf( "Mitering last = %d.\n", + pParams->nMiteringLimitLast ); + } // if SAT only, solve without iteration - if ( !fUseRewrite && !fUseFraig ) + if ( !pParams->fUseRewriting && !pParams->fUseFraiging ) { clk = clock(); - RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 ); - Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose ); + RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 ); + Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); *ppNtk = pNtk; return RetValue; } // check the current resource limits - do { - nIter++; - - if ( fVerbose ) + for ( nIter = 0; nIter < pParams->nItersMax; nIter++ ) + { + if ( pParams->fVerbose ) { - printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter, nConfs, nBTLimit ); + printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, + (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), + (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) ); fflush( stdout ); } // try brute-force SAT clk = clock(); - RetValue = Abc_NtkMiterSat( pNtk, nConfs, nImps, 0 ); - Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose ); + RetValue = Abc_NtkMiterSat( pNtk, (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 0, 0, 0 ); + Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); if ( RetValue >= 0 ) break; - if ( fUseRewrite ) + // try rewriting + if ( pParams->fUseRewriting ) { clk = clock(); - - // try rewriting - Abc_NtkRewrite( pNtk, 0, 0, 0 ); - if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) - break; - Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); - if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) - break; - pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp ); - if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) - break; - - Abc_NtkMiterPrint( pNtk, "Rewriting ", clk, fVerbose ); + Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter)); + while ( 1 ) + { + Abc_NtkRewrite( pNtk, 0, 0, 0 ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + if ( --Counter == 0 ) + break; + Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + if ( --Counter == 0 ) + break; + pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + if ( --Counter == 0 ) + break; + } + Abc_NtkMiterPrint( pNtk, "Rewriting ", clk, pParams->fVerbose ); } - - if ( fUseFraig ) + + if ( pParams->fUseFraiging ) { + int nSatFails; // try FRAIGing clk = clock(); - pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue, &nSatFails ); Abc_NtkDelete( pNtkTemp ); - Abc_NtkMiterPrint( pNtk, "FRAIGing ", clk, fVerbose ); + pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), &RetValue, &nSatFails ); Abc_NtkDelete( pNtkTemp ); + Abc_NtkMiterPrint( pNtk, "FRAIGing ", clk, pParams->fVerbose ); // printf( "NumFails = %d\n", nSatFails ); if ( RetValue >= 0 ) break; } - else - nSatFails = 1000; - - // increase resource limits -// nConfs = ABC_MIN( nConfs * 3 / 2, 1000000000 ); // was 4/2 - nConfs = nSatFails * nBTLimit / 2; - nImps = ABC_MIN( nImps * 3 / 2, 1000000000 ); - nBTLimit = ABC_MIN( nBTLimit * 8, 1000000000 ); - - // timeout at 5 minutes -// if ( clock() - timeStart >= 1200 * CLOCKS_PER_SEC ) -// break; - if ( nIter == 7 ) - break; } -// while ( (nConfLimit == 0 || nConfs <= nConfLimit) && -// (nImpLimit == 0 || nImps <= nImpLimit ) ); - while ( 1 ); // try to prove it using brute force SAT + if ( RetValue < 0 && pParams->fUseBdds ) + { + if ( pParams->fVerbose ) + { + printf( "Attempting BDDs with node limit %d ...\n", pParams->nBddSizeLimit ); + fflush( stdout ); + } + clk = clock(); + pNtk = Abc_NtkCollapse( pNtkTemp = pNtk, pParams->nBddSizeLimit, 0, pParams->fBddReorder, 0 ); + if ( pNtk ) + { + Abc_NtkDelete( pNtkTemp ); + RetValue = ( (Abc_NtkNodeNum(pNtk) == 1) && (Abc_ObjFanin0(Abc_NtkPo(pNtk,0))->pData == Cudd_ReadLogicZero(pNtk->pManFunc)) ); + } + else + pNtk = pNtkTemp; + Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose ); + } + if ( RetValue < 0 ) { + if ( pParams->fVerbose ) + { + printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast ); + fflush( stdout ); + } clk = clock(); - RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 ); - Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose ); + RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 ); + Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); } // assign the model if it was proved by rewriting (const 1 miter) @@ -240,7 +262,8 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose { if ( !fVerbose ) return; - printf( "Nodes = %7d. Levels = %4d. ", Abc_NtkNodeNum(pNtk), Abc_AigGetLevelNum(pNtk) ); + printf( "Nodes = %7d. Levels = %4d. ", Abc_NtkNodeNum(pNtk), + Abc_NtkIsStrash(pNtk)? Abc_AigGetLevelNum(pNtk) : Abc_NtkGetLevelNum(pNtk) ); PRT( pString, clock() - clk ); } diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c index c968025f..9ea3ad71 100644 --- a/src/base/abci/abcRefactor.c +++ b/src/base/abci/abcRefactor.c @@ -132,6 +132,10 @@ clk = clock(); Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain ); pManRef->timeNtk += clock() - clk; Dec_GraphFree( pFForm ); +// { +// extern int s_TotalChanges; +// s_TotalChanges++; +// } } Extra_ProgressBarStop( pProgress ); pManRef->timeTotal = clock() - clkStart; diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c index 32e878b8..49208772 100644 --- a/src/base/abci/abcRestruct.c +++ b/src/base/abci/abcRestruct.c @@ -74,7 +74,7 @@ static Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, C static Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCut ); static Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, Abc_Obj_t * pRoot, int Required, int nNodesSaved, int * pnNodesAdded ); -static Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fMulti ); +static Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fDag ); static Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose ); static void Abc_NtkManRstStop( Abc_ManRst_t * p ); static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p ); @@ -145,7 +145,7 @@ pManRst->timeCut += clock() - clk; break; // get the cuts for the given node clk = clock(); - pCutList = Abc_NodeGetCutsRecursive( pManCut, pNode, fMulti ); + pCutList = Abc_NodeGetCutsRecursive( pManCut, pNode, fMulti, 0 ); pManRst->timeCut += clock() - clk; // perform restructuring @@ -203,7 +203,7 @@ pManRst->timeTotal = clock() - clkStart; ***********************************************************************/ void Abc_RestructNodeDivisors( Abc_ManRst_t * p, Abc_Obj_t * pRoot, int nNodesSaved ) { - Abc_Obj_t * pNode, * pFanin, * pFanout; + Abc_Obj_t * pNode, * pFanout;//, * pFanin; int i, k; // start with the leaves Vec_PtrClear( p->vDecs ); @@ -276,7 +276,7 @@ Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_ { Dec_Graph_t * pGraph; Cut_Cut_t * pCut; - int nCuts; +// int nCuts; p->nNodesConsidered++; /* // count the number of cuts with four inputs or more @@ -949,7 +949,7 @@ Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd SeeAlso [] ***********************************************************************/ -Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fMulti ) +Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fDag ) { static Cut_Params_t Params, * pParams = &Params; Cut_Man_t * pManCut; @@ -963,7 +963,8 @@ Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fM pParams->fFilter = 1; // filter dominated cuts pParams->fSeq = 0; // compute sequential cuts pParams->fDrop = 0; // drop cuts on the fly - pParams->fMulti = fMulti; // compute factor-cuts + pParams->fDag = fDag; // compute DAG cuts + pParams->fTree = 0; // compute tree cuts pParams->fVerbose = 0; // the verbosiness flag pParams->nIdsMax = Abc_NtkObjNumMax( pNtk ); pManCut = Cut_ManStart( pParams ); @@ -1351,9 +1352,9 @@ Dec_Graph_t * Abc_NodeMffcSingleNode( Abc_ManRst_t * p, Vec_Int_t * vSims, int n ***********************************************************************/ Dec_Graph_t * Abc_NodeMffcDoubleNode( Abc_ManRst_t * p, Vec_Int_t * vSims, int nNodes, Vec_Int_t * vOnes ) { - Dec_Graph_t * pGraph; - unsigned uRoot, uNode; - int i; +// Dec_Graph_t * pGraph; +// unsigned uRoot, uNode; +// int i; return NULL; diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 71a4466f..e9de4858 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -25,6 +25,9 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define ABC_RS_DIV1_MAX 150 // the max number of divisors to consider +#define ABC_RS_DIV2_MAX 500 // the max number of pair-wise divisors to consider + typedef struct Abc_ManRes_t_ Abc_ManRes_t; struct Abc_ManRes_t_ { @@ -79,6 +82,7 @@ struct Abc_ManRes_t_ int nUsedNodeTotal; int nTotalDivs; int nTotalLeaves; + int nTotalGain; }; // external procedures @@ -90,8 +94,8 @@ static void Abc_ManResubPrint( Abc_ManRes_t * p ); // other procedures static int Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required ); -static int Abc_ManResubMffc( Abc_ManRes_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves ); static void Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords ); +static void Abc_ManResubPrintDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ); static void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ); static void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ); @@ -136,13 +140,17 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd // cleanup the AIG Abc_AigCleanup(pNtk->pManFunc); // start the managers - pManCut = Abc_NtkManCutStart( nCutMax, 10000, 100000, 100000 ); - pManRes = Abc_ManResubStart( nCutMax, 200 ); + pManCut = Abc_NtkManCutStart( nCutMax, 100000, 100000, 100000 ); + pManRes = Abc_ManResubStart( nCutMax, ABC_RS_DIV1_MAX ); // compute the reverse levels if level update is requested if ( fUpdateLevel ) Abc_NtkStartReverseLevels( pNtk ); + if ( Abc_NtkLatchNum(pNtk) ) + Abc_NtkForEachLatch(pNtk, pNode, i) + pNode->pNext = pNode->pData; + // resynthesize each node once nNodes = Abc_NtkObjNumMax(pNtk); pProgress = Extra_ProgressBarStart( stdout, nNodes ); @@ -179,13 +187,16 @@ clk = clock(); pManRes->timeRes += clock() - clk; if ( pFForm == NULL ) continue; + pManRes->nTotalGain += pManRes->nLastGain; /* - if ( pNode->Id % 25 == 0 ) + if ( pManRes->nLeaves == 4 && pManRes->nMffc == 2 && pManRes->nLastGain == 1 ) + { printf( "%6d : L = %2d. V = %2d. Mffc = %2d. Divs = %3d. Up = %3d. Un = %3d. B = %3d.\n", pNode->Id, pManRes->nLeaves, Abc_CutVolumeCheck(pNode, vLeaves), pManRes->nMffc, pManRes->nDivs, pManRes->vDivs1UP->nSize, pManRes->vDivs1UN->nSize, pManRes->vDivs1B->nSize ); + Abc_ManResubPrintDivs( pManRes, pNode, vLeaves ); + } */ - // acceptable replacement found, update the graph clk = clock(); Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRes->nLastGain ); @@ -207,6 +218,10 @@ pManRes->timeTotal = clock() - clkStart; Abc_NtkForEachObj( pNtk, pNode, i ) pNode->pData = NULL; + if ( Abc_NtkLatchNum(pNtk) ) + Abc_NtkForEachLatch(pNtk, pNode, i) + pNode->pData = pNode->pNext, pNode->pNext = NULL; + // put the nodes into the DFS order and reassign their IDs Abc_NtkReassignIds( pNtk ); // Abc_AigCheckFaninOrder( pNtk->pManFunc ); @@ -340,6 +355,7 @@ void Abc_ManResubPrint( Abc_ManRes_t * p ) ); PRT( "TOTAL ", p->timeTotal ); printf( "Total leaves = %8d.\n", p->nTotalLeaves ); printf( "Total divisors = %8d.\n", p->nTotalDivs ); + printf( "Total gain = %8d.\n", p->nTotalGain ); } @@ -382,7 +398,7 @@ void Abc_ManResubCollectDivs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vInternal ) ***********************************************************************/ int Abc_ManResubCollectDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int Required ) { - Abc_Obj_t * pNode, * pFanout;//, * pFanin; + Abc_Obj_t * pNode, * pFanout; int i, k, Limit, Counter; Vec_PtrClear( p->vDivs1UP ); @@ -451,10 +467,24 @@ Quits : assert( pRoot == Vec_PtrEntryLast(p->vDivs) ); assert( Vec_PtrSize(p->vDivs) - Vec_PtrSize(vLeaves) <= Vec_PtrSize(p->vSims) - p->nLeavesMax ); + return 1; +} -/* -if (pRoot->Id == 15281 ) +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ManResubPrintDivs( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves ) { + Abc_Obj_t * pFanin, * pNode; + int i, k; // print the nodes Vec_PtrForEachEntry( p->vDivs, pNode, i ) { @@ -488,59 +518,7 @@ if (pRoot->Id == 15281 ) } printf( "\n" ); } -*/ - return 1; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_ManResubMffc( Abc_ManRes_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves ) -{ - Abc_Obj_t * pObj; - int Counter, i, k; - // increment the traversal ID for the leaves - // increment the fanout counters of the leaves - Abc_NtkIncrementTravId( pRoot->pNtk ); - Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves ) - { - pObj->vFanouts.nSize++; - Abc_NodeSetTravIdCurrent( pObj ); - } - // make sure the node is in the cone and is no one of the leaves - assert( Abc_NodeIsTravIdPrevious(pRoot) ); - Counter = Abc_NodeMffcLabel( pRoot ); - // remove the extra counters - Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves ) - pObj->vFanouts.nSize--; - - // sort the nodes by level!!! - - // move the labeled nodes to the end - Vec_PtrClear( p->vTemp ); - k = nLeaves; - Vec_PtrForEachEntryStart( vDivs, pObj, i, nLeaves ) - if ( Abc_NodeIsTravIdCurrent(pObj) ) - Vec_PtrPush( p->vTemp, pObj ); - else - Vec_PtrWriteEntry( vDivs, k++, pObj ); - // add the labeled nodes - Vec_PtrForEachEntry( p->vTemp, pObj, i ) - Vec_PtrWriteEntry( vDivs, k++, pObj ); - assert( k == Vec_PtrSize(p->vDivs) ); - assert( pRoot == Vec_PtrEntryLast(p->vDivs) ); - return Counter; -} /**Function************************************************************* @@ -928,7 +906,7 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) puData1 = pObj1->pData; - if ( Vec_PtrSize(p->vDivs2UP0) < 500 ) + if ( Vec_PtrSize(p->vDivs2UP0) < ABC_RS_DIV2_MAX ) { // get positive unate divisors for ( w = 0; w < p->nWords; w++ ) @@ -965,7 +943,7 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) } } - if ( Vec_PtrSize(p->vDivs2UN0) < 500 ) + if ( Vec_PtrSize(p->vDivs2UN0) < ABC_RS_DIV2_MAX ) { // get negative unate divisors for ( w = 0; w < p->nWords; w++ ) diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index f3360421..f11e5e9d 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -110,6 +110,10 @@ clk = clock(); Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain ); Rwr_ManAddTimeUpdate( pManRwr, clock() - clk ); if ( fCompl ) Dec_GraphComplement( pGraph ); +// { +// extern int s_TotalChanges; +// s_TotalChanges++; +// } } } Extra_ProgressBarStop( pProgress ); diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c new file mode 100644 index 00000000..3a6a29c9 --- /dev/null +++ b/src/base/abci/abcRr.c @@ -0,0 +1,601 @@ +/**CFile**************************************************************** + + FileName [abcRr.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Redundancy removal.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcRr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "fraig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Abc_RRMan_t_ Abc_RRMan_t; +struct Abc_RRMan_t_ +{ + // the parameters + Abc_Ntk_t * pNtk; // the network + int nFaninLevels; // the number of fanin levels + int nFanoutLevels; // the number of fanout levels + // the node/fanin/fanout + Abc_Obj_t * pNode; // the node + Abc_Obj_t * pFanin; // the fanin + Abc_Obj_t * pFanout; // the fanout + // the intermediate cones + Vec_Ptr_t * vFaninLeaves; // the leaves of the fanin cone + Vec_Ptr_t * vFanoutRoots; // the roots of the fanout cone + // the window + Vec_Ptr_t * vLeaves; // the leaves of the window + Vec_Ptr_t * vCone; // the internal nodes of the window + Vec_Ptr_t * vRoots; // the roots of the window + Abc_Ntk_t * pWnd; // the window derived for the edge + // the miter + Abc_Ntk_t * pMiter; // the miter derived from the window + Prove_Params_t * pParams; // the miter proving parameters +}; + +static Abc_RRMan_t * Abc_RRManStart(); +static void Abc_RRManStop( Abc_RRMan_t * p ); +static void Abc_RRManClean( Abc_RRMan_t * p ); +static int Abc_NtkRRProve( Abc_RRMan_t * p ); +static int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Abc_Obj_t * pFanout ); +static int Abc_NtkRRWindow( Abc_RRMan_t * p ); + +static int Abc_NtkRRTfi_int( Vec_Ptr_t * vFaninLeaves, int LevelLimit ); +static int Abc_NtkRRTfo_int( Vec_Ptr_t * vFanoutRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout ); +static int Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit ); +static void Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ); +static Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vRoots ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Removes stuck-at redundancies.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFanouts, int fVerbose ) +{ + ProgressBar * pProgress; + Abc_RRMan_t * p; + Abc_Obj_t * pNode, * pFanin, * pFanout; + int i, k, m, nNodes; + // start the manager + p = Abc_RRManStart( nFaninLevels, nFanoutLevels ); + p->pNtk = pNtk; + p->nFaninLevels = nFaninLevels; + p->nFanoutLevels = nFanoutLevels; + // go through the nodes + nNodes = Abc_NtkObjNumMax(pNtk); + pProgress = Extra_ProgressBarStart( stdout, nNodes ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // stop if all nodes have been tried once + if ( i >= nNodes ) + break; + // skip the constant node + if ( Abc_NodeIsConst(pNode) ) + continue; + // skip the nodes with many fanouts + if ( Abc_ObjFanoutNum(pNode) > 1000 ) + continue; + // construct the window + if ( !fUseFanouts ) + { + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + Abc_RRManClean( p ); + p->pNode = pNode; + p->pFanin = pFanin; + p->pFanout = NULL; + if ( !Abc_NtkRRWindow( p ) ) + continue; + if ( !Abc_NtkRRProve( p ) ) + continue; + Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout ); + break; + } + continue; + } + // use the fanouts + Abc_ObjForEachFanout( pNode, pFanout, m ) + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + Abc_RRManClean( p ); + p->pNode = pNode; + p->pFanin = pFanin; + p->pFanout = pFanout; + if ( !Abc_NtkRRWindow( p ) ) + continue; + if ( !Abc_NtkRRProve( p ) ) + continue; + Abc_NtkRRUpdate( pNtk, p->pNode, p->pFanin, p->pFanout ); + break; + } + } + Extra_ProgressBarStop( pProgress ); + Abc_RRManStop( p ); + // put the nodes into the DFS order and reassign their IDs + Abc_NtkReassignIds( pNtk ); + Abc_NtkGetLevelNum( pNtk ); + // check + if ( !Abc_NtkCheck( pNtk ) ) + { + printf( "Abc_NtkRR: The network check has failed.\n" ); + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Start the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_RRMan_t * Abc_RRManStart() +{ + Abc_RRMan_t * p; + p = ALLOC( Abc_RRMan_t, 1 ); + memset( p, 0, sizeof(Abc_RRMan_t) ); + p->vFaninLeaves = Vec_PtrAlloc( 100 ); // the leaves of the fanin cone + p->vFanoutRoots = Vec_PtrAlloc( 100 ); // the roots of the fanout cone + p->vLeaves = Vec_PtrAlloc( 100 ); // the leaves of the window + p->vCone = Vec_PtrAlloc( 100 ); // the internal nodes of the window + p->vRoots = Vec_PtrAlloc( 100 ); // the roots of the window + p->pParams = ALLOC( Prove_Params_t, 1 ); + memset( p->pParams, 0, sizeof(Prove_Params_t) ); + Prove_ParamsSetDefault( p->pParams ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stop the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_RRManStop( Abc_RRMan_t * p ) +{ + Abc_RRManClean( p ); + Vec_PtrFree( p->vFaninLeaves ); + Vec_PtrFree( p->vFanoutRoots ); + Vec_PtrFree( p->vLeaves ); + Vec_PtrFree( p->vCone ); + Vec_PtrFree( p->vRoots ); + free( p->pParams ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Clean the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_RRManClean( Abc_RRMan_t * p ) +{ + p->pNode = NULL; + p->pFanin = NULL; + p->pFanout = NULL; + Vec_PtrClear( p->vFaninLeaves ); + Vec_PtrClear( p->vFanoutRoots ); + Vec_PtrClear( p->vLeaves ); + Vec_PtrClear( p->vCone ); + Vec_PtrClear( p->vRoots ); + if ( p->pWnd ) Abc_NtkDelete( p->pWnd ); + if ( p->pMiter ) Abc_NtkDelete( p->pMiter ); + p->pWnd = NULL; + p->pMiter = NULL; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the miter is constant 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRRProve( Abc_RRMan_t * p ) +{ + Abc_Ntk_t * pWndCopy; + int RetValue; + pWndCopy = Abc_NtkDup( p->pWnd ); + Abc_NtkRRUpdate( pWndCopy, p->pNode->pCopy, p->pFanin->pCopy, p->pFanout? p->pFanout->pCopy : NULL ); + p->pMiter = Abc_NtkMiter( p->pWnd, pWndCopy, 1 ); + RetValue = Abc_NtkMiterProve( &p->pMiter, p->pParams ); + if ( RetValue == 1 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Updates the network after redundancy removal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Abc_Obj_t * pFanout ) +{ + Abc_Obj_t * pNodeNew, * pFanoutNew; + assert( pFanout == NULL ); + assert( !Abc_ObjIsComplement(pNode) ); + assert( !Abc_ObjIsComplement(pFanin) ); + assert( !Abc_ObjIsComplement(pFanout) ); + // find the node after redundancy removal + if ( pFanin == Abc_ObjFanin0(pNode) ) + pNodeNew = Abc_ObjChild1(pNode); + else if ( pFanin == Abc_ObjFanin1(pNode) ) + pNodeNew = Abc_ObjChild0(pNode); + else assert( 0 ); + // replace + if ( pFanout == NULL ) + { + Abc_AigReplace( pNtk->pManFunc, pNode, pNodeNew, 0 ); + return 1; + } + // find the fanout after redundancy removal + if ( pNode == Abc_ObjFanin0(pFanout) ) + pFanoutNew = Abc_AigAnd( pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC0(pFanout)), Abc_ObjChild1(pFanout) ); + else if ( pNode == Abc_ObjFanin1(pFanout) ) + pFanoutNew = Abc_AigAnd( pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC1(pFanout)), Abc_ObjChild0(pFanout) ); + else assert( 0 ); + // replace + Abc_AigReplace( pNtk->pManFunc, pFanout, pFanoutNew, 0 ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Constructs window for checking RR.] + + Description [If the window (p->pWnd) with the given scope (p->nFaninLevels, + p->nFanoutLevels) cannot be constructed, returns 0. Otherwise, returns 1. + The levels are measured from the fanin node (pFanin) and the fanout node + (pEdgeFanout), respectively.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRRWindow( Abc_RRMan_t * p ) +{ + Abc_Obj_t * pObj, * pFanout, * pEdgeFanin, * pEdgeFanout; + int i, k; + + // get the edge + pEdgeFanout = p->pFanout? p->pFanout : p->pNode; + pEdgeFanin = p->pFanout? p->pNode : p->pFanin; + + // start the TFI leaves with the fanin + Abc_NtkIncrementTravId( p->pNtk ); + Abc_NodeSetTravIdCurrent( p->pFanin ); + Vec_PtrPush( p->vFaninLeaves, p->pFanin ); + // mark the TFI cone and collect the leaves down to the given level + while ( Abc_NtkRRTfi_int(p->vFaninLeaves, p->pFanin->Level - p->nFaninLevels) ); + + // collect the TFO cone of the leaves + Abc_NtkIncrementTravId( p->pNtk ); + Vec_PtrForEachEntry( p->vFaninLeaves, pObj, i ) + { + Abc_ObjForEachFanout( pObj, pFanout, k ) + { + if ( !Abc_ObjIsNode(pFanout) ) + continue; + if ( pFanout->Level > pEdgeFanout->Level + p->nFanoutLevels ) + continue; + if ( Abc_NodeIsTravIdCurrent(pFanout) ) + continue; + Abc_NodeSetTravIdCurrent( pFanout ); + Vec_PtrPush( p->vFanoutRoots, pFanout ); + } + } + // mark the TFO cone and collect the leaves up to the given level (while skipping the edge) + while ( Abc_NtkRRTfo_int(p->vFanoutRoots, pEdgeFanout->Level + p->nFanoutLevels, pEdgeFanin, pEdgeFanout) ); + // unmark the nodes + Vec_PtrForEachEntry( p->vFanoutRoots, pObj, i ) + pObj->fMarkA = 0; + + // mark the current roots + Abc_NtkIncrementTravId( p->pNtk ); + Vec_PtrForEachEntry( p->vFanoutRoots, pObj, i ) + Abc_NodeSetTravIdCurrent( pObj ); + // collect roots reachable from the fanout (p->vRoots) + if ( !Abc_NtkRRTfo_rec( pEdgeFanout, p->vRoots, pEdgeFanout->Level + p->nFanoutLevels + 5 ) ) + return 0; + + // collect the DFS-ordered new cone (p->vCone) and new leaves (p->vLeaves) + // using the previous marks coming from the TFO cone + Vec_PtrForEachEntry( p->vRoots, pObj, i ) + Abc_NtkRRTfi_rec( pObj, p->vLeaves, p->vCone ); + // unmark the nodes + Vec_PtrForEachEntry( p->vCone, pObj, i ) + pObj->fMarkA = 0; + Vec_PtrForEachEntry( p->vLeaves, pObj, i ) + pObj->fMarkA = 0; + + // create a new network + p->pWnd = Abc_NtkWindow( p->pNtk, p->vLeaves, p->vCone, p->vRoots ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Marks the nodes in the TFI and collects their leaves.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRRTfi_int( Vec_Ptr_t * vFaninLeaves, int LevelLimit ) +{ + Abc_Obj_t * pObj, * pNext; + int i, k, LevelMax, nSize; + // find the maximum level of leaves + LevelMax = 0; + Vec_PtrForEachEntry( vFaninLeaves, pObj, i ) + if ( LevelMax < (int)pObj->Level ) + LevelMax = pObj->Level; + // if the nodes are all PIs, LevelMax == 0 + if ( LevelMax == 0 || LevelMax <= LevelLimit ) + return 0; + // expand the nodes with the minimum level + nSize = Vec_PtrSize(vFaninLeaves); + Vec_PtrForEachEntryStop( vFaninLeaves, pObj, i, nSize ) + { + if ( LevelMax != (int)pObj->Level ) + continue; + Abc_ObjForEachFanin( pObj, pNext, k ) + { + if ( Abc_NodeIsTravIdCurrent(pNext) ) + continue; + Abc_NodeSetTravIdCurrent( pNext ); + Vec_PtrPush( vFaninLeaves, pNext ); + } + } + // remove old nodes (cannot remove a PI) + k = 0; + Vec_PtrForEachEntry( vFaninLeaves, pObj, i ) + { + if ( LevelMax == (int)pObj->Level ) + continue; + Vec_PtrWriteEntry( vFaninLeaves, k++, pObj ); + } + Vec_PtrShrink( vFaninLeaves, k ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Marks the nodes in the TFO and collects their roots.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRRTfo_int( Vec_Ptr_t * vFanoutRoots, int LevelLimit, Abc_Obj_t * pEdgeFanin, Abc_Obj_t * pEdgeFanout ) +{ + Abc_Obj_t * pObj, * pNext; + int i, k, LevelMin, nSize; + // find the minimum level of roots + LevelMin = ABC_INFINITY; + Vec_PtrForEachEntry( vFanoutRoots, pObj, i ) + if ( Abc_ObjIsNode(pObj) && !pObj->fMarkA && LevelMin > (int)pObj->Level ) + LevelMin = pObj->Level; + // if the nodes are all POs, LevelMin == ABC_INFINITY + if ( LevelMin == ABC_INFINITY || LevelMin > LevelLimit ) + return 0; + // expand the nodes with the minimum level + nSize = Vec_PtrSize(vFanoutRoots); + Vec_PtrForEachEntryStop( vFanoutRoots, pObj, i, nSize ) + { + if ( LevelMin != (int)pObj->Level ) + continue; + Abc_ObjForEachFanout( pObj, pNext, k ) + { + if ( !Abc_ObjIsNode(pNext) || pNext->Level > (unsigned)LevelLimit ) + { + pObj->fMarkA = 1; + continue; + } + if ( pObj == pEdgeFanin && pNext == pEdgeFanout ) + continue; + if ( Abc_NodeIsTravIdCurrent(pNext) ) + continue; + Abc_NodeSetTravIdCurrent( pNext ); + Vec_PtrPush( vFanoutRoots, pNext ); + } + } + // remove old nodes + k = 0; + Vec_PtrForEachEntry( vFanoutRoots, pObj, i ) + { + if ( LevelMin == (int)pObj->Level ) + { + // check if the node has external fanouts + Abc_ObjForEachFanout( pObj, pNext, k ) + { + if ( pObj == pEdgeFanin && pNext == pEdgeFanout ) + continue; + if ( !Abc_NodeIsTravIdCurrent(pNext) ) + break; + } + // if external fanout is found, do not remove the node + if ( pNext ) + continue; + } + Vec_PtrWriteEntry( vFanoutRoots, k++, pObj ); + } + Vec_PtrShrink( vFanoutRoots, k ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Collects the roots in the TFO of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRRTfo_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vRoots, int LevelLimit ) +{ + Abc_Obj_t * pFanout; + int i; + if ( Abc_ObjIsCo(pNode) || pNode->Level > (unsigned)LevelLimit ) + return 0; + if ( Abc_NodeIsTravIdCurrent(pNode) ) + { + Vec_PtrPushUnique( vRoots, pNode ); + return 1; + } + Abc_NodeSetTravIdCurrent( pNode ); + Abc_ObjForEachFanout( pNode, pFanout, i ) + if ( !Abc_NtkRRTfo_rec( pFanout, vRoots, LevelLimit ) ) + return 0; + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRRTfi_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ) +{ + Abc_Obj_t * pFanin; + int i; + // skip visited nodes + if ( pNode->fMarkA ) + return; + pNode->fMarkA = 1; + // add the node if it was not visited in the previus run + if ( !Abc_NodeIsTravIdPrevious(pNode) ) + { + Vec_PtrPush( vLeaves, pNode ); + return; + } + Abc_ObjForEachFanin( pNode, pFanin, i ) + Abc_NtkRRTfi_rec( pFanin, vLeaves, vCone ); + Vec_PtrPush( vCone, pNode ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Vec_Ptr_t * vRoots ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj; + int i; + assert( Abc_NtkIsStrash(pNtk) ); + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); + // duplicate the name and the spec + pNtkNew->pName = Extra_UtilStrsav( "temp" ); + // map the constant nodes + if ( Abc_NtkConst1(pNtk) ) + Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + // create and map the PIs + Vec_PtrForEachEntry( vLeaves, pObj, i ) + pObj->pCopy = Abc_NtkCreatePi(pNtkNew); + // copy the AND gates + Vec_PtrForEachEntry( vCone, pObj, i ) + pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + // compare the number of nodes before and after + if ( Vec_PtrSize(vCone) != Abc_NtkNodeNum(pNtkNew) ) + printf( "Warning: Structural hashing during windowing reduced %d nodes (this is a bug).\n", + Vec_PtrSize(vCone) - Abc_NtkNodeNum(pNtkNew) ); + // create the POs + Vec_PtrForEachEntry( vRoots, pObj, i ) + Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pObj->pCopy ); + // add the PI/PO names + Abc_NtkAddDummyPiNames( pNtkNew ); + Abc_NtkAddDummyPoNames( pNtkNew ); + // check + if ( !Abc_NtkCheck( pNtkNew ) ) + { + printf( "Abc_NtkWindow: The network check has failed.\n" ); + return NULL; + } + return pNtkNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index f7400313..9348231b 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -24,7 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ); +extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ); static nMuxes; //////////////////////////////////////////////////////////////////////// @@ -42,7 +42,7 @@ static nMuxes; SeeAlso [] ***********************************************************************/ -int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose ) +int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFront, int fVerbose ) { solver * pSat; lbool status; @@ -56,7 +56,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbo // load clauses into the solver clk = clock(); - pSat = Abc_NtkMiterSatCreate( pNtk ); + pSat = Abc_NtkMiterSatCreate( pNtk, fJFront ); if ( pSat == NULL ) return 1; // printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); @@ -107,6 +107,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbo Vec_IntFree( vCiIds ); } // free the solver + if ( fVerbose ) + Asat_SatPrintStats( stdout, pSat ); solver_delete( pSat ); return RetValue; } @@ -391,12 +393,14 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo SeeAlso [] ***********************************************************************/ -int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk ) +int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront ) { Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE; Vec_Ptr_t * vNodes, * vSuper; - Vec_Int_t * vVars; + Vec_Int_t * vVars, * vFanio; + Vec_Vec_t * vCircuit; int i, k, fUseMuxes = 1; + int clk1 = clock(), clk; assert( Abc_NtkIsStrash(pNtk) ); @@ -408,6 +412,9 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk ) vNodes = Vec_PtrAlloc( 1000 ); // the nodes corresponding to vars in the solver vSuper = Vec_PtrAlloc( 100 ); // the nodes belonging to the given implication supergate vVars = Vec_IntAlloc( 100 ); // the temporary array for variables in the clause + if ( fJFront ) + vCircuit = Vec_VecAlloc( 1000 ); +// vCircuit = Vec_VecStart( 184 ); // add the clause for the constant node pNode = Abc_NtkConst1(pNtk); @@ -485,6 +492,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk ) if ( vSuper->nSize == 0 ) { if ( !Abc_NtkClauseTriv( pSat, Abc_ObjNot(pNode), vVars ) ) +// if ( !Abc_NtkClauseTriv( pSat, pNode, vVars ) ) return 0; } else @@ -493,6 +501,32 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk ) return 0; } } + // add the variables to the J-frontier + if ( !fJFront ) + continue; + // make sure that the fanin entries go first + assert( pNode->pCopy ); + Vec_VecExpand( vCircuit, (int)pNode->pCopy ); + vFanio = Vec_VecEntry( vCircuit, (int)pNode->pCopy ); + Vec_PtrForEachEntryReverse( vSuper, pFanin, k ) +// Vec_PtrForEachEntry( vSuper, pFanin, k ) + { + pFanin = Abc_ObjRegular( pFanin ); + assert( pFanin->pCopy && pFanin->pCopy != pNode->pCopy ); + Vec_IntPushFirst( vFanio, (int)pFanin->pCopy ); + Vec_VecPush( vCircuit, (int)pFanin->pCopy, pNode->pCopy ); + } + } + + // create the variable order + if ( fJFront ) + { + clk = clock(); + Asat_JManStart( pSat, vCircuit ); + Vec_VecFree( vCircuit ); + PRT( "Setup", clock() - clk ); +// Asat_JManStop( pSat ); +// PRT( "Total", clock() - clk1 ); } // delete @@ -513,7 +547,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) +solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront ) { solver * pSat; Abc_Obj_t * pNode; @@ -522,7 +556,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) nMuxes = 0; pSat = solver_new(); - RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk ); + RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk, fJFront ); Abc_NtkForEachObj( pNtk, pNode, i ) pNode->fMarkA = 0; // Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index fbaca324..cfbd4694 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -58,7 +58,13 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) assert( !Abc_NtkIsNetlist(pNtk) ); assert( !Abc_NtkIsSeq(pNtk) ); if ( Abc_NtkIsBddLogic(pNtk) ) - Abc_NtkBddToSop(pNtk, 0); + { + if ( !Abc_NtkBddToSop(pNtk, 0) ) + { + printf( "Converting to SOPs has failed.\n" ); + return NULL; + } + } // print warning about choice nodes if ( Abc_NtkGetChoiceNum( pNtk ) ) printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" ); @@ -72,7 +78,9 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup ) // if ( Abc_NtkCountSelfFeedLatches(pNtkAig) ) // printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) ); if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) - printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes ); + { +// printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes ); + } // duplicate EXDC if ( pNtk->pExdc ) pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); @@ -108,7 +116,13 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) assert( Abc_NtkIsStrash(pNtk1) ); assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); if ( Abc_NtkIsBddLogic(pNtk2) ) - Abc_NtkBddToSop(pNtk2, 0); + { + if ( !Abc_NtkBddToSop(pNtk2, 0) ) + { + printf( "Converting to SOPs has failed.\n" ); + return 0; + } + } // check that the networks have the same PIs // reorder PIs of pNtk2 according to pNtk1 if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1 ) ) @@ -163,6 +177,7 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fAllNodes assert( pObj->pCopy == NULL ); // mark the old object with the new AIG node pObj->pCopy = pNodeNew; + Abc_HManAddProto( pObj->pCopy, pObj ); } Vec_PtrFree( vNodes ); Extra_ProgressBarStop( pProgress ); diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c index 35cf896f..fad3bd92 100644 --- a/src/base/abci/abcSymm.c +++ b/src/base/abci/abcSymm.c @@ -88,7 +88,7 @@ void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose ) // compute the global functions clk = clock(); - dd = Abc_NtkGlobalBdds( pNtk, 10000000, 0 ); + dd = Abc_NtkGlobalBdds( pNtk, 10000000, 0, 1, fVerbose ); Cudd_AutodynDisable( dd ); Cudd_zddVarsFromBddVars( dd, 2 ); clkBdd = clock() - clk; diff --git a/src/base/abci/abcTrace.c b/src/base/abci/abcTrace.c new file mode 100644 index 00000000..0275c0a1 --- /dev/null +++ b/src/base/abci/abcTrace.c @@ -0,0 +1,804 @@ +/**CFile**************************************************************** + + FileName [abcHistory.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcHistory.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define ABC_SIM_VARS 16 // the max number of variables in the cone +#define ABC_SIM_OBJS 200 // the max number of objects in the cone + +typedef struct Abc_HMan_t_ Abc_HMan_t; +typedef struct Abc_HObj_t_ Abc_HObj_t; +typedef struct Abc_HNum_t_ Abc_HNum_t; + +struct Abc_HNum_t_ +{ + unsigned fCompl : 1; // set to 1 if the node is complemented + unsigned NtkId : 6; // the network ID + unsigned ObjId : 24; // the node ID +}; + +struct Abc_HObj_t_ +{ + // object info + unsigned fProof : 1; // set to 1 if the node is proved + unsigned fPhase : 1; // set to 1 if the node's phase differs from Old + unsigned fPi : 1; // the node is a PI + unsigned fPo : 1; // the node is a PO + unsigned fConst : 1; // the node is a constant + unsigned fVisited: 1; // the flag shows if the node is visited + unsigned NtkId : 10; // the network ID + unsigned Num : 16; // a temporary number + // history record + Abc_HNum_t Fan0; // immediate fanin + Abc_HNum_t Fan1; // immediate fanin + Abc_HNum_t Proto; // old node if present +// Abc_HNum_t Equ; // equiv node if present +}; + +struct Abc_HMan_t_ +{ + // storage for history information + Vec_Vec_t * vNtks; // the history nodes belonging to each network + Vec_Int_t * vProof; // flags showing if the network is proved + // storage for simulation info + int nVarsMax; // the max number of cone leaves + int nObjsMax; // the max number of cone nodes + Vec_Ptr_t * vObjs; // the cone nodes + int nBits; // the number of simulation bits + int nWords; // the number of unsigneds for siminfo + int nWordsCur; // the current number of words + Vec_Ptr_t * vSims; // simulation info + unsigned * pInfo; // pointer to simulation info + // other info + Vec_Ptr_t * vCone0; + Vec_Ptr_t * vCone1; + // memory manager + Extra_MmFixed_t* pMmObj; // memory manager for objects +}; + +static Abc_HMan_t * s_pHMan = NULL; + +static inline int Abc_HObjProof( Abc_HObj_t * p ) { return p->fProof; } +static inline int Abc_HObjPhase( Abc_HObj_t * p ) { return p->fPhase; } +static inline int Abc_HObjPi ( Abc_HObj_t * p ) { return p->fPi; } +static inline int Abc_HObjPo ( Abc_HObj_t * p ) { return p->fPo; } +static inline int Abc_HObjConst( Abc_HObj_t * p ) { return p->fConst; } +static inline int Abc_HObjNtkId( Abc_HObj_t * p ) { return p->NtkId; } +static inline int Abc_HObjNum ( Abc_HObj_t * p ) { return p->Num; } +static inline Abc_HObj_t * Abc_HObjFanin0( Abc_HObj_t * p ) { return !p->Fan0.NtkId ? NULL : Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->Fan0.NtkId), p->Fan0.ObjId ); } +static inline Abc_HObj_t * Abc_HObjFanin1( Abc_HObj_t * p ) { return !p->Fan1.NtkId ? NULL : Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->Fan1.NtkId), p->Fan1.ObjId ); } +static inline Abc_HObj_t * Abc_HObjProto ( Abc_HObj_t * p ) { return !p->Proto.NtkId ? NULL : Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->Proto.NtkId), p->Proto.ObjId ); } +static inline int Abc_HObjFaninC0( Abc_HObj_t * p ) { return p->Fan0.fCompl; } +static inline int Abc_HObjFaninC1( Abc_HObj_t * p ) { return p->Fan1.fCompl; } + +static inline Abc_HObj_t * Abc_ObjHObj( Abc_Obj_t * p ) { return Vec_PtrEntry( Vec_VecEntry(s_pHMan->vNtks, p->pNtk->Id), p->Id ); } + +static int Abc_HManVerifyPair( int NtkIdOld, int NtkIdNew ); +static int Abc_HManVerifyNodes_rec( Abc_HObj_t * pHOld, Abc_HObj_t * pHNew ); + +static Vec_Ptr_t * Abc_HManCollectLeaves( Abc_HObj_t * pHNew ); +static Vec_Ptr_t * Abc_HManCollectCone( Abc_HObj_t * pHOld, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ); +static int Abc_HManSimulate( Vec_Ptr_t * vCone0, Vec_Ptr_t * vCone1, int nLeaves, int * pPhase ); + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManStart() +{ + Abc_HMan_t * p; + unsigned * pData; + int i, k; + assert( s_pHMan == NULL ); + assert( sizeof(unsigned) == 4 ); + // allocate manager + p = ALLOC( Abc_HMan_t, 1 ); + memset( p, 0, sizeof(Abc_HMan_t) ); + // allocate storage for all nodes + p->vNtks = Vec_VecStart( 1 ); + p->vProof = Vec_IntStart( 1 ); + // allocate temporary storage for objects + p->nVarsMax = ABC_SIM_VARS; + p->nObjsMax = ABC_SIM_OBJS; + p->vObjs = Vec_PtrAlloc( p->nObjsMax ); + // allocate simulation info + p->nBits = (1 << p->nVarsMax); + p->nWords = (p->nBits <= 32)? 1 : (p->nBits / 32); + p->pInfo = ALLOC( unsigned, p->nWords * p->nObjsMax ); + memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nVarsMax ); + p->vSims = Vec_PtrAlloc( p->nObjsMax ); + for ( i = 0; i < p->nObjsMax; i++ ) + Vec_PtrPush( p->vSims, p->pInfo + i * p->nWords ); + // set elementary truth tables + for ( k = 0; k < p->nVarsMax; k++ ) + { + pData = p->vSims->pArray[k]; + for ( i = 0; i < p->nBits; i++ ) + if ( i & (1 << k) ) + pData[i/32] |= (1 << (i%32)); + } + // allocate storage for the nodes + p->pMmObj = Extra_MmFixedStart( sizeof(Abc_HObj_t) ); + p->vCone0 = Vec_PtrAlloc( p->nObjsMax ); + p->vCone1 = Vec_PtrAlloc( p->nObjsMax ); + s_pHMan = p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManStop() +{ + assert( s_pHMan != NULL ); + Extra_MmFixedStop( s_pHMan->pMmObj, 0 ); + Vec_PtrFree( s_pHMan->vObjs ); + Vec_PtrFree( s_pHMan->vSims ); + Vec_VecFree( s_pHMan->vNtks ); + Vec_IntFree( s_pHMan->vProof ); + Vec_PtrFree( s_pHMan->vCone0 ); + Vec_PtrFree( s_pHMan->vCone1 ); + free( s_pHMan->pInfo ); + free( s_pHMan ); + s_pHMan = NULL; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_HManIsRunning() +{ + return s_pHMan != NULL; +} + +/**Function************************************************************* + + Synopsis [Called when a new network is created.] + + Description [Returns the new ID for the network.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_HManGetNewNtkId() +{ + if ( s_pHMan == NULL ) + return 0; + return Vec_VecSize( s_pHMan->vNtks ); // what if the new network has no nodes? +} + +/**Function************************************************************* + + Synopsis [Called when the object is created.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManAddObj( Abc_Obj_t * pObj ) +{ + Abc_HObj_t * pHObj; + if ( s_pHMan == NULL ) + return; + pHObj = (Abc_HObj_t *)Extra_MmFixedEntryFetch( s_pHMan->pMmObj ); + memset( pHObj, 0, sizeof(Abc_HObj_t) ); + // set the object type + pHObj->NtkId = pObj->pNtk->Id; + if ( Abc_ObjIsCi(pObj) ) + pHObj->fPi = 1; + else if ( Abc_ObjIsCo(pObj) ) + pHObj->fPo = 1; + Vec_VecPush( s_pHMan->vNtks, pObj->pNtk->Id, pHObj ); + // set the proof parameter for the network + if ( Vec_IntSize( s_pHMan->vProof ) == pObj->pNtk->Id ) + Vec_IntPush( s_pHMan->vProof, 0 ); +} + +/**Function************************************************************* + + Synopsis [Called when the fanin is added to the object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin ) +{ + Abc_HObj_t * pHObj; + int fCompl; + if ( s_pHMan == NULL ) + return; + // take off the complemented attribute + assert( !Abc_ObjIsComplement(pObj) ); + fCompl = Abc_ObjIsComplement(pFanin); + pFanin = Abc_ObjRegular(pFanin); + // add the fanin + assert( pObj->pNtk == pFanin->pNtk ); + pHObj = Abc_ObjHObj(pObj); + if ( pHObj->Fan0.NtkId == 0 ) + { + pHObj->Fan0.NtkId = pFanin->pNtk->Id; + pHObj->Fan0.ObjId = pFanin->Id; + pHObj->Fan0.fCompl = fCompl; + } + else if ( pHObj->Fan1.NtkId == 0 ) + { + pHObj->Fan1.NtkId = pFanin->pNtk->Id; + pHObj->Fan1.ObjId = pFanin->Id; + pHObj->Fan1.fCompl = fCompl; + } + else assert( 0 ); +} + +/**Function************************************************************* + + Synopsis [Called when the fanin's input should be complemented.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManXorFaninC( Abc_Obj_t * pObj, int iFanin ) +{ + Abc_HObj_t * pHObj; + if ( s_pHMan == NULL ) + return; + assert( iFanin < 2 ); + pHObj = Abc_ObjHObj(pObj); + if ( iFanin == 0 ) + pHObj->Fan0.fCompl ^= 1; + else if ( iFanin == 1 ) + pHObj->Fan1.fCompl ^= 1; +} + +/**Function************************************************************* + + Synopsis [Called when the fanin is added to the object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManRemoveFanins( Abc_Obj_t * pObj ) +{ + Abc_HObj_t * pHObj; + if ( s_pHMan == NULL ) + return; + assert( !Abc_ObjIsComplement(pObj) ); + pHObj = Abc_ObjHObj(pObj); + pHObj->Fan0.NtkId = 0; + pHObj->Fan0.ObjId = 0; + pHObj->Fan0.fCompl = 0; + pHObj->Fan1.NtkId = 0; + pHObj->Fan1.ObjId = 0; + pHObj->Fan1.fCompl = 0; +} + +/**Function************************************************************* + + Synopsis [Called when a new prototype of the old object is set.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManAddProto( Abc_Obj_t * pObj, Abc_Obj_t * pProto ) +{ + Abc_HObj_t * pHObj; + if ( s_pHMan == NULL ) + return; + // ignore polarity for now + pObj = Abc_ObjRegular(pObj); + pProto = Abc_ObjRegular(pProto); + // set the prototype + assert( pObj->pNtk != pProto->pNtk ); + if ( pObj->pNtk->Id == 0 ) + return; + pHObj = Abc_ObjHObj(pObj); + pHObj->Proto.NtkId = pProto->pNtk->Id; + pHObj->Proto.ObjId = pProto->Id; +} + +/**Function************************************************************* + + Synopsis [Called when an equivalent node is created.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManMapAddEqu( Abc_Obj_t * pObj, Abc_Obj_t * pEqu ) +{ +/* + Abc_HObj_t * pHObj; + if ( s_pHMan == NULL ) + return; + // ignore polarity for now + pObj = Abc_ObjRegular(pObj); + pEqu = Abc_ObjRegular(pEqu); + // set the equivalent node + assert( pObj->pNtk == pEqu->pNtk ); + pHObj = Abc_ObjHObj(pObj); + Abc_ObjHObj(pObj)->Equ.NtkId = pEqu->pNtk->Id; + Abc_ObjHObj(pObj)->Equ.ObjId = pEqu->Id; +*/ +} + + + +/**Function************************************************************* + + Synopsis [Starts the verification procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_HManPopulate( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i; + if ( !Abc_NtkIsStrash(pNtk) ) + return 0; + // allocate the network ID + pNtk->Id = Abc_HManGetNewNtkId(); + assert( pNtk->Id == 1 ); + // create the objects + Abc_NtkForEachObj( pNtk, pObj, i ) + { + Abc_HManAddObj( pObj ); + if ( Abc_ObjFaninNum(pObj) > 0 ) + Abc_HManAddFanin( pObj, Abc_ObjChild0(pObj) ); + if ( Abc_ObjFaninNum(pObj) > 1 ) + Abc_HManAddFanin( pObj, Abc_ObjChild1(pObj) ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [The main verification procedure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_HManVerify( int NtkIdOld, int NtkIdNew ) +{ + int i; + // prove the equality pairwise + for ( i = NtkIdOld; i < NtkIdNew; i++ ) + { + if ( Vec_IntEntry(s_pHMan->vProof, i) ) + continue; + if ( !Abc_HManVerifyPair( i, i+1 ) ) + return 0; + Vec_IntWriteEntry( s_pHMan->vProof, i, 1 ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Verifies two networks.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_HManVerifyPair( int NtkIdOld, int NtkIdNew ) +{ + Vec_Ptr_t * vNtkNew, * vNtkOld, * vPosNew; + Abc_HObj_t * pHObj; + int i; + // get hold of the network nodes + vNtkNew = Vec_VecEntry( s_pHMan->vNtks, NtkIdNew ); + vNtkOld = Vec_VecEntry( s_pHMan->vNtks, NtkIdOld ); + Vec_PtrForEachEntry( vNtkNew, pHObj, i ) + pHObj->fVisited = 0; + Vec_PtrForEachEntry( vNtkOld, pHObj, i ) + pHObj->fVisited = 0; + // collect new POs + vPosNew = Vec_PtrAlloc( 100 ); + Vec_PtrForEachEntry( vNtkNew, pHObj, i ) + if ( pHObj->fPo ) + Vec_PtrPush( vPosNew, pHObj ); + // prove them recursively (assuming PO ordering is the same) + Vec_PtrForEachEntry( vPosNew, pHObj, i ) + { + if ( Abc_HObjProto(pHObj) == NULL ) + { + printf( "History: PO %d has no prototype\n", i ); + return 0; + } + if ( !Abc_HManVerifyNodes_rec( Abc_HObjProto(pHObj), pHObj ) ) + { + printf( "History: Verification failed for outputs of PO pair number %d\n", i ); + return 0; + } + } + printf( "History: Verification succeeded.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Recursively verifies two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_HManVerifyNodes_rec( Abc_HObj_t * pHOld, Abc_HObj_t * pHNew ) +{ + Vec_Ptr_t * vLeaves; + Abc_HObj_t * pHObj, * pHPro0, * pHPro1; + int i, fPhase; + + assert( Abc_HObjProto(pHNew) == pHOld ); + if ( pHNew->fProof ) + return 1; + pHNew->fProof = 1; + // consider simple cases + if ( pHNew->fPi || pHNew->fConst ) + return 1; + if ( pHNew->fPo ) + { + if ( !Abc_HManVerifyNodes_rec( Abc_HObjFanin0(pHOld), Abc_HObjFanin0(pHNew) ) ) + return 0; + if ( (Abc_HObjFaninC0(pHOld) ^ Abc_HObjFaninC0(pHNew)) != (int)pHNew->fPhase ) + { + printf( "History: Phase of PO nodes does not agree.\n" ); + return 0; + } + return 1; + } + // the elementary node + pHPro0 = Abc_HObjProto( Abc_HObjFanin0(pHNew) ); + pHPro1 = Abc_HObjProto( Abc_HObjFanin1(pHNew) ); + if ( pHPro0 && pHPro1 ) + { + if ( !Abc_HManVerifyNodes_rec( pHPro0, Abc_HObjFanin0(pHNew) ) ) + return 0; + if ( !Abc_HManVerifyNodes_rec( pHPro1, Abc_HObjFanin1(pHNew) ) ) + return 0; + if ( Abc_HObjFanin0(pHOld) != pHPro0 || Abc_HObjFanin1(pHOld) != pHPro1 ) + { + printf( "History: Internal node does not match.\n" ); + return 0; + } + if ( Abc_HObjFaninC0(pHOld) != Abc_HObjFaninC0(pHNew) || + Abc_HObjFaninC1(pHOld) != Abc_HObjFaninC1(pHNew) ) + { + printf( "History: Phase of internal node does not match.\n" ); + return 0; + } + return 1; + } + // collect the leaves + vLeaves = Abc_HManCollectLeaves( pHNew ); + if ( Vec_PtrSize(vLeaves) > 16 ) + { + printf( "History: The bound on the number of inputs is exceeded.\n" ); + return 0; + } + s_pHMan->nWordsCur = ((1 << Vec_PtrSize(vLeaves)) <= 32)? 1 : ((1 << Vec_PtrSize(vLeaves)) / 32); + // prove recursively + Vec_PtrForEachEntry( vLeaves, pHObj, i ) + if ( !Abc_HManVerifyNodes_rec( Abc_HObjProto(pHObj), pHObj ) ) + { + Vec_PtrFree( vLeaves ); + return 0; + } + // get the first node + Abc_HManCollectCone( pHNew, vLeaves, s_pHMan->vCone1 ); + if ( Vec_PtrSize(s_pHMan->vCone1) > ABC_SIM_OBJS - ABC_SIM_VARS - 1 ) + { + printf( "History: The bound on the number of cone nodes is exceeded.\n" ); + return 0; + } + // get the second cone + Vec_PtrForEachEntry( vLeaves, pHObj, i ) + Vec_PtrWriteEntry( vLeaves, i, Abc_HObjProto(pHObj) ); + Abc_HManCollectCone( pHOld, vLeaves, s_pHMan->vCone0 ); + if ( Vec_PtrSize(s_pHMan->vCone0) > ABC_SIM_OBJS - ABC_SIM_VARS - 1 ) + { + printf( "History: The bound on the number of cone nodes is exceeded.\n" ); + return 0; + } + // compare the truth tables + if ( !Abc_HManSimulate( s_pHMan->vCone0, s_pHMan->vCone1, Vec_PtrSize(vLeaves), &fPhase ) ) + { + Vec_PtrFree( vLeaves ); + printf( "History: Verification failed at an internal node.\n" ); + return 0; + } + printf( "Succeeded.\n" ); + pHNew->fPhase = fPhase; + Vec_PtrFree( vLeaves ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Finds the leaves of the TFI cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManCollectLeaves_rec( Abc_HObj_t * pHNew, Vec_Ptr_t * vLeaves ) +{ + Abc_HObj_t * pHPro; + if ( pHPro = Abc_HObjProto( pHNew ) ) + { + Vec_PtrPushUnique( vLeaves, pHNew ); + return; + } + assert( !pHNew->fPi && !pHNew->fPo && !pHNew->fConst ); + Abc_HManCollectLeaves_rec( Abc_HObjFanin0(pHNew), vLeaves ); + Abc_HManCollectLeaves_rec( Abc_HObjFanin1(pHNew), vLeaves ); +} + +/**Function************************************************************* + + Synopsis [Finds the leaves of the TFI cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_HManCollectLeaves( Abc_HObj_t * pHNew ) +{ + Vec_Ptr_t * vLeaves; + vLeaves = Vec_PtrAlloc( 100 ); + Abc_HManCollectLeaves_rec( Abc_HObjFanin0(pHNew), vLeaves ); + Abc_HManCollectLeaves_rec( Abc_HObjFanin1(pHNew), vLeaves ); + return vLeaves; +} + + +/**Function************************************************************* + + Synopsis [Collects the TFI cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManCollectCone_rec( Abc_HObj_t * pHObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ) +{ + if ( pHObj->fVisited ) + return; + pHObj->fVisited = 1; + assert( !pHObj->fPi && !pHObj->fPo && !pHObj->fConst ); + Abc_HManCollectCone_rec( Abc_HObjFanin0(pHObj), vLeaves, vCone ); + Abc_HManCollectCone_rec( Abc_HObjFanin1(pHObj), vLeaves, vCone ); + pHObj->Num = Vec_PtrSize(vCone); + Vec_PtrPush( vCone, pHObj ); +} + +/**Function************************************************************* + + Synopsis [Collects the TFI cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_HManCollectCone( Abc_HObj_t * pHRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone ) +{ + Abc_HObj_t * pHObj; + int i; + Vec_PtrClear( vCone ); + Vec_PtrForEachEntry( vLeaves, pHObj, i ) + { + pHObj->fVisited = 1; + pHObj->Num = Vec_PtrSize(vCone); + Vec_PtrPush( vCone, pHObj ); + } + Abc_HManCollectCone_rec( Abc_HObjFanin0(pHRoot), vLeaves, vCone ); + Abc_HManCollectCone_rec( Abc_HObjFanin1(pHRoot), vLeaves, vCone ); + return vCone; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_HManSimulateOne( Vec_Ptr_t * vCone, int nLeaves, int fUsePhase ) +{ + Abc_HObj_t * pHObj, * pHFan0, * pHFan1; + unsigned * puData0, * puData1, * puData; + int k, i, fComp0, fComp1; + // set the leaves + Vec_PtrForEachEntryStart( vCone, pHObj, i, nLeaves ) + { + pHFan0 = Abc_HObjFanin0(pHObj); + pHFan1 = Abc_HObjFanin1(pHObj); + // consider the case of interver or buffer + if ( pHFan1 == NULL ) + { + puData = Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+i-nLeaves); + puData0 = ((int)pHFan0->Num < nLeaves)? Vec_PtrEntry(s_pHMan->vSims, pHFan0->Num) : + Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+pHFan0->Num-nLeaves); + fComp0 = Abc_HObjFaninC0(pHObj) ^ (fUsePhase && (int)pHFan0->Num < nLeaves && pHFan0->fPhase); + if ( fComp0 ) + for ( k = 0; k < s_pHMan->nWordsCur; k++ ) + puData[k] = ~puData0[k]; + else + for ( k = 0; k < s_pHMan->nWordsCur; k++ ) + puData[k] = puData0[k]; + continue; + } + // get the pointers to simulation data + puData = Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+i-nLeaves); + puData0 = ((int)pHFan0->Num < nLeaves)? Vec_PtrEntry(s_pHMan->vSims, pHFan0->Num) : + Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+pHFan0->Num-nLeaves); + puData1 = ((int)pHFan1->Num < nLeaves)? Vec_PtrEntry(s_pHMan->vSims, pHFan1->Num) : + Vec_PtrEntry(s_pHMan->vSims, ABC_SIM_VARS+pHFan1->Num-nLeaves); + // here are the phases + fComp0 = Abc_HObjFaninC0(pHObj) ^ (fUsePhase && (int)pHFan0->Num < nLeaves && pHFan0->fPhase); + fComp1 = Abc_HObjFaninC1(pHObj) ^ (fUsePhase && (int)pHFan1->Num < nLeaves && pHFan1->fPhase); + // simulate + if ( fComp0 && fComp1 ) + for ( k = 0; k < s_pHMan->nWordsCur; k++ ) + puData[k] = ~puData0[k] & ~puData1[k]; + else if ( fComp0 ) + for ( k = 0; k < s_pHMan->nWordsCur; k++ ) + puData[k] = ~puData0[k] & puData1[k]; + else if ( fComp1 ) + for ( k = 0; k < s_pHMan->nWordsCur; k++ ) + puData[k] = puData0[k] & ~puData1[k]; + else + for ( k = 0; k < s_pHMan->nWordsCur; k++ ) + puData[k] = puData0[k] & puData1[k]; + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_HManSimulate( Vec_Ptr_t * vCone0, Vec_Ptr_t * vCone1, int nLeaves, int * pPhase ) +{ + unsigned * pDataTop, * pDataLast; + int w; + // simulate the first one + Abc_HManSimulateOne( vCone0, nLeaves, 0 ); + // save the last simulation value + pDataTop = Vec_PtrEntry( s_pHMan->vSims, ((Abc_HObj_t *)Vec_PtrEntryLast(vCone0))->Num ); + pDataLast = Vec_PtrEntry( s_pHMan->vSims, Vec_PtrSize(s_pHMan->vSims)-1 ); + for ( w = 0; w < s_pHMan->nWordsCur; w++ ) + pDataLast[w] = pDataTop[w]; + // simulate the other one + Abc_HManSimulateOne( vCone1, nLeaves, 1 ); + // complement the output if needed + pDataTop = Vec_PtrEntry( s_pHMan->vSims, ((Abc_HObj_t *)Vec_PtrEntryLast(vCone1))->Num ); + // mask unused bits + if ( nLeaves < 5 ) + { + pDataTop[0] &= ((~((unsigned)0)) >> (32-(1<<nLeaves))); + pDataLast[0] &= ((~((unsigned)0)) >> (32-(1<<nLeaves))); + } + if ( *pPhase = ((pDataTop[0] & 1) != (pDataLast[0] & 1)) ) + for ( w = 0; w < s_pHMan->nWordsCur; w++ ) + pDataTop[w] = ~pDataTop[w]; + // compare + for ( w = 0; w < s_pHMan->nWordsCur; w++ ) + if ( pDataLast[w] != pDataTop[w] ) + return 0; + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c index 88188655..48b7eb92 100644 --- a/src/base/abci/abcUnate.c +++ b/src/base/abci/abcUnate.c @@ -73,7 +73,7 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose ) int clkBdd, clkUnate; // compute the global BDDs - if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL ) + if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0, 1, fVerbose) == NULL ) return; clkBdd = clock() - clk; diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index 5690013b..f1ec3847 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -58,7 +58,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose ) } // compute the global BDDs of the latches - dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1 ); + dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1, 1, fVerbose ); if ( dd == NULL ) return 0; if ( fVerbose ) @@ -331,7 +331,11 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); // transform the network to the SOP representation - Abc_NtkBddToSop( pNtkNew, 0 ); + if ( !Abc_NtkBddToSop( pNtkNew, 0 ) ) + { + printf( "Converting to SOPs has failed.\n" ); + return NULL; + } return pNtkNew; } diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c index c178c013..8d8784e0 100644 --- a/src/base/abci/abcVanEijk.c +++ b/src/base/abci/abcVanEijk.c @@ -713,7 +713,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ) Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) { Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pClass, * pNode, * pRepr, * pObj, *pObjNew; + Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;//, *pObjNew; Abc_Obj_t * pMiter, * pTotal; Vec_Ptr_t * vCone; int i, k; diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c index c92667a3..77de5185 100644 --- a/src/base/abci/abcVanImp.c +++ b/src/base/abci/abcVanImp.c @@ -870,7 +870,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I { Abc_Ntk_t * pNtkNew; Vec_Ptr_t * vCone; - Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2, * pObjNew; + Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2;//, * pObjNew; unsigned Imp; int i, k; diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 5456693b..e0c65058 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -85,7 +85,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI } // solve the CNF using the SAT solver - RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 ); + RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 ); if ( RetValue == -1 ) printf( "Networks are undecided (SAT solver timed out).\n" ); else if ( RetValue == 0 ) @@ -112,6 +112,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI ***********************************************************************/ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ) { + Prove_Params_t Params, * pParams = &Params; // Fraig_Params_t Params; // Fraig_Man_t * pMan; Abc_Ntk_t * pMiter; @@ -171,7 +172,9 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV Abc_NtkDelete( pMiter ); */ // solve the CNF using the SAT solver - RetValue = Abc_NtkMiterProve( &pMiter, 0, 0, 1, 1, 0 ); + Prove_ParamsSetDefault( pParams ); + pParams->nItersMax = 5; + RetValue = Abc_NtkMiterProve( &pMiter, pParams ); if ( RetValue == -1 ) printf( "Networks are undecided (resource limits is reached).\n" ); else if ( RetValue == 0 ) @@ -254,7 +257,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI } // solve the CNF using the SAT solver - RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 ); + RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 ); if ( RetValue == -1 ) printf( "Networks are undecided (SAT solver timed out).\n" ); else if ( RetValue == 0 ) diff --git a/src/base/abci/abc_.c b/src/base/abci/abc_.c index 50558bdb..75ec88c3 100644 --- a/src/base/abci/abc_.c +++ b/src/base/abci/abc_.c @@ -23,7 +23,7 @@ //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// - + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -40,6 +40,7 @@ ***********************************************************************/ + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 4339b520..41223c0b 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -10,6 +10,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcFpga.c \ src/base/abci/abcFraig.c \ src/base/abci/abcFxu.c \ + src/base/abci/abcGen.c \ src/base/abci/abcMap.c \ src/base/abci/abcMiter.c \ src/base/abci/abcNtbdd.c \ @@ -22,11 +23,13 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcRestruct.c \ src/base/abci/abcResub.c \ src/base/abci/abcRewrite.c \ + src/base/abci/abcRr.c \ src/base/abci/abcSat.c \ src/base/abci/abcStrash.c \ src/base/abci/abcSweep.c \ src/base/abci/abcSymm.c \ src/base/abci/abcTiming.c \ + src/base/abci/abcTrace.c \ src/base/abci/abcUnate.c \ src/base/abci/abcUnreach.c \ src/base/abci/abcVanEijk.c \ |