summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/hop/hop.h1
-rw-r--r--src/aig/hop/hopUtil.c47
-rw-r--r--src/aig/ivy/attr.h2
-rw-r--r--src/aig/ivy/ivy.h1
-rw-r--r--src/aig/ivy/ivyFraig.c43
5 files changed, 89 insertions, 5 deletions
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index a5d6e2e5..ce4cdfde 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -304,6 +304,7 @@ extern void Hop_ObjCollectMulti( Hop_Obj_t * pFunc, Vec_Ptr_t * vSupe
extern int Hop_ObjIsMuxType( Hop_Obj_t * pObj );
extern int Hop_ObjRecognizeExor( Hop_Obj_t * pObj, Hop_Obj_t ** ppFan0, Hop_Obj_t ** ppFan1 );
extern Hop_Obj_t * Hop_ObjRecognizeMux( Hop_Obj_t * pObj, Hop_Obj_t ** ppObjT, Hop_Obj_t ** ppObjE );
+extern void Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
extern void Hop_ObjPrintVerilog( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
extern void Hop_ObjPrintVerbose( Hop_Obj_t * pObj, int fHaig );
extern void Hop_ManPrintVerbose( Hop_Man_t * p, int fHaig );
diff --git a/src/aig/hop/hopUtil.c b/src/aig/hop/hopUtil.c
index 738caa4a..a49e8397 100644
--- a/src/aig/hop/hopUtil.c
+++ b/src/aig/hop/hopUtil.c
@@ -283,6 +283,53 @@ Hop_Obj_t * Hop_ObjRecognizeMux( Hop_Obj_t * pNode, Hop_Obj_t ** ppNodeT, Hop_Ob
/**Function*************************************************************
+ Synopsis [Prints Eqn formula for the AIG rooted at this node.]
+
+ Description [The formula is in terms of PIs, which should have
+ their names assigned in pObj->pData fields.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Hop_ObjPrintEqn( FILE * pFile, Hop_Obj_t * pObj, Vec_Vec_t * vLevels, int Level )
+{
+ Vec_Ptr_t * vSuper;
+ Hop_Obj_t * pFanin;
+ int fCompl, i;
+ // store the complemented attribute
+ fCompl = Hop_IsComplement(pObj);
+ pObj = Hop_Regular(pObj);
+ // constant case
+ if ( Hop_ObjIsConst1(pObj) )
+ {
+ fprintf( pFile, "%d", !fCompl );
+ return;
+ }
+ // PI case
+ if ( Hop_ObjIsPi(pObj) )
+ {
+ fprintf( pFile, "%s%s", fCompl? "!" : "", pObj->pData );
+ return;
+ }
+ // AND case
+ Vec_VecExpand( vLevels, Level );
+ vSuper = Vec_VecEntry(vLevels, Level);
+ Hop_ObjCollectMulti( pObj, vSuper );
+ fprintf( pFile, "%s", (Level==0? "" : "(") );
+ Vec_PtrForEachEntry( vSuper, pFanin, i )
+ {
+ Hop_ObjPrintEqn( pFile, Hop_NotCond(pFanin, fCompl), vLevels, Level+1 );
+ if ( i < Vec_PtrSize(vSuper) - 1 )
+ fprintf( pFile, " %s ", fCompl? "+" : "*" );
+ }
+ fprintf( pFile, "%s", (Level==0? "" : ")") );
+ return;
+}
+
+/**Function*************************************************************
+
Synopsis [Prints Verilog formula for the AIG rooted at this node.]
Description [The formula is in terms of PIs, which should have
diff --git a/src/aig/ivy/attr.h b/src/aig/ivy/attr.h
index 5a760239..16cf0b84 100644
--- a/src/aig/ivy/attr.h
+++ b/src/aig/ivy/attr.h
@@ -193,7 +193,7 @@ static inline void Attr_ManStop( Attr_Man_t * p )
p->pFuncFreeMan( p->pManAttr );
// free the memory manager
if ( p->pManMem )
- Extra_MmFixedStop( p->pManMem, 0 );
+ Extra_MmFixedStop( p->pManMem);
// free the attribute manager
FREE( p->pAttrs );
free( p );
diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h
index f48466ef..9e944028 100644
--- a/src/aig/ivy/ivy.h
+++ b/src/aig/ivy/ivy.h
@@ -268,6 +268,7 @@ static inline Ivy_Obj_t * Ivy_ObjChild0( Ivy_Obj_t * pObj ) { return pObj-
static inline Ivy_Obj_t * Ivy_ObjChild1( Ivy_Obj_t * pObj ) { return pObj->pFanin1; }
static inline Ivy_Obj_t * Ivy_ObjChild0Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin0(pObj)? Ivy_NotCond(Ivy_ObjFanin0(pObj)->pEquiv, Ivy_ObjFaninC0(pObj)) : NULL; }
static inline Ivy_Obj_t * Ivy_ObjChild1Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL; }
+static inline Ivy_Obj_t * Ivy_ObjEquiv( Ivy_Obj_t * pObj ) { return Ivy_Regular(pObj)->pEquiv? Ivy_NotCond(Ivy_Regular(pObj)->pEquiv, Ivy_IsComplement(pObj)) : NULL; }
static inline int Ivy_ObjLevel( Ivy_Obj_t * pObj ) { return pObj->Level; }
static inline int Ivy_ObjLevelNew( Ivy_Obj_t * pObj ) { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); }
static inline int Ivy_ObjFaninPhase( Ivy_Obj_t * pObj ) { return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; }
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 269ca257..ce21c269 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -752,6 +752,26 @@ int Ivy_NodeHasZeroSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
/**Function*************************************************************
+ Synopsis [Returns 1 if simulation info is composed of all zeros.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ivy_NodeComplementSim( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
+{
+ Ivy_FraigSim_t * pSims;
+ int i;
+ pSims = Ivy_ObjSim(pObj);
+ for ( i = 0; i < p->nSimWords; i++ )
+ pSims->pData[i] = ~pSims->pData[i];
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if simulation infos are equal.]
Description []
@@ -1277,7 +1297,11 @@ void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj )
// fill in the counter-example data
pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
Ivy_ManForEachPi( p->pManAig, pObj, i )
+ {
pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat);
+// printf( "%d", pModel[i] );
+ }
+// printf( "\n" );
// set the model
assert( p->pManFraig->pData == NULL );
p->pManFraig->pData = pModel;
@@ -1299,13 +1323,25 @@ int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p )
{
Ivy_Obj_t * pObj;
int i;
+ // make sure the reference simulation pattern does not detect the bug
+ pObj = Ivy_ManPo( p->pManAig, 0 );
+ assert( Ivy_ObjFanin0(pObj)->fPhase == (unsigned)Ivy_ObjFaninC0(pObj) ); // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) == 0
Ivy_ManForEachPo( p->pManAig, pObj, i )
+ {
+ // complement simulation info
+// if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) ) // Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj))
+// Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
+ // check
if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) )
{
// create the counter-example from this pattern
Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) );
return 1;
}
+ // complement simulation info
+// if ( Ivy_ObjFanin0(pObj)->fPhase ^ Ivy_ObjFaninC0(pObj) )
+// Ivy_NodeComplementSim( p, Ivy_ObjFanin0(pObj) );
+ }
return 0;
}
@@ -1819,6 +1855,9 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p )
{
if ( fVerbose )
printf( "Output %2d (out of %2d) is constant 1. ", i, Ivy_ManPoNum(p->pManAig) );
+ // assing constant 0 model
+ p->pManFraig->pData = ALLOC( int, Ivy_ManPiNum(p->pManFraig) );
+ memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) );
break;
}
// check if the output is constant 0
@@ -1957,10 +1996,6 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
(!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
{
-// if ( Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1 )
-// {
-// int x = 0;
-// }
assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
assert( pObjNew != Ivy_Regular(pFanin0New) );
assert( pObjNew != Ivy_Regular(pFanin1New) );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 18:45:14 +0000