diff options
Diffstat (limited to 'src/base/abci/abcDarUnfold2.c')
-rw-r--r-- | src/base/abci/abcDarUnfold2.c | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/src/base/abci/abcDarUnfold2.c b/src/base/abci/abcDarUnfold2.c new file mode 100644 index 00000000..bacda407 --- /dev/null +++ b/src/base/abci/abcDarUnfold2.c @@ -0,0 +1,69 @@ +/**Function************************************************************* + + Synopsis [Performs BDD-based reachability analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose , int); +Abc_Ntk_t * Abc_NtkDarUnfold2( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + int typeII_cnt = 0; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + if ( fStruct ){ + assert(0);//pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan ); + }else + pMan = Saig_ManDupUnfoldConstrsFunc2( pTemp = pMan, nFrames, nConfs, nProps, fOldAlgo, fVerbose , &typeII_cnt); + Aig_ManStop( pTemp ); + if ( pMan == NULL ) + return NULL; + // typeII_cnt = pMan->nConstrsTypeII; + pNtkAig = Abc_NtkFromAigPhase( pMan ); + pNtkAig->pName = Extra_UtilStrsav(pMan->pName); + pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec); + Aig_ManStop( pMan ); + + return Abc_NtkDarFold2(pNtkAig, 0, fVerbose, typeII_cnt); + + //return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Performs BDD-based reachability analysis.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarFold2( Abc_Ntk_t * pNtk, int fCompl, int fVerbose + , int typeII_cnt + ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + return NULL; + pMan = Saig_ManDupFoldConstrsFunc2( pTemp = pMan, fCompl, fVerbose, typeII_cnt ); + Aig_ManStop( pTemp ); + pNtkAig = Abc_NtkFromAigPhase( pMan ); + pNtkAig->pName = Extra_UtilStrsav(pMan->pName); + pNtkAig->pSpec = Extra_UtilStrsav(pMan->pSpec); + Aig_ManStop( pMan ); + return pNtkAig; +} + |