summaryrefslogtreecommitdiffstats
path: root/src/temp/ivy/ivyHaig.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/temp/ivy/ivyHaig.c')
-rw-r--r--src/temp/ivy/ivyHaig.c248
1 files changed, 211 insertions, 37 deletions
diff --git a/src/temp/ivy/ivyHaig.c b/src/temp/ivy/ivyHaig.c
index 7ce71a60..ca68c3c6 100644
--- a/src/temp/ivy/ivyHaig.c
+++ b/src/temp/ivy/ivyHaig.c
@@ -26,16 +26,17 @@
/*
HAIGing rules in working AIG:
- - The node points to the representative of its class
- - The pointer can be complemented if they have different polarity
+ - Each node in the working AIG has a pointer to the corresponding node in HAIG
+ (this node is not necessarily the representative of the equivalence class of HAIG nodes)
+ - This pointer is complemented if the AIG node and its corresponding HAIG node have different phase
Choice node rules in HAIG:
- Equivalent nodes are linked into a ring
- - Exactly one node in the ring has fanouts (this node is called representative)
- - Pointer going from a node to the next node in the ring is complemented
- if the first node is complemented, compared to the representative node
- - The representative node always has non-complemented pointer to the next node
- - New nodes are inserted into the ring before the representative node
+ - Exactly one node in the ring has fanouts (this node is called the representative)
+ - The pointer going from a node to the next node in the ring is complemented
+ if the first node is complemented, compared to the representative node of the equivalence class
+ - (consequence of the above) The representative node always has non-complemented pointer to the next node
+ - New nodes are inserted into the ring immediately after the representative node
*/
// returns the representative node of the given HAIG node
@@ -52,7 +53,7 @@ static inline Ivy_Obj_t * Ivy_HaigObjRepr( Ivy_Obj_t * pObj )
if ( Ivy_ObjRefs(pTemp) > 0 )
break;
// return the representative node
- assert( pTemp != pObj );
+ assert( Ivy_ObjRefs(pTemp) > 0 );
return Ivy_NotCond( pTemp, Ivy_IsComplement(pObj->pEquiv) );
}
@@ -65,8 +66,8 @@ static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj )
assert( Ivy_ObjRefs(pObj) > 0 );
if ( pObj->pEquiv == NULL )
return 1;
- Counter = 1;
assert( !Ivy_IsComplement(pObj->pEquiv) );
+ Counter = 1;
for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
Counter++;
return Counter;
@@ -87,10 +88,28 @@ static inline int Ivy_HaigObjCountClass( Ivy_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-void Ivy_ManHaigStart( Ivy_Man_t * p )
+void Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose )
{
+ Vec_Int_t * vLatches;
+ Ivy_Obj_t * pObj;
+ int i;
assert( p->pHaig == NULL );
p->pHaig = Ivy_ManDup( p );
+
+ if ( fVerbose )
+ {
+ printf( "Starting : " );
+ Ivy_ManPrintStats( p->pHaig );
+ }
+
+ // collect latches of design D and set their values to be DC
+ vLatches = Vec_IntAlloc( 100 );
+ Ivy_ManForEachLatch( p->pHaig, pObj, i )
+ {
+ pObj->Init = IVY_INIT_DC;
+ Vec_IntPush( vLatches, pObj->Id );
+ }
+ p->pHaig->pData = vLatches;
}
/**Function*************************************************************
@@ -131,6 +150,7 @@ void Ivy_ManHaigStop( Ivy_Man_t * p )
Ivy_Obj_t * pObj;
int i;
assert( p->pHaig != NULL );
+ Vec_IntFree( p->pHaig->pData );
Ivy_ManStop( p->pHaig );
p->pHaig = NULL;
// remove dangling pointers to the HAIG objects
@@ -151,17 +171,54 @@ void Ivy_ManHaigStop( Ivy_Man_t * p )
***********************************************************************/
void Ivy_ManHaigCreateObj( Ivy_Man_t * p, Ivy_Obj_t * pObj )
{
+ Ivy_Obj_t * pEquiv0, * pEquiv1;
assert( p->pHaig != NULL );
assert( !Ivy_IsComplement(pObj) );
if ( Ivy_ObjType(pObj) == IVY_BUF )
pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
else if ( Ivy_ObjType(pObj) == IVY_LATCH )
- pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
+ {
+// pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
+ pEquiv0 = Ivy_ObjChild0Equiv(pObj);
+ pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
+ pObj->pEquiv = Ivy_Latch( p->pHaig, pEquiv0, pObj->Init );
+ }
else if ( Ivy_ObjType(pObj) == IVY_AND )
- pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+ {
+// pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
+ pEquiv0 = Ivy_ObjChild0Equiv(pObj);
+ pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
+ pEquiv1 = Ivy_ObjChild1Equiv(pObj);
+ pEquiv1 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv1)), Ivy_IsComplement(pEquiv1) );
+ pObj->pEquiv = Ivy_And( p->pHaig, pEquiv0, pEquiv1 );
+ }
else assert( 0 );
// make sure the node points to the representative
- pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
+// pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Checks if the old node is in the TFI of the new node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ivy_ObjIsInTfi_rec( Ivy_Obj_t * pObjNew, Ivy_Obj_t * pObjOld, int Levels )
+{
+ if ( pObjNew == pObjOld )
+ return 1;
+ if ( Levels == 0 || Ivy_ObjIsCi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
+ return 0;
+ if ( Ivy_ObjIsInTfi_rec( Ivy_ObjFanin0(pObjNew), pObjOld, Levels - 1 ) )
+ return 1;
+ if ( Ivy_ObjIsNode(pObjNew) && Ivy_ObjIsInTfi_rec( Ivy_ObjFanin1(pObjNew), pObjOld, Levels - 1 ) )
+ return 1;
+ return 0;
}
/**Function*************************************************************
@@ -180,10 +237,16 @@ void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pO
Ivy_Obj_t * pObjOldHaig, * pObjNewHaig;
Ivy_Obj_t * pObjOldHaigR, * pObjNewHaigR;
int fCompl;
+//printf( "\nCreating choice for %d and %d in AIG\n", pObjOld->Id, Ivy_Regular(pObjNew)->Id );
+
assert( p->pHaig != NULL );
- // get pointers to the classes
+ assert( !Ivy_IsComplement(pObjOld) );
+ // get pointers to the representatives of pObjOld and pObjNew
pObjOldHaig = pObjOld->pEquiv;
pObjNewHaig = Ivy_NotCond( Ivy_Regular(pObjNew)->pEquiv, Ivy_IsComplement(pObjNew) );
+ // get the classes
+ pObjOldHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjOldHaig)), Ivy_IsComplement(pObjOldHaig) );
+ pObjNewHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjNewHaig)), Ivy_IsComplement(pObjNewHaig) );
// get regular pointers
pObjOldHaigR = Ivy_Regular(pObjOldHaig);
pObjNewHaigR = Ivy_Regular(pObjNewHaig);
@@ -192,17 +255,41 @@ void Ivy_ManHaigCreateChoice( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pO
// if the class is the same, nothing to do
if ( pObjOldHaigR == pObjNewHaigR )
return;
- // combine classes
- // assume the second node does not belong to a class
- assert( pObjNewHaigR->pEquiv == NULL );
+ // if the second node belongs to a class, do not merge classes (for the time being)
+ if ( Ivy_ObjRefs(pObjOldHaigR) == 0 || pObjNewHaigR->pEquiv != NULL ||
+ Ivy_ObjRefs(pObjNewHaigR) > 0 || Ivy_ObjIsInTfi_rec(pObjNewHaigR, pObjOldHaigR, 10) )
+ {
+/*
+ if ( pObjNewHaigR->pEquiv != NULL )
+ printf( "c" );
+ if ( Ivy_ObjRefs(pObjNewHaigR) > 0 )
+ printf( "f" );
+ printf( " " );
+*/
+ p->pHaig->nClassesSkip++;
+ return;
+ }
+
// add this node to the class of pObjOldHaig
+ assert( Ivy_ObjRefs(pObjOldHaigR) > 0 );
+ assert( !Ivy_IsComplement(pObjOldHaigR->pEquiv) );
if ( pObjOldHaigR->pEquiv == NULL )
pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl );
else
pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR->pEquiv, fCompl );
pObjOldHaigR->pEquiv = pObjNewHaigR;
+//printf( "Setting choice node %d -> %d.\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
// update the class of the new node
- Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
+// Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
+//printf( "Creating choice for %d and %d in HAIG\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
+
+// if ( pObjOldHaigR->Id == 13 )
+// {
+// Ivy_ManShow( p, 0 );
+// Ivy_ManShow( p->pHaig, 1 );
+// }
+// if ( !Ivy_ManIsAcyclic( p->pHaig ) )
+// printf( "HAIG contains a cycle\n" );
}
/**Function*************************************************************
@@ -227,17 +314,16 @@ int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices )
if ( Ivy_ObjIsTerm(pObj) || i == 0 )
continue;
if ( Ivy_ObjRefs(pObj) == 0 )
- {
- assert( pObj->pEquiv == Ivy_HaigObjRepr(pObj) );
continue;
- }
Counter = Ivy_HaigObjCountClass( pObj );
nChoiceNodes += (int)(Counter > 1);
nChoices += Counter - 1;
+// if ( Counter > 1 )
+// printf( "Choice node %d %s\n", pObj->Id, Ivy_ObjIsLatch(pObj)? "(latch)": "" );
}
*pnChoices = nChoices;
return nChoiceNodes;
-}
+}
/**Function*************************************************************
@@ -250,19 +336,35 @@ int Ivy_ManHaigCountChoices( Ivy_Man_t * p, int * pnChoices )
SeeAlso []
***********************************************************************/
-void Ivy_ManHaigPrintStats( Ivy_Man_t * p )
+void Ivy_ManHaigPostprocess( Ivy_Man_t * p, int fVerbose )
{
int nChoices, nChoiceNodes;
+
assert( p->pHaig != NULL );
- printf( "Original : " );
- Ivy_ManPrintStats( p );
- printf( "HAIG : " );
- Ivy_ManPrintStats( p->pHaig );
-
- // print choice node stats
- nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
- printf( "Total choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
- Ivy_ManHaigSimulate( p );
+
+ if ( fVerbose )
+ {
+ printf( "Final : " );
+ Ivy_ManPrintStats( p );
+ printf( "HAIG : " );
+ Ivy_ManPrintStats( p->pHaig );
+
+ // print choice node stats
+ nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
+ printf( "Total choice nodes = %d. Total choices = %d. Skipped classes = %d.\n",
+ nChoiceNodes, nChoices, p->pHaig->nClassesSkip );
+ }
+
+ if ( Ivy_ManIsAcyclic( p->pHaig ) )
+ {
+ if ( fVerbose )
+ printf( "HAIG is acyclic\n" );
+ }
+ else
+ printf( "HAIG contains a cycle\n" );
+
+ if ( fVerbose )
+ Ivy_ManHaigSimulate( p );
}
@@ -289,6 +391,32 @@ static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1
/**Function*************************************************************
+ Synopsis [Applies the simulation rules.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Ivy_Init_t Ivy_ManHaigSimulateChoice( Ivy_Init_t In0, Ivy_Init_t In1 )
+{
+ assert( In0 != IVY_INIT_NONE && In1 != IVY_INIT_NONE );
+ if ( (In0 == IVY_INIT_0 && In1 == IVY_INIT_1) || (In0 == IVY_INIT_1 && In1 == IVY_INIT_0) )
+ {
+ printf( "Compatibility fails.\n" );
+ return IVY_INIT_0;
+ }
+ if ( In0 == IVY_INIT_DC && In1 == IVY_INIT_DC )
+ return IVY_INIT_DC;
+ if ( In0 != IVY_INIT_DC )
+ return In0;
+ return In1;
+}
+
+/**Function*************************************************************
+
Synopsis [Simulate HAIG using modified 3-valued simulation.]
Description []
@@ -300,39 +428,85 @@ static inline Ivy_Init_t Ivy_ManHaigSimulateAnd( Ivy_Init_t In0, Ivy_Init_t In1
***********************************************************************/
void Ivy_ManHaigSimulate( Ivy_Man_t * p )
{
- Vec_Int_t * vNodes, * vLatches;
- Ivy_Obj_t * pObj;
+ Vec_Int_t * vNodes, * vLatches, * vLatchesD;
+ Ivy_Obj_t * pObj, * pTemp;
Ivy_Init_t In0, In1;
int i, k, Counter;
+ int fVerbose = 0;
+
+ // check choices
+ Ivy_ManCheckChoices( p );
+
+ // switch to HAIG
assert( p->pHaig != NULL );
p = p->pHaig;
+
+if ( fVerbose )
+Ivy_ManForEachPi( p, pObj, i )
+printf( "Setting PI %d\n", pObj->Id );
+
// collect latches and nodes in the DFS order
vNodes = Ivy_ManDfsSeq( p, &vLatches );
+
+if ( fVerbose )
+Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
+printf( "Collected node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
+
// set the PI values
- Ivy_ManConst1(p)->Init = IVY_INIT_0;
+ Ivy_ManConst1(p)->Init = IVY_INIT_1;
Ivy_ManForEachPi( p, pObj, i )
pObj->Init = IVY_INIT_0;
+
// set the latch values
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
pObj->Init = IVY_INIT_DC;
+ // set the latches of D to be determinate
+ vLatchesD = p->pData;
+ Ivy_ManForEachNodeVec( p, vLatchesD, pObj, i )
+ pObj->Init = IVY_INIT_0;
+
// perform several rounds of simulation
- for ( k = 0; k < 5; k++ )
+ for ( k = 0; k < 10; k++ )
{
// count the number of non-determinate values
Counter = 0;
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
Counter += ( pObj->Init == IVY_INIT_DC );
- printf( "Iter %d : Non-determinate = %d\n", k, Counter );
+ printf( "Iter %d : Non-determinate = %d\n", k, Counter );
+
// simulate the internal nodes
Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
{
+if ( fVerbose )
+printf( "Processing node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
In0 = Ivy_InitNotCond( Ivy_ObjFanin0(pObj)->Init, Ivy_ObjFaninC0(pObj) );
In1 = Ivy_InitNotCond( Ivy_ObjFanin1(pObj)->Init, Ivy_ObjFaninC1(pObj) );
pObj->Init = Ivy_ManHaigSimulateAnd( In0, In1 );
+ // simulate the equivalence class if the node is a representative
+ if ( pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
+ {
+if ( fVerbose )
+printf( "Processing choice node %d\n", pObj->Id );
+ In0 = pObj->Init;
+ assert( !Ivy_IsComplement(pObj->pEquiv) );
+ for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
+ {
+if ( fVerbose )
+printf( "Processing secondary node %d\n", pTemp->Id );
+ In1 = Ivy_InitNotCond( pTemp->Init, Ivy_IsComplement(pTemp->pEquiv) );
+ In0 = Ivy_ManHaigSimulateChoice( In0, In1 );
+ }
+ pObj->Init = In0;
+ }
}
+
// simulate the latches
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+ {
pObj->Level = Ivy_ObjFanin0(pObj)->Init;
+if ( fVerbose )
+printf( "Using latch %d with fanin %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id );
+ }
Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
pObj->Init = pObj->Level, pObj->Level = 0;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 19:31:54 +0000