1 /**CFile****************************************************************
2
3 FileName [rwrLib.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [DAG-aware AIG rewriting package.]
8
9 Synopsis []
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: rwrLib.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "rwr.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 static Rwr_Node_t * Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
31 static void Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode );
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis [Precomputes the forest in the manager.]
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Rwr_ManPrecompute(Rwr_Man_t * p)48 void Rwr_ManPrecompute( Rwr_Man_t * p )
49 {
50 Rwr_Node_t * p0, * p1;
51 int i, k, Level, Volume;
52 int LevelOld = -1;
53 int nNodes;
54
55 Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 1 )
56 Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p1, k, 1 )
57 {
58 if ( LevelOld < (int)p0->Level )
59 {
60 LevelOld = p0->Level;
61 printf( "Starting level %d (at %d nodes).\n", LevelOld+1, i );
62 printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
63 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
64 }
65
66 if ( k == i )
67 break;
68 // if ( p0->Level + p1->Level > 6 ) // hard
69 // break;
70
71 if ( p0->Level + p1->Level > 5 ) // easy
72 break;
73
74 // if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) )
75 // break;
76
77 // compute the level and volume of the new nodes
78 Level = 1 + Abc_MaxInt( p0->Level, p1->Level );
79 Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
80 // try four different AND nodes
81 Rwr_ManTryNode( p, p0 , p1 , 0, Level, Volume );
82 Rwr_ManTryNode( p, Rwr_Not(p0), p1 , 0, Level, Volume );
83 Rwr_ManTryNode( p, p0 , Rwr_Not(p1), 0, Level, Volume );
84 Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume );
85 // try EXOR
86 Rwr_ManTryNode( p, p0 , p1 , 1, Level, Volume + 1 );
87 // report the progress
88 if ( p->nConsidered % 50000000 == 0 )
89 printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
90 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
91 // quit after some time
92 if ( p->vForest->nSize == RWR_LIMIT + 5 )
93 {
94 printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
95 p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
96 goto save;
97 }
98 }
99 save :
100
101 // mark the relevant ones
102 Rwr_ManIncTravId( p );
103 k = 5;
104 nNodes = 0;
105 Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 5 )
106 if ( p0->uTruth == p->puCanons[p0->uTruth] )
107 {
108 Rwr_MarkUsed_rec( p, p0 );
109 nNodes++;
110 }
111
112 // compact the array by throwing away non-canonical
113 k = 5;
114 Vec_PtrForEachEntryStart( Rwr_Node_t *, p->vForest, p0, i, 5 )
115 if ( p0->fUsed )
116 {
117 p->vForest->pArray[k] = p0;
118 p0->Id = k++;
119 }
120 p->vForest->nSize = k;
121 printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize );
122 }
123
124 /**Function*************************************************************
125
126 Synopsis [Adds one node.]
127
128 Description []
129
130 SideEffects []
131
132 SeeAlso []
133
134 ***********************************************************************/
Rwr_ManTryNode(Rwr_Man_t * p,Rwr_Node_t * p0,Rwr_Node_t * p1,int fExor,int Level,int Volume)135 Rwr_Node_t * Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
136 {
137 Rwr_Node_t * pOld, * pNew, ** ppPlace;
138 unsigned uTruth;
139 // compute truth table, level, volume
140 p->nConsidered++;
141 if ( fExor )
142 {
143 // printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id );
144 uTruth = (p0->uTruth ^ p1->uTruth);
145 }
146 else
147 uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) &
148 (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
149 // skip non-practical classes
150 if ( Level > 2 && !p->pPractical[p->puCanons[uTruth]] )
151 return NULL;
152 // enumerate through the nodes with the same canonical form
153 ppPlace = p->pTable + uTruth;
154 for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext )
155 {
156 if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume )
157 return NULL;
158 if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
159 return NULL;
160 // if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume )
161 // return NULL;
162 }
163 /*
164 // enumerate through the nodes with the opposite polarity
165 for ( pOld = p->pTable[~uTruth & 0xFFFF]; pOld; pOld = pOld->pNext )
166 {
167 if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume )
168 return NULL;
169 if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
170 return NULL;
171 // if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume )
172 // return NULL;
173 }
174 */
175 // count the classes
176 if ( p->pTable[uTruth] == NULL && p->puCanons[uTruth] == uTruth )
177 p->nClasses++;
178 // create the new node
179 pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
180 pNew->Id = p->vForest->nSize;
181 pNew->TravId = 0;
182 pNew->uTruth = uTruth;
183 pNew->Level = Level;
184 pNew->Volume = Volume;
185 pNew->fUsed = 0;
186 pNew->fExor = fExor;
187 pNew->p0 = p0;
188 pNew->p1 = p1;
189 pNew->pNext = NULL;
190 Vec_PtrPush( p->vForest, pNew );
191 *ppPlace = pNew;
192 return pNew;
193 }
194
195 /**Function*************************************************************
196
197 Synopsis [Adds one node.]
198
199 Description []
200
201 SideEffects []
202
203 SeeAlso []
204
205 ***********************************************************************/
Rwr_ManAddNode(Rwr_Man_t * p,Rwr_Node_t * p0,Rwr_Node_t * p1,int fExor,int Level,int Volume)206 Rwr_Node_t * Rwr_ManAddNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
207 {
208 Rwr_Node_t * pNew;
209 unsigned uTruth;
210 // compute truth table, leve, volume
211 p->nConsidered++;
212 if ( fExor )
213 uTruth = (p0->uTruth ^ p1->uTruth);
214 else
215 uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) &
216 (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
217 // create the new node
218 pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
219 pNew->Id = p->vForest->nSize;
220 pNew->TravId = 0;
221 pNew->uTruth = uTruth;
222 pNew->Level = Level;
223 pNew->Volume = Volume;
224 pNew->fUsed = 0;
225 pNew->fExor = fExor;
226 pNew->p0 = p0;
227 pNew->p1 = p1;
228 pNew->pNext = NULL;
229 Vec_PtrPush( p->vForest, pNew );
230 // do not add if the node is not essential
231 if ( uTruth != p->puCanons[uTruth] )
232 return pNew;
233
234 // add to the list
235 p->nAdded++;
236 if ( p->pTable[uTruth] == NULL )
237 p->nClasses++;
238 Rwr_ListAddToTail( p->pTable + uTruth, pNew );
239 return pNew;
240 }
241
242 /**Function*************************************************************
243
244 Synopsis [Adds one node.]
245
246 Description []
247
248 SideEffects []
249
250 SeeAlso []
251
252 ***********************************************************************/
Rwr_ManAddVar(Rwr_Man_t * p,unsigned uTruth,int fPrecompute)253 Rwr_Node_t * Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute )
254 {
255 Rwr_Node_t * pNew;
256 pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
257 pNew->Id = p->vForest->nSize;
258 pNew->TravId = 0;
259 pNew->uTruth = uTruth;
260 pNew->Level = 0;
261 pNew->Volume = 0;
262 pNew->fUsed = 1;
263 pNew->fExor = 0;
264 pNew->p0 = NULL;
265 pNew->p1 = NULL;
266 pNew->pNext = NULL;
267 Vec_PtrPush( p->vForest, pNew );
268 if ( fPrecompute )
269 Rwr_ListAddToTail( p->pTable + uTruth, pNew );
270 return pNew;
271 }
272
273
274
275 /**Function*************************************************************
276
277 Synopsis [Adds one node.]
278
279 Description []
280
281 SideEffects []
282
283 SeeAlso []
284
285 ***********************************************************************/
Rwr_MarkUsed_rec(Rwr_Man_t * p,Rwr_Node_t * pNode)286 void Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode )
287 {
288 if ( pNode->fUsed || pNode->TravId == p->nTravIds )
289 return;
290 pNode->TravId = p->nTravIds;
291 pNode->fUsed = 1;
292 Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) );
293 Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) );
294 }
295
296 /**Function*************************************************************
297
298 Synopsis [Adds one node.]
299
300 Description []
301
302 SideEffects []
303
304 SeeAlso []
305
306 ***********************************************************************/
Rwr_Trav_rec(Rwr_Man_t * p,Rwr_Node_t * pNode,int * pVolume)307 void Rwr_Trav_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, int * pVolume )
308 {
309 if ( pNode->fUsed || pNode->TravId == p->nTravIds )
310 return;
311 pNode->TravId = p->nTravIds;
312 (*pVolume)++;
313 if ( pNode->fExor )
314 (*pVolume)++;
315 Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume );
316 Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume );
317 }
318
319 /**Function*************************************************************
320
321 Synopsis [Adds one node.]
322
323 Description []
324
325 SideEffects []
326
327 SeeAlso []
328
329 ***********************************************************************/
Rwr_ManNodeVolume(Rwr_Man_t * p,Rwr_Node_t * p0,Rwr_Node_t * p1)330 int Rwr_ManNodeVolume( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 )
331 {
332 int Volume = 0;
333 Rwr_ManIncTravId( p );
334 Rwr_Trav_rec( p, p0, &Volume );
335 Rwr_Trav_rec( p, p1, &Volume );
336 return Volume;
337 }
338
339 /**Function*************************************************************
340
341 Synopsis [Adds one node.]
342
343 Description []
344
345 SideEffects []
346
347 SeeAlso []
348
349 ***********************************************************************/
Rwr_ManIncTravId(Rwr_Man_t * p)350 void Rwr_ManIncTravId( Rwr_Man_t * p )
351 {
352 Rwr_Node_t * pNode;
353 int i;
354 if ( p->nTravIds++ < 0x8FFFFFFF )
355 return;
356 Vec_PtrForEachEntry( Rwr_Node_t *, p->vForest, pNode, i )
357 pNode->TravId = 0;
358 p->nTravIds = 1;
359 }
360
361 ////////////////////////////////////////////////////////////////////////
362 /// END OF FILE ///
363 ////////////////////////////////////////////////////////////////////////
364
365
366 ABC_NAMESPACE_IMPL_END
367
368