From faf1265bb82f934cc14b6106ccce89e37203efbd Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 2 Nov 2006 08:01:00 -0800 Subject: Version abc61102 --- src/base/abci/abc.c | 400 ++++++++++++++++++++++++++++++++++---------- src/base/abci/abcBmc.c | 115 +++++++++++++ src/base/abci/abcDsd.c | 2 +- src/base/abci/abcFpga.c | 2 +- src/base/abci/abcFpgaFast.c | 4 +- src/base/abci/abcIvy.c | 35 ++-- src/base/abci/abcLut.c | 4 +- src/base/abci/abcMap.c | 10 +- src/base/abci/abcNtbdd.c | 8 +- src/base/abci/abcPrint.c | 107 +++++++++++- src/base/abci/abcSweep.c | 262 ++++++++++++++++++++++++++++- src/base/abci/abcVerify.c | 4 +- src/base/abci/abcXsim.c | 164 ++++++++++++++++++ src/base/abci/module.make | 4 +- 14 files changed, 993 insertions(+), 128 deletions(-) create mode 100644 src/base/abci/abcBmc.c create mode 100644 src/base/abci/abcXsim.c (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b25ca2f7..5d6af56d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36,6 +36,7 @@ static int Abc_CommandPrintExdc ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandPrintIo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintLatch ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintFanio ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrintMffc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -90,6 +91,7 @@ static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** arg 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_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -102,6 +104,7 @@ static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -166,6 +169,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Printing", "print_io", Abc_CommandPrintIo, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_latch", Abc_CommandPrintLatch, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_fanio", Abc_CommandPrintFanio, 0 ); + Cmd_CommandAdd( pAbc, "Printing", "print_mffc", Abc_CommandPrintMffc, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_factor", Abc_CommandPrintFactor, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_level", Abc_CommandPrintLevel, 0 ); Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 0 ); @@ -220,6 +224,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "espresso", Abc_CommandEspresso, 1 ); Cmd_CommandAdd( pAbc, "Various", "gen", Abc_CommandGen, 0 ); Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 ); + Cmd_CommandAdd( pAbc, "Various", "xsim", Abc_CommandXsim, 0 ); Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 ); Cmd_CommandAdd( pAbc, "New AIG", "istrash", Abc_CommandIStrash, 1 ); @@ -232,6 +237,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "New AIG", "iprove", Abc_CommandIProve, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 ); + Cmd_CommandAdd( pAbc, "New AIG", "bmc", Abc_CommandBmc, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Abc_CommandFraigTrust, 1 ); @@ -250,15 +256,15 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga", Abc_CommandFpgaFast, 1 ); Cmd_CommandAdd( pAbc, "FPGA mapping", "pga", Abc_CommandPga, 1 ); - Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 ); - Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 ); - Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 ); - Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 ); - Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 ); +// Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 ); +// Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 ); +// Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 ); +// Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 ); +// Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 ); - Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 ); - Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 ); - Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 ); +// Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 ); +// Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 ); +// Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 ); Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); @@ -269,8 +275,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) // Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 ); - Cmd_CommandAdd( pAbc, "Sequential", "howard", Abc_CommandHoward, 0 ); - Cmd_CommandAdd( pAbc, "Sequential", "skew_fwd", Abc_CommandSkewForward, 0 ); +// Cmd_CommandAdd( pAbc, "Sequential", "howard", Abc_CommandHoward, 0 ); +// Cmd_CommandAdd( pAbc, "Sequential", "skew_fwd", Abc_CommandSkewForward, 0 ); // Rwt_Man4ExploreStart(); // Map_Var3Print(); @@ -618,6 +624,58 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandPrintMffc( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + extern void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk ); + + 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; + } + + // print the nodes + Abc_NtkPrintMffc( pOut, pNtk ); + return 0; + +usage: + fprintf( pErr, "usage: print_mffc [-h]\n" ); + fprintf( pErr, "\t prints the MFFC of each node in the network\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -1581,7 +1639,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk; int c; int fMulti; - extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk ); + extern void Abc_NtkShowAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesShow ); extern void Abc_NtkShowMulti( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); @@ -1609,7 +1667,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( !Abc_NtkHasAig(pNtk) ) + if ( !Abc_NtkIsStrash(pNtk) ) { fprintf( pErr, "Visualizing networks other than AIGs can be done using command \"show_ntk\".\n" ); return 1; @@ -1622,7 +1680,7 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !fMulti ) - Abc_NtkShowAig( pNtk ); + Abc_NtkShowAig( pNtk, NULL ); else Abc_NtkShowMulti( pNtk ); return 0; @@ -1683,7 +1741,7 @@ int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( Abc_NtkHasAig(pNtk) ) + if ( Abc_NtkIsStrash(pNtk) ) { fprintf( pErr, "Visualizing AIG can only be done using command \"show_aig\".\n" ); return 1; @@ -4964,6 +5022,88 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int nFrames; + int fInputs; + int fVerbose; + extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFrames = 10; + fInputs = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'i': + fInputs ^= 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, "Only works for strashed networks.\n" ); + return 1; + } + + Abc_NtkXValueSimulate( pNtk, nFrames, fInputs, fVerbose ); + return 0; + +usage: + fprintf( pErr, "usage: xsim [-F num] [-ivh]\n" ); + fprintf( pErr, "\t performs X-valued simulation of the AIG\n" ); + fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames ); + fprintf( pErr, "\t-i : toggle X-valued state or X-valued inputs [default = %s]\n", fInputs? "inputs": "state" ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -4978,11 +5118,12 @@ 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; int nLevels; // extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); - extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ); +// extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ); + extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -5064,7 +5205,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Ivy_TruthEstimateNodesTest(); - +/* pNtkRes = Abc_NtkIvy( pNtk ); // pNtkRes = Abc_NtkPlayer( pNtk, nLevels, 0 ); // pNtkRes = NULL; @@ -5075,7 +5216,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); - +*/ + Abc_NtkMaxFlowTest( pNtk ); return 0; usage: @@ -5100,7 +5242,7 @@ usage: int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtkRes; + Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp; int c; extern Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk ); @@ -5132,11 +5274,12 @@ int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( pErr, "Only works for combinatinally strashed AIG networks.\n" ); - return 1; + pNtkTemp = Abc_NtkStrash( pNtk, 0, 1 ); + pNtkRes = Abc_NtkIvyStrash( pNtkTemp ); + Abc_NtkDelete( pNtkTemp ); } - - pNtkRes = Abc_NtkIvyStrash( pNtk ); + else + pNtkRes = Abc_NtkIvyStrash( pNtk ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -5741,9 +5884,9 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - nIters = 3; - fUseZeroCost = 1; - fVerbose = 0; + nIters = 2; + fUseZeroCost = 0; + fVerbose = 1; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Izvh" ) ) != EOF ) { @@ -5869,6 +6012,94 @@ usage: fprintf( pErr, "\t-h : print the command usage\n"); return 1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int nFrames; + int fInit; + int fVerbose; + + extern void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFrames = 5; + fInit = 0; + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Kivh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'i': + fInit ^= 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_NtkIsSeq(pNtk) ) + { + fprintf( pErr, "Only works for non-sequential networks.\n" ); + return 1; + } + if ( Abc_NtkIsStrash(pNtk) ) + Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose ); + else + { + pNtk = Abc_NtkStrash( pNtk, 0, 1 ); + Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose ); + Abc_NtkDelete( pNtk ); + } + return 0; + +usage: + fprintf( pErr, "usage: bmc [-K num] [-ivh]\n" ); + fprintf( pErr, "\t perform bounded model checking\n" ); + fprintf( pErr, "\t-K num : number of time frames [default = %d]\n", nFrames ); + fprintf( pErr, "\t-i : toggle initialization of the first frame [default = %s]\n", fInit? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} /**Function************************************************************* @@ -7573,48 +7804,38 @@ usage: int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtkRes, * pNtkTemp; + Abc_Ntk_t * pNtk, * pNtkTemp; int c, nMaxIters; - int fForward; - int fBackward; int fInitial; int fVerbose; + int Mode; + extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fForward = 0; - fBackward = 0; + Mode = 3; fInitial = 1; - fVerbose = 0; + fVerbose = 1; nMaxIters = 15; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Ifbivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Mvh" ) ) != EOF ) { switch ( c ) { - case 'I': + case 'M': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" ); + fprintf( pErr, "Command line switch \"-M\" should be followed by a positive integer.\n" ); goto usage; } - nMaxIters = atoi(argv[globalUtilOptind]); + Mode = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nMaxIters < 0 ) + if ( Mode < 0 ) goto usage; break; - case 'f': - fForward ^= 1; - break; - case 'b': - fBackward ^= 1; - break; - case 'i': - fInitial ^= 1; - break; case 'v': fVerbose ^= 1; break; @@ -7631,61 +7852,56 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( !Abc_NtkIsSeq(pNtk) && Abc_NtkLatchNum(pNtk) == 0 ) + if ( !Abc_NtkLatchNum(pNtk) ) { fprintf( pErr, "The network has no latches. Retiming is not performed.\n" ); return 0; } - if ( Abc_NtkHasAig(pNtk) ) + if ( Abc_NtkIsStrash(pNtk) ) { - // quit if there are choice nodes if ( Abc_NtkGetChoiceNum(pNtk) ) { - fprintf( pErr, "Currently cannot retime networks with choice nodes.\n" ); + fprintf( pErr, "Retiming with choice nodes is not implemented.\n" ); return 0; } - if ( Abc_NtkIsStrash(pNtk) ) - pNtkRes = Abc_NtkAigToSeq(pNtk); - else - pNtkRes = Abc_NtkDup(pNtk); - // retime the network - if ( fForward ) - Seq_NtkSeqRetimeForward( pNtkRes, fInitial, fVerbose ); - else if ( fBackward ) - Seq_NtkSeqRetimeBackward( pNtkRes, fInitial, fVerbose ); - else - Seq_NtkSeqRetimeDelay( pNtkRes, nMaxIters, fInitial, fVerbose ); - // if the network is an AIG, convert the result into an AIG - if ( Abc_NtkIsStrash(pNtk) ) - { - pNtkRes = Abc_NtkSeqToLogicSop( pNtkTemp = pNtkRes ); - Abc_NtkDelete( pNtkTemp ); - pNtkRes = Abc_NtkStrash( pNtkTemp = pNtkRes, 0, 0 ); - Abc_NtkDelete( pNtkTemp ); - } + pNtk = Abc_NtkAigToLogicSop( pNtkTemp = pNtk ); + Abc_NtkDelete( pNtkTemp ); } - else - pNtkRes = Seq_NtkRetime( pNtk, nMaxIters, fInitial, fVerbose ); - // replace the network - if ( pNtkRes == NULL ) + + // get the network in the SOP form + if ( !Abc_NtkLogicToSop(pNtk, 0) ) { - fprintf( pErr, "Retiming has failed.\n" ); + printf( "Converting to SOPs has failed.\n" ); return 0; } - // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + + if ( !Abc_NtkIsLogic(pNtk) ) + { + fprintf( pErr, "The network is not a logic network. Retiming is not performed.\n" ); + return 0; + } + + // perform the retiming + Abc_NtkRetime( pNtk, Mode, fVerbose ); return 0; usage: - fprintf( pErr, "usage: retime [-I num] [-fbih]\n" ); - fprintf( pErr, "\t retimes the current network using Pan's delay-optimal retiming\n" ); - fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters ); - fprintf( pErr, "\t-f : toggle forward retiming (for AIGs) [default = %s]\n", fForward? "yes": "no" ); - fprintf( pErr, "\t-b : toggle backward retiming (for AIGs) [default = %s]\n", fBackward? "yes": "no" ); - fprintf( pErr, "\t-i : toggle computation of initial state [default = %s]\n", fInitial? "yes": "no" ); + fprintf( pErr, "usage: retime [-M num] [-vh]\n" ); + fprintf( pErr, "\t retimes the current network using one of the algorithms:\n" ); + fprintf( pErr, "\t 1: most forward retiming\n" ); + fprintf( pErr, "\t 2: most backward retiming\n" ); + fprintf( pErr, "\t 3: min-area retiming\n" ); + fprintf( pErr, "\t 4: min-delay retiming\n" ); + fprintf( pErr, "\t 5: min-area under min-delay constraint retiming\n" ); + fprintf( pErr, "\t-M num : the retiming algorithm to use [default = %d]\n", Mode ); + fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; +// fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters ); +// fprintf( pErr, "\t-f : toggle forward retiming (for AIGs) [default = %s]\n", fForward? "yes": "no" ); +// fprintf( pErr, "\t-b : toggle backward retiming (for AIGs) [default = %s]\n", fBackward? "yes": "no" ); +// fprintf( pErr, "\t-i : toggle computation of initial state [default = %s]\n", fInitial? "yes": "no" ); } /**Function************************************************************* @@ -8069,17 +8285,22 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; + int fVerbose; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fVerbose = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { switch ( c ) { + case 'v': + fVerbose ^= 1; + break; case 'h': goto usage; default: @@ -8091,18 +8312,23 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } - if ( !Abc_NtkIsSeq(pNtk) ) + if ( !Abc_NtkIsLogic(pNtk) ) { - fprintf( pErr, "Only works for sequential AIGs.\n" ); + fprintf( pErr, "Only works for logic networks.\n" ); return 1; } // modify the current network - Seq_NtkCleanup( pNtk, 1 ); + Abc_NtkCleanupSeq( pNtk, fVerbose ); return 0; usage: - fprintf( pErr, "usage: scleanup [-h]\n" ); + fprintf( pErr, "usage: scleanup [-vh]\n" ); fprintf( pErr, "\t performs sequential cleanup\n" ); + fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" ); + fprintf( pErr, "\t - removes and shared latches driven by constants\n" ); + fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" ); + fprintf( pErr, "\t (the latter may change sequential behaviour)\n" ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcBmc.c b/src/base/abci/abcBmc.c new file mode 100644 index 00000000..af6d237b --- /dev/null +++ b/src/base/abci/abcBmc.c @@ -0,0 +1,115 @@ +/**CFile**************************************************************** + + FileName [abcBmc.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Performs bounded model check.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc ); + +static void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose ) +{ + Ivy_FraigParams_t Params, * pParams = &Params; + Ivy_Man_t * pMan, * pFrames, * pFraig; + Vec_Ptr_t * vMapping; + // convert to IVY manager + pMan = Abc_NtkIvyBefore( pNtk, 0, 0 ); + // generate timeframes + pFrames = Ivy_ManFrames( pMan, Abc_NtkLatchNum(pNtk), nFrames, fInit, &vMapping ); + // fraig the timeframes + Ivy_FraigParamsDefault( pParams ); + pParams->nBTLimitNode = ABC_INFINITY; + pParams->fVerbose = 0; + pParams->fProve = 0; + pFraig = Ivy_FraigPerform( pFrames, pParams ); +printf( "Frames have %6d nodes. ", Ivy_ManNodeNum(pFrames) ); +printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) ); + // report the classes +// if ( fVerbose ) +// Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames ); + // free stuff + Vec_PtrFree( vMapping ); + Ivy_ManStop( pFraig ); + Ivy_ManStop( pFrames ); + Ivy_ManStop( pMan ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames ) +{ + Ivy_Obj_t * pFirst1, * pFirst2, * pFirst3; + int i, f, nIdMax, Prev2, Prev3; + nIdMax = Ivy_ManObjIdMax(pMan); + // check what is the number of nodes in each frame + Prev2 = Prev3 = 0; + for ( f = 0; f < nFrames; f++ ) + { + Ivy_ManForEachNode( pMan, pFirst1, i ) + { + pFirst2 = Ivy_Regular( Vec_PtrEntry(vMapping, f * nIdMax + pFirst1->Id) ); + if ( Ivy_ObjIsConst1(pFirst2) || pFirst2->Type == 0 ) + continue; + pFirst3 = Ivy_Regular( pFirst2->pEquiv ); + if ( Ivy_ObjIsConst1(pFirst3) || pFirst3->Type == 0 ) + continue; + break; + } + if ( f ) + printf( "Frame %3d : Strash = %5d Fraig = %5d\n", f, pFirst2->Id - Prev2, pFirst3->Id - Prev3 ); + Prev2 = pFirst2->Id; + Prev3 = pFirst3->Id; + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index 6708217c..b38012cd 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -172,7 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * int i, nNodesDsd; // save the CI nodes in the DSD nodes - Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NodeCreateConst1(pNtkNew) ); + Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkCreateNodeConst1(pNtkNew) ); Abc_NtkForEachCi( pNtk, pNode, i ) { pNodeDsd = Dsd_ManagerReadInput( pManDsd, i ); diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c index 80238b48..3bc9fbed 100644 --- a/src/base/abci/abcFpga.c +++ b/src/base/abci/abcFpga.c @@ -210,7 +210,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk ) Fpga_NodeSetData0( Fpga_ManReadInputs(pMan)[i], (char *)pNode->pCopy ); // set the constant node // if ( Fpga_NodeReadRefs(Fpga_ManReadConst1(pMan)) > 0 ) - Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NodeCreateConst1(pNtkNew) ); + Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NtkCreateNodeConst1(pNtkNew) ); // process the nodes in topological order pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) diff --git a/src/base/abci/abcFpgaFast.c b/src/base/abci/abcFpgaFast.c index b307273f..3ad29291 100644 --- a/src/base/abci/abcFpgaFast.c +++ b/src/base/abci/abcFpgaFast.c @@ -99,7 +99,7 @@ Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan ) // start the new ABC network pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG ); // transfer the pointers to the basic nodes - Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NodeCreateConst1(pNtkNew) ); + Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NtkCreateNodeConst1(pNtkNew) ); Abc_NtkForEachCi( pNtkNew, pObjAbc, i ) Abc_ObjSetIvy2Abc( pMan, Ivy_ManPi(pMan, i)->Id, pObjAbc ); // recursively construct the network @@ -112,7 +112,7 @@ Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan ) if ( Ivy_ObjFaninC0(pObjIvy) ) // complement { if ( Abc_ObjIsCi(pObjAbc) ) - pObjAbc = Abc_NodeCreateInv( pNtkNew, pObjAbc ); + pObjAbc = Abc_NtkCreateNodeInv( pNtkNew, pObjAbc ); else { // clone the node diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 82e03119..446eb0cc 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -51,7 +51,7 @@ static inline Abc_Obj_t * Abc_EdgeToNode( Abc_Ntk_t * p, Abc_Edge_t Edge ) { static inline Abc_Obj_t * Abc_ObjFanin0Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ); } static inline Abc_Obj_t * Abc_ObjFanin1Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ); } -static int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk, int fUseDcs ); +static Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -85,7 +85,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc ) if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) ) { printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) ); - return NULL; +// return NULL; } // print warning about choice nodes if ( Abc_NtkGetChoiceNum( pNtk ) ) @@ -102,9 +102,9 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc ) if ( fSeq ) { int nLatches = Abc_NtkLatchNum(pNtk); - int * pInit = Abc_NtkCollectLatchValues( pNtk, fUseDc ); - Ivy_ManMakeSeq( pMan, nLatches, pInit ); - FREE( pInit ); + Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, fUseDc ); + Ivy_ManMakeSeq( pMan, nLatches, vInit->pArray ); + Vec_IntFree( vInit ); // Ivy_ManPrintStats( pMan ); } return pMan; @@ -191,8 +191,8 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int return NULL; Ivy_ManHaigStart( pMan, fVerbose ); - Ivy_ManRewriteSeq( pMan, 0, 0 ); - for ( i = 1; i < nIters; i++ ) +// Ivy_ManRewriteSeq( pMan, 0, 0 ); + for ( i = 0; i < nIters; i++ ) Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 ); Ivy_ManHaigPostprocess( pMan, fVerbose ); @@ -486,7 +486,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ) int fCleanup = 1; // int nNodes; int nLatches = Abc_NtkLatchNum(pNtk); - int * pInit = Abc_NtkCollectLatchValues( pNtk, 0 ); + Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 ); assert( !Abc_NtkIsNetlist(pNtk) ); assert( !Abc_NtkIsSeq(pNtk) ); @@ -494,7 +494,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ) { if ( !Abc_NtkBddToSop(pNtk, 0) ) { - FREE( pInit ); + Vec_IntFree( vInit ); printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" ); return NULL; } @@ -513,7 +513,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ) pMan = Abc_NtkToAig( pNtk ); if ( !Ivy_ManCheck( pMan ) ) { - FREE( pInit ); + Vec_IntFree( vInit ); printf( "AIG check has failed.\n" ); Ivy_ManStop( pMan ); return NULL; @@ -975,22 +975,23 @@ Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pRoot, cha SeeAlso [] ***********************************************************************/ -int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk, int fUseDcs ) +Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs ) { Abc_Obj_t * pLatch; - int * pArray, i; - pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) ); + Vec_Int_t * vArray; + int i; + vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) ); Abc_NtkForEachLatch( pNtk, pLatch, i ) { if ( fUseDcs || Abc_LatchIsInitDc(pLatch) ) - pArray[i] = IVY_INIT_DC; + Vec_IntPush( vArray, IVY_INIT_DC ); else if ( Abc_LatchIsInit1(pLatch) ) - pArray[i] = IVY_INIT_1; + Vec_IntPush( vArray, IVY_INIT_1 ); else if ( Abc_LatchIsInit0(pLatch) ) - pArray[i] = IVY_INIT_0; + Vec_IntPush( vArray, IVY_INIT_0 ); else assert( 0 ); } - return pArray; + return vArray; } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c index 165d84c5..61b1ce78 100644 --- a/src/base/abci/abcLut.c +++ b/src/base/abci/abcLut.c @@ -148,7 +148,7 @@ int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int // if there is no delay improvement, skip; otherwise, update level if ( pObjTop->Level >= pObj->Level ) { - Abc_NtkDeleteObj_rec( pObjTop ); + Abc_NtkDeleteObj_rec( pObjTop, 1 ); continue; } pObj->Level = pObjTop->Level; @@ -570,7 +570,7 @@ Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * p, Abc_Obj_t * pObj ) { Vec_PtrForEachEntry( p->vLeaves, pFanin, i ) if ( Abc_ObjIsNode(pFanin) && Abc_ObjFanoutNum(pFanin) == 0 ) - Abc_NtkDeleteObj_rec( pFanin ); + Abc_NtkDeleteObj_rec( pFanin, 1 ); return NULL; } // create the topmost node diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index 276e41d0..c4f9850a 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -259,7 +259,7 @@ Abc_Obj_t * Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int // check the case of constant node if ( Map_NodeIsConst(pNodeMap) ) - return fPhase? Abc_NodeCreateConst1(pNtkNew) : Abc_NodeCreateConst0(pNtkNew); + return fPhase? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew); // check if the phase is already implemented pNodeNew = (Abc_Obj_t *)Map_NodeReadData( pNodeMap, fPhase ); @@ -369,7 +369,7 @@ Abc_Obj_t * Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap * (since the cut only has 4 variables). An interesting question is what * if the first variable (and not the fifth one is the redundant one; * can that happen?) */ - return Abc_NodeCreateConst0(pNtkNew); + return Abc_NtkCreateNodeConst0(pNtkNew); } } @@ -503,14 +503,14 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk ) // set the pointers from the mapper to the new nodes Abc_NtkForEachCi( pNtk, pNode, i ) { - Map_NodeSetData( Map_ManReadInputs(pMan)[i], 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) ); + Map_NodeSetData( Map_ManReadInputs(pMan)[i], 0, (char *)Abc_NtkCreateNodeInv(pNtkNew,pNode->pCopy) ); Map_NodeSetData( Map_ManReadInputs(pMan)[i], 1, (char *)pNode->pCopy ); } Abc_NtkForEachNode( pNtk, pNode, i ) { // if ( Abc_NodeIsConst(pNode) ) // continue; - Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) ); + Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NtkCreateNodeInv(pNtkNew,pNode->pCopy) ); Map_NodeSetData( (Map_Node_t *)pNode->pNext, 1, (char *)pNode->pCopy ); } @@ -630,7 +630,7 @@ Abc_Obj_t * Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Super_t * p * (since the cut only has 4 variables). An interesting question is what * if the first variable (and not the fifth one is the redundant one; * can that happen?) */ - return Abc_NodeCreateConst0(pNtkNew); + return Abc_NtkCreateNodeConst0(pNtkNew); } } diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index 9b67ab13..a1f6b9f9 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -195,7 +195,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew ) pNodeNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node ); st_free_table( tBdd2Node ); if ( Cudd_IsComplement(bFunc) ) - pNodeNew = Abc_NodeCreateInv( pNtkNew, pNodeNew ); + pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew ); return pNodeNew; } @@ -215,18 +215,18 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC; assert( !Cudd_IsComplement(bFunc) ); if ( bFunc == b1 ) - return Abc_NodeCreateConst1(pNtkNew); + return Abc_NtkCreateNodeConst1(pNtkNew); if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) ) return pNodeNew; // solve for the children nodes pNodeNew0 = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node ); if ( Cudd_IsComplement(cuddE(bFunc)) ) - pNodeNew0 = Abc_NodeCreateInv( pNtkNew, pNodeNew0 ); + pNodeNew0 = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew0 ); pNodeNew1 = Abc_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node ); if ( !st_lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) ) assert( 0 ); // create the MUX node - pNodeNew = Abc_NodeCreateMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 ); + pNodeNew = Abc_NtkCreateNodeMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 ); st_insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew ); return pNodeNew; } diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index afc635e9..6af12afd 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -61,10 +61,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) else fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) ); - if ( !Abc_NtkIsSeq(pNtk) ) +// if ( !Abc_NtkIsSeq(pNtk) ) fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) ); - else - fprintf( pFile, " lat = %4d(%d,%d)", Seq_NtkLatchNum(pNtk), Seq_NtkLatchNumShared(pNtk), Seq_NtkLatchNumMax(pNtk) ); +// else +// fprintf( pFile, " lat = %4d(%d,%d)", Seq_NtkLatchNum(pNtk), Seq_NtkLatchNumShared(pNtk), Seq_NtkLatchNumMax(pNtk) ); if ( Abc_NtkIsNetlist(pNtk) ) { @@ -228,6 +228,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ) int InitNums[4], Init; assert( !Abc_NtkIsNetlist(pNtk) ); +/* if ( Abc_NtkIsSeq(pNtk) ) { Seq_NtkLatchGetInitNums( pNtk, InitNums ); @@ -236,7 +237,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ) Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] ); return; } - +*/ if ( Abc_NtkLatchNum(pNtk) == 0 ) { fprintf( pFile, "The network is combinational.\n" ); @@ -381,6 +382,26 @@ void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode ) fprintf( pFile, "\n" ); } +/**Function************************************************************* + + Synopsis [Prints the MFFCs of the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i; + extern void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ); + Abc_NtkForEachNode( pNtk, pNode, i ) + Abc_NodeMffsConeSuppPrint( pNode ); +} + /**Function************************************************************* Synopsis [Prints the factored form of one node.] @@ -833,6 +854,84 @@ void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll ) { fprintf( pFile, "Endpoint Skews : Total |Skew| = %.2f\t Avg |Skew| = %.2f\t Non-Zero Skews = %d\n", sum, avg, nNonZero ); } + +/**Function************************************************************* + + Synopsis [Prints information about the object.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj ) +{ + Abc_Obj_t * pFanin; + int i; + fprintf( pFile, "Object %5d : ", pObj->Id ); + switch ( pObj->Type ) + { + case ABC_OBJ_NONE: + fprintf( pFile, "NONE " ); + break; + case ABC_OBJ_CONST1: + fprintf( pFile, "Const1 " ); + break; + case ABC_OBJ_PIO: + fprintf( pFile, "PIO " ); + break; + case ABC_OBJ_PI: + fprintf( pFile, "PI " ); + break; + case ABC_OBJ_PO: + fprintf( pFile, "PO " ); + break; + case ABC_OBJ_BI: + fprintf( pFile, "BI " ); + break; + case ABC_OBJ_BO: + fprintf( pFile, "BO " ); + break; + case ABC_OBJ_ASSERT: + fprintf( pFile, "Assert " ); + break; + case ABC_OBJ_NET: + fprintf( pFile, "Net " ); + break; + case ABC_OBJ_NODE: + fprintf( pFile, "Node " ); + break; + case ABC_OBJ_GATE: + fprintf( pFile, "Gate " ); + break; + case ABC_OBJ_LATCH: + fprintf( pFile, "Latch " ); + break; + case ABC_OBJ_TRI: + fprintf( pFile, "Tristate" ); + break; + case ABC_OBJ_BLACKBOX: + fprintf( pFile, "Blackbox" ); + break; + default: + assert(0); + break; + } + // print the fanins + fprintf( pFile, " Fanins ( " ); + Abc_ObjForEachFanin( pObj, pFanin, i ) + fprintf( pFile, "%d ", pFanin->Id ); + fprintf( pFile, ") " ); + // print the logic function + if ( Abc_ObjIsNode(pObj) && Abc_NtkIsSopLogic(pObj->pNtk) ) + fprintf( pFile, " %s", pObj->pData ); + else + fprintf( pFile, "\n" ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index cac634da..076bee46 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -32,6 +32,7 @@ static void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t static void Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose ); static int Abc_NodeDroppingCost( Abc_Obj_t * pNode ); +static int Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes ); static void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose ); static void Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, bool fConst0 ); static void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin ); @@ -425,7 +426,7 @@ void Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, return; // add the invertor - pNodeMinInv = Abc_NodeCreateInv( pNtk, pNodeMin ); + pNodeMinInv = Abc_NtkCreateNodeInv( pNtk, pNodeMin ); // move the fanouts of the inverted nodes for ( pNode = pListInv; pNode; pNode = pNode->pNext ) @@ -583,7 +584,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose ) if ( Abc_ObjFanoutNum(pNode) > 0 ) Vec_PtrPush( vNodes, pNode ); else - Abc_NtkDeleteObj_rec( pNode ); + Abc_NtkDeleteObj_rec( pNode, 1 ); } Vec_PtrFree( vNodes ); // sweep a node into its CO fanout if all of this is true: @@ -672,6 +673,263 @@ void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin ) Cudd_RecursiveDeref( dd, bCof1 ); } + + +/**Function************************************************************* + + Synopsis [Removes all objects whose trav ID is not current.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeRemoveNonCurrentObjects( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int Counter, i; + int fVerbose = 0; + + // report on the nodes to be deleted + if ( fVerbose ) + { + printf( "These nodes will be deleted: \n" ); + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( !Abc_NodeIsTravIdCurrent( pObj ) ) + { + printf( " " ); + Abc_ObjPrint( stdout, pObj ); + } + } + + // delete the nodes + Counter = 0; + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( !Abc_NodeIsTravIdCurrent( pObj ) ) + { + Abc_NtkDeleteObj( pObj ); + Counter++; + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Check if the fanin of this latch is a constant.] + + Description [Returns 0/1 if constant; -1 if not a constant.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkSetTravId_rec( Abc_Obj_t * pObj ) +{ + Abc_NodeSetTravIdCurrent(pObj); + if ( Abc_ObjFaninNum(pObj) == 0 ) + return; + assert( Abc_ObjFaninNum(pObj) == 1 ); + Abc_NtkSetTravId_rec( Abc_ObjFanin0(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Check if the fanin of this latch is a constant.] + + Description [Returns 0/1 if constant; -1 if not a constant.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCheckConstant_rec( Abc_Obj_t * pObj ) +{ + if ( Abc_ObjFaninNum(pObj) == 0 ) + { + if ( !Abc_ObjIsNode(pObj) ) + return -1; + if ( Abc_NodeIsConst0(pObj) ) + return 0; + if ( Abc_NodeIsConst1(pObj) ) + return 1; + assert( 0 ); + return -1; + } + if ( Abc_ObjIsLatch(pObj) || Abc_ObjFaninNum(pObj) > 1 ) + return -1; + if ( !Abc_ObjIsNode(pObj) || Abc_NodeIsBuf(pObj) ) + return Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pObj) ); + if ( Abc_NodeIsInv(pObj) ) + { + int RetValue = Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pObj) ); + if ( RetValue == 0 ) + return 1; + if ( RetValue == 1 ) + return 0; + return RetValue; + } + assert( 0 ); + return -1; +} + +/**Function************************************************************* + + Synopsis [Removes redundant latches.] + + Description [The redundant latches are of two types: + - Latches fed by a constant which matches the init value of the latch. + - Latches fed by a constant which does not match the init value of the latch + can be all replaced by one latch.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkLatchSweep( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pFanin, * pLatch, * pLatchPivot = NULL; + int Counter, RetValue, i; + Counter = 0; + // go through the latches + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + // check if the latch has constant input + RetValue = Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pLatch) ); + if ( RetValue == -1 ) + continue; + // found a latch with constant fanin + if ( (RetValue == 1 && Abc_LatchIsInit0(pLatch)) || + (RetValue == 0 && Abc_LatchIsInit1(pLatch)) ) + { + // fanin constant differs from the latch init value + if ( pLatchPivot == NULL ) + { + pLatchPivot = pLatch; + continue; + } + if ( Abc_LatchInit(pLatch) != Abc_LatchInit(pLatchPivot) ) // add inverter + pFanin = Abc_NtkCreateNodeInv( pNtk, Abc_ObjFanout0(pLatchPivot) ); + else + pFanin = Abc_ObjFanout0(pLatchPivot); + } + else + pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch)); + // replace latch + Abc_ObjTransferFanout( Abc_ObjFanout0(pLatch), pFanin ); + // delete the extra nodes + Abc_NtkDeleteObj_rec( Abc_ObjFanout0(pLatch), 0 ); + Counter++; + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Replaces autonumnous logic by free inputs.] + + Description [Assumes that non-autonomous logic is marked with + the current ID.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode, * pFanin; + Vec_Ptr_t * vNodes; + int i, k, Counter; + // collect the nodes that feed into the reachable logic + vNodes = Vec_PtrAlloc( 100 ); + Abc_NtkForEachObj( pNtk, pNode, i ) + { + // skip non-visited fanins + if ( !Abc_NodeIsTravIdCurrent(pNode) ) + continue; + // look for non-visited fanins + Abc_ObjForEachFanin( pNode, pFanin, k ) + { + // skip visited fanins + if ( Abc_NodeIsTravIdCurrent(pFanin) ) + continue; + // skip constants and latches fed by constants + if ( Abc_NtkCheckConstant_rec(pFanin) != -1 || + (Abc_ObjIsBi(pFanin) && Abc_NtkCheckConstant_rec(Abc_ObjFanin0(Abc_ObjFanin0(pFanin))) != -1) ) + { + Abc_NtkSetTravId_rec( pFanin ); + continue; + } + assert( !Abc_ObjIsLatch(pFanin) ); + Vec_PtrPush( vNodes, pFanin ); + } + } + Vec_PtrUniqify( vNodes, Abc_ObjPointerCompare ); + // replace these nodes by the PIs + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + pFanin = Abc_NtkCreatePi(pNtk); + Abc_NodeSetTravIdCurrent( pFanin ); + Abc_ObjTransferFanout( pNode, pFanin ); + } + Counter = Vec_PtrSize(vNodes); + Vec_PtrFree( vNodes ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Sequential cleanup.] + + Description [Performs three tasks: + - Removes logic that does not feed into POs. + - Removes latches driven by constant values equal to the initial state. + - Replaces the autonomous components by additional PI variables.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Vec_Ptr_t * vNodes; + int Counter; + assert( Abc_NtkIsLogic(pNtk) ); + // mark the nodes reachable from the POs + vNodes = Abc_NtkDfsSeq( pNtk ); + Vec_PtrFree( vNodes ); + // remove the non-marked nodes + Counter = Abc_NodeRemoveNonCurrentObjects( pNtk ); + if ( fVerbose ) + printf( "Cleanup removed %4d dangling objects.\n", Counter ); + // check if some of the latches can be removed + Counter = Abc_NtkLatchSweep( pNtk ); + if ( fVerbose ) + printf( "Cleanup removed %4d redundant latches.\n", Counter ); + // detect the autonomous components + vNodes = Abc_NtkDfsSeqReverse( pNtk ); + Vec_PtrFree( vNodes ); + // replace them by PIs + Counter = Abc_NtkReplaceAutonomousLogic( pNtk ); + if ( fVerbose ) + printf( "Cleanup added %4d additional PIs.\n", Counter ); + // remove the non-marked nodes + Counter = Abc_NodeRemoveNonCurrentObjects( pNtk ); + if ( fVerbose ) + printf( "Cleanup removed %4d autonomous objects.\n", Counter ); + // check + if ( !Abc_NtkCheck( pNtk ) ) + printf( "Abc_NtkCleanupSeq: The network check has failed.\n" ); + return 1; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 622b4103..594cc2d6 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -333,7 +333,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF printf( "Networks are NOT EQUIVALENT after framing.\n" ); // report the error pFrames->pModel = Abc_NtkVerifyGetCleanModel( pFrames, 1 ); - Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames ); +// Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames ); FREE( pFrames->pModel ); Abc_NtkDelete( pFrames ); return; @@ -365,7 +365,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF else if ( RetValue == 0 ) { printf( "Networks are NOT EQUIVALENT after fraiging.\n" ); - Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames ); +// Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames ); } else assert( 0 ); // delete the fraig manager diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c new file mode 100644 index 00000000..1d56ba36 --- /dev/null +++ b/src/base/abci/abcXsim.c @@ -0,0 +1,164 @@ +/**CFile**************************************************************** + + FileName [abcXsim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Using X-valued simulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcXsim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define XVS0 1 +#define XVS1 2 +#define XVSX 3 + +static inline void Abc_ObjSetXsim( Abc_Obj_t * pObj, int Value ) { pObj->pCopy = (void *)Value; } +static inline int Abc_ObjGetXsim( Abc_Obj_t * pObj ) { return (int)pObj->pCopy; } +static inline int Abc_XsimInv( int Value ) +{ + if ( Value == XVS0 ) + return XVS1; + if ( Value == XVS1 ) + return XVS0; + assert( Value == XVSX ); + return XVSX; +} +static inline int Abc_XsimAnd( int Value0, int Value1 ) +{ + if ( Value0 == XVS0 || Value1 == XVS0 ) + return XVS0; + if ( Value0 == XVSX || Value1 == XVSX ) + return XVSX; + assert( Value0 == XVS1 && Value1 == XVS1 ); + return XVS1; +} +static inline int Abc_XsimRand2() +{ + return (rand() & 1) ? XVS1 : XVS0; +} +static inline int Abc_XsimRand3() +{ + int RetValue; + do { + RetValue = rand() & 3; + } while ( RetValue == 0 ); + return RetValue; +} +static inline int Abc_ObjGetXsimFanin0( Abc_Obj_t * pObj ) +{ + int RetValue; + RetValue = Abc_ObjGetXsim(Abc_ObjFanin0(pObj)); + return Abc_ObjFaninC0(pObj)? Abc_XsimInv(RetValue) : RetValue; +} +static inline int Abc_ObjGetXsimFanin1( Abc_Obj_t * pObj ) +{ + int RetValue; + RetValue = Abc_ObjGetXsim(Abc_ObjFanin1(pObj)); + return Abc_ObjFaninC1(pObj)? Abc_XsimInv(RetValue) : RetValue; +} +static inline void Abc_XsimPrint( FILE * pFile, int Value ) +{ + if ( Value == XVS0 ) + { + fprintf( pFile, "0" ); + return; + } + if ( Value == XVS1 ) + { + fprintf( pFile, "1" ); + return; + } + assert( Value == XVSX ); + fprintf( pFile, "x" ); +} + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs X-valued simulation of the sequential network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose ) +{ + Abc_Obj_t * pObj; + int i, f; + assert( Abc_NtkIsStrash(pNtk) ); + srand( 0x12341234 ); + // start simulation + Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 ); + if ( fInputs ) + { + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_ObjSetXsim( pObj, XVSX ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) ); + } + else + { + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_ObjSetXsim( pObj, Abc_XsimRand2() ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjSetXsim( Abc_ObjFanout0(pObj), XVSX ); + } + // simulate and print the result + fprintf( stdout, "Frame : Inputs : Latches : Outputs\n" ); + for ( f = 0; f < nFrames; f++ ) + { + Abc_AigForEachAnd( pNtk, pObj, i ) + Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + Abc_ObjSetXsim( pObj, Abc_ObjGetXsimFanin0(pObj) ); + // print out + fprintf( stdout, "%2d : ", f ); + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) ); + fprintf( stdout, " : " ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_XsimPrint( stdout, Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) ); + fprintf( stdout, " : " ); + Abc_NtkForEachPo( pNtk, pObj, i ) + Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) ); + fprintf( stdout, "\n" ); + // assign input values + if ( fInputs ) + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_ObjSetXsim( pObj, XVSX ); + else + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_ObjSetXsim( pObj, Abc_XsimRand2() ); + // transfer the latch values + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) ); + } +} + +/////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/module.make b/src/base/abci/module.make index bb2ae1a0..50a40393 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -2,6 +2,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcAttach.c \ src/base/abci/abcAuto.c \ src/base/abci/abcBalance.c \ + src/base/abci/abcBmc.c \ src/base/abci/abcClpBdd.c \ src/base/abci/abcClpSop.c \ src/base/abci/abcCut.c \ @@ -37,4 +38,5 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcTiming.c \ src/base/abci/abcUnate.c \ src/base/abci/abcUnreach.c \ - src/base/abci/abcVerify.c + src/base/abci/abcVerify.c \ + src/base/abci/abcXsim.c -- cgit v1.2.3