diff options
Diffstat (limited to 'src/temp/ivy/ivyRewrite.c')
| -rw-r--r-- | src/temp/ivy/ivyRewrite.c | 365 |
1 files changed, 365 insertions, 0 deletions
diff --git a/src/temp/ivy/ivyRewrite.c b/src/temp/ivy/ivyRewrite.c new file mode 100644 index 00000000..031db9bc --- /dev/null +++ b/src/temp/ivy/ivyRewrite.c @@ -0,0 +1,365 @@ +/**CFile**************************************************************** + + FileName [ivyRewrite.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [And-Inverter Graph package.] + + Synopsis [AIG rewriting.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - May 11, 2006.] + + Revision [$Id: ivyRewrite.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ivy.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static unsigned Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront ); +static void Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone ); +static int Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs Boolean rewriting of sequential AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ) +{ + Vec_Int_t * vNodes, * vFront, * vInside, * vTree; + Ivy_Obj_t * pNode, * pNodeNew, * pTemp; + int i, k, nCostOld, nCostInt, nCostInt2, nCostNew, RetValue, Entry, nRefsSaved, nInputs; + int clk, clkCut = 0, clkTru = 0, clkDsd = 0, clkUpd = 0, clkStart = clock(); + unsigned uTruth; + + nInputs = 4; + vTree = Vec_IntAlloc( 8 ); + vFront = Vec_IntAlloc( 8 ); + vInside = Vec_IntAlloc( 50 ); + vNodes = Ivy_ManDfs( p ); + Ivy_ManForEachNodeVec( p, vNodes, pNode, i ) + { + if ( Ivy_ObjIsBuf(pNode) ) + continue; + // fix the fanin buffer problem + Ivy_NodeFixBufferFanins( pNode ); + if ( Ivy_ObjIsBuf(pNode) ) + continue; + + // find one sequential cut rooted at this node +clk = clock(); + Ivy_ManSeqFindCut( pNode, vFront, vInside, nInputs ); +clkCut += clock() - clk; + // compute the truth table of the cut +clk = clock(); + uTruth = Ivy_ManSeqFindTruth( pNode, vFront ); +clkTru += clock() - clk; + // decompose the truth table +clk = clock(); + RetValue = Ivy_TruthDsd( uTruth, vTree ); +clkDsd += clock() - clk; + if ( !RetValue ) + continue; // DSD does not exist +// Ivy_TruthDsdPrint( stdout, vTree ); + +clk = clock(); + // remember the cost of the current network + nCostOld = Ivy_ManGetCost(p); + // increment references of the cut variables + Vec_IntForEachEntry( vFront, Entry, k ) + { + pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); + Ivy_ObjRefsInc( pTemp ); + } + // dereference and record undo + nRefsSaved = pNode->nRefs; pNode->nRefs = 0; + Ivy_ManUndoStart( p ); + Ivy_ObjDelete_rec( pNode, 0 ); + Ivy_ManUndoStop( p ); + pNode->nRefs = nRefsSaved; + + // get the intermediate cost + nCostInt = Ivy_ManGetCost(p); + +// printf( "Removed by dereferencing = %d.\n", nCostOld - nCostInt ); + + // construct the new logic cone + pNodeNew = Ivy_ManDsdConstruct( p, vFront, vTree ); + // remember the cost + nCostNew = Ivy_ManGetCost(p); + +// printf( "Added by dereferencing = %d.\n", nCostInt - nCostNew ); +// nCostNew = nCostNew; + +/* + if ( Ivy_Regular(pNodeNew)->nRefs == 0 ) + Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 ); + // get the intermediate cost + nCostInt2 = Ivy_ManGetCost(p); + assert( nCostInt == nCostInt2 ); + + Ivy_ManUndoPerform( p, pNode ); + pNode->nRefs = nRefsSaved; + + Vec_IntForEachEntry( vFront, Entry, k ) + { +// pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); + pTemp = Ivy_ManObj(p, Entry); + Ivy_ObjRefsDec( pTemp ); + } +clkUpd += clock() - clk; + continue; +*/ + + // detect the case when they are exactly the same +// if ( pNodeNew == pNode ) +// continue; + + // compare the costs + if ( nCostOld > nCostNew || nCostOld == nCostNew && fUseZeroCost ) + { // accept the change +// printf( "NODES GAINED = %d\n", nCostOld - nCostNew ); + + Ivy_ObjReplace( pNode, pNodeNew, 0, 1 ); + pNode->nRefs = nRefsSaved; + } + else + { // reject change +// printf( "Rejected\n" ); + + if ( Ivy_Regular(pNodeNew)->nRefs == 0 ) + Ivy_ObjDelete_rec( Ivy_Regular(pNodeNew), 1 ); + + // get the intermediate cost + nCostInt2 = Ivy_ManGetCost(p); + assert( nCostInt == nCostInt2 ); + + // reconstruct the old node + Ivy_ManUndoPerform( p, pNode ); + pNode->nRefs = nRefsSaved; + } + // decrement references of the cut variables + Vec_IntForEachEntry( vFront, Entry, k ) + { +// pTemp = Ivy_ManObj(p, Ivy_LeafId(Entry)); + pTemp = Ivy_ManObj(p, Entry); + if ( Ivy_ObjIsNone(pTemp) ) + continue; + Ivy_ObjRefsDec( pTemp ); + if ( Ivy_ObjRefs(pTemp) == 0 ) + Ivy_ObjDelete_rec( pTemp, 1 ); + } + +clkUpd += clock() - clk; + } + +PRT( "Cut ", clkCut ); +PRT( "Truth ", clkTru ); +PRT( "DSD ", clkDsd ); +PRT( "Update ", clkUpd ); +PRT( "TOTAL ", clock() - clkStart ); + + Vec_IntFree( vTree ); + Vec_IntFree( vFront ); + Vec_IntFree( vInside ); + Vec_IntFree( vNodes ); + + if ( !Ivy_ManCheck(p) ) + { + printf( "Ivy_ManSeqRewrite(): The check has failed.\n" ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes the truth table of the sequential cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_ManSeqFindTruth_rec( Ivy_Man_t * p, unsigned Node, Vec_Int_t * vFront ) +{ + static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + unsigned uTruth0, uTruth1; + Ivy_Obj_t * pNode; + int nLatches, Number; + // consider the case of a constant + if ( Node == 0 ) + return ~((unsigned)0); + // try to find this node in the frontier + Number = Vec_IntFind( vFront, Node ); + if ( Number >= 0 ) + return uMasks[Number]; + // get the node + pNode = Ivy_ManObj( p, Ivy_LeafId(Node) ); + assert( !Ivy_ObjIsPi(pNode) && !Ivy_ObjIsConst1(pNode) ); + // get the number of latches + nLatches = Ivy_LeafLat(Node) + Ivy_ObjIsLatch(pNode); + // expand the first fanin + uTruth0 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId0(pNode), nLatches), vFront ); + if ( Ivy_ObjFaninC0(pNode) ) + uTruth0 = ~uTruth0; + // quit if this is the one fanin node + if ( Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) + return uTruth0; + assert( Ivy_ObjIsNode(pNode) ); + // expand the second fanin + uTruth1 = Ivy_ManSeqFindTruth_rec( p, Ivy_LeafCreate(Ivy_ObjFaninId1(pNode), nLatches), vFront ); + if ( Ivy_ObjFaninC1(pNode) ) + uTruth1 = ~uTruth1; + // return the truth table + return Ivy_ObjIsAnd(pNode)? uTruth0 & uTruth1 : uTruth0 ^ uTruth1; +} + +/**Function************************************************************* + + Synopsis [Computes the truth table of the sequential cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_ManSeqFindTruth( Ivy_Obj_t * pNode, Vec_Int_t * vFront ) +{ + assert( Ivy_ObjIsNode(pNode) ); + return Ivy_ManSeqFindTruth_rec( Ivy_ObjMan(pNode), Ivy_LeafCreate(pNode->Id, 0), vFront ); +} + + +/**Function************************************************************* + + Synopsis [Recursively dereferences the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqDeref_rec( Ivy_Obj_t * pNode, Vec_Int_t * vCone ) +{ + Ivy_Obj_t * pFan; + assert( !Ivy_IsComplement(pNode) ); + assert( !Ivy_ObjIsNone(pNode) ); + if ( Ivy_ObjIsPi(pNode) ) + return; + // deref the first fanin + pFan = Ivy_ObjFanin0(pNode); + Ivy_ObjRefsDec( pFan ); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqDeref_rec( pFan, vCone ); + // deref the second fanin + pFan = Ivy_ObjFanin1(pNode); + Ivy_ObjRefsDec( pFan ); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqDeref_rec( pFan, vCone ); + // save the node + Vec_IntPush( vCone, pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Recursively references the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqRef_rec( Ivy_Obj_t * pNode ) +{ + Ivy_Obj_t * pFan; + assert( !Ivy_IsComplement(pNode) ); + assert( !Ivy_ObjIsNone(pNode) ); + if ( Ivy_ObjIsPi(pNode) ) + return; + // ref the first fanin + pFan = Ivy_ObjFanin0(pNode); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqRef_rec( pFan ); + Ivy_ObjRefsInc( pFan ); + // ref the second fanin + pFan = Ivy_ObjFanin1(pNode); + if ( Ivy_ObjRefs( pFan ) == 0 ) + Ivy_ManSeqRef_rec( pFan ); + Ivy_ObjRefsInc( pFan ); +} + +/**Function************************************************************* + + Synopsis [Collect MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_ManSeqCollectCone( Ivy_Obj_t * pNode, Vec_Int_t * vCone ) +{ + Vec_IntClear( vCone ); + Ivy_ManSeqDeref_rec( pNode, vCone ); + Ivy_ManSeqRef_rec( pNode ); +} + +/**Function************************************************************* + + Synopsis [Computes the cost of the logic cone.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManSeqGetCost( Ivy_Man_t * p, Vec_Int_t * vCone ) +{ + Ivy_Obj_t * pObj; + int i, Cost = 0; + Ivy_ManForEachNodeVec( p, vCone, pObj, i ) + { + if ( Ivy_ObjIsAnd(pObj) ) + Cost += 1; + else if ( Ivy_ObjIsExor(pObj) ) + Cost += 2; + } + return 0; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |