diff options
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 327 | ||||
| -rw-r--r-- | src/base/abci/abcDar.c | 238 | ||||
| -rw-r--r-- | src/base/abci/abcMiter.c | 1 | ||||
| -rw-r--r-- | src/base/abci/abcPrint.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abcVerify.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abcXsim.c | 4 |
6 files changed, 501 insertions, 73 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3a916fdc..1b5e2361 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -93,6 +93,7 @@ static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandNode ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTopmost ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTrim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -171,6 +172,7 @@ static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -257,6 +259,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandCone, 1 ); Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandNode, 1 ); Cmd_CommandAdd( pAbc, "Various", "topmost", Abc_CommandTopmost, 1 ); + Cmd_CommandAdd( pAbc, "Various", "trim", Abc_CommandTrim, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 ); Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 ); @@ -335,6 +338,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "dsec", Abc_CommandDSec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); @@ -5134,6 +5138,84 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTrim( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c, nLevels; + extern Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nLevels = 10; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF ) + { + switch ( c ) + { +/* + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nLevels = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLevels < 0 ) + goto usage; + break; +*/ + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for logic circuits.\n" ); + return 0; + } + + pNtkRes = Abc_NtkTrim( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "The command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: trim [-h]\n" ); + fprintf( pErr, "\t removes POs fed by PIs and constants, and PIs w/o fanout\n" ); +// fprintf( pErr, "\t-N num : max number of levels [default = %d]\n", nLevels ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -6085,6 +6167,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ); + extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -6200,10 +6284,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Network should be strashed. Command has failed.\n" ); return 1; } -// pNtkRes = Abc_NtkDar( pNtk ); - pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); */ - pNtkRes = NULL; + + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + +// pNtkRes = Abc_NtkDar( pNtk ); + pNtkRes = Abc_NtkDarRetime( pNtk, 100, 1 ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -6211,7 +6301,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); - return 0; usage: fprintf( pErr, "usage: test [-h]\n" ); @@ -6627,6 +6716,11 @@ int Abc_CommandICut( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } Abc_NtkIvyCuts( pNtk, nInputs ); return 0; @@ -6690,6 +6784,11 @@ int Abc_CommandIRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvyRewrite( pNtk, fUpdateLevel, fUseZeroCost, fVerbose ); if ( pNtkRes == NULL ) @@ -6790,6 +6889,11 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkDRewrite( pNtk, pPars ); if ( pNtkRes == NULL ) { @@ -6904,6 +7008,11 @@ int Abc_CommandDRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } if ( pPars->nLeafMax < 4 || pPars->nLeafMax > 15 ) { fprintf( pErr, "This command only works for cut sizes 4 <= K <= 15.\n" ); @@ -6986,6 +7095,11 @@ int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkDCompress2( pNtk, fBalance, fUpdateLevel, fVerbose ); if ( pNtkRes == NULL ) { @@ -7054,6 +7168,11 @@ int Abc_CommandDrwsat( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkDrwsat( pNtk, fBalance, fVerbose ); if ( pNtkRes == NULL ) { @@ -7124,6 +7243,11 @@ int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvyRewriteSeq( pNtk, fUseZeroCost, fVerbose ); if ( pNtkRes == NULL ) @@ -7192,6 +7316,11 @@ int Abc_CommandIResyn( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvyResyn( pNtk, fUpdateLevel, fVerbose ); if ( pNtkRes == NULL ) @@ -7273,6 +7402,11 @@ int Abc_CommandISat( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvySat( pNtk, nConfLimit, fVerbose ); if ( pNtkRes == NULL ) @@ -7359,6 +7493,11 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose ); if ( pNtkRes == NULL ) @@ -7453,6 +7592,11 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fChoicing, fVerbose ); if ( pNtkRes == NULL ) @@ -7557,6 +7701,11 @@ int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "The number of leaves is infeasible.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkCSweep( pNtk, nCutsMax, nLeafMax, fVerbose ); if ( pNtkRes == NULL ) @@ -7728,6 +7877,11 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Empty network.\n" ); return 1; } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose ); if ( pNtkRes == NULL ) @@ -10417,9 +10571,10 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, nMaxIters; int fForward; int fBackward; + int fOneStep; int fVerbose; int Mode; - extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose ); + extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fOneStep, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -10429,10 +10584,11 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) Mode = 5; fForward = 0; fBackward = 0; + fOneStep = 0; fVerbose = 0; nMaxIters = 15; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbsvh" ) ) != EOF ) { switch ( c ) { @@ -10453,6 +10609,9 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': fBackward ^= 1; break; + case 's': + fOneStep ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -10497,7 +10656,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) // convert the network into an SOP network pNtkRes = Abc_NtkToLogic( pNtk ); // perform the retiming - Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fVerbose ); + Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fOneStep, fVerbose ); // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; @@ -10517,7 +10676,7 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) } // perform the retiming - Abc_NtkRetime( pNtk, Mode, fForward, fBackward, fVerbose ); + Abc_NtkRetime( pNtk, Mode, fForward, fBackward, fOneStep, fVerbose ); return 0; usage: @@ -10532,6 +10691,7 @@ usage: fprintf( pErr, "\t-M num : the retiming algorithm to use [default = %d]\n", Mode ); fprintf( pErr, "\t-f : enables forward-only retiming in modes 3,4,5 [default = %s]\n", fForward? "yes": "no" ); fprintf( pErr, "\t-b : enables backward-only retiming in modes 3,4,5 [default = %s]\n", fBackward? "yes": "no" ); + fprintf( pErr, "\t-s : enables retiming one step only in mode 4 [default = %s]\n", fOneStep? "yes": "no" ); fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -10816,21 +10976,23 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) int fExdc; int fImp; int fRewrite; + int fLatchCorr; int fVerbose; - extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fLatchCorr, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nFramesK = 1; - fExdc = 1; - fImp = 0; - fRewrite = 0; - fVerbose = 0; + nFramesK = 1; + fExdc = 1; + fImp = 0; + fRewrite = 0; + fLatchCorr = 0; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Feirvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Feirlvh" ) ) != EOF ) { switch ( c ) { @@ -10854,6 +11016,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRewrite ^= 1; break; + case 'l': + fLatchCorr ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -10883,7 +11048,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fVerbose ); + pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fLatchCorr, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -10894,11 +11059,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-F num] [-rvh]\n" ); + fprintf( pErr, "usage: ssweep [-F num] [-lrvh]\n" ); fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK ); // fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); // fprintf( pErr, "\t-i : toggle computing implications [default = %s]\n", fImp? "yes": "no" ); + fprintf( pErr, "\t-l : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" ); fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -10919,11 +11085,12 @@ usage: int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk; + Abc_Ntk_t * pNtk, * pNtkRes, * pTemp; int c; int fLatchSweep; int fAutoSweep; int fVerbose; + extern Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -10964,14 +11131,31 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } // modify the current network - Abc_NtkCleanupSeq( pNtk, fLatchSweep, fAutoSweep, fVerbose ); + + // get the new network + pNtkRes = Abc_NtkDup( pNtk ); + Abc_NtkCleanupSeq( pNtkRes, 0, fAutoSweep, fVerbose ); + if ( fLatchSweep ) + { + pNtkRes = Abc_NtkStrash( pTemp = pNtkRes, 0, 0, 0 ); + Abc_NtkDelete( pTemp ); + pNtkRes = Abc_NtkDarLatchSweep( pTemp = pNtkRes, fVerbose ); + Abc_NtkDelete( pTemp ); + } + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Sequential cleanup has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: fprintf( pErr, "usage: scleanup [-lavh]\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 - removes stuck-at and identical latches (latch sweep)\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-l : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" ); @@ -11402,17 +11586,17 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( Abc_NtkLatchNum(pNtk) == 0 ) - { - printf( "The network has no latches. Used combinational command \"cec\".\n" ); - return 0; - } - pArgvNew = argv + globalUtilOptind; nArgcNew = argc - globalUtilOptind; if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; + if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 ) + { + printf( "The network has no latches. Used combinational command \"cec\".\n" ); + return 0; + } + // perform equivalence checking if ( fRetime ) Abc_NtkSecRetime( pNtk1, pNtk2 ); @@ -11454,6 +11638,97 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtk1, * pNtk2; + int fDelete1, fDelete2; + char ** pArgvNew; + int nArgcNew; + int c; + int fVerbose; + int fVeryVerbose; + int nFrames; + + extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFrames = 0; // if 0, iterates through frames + fVerbose = 1; + fVeryVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Fwvh" ) ) != 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 'w': + fVeryVerbose ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + default: + goto usage; + } + } + + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) + return 1; + + if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 ) + { + printf( "The network has no latches. Used combinational command \"cec\".\n" ); + return 0; + } + + // perform verification + Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fVerbose, fVeryVerbose ); + + if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + return 0; + +usage: + fprintf( pErr, "usage: dsec [-F num] [-wvh] <file1> <file2>\n" ); + fprintf( pErr, "\t performs inductive sequential equivalence checking\n" ); + fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames ); + fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); + fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tfile1 : (optional) the file with the first network\n"); + fprintf( pErr, "\tfile2 : (optional) the file with the second network\n"); + fprintf( pErr, "\t if no files are given, uses the current network and its spec\n"); + fprintf( pErr, "\t if one file is given, uses the current network and the file\n"); + return 1; +} +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index ca80fec8..4013b98d 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -23,6 +23,7 @@ #include "dar.h" #include "cnf.h" #include "fra.h" +#include "fraig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -79,11 +80,13 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) if ( Abc_LatchIsInit1(pObj) ) Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy); // perform the conversion of the internal nodes (assumes DFS ordering) +// pMan->fAddStrash = 1; Abc_NtkForEachNode( pNtk, pObj, i ) { pObj->pCopy = (Abc_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj), (Aig_Obj_t *)Abc_ObjChild1Copy(pObj) ); // printf( "%d->%d ", pObj->Id, ((Aig_Obj_t *)pObj->pCopy)->Id ); } + pMan->fAddStrash = 0; // create the POs Abc_NtkForEachCo( pNtk, pObj, i ) Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) ); @@ -121,6 +124,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_Ntk_t * pNtkNew; Aig_Obj_t * pObj; int i; + assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) ); // perform strashing pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); // transfer the pointers to the basic nodes @@ -147,6 +151,59 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Synopsis [Converts the network from the AIG manager into ABC.] + Description [This procedure should be called after seq sweeping, + which changes the number of registers.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjNew; + Aig_Obj_t * pObj, * pObjLo, * pObjLi; + int i; +// assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) ); + // perform strashing + pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Aig_ManForEachPiSeq( pMan, pObj, i ) + pObj->pData = Abc_NtkCi(pNtkNew, i); + // create as many latches as there are registers in the manager + Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i ) + { + pObjNew = Abc_NtkCreateLatch( pNtkNew ); + pObjLi->pData = Abc_NtkCreateBi( pNtkNew ); + pObjLo->pData = Abc_NtkCreateBo( pNtkNew ); + Abc_ObjAddFanin( pObjNew, pObjLi->pData ); + Abc_ObjAddFanin( pObjLo->pData, pObjNew ); + Abc_LatchSetInit0( pObjNew ); + } + Abc_NtkAddDummyBoxNames( pNtkNew ); + // rebuild the AIG + vNodes = Aig_ManDfs( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + if ( Aig_ObjIsBuf(pObj) ) + pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj); + else + pObj->pData = Abc_AigAnd( pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) ); + Vec_PtrFree( vNodes ); + // connect the PO nodes + Aig_ManForEachPo( pMan, pObj, i ) + Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + Description [] SideEffects [] @@ -367,55 +424,23 @@ void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) { - Abc_Ntk_t * pNtkAig; - Aig_Man_t * pMan;//, * pTemp; -// int * pArray; + Abc_Ntk_t * pNtkAig = NULL; + Aig_Man_t * pMan; + extern void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim ); assert( Abc_NtkIsStrash(pNtk) ); // convert to the AIG manager pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; - if ( !Aig_ManCheck( pMan ) ) - { - printf( "Abc_NtkDar: AIG check has failed.\n" ); - Aig_ManStop( pMan ); - return NULL; - } - // perform balance - Aig_ManPrintStats( pMan ); -/* - pArray = Abc_NtkGetLatchValues(pNtk); - Aig_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray ); - free( pArray ); -*/ -// Aig_ManDumpBlif( pMan, "aig_temp.blif" ); -// pMan->pPars = Dar_ManDefaultRwrPars(); - Dar_ManRewrite( pMan, NULL ); - Aig_ManPrintStats( pMan ); -// Dar_ManComputeCuts( pMan ); - -/* -{ -extern Aig_Cnf_t * Aig_ManDeriveCnf( Aig_Man_t * p ); -extern void Aig_CnfFree( Aig_Cnf_t * pCnf ); -Aig_Cnf_t * pCnf; -pCnf = Aig_ManDeriveCnf( pMan ); -Aig_CnfFree( pCnf ); -} -*/ - - // convert from the AIG manager - if ( Aig_ManLatchNum(pMan) ) - pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan ); - else - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); - if ( pNtkAig == NULL ) - return NULL; + // perform computation +// Fra_ManPartitionTest( pMan, 4 ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); Aig_ManStop( pMan ); + // make sure everything is okay - if ( !Abc_NtkCheck( pNtkAig ) ) + if ( pNtkAig && !Abc_NtkCheck( pNtkAig ) ) { printf( "Abc_NtkDar: The network check has failed.\n" ); Abc_NtkDelete( pNtkAig ); @@ -867,23 +892,146 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fVerbose ) +Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; - pMan = Abc_NtkToDar( pNtk, 0 ); + pMan = Abc_NtkToDar( pNtk, 1 ); if ( pMan == NULL ) return NULL; - pMan->nRegs = Abc_NtkLatchNum(pNtk); +// pMan->nRegs = Abc_NtkLatchNum(pNtk); - pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fVerbose ); + pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fLatchCorr, fVerbose, NULL ); Aig_ManStop( pTemp ); - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) ) + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbose, int fVeryVerbose ) +{ + Fraig_Params_t Params; + Aig_Man_t * pMan; + Abc_Ntk_t * pMiter, * pTemp; + int RetValue; + + // get the miter of the two networks + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); + if ( pMiter == NULL ) + { + printf( "Miter computation has failed.\n" ); + return 0; + } + RetValue = Abc_NtkMiterIsConstant( pMiter ); + if ( RetValue == 0 ) + { + extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); + printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + // report the error + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames ); + Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames ); + FREE( pMiter->pModel ); + Abc_NtkDelete( pMiter ); + return 0; + } + if ( RetValue == 1 ) + { + Abc_NtkDelete( pMiter ); + printf( "Networks are equivalent after structural hashing.\n" ); + return 1; + } + + // preprocess the miter by fraiging it + // (note that for each functional class, fraiging leaves one representative; + // so fraiging does not reduce the number of functions represented by nodes + Fraig_ParamsSetDefault( &Params ); + pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 ); + Abc_NtkDelete( pTemp ); + + // derive the AIG manager + pMan = Abc_NtkToDar( pMiter, 1 ); + Abc_NtkDelete( pMiter ); + if ( pMan == NULL ) + { + printf( "Converting miter into AIG has failed.\n" ); + return -1; + } + assert( pMan->nRegs > 0 ); + + // perform verification + RetValue = Fra_FraigSec( pMan, nFrames, fVerbose, fVeryVerbose ); + Aig_ManStop( pMan ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return NULL; + pMan = Aig_ManReduceLaches( pMan, fVerbose ); + pMan = Aig_ManConstReduce( pMan, fVerbose ); + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); Aig_ManStop( pMan ); return pNtkAig; } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + pMan = Abc_NtkToDar( pNtk, 1 ); + if ( pMan == NULL ) + return NULL; + pMan = Rtm_ManRetimeFwd( pTemp = pMan, nStepsMax, fVerbose ); + Aig_ManStop( pTemp ); + +// pMan = Aig_ManReduceLaches( pMan, 1 ); +// pMan = Aig_ManConstReduce( pMan, 1 ); + + pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index a33b9875..5dc63750 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -98,6 +98,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb, in Abc_NtkMiterAddOne( pNtk1, pNtkMiter ); Abc_NtkMiterAddOne( pNtk2, pNtkMiter ); Abc_NtkMiterFinalize( pNtk1, pNtk2, pNtkMiter, fComb, nPartSize ); + Abc_AigCleanup(pNtkMiter->pManFunc); // make sure that everything is okay if ( !Abc_NtkCheck( pNtkMiter ) ) diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index ad8eec6a..4c061637 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -322,7 +322,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ) fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n", Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] ); fprintf( pFile, "Const fanin = %3d. DC init = %3d. Matching init = %3d. ", Counter0, Counter1, Counter2 ); - fprintf( pFile, "Self-feed latches = %2d.\n", Abc_NtkCountSelfFeedLatches(pNtk) ); + fprintf( pFile, "Self-feed latches = %2d.\n", -1 ); //Abc_NtkCountSelfFeedLatches(pNtk) ); } /**Function************************************************************* diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 63ba4843..67ecaae0 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -27,7 +27,7 @@ //////////////////////////////////////////////////////////////////////// static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel ); -static void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); +extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c index d17ab1dd..c05823da 100644 --- a/src/base/abci/abcXsim.c +++ b/src/base/abci/abcXsim.c @@ -139,7 +139,11 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) ); fprintf( stdout, " : " ); Abc_NtkForEachLatch( pNtk, pObj, i ) + { +// if ( Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) != XVSX ) +// printf( " %s=", Abc_ObjName(pObj) ); Abc_XsimPrint( stdout, Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) ); + } fprintf( stdout, " : " ); Abc_NtkForEachPo( pNtk, pObj, i ) Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) ); |