#include "rwr.h"
Go to the source code of this file.
Functions | |
static Rwr_Node_t * | Rwr_ManTryNode (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1, int fExor, int Level, int Volume) |
static void | Rwr_MarkUsed_rec (Rwr_Man_t *p, Rwr_Node_t *pNode) |
void | Rwr_ManPrecompute (Rwr_Man_t *p) |
Rwr_Node_t * | Rwr_ManAddNode (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1, int fExor, int Level, int Volume) |
Rwr_Node_t * | Rwr_ManAddVar (Rwr_Man_t *p, unsigned uTruth, int fPrecompute) |
void | Rwr_Trav_rec (Rwr_Man_t *p, Rwr_Node_t *pNode, int *pVolume) |
int | Rwr_ManNodeVolume (Rwr_Man_t *p, Rwr_Node_t *p0, Rwr_Node_t *p1) |
void | Rwr_ManIncTravId (Rwr_Man_t *p) |
Rwr_Node_t* Rwr_ManAddNode | ( | Rwr_Man_t * | p, | |
Rwr_Node_t * | p0, | |||
Rwr_Node_t * | p1, | |||
int | fExor, | |||
int | Level, | |||
int | Volume | |||
) |
Function*************************************************************
Synopsis [Adds one node.]
Description []
SideEffects []
SeeAlso []
Definition at line 203 of file rwrLib.c.
00204 { 00205 Rwr_Node_t * pNew; 00206 unsigned uTruth; 00207 // compute truth table, leve, volume 00208 p->nConsidered++; 00209 if ( fExor ) 00210 uTruth = (p0->uTruth ^ p1->uTruth); 00211 else 00212 uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 00213 (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF; 00214 // create the new node 00215 pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode ); 00216 pNew->Id = p->vForest->nSize; 00217 pNew->TravId = 0; 00218 pNew->uTruth = uTruth; 00219 pNew->Level = Level; 00220 pNew->Volume = Volume; 00221 pNew->fUsed = 0; 00222 pNew->fExor = fExor; 00223 pNew->p0 = p0; 00224 pNew->p1 = p1; 00225 pNew->pNext = NULL; 00226 Vec_PtrPush( p->vForest, pNew ); 00227 // do not add if the node is not essential 00228 if ( uTruth != p->puCanons[uTruth] ) 00229 return pNew; 00230 00231 // add to the list 00232 p->nAdded++; 00233 if ( p->pTable[uTruth] == NULL ) 00234 p->nClasses++; 00235 Rwr_ListAddToTail( p->pTable + uTruth, pNew ); 00236 return pNew; 00237 }
Rwr_Node_t* Rwr_ManAddVar | ( | Rwr_Man_t * | p, | |
unsigned | uTruth, | |||
int | fPrecompute | |||
) |
Function*************************************************************
Synopsis [Adds one node.]
Description []
SideEffects []
SeeAlso []
Definition at line 250 of file rwrLib.c.
00251 { 00252 Rwr_Node_t * pNew; 00253 pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode ); 00254 pNew->Id = p->vForest->nSize; 00255 pNew->TravId = 0; 00256 pNew->uTruth = uTruth; 00257 pNew->Level = 0; 00258 pNew->Volume = 0; 00259 pNew->fUsed = 1; 00260 pNew->fExor = 0; 00261 pNew->p0 = NULL; 00262 pNew->p1 = NULL; 00263 pNew->pNext = NULL; 00264 Vec_PtrPush( p->vForest, pNew ); 00265 if ( fPrecompute ) 00266 Rwr_ListAddToTail( p->pTable + uTruth, pNew ); 00267 return pNew; 00268 }
void Rwr_ManIncTravId | ( | Rwr_Man_t * | p | ) |
Function*************************************************************
Synopsis [Adds one node.]
Description []
SideEffects []
SeeAlso []
Definition at line 347 of file rwrLib.c.
00348 { 00349 Rwr_Node_t * pNode; 00350 int i; 00351 if ( p->nTravIds++ < 0x8FFFFFFF ) 00352 return; 00353 Vec_PtrForEachEntry( p->vForest, pNode, i ) 00354 pNode->TravId = 0; 00355 p->nTravIds = 1; 00356 }
int Rwr_ManNodeVolume | ( | Rwr_Man_t * | p, | |
Rwr_Node_t * | p0, | |||
Rwr_Node_t * | p1 | |||
) |
Function*************************************************************
Synopsis [Adds one node.]
Description []
SideEffects []
SeeAlso []
Definition at line 327 of file rwrLib.c.
00328 { 00329 int Volume = 0; 00330 Rwr_ManIncTravId( p ); 00331 Rwr_Trav_rec( p, p0, &Volume ); 00332 Rwr_Trav_rec( p, p1, &Volume ); 00333 return Volume; 00334 }
void Rwr_ManPrecompute | ( | Rwr_Man_t * | p | ) |
FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Precomputes the forest in the manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 45 of file rwrLib.c.
00046 { 00047 Rwr_Node_t * p0, * p1; 00048 int i, k, Level, Volume; 00049 int LevelOld = -1; 00050 int nNodes; 00051 00052 Vec_PtrForEachEntryStart( p->vForest, p0, i, 1 ) 00053 Vec_PtrForEachEntryStart( p->vForest, p1, k, 1 ) 00054 { 00055 if ( LevelOld < (int)p0->Level ) 00056 { 00057 LevelOld = p0->Level; 00058 printf( "Starting level %d (at %d nodes).\n", LevelOld+1, i ); 00059 printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n", 00060 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i ); 00061 } 00062 00063 if ( k == i ) 00064 break; 00065 // if ( p0->Level + p1->Level > 6 ) // hard 00066 // break; 00067 00068 if ( p0->Level + p1->Level > 5 ) // easy 00069 break; 00070 00071 // if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) ) 00072 // break; 00073 00074 // compute the level and volume of the new nodes 00075 Level = 1 + ABC_MAX( p0->Level, p1->Level ); 00076 Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 ); 00077 // try four different AND nodes 00078 Rwr_ManTryNode( p, p0 , p1 , 0, Level, Volume ); 00079 Rwr_ManTryNode( p, Rwr_Not(p0), p1 , 0, Level, Volume ); 00080 Rwr_ManTryNode( p, p0 , Rwr_Not(p1), 0, Level, Volume ); 00081 Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume ); 00082 // try EXOR 00083 Rwr_ManTryNode( p, p0 , p1 , 1, Level, Volume + 1 ); 00084 // report the progress 00085 if ( p->nConsidered % 50000000 == 0 ) 00086 printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n", 00087 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i ); 00088 // quit after some time 00089 if ( p->vForest->nSize == RWR_LIMIT + 5 ) 00090 { 00091 printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n", 00092 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i ); 00093 goto save; 00094 } 00095 } 00096 save : 00097 00098 // mark the relevant ones 00099 Rwr_ManIncTravId( p ); 00100 k = 5; 00101 nNodes = 0; 00102 Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 ) 00103 if ( p0->uTruth == p->puCanons[p0->uTruth] ) 00104 { 00105 Rwr_MarkUsed_rec( p, p0 ); 00106 nNodes++; 00107 } 00108 00109 // compact the array by throwing away non-canonical 00110 k = 5; 00111 Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 ) 00112 if ( p0->fUsed ) 00113 { 00114 p->vForest->pArray[k] = p0; 00115 p0->Id = k++; 00116 } 00117 p->vForest->nSize = k; 00118 printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize ); 00119 }
Rwr_Node_t * Rwr_ManTryNode | ( | Rwr_Man_t * | p, | |
Rwr_Node_t * | p0, | |||
Rwr_Node_t * | p1, | |||
int | fExor, | |||
int | Level, | |||
int | Volume | |||
) | [static] |
CFile****************************************************************
FileName [rwrLib.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware AIG rewriting package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [
] DECLARATIONS ///
Function*************************************************************
Synopsis [Adds one node.]
Description []
SideEffects []
SeeAlso []
Definition at line 132 of file rwrLib.c.
00133 { 00134 Rwr_Node_t * pOld, * pNew, ** ppPlace; 00135 unsigned uTruth; 00136 // compute truth table, level, volume 00137 p->nConsidered++; 00138 if ( fExor ) 00139 { 00140 // printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id ); 00141 uTruth = (p0->uTruth ^ p1->uTruth); 00142 } 00143 else 00144 uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) & 00145 (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF; 00146 // skip non-practical classes 00147 if ( Level > 2 && !p->pPractical[p->puCanons[uTruth]] ) 00148 return NULL; 00149 // enumerate through the nodes with the same canonical form 00150 ppPlace = p->pTable + uTruth; 00151 for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext ) 00152 { 00153 if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume ) 00154 return NULL; 00155 if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume ) 00156 return NULL; 00157 // if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume ) 00158 // return NULL; 00159 } 00160 /* 00161 // enumerate through the nodes with the opposite polarity 00162 for ( pOld = p->pTable[~uTruth & 0xFFFF]; pOld; pOld = pOld->pNext ) 00163 { 00164 if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume ) 00165 return NULL; 00166 if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume ) 00167 return NULL; 00168 // if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume ) 00169 // return NULL; 00170 } 00171 */ 00172 // count the classes 00173 if ( p->pTable[uTruth] == NULL && p->puCanons[uTruth] == uTruth ) 00174 p->nClasses++; 00175 // create the new node 00176 pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode ); 00177 pNew->Id = p->vForest->nSize; 00178 pNew->TravId = 0; 00179 pNew->uTruth = uTruth; 00180 pNew->Level = Level; 00181 pNew->Volume = Volume; 00182 pNew->fUsed = 0; 00183 pNew->fExor = fExor; 00184 pNew->p0 = p0; 00185 pNew->p1 = p1; 00186 pNew->pNext = NULL; 00187 Vec_PtrPush( p->vForest, pNew ); 00188 *ppPlace = pNew; 00189 return pNew; 00190 }
void Rwr_MarkUsed_rec | ( | Rwr_Man_t * | p, | |
Rwr_Node_t * | pNode | |||
) | [static] |
Function*************************************************************
Synopsis [Adds one node.]
Description []
SideEffects []
SeeAlso []
Definition at line 283 of file rwrLib.c.
00284 { 00285 if ( pNode->fUsed || pNode->TravId == p->nTravIds ) 00286 return; 00287 pNode->TravId = p->nTravIds; 00288 pNode->fUsed = 1; 00289 Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) ); 00290 Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) ); 00291 }
void Rwr_Trav_rec | ( | Rwr_Man_t * | p, | |
Rwr_Node_t * | pNode, | |||
int * | pVolume | |||
) |
Function*************************************************************
Synopsis [Adds one node.]
Description []
SideEffects []
SeeAlso []
Definition at line 304 of file rwrLib.c.
00305 { 00306 if ( pNode->fUsed || pNode->TravId == p->nTravIds ) 00307 return; 00308 pNode->TravId = p->nTravIds; 00309 (*pVolume)++; 00310 if ( pNode->fExor ) 00311 (*pVolume)++; 00312 Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume ); 00313 Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume ); 00314 }