diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 20 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 42 |
2 files changed, 52 insertions, 10 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0db761c7..a0d26e3b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7684,7 +7684,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk; -// Abc_Ntk_t * pNtkRes; + Abc_Ntk_t * pNtkRes = NULL; int c; int fBmc; int nFrames; @@ -7712,6 +7712,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose ); extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk ); // extern void Aig_ProcedureTest(); + extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); @@ -7912,14 +7914,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); -*//* - - if ( argc != globalUtilOptind + 1 ) - goto usage; - pFileName = argv[globalUtilOptind]; - Nwk_ManLutMergeGraphTest( pFileName ); */ -// Aig_ProcedureTest(); + + pNtkRes = Abc_NtkDarTestNtk( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; usage: diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index f1e5efb0..388fc5df 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2351,20 +2351,58 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio ***********************************************************************/ void Abc_NtkDarTest( Abc_Ntk_t * pNtk ) { - Aig_Man_t * pMan; + extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ); + + Aig_Man_t * pMan, * pTemp; assert( Abc_NtkIsStrash(pNtk) ); pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return; - +/* Aig_ManSetRegNum( pMan, pMan->nRegs ); Aig_ManPrintStats( pMan ); Saig_ManDumpBlif( pMan, "_temp_.blif" ); Aig_ManStop( pMan ); pMan = Saig_ManReadBlif( "_temp_.blif" ); Aig_ManPrintStats( pMan ); +*/ + Aig_ManSetRegNum( pMan, pMan->nRegs ); + pTemp = Ssw_SignalCorrespondeceTestPairs( pMan ); + Aig_ManStop( pTemp ); + Aig_ManStop( pMan ); +} +/**Function************************************************************* + + Synopsis [Performs BDD-based reachability analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk ) +{ + extern Aig_Man_t * Ssw_SignalCorrespondeceTestPairs( Aig_Man_t * pAig ); + + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + + Aig_ManSetRegNum( pMan, pMan->nRegs ); + pMan = Ssw_SignalCorrespondeceTestPairs( pTemp = pMan ); + Aig_ManStop( pTemp ); + + pNtkAig = Abc_NtkFromAigPhase( pMan ); + pNtkAig->pName = Extra_UtilStrsav(pNtk->pName); + pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec); Aig_ManStop( pMan ); + return pNtkAig; } //////////////////////////////////////////////////////////////////////// |