summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcQuant.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcQuant.c')
-rw-r--r--src/base/abci/abcQuant.c11
1 files changed, 7 insertions, 4 deletions
diff --git a/src/base/abci/abcQuant.c b/src/base/abci/abcQuant.c
index 8591663e..0f2bd72f 100644
--- a/src/base/abci/abcQuant.c
+++ b/src/base/abci/abcQuant.c
@@ -72,7 +72,7 @@ void Abc_NtkSynthesize( Abc_Ntk_t ** ppNtk, int fMoreEffort )
SeeAlso []
***********************************************************************/
-int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose )
+int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int fUniv, int iVar, int fVerbose )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj, * pNext, * pFanin;
@@ -112,7 +112,10 @@ int Abc_NtkQuantify( Abc_Ntk_t * pNtk, int iVar, int fVerbose )
continue;
pFanin = Abc_ObjFanin0(pObj);
// get the result of quantification
- pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
+ if ( fUniv )
+ pNext = Abc_AigAnd( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
+ else
+ pNext = Abc_AigOr( pNtk->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild0Data(pObj) );
pNext = Abc_ObjNotCond( pNext, Abc_ObjFaninC0(pObj) );
if ( Abc_ObjRegular(pNext) == pFanin )
continue;
@@ -197,7 +200,7 @@ Abc_Ntk_t * Abc_NtkTransRel( Abc_Ntk_t * pNtk, int fInputs, int fVerbose )
for ( i = Abc_NtkPiNum(pNtkNew) - 1; i >= 2*nLatches; i-- )
// for ( i = 2*nLatches; i < Abc_NtkPiNum(pNtkNew); i++ )
{
- Abc_NtkQuantify( pNtkNew, i, fVerbose );
+ Abc_NtkQuantify( pNtkNew, 0, i, fVerbose );
// if ( fSynthesis && (i % 3 == 2) )
if ( fSynthesis )
{
@@ -339,7 +342,7 @@ Abc_Ntk_t * Abc_NtkReachability( Abc_Ntk_t * pNtkRel, int nIters, int fVerbose )
// quantify the current state variables
for ( v = 0; v < nVars; v++ )
{
- Abc_NtkQuantify( pNtkNext, v, fVerbose );
+ Abc_NtkQuantify( pNtkNext, 0, v, fVerbose );
if ( fSynthesis && (v % 3 == 2) )
{
Abc_NtkCleanData( pNtkNext );