src/aig/ivy/ivy.h File Reference
#include <stdio.h>#include "extra.h"#include "vec.h"
Include dependency graph for ivy.h:
This graph shows which files directly or indirectly include this file:
Go to the source code of this file.
Define Documentation
| #define Ivy_ManForEachCi | ( | p, | |||
| pObj, | |||||
| i | ) | Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCi(pObj) ) {} else |
| #define Ivy_ManForEachCo | ( | p, | |||
| pObj, | |||||
| i | ) | Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsCo(pObj) ) {} else |
| #define Ivy_ManForEachLatch | ( | p, | |||
| pObj, | |||||
| i | ) | Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsLatch(pObj) ) {} else |
| #define Ivy_ManForEachNode | ( | p, | |||
| pObj, | |||||
| i | ) | Ivy_ManForEachObj( p, pObj, i ) if ( !Ivy_ObjIsNode(pObj) ) {} else |
| #define Ivy_ManForEachNodeVec | ( | p, | |||
| vIds, | |||||
| pObj, | |||||
| i | ) | for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Ivy_ManObj(p, Vec_IntEntry(vIds,i))); i++ ) |
| #define Ivy_ManForEachObj | ( | p, | |||
| pObj, | |||||
| i | ) | Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else |
| #define Ivy_ManForEachPi | ( | p, | |||
| pObj, | |||||
| i | ) | Vec_PtrForEachEntry( p->vPis, pObj, i ) |
| #define Ivy_ManForEachPo | ( | p, | |||
| pObj, | |||||
| i | ) | Vec_PtrForEachEntry( p->vPos, pObj, i ) |
| #define IVY_MIN | ( | a, | |||
| b | ) | (((a) < (b))? (a) : (b)) |
| #define Ivy_ObjForEachFanout | ( | p, | |||
| pObj, | |||||
| vArray, | |||||
| pFanout, | |||||
| i | ) |
Value:
for ( i = 0, Ivy_ObjCollectFanouts(p, pObj, vArray); \ i < Vec_PtrSize(vArray) && ((pFanout) = Vec_PtrEntry(vArray,i)); i++ )
Typedef Documentation
| typedef struct Ivy_Cut_t_ Ivy_Cut_t |
| typedef int Ivy_Edge_t |
| typedef struct Ivy_FraigParams_t_ Ivy_FraigParams_t |
| typedef struct Ivy_Man_t_ Ivy_Man_t |
CFile****************************************************************
FileName [ivy.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [
- Id
- ivy.c,v 1.00 2006/05/11 00:00:00 alanmi Exp
] INCLUDES /// PARAMETERS /// BASIC TYPES ///
| typedef struct Ivy_Obj_t_ Ivy_Obj_t |
| typedef struct Ivy_Store_t_ Ivy_Store_t |
Enumeration Type Documentation
| enum Ivy_Init_t |
Definition at line 63 of file ivy.h.
00063 { 00064 IVY_INIT_NONE, // 0: not a latch 00065 IVY_INIT_0, // 1: zero 00066 IVY_INIT_1, // 2: one 00067 IVY_INIT_DC // 3: don't-care 00068 } Ivy_Init_t;
| enum Ivy_Type_t |
Definition at line 50 of file ivy.h.
00050 { 00051 IVY_NONE, // 0: non-existent object 00052 IVY_PI, // 1: primary input (and constant 1 node) 00053 IVY_PO, // 2: primary output 00054 IVY_ASSERT, // 3: assertion 00055 IVY_LATCH, // 4: sequential element 00056 IVY_AND, // 5: AND node 00057 IVY_EXOR, // 6: EXOR node 00058 IVY_BUF, // 7: buffer (temporary) 00059 IVY_VOID // 8: unused object 00060 } Ivy_Type_t;
Function Documentation
Function*************************************************************
Synopsis [Performs canonicization step.]
Description [The argument nodes can be complemented.]
SideEffects []
SeeAlso []
Definition at line 81 of file ivyOper.c.
00082 { 00083 // Ivy_Obj_t * pFan0, * pFan1; 00084 // check trivial cases 00085 if ( p0 == p1 ) 00086 return p0; 00087 if ( p0 == Ivy_Not(p1) ) 00088 return Ivy_Not(p->pConst1); 00089 if ( Ivy_Regular(p0) == p->pConst1 ) 00090 return p0 == p->pConst1 ? p1 : Ivy_Not(p->pConst1); 00091 if ( Ivy_Regular(p1) == p->pConst1 ) 00092 return p1 == p->pConst1 ? p0 : Ivy_Not(p->pConst1); 00093 // check if it can be an EXOR gate 00094 // if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) 00095 // return Ivy_CanonExor( pFan0, pFan1 ); 00096 return Ivy_CanonAnd( p, p0, p1 ); 00097 }
| static int Ivy_BitWordNum | ( | int | nBits | ) | [inline, static] |
Function*************************************************************
Synopsis [Creates the canonical form of the node.]
Description []
SideEffects []
SeeAlso []
Definition at line 87 of file ivyCanon.c.
00088 { 00089 Ivy_Obj_t * pGhost, * pResult; 00090 pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_AND, IVY_INIT_NONE ); 00091 pResult = Ivy_CanonPair_rec( p, pGhost ); 00092 return pResult; 00093 }
Function*************************************************************
Synopsis [Creates the canonical form of the node.]
Description []
SideEffects []
SeeAlso []
Definition at line 106 of file ivyCanon.c.
00107 { 00108 Ivy_Obj_t * pGhost, * pResult; 00109 int fCompl = Ivy_IsComplement(pObj0) ^ Ivy_IsComplement(pObj1); 00110 pObj0 = Ivy_Regular(pObj0); 00111 pObj1 = Ivy_Regular(pObj1); 00112 pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE ); 00113 pResult = Ivy_CanonPair_rec( p, pGhost ); 00114 return Ivy_NotCond( pResult, fCompl ); 00115 }
| Ivy_Obj_t* Ivy_CanonLatch | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t * | pObj, | |||
| Ivy_Init_t | Init | |||
| ) |
Function*************************************************************
Synopsis [Creates the canonical form of the node.]
Description []
SideEffects []
SeeAlso []
Definition at line 128 of file ivyCanon.c.
00129 { 00130 Ivy_Obj_t * pGhost, * pResult; 00131 int fCompl = Ivy_IsComplement(pObj); 00132 pObj = Ivy_Regular(pObj); 00133 pGhost = Ivy_ObjCreateGhost( p, pObj, NULL, IVY_LATCH, Ivy_InitNotCond(Init, fCompl) ); 00134 pResult = Ivy_TableLookup( p, pGhost ); 00135 if ( pResult == NULL ) 00136 pResult = Ivy_ObjCreate( p, pGhost ); 00137 return Ivy_NotCond( pResult, fCompl ); 00138 }
Function*************************************************************
Synopsis [Performs incremental rewriting of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 767 of file ivyUtil.c.
00768 { 00769 Vec_Ptr_t * vArray; 00770 Ivy_Obj_t * pObj, * pFanout; 00771 int nLatches = 0; 00772 int nPresent = 0; 00773 int i, k; 00774 int fVerbose = 0; 00775 00776 if ( fVerbose ) 00777 printf( "Trying cut : {" ); 00778 for ( i = 0; i < pCut->nSize; i++ ) 00779 { 00780 if ( fVerbose ) 00781 printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) ); 00782 nLatches += Ivy_LeafLat(pCut->pArray[i]); 00783 } 00784 if ( fVerbose ) 00785 printf( " } " ); 00786 if ( fVerbose ) 00787 printf( "Latches = %d. ", nLatches ); 00788 00789 // check if there are latches on the fanout edges 00790 vArray = Vec_PtrAlloc( 100 ); 00791 for ( i = 0; i < pCut->nSize; i++ ) 00792 { 00793 pObj = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[i]) ); 00794 Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, k ) 00795 { 00796 if ( Ivy_ObjIsLatch(pFanout) ) 00797 { 00798 nPresent++; 00799 break; 00800 } 00801 } 00802 } 00803 Vec_PtrSize( vArray ); 00804 if ( fVerbose ) 00805 { 00806 printf( "Present = %d. ", nPresent ); 00807 if ( nLatches > nPresent ) 00808 printf( "Clauses = %d. ", 2*(nLatches - nPresent) ); 00809 printf( "\n" ); 00810 } 00811 return ( nLatches > nPresent ) ? 2*(nLatches - nPresent) : 0; 00812 }
| static Ivy_Edge_t Ivy_EdgeCreate | ( | int | Id, | |
| int | fCompl | |||
| ) | [inline, static] |
| static Ivy_Edge_t Ivy_EdgeFromNode | ( | Ivy_Obj_t * | pNode | ) | [inline, static] |
Definition at line 207 of file ivy.h.
00207 { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) ); }
| static int Ivy_EdgeId | ( | Ivy_Edge_t | Edge | ) | [inline, static] |
| static int Ivy_EdgeIsComplement | ( | Ivy_Edge_t | Edge | ) | [inline, static] |
| static Ivy_Edge_t Ivy_EdgeNot | ( | Ivy_Edge_t | Edge | ) | [inline, static] |
| static Ivy_Edge_t Ivy_EdgeNotCond | ( | Ivy_Edge_t | Edge, | |
| int | fCond | |||
| ) | [inline, static] |
| static Ivy_Edge_t Ivy_EdgeRegular | ( | Ivy_Edge_t | Edge | ) | [inline, static] |
| static Ivy_Obj_t* Ivy_EdgeToNode | ( | Ivy_Man_t * | p, | |
| Ivy_Edge_t | Edge | |||
| ) | [inline, static] |
Definition at line 208 of file ivy.h.
00208 { return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); }
Function*************************************************************
Synopsis [Performs canonicization step.]
Description [The argument nodes can be complemented.]
SideEffects []
SeeAlso []
Definition at line 110 of file ivyOper.c.
00111 { 00112 /* 00113 // check trivial cases 00114 if ( p0 == p1 ) 00115 return Ivy_Not(p->pConst1); 00116 if ( p0 == Ivy_Not(p1) ) 00117 return p->pConst1; 00118 if ( Ivy_Regular(p0) == p->pConst1 ) 00119 return Ivy_NotCond( p1, p0 == p->pConst1 ); 00120 if ( Ivy_Regular(p1) == p->pConst1 ) 00121 return Ivy_NotCond( p0, p1 == p->pConst1 ); 00122 // check the table 00123 return Ivy_CanonExor( p, p0, p1 ); 00124 */ 00125 return Ivy_Or( p, Ivy_And(p, p0, Ivy_Not(p1)), Ivy_And(p, Ivy_Not(p0), p1) ); 00126 }
| void Ivy_FastMapPerform | ( | Ivy_Man_t * | pAig, | |
| int | nLimit, | |||
| int | fRecovery, | |||
| int | fVerbose | |||
| ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Performs fast K-LUT mapping of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 102 of file ivyFastMap.c.
00103 { 00104 Ivy_SuppMan_t * pMan; 00105 Ivy_Obj_t * pObj; 00106 int i, Delay, Area, clk, clkTotal = clock(); 00107 // start the memory for supports 00108 pMan = ALLOC( Ivy_SuppMan_t, 1 ); 00109 memset( pMan, 0, sizeof(Ivy_SuppMan_t) ); 00110 pMan->nLimit = nLimit; 00111 pMan->nObjs = Ivy_ManObjIdMax(pAig) + 1; 00112 pMan->nSize = sizeof(Ivy_Supp_t) + nLimit * sizeof(int); 00113 pMan->pMem = (char *)malloc( pMan->nObjs * pMan->nSize ); 00114 memset( pMan->pMem, 0, pMan->nObjs * pMan->nSize ); 00115 pMan->vLuts = Vec_VecAlloc( 100 ); 00116 pAig->pData = pMan; 00117 clk = clock(); 00118 // set the PI mapping 00119 Ivy_ObjSuppStart( pAig, Ivy_ManConst1(pAig) ); 00120 Ivy_ManForEachPi( pAig, pObj, i ) 00121 Ivy_ObjSuppStart( pAig, pObj ); 00122 // iterate through all nodes in the topological order 00123 Ivy_ManForEachNode( pAig, pObj, i ) 00124 Ivy_FastMapNode( pAig, pObj, nLimit ); 00125 // find the best arrival time and area 00126 Delay = Ivy_FastMapDelay( pAig ); 00127 Area = Ivy_FastMapArea(pAig); 00128 if ( fVerbose ) 00129 Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Delay oriented mapping: " ); 00130 00131 // 2-1-2 (doing 2-1-2-1-2 improves 0.5%) 00132 00133 if ( fRecovery ) 00134 { 00135 clk = clock(); 00136 Ivy_FastMapRequired( pAig, Delay, 0 ); 00137 // remap the nodes 00138 Ivy_FastMapRecover( pAig, nLimit ); 00139 Delay = Ivy_FastMapDelay( pAig ); 00140 Area = Ivy_FastMapArea(pAig); 00141 if ( fVerbose ) 00142 Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 2 : " ); 00143 00144 clk = clock(); 00145 Ivy_FastMapRequired( pAig, Delay, 0 ); 00146 // iterate through all nodes in the topological order 00147 Ivy_ManForEachNode( pAig, pObj, i ) 00148 Ivy_FastMapNodeArea( pAig, pObj, nLimit ); 00149 Delay = Ivy_FastMapDelay( pAig ); 00150 Area = Ivy_FastMapArea(pAig); 00151 if ( fVerbose ) 00152 Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 1 : " ); 00153 00154 clk = clock(); 00155 Ivy_FastMapRequired( pAig, Delay, 0 ); 00156 // remap the nodes 00157 Ivy_FastMapRecover( pAig, nLimit ); 00158 Delay = Ivy_FastMapDelay( pAig ); 00159 Area = Ivy_FastMapArea(pAig); 00160 if ( fVerbose ) 00161 Ivy_FastMapPrint( pAig, Delay, Area, clock() - clk, "Area recovery 2 : " ); 00162 } 00163 00164 00165 s_MappingTime = clock() - clkTotal; 00166 s_MappingMem = pMan->nObjs * pMan->nSize; 00167 /* 00168 { 00169 Vec_Ptr_t * vNodes; 00170 vNodes = Vec_PtrAlloc( 100 ); 00171 Vec_VecForEachEntry( pMan->vLuts, pObj, i, k ) 00172 Vec_PtrPush( vNodes, pObj ); 00173 Ivy_ManShow( pAig, 0, vNodes ); 00174 Vec_PtrFree( vNodes ); 00175 } 00176 */ 00177 }
Function*************************************************************
Synopsis [Creates integer vector with the support of the node.]
Description []
SideEffects []
SeeAlso []
Definition at line 815 of file ivyFastMap.c.
00816 { 00817 Ivy_Supp_t * pSupp; 00818 pSupp = Ivy_ObjSupp( pAig, pObj ); 00819 vLeaves->nCap = 8; 00820 vLeaves->nSize = pSupp->nSize; 00821 vLeaves->pArray = pSupp->pArray; 00822 }
| void Ivy_FastMapReverseLevel | ( | Ivy_Man_t * | pAig | ) |
| void Ivy_FastMapStop | ( | Ivy_Man_t * | pAig | ) |
Function*************************************************************
Synopsis [Cleans memory used for decomposition.]
Description []
SideEffects []
SeeAlso []
Definition at line 190 of file ivyFastMap.c.
00191 { 00192 Ivy_SuppMan_t * p = pAig->pData; 00193 Vec_VecFree( p->vLuts ); 00194 free( p->pMem ); 00195 free( p ); 00196 pAig->pData = NULL; 00197 }
| Ivy_Man_t* Ivy_FraigMiter | ( | Ivy_Man_t * | pManAig, | |
| Ivy_FraigParams_t * | pParams | |||
| ) |
Function*************************************************************
Synopsis [Applies brute-force SAT to the miter.]
Description []
SideEffects []
SeeAlso []
Definition at line 471 of file ivyFraig.c.
00472 { 00473 Ivy_FraigMan_t * p; 00474 Ivy_Man_t * pManAigNew; 00475 Ivy_Obj_t * pObj; 00476 int i, clk; 00477 clk = clock(); 00478 assert( Ivy_ManLatchNum(pManAig) == 0 ); 00479 p = Ivy_FraigStartSimple( pManAig, pParams ); 00480 // set global limits 00481 p->nBTLimitGlobal = s_nBTLimitGlobal; 00482 p->nInsLimitGlobal = s_nInsLimitGlobal; 00483 // duplicate internal nodes 00484 Ivy_ManForEachNode( p->pManAig, pObj, i ) 00485 pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); 00486 // try to prove each output of the miter 00487 Ivy_FraigMiterProve( p ); 00488 // add the POs 00489 Ivy_ManForEachPo( p->pManAig, pObj, i ) 00490 Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) ); 00491 // clean the new manager 00492 Ivy_ManForEachObj( p->pManFraig, pObj, i ) 00493 { 00494 if ( Ivy_ObjFaninVec(pObj) ) 00495 Vec_PtrFree( Ivy_ObjFaninVec(pObj) ); 00496 pObj->pNextFan0 = pObj->pNextFan1 = NULL; 00497 } 00498 // remove dangling nodes 00499 Ivy_ManCleanup( p->pManFraig ); 00500 pManAigNew = p->pManFraig; 00501 p->timeTotal = clock() - clk; 00502 00503 //printf( "Final nodes = %6d. ", Ivy_ManNodeNum(pManAigNew) ); 00504 //PRT( "Time", p->timeTotal ); 00505 Ivy_FraigStop( p ); 00506 return pManAigNew; 00507 }
| void Ivy_FraigParamsDefault | ( | Ivy_FraigParams_t * | pParams | ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Sets the default solving parameters.]
Description []
SideEffects []
SeeAlso []
Definition at line 220 of file ivyFraig.c.
00221 { 00222 memset( pParams, 0, sizeof(Ivy_FraigParams_t) ); 00223 pParams->nSimWords = 32; // the number of words in the simulation info 00224 pParams->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached 00225 pParams->fPatScores = 0; // enables simulation pattern scoring 00226 pParams->MaxScore = 25; // max score after which resimulation is used 00227 pParams->fDoSparse = 1; // skips sparse functions 00228 // pParams->dActConeRatio = 0.05; // the ratio of cone to be bumped 00229 // pParams->dActConeBumpMax = 5.0; // the largest bump of activity 00230 pParams->dActConeRatio = 0.3; // the ratio of cone to be bumped 00231 pParams->dActConeBumpMax = 10.0; // the largest bump of activity 00232 00233 pParams->nBTLimitNode = 100; // conflict limit at a node 00234 pParams->nBTLimitMiter = 500000; // conflict limit at an output 00235 // pParams->nBTLimitGlobal = 0; // conflict limit global 00236 // pParams->nInsLimitGlobal = 0; // inspection limit global 00237 }
| Ivy_Man_t* Ivy_FraigPerform | ( | Ivy_Man_t * | pManAig, | |
| Ivy_FraigParams_t * | pParams | |||
| ) |
Function*************************************************************
Synopsis [Performs fraiging of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 442 of file ivyFraig.c.
00443 { 00444 Ivy_FraigMan_t * p; 00445 Ivy_Man_t * pManAigNew; 00446 int clk; 00447 if ( Ivy_ManNodeNum(pManAig) == 0 ) 00448 return Ivy_ManDup(pManAig); 00449 clk = clock(); 00450 assert( Ivy_ManLatchNum(pManAig) == 0 ); 00451 p = Ivy_FraigStart( pManAig, pParams ); 00452 Ivy_FraigSimulate( p ); 00453 Ivy_FraigSweep( p ); 00454 pManAigNew = p->pManFraig; 00455 p->timeTotal = clock() - clk; 00456 Ivy_FraigStop( p ); 00457 return pManAigNew; 00458 }
| int Ivy_FraigProve | ( | Ivy_Man_t ** | ppManAig, | |
| void * | pPars | |||
| ) |
Function*************************************************************
Synopsis [Performs combinational equivalence checking for the miter.]
Description []
SideEffects []
SeeAlso []
Definition at line 250 of file ivyFraig.c.
00251 { 00252 Prove_Params_t * pParams = pPars; 00253 Ivy_FraigParams_t Params, * pIvyParams = &Params; 00254 Ivy_Man_t * pManAig, * pManTemp; 00255 int RetValue, nIter, clk, timeStart = clock();//, Counter; 00256 sint64 nSatConfs, nSatInspects; 00257 00258 // start the network and parameters 00259 pManAig = *ppManAig; 00260 Ivy_FraigParamsDefault( pIvyParams ); 00261 pIvyParams->fVerbose = pParams->fVerbose; 00262 pIvyParams->fProve = 1; 00263 00264 if ( pParams->fVerbose ) 00265 { 00266 printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n", 00267 pParams->nItersMax, pParams->fUseRewriting? "yes":"no", pParams->fUseFraiging? "yes":"no" ); 00268 printf( "Mitering = %d (%3.1f). Rewriting = %d (%3.1f). Fraiging = %d (%3.1f).\n", 00269 pParams->nMiteringLimitStart, pParams->nMiteringLimitMulti, 00270 pParams->nRewritingLimitStart, pParams->nRewritingLimitMulti, 00271 pParams->nFraigingLimitStart, pParams->nFraigingLimitMulti ); 00272 printf( "Mitering last = %d.\n", 00273 pParams->nMiteringLimitLast ); 00274 } 00275 00276 // if SAT only, solve without iteration 00277 if ( !pParams->fUseRewriting && !pParams->fUseFraiging ) 00278 { 00279 clk = clock(); 00280 pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig); 00281 pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp ); 00282 RetValue = Ivy_FraigMiterStatus( pManAig ); 00283 Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); 00284 *ppManAig = pManAig; 00285 return RetValue; 00286 } 00287 00288 if ( Ivy_ManNodeNum(pManAig) < 500 ) 00289 { 00290 // run the first mitering 00291 clk = clock(); 00292 pIvyParams->nBTLimitMiter = pParams->nMiteringLimitStart / Ivy_ManPoNum(pManAig); 00293 pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp ); 00294 RetValue = Ivy_FraigMiterStatus( pManAig ); 00295 Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); 00296 if ( RetValue >= 0 ) 00297 { 00298 *ppManAig = pManAig; 00299 return RetValue; 00300 } 00301 } 00302 00303 // check the current resource limits 00304 RetValue = -1; 00305 for ( nIter = 0; nIter < pParams->nItersMax; nIter++ ) 00306 { 00307 if ( pParams->fVerbose ) 00308 { 00309 printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter+1, 00310 (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 00311 (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)) ); 00312 fflush( stdout ); 00313 } 00314 00315 // try rewriting 00316 if ( pParams->fUseRewriting ) 00317 { // bug in Ivy_NodeFindCutsAll() when leaves are identical! 00318 /* 00319 clk = clock(); 00320 Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter)); 00321 pManAig = Ivy_ManRwsat( pManAig, 0 ); 00322 RetValue = Ivy_FraigMiterStatus( pManAig ); 00323 Ivy_FraigMiterPrint( pManAig, "Rewriting ", clk, pParams->fVerbose ); 00324 */ 00325 } 00326 if ( RetValue >= 0 ) 00327 break; 00328 00329 // try fraiging followed by mitering 00330 if ( pParams->fUseFraiging ) 00331 { 00332 clk = clock(); 00333 pIvyParams->nBTLimitNode = (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)); 00334 pIvyParams->nBTLimitMiter = (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)) / Ivy_ManPoNum(pManAig); 00335 pManAig = Ivy_FraigPerform_int( pManTemp = pManAig, pIvyParams, pParams->nTotalBacktrackLimit, pParams->nTotalInspectLimit, &nSatConfs, &nSatInspects ); Ivy_ManStop( pManTemp ); 00336 RetValue = Ivy_FraigMiterStatus( pManAig ); 00337 Ivy_FraigMiterPrint( pManAig, "Fraiging ", clk, pParams->fVerbose ); 00338 } 00339 if ( RetValue >= 0 ) 00340 break; 00341 00342 // add to the number of backtracks and inspects 00343 pParams->nTotalBacktracksMade += nSatConfs; 00344 pParams->nTotalInspectsMade += nSatInspects; 00345 // check if global resource limit is reached 00346 if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) || 00347 (pParams->nTotalInspectLimit && pParams->nTotalInspectsMade >= pParams->nTotalInspectLimit) ) 00348 { 00349 printf( "Reached global limit on conflicts/inspects. Quitting.\n" ); 00350 *ppManAig = pManAig; 00351 return -1; 00352 } 00353 } 00354 00355 if ( RetValue < 0 ) 00356 { 00357 if ( pParams->fVerbose ) 00358 { 00359 printf( "Attempting SAT with conflict limit %d ...\n", pParams->nMiteringLimitLast ); 00360 fflush( stdout ); 00361 } 00362 clk = clock(); 00363 pIvyParams->nBTLimitMiter = pParams->nMiteringLimitLast / Ivy_ManPoNum(pManAig); 00364 if ( pParams->nTotalBacktrackLimit ) 00365 s_nBTLimitGlobal = pParams->nTotalBacktrackLimit - pParams->nTotalBacktracksMade; 00366 if ( pParams->nTotalInspectLimit ) 00367 s_nInsLimitGlobal = pParams->nTotalInspectLimit - pParams->nTotalInspectsMade; 00368 pManAig = Ivy_FraigMiter( pManTemp = pManAig, pIvyParams ); Ivy_ManStop( pManTemp ); 00369 s_nBTLimitGlobal = 0; 00370 s_nInsLimitGlobal = 0; 00371 RetValue = Ivy_FraigMiterStatus( pManAig ); 00372 Ivy_FraigMiterPrint( pManAig, "SAT solving", clk, pParams->fVerbose ); 00373 // make sure that the sover never returns "undecided" when infinite resource limits are set 00374 if( RetValue == -1 && pParams->nTotalInspectLimit == 0 && 00375 pParams->nTotalBacktrackLimit == 0 ) 00376 { 00377 extern void Prove_ParamsPrint( Prove_Params_t * pParams ); 00378 Prove_ParamsPrint( pParams ); 00379 printf("ERROR: ABC has returned \"undecided\" in spite of no limits...\n"); 00380 exit(1); 00381 } 00382 } 00383 00384 // assign the model if it was proved by rewriting (const 1 miter) 00385 if ( RetValue == 0 && pManAig->pData == NULL ) 00386 { 00387 pManAig->pData = ALLOC( int, Ivy_ManPiNum(pManAig) ); 00388 memset( pManAig->pData, 0, sizeof(int) * Ivy_ManPiNum(pManAig) ); 00389 } 00390 *ppManAig = pManAig; 00391 return RetValue; 00392 }
| static int Ivy_InfoHasBit | ( | unsigned * | p, | |
| int | i | |||
| ) | [inline, static] |
| static void Ivy_InfoSetBit | ( | unsigned * | p, | |
| int | i | |||
| ) | [inline, static] |
| static void Ivy_InfoXorBit | ( | unsigned * | p, | |
| int | i | |||
| ) | [inline, static] |
| static Ivy_Init_t Ivy_InitAnd | ( | Ivy_Init_t | InitA, | |
| Ivy_Init_t | InitB | |||
| ) | [static] |
Definition at line 336 of file ivy.h.
00337 { 00338 assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE ); 00339 if ( InitA == IVY_INIT_0 || InitB == IVY_INIT_0 ) 00340 return IVY_INIT_0; 00341 if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC ) 00342 return IVY_INIT_DC; 00343 return IVY_INIT_1; 00344 }
| static Ivy_Init_t Ivy_InitExor | ( | Ivy_Init_t | InitA, | |
| Ivy_Init_t | InitB | |||
| ) | [static] |
Definition at line 347 of file ivy.h.
00348 { 00349 assert( InitA != IVY_INIT_NONE && InitB != IVY_INIT_NONE ); 00350 if ( InitA == IVY_INIT_DC || InitB == IVY_INIT_DC ) 00351 return IVY_INIT_DC; 00352 if ( InitA == IVY_INIT_0 && InitB == IVY_INIT_1 ) 00353 return IVY_INIT_1; 00354 if ( InitA == IVY_INIT_1 && InitB == IVY_INIT_0 ) 00355 return IVY_INIT_1; 00356 return IVY_INIT_0; 00357 }
| static Ivy_Init_t Ivy_InitNotCond | ( | Ivy_Init_t | Init, | |
| int | fCompl | |||
| ) | [static] |
Definition at line 323 of file ivy.h.
00324 { 00325 assert( Init != IVY_INIT_NONE ); 00326 if ( fCompl == 0 ) 00327 return Init; 00328 if ( Init == IVY_INIT_0 ) 00329 return IVY_INIT_1; 00330 if ( Init == IVY_INIT_1 ) 00331 return IVY_INIT_0; 00332 return IVY_INIT_DC; 00333 }
| static int Ivy_IsComplement | ( | Ivy_Obj_t * | p | ) | [inline, static] |
| Ivy_Obj_t* Ivy_Latch | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t * | pObj, | |||
| Ivy_Init_t | Init | |||
| ) |
Function*************************************************************
Synopsis [Performs canonicization step.]
Description []
SideEffects []
SeeAlso []
Definition at line 284 of file ivyOper.c.
00285 { 00286 return Ivy_CanonLatch( p, pObj, Init ); 00287 }
| static int Ivy_LeafCreate | ( | int | Id, | |
| int | Lat | |||
| ) | [inline, static] |
Definition at line 210 of file ivy.h.
00210 { return (Id << IVY_LEAF_BITS) | Lat; }
| static int Ivy_LeafId | ( | int | Leaf | ) | [inline, static] |
Definition at line 211 of file ivy.h.
00211 { return Leaf >> IVY_LEAF_BITS; }
| static int Ivy_LeafLat | ( | int | Leaf | ) | [inline, static] |
Definition at line 212 of file ivy.h.
00212 { return Leaf & IVY_LEAF_MASK; }
Function*************************************************************
Synopsis [Implements ITE operation.]
Description []
SideEffects []
SeeAlso []
| static int Ivy_ManAndNum | ( | Ivy_Man_t * | p | ) | [inline, static] |
| static int Ivy_ManAssertNum | ( | Ivy_Man_t * | p | ) | [inline, static] |
Definition at line 216 of file ivy.h.
00216 { return p->nObjs[IVY_ASSERT]; }
FUNCTION DECLARATIONS ///
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Performs algebraic balancing of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 48 of file ivyBalance.c.
00049 { 00050 Ivy_Man_t * pNew; 00051 Ivy_Obj_t * pObj, * pDriver; 00052 Vec_Vec_t * vStore; 00053 int i, NewNodeId; 00054 // clean the old manager 00055 Ivy_ManCleanTravId( p ); 00056 // create the new manager 00057 pNew = Ivy_ManStart(); 00058 // map the nodes 00059 Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) ); 00060 Ivy_ManForEachPi( p, pObj, i ) 00061 pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) ); 00062 // if HAIG is defined, trasfer the pointers to the PIs/latches 00063 // if ( p->pHaig ) 00064 // Ivy_ManHaigTrasfer( p, pNew ); 00065 // balance the AIG 00066 vStore = Vec_VecAlloc( 50 ); 00067 Ivy_ManForEachPo( p, pObj, i ) 00068 { 00069 pDriver = Ivy_ObjReal( Ivy_ObjChild0(pObj) ); 00070 NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel ); 00071 NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) ); 00072 Ivy_ObjCreatePo( pNew, Ivy_EdgeToNode(pNew, NewNodeId) ); 00073 } 00074 Vec_VecFree( vStore ); 00075 if ( i = Ivy_ManCleanup( pNew ) ) 00076 { 00077 // printf( "Cleanup after balancing removed %d dangling nodes.\n", i ); 00078 } 00079 // check the resulting AIG 00080 if ( !Ivy_ManCheck(pNew) ) 00081 printf( "Ivy_ManBalance(): The check has failed.\n" ); 00082 return pNew; 00083 }
| static int Ivy_ManBufNum | ( | Ivy_Man_t * | p | ) | [inline, static] |
| int Ivy_ManCheck | ( | Ivy_Man_t * | p | ) |
CFile****************************************************************
FileName [ivyCheck.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [AIG checking procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [
- Id
- ivyCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Checks the consistency of the AIG manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file ivyCheck.c.
00043 { 00044 Ivy_Obj_t * pObj, * pObj2; 00045 int i; 00046 Ivy_ManForEachObj( p, pObj, i ) 00047 { 00048 // skip deleted nodes 00049 if ( Ivy_ObjId(pObj) != i ) 00050 { 00051 printf( "Ivy_ManCheck: Node with ID %d is listed as number %d in the array of objects.\n", pObj->Id, i ); 00052 return 0; 00053 } 00054 // consider the constant node and PIs 00055 if ( i == 0 || Ivy_ObjIsPi(pObj) ) 00056 { 00057 if ( Ivy_ObjFaninId0(pObj) || Ivy_ObjFaninId1(pObj) || Ivy_ObjLevel(pObj) ) 00058 { 00059 printf( "Ivy_ManCheck: The AIG has non-standard constant or PI node with ID \"%d\".\n", pObj->Id ); 00060 return 0; 00061 } 00062 continue; 00063 } 00064 if ( Ivy_ObjIsPo(pObj) ) 00065 { 00066 if ( Ivy_ObjFaninId1(pObj) ) 00067 { 00068 printf( "Ivy_ManCheck: The AIG has non-standard PO node with ID \"%d\".\n", pObj->Id ); 00069 return 0; 00070 } 00071 continue; 00072 } 00073 if ( Ivy_ObjIsBuf(pObj) ) 00074 { 00075 if ( Ivy_ObjFanin1(pObj) ) 00076 { 00077 printf( "Ivy_ManCheck: The buffer with ID \"%d\" contains second fanin.\n", pObj->Id ); 00078 return 0; 00079 } 00080 continue; 00081 } 00082 if ( Ivy_ObjIsLatch(pObj) ) 00083 { 00084 if ( Ivy_ObjFanin1(pObj) ) 00085 { 00086 printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id ); 00087 return 0; 00088 } 00089 if ( Ivy_ObjInit(pObj) == IVY_INIT_NONE ) 00090 { 00091 printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id ); 00092 return 0; 00093 } 00094 pObj2 = Ivy_TableLookup( p, pObj ); 00095 if ( pObj2 != pObj ) 00096 printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id ); 00097 continue; 00098 } 00099 // consider the AND node 00100 if ( !Ivy_ObjFanin0(pObj) || !Ivy_ObjFanin1(pObj) ) 00101 { 00102 printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a NULL fanin.\n", pObj->Id ); 00103 return 0; 00104 } 00105 if ( Ivy_ObjFaninId0(pObj) >= Ivy_ObjFaninId1(pObj) ) 00106 { 00107 printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id ); 00108 return 0; 00109 } 00110 if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) ) 00111 printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) ); 00112 pObj2 = Ivy_TableLookup( p, pObj ); 00113 if ( pObj2 != pObj ) 00114 printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id ); 00115 if ( Ivy_ObjRefs(pObj) == 0 ) 00116 printf( "Ivy_ManCheck: Node with ID \"%d\" has no fanouts.\n", pObj->Id ); 00117 // check fanouts 00118 if ( p->fFanout && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) ) 00119 printf( "Ivy_ManCheck: Node with ID \"%d\" has mismatch between the number of fanouts and refs.\n", pObj->Id ); 00120 } 00121 // count the number of nodes in the table 00122 if ( Ivy_TableCountEntries(p) != Ivy_ManAndNum(p) + Ivy_ManExorNum(p) + Ivy_ManLatchNum(p) ) 00123 { 00124 printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); 00125 return 0; 00126 } 00127 // if ( !Ivy_ManCheckFanouts(p) ) 00128 // return 0; 00129 if ( !Ivy_ManIsAcyclic(p) ) 00130 return 0; 00131 return 1; 00132 }
| int Ivy_ManCheckChoices | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Checks that each choice node has exactly one node with fanouts.]
Description []
SideEffects []
SeeAlso []
Definition at line 252 of file ivyCheck.c.
00253 { 00254 Ivy_Obj_t * pObj, * pTemp; 00255 int i; 00256 Ivy_ManForEachObj( p->pHaig, pObj, i ) 00257 { 00258 if ( Ivy_ObjRefs(pObj) == 0 ) 00259 continue; 00260 // count the number of nodes in the loop 00261 assert( !Ivy_IsComplement(pObj->pEquiv) ); 00262 for ( pTemp = pObj->pEquiv; pTemp && pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) ) 00263 if ( Ivy_ObjRefs(pTemp) > 1 ) 00264 printf( "Node %d has member %d in its equiv class with %d fanouts.\n", pObj->Id, pTemp->Id, Ivy_ObjRefs(pTemp) ); 00265 } 00266 return 1; 00267 }
| int Ivy_ManCheckFanoutNums | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Verifies the fanouts.]
Description []
SideEffects []
SeeAlso []
Definition at line 145 of file ivyCheck.c.
00146 { 00147 Ivy_Obj_t * pObj; 00148 int i, Counter = 0; 00149 Ivy_ManForEachObj( p, pObj, i ) 00150 if ( Ivy_ObjIsNode(pObj) ) 00151 Counter += (Ivy_ObjRefs(pObj) == 0); 00152 if ( Counter ) 00153 printf( "Sequential AIG has %d dangling nodes.\n", Counter ); 00154 return Counter; 00155 }
| int Ivy_ManCheckFanouts | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Verifies the fanouts.]
Description []
SideEffects []
SeeAlso []
Definition at line 168 of file ivyCheck.c.
00169 { 00170 Vec_Ptr_t * vFanouts; 00171 Ivy_Obj_t * pObj, * pFanout, * pFanin; 00172 int i, k, RetValue = 1; 00173 if ( !p->fFanout ) 00174 return 1; 00175 vFanouts = Vec_PtrAlloc( 100 ); 00176 // make sure every fanin is a fanout 00177 Ivy_ManForEachObj( p, pObj, i ) 00178 { 00179 pFanin = Ivy_ObjFanin0(pObj); 00180 if ( pFanin == NULL ) 00181 continue; 00182 Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k ) 00183 if ( pFanout == pObj ) 00184 break; 00185 if ( k == Vec_PtrSize(vFanouts) ) 00186 { 00187 printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id ); 00188 RetValue = 0; 00189 } 00190 00191 pFanin = Ivy_ObjFanin1(pObj); 00192 if ( pFanin == NULL ) 00193 continue; 00194 Ivy_ObjForEachFanout( p, pFanin, vFanouts, pFanout, k ) 00195 if ( pFanout == pObj ) 00196 break; 00197 if ( k == Vec_PtrSize(vFanouts) ) 00198 { 00199 printf( "Node %d is a fanin of node %d but the fanout is not there.\n", pFanin->Id, pObj->Id ); 00200 RetValue = 0; 00201 } 00202 // check that the previous fanout has the same fanin 00203 if ( pObj->pPrevFan0 ) 00204 { 00205 if ( Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 00206 Ivy_ObjFanin0(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) && 00207 Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin0(pObj) && 00208 Ivy_ObjFanin1(pObj->pPrevFan0) != Ivy_ObjFanin1(pObj) ) 00209 { 00210 printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan0->Id ); 00211 RetValue = 0; 00212 } 00213 } 00214 // check that the previous fanout has the same fanin 00215 if ( pObj->pPrevFan1 ) 00216 { 00217 if ( Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 00218 Ivy_ObjFanin0(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) && 00219 Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin0(pObj) && 00220 Ivy_ObjFanin1(pObj->pPrevFan1) != Ivy_ObjFanin1(pObj) ) 00221 { 00222 printf( "Node %d has prev %d without common fanin.\n", pObj->Id, pObj->pPrevFan1->Id ); 00223 RetValue = 0; 00224 } 00225 } 00226 } 00227 // make sure every fanout is a fanin 00228 Ivy_ManForEachObj( p, pObj, i ) 00229 { 00230 Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, k ) 00231 if ( Ivy_ObjFanin0(pFanout) != pObj && Ivy_ObjFanin1(pFanout) != pObj ) 00232 { 00233 printf( "Node %d is a fanout of node %d but the fanin is not there.\n", pFanout->Id, pObj->Id ); 00234 RetValue = 0; 00235 } 00236 } 00237 Vec_PtrFree( vFanouts ); 00238 return RetValue; 00239 }
| void Ivy_ManCleanTravId | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Sets the DFS ordering of the nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 60 of file ivyUtil.c.
00061 { 00062 Ivy_Obj_t * pObj; 00063 int i; 00064 p->nTravIds = 1; 00065 Ivy_ManForEachObj( p, pObj, i ) 00066 pObj->TravId = 0; 00067 }
| int Ivy_ManCleanup | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Removes nodes without fanout.]
Description [Returns the number of dangling nodes removed.]
SideEffects []
SeeAlso []
Definition at line 262 of file ivyMan.c.
00263 { 00264 Ivy_Obj_t * pNode; 00265 int i, nNodesOld; 00266 nNodesOld = Ivy_ManNodeNum(p); 00267 Ivy_ManForEachObj( p, pNode, i ) 00268 if ( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) 00269 if ( Ivy_ObjRefs(pNode) == 0 ) 00270 Ivy_ObjDelete_rec( p, pNode, 1 ); 00271 //printf( "Cleanup removed %d nodes.\n", nNodesOld - Ivy_ManNodeNum(p) ); 00272 return nNodesOld - Ivy_ManNodeNum(p); 00273 }
Function*************************************************************
Synopsis [Collects nodes in the cone.]
Description []
SideEffects []
SeeAlso []
Definition at line 192 of file ivyDfs.c.
00193 { 00194 Ivy_Obj_t * pTemp; 00195 int i; 00196 assert( !Ivy_IsComplement(pObj) ); 00197 assert( Ivy_ObjIsNode(pObj) ); 00198 // mark the nodes 00199 Vec_PtrForEachEntry( vFront, pTemp, i ) 00200 Ivy_Regular(pTemp)->fMarkA = 1; 00201 assert( pObj->fMarkA == 0 ); 00202 // collect the cone 00203 Vec_PtrClear( vCone ); 00204 Ivy_ManCollectCone_rec( pObj, vCone ); 00205 // unmark the nodes 00206 Vec_PtrForEachEntry( vFront, pTemp, i ) 00207 Ivy_Regular(pTemp)->fMarkA = 0; 00208 }
| void Ivy_ManCollectCut | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t * | pRoot, | |||
| Vec_Int_t * | vLeaves, | |||
| Vec_Int_t * | vNodes | |||
| ) |
Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description [Does not modify the array of leaves. Uses array vTruth to store temporary truth tables. The returned pointer should be used immediately.]
SideEffects []
SeeAlso []
Definition at line 103 of file ivyUtil.c.
00104 { 00105 int i, Leaf; 00106 // collect and mark the leaves 00107 Vec_IntClear( vNodes ); 00108 Vec_IntForEachEntry( vLeaves, Leaf, i ) 00109 { 00110 Vec_IntPush( vNodes, Leaf ); 00111 Ivy_ManObj(p, Leaf)->fMarkA = 1; 00112 } 00113 // collect and mark the nodes 00114 Ivy_ManCollectCut_rec( p, pRoot, vNodes ); 00115 // clean the nodes 00116 Vec_IntForEachEntry( vNodes, Leaf, i ) 00117 Ivy_ManObj(p, Leaf)->fMarkA = 0; 00118 }
| unsigned* Ivy_ManCutTruth | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t * | pRoot, | |||
| Vec_Int_t * | vLeaves, | |||
| Vec_Int_t * | vNodes, | |||
| Vec_Int_t * | vTruth | |||
| ) |
Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description [Does not modify the array of leaves. Uses array vTruth to store temporary truth tables. The returned pointer should be used immediately.]
SideEffects []
SeeAlso []
Definition at line 183 of file ivyUtil.c.
00184 { 00185 static unsigned uTruths[8][8] = { // elementary truth tables 00186 { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, 00187 { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, 00188 { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, 00189 { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, 00190 { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 00191 { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 00192 { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 00193 { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 00194 }; 00195 int i, Leaf; 00196 // collect the cut 00197 Ivy_ManCollectCut( p, pRoot, vLeaves, vNodes ); 00198 // set the node numbers 00199 Vec_IntForEachEntry( vNodes, Leaf, i ) 00200 Ivy_ManObj(p, Leaf)->TravId = i; 00201 // alloc enough memory 00202 Vec_IntClear( vTruth ); 00203 Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) ); 00204 // set the elementary truth tables 00205 Vec_IntForEachEntry( vLeaves, Leaf, i ) 00206 memcpy( Ivy_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) ); 00207 // compute truths for other nodes 00208 Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) ) 00209 Ivy_ManCutTruthOne( p, Ivy_ManObj(p, Leaf), vTruth, 8 ); 00210 return Ivy_ObjGetTruthStore( pRoot->TravId, vTruth ); 00211 }
Function*************************************************************
Synopsis [Collects AND/EXOR nodes in the DFS order from CIs to COs.]
Description []
SideEffects []
SeeAlso []
Definition at line 84 of file ivyDfs.c.
00085 { 00086 Vec_Int_t * vNodes; 00087 Ivy_Obj_t * pObj; 00088 int i; 00089 assert( Ivy_ManLatchNum(p) == 0 ); 00090 // make sure the nodes are not marked 00091 Ivy_ManForEachObj( p, pObj, i ) 00092 assert( !pObj->fMarkA && !pObj->fMarkB ); 00093 // collect the nodes 00094 vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) ); 00095 Ivy_ManForEachPo( p, pObj, i ) 00096 Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes ); 00097 // unmark the collected nodes 00098 // Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) 00099 // Ivy_ObjClearMarkA(pObj); 00100 Ivy_ManForEachObj( p, pObj, i ) 00101 Ivy_ObjClearMarkA(pObj); 00102 // make sure network does not have dangling nodes 00103 assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) ); 00104 return vNodes; 00105 }
Function*************************************************************
Synopsis [Collects AND/EXOR nodes in the DFS order from CIs to COs.]
Description []
SideEffects []
SeeAlso []
Definition at line 118 of file ivyDfs.c.
00119 { 00120 Vec_Int_t * vNodes, * vLatches; 00121 Ivy_Obj_t * pObj; 00122 int i; 00123 // assert( Ivy_ManLatchNum(p) > 0 ); 00124 // make sure the nodes are not marked 00125 Ivy_ManForEachObj( p, pObj, i ) 00126 assert( !pObj->fMarkA && !pObj->fMarkB ); 00127 // collect the latches 00128 vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) ); 00129 Ivy_ManForEachLatch( p, pObj, i ) 00130 Vec_IntPush( vLatches, pObj->Id ); 00131 // collect the nodes 00132 vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) ); 00133 Ivy_ManForEachPo( p, pObj, i ) 00134 Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes ); 00135 Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) 00136 Ivy_ManDfs_rec( p, Ivy_ObjFanin0(pObj), vNodes ); 00137 // unmark the collected nodes 00138 // Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) 00139 // Ivy_ObjClearMarkA(pObj); 00140 Ivy_ManForEachObj( p, pObj, i ) 00141 Ivy_ObjClearMarkA(pObj); 00142 // make sure network does not have dangling nodes 00143 // assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) ); 00144 00145 // temporary!!! 00146 00147 if ( pvLatches == NULL ) 00148 Vec_IntFree( vLatches ); 00149 else 00150 *pvLatches = vLatches; 00151 return vNodes; 00152 }
Function*************************************************************
Synopsis [Implement DSD in the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 648 of file ivyDsd.c.
00649 { 00650 int Entry, i; 00651 // implement latches on the frontier (TEMPORARY!!!) 00652 Vec_IntForEachEntry( vFront, Entry, i ) 00653 Vec_IntWriteEntry( vFront, i, Ivy_LeafId(Entry) ); 00654 // recursively construct the tree 00655 return Ivy_ManDsdConstruct_rec( p, vFront, Vec_IntSize(vTree)-1, vTree ); 00656 }
Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 107 of file ivyMan.c.
00108 { 00109 Vec_Int_t * vNodes, * vLatches; 00110 Ivy_Man_t * pNew; 00111 Ivy_Obj_t * pObj; 00112 int i; 00113 // collect latches and nodes in the DFS order 00114 vNodes = Ivy_ManDfsSeq( p, &vLatches ); 00115 // create the new manager 00116 pNew = Ivy_ManStart(); 00117 // create the PIs 00118 Ivy_ManConst1(p)->pEquiv = Ivy_ManConst1(pNew); 00119 Ivy_ManForEachPi( p, pObj, i ) 00120 pObj->pEquiv = Ivy_ObjCreatePi(pNew); 00121 // create the fake PIs for latches 00122 Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) 00123 pObj->pEquiv = Ivy_ObjCreatePi(pNew); 00124 // duplicate internal nodes 00125 Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) 00126 if ( Ivy_ObjIsBuf(pObj) ) 00127 pObj->pEquiv = Ivy_ObjChild0Equiv(pObj); 00128 else 00129 pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); 00130 // add the POs 00131 Ivy_ManForEachPo( p, pObj, i ) 00132 Ivy_ObjCreatePo( pNew, Ivy_ObjChild0Equiv(pObj) ); 00133 // transform additional PI nodes into latches and connect them 00134 Ivy_ManForEachNodeVec( p, vLatches, pObj, i ) 00135 { 00136 assert( !Ivy_ObjFaninC0(pObj) ); 00137 pObj->pEquiv->Type = IVY_LATCH; 00138 pObj->pEquiv->Init = pObj->Init; 00139 Ivy_ObjConnect( pNew, pObj->pEquiv, Ivy_ObjChild0Equiv(pObj), NULL ); 00140 } 00141 // shrink the arrays 00142 Vec_PtrShrink( pNew->vPis, Ivy_ManPiNum(p) ); 00143 // update the counters of different objects 00144 pNew->nObjs[IVY_PI] -= Ivy_ManLatchNum(p); 00145 pNew->nObjs[IVY_LATCH] += Ivy_ManLatchNum(p); 00146 // free arrays 00147 Vec_IntFree( vNodes ); 00148 Vec_IntFree( vLatches ); 00149 // make sure structural hashing did not change anything 00150 assert( Ivy_ManNodeNum(p) == Ivy_ManNodeNum(pNew) ); 00151 assert( Ivy_ManLatchNum(p) == Ivy_ManLatchNum(pNew) ); 00152 // check the resulting network 00153 if ( !Ivy_ManCheck(pNew) ) 00154 printf( "Ivy_ManMakeSeq(): The check has failed.\n" ); 00155 return pNew; 00156 }
| static int Ivy_ManExorNum | ( | Ivy_Man_t * | p | ) | [inline, static] |
| Ivy_Man_t* Ivy_ManFrames | ( | Ivy_Man_t * | pMan, | |
| int | nLatches, | |||
| int | nFrames, | |||
| int | fInit, | |||
| Vec_Ptr_t ** | pvMapping | |||
| ) |
Function*************************************************************
Synopsis [Stops the AIG manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 169 of file ivyMan.c.
00170 { 00171 Vec_Ptr_t * vMapping; 00172 Ivy_Man_t * pNew; 00173 Ivy_Obj_t * pObj; 00174 int i, f, nPis, nPos, nIdMax; 00175 assert( Ivy_ManLatchNum(pMan) == 0 ); 00176 assert( nFrames > 0 ); 00177 // prepare the mapping 00178 nPis = Ivy_ManPiNum(pMan) - nLatches; 00179 nPos = Ivy_ManPoNum(pMan) - nLatches; 00180 nIdMax = Ivy_ManObjIdMax(pMan); 00181 // create the new manager 00182 pNew = Ivy_ManStart(); 00183 // set the starting values of latch inputs 00184 for ( i = 0; i < nLatches; i++ ) 00185 Ivy_ManPo(pMan, nPos+i)->pEquiv = fInit? Ivy_Not(Ivy_ManConst1(pNew)) : Ivy_ObjCreatePi(pNew); 00186 // add timeframes 00187 vMapping = Vec_PtrStart( nIdMax * nFrames + 1 ); 00188 for ( f = 0; f < nFrames; f++ ) 00189 { 00190 // create PIs 00191 Ivy_ManConst1(pMan)->pEquiv = Ivy_ManConst1(pNew); 00192 for ( i = 0; i < nPis; i++ ) 00193 Ivy_ManPi(pMan, i)->pEquiv = Ivy_ObjCreatePi(pNew); 00194 // transfer values to latch outputs 00195 for ( i = 0; i < nLatches; i++ ) 00196 Ivy_ManPi(pMan, nPis+i)->pEquiv = Ivy_ManPo(pMan, nPos+i)->pEquiv; 00197 // perform strashing 00198 Ivy_ManForEachNode( pMan, pObj, i ) 00199 pObj->pEquiv = Ivy_And( pNew, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); 00200 // create POs 00201 for ( i = 0; i < nPos; i++ ) 00202 Ivy_ManPo(pMan, i)->pEquiv = Ivy_ObjCreatePo( pNew, Ivy_ObjChild0Equiv(Ivy_ManPo(pMan, i)) ); 00203 // set the results of latch inputs 00204 for ( i = 0; i < nLatches; i++ ) 00205 Ivy_ManPo(pMan, nPos+i)->pEquiv = Ivy_ObjChild0Equiv(Ivy_ManPo(pMan, nPos+i)); 00206 // save the pointers in this frame 00207 Ivy_ManForEachObj( pMan, pObj, i ) 00208 Vec_PtrWriteEntry( vMapping, f * nIdMax + i, pObj->pEquiv ); 00209 } 00210 // connect latches 00211 if ( !fInit ) 00212 for ( i = 0; i < nLatches; i++ ) 00213 Ivy_ObjCreatePo( pNew, Ivy_ManPo(pMan, nPos+i)->pEquiv ); 00214 // remove dangling nodes 00215 Ivy_ManCleanup(pNew); 00216 *pvMapping = vMapping; 00217 // check the resulting network 00218 if ( !Ivy_ManCheck(pNew) ) 00219 printf( "Ivy_ManFrames(): The check has failed.\n" ); 00220 return pNew; 00221 }
| static int Ivy_ManGetCost | ( | Ivy_Man_t * | p | ) | [inline, static] |
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 }
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 }
| 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 }
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 }
| static int Ivy_ManHashObjNum | ( | Ivy_Man_t * | p | ) | [inline, static] |
| void Ivy_ManIncrementTravId | ( | Ivy_Man_t * | p | ) |
CFile****************************************************************
FileName [ivyUtil.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [Various procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [
- Id
- ivyUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Increments the current traversal ID of the network.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file ivyUtil.c.
00043 { 00044 if ( p->nTravIds >= (1<<30)-1 - 1000 ) 00045 Ivy_ManCleanTravId( p ); 00046 p->nTravIds++; 00047 }
| int Ivy_ManIsAcyclic | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Detects combinational loops.]
Description [This procedure is based on the idea suggested by Donald Chai. As we traverse the network and visit the nodes, we need to distinquish three types of nodes: (1) those that are visited for the first time, (2) those that have been visited in this traversal but are currently not on the traversal path, (3) those that have been visited and are currently on the travesal path. When the node of type (3) is encountered, it means that there is a combinational loop. To mark the three types of nodes, two new values of the traversal IDs are used.]
SideEffects []
SeeAlso []
Definition at line 370 of file ivyDfs.c.
00371 { 00372 Ivy_Obj_t * pObj; 00373 int fAcyclic, i; 00374 // set the traversal ID for this DFS ordering 00375 Ivy_ManIncrementTravId( p ); 00376 Ivy_ManIncrementTravId( p ); 00377 // pObj->TravId == pNet->nTravIds means "pObj is on the path" 00378 // pObj->TravId == pNet->nTravIds - 1 means "pObj is visited but is not on the path" 00379 // pObj->TravId < pNet->nTravIds - 1 means "pObj is not visited" 00380 // traverse the network to detect cycles 00381 fAcyclic = 1; 00382 Ivy_ManForEachCo( p, pObj, i ) 00383 { 00384 // traverse the output logic cone 00385 if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pObj)) ) 00386 continue; 00387 // stop as soon as the first loop is detected 00388 fprintf( stdout, " (cone of %s \"%d\")\n", Ivy_ObjIsLatch(pObj)? "latch" : "PO", Ivy_ObjId(pObj) ); 00389 break; 00390 } 00391 return fAcyclic; 00392 }
Function*************************************************************
Synopsis [Collect the latches.]
Description []
SideEffects []
SeeAlso []
Definition at line 224 of file ivyUtil.c.
00225 { 00226 Vec_Int_t * vLatches; 00227 Ivy_Obj_t * pObj; 00228 int i; 00229 vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) ); 00230 Ivy_ManForEachLatch( p, pObj, i ) 00231 Vec_IntPush( vLatches, pObj->Id ); 00232 return vLatches; 00233 }
| static int Ivy_ManLatchNum | ( | Ivy_Man_t * | p | ) | [inline, static] |
Function*************************************************************
Synopsis [Returns the nodes by level.]
Description []
SideEffects []
SeeAlso []
Definition at line 221 of file ivyDfs.c.
00222 { 00223 Vec_Vec_t * vNodes; 00224 Ivy_Obj_t * pObj; 00225 int i; 00226 vNodes = Vec_VecAlloc( 100 ); 00227 Ivy_ManForEachObj( p, pObj, i ) 00228 { 00229 assert( !Ivy_ObjIsBuf(pObj) ); 00230 if ( Ivy_ObjIsNode(pObj) ) 00231 Vec_VecPush( vNodes, pObj->Level, pObj ); 00232 } 00233 return vNodes; 00234 }
| int Ivy_ManLevels | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Collect the latches.]
Description []
SideEffects []
SeeAlso []
Definition at line 246 of file ivyUtil.c.
00247 { 00248 Ivy_Obj_t * pObj; 00249 int i, LevelMax = 0; 00250 Ivy_ManForEachPo( p, pObj, i ) 00251 LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level ); 00252 return LevelMax; 00253 }
| void Ivy_ManMakeSeq | ( | Ivy_Man_t * | p, | |
| int | nLatches, | |||
| int * | pInits | |||
| ) |
Function*************************************************************
Synopsis [Converts a combinational AIG manager into a sequential one.]
Description []
SideEffects []
SeeAlso []
Definition at line 478 of file ivyMan.c.
00479 { 00480 Ivy_Obj_t * pObj, * pLatch; 00481 Ivy_Init_t Init; 00482 int i; 00483 if ( nLatches == 0 ) 00484 return; 00485 assert( nLatches < Ivy_ManPiNum(p) && nLatches < Ivy_ManPoNum(p) ); 00486 assert( Ivy_ManPiNum(p) == Vec_PtrSize(p->vPis) ); 00487 assert( Ivy_ManPoNum(p) == Vec_PtrSize(p->vPos) ); 00488 assert( Vec_PtrSize( p->vBufs ) == 0 ); 00489 // create fanouts 00490 if ( p->fFanout == 0 ) 00491 Ivy_ManStartFanout( p ); 00492 // collect the POs to be converted into latches 00493 for ( i = 0; i < nLatches; i++ ) 00494 { 00495 // get the latch value 00496 Init = pInits? pInits[i] : IVY_INIT_0; 00497 // create latch 00498 pObj = Ivy_ManPo( p, Ivy_ManPoNum(p) - nLatches + i ); 00499 pLatch = Ivy_Latch( p, Ivy_ObjChild0(pObj), Init ); 00500 Ivy_ObjDisconnect( p, pObj ); 00501 // recycle the old PO object 00502 Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); 00503 Ivy_ManRecycleMemory( p, pObj ); 00504 // convert the corresponding PI to a buffer and connect it to the latch 00505 pObj = Ivy_ManPi( p, Ivy_ManPiNum(p) - nLatches + i ); 00506 pObj->Type = IVY_BUF; 00507 Ivy_ObjConnect( p, pObj, pLatch, NULL ); 00508 // save the buffer 00509 Vec_PtrPush( p->vBufs, pObj ); 00510 } 00511 // shrink the arrays 00512 Vec_PtrShrink( p->vPis, Ivy_ManPiNum(p) - nLatches ); 00513 Vec_PtrShrink( p->vPos, Ivy_ManPoNum(p) - nLatches ); 00514 // update the counters of different objects 00515 p->nObjs[IVY_PI] -= nLatches; 00516 p->nObjs[IVY_PO] -= nLatches; 00517 p->nObjs[IVY_BUF] += nLatches; 00518 p->nDeleted -= 2 * nLatches; 00519 // remove dangling nodes 00520 Ivy_ManCleanup(p); 00521 Ivy_ManCleanupSeq(p); 00522 /* 00523 // check for dangling nodes 00524 Ivy_ManForEachObj( p, pObj, i ) 00525 if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsPo(pObj) && !Ivy_ObjIsConst1(pObj) ) 00526 { 00527 assert( Ivy_ObjRefs(pObj) > 0 ); 00528 assert( Ivy_ObjRefs(pObj) == Ivy_ObjFanoutNum(p, pObj) ); 00529 } 00530 */ 00531 // perform hashing by propagating the buffers 00532 Ivy_ManPropagateBuffers( p, 0 ); 00533 if ( Ivy_ManBufNum(p) ) 00534 printf( "The number of remaining buffers is %d.\n", Ivy_ManBufNum(p) ); 00535 // fix the levels 00536 Ivy_ManResetLevels( p ); 00537 // check the resulting network 00538 if ( !Ivy_ManCheck(p) ) 00539 printf( "Ivy_ManMakeSeq(): The check has failed.\n" ); 00540 }
| static int Ivy_ManNodeNum | ( | Ivy_Man_t * | p | ) | [inline, static] |
Definition at line 199 of file ivy.h.
00199 { return (Ivy_Obj_t *)Vec_PtrEntry(p->vObjs, i); }
| static int Ivy_ManObjIdMax | ( | Ivy_Man_t * | p | ) | [inline, static] |
Definition at line 222 of file ivy.h.
00222 { return Vec_PtrSize(p->vObjs)-1; }
| static int Ivy_ManObjNum | ( | Ivy_Man_t * | p | ) | [inline, static] |
Definition at line 197 of file ivy.h.
00197 { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPis, i); }
| static int Ivy_ManPiNum | ( | Ivy_Man_t * | p | ) | [inline, static] |
Definition at line 198 of file ivy.h.
00198 { return (Ivy_Obj_t *)Vec_PtrEntry(p->vPos, i); }
| static int Ivy_ManPoNum | ( | Ivy_Man_t * | p | ) | [inline, static] |
| void Ivy_ManPrintStats | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Stops the AIG manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 453 of file ivyMan.c.
00454 { 00455 printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) ); 00456 printf( "A = %7d. ", Ivy_ManAndNum(p) ); 00457 printf( "L = %5d. ", Ivy_ManLatchNum(p) ); 00458 // printf( "X = %d. ", Ivy_ManExorNum(p) ); 00459 // printf( "B = %3d. ", Ivy_ManBufNum(p) ); 00460 printf( "MaxID = %7d. ", Ivy_ManObjIdMax(p) ); 00461 // printf( "Cre = %d. ", p->nCreated ); 00462 // printf( "Del = %d. ", p->nDeleted ); 00463 printf( "Lev = %3d. ", Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) ); 00464 printf( "\n" ); 00465 }
| void Ivy_ManPrintVerbose | ( | Ivy_Man_t * | p, | |
| int | fHaig | |||
| ) |
Function*************************************************************
Synopsis [Prints node in HAIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 711 of file ivyUtil.c.
00712 { 00713 Vec_Int_t * vNodes; 00714 Ivy_Obj_t * pObj; 00715 int i; 00716 printf( "PIs: " ); 00717 Ivy_ManForEachPi( p, pObj, i ) 00718 printf( " %d", pObj->Id ); 00719 printf( "\n" ); 00720 printf( "POs: " ); 00721 Ivy_ManForEachPo( p, pObj, i ) 00722 printf( " %d", pObj->Id ); 00723 printf( "\n" ); 00724 printf( "Latches: " ); 00725 Ivy_ManForEachLatch( p, pObj, i ) 00726 printf( " %d=%d%s", pObj->Id, Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") ); 00727 printf( "\n" ); 00728 vNodes = Ivy_ManDfsSeq( p, NULL ); 00729 Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) 00730 Ivy_ObjPrintVerbose( p, pObj, fHaig ), printf( "\n" ); 00731 printf( "\n" ); 00732 }
| int Ivy_ManPropagateBuffers | ( | Ivy_Man_t * | p, | |
| int | fUpdateLevel | |||
| ) |
Function*************************************************************
Synopsis [Returns the number of dangling nodes removed.]
Description []
SideEffects []
SeeAlso []
Definition at line 411 of file ivyMan.c.
00412 { 00413 Ivy_Obj_t * pNode; 00414 int LimitFactor = 100; 00415 int NodeBeg = Ivy_ManNodeNum(p); 00416 int nSteps; 00417 for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ ) 00418 { 00419 pNode = Vec_PtrEntryLast(p->vBufs); 00420 while ( Ivy_ObjIsBuf(pNode) ) 00421 pNode = Ivy_ObjReadFirstFanout( p, pNode ); 00422 // check if this buffer should remain 00423 if ( Ivy_ManLatchIsSelfFeed(pNode) ) 00424 { 00425 Vec_PtrPop(p->vBufs); 00426 continue; 00427 } 00428 //printf( "Propagating buffer %d with input %d and output %d\n", Ivy_ObjFaninId0(pNode), Ivy_ObjFaninId0(Ivy_ObjFanin0(pNode)), pNode->Id ); 00429 //printf( "Latch num %d\n", Ivy_ManLatchNum(p) ); 00430 Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel ); 00431 if ( nSteps > NodeBeg * LimitFactor ) 00432 { 00433 printf( "Structural hashing is not finished after %d forward latch moves.\n", NodeBeg * LimitFactor ); 00434 printf( "This circuit cannot be forward-retimed completely. Quitting.\n" ); 00435 break; 00436 } 00437 } 00438 // printf( "Number of steps = %d. Nodes beg = %d. Nodes end = %d.\n", nSteps, NodeBeg, Ivy_ManNodeNum(p) ); 00439 return nSteps; 00440 }
Function*************************************************************
Synopsis [Computes required levels for each node.]
Description [Assumes topological ordering of the nodes.]
SideEffects []
SeeAlso []
Definition at line 247 of file ivyDfs.c.
00248 { 00249 Ivy_Obj_t * pObj; 00250 Vec_Int_t * vLevelsR; 00251 Vec_Vec_t * vNodes; 00252 int i, k, Level, LevelMax; 00253 assert( p->vRequired == NULL ); 00254 // start the required times 00255 vLevelsR = Vec_IntStart( Ivy_ManObjIdMax(p) + 1 ); 00256 // iterate through the nodes in the reverse order 00257 vNodes = Ivy_ManLevelize( p ); 00258 Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k ) 00259 { 00260 Level = Vec_IntEntry( vLevelsR, pObj->Id ) + 1 + Ivy_ObjIsExor(pObj); 00261 if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId0(pObj) ) < Level ) 00262 Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId0(pObj), Level ); 00263 if ( Vec_IntEntry( vLevelsR, Ivy_ObjFaninId1(pObj) ) < Level ) 00264 Vec_IntWriteEntry( vLevelsR, Ivy_ObjFaninId1(pObj), Level ); 00265 } 00266 Vec_VecFree( vNodes ); 00267 // convert it into the required times 00268 LevelMax = Ivy_ManLevels( p ); 00269 //printf( "max %5d\n",LevelMax ); 00270 Ivy_ManForEachObj( p, pObj, i ) 00271 { 00272 Level = Vec_IntEntry( vLevelsR, pObj->Id ); 00273 Vec_IntWriteEntry( vLevelsR, pObj->Id, LevelMax - Level ); 00274 //printf( "%5d : %5d %5d\n", pObj->Id, Level, LevelMax - Level ); 00275 } 00276 p->vRequired = vLevelsR; 00277 return vLevelsR; 00278 }
| void Ivy_ManResetLevels | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Collect the latches.]
Description []
SideEffects []
SeeAlso []
Definition at line 289 of file ivyUtil.c.
00290 { 00291 Ivy_Obj_t * pObj; 00292 int i; 00293 Ivy_ManForEachObj( p, pObj, i ) 00294 pObj->Level = 0; 00295 Ivy_ManForEachCo( p, pObj, i ) 00296 Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) ); 00297 }
Function*************************************************************
Synopsis [Performs several passes of rewriting on the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 83 of file ivyResyn.c.
00084 { 00085 int clk; 00086 Ivy_Man_t * pTemp; 00087 00088 if ( fVerbose ) { printf( "Original:\n" ); } 00089 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00090 00091 clk = clock(); 00092 pMan = Ivy_ManBalance( pMan, fUpdateLevel ); 00093 if ( fVerbose ) { printf( "\n" ); } 00094 if ( fVerbose ) { PRT( "Balance", clock() - clk ); } 00095 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00096 00097 // Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 ); 00098 clk = clock(); 00099 Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 ); 00100 if ( fVerbose ) { printf( "\n" ); } 00101 if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); } 00102 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00103 00104 clk = clock(); 00105 pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel ); 00106 Ivy_ManStop( pTemp ); 00107 if ( fVerbose ) { printf( "\n" ); } 00108 if ( fVerbose ) { PRT( "Balance", clock() - clk ); } 00109 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00110 00111 // Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 ); 00112 clk = clock(); 00113 Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 ); 00114 if ( fVerbose ) { printf( "\n" ); } 00115 if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); } 00116 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00117 00118 clk = clock(); 00119 pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel ); 00120 Ivy_ManStop( pTemp ); 00121 if ( fVerbose ) { printf( "\n" ); } 00122 if ( fVerbose ) { PRT( "Balance", clock() - clk ); } 00123 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00124 00125 // Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 ); 00126 clk = clock(); 00127 Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 ); 00128 if ( fVerbose ) { printf( "\n" ); } 00129 if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); } 00130 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00131 00132 clk = clock(); 00133 pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel ); 00134 Ivy_ManStop( pTemp ); 00135 if ( fVerbose ) { printf( "\n" ); } 00136 if ( fVerbose ) { PRT( "Balance", clock() - clk ); } 00137 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00138 return pMan; 00139 }
CFile****************************************************************
FileName [ivyResyn.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [AIG rewriting script.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [
- Id
- ivyResyn.c,v 1.00 2006/05/11 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Performs several passes of rewriting on the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file ivyResyn.c.
00043 { 00044 int clk; 00045 Ivy_Man_t * pTemp; 00046 00047 if ( fVerbose ) { printf( "Original:\n" ); } 00048 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00049 00050 clk = clock(); 00051 pMan = Ivy_ManBalance( pMan, fUpdateLevel ); 00052 if ( fVerbose ) { printf( "\n" ); } 00053 if ( fVerbose ) { PRT( "Balance", clock() - clk ); } 00054 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00055 00056 // Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 ); 00057 clk = clock(); 00058 Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 ); 00059 if ( fVerbose ) { printf( "\n" ); } 00060 if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); } 00061 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00062 00063 clk = clock(); 00064 pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel ); 00065 Ivy_ManStop( pTemp ); 00066 if ( fVerbose ) { printf( "\n" ); } 00067 if ( fVerbose ) { PRT( "Balance", clock() - clk ); } 00068 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00069 return pMan; 00070 }
| int Ivy_ManRewriteAlg | ( | Ivy_Man_t * | p, | |
| int | fUpdateLevel, | |||
| int | fUseZeroCost | |||
| ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Algebraic AIG rewriting.]
Description []
SideEffects []
SeeAlso []
Definition at line 46 of file ivyRwrAlg.c.
00047 { 00048 Vec_Int_t * vRequired; 00049 Vec_Ptr_t * vFront, * vLeaves, * vCone, * vSol; 00050 Ivy_Obj_t * pObj, * pResult; 00051 int i, RetValue, LevelR, nNodesOld; 00052 int CountUsed, CountUndo; 00053 vRequired = fUpdateLevel? Ivy_ManRequiredLevels( p ) : NULL; 00054 vFront = Vec_PtrAlloc( 100 ); 00055 vLeaves = Vec_PtrAlloc( 100 ); 00056 vCone = Vec_PtrAlloc( 100 ); 00057 vSol = Vec_PtrAlloc( 100 ); 00058 // go through the nodes in the topological order 00059 CountUsed = CountUndo = 0; 00060 nNodesOld = Ivy_ManObjIdNext(p); 00061 Ivy_ManForEachObj( p, pObj, i ) 00062 { 00063 assert( !Ivy_ObjIsBuf(pObj) ); 00064 if ( i >= nNodesOld ) 00065 break; 00066 // skip no-nodes and MUX roots 00067 if ( !Ivy_ObjIsNode(pObj) || Ivy_ObjIsExor(pObj) || Ivy_ObjIsMuxType(pObj) ) 00068 continue; 00069 // if ( pObj->Id > 297 ) // 296 --- 297 00070 // break; 00071 if ( pObj->Id == 297 ) 00072 { 00073 int x = 0; 00074 } 00075 // get the largest algebraic cut 00076 RetValue = Ivy_ManFindAlgCut( pObj, vFront, vLeaves, vCone ); 00077 // the case of a trivial tree cut 00078 if ( RetValue == 1 ) 00079 continue; 00080 // the case of constant 0 cone 00081 if ( RetValue == -1 ) 00082 { 00083 Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0, 1 ); 00084 continue; 00085 } 00086 assert( Vec_PtrSize(vLeaves) > 2 ); 00087 // get the required level for this node 00088 LevelR = vRequired? Vec_IntEntry(vRequired, pObj->Id) : 1000000; 00089 // create a new cone 00090 pResult = Ivy_NodeRewriteAlg( pObj, vFront, vLeaves, vCone, vSol, LevelR, fUseZeroCost ); 00091 if ( pResult == NULL || pResult == pObj ) 00092 continue; 00093 assert( Vec_PtrSize(vSol) == 1 || !Ivy_IsComplement(pResult) ); 00094 if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 ) 00095 Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++; 00096 else 00097 Ivy_ObjReplace( pObj, pResult, 1, 0, 1 ), CountUsed++; 00098 } 00099 printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo ); 00100 Vec_PtrFree( vFront ); 00101 Vec_PtrFree( vCone ); 00102 Vec_PtrFree( vSol ); 00103 if ( vRequired ) Vec_IntFree( vRequired ); 00104 if ( i = Ivy_ManCleanup(p) ) 00105 printf( "Cleanup after rewriting removed %d dangling nodes.\n", i ); 00106 if ( !Ivy_ManCheck(p) ) 00107 printf( "Ivy_ManRewriteAlg(): The check has failed.\n" ); 00108 return 1; 00109 }
| int Ivy_ManRewritePre | ( | Ivy_Man_t * | p, | |
| int | fUpdateLevel, | |||
| int | fUseZeroCost, | |||
| int | fVerbose | |||
| ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Performs incremental rewriting of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 52 of file ivyRwr.c.
00053 { 00054 Rwt_Man_t * pManRwt; 00055 Ivy_Obj_t * pNode; 00056 int i, nNodes, nGain; 00057 int clk, clkStart = clock(); 00058 // start the rewriting manager 00059 pManRwt = Rwt_ManStart( 0 ); 00060 p->pData = pManRwt; 00061 if ( pManRwt == NULL ) 00062 return 0; 00063 // create fanouts 00064 if ( fUpdateLevel && p->fFanout == 0 ) 00065 Ivy_ManStartFanout( p ); 00066 // compute the reverse levels if level update is requested 00067 if ( fUpdateLevel ) 00068 Ivy_ManRequiredLevels( p ); 00069 // set the number of levels 00070 // p->nLevelMax = Ivy_ManLevels( p ); 00071 // resynthesize each node once 00072 nNodes = Ivy_ManObjIdMax(p); 00073 Ivy_ManForEachNode( p, pNode, i ) 00074 { 00075 // fix the fanin buffer problem 00076 Ivy_NodeFixBufferFanins( p, pNode, 1 ); 00077 if ( Ivy_ObjIsBuf(pNode) ) 00078 continue; 00079 // stop if all nodes have been tried once 00080 if ( i > nNodes ) 00081 break; 00082 // for each cut, try to resynthesize it 00083 nGain = Ivy_NodeRewrite( p, pManRwt, pNode, fUpdateLevel, fUseZeroCost ); 00084 if ( nGain > 0 || nGain == 0 && fUseZeroCost ) 00085 { 00086 Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt); 00087 int fCompl = Rwt_ManReadCompl(pManRwt); 00088 /* 00089 { 00090 Ivy_Obj_t * pObj; 00091 int i; 00092 printf( "USING: (" ); 00093 Vec_PtrForEachEntry( Rwt_ManReadLeaves(pManRwt), pObj, i ) 00094 printf( "%d ", Ivy_ObjFanoutNum(Ivy_Regular(pObj)) ); 00095 printf( ") Gain = %d.\n", nGain ); 00096 } 00097 if ( nGain > 0 ) 00098 { // print stats on the MFFC 00099 extern void Ivy_NodeMffsConeSuppPrint( Ivy_Obj_t * pNode ); 00100 printf( "Node %6d : Gain = %4d ", pNode->Id, nGain ); 00101 Ivy_NodeMffsConeSuppPrint( pNode ); 00102 } 00103 */ 00104 // complement the FF if needed 00105 clk = clock(); 00106 if ( fCompl ) Dec_GraphComplement( pGraph ); 00107 Ivy_GraphUpdateNetwork( p, pNode, pGraph, fUpdateLevel, nGain ); 00108 if ( fCompl ) Dec_GraphComplement( pGraph ); 00109 Rwt_ManAddTimeUpdate( pManRwt, clock() - clk ); 00110 } 00111 } 00112 Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart ); 00113 // print stats 00114 if ( fVerbose ) 00115 Rwt_ManPrintStats( pManRwt ); 00116 // delete the managers 00117 Rwt_ManStop( pManRwt ); 00118 p->pData = NULL; 00119 // fix the levels 00120 if ( fUpdateLevel ) 00121 Vec_IntFree( p->vRequired ), p->vRequired = NULL; 00122 else 00123 Ivy_ManResetLevels( p ); 00124 // check 00125 if ( i = Ivy_ManCleanup(p) ) 00126 printf( "Cleanup after rewriting removed %d dangling nodes.\n", i ); 00127 if ( !Ivy_ManCheck(p) ) 00128 printf( "Ivy_ManRewritePre(): The check has failed.\n" ); 00129 return 1; 00130 }
| int Ivy_ManRewriteSeq | ( | Ivy_Man_t * | p, | |
| int | fUseZeroCost, | |||
| int | fVerbose | |||
| ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Performs incremental rewriting of the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 60 of file ivySeq.c.
00061 { 00062 Rwt_Man_t * pManRwt; 00063 Ivy_Obj_t * pNode; 00064 int i, nNodes, nGain; 00065 int clk, clkStart = clock(); 00066 00067 // set the DC latch values 00068 Ivy_ManForEachLatch( p, pNode, i ) 00069 pNode->Init = IVY_INIT_DC; 00070 // start the rewriting manager 00071 pManRwt = Rwt_ManStart( 0 ); 00072 p->pData = pManRwt; 00073 if ( pManRwt == NULL ) 00074 return 0; 00075 // create fanouts 00076 if ( p->fFanout == 0 ) 00077 Ivy_ManStartFanout( p ); 00078 // resynthesize each node once 00079 nNodes = Ivy_ManObjIdMax(p); 00080 Ivy_ManForEachNode( p, pNode, i ) 00081 { 00082 assert( !Ivy_ObjIsBuf(pNode) ); 00083 assert( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) ); 00084 assert( !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) ); 00085 // fix the fanin buffer problem 00086 // Ivy_NodeFixBufferFanins( p, pNode ); 00087 // if ( Ivy_ObjIsBuf(pNode) ) 00088 // continue; 00089 // stop if all nodes have been tried once 00090 if ( i > nNodes ) 00091 break; 00092 // for each cut, try to resynthesize it 00093 nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost ); 00094 if ( nGain > 0 || nGain == 0 && fUseZeroCost ) 00095 { 00096 Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt); 00097 int fCompl = Rwt_ManReadCompl(pManRwt); 00098 // complement the FF if needed 00099 clk = clock(); 00100 if ( fCompl ) Dec_GraphComplement( pGraph ); 00101 Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain ); 00102 if ( fCompl ) Dec_GraphComplement( pGraph ); 00103 Rwt_ManAddTimeUpdate( pManRwt, clock() - clk ); 00104 } 00105 } 00106 Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart ); 00107 // print stats 00108 if ( fVerbose ) 00109 Rwt_ManPrintStats( pManRwt ); 00110 // delete the managers 00111 Rwt_ManStop( pManRwt ); 00112 p->pData = NULL; 00113 // fix the levels 00114 Ivy_ManResetLevels( p ); 00115 // if ( Ivy_ManCheckFanoutNums(p) ) 00116 // printf( "Ivy_ManRewritePre(): The check has failed.\n" ); 00117 // check 00118 if ( !Ivy_ManCheck(p) ) 00119 printf( "Ivy_ManRewritePre(): The check has failed.\n" ); 00120 return 1; 00121 }
Function*************************************************************
Synopsis [Performs several passes of rewriting on the AIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 152 of file ivyResyn.c.
00153 { 00154 int clk; 00155 Ivy_Man_t * pTemp; 00156 00157 if ( fVerbose ) { printf( "Original:\n" ); } 00158 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00159 00160 clk = clock(); 00161 Ivy_ManRewritePre( pMan, 0, 0, 0 ); 00162 if ( fVerbose ) { printf( "\n" ); } 00163 if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); } 00164 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00165 00166 clk = clock(); 00167 pMan = Ivy_ManBalance( pTemp = pMan, 0 ); 00168 // pMan = Ivy_ManDup( pTemp = pMan ); 00169 Ivy_ManStop( pTemp ); 00170 if ( fVerbose ) { printf( "\n" ); } 00171 if ( fVerbose ) { PRT( "Balance", clock() - clk ); } 00172 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00173 00174 /* 00175 clk = clock(); 00176 Ivy_ManRewritePre( pMan, 0, 0, 0 ); 00177 if ( fVerbose ) { printf( "\n" ); } 00178 if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); } 00179 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00180 00181 clk = clock(); 00182 pMan = Ivy_ManBalance( pTemp = pMan, 0 ); 00183 Ivy_ManStop( pTemp ); 00184 if ( fVerbose ) { printf( "\n" ); } 00185 if ( fVerbose ) { PRT( "Balance", clock() - clk ); } 00186 if ( fVerbose ) Ivy_ManPrintStats( pMan ); 00187 */ 00188 return pMan; 00189 }
| void Ivy_ManSeqFindCut | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t * | pRoot, | |||
| Vec_Int_t * | vFront, | |||
| Vec_Int_t * | vInside, | |||
| int | nSize | |||
| ) |
Function*************************************************************
Synopsis [Computes one sequential cut of the given size.]
Description []
SideEffects []
SeeAlso []
Definition at line 180 of file ivyCut.c.
00181 { 00182 assert( !Ivy_IsComplement(pRoot) ); 00183 assert( Ivy_ObjIsNode(pRoot) ); 00184 assert( Ivy_ObjFaninId0(pRoot) ); 00185 assert( Ivy_ObjFaninId1(pRoot) ); 00186 00187 // start the cut 00188 Vec_IntClear( vFront ); 00189 Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) ); 00190 Vec_IntPush( vFront, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) ); 00191 00192 // start the visited nodes 00193 Vec_IntClear( vInside ); 00194 Vec_IntPush( vInside, Ivy_LeafCreate(pRoot->Id, 0) ); 00195 Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId0(pRoot), 0) ); 00196 Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) ); 00197 00198 // compute the cut 00199 while ( Ivy_ManSeqFindCut_int( p, vFront, vInside, nSize ) ); 00200 assert( Vec_IntSize(vFront) <= nSize ); 00201 }
| int Ivy_ManSeqRewrite | ( | Ivy_Man_t * | p, | |
| int | fUpdateLevel, | |||
| int | fUseZeroCost | |||
| ) |
| int Ivy_ManSetLevels | ( | Ivy_Man_t * | p, | |
| int | fHaig | |||
| ) |
Function*************************************************************
Synopsis [Sets the levels of the nodes.]
Description []
SideEffects []
SeeAlso []
Definition at line 454 of file ivyDfs.c.
00455 { 00456 Ivy_Obj_t * pObj; 00457 int i, LevelMax; 00458 // check if CIs have choices 00459 if ( fHaig ) 00460 { 00461 Ivy_ManForEachCi( p, pObj, i ) 00462 if ( pObj->pEquiv ) 00463 printf( "CI %d has a choice, which will not be visualized.\n", pObj->Id ); 00464 } 00465 // clean the levels 00466 Ivy_ManForEachObj( p, pObj, i ) 00467 pObj->Level = 0; 00468 // compute the levels 00469 LevelMax = 0; 00470 Ivy_ManForEachCo( p, pObj, i ) 00471 { 00472 Ivy_ManSetLevels_rec( Ivy_ObjFanin0(pObj), fHaig ); 00473 LevelMax = IVY_MAX( LevelMax, (int)Ivy_ObjFanin0(pObj)->Level ); 00474 } 00475 // compute levels of nodes without fanout 00476 Ivy_ManForEachObj( p, pObj, i ) 00477 if ( (Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj)) && Ivy_ObjRefs(pObj) == 0 ) 00478 { 00479 Ivy_ManSetLevels_rec( pObj, fHaig ); 00480 LevelMax = IVY_MAX( LevelMax, (int)pObj->Level ); 00481 } 00482 // clean the marks 00483 Ivy_ManForEachObj( p, pObj, i ) 00484 Ivy_ObjClearMarkA(pObj); 00485 return LevelMax; 00486 }
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 44 of file ivyShow.c.
00045 { 00046 extern void Abc_ShowFile( char * FileNameDot ); 00047 static Counter = 0; 00048 char FileNameDot[200]; 00049 FILE * pFile; 00050 // create the file name 00051 // Ivy_ShowGetFileName( pMan->pName, FileNameDot ); 00052 sprintf( FileNameDot, "temp%02d.dot", Counter++ ); 00053 // check that the file can be opened 00054 if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) 00055 { 00056 fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot ); 00057 return; 00058 } 00059 fclose( pFile ); 00060 // generate the file 00061 Ivy_WriteDotAig( pMan, FileNameDot, fHaig, vBold ); 00062 // visualize the file 00063 Abc_ShowFile( FileNameDot ); 00064 }
| Ivy_Man_t* Ivy_ManStart | ( | ) |
CFile****************************************************************
FileName [ivyMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [AIG manager.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [
- Id
- ivy_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Starts the AIG manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file ivyMan.c.
00043 { 00044 Ivy_Man_t * p; 00045 // start the manager 00046 p = ALLOC( Ivy_Man_t, 1 ); 00047 memset( p, 0, sizeof(Ivy_Man_t) ); 00048 // perform initializations 00049 p->Ghost.Id = -1; 00050 p->nTravIds = 1; 00051 p->fCatchExor = 1; 00052 // allocate arrays for nodes 00053 p->vPis = Vec_PtrAlloc( 100 ); 00054 p->vPos = Vec_PtrAlloc( 100 ); 00055 p->vBufs = Vec_PtrAlloc( 100 ); 00056 p->vObjs = Vec_PtrAlloc( 100 ); 00057 // prepare the internal memory manager 00058 Ivy_ManStartMemory( p ); 00059 // create the constant node 00060 p->pConst1 = Ivy_ManFetchMemory( p ); 00061 p->pConst1->fPhase = 1; 00062 Vec_PtrPush( p->vObjs, p->pConst1 ); 00063 p->nCreated = 1; 00064 // start the table 00065 p->nTableSize = 10007; 00066 p->pTable = ALLOC( int, p->nTableSize ); 00067 memset( p->pTable, 0, sizeof(int) * p->nTableSize ); 00068 return p; 00069 }
| void Ivy_ManStartFanout | ( | Ivy_Man_t * | p | ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Starts the fanout representation.]
Description []
SideEffects []
SeeAlso []
Definition at line 133 of file ivyFanout.c.
00134 { 00135 Ivy_Obj_t * pObj; 00136 int i; 00137 assert( !p->fFanout ); 00138 p->fFanout = 1; 00139 Ivy_ManForEachObj( p, pObj, i ) 00140 { 00141 if ( Ivy_ObjFanin0(pObj) ) 00142 Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj ); 00143 if ( Ivy_ObjFanin1(pObj) ) 00144 Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj ); 00145 } 00146 }
Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 82 of file ivyMan.c.
00083 { 00084 Ivy_Man_t * pNew; 00085 Ivy_Obj_t * pObj; 00086 int i; 00087 // create the new manager 00088 pNew = Ivy_ManStart(); 00089 // create the PIs 00090 Ivy_ManConst1(p)->pEquiv = Ivy_ManConst1(pNew); 00091 Ivy_ManForEachPi( p, pObj, i ) 00092 pObj->pEquiv = Ivy_ObjCreatePi(pNew); 00093 return pNew; 00094 }
| void Ivy_ManStartMemory | ( | Ivy_Man_t * | p | ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Starts the internal memory manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 46 of file ivyMem.c.
00047 { 00048 p->vChunks = Vec_PtrAlloc( 128 ); 00049 p->vPages = Vec_PtrAlloc( 128 ); 00050 }
| void Ivy_ManStop | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Stops the AIG manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 235 of file ivyMan.c.
00236 { 00237 if ( p->time1 ) { PRT( "Update lev ", p->time1 ); } 00238 if ( p->time2 ) { PRT( "Update levR ", p->time2 ); } 00239 // Ivy_TableProfile( p ); 00240 // if ( p->vFanouts ) Ivy_ManStopFanout( p ); 00241 if ( p->vChunks ) Ivy_ManStopMemory( p ); 00242 if ( p->vRequired ) Vec_IntFree( p->vRequired ); 00243 if ( p->vPis ) Vec_PtrFree( p->vPis ); 00244 if ( p->vPos ) Vec_PtrFree( p->vPos ); 00245 if ( p->vBufs ) Vec_PtrFree( p->vBufs ); 00246 if ( p->vObjs ) Vec_PtrFree( p->vObjs ); 00247 free( p->pTable ); 00248 free( p ); 00249 }
| void Ivy_ManStopFanout | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Stops the fanout representation.]
Description []
SideEffects []
SeeAlso []
Definition at line 159 of file ivyFanout.c.
| void Ivy_ManStopMemory | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Stops the internal memory manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 63 of file ivyMem.c.
00064 { 00065 void * pMemory; 00066 int i; 00067 Vec_PtrForEachEntry( p->vChunks, pMemory, i ) 00068 free( pMemory ); 00069 Vec_PtrFree( p->vChunks ); 00070 Vec_PtrFree( p->vPages ); 00071 p->pListFree = NULL; 00072 }
Function*************************************************************
Synopsis [Implements the miter.]
Description []
SideEffects []
SeeAlso []
Definition at line 261 of file ivyOper.c.
00262 { 00263 int i; 00264 assert( vPairs->nSize > 0 ); 00265 assert( vPairs->nSize % 2 == 0 ); 00266 // go through the cubes of the node's SOP 00267 for ( i = 0; i < vPairs->nSize; i += 2 ) 00268 vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) ); 00269 vPairs->nSize = vPairs->nSize/2; 00270 return Ivy_Not( Ivy_Multi_rec( p, (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) ); 00271 }
| Ivy_Obj_t* Ivy_Multi | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t ** | pArgs, | |||
| int | nArgs, | |||
| Ivy_Type_t | Type | |||
| ) |
Function*************************************************************
Synopsis [Old code.]
Description []
SideEffects []
SeeAlso []
Definition at line 243 of file ivyOper.c.
00244 { 00245 assert( Type == IVY_AND || Type == IVY_EXOR ); 00246 assert( nArgs > 0 ); 00247 return Ivy_Multi_rec( p, pArgs, nArgs, Type ); 00248 }
| Ivy_Obj_t* Ivy_Multi1 | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t ** | pArgs, | |||
| int | nArgs, | |||
| Ivy_Type_t | Type | |||
| ) |
| Ivy_Obj_t* Ivy_Multi_rec | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t ** | ppObjs, | |||
| int | nObjs, | |||
| Ivy_Type_t | Type | |||
| ) |
Function*************************************************************
Synopsis [Constructs the well-balanced tree of gates.]
Description [Disregards levels and possible logic sharing.]
SideEffects []
SeeAlso []
Definition at line 222 of file ivyOper.c.
00223 { 00224 Ivy_Obj_t * pObj1, * pObj2; 00225 if ( nObjs == 1 ) 00226 return ppObjs[0]; 00227 pObj1 = Ivy_Multi_rec( p, ppObjs, nObjs/2, Type ); 00228 pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type ); 00229 return Ivy_Oper( p, pObj1, pObj2, Type ); 00230 }
| Ivy_Obj_t* Ivy_MultiBalance_rec | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t ** | pArgs, | |||
| int | nArgs, | |||
| Ivy_Type_t | Type | |||
| ) |
| int Ivy_MultiPlus | ( | Ivy_Man_t * | p, | |
| Vec_Ptr_t * | vLeaves, | |||
| Vec_Ptr_t * | vCone, | |||
| Ivy_Type_t | Type, | |||
| int | nLimit, | |||
| Vec_Ptr_t * | vSols | |||
| ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Constructs a balanced tree while taking sharing into account.]
Description [Returns 1 if the implementation exists.]
SideEffects []
SeeAlso []
Definition at line 55 of file ivyMulti.c.
00056 { 00057 static Ivy_Eva_t pEvals[IVY_EVAL_LIMIT]; 00058 Ivy_Eva_t * pEval, * pFan0, * pFan1; 00059 Ivy_Obj_t * pObj, * pTemp; 00060 int nEvals, nEvalsOld, i, k, x, nLeaves; 00061 unsigned uMaskAll; 00062 00063 // consider special cases 00064 nLeaves = Vec_PtrSize(vLeaves); 00065 assert( nLeaves > 2 ); 00066 if ( nLeaves > 32 || nLeaves + Vec_PtrSize(vCone) > IVY_EVAL_LIMIT ) 00067 return 0; 00068 // if ( nLeaves == 1 ) 00069 // return Vec_PtrEntry( vLeaves, 0 ); 00070 // if ( nLeaves == 2 ) 00071 // return Ivy_Oper( Vec_PtrEntry(vLeaves, 0), Vec_PtrEntry(vLeaves, 1), Type ); 00072 00073 // set the leaf entries 00074 uMaskAll = ((1 << nLeaves) - 1); 00075 nEvals = 0; 00076 Vec_PtrForEachEntry( vLeaves, pObj, i ) 00077 { 00078 pEval = pEvals + nEvals; 00079 pEval->pArg = pObj; 00080 pEval->Mask = (1 << nEvals); 00081 pEval->Weight = 1; 00082 // mark the leaf 00083 Ivy_Regular(pObj)->TravId = nEvals; 00084 nEvals++; 00085 } 00086 00087 // propagate masks through the cone 00088 Vec_PtrForEachEntry( vCone, pObj, i ) 00089 { 00090 pObj->TravId = nEvals + i; 00091 if ( Ivy_ObjIsBuf(pObj) ) 00092 pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask; 00093 else 00094 pEvals[pObj->TravId].Mask = pEvals[Ivy_ObjFanin0(pObj)->TravId].Mask | pEvals[Ivy_ObjFanin1(pObj)->TravId].Mask; 00095 } 00096 00097 // set the internal entries 00098 Vec_PtrForEachEntry( vCone, pObj, i ) 00099 { 00100 if ( i == Vec_PtrSize(vCone) - 1 ) 00101 break; 00102 // skip buffers 00103 if ( Ivy_ObjIsBuf(pObj) ) 00104 continue; 00105 // skip nodes without external fanout 00106 if ( Ivy_ObjRefs(pObj) == 0 ) 00107 continue; 00108 assert( !Ivy_IsComplement(pObj) ); 00109 pEval = pEvals + nEvals; 00110 pEval->pArg = pObj; 00111 pEval->Mask = pEvals[pObj->TravId].Mask; 00112 pEval->Weight = Extra_WordCountOnes(pEval->Mask); 00113 // mark the node 00114 pObj->TravId = nEvals; 00115 nEvals++; 00116 } 00117 00118 // find the available nodes 00119 nEvalsOld = nEvals; 00120 for ( i = 1; i < nEvals; i++ ) 00121 for ( k = 0; k < i; k++ ) 00122 { 00123 pFan0 = pEvals + i; 00124 pFan1 = pEvals + k; 00125 pTemp = Ivy_TableLookup(p, Ivy_ObjCreateGhost(p, pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE)); 00126 // skip nodes in the cone 00127 if ( pTemp == NULL || pTemp->fMarkB ) 00128 continue; 00129 // skip the leaves 00130 for ( x = 0; x < nLeaves; x++ ) 00131 if ( pTemp == Ivy_Regular(vLeaves->pArray[x]) ) 00132 break; 00133 if ( x < nLeaves ) 00134 continue; 00135 pEval = pEvals + nEvals; 00136 pEval->pArg = pTemp; 00137 pEval->Mask = pFan0->Mask | pFan1->Mask; 00138 pEval->Weight = (pFan0->Mask & pFan1->Mask) ? Extra_WordCountOnes(pEval->Mask) : pFan0->Weight + pFan1->Weight; 00139 // save the argument 00140 pObj->TravId = nEvals; 00141 nEvals++; 00142 // quit if the number of entries exceeded the limit 00143 if ( nEvals == IVY_EVAL_LIMIT ) 00144 goto Outside; 00145 // quit if we found an acceptable implementation 00146 if ( pEval->Mask == uMaskAll ) 00147 goto Outside; 00148 } 00149 Outside: 00150 00151 // Ivy_MultiPrint( pEvals, nLeaves, nEvals ); 00152 if ( !Ivy_MultiCover( p, pEvals, nLeaves, nEvals, nLimit, vSols ) ) 00153 return 0; 00154 assert( Vec_PtrSize( vSols ) > 0 ); 00155 return 1; 00156 }
Function*************************************************************
Synopsis [Implements ITE operation.]
Description []
SideEffects []
SeeAlso []
Definition at line 155 of file ivyOper.c.
00156 { 00157 Ivy_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp; 00158 int Count0, Count1; 00159 // consider trivial cases 00160 if ( p0 == Ivy_Not(p1) ) 00161 return Ivy_Exor( p, pC, p0 ); 00162 // other cases can be added 00163 // implement the first MUX (F = C * x1 + C' * x0) 00164 pTempA1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pC, p1, IVY_AND, IVY_INIT_NONE) ); 00165 pTempA2 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) ); 00166 if ( pTempA1 && pTempA2 ) 00167 { 00168 pTemp = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) ); 00169 if ( pTemp ) return Ivy_Not(pTemp); 00170 } 00171 Count0 = (pTempA1 != NULL) + (pTempA2 != NULL); 00172 // implement the second MUX (F' = C * x1' + C' * x0') 00173 pTempB1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pC, Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) ); 00174 pTempB2 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) ); 00175 if ( pTempB1 && pTempB2 ) 00176 { 00177 pTemp = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) ); 00178 if ( pTemp ) return pTemp; 00179 } 00180 Count1 = (pTempB1 != NULL) + (pTempB2 != NULL); 00181 // compare and decide which one to implement 00182 if ( Count0 >= Count1 ) 00183 { 00184 pTempA1 = pTempA1? pTempA1 : Ivy_And(p, pC, p1); 00185 pTempA2 = pTempA2? pTempA2 : Ivy_And(p, Ivy_Not(pC), p0); 00186 return Ivy_Or( p, pTempA1, pTempA2 ); 00187 } 00188 pTempB1 = pTempB1? pTempB1 : Ivy_And(p, pC, Ivy_Not(p1)); 00189 pTempB2 = pTempB2? pTempB2 : Ivy_And(p, Ivy_Not(pC), Ivy_Not(p0)); 00190 return Ivy_Not( Ivy_Or( p, pTempB1, pTempB2 ) ); 00191 00192 // return Ivy_Or( Ivy_And(pC, p1), Ivy_And(Ivy_Not(pC), p0) ); 00193 }
| Ivy_Obj_t* Ivy_NodeBalanceBuildSuper | ( | Ivy_Man_t * | p, | |
| Vec_Ptr_t * | vSuper, | |||
| Ivy_Type_t | Type, | |||
| int | fUpdateLevel | |||
| ) |
Function*************************************************************
Synopsis [Builds implication supergate.]
Description []
SideEffects []
SeeAlso []
Definition at line 167 of file ivyBalance.c.
00168 { 00169 Ivy_Obj_t * pObj1, * pObj2; 00170 int LeftBound; 00171 assert( vSuper->nSize > 1 ); 00172 // sort the new nodes by level in the decreasing order 00173 Vec_PtrSort( vSuper, Ivy_NodeCompareLevelsDecrease ); 00174 // balance the nodes 00175 while ( vSuper->nSize > 1 ) 00176 { 00177 // find the left bound on the node to be paired 00178 LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper ); 00179 // find the node that can be shared (if no such node, randomize choice) 00180 Ivy_NodeBalancePermute( p, vSuper, LeftBound, Type == IVY_EXOR ); 00181 // pull out the last two nodes 00182 pObj1 = Vec_PtrPop(vSuper); 00183 pObj2 = Vec_PtrPop(vSuper); 00184 Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(p, pObj1, pObj2, Type) ); 00185 } 00186 return Vec_PtrEntry(vSuper, 0); 00187 }
| Ivy_Store_t* Ivy_NodeFindCutsAll | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t * | pObj, | |||
| int | nLeaves | |||
| ) |
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 888 of file ivyCut.c.
00889 { 00890 static Ivy_Store_t CutStore, * pCutStore = &CutStore; 00891 Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut; 00892 Ivy_Obj_t * pLeaf; 00893 int i, k, iLeaf0, iLeaf1; 00894 00895 assert( nLeaves <= IVY_CUT_INPUT ); 00896 00897 // start the structure 00898 pCutStore->nCuts = 0; 00899 pCutStore->nCutsMax = IVY_CUT_LIMIT; 00900 // start the trivial cut 00901 pCutNew->uHash = 0; 00902 pCutNew->nSize = 1; 00903 pCutNew->nSizeMax = nLeaves; 00904 pCutNew->pArray[0] = pObj->Id; 00905 Ivy_NodeCutHash( pCutNew ); 00906 // add the trivial cut 00907 Ivy_NodeCutFindOrAdd( pCutStore, pCutNew ); 00908 assert( pCutStore->nCuts == 1 ); 00909 00910 // explore the cuts 00911 for ( i = 0; i < pCutStore->nCuts; i++ ) 00912 { 00913 // expand this cut 00914 pCut = pCutStore->pCuts + i; 00915 if ( pCut->nSize == 0 ) 00916 continue; 00917 for ( k = 0; k < pCut->nSize; k++ ) 00918 { 00919 pLeaf = Ivy_ManObj( p, pCut->pArray[k] ); 00920 if ( Ivy_ObjIsCi(pLeaf) ) 00921 continue; 00922 /* 00923 *pCutNew = *pCut; 00924 Ivy_NodeCutShrink( pCutNew, pLeaf->Id ); 00925 if ( !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId0(pLeaf) ) ) 00926 continue; 00927 if ( Ivy_ObjIsNode(pLeaf) && !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId1(pLeaf) ) ) 00928 continue; 00929 Ivy_NodeCutHash( pCutNew ); 00930 */ 00931 iLeaf0 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin0(pLeaf)) ); 00932 iLeaf1 = Ivy_ObjId( Ivy_ObjRealFanin(Ivy_ObjFanin1(pLeaf)) ); 00933 // if ( iLeaf0 == iLeaf1 ) // strange situation observed on Jan 18, 2007 00934 // continue; 00935 if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) ) 00936 continue; 00937 if ( iLeaf0 > iLeaf1 ) 00938 Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf1, iLeaf0 ); 00939 else 00940 Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 ); 00941 Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew ); 00942 if ( pCutStore->nCuts == IVY_CUT_LIMIT ) 00943 break; 00944 } 00945 if ( pCutStore->nCuts == IVY_CUT_LIMIT ) 00946 break; 00947 } 00948 Ivy_NodeCompactCuts( pCutStore ); 00949 // Ivy_NodePrintCuts( pCutStore ); 00950 return pCutStore; 00951 }
Function*************************************************************
Synopsis [Fixes buffer fanins.]
Description [This situation happens because NodeReplace is a lazy procedure, which does not propagate the change to the fanouts but instead records the change in the form of a buf/inv node.]
SideEffects []
SeeAlso []
Definition at line 439 of file ivyObj.c.
00440 { 00441 Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult; 00442 if ( Ivy_ObjIsPo(pNode) ) 00443 { 00444 if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) ) 00445 return; 00446 pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) ); 00447 Ivy_ObjPatchFanin0( p, pNode, pFanReal0 ); 00448 // Ivy_ManCheckFanouts( p ); 00449 return; 00450 } 00451 if ( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) && !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) ) 00452 return; 00453 // get the real fanins 00454 pFanReal0 = Ivy_ObjReal( Ivy_ObjChild0(pNode) ); 00455 pFanReal1 = Ivy_ObjReal( Ivy_ObjChild1(pNode) ); 00456 // get the new node 00457 if ( Ivy_ObjIsNode(pNode) ) 00458 pResult = Ivy_Oper( p, pFanReal0, pFanReal1, Ivy_ObjType(pNode) ); 00459 else if ( Ivy_ObjIsLatch(pNode) ) 00460 pResult = Ivy_Latch( p, pFanReal0, Ivy_ObjInit(pNode) ); 00461 else 00462 assert( 0 ); 00463 00464 //printf( "===== Replacing %d by %d.\n", pNode->Id, pResult->Id ); 00465 //Ivy_ObjPrintVerbose( p, pNode, 0 ); printf( "\n" ); 00466 //Ivy_ObjPrintVerbose( p, pResult, 0 ); printf( "\n" ); 00467 00468 // perform the replacement 00469 Ivy_ObjReplace( p, pNode, pResult, 1, 0, fUpdateLevel ); 00470 }
Function*************************************************************
Synopsis [Add the fanout.]
Description []
SideEffects []
SeeAlso []
Definition at line 180 of file ivyFanout.c.
00181 { 00182 assert( p->fFanout ); 00183 if ( pFanin->pFanout ) 00184 { 00185 *Ivy_ObjNextFanoutPlace(pFanin, pFanout) = pFanin->pFanout; 00186 *Ivy_ObjPrevFanoutPlace(pFanin, pFanin->pFanout) = pFanout; 00187 } 00188 pFanin->pFanout = pFanout; 00189 }
Definition at line 271 of file ivy.h.
00271 { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin0(pObj)? Ivy_NotCond(Ivy_ObjFanin0(pObj)->pEquiv, Ivy_ObjFaninC0(pObj)) : NULL; }
Definition at line 272 of file ivy.h.
00272 { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL; }
| static void Ivy_ObjClean | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static void Ivy_ObjClearMarkA | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Function*************************************************************
Synopsis [Starts iteration through the fanouts.]
Description [Copies the currently available fanouts into the array.]
SideEffects [Can be used while the fanouts are being removed.]
SeeAlso []
Definition at line 259 of file ivyFanout.c.
00260 { 00261 Ivy_Obj_t * pFanout; 00262 assert( p->fFanout ); 00263 assert( !Ivy_IsComplement(pObj) ); 00264 Vec_PtrClear( vArray ); 00265 Ivy_ObjForEachFanoutInt( pObj, pFanout ) 00266 Vec_PtrPush( vArray, pFanout ); 00267 }
Function*************************************************************
Synopsis [Connect the object to the fanin.]
Description []
SideEffects []
SeeAlso []
Definition at line 147 of file ivyObj.c.
00148 { 00149 assert( !Ivy_IsComplement(pObj) ); 00150 assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || pFan1 != NULL ); 00151 // add the first fanin 00152 pObj->pFanin0 = pFan0; 00153 pObj->pFanin1 = pFan1; 00154 // increment references of the fanins and add their fanouts 00155 if ( Ivy_ObjFanin0(pObj) != NULL ) 00156 { 00157 Ivy_ObjRefsInc( Ivy_ObjFanin0(pObj) ); 00158 if ( p->fFanout ) 00159 Ivy_ObjAddFanout( p, Ivy_ObjFanin0(pObj), pObj ); 00160 } 00161 if ( Ivy_ObjFanin1(pObj) != NULL ) 00162 { 00163 Ivy_ObjRefsInc( Ivy_ObjFanin1(pObj) ); 00164 if ( p->fFanout ) 00165 Ivy_ObjAddFanout( p, Ivy_ObjFanin1(pObj), pObj ); 00166 } 00167 // add the node to the structural hash table 00168 Ivy_TableInsert( p, pObj ); 00169 }
Function*************************************************************
Synopsis [Create the new node assuming it does not exist.]
Description []
SideEffects []
SeeAlso []
Definition at line 74 of file ivyObj.c.
00075 { 00076 Ivy_Obj_t * pObj; 00077 assert( !Ivy_IsComplement(pGhost) ); 00078 assert( Ivy_ObjIsGhost(pGhost) ); 00079 assert( Ivy_TableLookup(p, pGhost) == NULL ); 00080 // get memory for the new object 00081 pObj = Ivy_ManFetchMemory( p ); 00082 assert( Ivy_ObjIsNone(pObj) ); 00083 pObj->Id = Vec_PtrSize(p->vObjs); 00084 Vec_PtrPush( p->vObjs, pObj ); 00085 // add basic info (fanins, compls, type, init) 00086 pObj->Type = pGhost->Type; 00087 pObj->Init = pGhost->Init; 00088 // add connections 00089 Ivy_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 ); 00090 // compute level 00091 if ( Ivy_ObjIsNode(pObj) ) 00092 pObj->Level = Ivy_ObjLevelNew(pObj); 00093 else if ( Ivy_ObjIsLatch(pObj) ) 00094 pObj->Level = 0; 00095 else if ( Ivy_ObjIsOneFanin(pObj) ) 00096 pObj->Level = Ivy_ObjFanin0(pObj)->Level; 00097 else if ( !Ivy_ObjIsPi(pObj) ) 00098 assert( 0 ); 00099 // create phase 00100 if ( Ivy_ObjIsNode(pObj) ) 00101 pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) & Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj)); 00102 else if ( Ivy_ObjIsOneFanin(pObj) ) 00103 pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)); 00104 // set the fail TFO flag 00105 if ( Ivy_ObjIsNode(pObj) ) 00106 pObj->fFailTfo = Ivy_ObjFanin0(pObj)->fFailTfo | Ivy_ObjFanin1(pObj)->fFailTfo; 00107 // mark the fanins in a special way if the node is EXOR 00108 if ( Ivy_ObjIsExor(pObj) ) 00109 { 00110 Ivy_ObjFanin0(pObj)->fExFan = 1; 00111 Ivy_ObjFanin1(pObj)->fExFan = 1; 00112 } 00113 // add PIs/POs to the arrays 00114 if ( Ivy_ObjIsPi(pObj) ) 00115 Vec_PtrPush( p->vPis, pObj ); 00116 else if ( Ivy_ObjIsPo(pObj) ) 00117 Vec_PtrPush( p->vPos, pObj ); 00118 // else if ( Ivy_ObjIsBuf(pObj) ) 00119 // Vec_PtrPush( p->vBufs, pObj ); 00120 if ( p->vRequired && Vec_IntSize(p->vRequired) <= pObj->Id ) 00121 Vec_IntFillExtra( p->vRequired, 2 * Vec_IntSize(p->vRequired), 1000000 ); 00122 // update node counters of the manager 00123 p->nObjs[Ivy_ObjType(pObj)]++; 00124 p->nCreated++; 00125 00126 // printf( "Adding %sAIG node: ", p->pHaig==NULL? "H":" " ); 00127 // Ivy_ObjPrintVerbose( p, pObj, p->pHaig==NULL ); 00128 // printf( "\n" ); 00129 00130 // if HAIG is defined, create a corresponding node 00131 if ( p->pHaig ) 00132 Ivy_ManHaigCreateObj( p, pObj ); 00133 return pObj; 00134 }
| static Ivy_Obj_t* Ivy_ObjCreateGhost | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t * | p0, | |||
| Ivy_Obj_t * | p1, | |||
| Ivy_Type_t | Type, | |||
| Ivy_Init_t | Init | |||
| ) | [inline, static] |
Definition at line 304 of file ivy.h.
00305 { 00306 Ivy_Obj_t * pGhost, * pTemp; 00307 assert( Type != IVY_AND || !Ivy_ObjIsConst1(Ivy_Regular(p0)) ); 00308 assert( p1 == NULL || !Ivy_ObjIsConst1(Ivy_Regular(p1)) ); 00309 assert( Type == IVY_PI || Ivy_Regular(p0) != Ivy_Regular(p1) ); 00310 assert( Type != IVY_LATCH || !Ivy_IsComplement(p0) ); 00311 // assert( p1 == NULL || (!Ivy_ObjIsLatch(Ivy_Regular(p0)) || !Ivy_ObjIsLatch(Ivy_Regular(p1))) ); 00312 pGhost = Ivy_ManGhost(p); 00313 pGhost->Type = Type; 00314 pGhost->Init = Init; 00315 pGhost->pFanin0 = p0; 00316 pGhost->pFanin1 = p1; 00317 if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) ) 00318 pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp; 00319 return pGhost; 00320 }
CFile****************************************************************
FileName [ivyObj.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis [Adding/removing objects.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 11, 2006.]
Revision [
- Id
- ivyObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Create the new node assuming it does not exist.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file ivyObj.c.
00043 { 00044 return Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, NULL, NULL, IVY_PI, IVY_INIT_NONE) ); 00045 }
Function*************************************************************
Synopsis [Create the new node assuming it does not exist.]
Description []
SideEffects []
SeeAlso []
Definition at line 58 of file ivyObj.c.
00059 { 00060 return Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pDriver, NULL, IVY_PO, IVY_INIT_NONE) ); 00061 }
Function*************************************************************
Synopsis [Deletes the node.]
Description []
SideEffects []
SeeAlso []
Definition at line 252 of file ivyObj.c.
00253 { 00254 assert( !Ivy_IsComplement(pObj) ); 00255 assert( Ivy_ObjRefs(pObj) == 0 || !fFreeTop ); 00256 // update node counters of the manager 00257 p->nObjs[pObj->Type]--; 00258 p->nDeleted++; 00259 // remove connections 00260 Ivy_ObjDisconnect( p, pObj ); 00261 // remove PIs/POs from the arrays 00262 if ( Ivy_ObjIsPi(pObj) ) 00263 Vec_PtrRemove( p->vPis, pObj ); 00264 else if ( Ivy_ObjIsPo(pObj) ) 00265 Vec_PtrRemove( p->vPos, pObj ); 00266 else if ( p->fFanout && Ivy_ObjIsBuf(pObj) ) 00267 Vec_PtrRemove( p->vBufs, pObj ); 00268 // clean and recycle the entry 00269 if ( fFreeTop ) 00270 { 00271 // free the node 00272 Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); 00273 Ivy_ManRecycleMemory( p, pObj ); 00274 } 00275 else 00276 { 00277 int nRefsOld = pObj->nRefs; 00278 Ivy_Obj_t * pFanout = pObj->pFanout; 00279 Ivy_ObjClean( pObj ); 00280 pObj->pFanout = pFanout; 00281 pObj->nRefs = nRefsOld; 00282 } 00283 }
Function*************************************************************
Synopsis [Deletes the MFFC of the node.]
Description []
SideEffects []
SeeAlso []
Definition at line 296 of file ivyObj.c.
00297 { 00298 Ivy_Obj_t * pFanin0, * pFanin1; 00299 assert( !Ivy_IsComplement(pObj) ); 00300 assert( !Ivy_ObjIsNone(pObj) ); 00301 if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsPi(pObj) ) 00302 return; 00303 pFanin0 = Ivy_ObjFanin0(pObj); 00304 pFanin1 = Ivy_ObjFanin1(pObj); 00305 Ivy_ObjDelete( p, pObj, fFreeTop ); 00306 if ( pFanin0 && !Ivy_ObjIsNone(pFanin0) && Ivy_ObjRefs(pFanin0) == 0 ) 00307 Ivy_ObjDelete_rec( p, pFanin0, 1 ); 00308 if ( pFanin1 && !Ivy_ObjIsNone(pFanin1) && Ivy_ObjRefs(pFanin1) == 0 ) 00309 Ivy_ObjDelete_rec( p, pFanin1, 1 ); 00310 }
Function*************************************************************
Synopsis [Removes the fanout.]
Description []
SideEffects []
SeeAlso []
Definition at line 202 of file ivyFanout.c.
00203 { 00204 Ivy_Obj_t ** ppPlace1, ** ppPlace2, ** ppPlaceN; 00205 assert( pFanin->pFanout != NULL ); 00206 00207 ppPlace1 = Ivy_ObjNextFanoutPlace(pFanin, pFanout); 00208 ppPlaceN = Ivy_ObjPrevNextFanoutPlace(pFanin, pFanout); 00209 assert( *ppPlaceN == pFanout ); 00210 if ( ppPlaceN ) 00211 *ppPlaceN = *ppPlace1; 00212 00213 ppPlace2 = Ivy_ObjPrevFanoutPlace(pFanin, pFanout); 00214 ppPlaceN = Ivy_ObjNextPrevFanoutPlace(pFanin, pFanout); 00215 assert( ppPlaceN == NULL || *ppPlaceN == pFanout ); 00216 if ( ppPlaceN ) 00217 *ppPlaceN = *ppPlace2; 00218 00219 *ppPlace1 = NULL; 00220 *ppPlace2 = NULL; 00221 }
Function*************************************************************
Synopsis [Connect the object to the fanin.]
Description []
SideEffects []
SeeAlso []
Definition at line 182 of file ivyObj.c.
00183 { 00184 assert( !Ivy_IsComplement(pObj) ); 00185 assert( Ivy_ObjIsPi(pObj) || Ivy_ObjIsOneFanin(pObj) || Ivy_ObjFanin1(pObj) != NULL ); 00186 // remove connections 00187 if ( pObj->pFanin0 != NULL ) 00188 { 00189 Ivy_ObjRefsDec(Ivy_ObjFanin0(pObj)); 00190 if ( p->fFanout ) 00191 Ivy_ObjDeleteFanout( p, Ivy_ObjFanin0(pObj), pObj ); 00192 } 00193 if ( pObj->pFanin1 != NULL ) 00194 { 00195 Ivy_ObjRefsDec(Ivy_ObjFanin1(pObj)); 00196 if ( p->fFanout ) 00197 Ivy_ObjDeleteFanout( p, Ivy_ObjFanin1(pObj), pObj ); 00198 } 00199 assert( pObj->pNextFan0 == NULL ); 00200 assert( pObj->pNextFan1 == NULL ); 00201 assert( pObj->pPrevFan0 == NULL ); 00202 assert( pObj->pPrevFan1 == NULL ); 00203 // remove the node from the structural hash table 00204 Ivy_TableDelete( p, pObj ); 00205 // add the first fanin 00206 pObj->pFanin0 = NULL; 00207 pObj->pFanin1 = NULL; 00208 }
Definition at line 273 of file ivy.h.
00273 { return Ivy_Regular(pObj)->pEquiv? Ivy_NotCond(Ivy_Regular(pObj)->pEquiv, Ivy_IsComplement(pObj)) : NULL; }
| static int Ivy_ObjExorFanout | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Definition at line 267 of file ivy.h.
00267 { return Ivy_Regular(pObj->pFanin0); }
Definition at line 268 of file ivy.h.
00268 { return Ivy_Regular(pObj->pFanin1); }
| static int Ivy_ObjFaninC0 | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Definition at line 265 of file ivy.h.
00265 { return Ivy_IsComplement(pObj->pFanin0); }
| static int Ivy_ObjFaninC1 | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Definition at line 266 of file ivy.h.
00266 { return Ivy_IsComplement(pObj->pFanin1); }
| static int Ivy_ObjFaninId0 | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjFaninId1 | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjFaninPhase | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Definition at line 276 of file ivy.h.
00276 { return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; }
Definition at line 296 of file ivy.h.
00297 { 00298 if ( Ivy_ObjFanin0(pFanout) == pObj ) return Ivy_ObjFaninC0(pObj); 00299 if ( Ivy_ObjFanin1(pFanout) == pObj ) return Ivy_ObjFaninC1(pObj); 00300 assert(0); return -1; 00301 }
Function*************************************************************
Synopsis [Reads one fanout.]
Description [Returns fanout if there is only one fanout.]
SideEffects []
SeeAlso []
Definition at line 296 of file ivyFanout.c.
00297 { 00298 Ivy_Obj_t * pFanout; 00299 int Counter = 0; 00300 Ivy_ObjForEachFanoutInt( pObj, pFanout ) 00301 Counter++; 00302 return Counter; 00303 }
| static int Ivy_ObjId | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static Ivy_Init_t Ivy_ObjInit | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsAnd | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsAssert | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Definition at line 236 of file ivy.h.
00236 { return pObj->Type == IVY_ASSERT; }
| static int Ivy_ObjIsBuf | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsCi | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsCo | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsConst1 | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsExor | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsGhost | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsHash | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsLatch | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsMarkA | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| int Ivy_ObjIsMuxType | ( | Ivy_Obj_t * | pNode | ) |
Function*************************************************************
Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
Description []
SideEffects []
SeeAlso []
Definition at line 476 of file ivyUtil.c.
00477 { 00478 Ivy_Obj_t * pNode0, * pNode1; 00479 // check that the node is regular 00480 assert( !Ivy_IsComplement(pNode) ); 00481 // if the node is not AND, this is not MUX 00482 if ( !Ivy_ObjIsAnd(pNode) ) 00483 return 0; 00484 // if the children are not complemented, this is not MUX 00485 if ( !Ivy_ObjFaninC0(pNode) || !Ivy_ObjFaninC1(pNode) ) 00486 return 0; 00487 // get children 00488 pNode0 = Ivy_ObjFanin0(pNode); 00489 pNode1 = Ivy_ObjFanin1(pNode); 00490 // if the children are not ANDs, this is not MUX 00491 if ( !Ivy_ObjIsAnd(pNode0) || !Ivy_ObjIsAnd(pNode1) ) 00492 return 0; 00493 // otherwise the node is MUX iff it has a pair of equal grandchildren 00494 return (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || 00495 (Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1))) || 00496 (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1))) || 00497 (Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1))); 00498 }
| static int Ivy_ObjIsNode | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsNone | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsOneFanin | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsPi | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsPo | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjIsTerm | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjLevel | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static int Ivy_ObjLevelNew | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Definition at line 275 of file ivy.h.
00275 { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level); }
Function*************************************************************
Synopsis [Labels MFFC with the current label.]
Description []
SideEffects []
SeeAlso []
Definition at line 356 of file ivyUtil.c.
00357 { 00358 int nConeSize1, nConeSize2; 00359 assert( !Ivy_IsComplement( pNode ) ); 00360 assert( Ivy_ObjIsNode( pNode ) ); 00361 nConeSize1 = Ivy_ObjRefDeref( p, pNode, 0, 1 ); // dereference 00362 nConeSize2 = Ivy_ObjRefDeref( p, pNode, 1, 0 ); // reference 00363 assert( nConeSize1 == nConeSize2 ); 00364 assert( nConeSize1 > 0 ); 00365 return nConeSize1; 00366 }
Function*************************************************************
Synopsis [Replaces the first fanin of the node by the new fanin.]
Description []
SideEffects []
SeeAlso []
Definition at line 221 of file ivyObj.c.
00222 { 00223 Ivy_Obj_t * pFaninOld; 00224 assert( !Ivy_IsComplement(pObj) ); 00225 pFaninOld = Ivy_ObjFanin0(pObj); 00226 // decrement ref and remove fanout 00227 Ivy_ObjRefsDec( pFaninOld ); 00228 if ( p->fFanout ) 00229 Ivy_ObjDeleteFanout( p, pFaninOld, pObj ); 00230 // update the fanin 00231 pObj->pFanin0 = pFaninNew; 00232 // increment ref and add fanout 00233 Ivy_ObjRefsInc( Ivy_Regular(pFaninNew) ); 00234 if ( p->fFanout ) 00235 Ivy_ObjAddFanout( p, Ivy_Regular(pFaninNew), pObj ); 00236 // get rid of old fanin 00237 if ( !Ivy_ObjIsPi(pFaninOld) && !Ivy_ObjIsConst1(pFaninOld) && Ivy_ObjRefs(pFaninOld) == 0 ) 00238 Ivy_ObjDelete_rec( p, pFaninOld, 1 ); 00239 }
| void Ivy_ObjPatchFanout | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t * | pFanin, | |||
| Ivy_Obj_t * | pFanoutOld, | |||
| Ivy_Obj_t * | pFanoutNew | |||
| ) |
Function*************************************************************
Synopsis [Replaces the fanout of pOld to be pFanoutNew.]
Description []
SideEffects []
SeeAlso []
Definition at line 234 of file ivyFanout.c.
00235 { 00236 Ivy_Obj_t ** ppPlace; 00237 ppPlace = Ivy_ObjPrevNextFanoutPlace(pFanin, pFanoutOld); 00238 assert( *ppPlace == pFanoutOld ); 00239 if ( ppPlace ) 00240 *ppPlace = pFanoutNew; 00241 ppPlace = Ivy_ObjNextPrevFanoutPlace(pFanin, pFanoutOld); 00242 assert( ppPlace == NULL || *ppPlace == pFanoutOld ); 00243 if ( ppPlace ) 00244 *ppPlace = pFanoutNew; 00245 // assuming that pFanoutNew already points to the next fanout 00246 }
| static int Ivy_ObjPhase | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Function*************************************************************
Synopsis [Prints node in HAIG.]
Description []
SideEffects []
SeeAlso []
Definition at line 626 of file ivyUtil.c.
00627 { 00628 Ivy_Obj_t * pTemp; 00629 int fShowFanouts = 0; 00630 assert( !Ivy_IsComplement(pObj) ); 00631 printf( "Node %5d : ", Ivy_ObjId(pObj) ); 00632 if ( Ivy_ObjIsConst1(pObj) ) 00633 printf( "constant 1" ); 00634 else if ( Ivy_ObjIsPi(pObj) ) 00635 printf( "PI" ); 00636 else if ( Ivy_ObjIsPo(pObj) ) 00637 printf( "PO" ); 00638 else if ( Ivy_ObjIsLatch(pObj) ) 00639 printf( "latch (%d%s)", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") ); 00640 else if ( Ivy_ObjIsBuf(pObj) ) 00641 printf( "buffer (%d%s)", Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " ") ); 00642 else 00643 printf( "AND( %5d%s, %5d%s )", 00644 Ivy_ObjFanin0(pObj)->Id, (Ivy_ObjFaninC0(pObj)? "\'" : " "), 00645 Ivy_ObjFanin1(pObj)->Id, (Ivy_ObjFaninC1(pObj)? "\'" : " ") ); 00646 printf( " (refs = %3d)", Ivy_ObjRefs(pObj) ); 00647 if ( fShowFanouts ) 00648 { 00649 Vec_Ptr_t * vFanouts; 00650 Ivy_Obj_t * pFanout; 00651 int i; 00652 vFanouts = Vec_PtrAlloc( 10 ); 00653 printf( "\nFanouts:\n" ); 00654 Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i ) 00655 { 00656 printf( " " ); 00657 printf( "Node %5d : ", Ivy_ObjId(pFanout) ); 00658 if ( Ivy_ObjIsPo(pFanout) ) 00659 printf( "PO" ); 00660 else if ( Ivy_ObjIsLatch(pFanout) ) 00661 printf( "latch (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") ); 00662 else if ( Ivy_ObjIsBuf(pFanout) ) 00663 printf( "buffer (%d%s)", Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " ") ); 00664 else 00665 printf( "AND( %5d%s, %5d%s )", 00666 Ivy_ObjFanin0(pFanout)->Id, (Ivy_ObjFaninC0(pFanout)? "\'" : " "), 00667 Ivy_ObjFanin1(pFanout)->Id, (Ivy_ObjFaninC1(pFanout)? "\'" : " ") ); 00668 printf( "\n" ); 00669 } 00670 Vec_PtrFree( vFanouts ); 00671 return; 00672 } 00673 if ( !fHaig ) 00674 { 00675 if ( pObj->pEquiv == NULL ) 00676 printf( " HAIG node not given" ); 00677 else 00678 printf( " HAIG node = %d%s", Ivy_Regular(pObj->pEquiv)->Id, (Ivy_IsComplement(pObj->pEquiv)? "\'" : " ") ); 00679 return; 00680 } 00681 if ( pObj->pEquiv == NULL ) 00682 return; 00683 // there are choices 00684 if ( Ivy_ObjRefs(pObj) > 0 ) 00685 { 00686 // print equivalence class 00687 printf( " { %5d ", pObj->Id ); 00688 assert( !Ivy_IsComplement(pObj->pEquiv) ); 00689 for ( pTemp = pObj->pEquiv; pTemp != pObj; pTemp = Ivy_Regular(pTemp->pEquiv) ) 00690 printf( " %5d%s", pTemp->Id, (Ivy_IsComplement(pTemp->pEquiv)? "\'" : " ") ); 00691 printf( " }" ); 00692 return; 00693 } 00694 // this is a secondary node 00695 for ( pTemp = Ivy_Regular(pObj->pEquiv); Ivy_ObjRefs(pTemp) == 0; pTemp = Ivy_Regular(pTemp->pEquiv) ); 00696 assert( Ivy_ObjRefs(pTemp) > 0 ); 00697 printf( " class of %d", pTemp->Id ); 00698 }
Function*************************************************************
Synopsis [Reads one fanout.]
Description [Returns fanout if there is only one fanout.]
SideEffects []
SeeAlso []
Definition at line 280 of file ivyFanout.c.
00281 { 00282 return pObj->pFanout; 00283 }
Function*************************************************************
Synopsis [Returns the real fanin.]
Description []
SideEffects []
SeeAlso []
Definition at line 606 of file ivyUtil.c.
00607 { 00608 Ivy_Obj_t * pFanin; 00609 if ( pObj == NULL || !Ivy_ObjIsBuf( Ivy_Regular(pObj) ) ) 00610 return pObj; 00611 pFanin = Ivy_ObjReal( Ivy_ObjChild0(Ivy_Regular(pObj)) ); 00612 return Ivy_NotCond( pFanin, Ivy_IsComplement(pObj) ); 00613 }
Function*************************************************************
Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
Description [If the node is a MUX, returns the control variable C. Assigns nodes T and E to be the then and else variables of the MUX. Node C is never complemented. Nodes T and E can be complemented. This function also recognizes EXOR/NEXOR gates as MUXes.]
SideEffects []
SeeAlso []
Definition at line 514 of file ivyUtil.c.
00515 { 00516 Ivy_Obj_t * pNode0, * pNode1; 00517 assert( !Ivy_IsComplement(pNode) ); 00518 assert( Ivy_ObjIsMuxType(pNode) ); 00519 // get children 00520 pNode0 = Ivy_ObjFanin0(pNode); 00521 pNode1 = Ivy_ObjFanin1(pNode); 00522 // find the control variable 00523 // if ( pNode1->p1 == Fraig_Not(pNode2->p1) ) 00524 if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) 00525 { 00526 // if ( Fraig_IsComplement(pNode1->p1) ) 00527 if ( Ivy_ObjFaninC0(pNode0) ) 00528 { // pNode2->p1 is positive phase of C 00529 *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); 00530 *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); 00531 return Ivy_ObjChild0(pNode1);//pNode2->p1; 00532 } 00533 else 00534 { // pNode1->p1 is positive phase of C 00535 *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); 00536 *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); 00537 return Ivy_ObjChild0(pNode0);//pNode1->p1; 00538 } 00539 } 00540 // else if ( pNode1->p1 == Fraig_Not(pNode2->p2) ) 00541 else if ( Ivy_ObjFaninId0(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC0(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) 00542 { 00543 // if ( Fraig_IsComplement(pNode1->p1) ) 00544 if ( Ivy_ObjFaninC0(pNode0) ) 00545 { // pNode2->p2 is positive phase of C 00546 *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); 00547 *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); 00548 return Ivy_ObjChild1(pNode1);//pNode2->p2; 00549 } 00550 else 00551 { // pNode1->p1 is positive phase of C 00552 *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode0));//pNode1->p2); 00553 *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); 00554 return Ivy_ObjChild0(pNode0);//pNode1->p1; 00555 } 00556 } 00557 // else if ( pNode1->p2 == Fraig_Not(pNode2->p1) ) 00558 else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId0(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC0(pNode1)) ) 00559 { 00560 // if ( Fraig_IsComplement(pNode1->p2) ) 00561 if ( Ivy_ObjFaninC1(pNode0) ) 00562 { // pNode2->p1 is positive phase of C 00563 *ppNodeT = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); 00564 *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); 00565 return Ivy_ObjChild0(pNode1);//pNode2->p1; 00566 } 00567 else 00568 { // pNode1->p2 is positive phase of C 00569 *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); 00570 *ppNodeE = Ivy_Not(Ivy_ObjChild1(pNode1));//pNode2->p2); 00571 return Ivy_ObjChild1(pNode0);//pNode1->p2; 00572 } 00573 } 00574 // else if ( pNode1->p2 == Fraig_Not(pNode2->p2) ) 00575 else if ( Ivy_ObjFaninId1(pNode0) == Ivy_ObjFaninId1(pNode1) && (Ivy_ObjFaninC1(pNode0) ^ Ivy_ObjFaninC1(pNode1)) ) 00576 { 00577 // if ( Fraig_IsComplement(pNode1->p2) ) 00578 if ( Ivy_ObjFaninC1(pNode0) ) 00579 { // pNode2->p2 is positive phase of C 00580 *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); 00581 *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); 00582 return Ivy_ObjChild1(pNode1);//pNode2->p2; 00583 } 00584 else 00585 { // pNode1->p2 is positive phase of C 00586 *ppNodeT = Ivy_Not(Ivy_ObjChild0(pNode0));//pNode1->p1); 00587 *ppNodeE = Ivy_Not(Ivy_ObjChild0(pNode1));//pNode2->p1); 00588 return Ivy_ObjChild1(pNode0);//pNode1->p2; 00589 } 00590 } 00591 assert( 0 ); // this is not MUX 00592 return NULL; 00593 }
| static int Ivy_ObjRefs | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static void Ivy_ObjRefsDec | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static void Ivy_ObjRefsInc | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| void Ivy_ObjReplace | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t * | pObjOld, | |||
| Ivy_Obj_t * | pObjNew, | |||
| int | fDeleteOld, | |||
| int | fFreeTop, | |||
| int | fUpdateLevel | |||
| ) |
Function*************************************************************
Synopsis [Replaces one object by another.]
Description [Both objects are currently in the manager. The new object (pObjNew) should be used instead of the old object (pObjOld). If the new object is complemented or used, the buffer is added.]
SideEffects []
SeeAlso []
Definition at line 325 of file ivyObj.c.
00326 { 00327 int nRefsOld;//, clk; 00328 // the object to be replaced cannot be complemented 00329 assert( !Ivy_IsComplement(pObjOld) ); 00330 // the object to be replaced cannot be a terminal 00331 assert( Ivy_ObjIsNone(pObjOld) || !Ivy_ObjIsPi(pObjOld) ); 00332 // the object to be used cannot be a PO or assert 00333 assert( !Ivy_ObjIsBuf(Ivy_Regular(pObjNew)) ); 00334 // the object cannot be the same 00335 assert( pObjOld != Ivy_Regular(pObjNew) ); 00336 //printf( "Replacing %d by %d.\n", Ivy_Regular(pObjOld)->Id, Ivy_Regular(pObjNew)->Id ); 00337 00338 // if HAIG is defined, create the choice node 00339 if ( p->pHaig ) 00340 { 00341 // if ( pObjOld->Id == 31 ) 00342 // { 00343 // Ivy_ManShow( p, 0 ); 00344 // Ivy_ManShow( p->pHaig, 1 ); 00345 // } 00346 Ivy_ManHaigCreateChoice( p, pObjOld, pObjNew ); 00347 } 00348 // if the new object is complemented or already used, add the buffer 00349 if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) ) 00350 pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) ); 00351 assert( !Ivy_IsComplement(pObjNew) ); 00352 if ( fUpdateLevel ) 00353 { 00354 //clk = clock(); 00355 // if the new node's arrival time is different, recursively update arrival time of the fanouts 00356 if ( p->fFanout && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level ) 00357 { 00358 assert( Ivy_ObjIsNode(pObjOld) ); 00359 pObjOld->Level = pObjNew->Level; 00360 Ivy_ObjUpdateLevel_rec( p, pObjOld ); 00361 } 00362 //p->time1 += clock() - clk; 00363 // if the new node's required time has changed, recursively update required time of the fanins 00364 //clk = clock(); 00365 if ( p->vRequired ) 00366 { 00367 int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id); 00368 if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) ) 00369 { 00370 Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew ); 00371 Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew ); 00372 } 00373 } 00374 //p->time2 += clock() - clk; 00375 } 00376 // delete the old object 00377 if ( fDeleteOld ) 00378 Ivy_ObjDelete_rec( p, pObjOld, fFreeTop ); 00379 // make sure object is not pointing to itself 00380 assert( Ivy_ObjFanin0(pObjNew) == NULL || pObjOld != Ivy_ObjFanin0(pObjNew) ); 00381 assert( Ivy_ObjFanin1(pObjNew) == NULL || pObjOld != Ivy_ObjFanin1(pObjNew) ); 00382 // make sure the old node has no fanin fanout pointers 00383 if ( p->fFanout ) 00384 { 00385 assert( pObjOld->pFanout != NULL ); 00386 assert( pObjNew->pFanout == NULL ); 00387 pObjNew->pFanout = pObjOld->pFanout; 00388 } 00389 // transfer the old object 00390 assert( Ivy_ObjRefs(pObjNew) == 0 ); 00391 nRefsOld = pObjOld->nRefs; 00392 Ivy_ObjOverwrite( pObjOld, pObjNew ); 00393 pObjOld->nRefs = nRefsOld; 00394 // patch the fanout of the fanins 00395 if ( p->fFanout ) 00396 { 00397 Ivy_ObjPatchFanout( p, Ivy_ObjFanin0(pObjOld), pObjNew, pObjOld ); 00398 if ( Ivy_ObjFanin1(pObjOld) ) 00399 Ivy_ObjPatchFanout( p, Ivy_ObjFanin1(pObjOld), pObjNew, pObjOld ); 00400 } 00401 // update the hash table 00402 Ivy_TableUpdate( p, pObjNew, pObjOld->Id ); 00403 // recycle the object that was taken over by pObjOld 00404 Vec_PtrWriteEntry( p->vObjs, pObjNew->Id, NULL ); 00405 Ivy_ManRecycleMemory( p, pObjNew ); 00406 // if the new node is the buffer propagate it 00407 if ( p->fFanout && Ivy_ObjIsBuf(pObjOld) ) 00408 Vec_PtrPush( p->vBufs, pObjOld ); 00409 // Ivy_ManCheckFanouts( p ); 00410 // printf( "\n" ); 00411 /* 00412 if ( p->pHaig ) 00413 { 00414 int x; 00415 Ivy_ManShow( p, 0, NULL ); 00416 Ivy_ManShow( p->pHaig, 1, NULL ); 00417 x = 0; 00418 } 00419 */ 00420 // if ( Ivy_ManCheckFanoutNums(p) ) 00421 // { 00422 // int x = 0; 00423 // } 00424 }
| static void Ivy_ObjSetMarkA | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static void Ivy_ObjSetTravId | ( | Ivy_Obj_t * | pObj, | |
| int | TravId | |||
| ) | [inline, static] |
| static int Ivy_ObjTravId | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
| static Ivy_Type_t Ivy_ObjType | ( | Ivy_Obj_t * | pObj | ) | [inline, static] |
Function*************************************************************
Synopsis [Recursively updates fanout levels.]
Description []
SideEffects []
SeeAlso []
Definition at line 379 of file ivyUtil.c.
00380 { 00381 Ivy_Obj_t * pFanout; 00382 Vec_Ptr_t * vFanouts; 00383 int i, LevelNew; 00384 assert( p->fFanout ); 00385 assert( Ivy_ObjIsNode(pObj) ); 00386 vFanouts = Vec_PtrAlloc( 10 ); 00387 Ivy_ObjForEachFanout( p, pObj, vFanouts, pFanout, i ) 00388 { 00389 if ( Ivy_ObjIsCo(pFanout) ) 00390 { 00391 // assert( (int)Ivy_ObjFanin0(pFanout)->Level <= p->nLevelMax ); 00392 continue; 00393 } 00394 LevelNew = Ivy_ObjLevelNew( pFanout ); 00395 if ( (int)pFanout->Level == LevelNew ) 00396 continue; 00397 pFanout->Level = LevelNew; 00398 Ivy_ObjUpdateLevel_rec( p, pFanout ); 00399 } 00400 Vec_PtrFree( vFanouts ); 00401 }
Function*************************************************************
Synopsis [Recursively updates fanout levels.]
Description []
SideEffects []
SeeAlso []
Definition at line 441 of file ivyUtil.c.
00442 { 00443 Ivy_Obj_t * pFanin; 00444 if ( Ivy_ObjIsConst1(pObj) || Ivy_ObjIsCi(pObj) ) 00445 return; 00446 assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) ); 00447 // process the first fanin 00448 pFanin = Ivy_ObjFanin0(pObj); 00449 if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 ) 00450 { 00451 Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 ); 00452 Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 ); 00453 } 00454 if ( Ivy_ObjIsBuf(pObj) ) 00455 return; 00456 // process the second fanin 00457 pFanin = Ivy_ObjFanin1(pObj); 00458 if ( Vec_IntEntry(p->vRequired, pFanin->Id) > ReqNew - 1 ) 00459 { 00460 Vec_IntWriteEntry( p->vRequired, pFanin->Id, ReqNew - 1 ); 00461 Ivy_ObjUpdateLevelR_rec( p, pFanin, ReqNew - 1 ); 00462 } 00463 }
Definition at line 290 of file ivy.h.
00291 { 00292 if ( Ivy_ObjFanin0(pObj) == pFanin ) return 0; 00293 if ( Ivy_ObjFanin1(pObj) == pFanin ) return 1; 00294 assert(0); return -1; 00295 }
| Ivy_Obj_t* Ivy_Oper | ( | Ivy_Man_t * | p, | |
| Ivy_Obj_t * | p0, | |||
| Ivy_Obj_t * | p1, | |||
| Ivy_Type_t | Type | |||
| ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Perform one operation.]
Description [The argument nodes can be complemented.]
SideEffects []
SeeAlso []
| int Ivy_TableCountEntries | ( | Ivy_Man_t * | p | ) |
Function*************************************************************
Synopsis [Count the number of nodes in the table.]
Description []
SideEffects []
SeeAlso []
Definition at line 184 of file ivyTable.c.
00185 { 00186 int i, Counter = 0; 00187 for ( i = 0; i < p->nTableSize; i++ ) 00188 Counter += (p->pTable[i] != 0); 00189 return Counter; 00190 }
Function*************************************************************
Synopsis [Deletes the node from the hash table.]
Description []
SideEffects []
SeeAlso []
Definition at line 129 of file ivyTable.c.
00130 { 00131 Ivy_Obj_t * pEntry; 00132 int i, * pPlace; 00133 assert( !Ivy_IsComplement(pObj) ); 00134 if ( !Ivy_ObjIsHash(pObj) ) 00135 return; 00136 pPlace = Ivy_TableFind( p, pObj ); 00137 assert( *pPlace == pObj->Id ); // node should be in the table 00138 *pPlace = 0; 00139 // rehash the adjacent entries 00140 i = pPlace - p->pTable; 00141 for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize ) 00142 { 00143 pEntry = Ivy_ManObj( p, p->pTable[i] ); 00144 p->pTable[i] = 0; 00145 Ivy_TableInsert( p, pEntry ); 00146 } 00147 }
Function*************************************************************
Synopsis [Adds the node to the hash table.]
Description []
SideEffects []
SeeAlso []
Definition at line 102 of file ivyTable.c.
00103 { 00104 int * pPlace; 00105 assert( !Ivy_IsComplement(pObj) ); 00106 if ( !Ivy_ObjIsHash(pObj) ) 00107 return; 00108 if ( (pObj->Id & 63) == 0 ) 00109 { 00110 if ( p->nTableSize < 2 * Ivy_ManHashObjNum(p) ) 00111 Ivy_TableResize( p ); 00112 } 00113 pPlace = Ivy_TableFind( p, pObj ); 00114 assert( *pPlace == 0 ); 00115 *pPlace = pObj->Id; 00116 }
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Checks if node with the given attributes is in the hash table.]
Description []
SideEffects []
SeeAlso []
Definition at line 68 of file ivyTable.c.
00069 { 00070 Ivy_Obj_t * pEntry; 00071 int i; 00072 assert( !Ivy_IsComplement(pObj) ); 00073 if ( !Ivy_ObjIsHash(pObj) ) 00074 return NULL; 00075 assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 ); 00076 assert( Ivy_ObjFaninId1(pObj) == 0 || Ivy_ObjFaninId0(pObj) < Ivy_ObjFaninId1(pObj) ); 00077 if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (Ivy_ObjChild1(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) ) 00078 return NULL; 00079 for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize ) 00080 { 00081 pEntry = Ivy_ManObj( p, p->pTable[i] ); 00082 if ( Ivy_ObjChild0(pEntry) == Ivy_ObjChild0(pObj) && 00083 Ivy_ObjChild1(pEntry) == Ivy_ObjChild1(pObj) && 00084 Ivy_ObjInit(pEntry) == Ivy_ObjInit(pObj) && 00085 Ivy_ObjType(pEntry) == Ivy_ObjType(pObj) ) 00086 return pEntry; 00087 } 00088 return NULL; 00089 }
| void Ivy_TableProfile | ( | Ivy_Man_t * | p | ) |
Function********************************************************************
Synopsis [Profiles the hash table.]
Description []
SideEffects []
SeeAlso []
Definition at line 246 of file ivyTable.c.
00247 { 00248 int i, Counter = 0; 00249 for ( i = 0; i < p->nTableSize; i++ ) 00250 { 00251 if ( p->pTable[i] ) 00252 Counter++; 00253 else if ( Counter ) 00254 { 00255 printf( "%d ", Counter ); 00256 Counter = 0; 00257 } 00258 } 00259 }
Function*************************************************************
Synopsis [Updates the table to point to the new node.]
Description [If the old node (pObj) is in the table, updates the table to point to an object with different ID (ObjIdNew). The table should not contain an object with ObjIdNew (this is currently not checked).]
SideEffects []
SeeAlso []
Definition at line 162 of file ivyTable.c.
00163 { 00164 int * pPlace; 00165 assert( !Ivy_IsComplement(pObj) ); 00166 if ( !Ivy_ObjIsHash(pObj) ) 00167 return; 00168 pPlace = Ivy_TableFind( p, pObj ); 00169 assert( *pPlace == pObj->Id ); // node should be in the table 00170 *pPlace = ObjIdNew; 00171 }
| int Ivy_TruthDsd | ( | unsigned | uTruth, | |
| Vec_Int_t * | vTree | |||
| ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Computes DSD of truth table of 5 variables or less.]
Description [Returns 1 if the function is a constant or is fully DSD decomposable using AND/EXOR/MUX gates.]
SideEffects []
SeeAlso []
Definition at line 159 of file ivyDsd.c.
00160 { 00161 Ivy_Dec_t Node; 00162 int i, RetValue; 00163 // set the PI variables 00164 Vec_IntClear( vTree ); 00165 for ( i = 0; i < 5; i++ ) 00166 Vec_IntPush( vTree, 0 ); 00167 // check if it is a constant 00168 if ( uTruth == 0 || ~uTruth == 0 ) 00169 { 00170 Ivy_DecClear( &Node ); 00171 Node.Type = IVY_DEC_CONST1; 00172 Node.fCompl = (uTruth == 0); 00173 Vec_IntPush( vTree, Ivy_DecToInt(Node) ); 00174 return 1; 00175 } 00176 // perform the decomposition 00177 RetValue = Ivy_TruthDecompose_rec( uTruth, vTree ); 00178 if ( RetValue == -1 ) 00179 return 0; 00180 // get the topmost node 00181 if ( (RetValue >> 1) < 5 ) 00182 { // add buffer 00183 Ivy_DecClear( &Node ); 00184 Node.Type = IVY_DEC_BUF; 00185 Node.fCompl = (RetValue & 1); 00186 Node.Fan0 = ((RetValue >> 1) << 1); 00187 Vec_IntPush( vTree, Ivy_DecToInt(Node) ); 00188 } 00189 else if ( RetValue & 1 ) 00190 { // check if the topmost node has to be complemented 00191 Node = Ivy_IntToDec( Vec_IntPop(vTree) ); 00192 assert( Node.fCompl == 0 ); 00193 Node.fCompl = (RetValue & 1); 00194 Vec_IntPush( vTree, Ivy_DecToInt(Node) ); 00195 } 00196 if ( uTruth != Ivy_TruthDsdCompute(vTree) ) 00197 printf( "Verification failed.\n" ); 00198 return 1; 00199 }
| unsigned Ivy_TruthDsdCompute | ( | Vec_Int_t * | vTree | ) |
Function*************************************************************
Synopsis [Computes truth table of decomposition tree for verification.]
Description []
SideEffects []
SeeAlso []
Definition at line 471 of file ivyDsd.c.
00472 { 00473 return Ivy_TruthDsdCompute_rec( Vec_IntSize(vTree)-1, vTree ); 00474 }
| void Ivy_TruthDsdComputePrint | ( | unsigned | uTruth | ) |
Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 671 of file ivyDsd.c.
00672 { 00673 static Vec_Int_t * vTree = NULL; 00674 if ( vTree == NULL ) 00675 vTree = Vec_IntAlloc( 12 ); 00676 if ( Ivy_TruthDsd( uTruth, vTree ) ) 00677 Ivy_TruthDsdPrint( stdout, vTree ); 00678 else 00679 printf( "Undecomposable\n" ); 00680 }
| void Ivy_TruthDsdPrint | ( | FILE * | pFile, | |
| Vec_Int_t * | vTree | |||
| ) |
Function*************************************************************
Synopsis [Prints the decomposition tree.]
Description []
SideEffects []
SeeAlso []
Definition at line 561 of file ivyDsd.c.
00562 { 00563 fprintf( pFile, "F = " ); 00564 Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree ); 00565 fprintf( pFile, "\n" ); 00566 }
