src/aig/ivy/ivyHaig.c File Reference

#include "ivy.h"
Include dependency graph for ivyHaig.c:

Go to the source code of this file.

Functions

static Ivy_Obj_t * Ivy_HaigObjRepr (Ivy_Obj_t *pObj)
static int Ivy_HaigObjCountClass (Ivy_Obj_t *pObj)
void Ivy_ManHaigStart (Ivy_Man_t *p, int fVerbose)
void Ivy_ManHaigTrasfer (Ivy_Man_t *p, Ivy_Man_t *pNew)
void Ivy_ManHaigStop (Ivy_Man_t *p)
void Ivy_ManHaigCreateObj (Ivy_Man_t *p, Ivy_Obj_t *pObj)
int Ivy_ObjIsInTfi_rec (Ivy_Obj_t *pObjNew, Ivy_Obj_t *pObjOld, int Levels)
void Ivy_ManHaigCreateChoice (Ivy_Man_t *p, Ivy_Obj_t *pObjOld, Ivy_Obj_t *pObjNew)
int Ivy_ManHaigCountChoices (Ivy_Man_t *p, int *pnChoices)
void Ivy_ManHaigPostprocess (Ivy_Man_t *p, int fVerbose)
static Ivy_Init_t Ivy_ManHaigSimulateAnd (Ivy_Init_t In0, Ivy_Init_t In1)
static Ivy_Init_t Ivy_ManHaigSimulateChoice (Ivy_Init_t In0, Ivy_Init_t In1)
void Ivy_ManHaigSimulate (Ivy_Man_t *p)

Function Documentation

static int Ivy_HaigObjCountClass ( Ivy_Obj_t *  pObj  )  [inline, static]

Definition at line 61 of file ivyHaig.c.

00062 {
00063     Ivy_Obj_t * pTemp;
00064     int Counter;
00065     assert( !Ivy_IsComplement(pObj) );
00066     assert( Ivy_ObjRefs(pObj) > 0 );
00067     if ( pObj->pEquiv == NULL )
00068         return 1;
00069     assert( !Ivy_IsComplement(pObj->pEquiv) );
00070     Counter = 1;
00071     for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
00072         Counter++;
00073     return Counter;
00074 }

static Ivy_Obj_t* Ivy_HaigObjRepr ( Ivy_Obj_t *  pObj  )  [inline, static]

CFile****************************************************************

FileName [ivyHaig.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [HAIG management procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id
ivyHaig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

] DECLARATIONS ///

Definition at line 43 of file ivyHaig.c.

00044 {
00045     Ivy_Obj_t * pTemp;
00046     assert( !Ivy_IsComplement(pObj) );
00047     // if the node has no equivalent node or has fanout, it is representative
00048     if ( pObj->pEquiv == NULL || Ivy_ObjRefs(pObj) > 0 )
00049         return pObj;
00050     // the node belongs to a class and is not a representative
00051     // complemented edge (pObj->pEquiv) tells if it is complemented w.r.t. the repr
00052     for ( pTemp = Ivy_Regular(pObj->pEquiv); pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
00053         if ( Ivy_ObjRefs(pTemp) > 0 )
00054             break;
00055     // return the representative node
00056     assert( Ivy_ObjRefs(pTemp) > 0 );
00057     return Ivy_NotCond( pTemp, Ivy_IsComplement(pObj->pEquiv) );
00058 }

int Ivy_ManHaigCountChoices ( Ivy_Man_t *  p,
int *  pnChoices 
)

Function*************************************************************

Synopsis [Count the number of choices and choice nodes in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 314 of file ivyHaig.c.

00315 {
00316     Ivy_Obj_t * pObj;
00317     int nChoices, nChoiceNodes, Counter, i;
00318     assert( p->pHaig != NULL );
00319     nChoices = nChoiceNodes = 0;
00320     Ivy_ManForEachObj( p->pHaig, pObj, i )
00321     {
00322         if ( Ivy_ObjIsTerm(pObj) || i == 0 )
00323             continue;
00324         if ( Ivy_ObjRefs(pObj) == 0 )
00325             continue;
00326         Counter = Ivy_HaigObjCountClass( pObj );
00327         nChoiceNodes += (int)(Counter > 1);
00328         nChoices += Counter - 1;
00329 //        if ( Counter > 1 )
00330 //            printf( "Choice node %d %s\n", pObj->Id, Ivy_ObjIsLatch(pObj)? "(latch)": "" );
00331     }
00332     *pnChoices = nChoices;
00333     return nChoiceNodes;
00334 }

void Ivy_ManHaigCreateChoice ( Ivy_Man_t *  p,
Ivy_Obj_t *  pObjOld,
Ivy_Obj_t *  pObjNew 
)

Function*************************************************************

Synopsis [Sets the pair of equivalent nodes in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 243 of file ivyHaig.c.

00244 {
00245     Ivy_Obj_t * pObjOldHaig, * pObjNewHaig;
00246     Ivy_Obj_t * pObjOldHaigR, * pObjNewHaigR;
00247     int fCompl;
00248 //printf( "\nCreating choice for %d and %d in AIG\n", pObjOld->Id, Ivy_Regular(pObjNew)->Id );
00249 
00250     assert( p->pHaig != NULL );
00251     assert( !Ivy_IsComplement(pObjOld) );
00252     // get pointers to the representatives of pObjOld and pObjNew
00253     pObjOldHaig = pObjOld->pEquiv;
00254     pObjNewHaig = Ivy_NotCond( Ivy_Regular(pObjNew)->pEquiv, Ivy_IsComplement(pObjNew) );
00255     // get the classes
00256     pObjOldHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjOldHaig)), Ivy_IsComplement(pObjOldHaig) );
00257     pObjNewHaig = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObjNewHaig)), Ivy_IsComplement(pObjNewHaig) );
00258     // get regular pointers
00259     pObjOldHaigR = Ivy_Regular(pObjOldHaig);
00260     pObjNewHaigR = Ivy_Regular(pObjNewHaig);
00261     // check if there is phase difference between them
00262     fCompl = (Ivy_IsComplement(pObjOldHaig) != Ivy_IsComplement(pObjNewHaig));
00263     // if the class is the same, nothing to do
00264     if ( pObjOldHaigR == pObjNewHaigR )
00265         return;
00266     // if the second node belongs to a class, do not merge classes (for the time being)
00267     if ( Ivy_ObjRefs(pObjOldHaigR) == 0 || pObjNewHaigR->pEquiv != NULL || 
00268         Ivy_ObjRefs(pObjNewHaigR) > 0 ) //|| Ivy_ObjIsInTfi_rec(pObjNewHaigR, pObjOldHaigR, 10) )
00269     {
00270 /*
00271         if ( pObjNewHaigR->pEquiv != NULL )
00272             printf( "c" );
00273         if ( Ivy_ObjRefs(pObjNewHaigR) > 0 )
00274             printf( "f" );
00275         printf( " " );
00276 */
00277         p->pHaig->nClassesSkip++;
00278         return;
00279     }
00280 
00281     // add this node to the class of pObjOldHaig
00282     assert( Ivy_ObjRefs(pObjOldHaigR) > 0 );
00283     assert( !Ivy_IsComplement(pObjOldHaigR->pEquiv) );
00284     if ( pObjOldHaigR->pEquiv == NULL )
00285         pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl );
00286     else
00287         pObjNewHaigR->pEquiv = Ivy_NotCond( pObjOldHaigR->pEquiv, fCompl );
00288     pObjOldHaigR->pEquiv = pObjNewHaigR;
00289 //printf( "Setting choice node %d -> %d.\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
00290     // update the class of the new node
00291 //    Ivy_Regular(pObjNew)->pEquiv = Ivy_NotCond( pObjOldHaigR, fCompl ^ Ivy_IsComplement(pObjNew) );
00292 //printf( "Creating choice for %d and %d in HAIG\n", pObjOldHaigR->Id, pObjNewHaigR->Id );
00293 
00294 //    if ( pObjOldHaigR->Id == 13 )
00295 //    {
00296 //        Ivy_ManShow( p, 0 );
00297 //        Ivy_ManShow( p->pHaig, 1 );
00298 //    }
00299 //    if ( !Ivy_ManIsAcyclic( p->pHaig ) )
00300 //        printf( "HAIG contains a cycle\n" );
00301 }

void Ivy_ManHaigCreateObj ( Ivy_Man_t *  p,
Ivy_Obj_t *  pObj 
)

Function*************************************************************

Synopsis [Creates a new node in HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file ivyHaig.c.

00181 {
00182     Ivy_Obj_t * pEquiv0, * pEquiv1;
00183     assert( p->pHaig != NULL );
00184     assert( !Ivy_IsComplement(pObj) );
00185     if ( Ivy_ObjType(pObj) == IVY_BUF )
00186         pObj->pEquiv = Ivy_ObjChild0Equiv(pObj);
00187     else if ( Ivy_ObjType(pObj) == IVY_LATCH )
00188     {
00189 //        pObj->pEquiv = Ivy_Latch( p->pHaig, Ivy_ObjChild0Equiv(pObj), pObj->Init );
00190         pEquiv0 = Ivy_ObjChild0Equiv(pObj);
00191         pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
00192         pObj->pEquiv = Ivy_Latch( p->pHaig, pEquiv0, pObj->Init );
00193     }
00194     else if ( Ivy_ObjType(pObj) == IVY_AND )
00195     {
00196 //        pObj->pEquiv = Ivy_And( p->pHaig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) );
00197         pEquiv0 = Ivy_ObjChild0Equiv(pObj);
00198         pEquiv0 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv0)), Ivy_IsComplement(pEquiv0) );
00199         pEquiv1 = Ivy_ObjChild1Equiv(pObj);
00200         pEquiv1 = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pEquiv1)), Ivy_IsComplement(pEquiv1) );
00201         pObj->pEquiv = Ivy_And( p->pHaig, pEquiv0, pEquiv1 );
00202     }
00203     else assert( 0 );
00204     // make sure the node points to the representative
00205 //    pObj->pEquiv = Ivy_NotCond( Ivy_HaigObjRepr(Ivy_Regular(pObj->pEquiv)), Ivy_IsComplement(pObj->pEquiv) );
00206 }

void Ivy_ManHaigPostprocess ( Ivy_Man_t *  p,
int  fVerbose 
)

Function*************************************************************

Synopsis [Prints statistics of the HAIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 347 of file ivyHaig.c.

00348 {
00349     int nChoices, nChoiceNodes;
00350 
00351     assert( p->pHaig != NULL );
00352 
00353     if ( fVerbose )
00354     {
00355         printf( "Final    : " );
00356         Ivy_ManPrintStats( p );
00357         printf( "HAIG     : " );
00358         Ivy_ManPrintStats( p->pHaig );
00359 
00360         // print choice node stats
00361         nChoiceNodes = Ivy_ManHaigCountChoices( p, &nChoices );
00362         printf( "Total choice nodes = %d. Total choices = %d. Skipped classes = %d.\n", 
00363             nChoiceNodes, nChoices, p->pHaig->nClassesSkip ); 
00364     }
00365 
00366     if ( Ivy_ManIsAcyclic( p->pHaig ) )
00367     {
00368         if ( fVerbose )
00369             printf( "HAIG is acyclic\n" );
00370     }
00371     else
00372         printf( "HAIG contains a cycle\n" );
00373 
00374 //    if ( fVerbose )
00375 //        Ivy_ManHaigSimulate( p );
00376 }

void Ivy_ManHaigSimulate ( Ivy_Man_t *  p  ) 

Function*************************************************************

Synopsis [Simulate HAIG using modified 3-valued simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 437 of file ivyHaig.c.

00438 {
00439     Vec_Int_t * vNodes, * vLatches, * vLatchesD;
00440     Ivy_Obj_t * pObj, * pTemp;
00441     Ivy_Init_t In0, In1;
00442     int i, k, Counter;
00443     int fVerbose = 0;
00444 
00445     // check choices
00446     Ivy_ManCheckChoices( p );
00447 
00448     // switch to HAIG
00449     assert( p->pHaig != NULL );
00450     p = p->pHaig;
00451 
00452 if ( fVerbose )
00453 Ivy_ManForEachPi( p, pObj, i )
00454 printf( "Setting PI %d\n", pObj->Id );
00455 
00456     // collect latches and nodes in the DFS order
00457     vNodes = Ivy_ManDfsSeq( p, &vLatches );
00458 
00459 if ( fVerbose )
00460 Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
00461 printf( "Collected node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
00462 
00463     // set the PI values
00464     Ivy_ManConst1(p)->Init = IVY_INIT_1;
00465     Ivy_ManForEachPi( p, pObj, i )
00466         pObj->Init = IVY_INIT_0;
00467 
00468     // set the latch values
00469     Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
00470         pObj->Init = IVY_INIT_DC;
00471     // set the latches of D to be determinate
00472     vLatchesD = p->pData;
00473     Ivy_ManForEachNodeVec( p, vLatchesD, pObj, i )
00474         pObj->Init = IVY_INIT_0;
00475 
00476     // perform several rounds of simulation
00477     for ( k = 0; k < 10; k++ )
00478     {
00479         // count the number of non-determinate values
00480         Counter = 0;
00481         Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
00482             Counter += ( pObj->Init == IVY_INIT_DC );
00483         printf( "Iter %d : Non-determinate = %d\n", k, Counter );    
00484         
00485         // simulate the internal nodes
00486         Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
00487         {
00488 if ( fVerbose )
00489 printf( "Processing node %d with fanins %d and %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id, Ivy_ObjFanin1(pObj)->Id );
00490             In0 = Ivy_InitNotCond( Ivy_ObjFanin0(pObj)->Init, Ivy_ObjFaninC0(pObj) );
00491             In1 = Ivy_InitNotCond( Ivy_ObjFanin1(pObj)->Init, Ivy_ObjFaninC1(pObj) );
00492             pObj->Init = Ivy_ManHaigSimulateAnd( In0, In1 );
00493             // simulate the equivalence class if the node is a representative
00494             if ( pObj->pEquiv && Ivy_ObjRefs(pObj) > 0 )
00495             {
00496 if ( fVerbose )
00497 printf( "Processing choice node %d\n", pObj->Id );
00498                 In0 = pObj->Init;
00499                 assert( !Ivy_IsComplement(pObj->pEquiv) );
00500                 for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) )
00501                 {
00502 if ( fVerbose )
00503 printf( "Processing secondary node %d\n", pTemp->Id );
00504                     In1 = Ivy_InitNotCond( pTemp->Init, Ivy_IsComplement(pTemp->pEquiv) );
00505                     In0 = Ivy_ManHaigSimulateChoice( In0, In1 );
00506                 }
00507                 pObj->Init = In0;
00508             }
00509         }
00510 
00511         // simulate the latches
00512         Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
00513         {
00514             pObj->Level = Ivy_ObjFanin0(pObj)->Init;
00515 if ( fVerbose )
00516 printf( "Using latch %d with fanin %d\n", pObj->Id, Ivy_ObjFanin0(pObj)->Id );
00517         }
00518         Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
00519             pObj->Init = pObj->Level, pObj->Level = 0;
00520     }
00521     // free arrays
00522     Vec_IntFree( vNodes );
00523     Vec_IntFree( vLatches );
00524 }

static Ivy_Init_t Ivy_ManHaigSimulateAnd ( Ivy_Init_t  In0,
Ivy_Init_t  In1 
) [inline, static]

Function*************************************************************

Synopsis [Applies the simulation rules.]

Description []

SideEffects []

SeeAlso []

Definition at line 390 of file ivyHaig.c.

00391 {
00392     assert( In0 != IVY_INIT_NONE && In1 != IVY_INIT_NONE );
00393     if ( In0 == IVY_INIT_DC || In1 == IVY_INIT_DC )
00394         return IVY_INIT_DC;
00395     if ( In0 == IVY_INIT_1 && In1 == IVY_INIT_1 )
00396         return IVY_INIT_1;
00397     return IVY_INIT_0;
00398 }

static Ivy_Init_t Ivy_ManHaigSimulateChoice ( Ivy_Init_t  In0,
Ivy_Init_t  In1 
) [inline, static]

Function*************************************************************

Synopsis [Applies the simulation rules.]

Description []

SideEffects []

SeeAlso []

Definition at line 411 of file ivyHaig.c.

00412 {
00413     assert( In0 != IVY_INIT_NONE && In1 != IVY_INIT_NONE );
00414     if ( (In0 == IVY_INIT_0 && In1 == IVY_INIT_1) || (In0 == IVY_INIT_1 && In1 == IVY_INIT_0) )
00415     {
00416          printf( "Compatibility fails.\n" );
00417          return IVY_INIT_0;
00418     }
00419     if ( In0 == IVY_INIT_DC && In1 == IVY_INIT_DC )
00420         return IVY_INIT_DC;
00421     if ( In0 != IVY_INIT_DC )
00422         return In0;
00423     return In1;
00424 }

void Ivy_ManHaigStart ( Ivy_Man_t *  p,
int  fVerbose 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Starts HAIG for the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file ivyHaig.c.

00092 {
00093     Vec_Int_t * vLatches;
00094     Ivy_Obj_t * pObj;
00095     int i;
00096     assert( p->pHaig == NULL );
00097     p->pHaig = Ivy_ManDup( p );
00098 
00099     if ( fVerbose )
00100     {
00101         printf( "Starting : " );
00102         Ivy_ManPrintStats( p->pHaig );
00103     }
00104 
00105     // collect latches of design D and set their values to be DC
00106     vLatches = Vec_IntAlloc( 100 );
00107     Ivy_ManForEachLatch( p->pHaig, pObj, i )
00108     {
00109         pObj->Init = IVY_INIT_DC;
00110         Vec_IntPush( vLatches, pObj->Id );
00111     }
00112     p->pHaig->pData = vLatches;
00113 /*
00114     {
00115         int x;
00116         Ivy_ManShow( p, 0, NULL );
00117         Ivy_ManShow( p->pHaig, 1, NULL );
00118         x = 0;
00119     }
00120 */
00121 }

void Ivy_ManHaigStop ( Ivy_Man_t *  p  ) 

Function*************************************************************

Synopsis [Stops HAIG for the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 156 of file ivyHaig.c.

00157 {
00158     Ivy_Obj_t * pObj;
00159     int i;
00160     assert( p->pHaig != NULL );
00161     Vec_IntFree( p->pHaig->pData );
00162     Ivy_ManStop( p->pHaig );
00163     p->pHaig = NULL;
00164     // remove dangling pointers to the HAIG objects
00165     Ivy_ManForEachObj( p, pObj, i )
00166         pObj->pEquiv = NULL;
00167 }

void Ivy_ManHaigTrasfer ( Ivy_Man_t *  p,
Ivy_Man_t *  pNew 
)

Function*************************************************************

Synopsis [Transfers the HAIG to the newly created manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 134 of file ivyHaig.c.

00135 {
00136     Ivy_Obj_t * pObj;
00137     int i;
00138     assert( p->pHaig != NULL );
00139     Ivy_ManConst1(pNew)->pEquiv = Ivy_ManConst1(p)->pEquiv;
00140     Ivy_ManForEachPi( pNew, pObj, i )
00141         pObj->pEquiv = Ivy_ManPi( p, i )->pEquiv;
00142     pNew->pHaig = p->pHaig;
00143 }

int Ivy_ObjIsInTfi_rec ( Ivy_Obj_t *  pObjNew,
Ivy_Obj_t *  pObjOld,
int  Levels 
)

Function*************************************************************

Synopsis [Checks if the old node is in the TFI of the new node.]

Description []

SideEffects []

SeeAlso []

Definition at line 219 of file ivyHaig.c.

00220 {
00221     if ( pObjNew == pObjOld )
00222         return 1;
00223     if ( Levels == 0 || Ivy_ObjIsCi(pObjNew) || Ivy_ObjIsConst1(pObjNew) )
00224         return 0;
00225     if ( Ivy_ObjIsInTfi_rec( Ivy_ObjFanin0(pObjNew), pObjOld, Levels - 1 ) )
00226         return 1;
00227     if ( Ivy_ObjIsNode(pObjNew) && Ivy_ObjIsInTfi_rec( Ivy_ObjFanin1(pObjNew), pObjOld, Levels - 1 ) )
00228         return 1;
00229     return 0;
00230 }

Generated on Tue Jan 5 12:18:24 2010 for abc70930 by  doxygen 1.6.1