summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcDar.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcDar.c')
-rw-r--r--src/base/abci/abcDar.c16
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;
}