diff options
Diffstat (limited to 'src/base/abci/abcDar.c')
-rw-r--r-- | src/base/abci/abcDar.c | 122 |
1 files changed, 14 insertions, 108 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index dbd461c4..ca33667f 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -702,35 +702,6 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkDarSatSweep( Abc_Ntk_t * pNtk, Cec_ParCsw_t * pPars ) -{ -/* - extern Aig_Man_t * Cec_ManSatSweep( Aig_Man_t * pAig, Cec_ParCsw_t * pPars ); - Abc_Ntk_t * pNtkAig; - Aig_Man_t * pMan, * pTemp; - pMan = Abc_NtkToDar( pNtk, 0, 0 ); - if ( pMan == NULL ) - return NULL; - pMan = Cec_ManSatSweep( pTemp = pMan, pPars ); - Aig_ManStop( pTemp ); - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); - Aig_ManStop( pMan ); - return pNtkAig; - */ - return NULL; -} - -/**Function************************************************************* - - Synopsis [Gives the current ABC network to AIG manager for processing.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose ) { Abc_Ntk_t * pNtkAig; @@ -1184,7 +1155,17 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPa Aig_Man_t * pMan, * pMan1, * pMan2; Abc_Ntk_t * pMiter; int RetValue, clkTotal = clock(); - +/* + { + extern void Cec_ManVerifyTwoAigs( Aig_Man_t * pAig0, Aig_Man_t * pAig1, int fVerbose ); + Aig_Man_t * pAig0 = Abc_NtkToDar( pNtk1, 0, 0 ); + Aig_Man_t * pAig1 = Abc_NtkToDar( pNtk2, 0, 0 ); + Cec_ManVerifyTwoAigs( pAig0, pAig1, 1 ); + Aig_ManStop( pAig0 ); + Aig_ManStop( pAig1 ); + return 1; + } +*/ // cannot partition if it is already a miter if ( pNtk2 == NULL && fPartition == 1 ) { @@ -1285,82 +1266,6 @@ ABC_PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarCec2( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Cec_ParCec_t * pPars ) -{ - Aig_Man_t * pMan1, * pMan2 = NULL; - int RetValue, clkTotal = clock(); - if ( pNtk2 ) - { - if ( Abc_NtkPiNum(pNtk1) != Abc_NtkPiNum(pNtk2) ) - { - printf( "Networks have different number of PIs.\n" ); - return -1; - } - if ( Abc_NtkPoNum(pNtk1) != Abc_NtkPoNum(pNtk2) ) - { - printf( "Networks have different number of POs.\n" ); - return -1; - } - } - if ( pNtk1 ) - { - pMan1 = Abc_NtkToDar( pNtk1, 0, 0 ); - if ( pMan1 == NULL ) - { - printf( "Converting into AIG has failed.\n" ); - return -1; - } - } - if ( pNtk2 ) - { - pMan2 = Abc_NtkToDar( pNtk2, 0, 0 ); - if ( pMan2 == NULL ) - { - Aig_ManStop( pMan1 ); - printf( "Converting into AIG has failed.\n" ); - return -1; - } - } - // perform verification -// RetValue = Cec_Solve( pMan1, pMan2, pPars ); - RetValue = -1; - // transfer model if given - pNtk1->pModel = pMan1->pData, pMan1->pData = NULL; - Aig_ManStop( pMan1 ); - if ( pMan2 ) - Aig_ManStop( pMan2 ); - - // report the miter - if ( RetValue == 1 ) - { - printf( "Networks are equivalent. " ); -ABC_PRT( "Time", clock() - clkTotal ); - } - else if ( RetValue == 0 ) - { - printf( "Networks are NOT EQUIVALENT. " ); -ABC_PRT( "Time", clock() - clkTotal ); - } - else - { - printf( "Networks are UNDECIDED. " ); -ABC_PRT( "Time", clock() - clkTotal ); - } - fflush( stdout ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Gives the current ABC network to AIG manager for processing.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, Fra_Ssw_t * pPars ) { Fraig_Params_t Params; @@ -1797,8 +1702,8 @@ int Abc_NtkDarDemiter( Abc_Ntk_t * pNtk ) Aig_ManStop( pPart1 ); Aig_ManStop( pMan ); return 1; -} - +} + /**Function************************************************************* Synopsis [Gives the current ABC network to AIG manager for processing.] @@ -1826,6 +1731,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) Abc_NtkMakeComb( pNtkComb, 1 ); // solve it using combinational equivalence checking Prove_ParamsSetDefault( pParams ); + pParams->fVerbose = 1; RetValue = Abc_NtkIvyProve( &pNtkComb, pParams ); // transfer model if given // pNtk->pModel = pNtkComb->pModel; pNtkComb->pModel = NULL; |