diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-12-08 08:01:00 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-12-08 08:01:00 -0800 |
| commit | 65687f72ae77440628c21d63966656c1049c4981 (patch) | |
| tree | 27a4c7800e372349f1521daac76c0b30e2578ca1 /src/base/abci/abcDar.c | |
| parent | 369f008e69a4f201cbc7c890a08221086bee4698 (diff) | |
| download | abc-65687f72ae77440628c21d63966656c1049c4981.tar.gz abc-65687f72ae77440628c21d63966656c1049c4981.tar.bz2 abc-65687f72ae77440628c21d63966656c1049c4981.zip | |
Version abc71208
Diffstat (limited to 'src/base/abci/abcDar.c')
| -rw-r--r-- | src/base/abci/abcDar.c | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 67f22eb7..e23b04dd 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -56,12 +56,20 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) ); Abc_NtkForEachCi( pNtk, pObj, i ) if ( i < Abc_NtkPiNum(pNtk) ) + { assert( Abc_ObjIsPi(pObj) ); + if ( !Abc_ObjIsPi(pObj) ) + printf( "Abc_NtkToDar(): Temporary bug: The PI ordering is wrong!\n" ); + } else assert( Abc_ObjIsBo(pObj) ); Abc_NtkForEachCo( pNtk, pObj, i ) if ( i < Abc_NtkPoNum(pNtk) ) + { assert( Abc_ObjIsPo(pObj) ); + if ( !Abc_ObjIsPo(pObj) ) + printf( "Abc_NtkToDar(): Temporary bug: The PO ordering is wrong!\n" ); + } else assert( Abc_ObjIsBi(pObj) ); // print warning about initial values @@ -1401,9 +1409,10 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose ) SeeAlso [] ***********************************************************************/ -int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) +int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose ) { - extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose ); + extern int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose ); + extern int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nClauses, int fBmc, int fVerbose, int fVeryVerbose ); Aig_Man_t * pMan; if ( Abc_NtkPoNum(pNtk) != 1 ) { @@ -1418,7 +1427,8 @@ int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ) Vec_IntFree( pMan->vFlopNums ); pMan->vFlopNums = NULL; - Fra_Clau( pMan, nStepsMax, fVerbose ); +// Fra_Clau( pMan, nStepsMax, fVerbose, fVeryVerbose ); + Fra_Claus( pMan, nFrames, nStepsMax, fBmc, fVerbose, fVeryVerbose ); Aig_ManStop( pMan ); return 1; } |