From 9e4213e202b516c6c920d7e0faaf603273d1795d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 17 Aug 2007 08:01:00 -0700 Subject: Version abc70817 --- src/base/abc/abcNtk.c | 83 ++++++++++++ src/base/abci/abc.c | 327 +++++++++++++++++++++++++++++++++++++++++---- src/base/abci/abcDar.c | 238 ++++++++++++++++++++++++++------- src/base/abci/abcMiter.c | 1 + src/base/abci/abcPrint.c | 2 +- src/base/abci/abcVerify.c | 2 +- src/base/abci/abcXsim.c | 4 + src/base/io/ioReadAiger.c | 123 +++++++++-------- src/base/io/ioWriteAiger.c | 6 + 9 files changed, 660 insertions(+), 126 deletions(-) (limited to 'src/base') diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 7d8d0f0f..00d8911b 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -1086,6 +1086,89 @@ void Abc_NtkMakeComb( Abc_Ntk_t * pNtk ) } +/**Function************************************************************* + + Synopsis [Removes POs with suppsize less than 2 and PIs without fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i, k, m; + + // filter POs + k = m = 0; + Abc_NtkForEachCo( pNtk, pObj, i ) + { + if ( Abc_ObjIsPo(pObj) ) + { + // remove constant nodes and PI pointers + if ( Abc_ObjFaninNum(Abc_ObjFanin0(pObj)) == 0 ) + { + Abc_ObjDeleteFanin( pObj, Abc_ObjFanin0(pObj) ); + if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) == 0 && !Abc_ObjIsPi(Abc_ObjFanin0(pObj)) ) + Abc_NtkDeleteObj_rec( Abc_ObjFanin0(pObj), 1 ); + pNtk->vObjs->pArray[pObj->Id] = NULL; + pObj->Id = (1<<26)-1; + pNtk->nObjCounts[pObj->Type]--; + pNtk->nObjs--; + Abc_ObjRecycle( pObj ); + continue; + } + // remove buffers/inverters of PIs + if ( Abc_ObjFaninNum(Abc_ObjFanin0(pObj)) == 1 ) + { + if ( Abc_ObjIsPi(Abc_ObjFanin0(Abc_ObjFanin0(pObj))) ) + { + Abc_ObjDeleteFanin( pObj, Abc_ObjFanin0(pObj) ); + if ( Abc_ObjFanoutNum(Abc_ObjFanin0(pObj)) == 0 ) + Abc_NtkDeleteObj_rec( Abc_ObjFanin0(pObj), 1 ); + pNtk->vObjs->pArray[pObj->Id] = NULL; + pObj->Id = (1<<26)-1; + pNtk->nObjCounts[pObj->Type]--; + pNtk->nObjs--; + Abc_ObjRecycle( pObj ); + continue; + } + } + Vec_PtrWriteEntry( pNtk->vPos, m++, pObj ); + } + Vec_PtrWriteEntry( pNtk->vCos, k++, pObj ); + } + Vec_PtrShrink( pNtk->vPos, m ); + Vec_PtrShrink( pNtk->vCos, k ); + + // filter PIs + k = m = 0; + Abc_NtkForEachCi( pNtk, pObj, i ) + { + if ( Abc_ObjIsPi(pObj) ) + { + if ( Abc_ObjFanoutNum(pObj) == 0 ) + { + pNtk->vObjs->pArray[pObj->Id] = NULL; + pObj->Id = (1<<26)-1; + pNtk->nObjCounts[pObj->Type]--; + pNtk->nObjs--; + Abc_ObjRecycle( pObj ); + continue; + } + Vec_PtrWriteEntry( pNtk->vPis, m++, pObj ); + } + Vec_PtrWriteEntry( pNtk->vCis, k++, pObj ); + } + Vec_PtrShrink( pNtk->vPis, m ); + Vec_PtrShrink( pNtk->vCis, k ); + + return Abc_NtkDup( pNtk ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// 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 ); @@ -11443,6 +11627,97 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + 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] \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 [] 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 @@ -143,6 +147,59 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) return pNtkNew; } +/**Function************************************************************* + + 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.] @@ -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) ); diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index 23b5b350..be80dc82 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -121,8 +121,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) Abc_ObjAddFanin( pNode1, pObj ); Vec_PtrPush( vNodes, pNode1 ); // assign names to latch and its input - Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL ); - +// Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL ); // printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id ); } @@ -142,7 +141,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) uLit = ((i + 1 + nInputs + nLatches) << 1); uLit1 = uLit - Io_ReadAigerDecode( &pCur ); uLit0 = uLit1 - Io_ReadAigerDecode( &pCur ); - assert( uLit1 > uLit0 ); +// assert( uLit1 > uLit0 ); pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); pNode1 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches ); @@ -171,66 +170,84 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); Abc_ObjAddFanin( pObj, pNode0 ); } - + // read the names if present pCur = pSymbols; - while ( pCur < pContents + nFileSize && *pCur != 'c' ) + if ( *pCur != 'c' ) { - // get the terminal type - pType = pCur; - if ( *pCur == 'i' ) - vTerms = pNtkNew->vPis; - else if ( *pCur == 'l' ) - vTerms = pNtkNew->vBoxes; - else if ( *pCur == 'o' ) - vTerms = pNtkNew->vPos; - else + int Counter = 0; + while ( pCur < pContents + nFileSize && *pCur != 'c' ) + { + // get the terminal type + pType = pCur; + if ( *pCur == 'i' ) + vTerms = pNtkNew->vPis; + else if ( *pCur == 'l' ) + vTerms = pNtkNew->vBoxes; + else if ( *pCur == 'o' ) + vTerms = pNtkNew->vPos; + else + { + fprintf( stdout, "Wrong terminal type.\n" ); + return NULL; + } + // get the terminal number + iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' ); + // get the node + if ( iTerm >= Vec_PtrSize(vTerms) ) + { + fprintf( stdout, "The number of terminal is out of bound.\n" ); + return NULL; + } + pObj = Vec_PtrEntry( vTerms, iTerm ); + if ( *pType == 'l' ) + pObj = Abc_ObjFanout0(pObj); + // assign the name + pName = pCur; while ( *pCur++ != '\n' ); + // assign this name + *(pCur-1) = 0; + Abc_ObjAssignName( pObj, pName, NULL ); + if ( *pType == 'l' ) + { + Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" ); + Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" ); + } + // mark the node as named + pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); + } + + // assign the remaining names + Abc_NtkForEachPi( pNtkNew, pObj, i ) { - fprintf( stdout, "Wrong terminal type.\n" ); - return NULL; + if ( pObj->pCopy ) continue; + Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); + Counter++; } - // get the terminal number - iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' ); - // get the node - if ( iTerm >= Vec_PtrSize(vTerms) ) + Abc_NtkForEachLatchOutput( pNtkNew, pObj, i ) { - fprintf( stdout, "The number of terminal is out of bound.\n" ); - return NULL; + if ( pObj->pCopy ) continue; + Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); + Abc_ObjAssignName( Abc_ObjFanin0(pObj), Abc_ObjName(pObj), "L" ); + Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "_in" ); + Counter++; } - pObj = Vec_PtrEntry( vTerms, iTerm ); - if ( *pType == 'l' ) - pObj = Abc_ObjFanout0(pObj); - // assign the name - pName = pCur; while ( *pCur++ != '\n' ); - // assign this name - *(pCur-1) = 0; - Abc_ObjAssignName( pObj, pName, NULL ); - if ( *pType == 'l' ) - Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" ); - // mark the node as named - pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); - } - // skipping the comments - free( pContents ); - Vec_PtrFree( vNodes ); - - // assign the remaining names - Abc_NtkForEachPi( pNtkNew, pObj, i ) - { - if ( pObj->pCopy ) continue; - Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); - } - Abc_NtkForEachLatchOutput( pNtkNew, pObj, i ) - { - if ( pObj->pCopy ) continue; - Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); - Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), NULL ); + Abc_NtkForEachPo( pNtkNew, pObj, i ) + { + if ( pObj->pCopy ) continue; + Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); + Counter++; + } + if ( Counter ) + printf( "Io_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter ); } - Abc_NtkForEachPo( pNtkNew, pObj, i ) + else { - if ( pObj->pCopy ) continue; - Abc_ObjAssignName( pObj, Abc_ObjName(pObj), NULL ); +// printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" ); + Abc_NtkShortNames( pNtkNew ); } + // skipping the comments + free( pContents ); + Vec_PtrFree( vNodes ); // remove the extra nodes Abc_AigCleanup( pNtkNew->pManFunc ); diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 7c9da184..958e3d96 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -163,6 +163,12 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) fprintf( stdout, "Io_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName ); return; } + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( !Abc_LatchIsInit0(pObj) ) + { + fprintf( stdout, "Io_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" ); + return; + } // set the node numbers to be used in the output file nNodes = 0; -- cgit v1.2.3