1 /**CFile****************************************************************
2
3 FileName [extraBddImage.c]
4
5 PackageName [extra]
6
7 Synopsis [Various reusable software utilities.]
8
9 Author [Alan Mishchenko]
10
11 Affiliation [UC Berkeley]
12
13 Date [Ver. 1.0. Started - September 1, 2003.]
14
15 Revision [$Id: extraBddImage.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
16
17 ***********************************************************************/
18
19 #include "extraBdd.h"
20
21 ABC_NAMESPACE_IMPL_START
22
23
24 /*
25 The ideas implemented in this file are inspired by the paper:
26 Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple,
27 Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in
28 Image Computation. ICCAD, 2001.
29 */
30
31 /*---------------------------------------------------------------------------*/
32 /* Constant declarations */
33 /*---------------------------------------------------------------------------*/
34
35 /*---------------------------------------------------------------------------*/
36 /* Stucture declarations */
37 /*---------------------------------------------------------------------------*/
38
39 typedef struct Extra_ImageNode_t_ Extra_ImageNode_t;
40 typedef struct Extra_ImagePart_t_ Extra_ImagePart_t;
41 typedef struct Extra_ImageVar_t_ Extra_ImageVar_t;
42
43 struct Extra_ImageTree_t_
44 {
45 Extra_ImageNode_t * pRoot; // the root of quantification tree
46 Extra_ImageNode_t * pCare; // the leaf node with the care set
47 DdNode * bCareSupp; // the cube to quantify from the care
48 int fVerbose; // the verbosity flag
49 int nNodesMax; // the max number of nodes in one iter
50 int nNodesMaxT; // the overall max number of nodes
51 int nIter; // the number of iterations with this tree
52 };
53
54 struct Extra_ImageNode_t_
55 {
56 DdManager * dd; // the manager
57 DdNode * bCube; // the cube to quantify
58 DdNode * bImage; // the partial image
59 Extra_ImageNode_t * pNode1; // the first branch
60 Extra_ImageNode_t * pNode2; // the second branch
61 Extra_ImagePart_t * pPart; // the partition (temporary)
62 };
63
64 struct Extra_ImagePart_t_
65 {
66 DdNode * bFunc; // the partition
67 DdNode * bSupp; // the support of this partition
68 int nNodes; // the number of BDD nodes
69 short nSupp; // the number of support variables
70 short iPart; // the number of this partition
71 };
72
73 struct Extra_ImageVar_t_
74 {
75 int iNum; // the BDD index of this variable
76 DdNode * bParts; // the partition numbers
77 int nParts; // the number of partitions
78 };
79
80 /*---------------------------------------------------------------------------*/
81 /* Type declarations */
82 /*---------------------------------------------------------------------------*/
83
84 /*---------------------------------------------------------------------------*/
85 /* Variable declarations */
86 /*---------------------------------------------------------------------------*/
87
88 /*---------------------------------------------------------------------------*/
89 /* Macro declarations */
90 /*---------------------------------------------------------------------------*/
91
92 /**AutomaticStart*************************************************************/
93
94
95 /*---------------------------------------------------------------------------*/
96 /* Static function prototypes */
97 /*---------------------------------------------------------------------------*/
98
99 static Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
100 int nParts, DdNode ** pbParts, DdNode * bCare );
101 static Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
102 int nParts, Extra_ImagePart_t ** pParts,
103 int nVars, DdNode ** pbVarsNs );
104 static Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
105 int nParts, Extra_ImagePart_t ** pParts,
106 int nVars, Extra_ImageVar_t ** pVars );
107 static void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode );
108 static int Extra_BuildTreeNode( DdManager * dd,
109 int nNodes, Extra_ImageNode_t ** pNodes,
110 int nVars, Extra_ImageVar_t ** pVars );
111 static Extra_ImageNode_t * Extra_MergeTopNodes( DdManager * dd,
112 int nNodes, Extra_ImageNode_t ** pNodes );
113 static void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode );
114 static void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode );
115 static int Extra_FindBestVariable( DdManager * dd,
116 int nNodes, Extra_ImageNode_t ** pNodes,
117 int nVars, Extra_ImageVar_t ** pVars );
118 static void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts,
119 int nNodes, Extra_ImageNode_t ** pNodes,
120 int * piNode1, int * piNode2 );
121 static Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
122 Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 );
123
124 static void Extra_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare,
125 int nParts, DdNode ** pbParts,
126 int nVars, DdNode ** pbVars );
127 static void Extra_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc,
128 DdNode * bVarsCs, DdNode * bVarsNs, int iPart );
129
130 static void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree );
131 static void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int nOffset );
132
133
134 /**AutomaticEnd***************************************************************/
135
136
137 /*---------------------------------------------------------------------------*/
138 /* Definition of exported functions */
139 /*---------------------------------------------------------------------------*/
140
141 /**Function*************************************************************
142
143 Synopsis [Starts the image computation using tree-based scheduling.]
144
145 Description [This procedure starts the image computation. It uses
146 the given care set to test-run the image computation and creates the
147 quantification tree by scheduling variable quantifications. The tree can
148 be used to compute images for other care sets without rescheduling.
149 In this case, Extra_bddImageCompute() should be called.]
150
151 SideEffects []
152
153 SeeAlso []
154
155 ***********************************************************************/
Extra_bddImageStart(DdManager * dd,DdNode * bCare,int nParts,DdNode ** pbParts,int nVars,DdNode ** pbVars,int fVerbose)156 Extra_ImageTree_t * Extra_bddImageStart(
157 DdManager * dd, DdNode * bCare, // the care set
158 int nParts, DdNode ** pbParts, // the partitions for image computation
159 int nVars, DdNode ** pbVars, int fVerbose ) // the NS and parameter variables (not quantified!)
160 {
161 Extra_ImageTree_t * pTree;
162 Extra_ImagePart_t ** pParts;
163 Extra_ImageVar_t ** pVars;
164 Extra_ImageNode_t ** pNodes;
165 int v;
166
167 if ( fVerbose && dd->size <= 80 )
168 Extra_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
169
170 // create variables, partitions and leaf nodes
171 pParts = Extra_CreateParts( dd, nParts, pbParts, bCare );
172 pVars = Extra_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
173 pNodes = Extra_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
174
175 // create the tree
176 pTree = ABC_ALLOC( Extra_ImageTree_t, 1 );
177 memset( pTree, 0, sizeof(Extra_ImageTree_t) );
178 pTree->pCare = pNodes[nParts];
179 pTree->fVerbose = fVerbose;
180
181 // process the nodes
182 while ( Extra_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars ) );
183
184 // make sure the variables are gone
185 for ( v = 0; v < dd->size; v++ )
186 assert( pVars[v] == NULL );
187 ABC_FREE( pVars );
188
189 // merge the topmost nodes
190 while ( (pTree->pRoot = Extra_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
191
192 // make sure the nodes are gone
193 for ( v = 0; v < nParts + 1; v++ )
194 assert( pNodes[v] == NULL );
195 ABC_FREE( pNodes );
196
197 // if ( fVerbose )
198 // Extra_bddImagePrintTree( pTree );
199
200 // set the support of the care set
201 pTree->bCareSupp = Cudd_Support( dd, bCare ); Cudd_Ref( pTree->bCareSupp );
202
203 // clean the partitions
204 Extra_DeleteParts_rec( pTree->pRoot );
205 ABC_FREE( pParts );
206 return pTree;
207 }
208
209 /**Function*************************************************************
210
211 Synopsis [Compute the image.]
212
213 Description []
214
215 SideEffects []
216
217 SeeAlso []
218
219 ***********************************************************************/
Extra_bddImageCompute(Extra_ImageTree_t * pTree,DdNode * bCare)220 DdNode * Extra_bddImageCompute( Extra_ImageTree_t * pTree, DdNode * bCare )
221 {
222 DdManager * dd = pTree->pCare->dd;
223 DdNode * bSupp, * bRem;
224
225 pTree->nIter++;
226
227 // make sure the supports are okay
228 bSupp = Cudd_Support( dd, bCare ); Cudd_Ref( bSupp );
229 if ( bSupp != pTree->bCareSupp )
230 {
231 bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp ); Cudd_Ref( bRem );
232 if ( bRem != b1 )
233 {
234 printf( "Original care set support: " );
235 ABC_PRB( dd, pTree->bCareSupp );
236 printf( "Current care set support: " );
237 ABC_PRB( dd, bSupp );
238 Cudd_RecursiveDeref( dd, bSupp );
239 Cudd_RecursiveDeref( dd, bRem );
240 printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
241 return NULL;
242 }
243 Cudd_RecursiveDeref( dd, bRem );
244 }
245 Cudd_RecursiveDeref( dd, bSupp );
246
247 // remove the previous image
248 Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
249 pTree->pCare->bImage = bCare; Cudd_Ref( bCare );
250
251 // compute the image
252 pTree->nNodesMax = 0;
253 Extra_bddImageCompute_rec( pTree, pTree->pRoot );
254 if ( pTree->nNodesMaxT < pTree->nNodesMax )
255 pTree->nNodesMaxT = pTree->nNodesMax;
256
257 // if ( pTree->fVerbose )
258 // printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
259 return pTree->pRoot->bImage;
260 }
261
262 /**Function*************************************************************
263
264 Synopsis [Delete the tree.]
265
266 Description []
267
268 SideEffects []
269
270 SeeAlso []
271
272 ***********************************************************************/
Extra_bddImageTreeDelete(Extra_ImageTree_t * pTree)273 void Extra_bddImageTreeDelete( Extra_ImageTree_t * pTree )
274 {
275 if ( pTree->bCareSupp )
276 Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
277 Extra_bddImageTreeDelete_rec( pTree->pRoot );
278 ABC_FREE( pTree );
279 }
280
281 /**Function*************************************************************
282
283 Synopsis [Reads the image from the tree.]
284
285 Description []
286
287 SideEffects []
288
289 SeeAlso []
290
291 ***********************************************************************/
Extra_bddImageRead(Extra_ImageTree_t * pTree)292 DdNode * Extra_bddImageRead( Extra_ImageTree_t * pTree )
293 {
294 return pTree->pRoot->bImage;
295 }
296
297 /*---------------------------------------------------------------------------*/
298 /* Definition of internal functions */
299 /*---------------------------------------------------------------------------*/
300
301 /*---------------------------------------------------------------------------*/
302 /* Definition of static Functions */
303 /*---------------------------------------------------------------------------*/
304
305 /**Function*************************************************************
306
307 Synopsis [Creates partitions.]
308
309 Description []
310
311 SideEffects []
312
313 SeeAlso []
314
315 ***********************************************************************/
Extra_CreateParts(DdManager * dd,int nParts,DdNode ** pbParts,DdNode * bCare)316 Extra_ImagePart_t ** Extra_CreateParts( DdManager * dd,
317 int nParts, DdNode ** pbParts, DdNode * bCare )
318 {
319 Extra_ImagePart_t ** pParts;
320 int i;
321
322 // start the partitions
323 pParts = ABC_ALLOC( Extra_ImagePart_t *, nParts + 1 );
324 // create structures for each variable
325 for ( i = 0; i < nParts; i++ )
326 {
327 pParts[i] = ABC_ALLOC( Extra_ImagePart_t, 1 );
328 pParts[i]->bFunc = pbParts[i]; Cudd_Ref( pParts[i]->bFunc );
329 pParts[i]->bSupp = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
330 pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp );
331 pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
332 pParts[i]->iPart = i;
333 }
334 // add the care set as the last partition
335 pParts[nParts] = ABC_ALLOC( Extra_ImagePart_t, 1 );
336 pParts[nParts]->bFunc = bCare; Cudd_Ref( pParts[nParts]->bFunc );
337 pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
338 pParts[nParts]->nSupp = Extra_bddSuppSize( dd, pParts[nParts]->bSupp );
339 pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc );
340 pParts[nParts]->iPart = nParts;
341 return pParts;
342 }
343
344 /**Function*************************************************************
345
346 Synopsis [Creates variables.]
347
348 Description []
349
350 SideEffects []
351
352 SeeAlso []
353
354 ***********************************************************************/
Extra_CreateVars(DdManager * dd,int nParts,Extra_ImagePart_t ** pParts,int nVars,DdNode ** pbVars)355 Extra_ImageVar_t ** Extra_CreateVars( DdManager * dd,
356 int nParts, Extra_ImagePart_t ** pParts,
357 int nVars, DdNode ** pbVars )
358 {
359 Extra_ImageVar_t ** pVars;
360 DdNode ** pbFuncs;
361 DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp;
362 int nVarsTotal, iVar, p, Counter;
363
364 // put all the functions into one array
365 pbFuncs = ABC_ALLOC( DdNode *, nParts );
366 for ( p = 0; p < nParts; p++ )
367 pbFuncs[p] = pParts[p]->bSupp;
368 bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts ); Cudd_Ref( bSupp );
369 ABC_FREE( pbFuncs );
370
371 // remove the NS vars
372 bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bCubeNs );
373 bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs ); Cudd_Ref( bSupp );
374 Cudd_RecursiveDeref( dd, bTemp );
375 Cudd_RecursiveDeref( dd, bCubeNs );
376
377 // get the number of I and CS variables to be quantified
378 nVarsTotal = Extra_bddSuppSize( dd, bSupp );
379
380 // start the variables
381 pVars = ABC_ALLOC( Extra_ImageVar_t *, dd->size );
382 memset( pVars, 0, sizeof(Extra_ImageVar_t *) * dd->size );
383 // create structures for each variable
384 for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
385 {
386 iVar = bSuppTemp->index;
387 pVars[iVar] = ABC_ALLOC( Extra_ImageVar_t, 1 );
388 pVars[iVar]->iNum = iVar;
389 // collect all the parts this var belongs to
390 Counter = 0;
391 bParts = b1; Cudd_Ref( bParts );
392 for ( p = 0; p < nParts; p++ )
393 if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) )
394 {
395 bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] ); Cudd_Ref( bParts );
396 Cudd_RecursiveDeref( dd, bTemp );
397 Counter++;
398 }
399 pVars[iVar]->bParts = bParts; // takes ref
400 pVars[iVar]->nParts = Counter;
401 }
402 Cudd_RecursiveDeref( dd, bSupp );
403 return pVars;
404 }
405
406 /**Function*************************************************************
407
408 Synopsis [Creates variables.]
409
410 Description []
411
412 SideEffects []
413
414 SeeAlso []
415
416 ***********************************************************************/
Extra_CreateNodes(DdManager * dd,int nParts,Extra_ImagePart_t ** pParts,int nVars,Extra_ImageVar_t ** pVars)417 Extra_ImageNode_t ** Extra_CreateNodes( DdManager * dd,
418 int nParts, Extra_ImagePart_t ** pParts,
419 int nVars, Extra_ImageVar_t ** pVars )
420 {
421 Extra_ImageNode_t ** pNodes;
422 Extra_ImageNode_t * pNode;
423 DdNode * bTemp;
424 int i, v, iPart;
425 /*
426 DdManager * dd; // the manager
427 DdNode * bCube; // the cube to quantify
428 DdNode * bImage; // the partial image
429 Extra_ImageNode_t * pNode1; // the first branch
430 Extra_ImageNode_t * pNode2; // the second branch
431 Extra_ImagePart_t * pPart; // the partition (temporary)
432 */
433 // start the partitions
434 pNodes = ABC_ALLOC( Extra_ImageNode_t *, nParts );
435 // create structures for each leaf nodes
436 for ( i = 0; i < nParts; i++ )
437 {
438 pNodes[i] = ABC_ALLOC( Extra_ImageNode_t, 1 );
439 memset( pNodes[i], 0, sizeof(Extra_ImageNode_t) );
440 pNodes[i]->dd = dd;
441 pNodes[i]->pPart = pParts[i];
442 }
443 // find the quantification cubes for each leaf node
444 for ( v = 0; v < nVars; v++ )
445 {
446 if ( pVars[v] == NULL )
447 continue;
448 assert( pVars[v]->nParts > 0 );
449 if ( pVars[v]->nParts > 1 )
450 continue;
451 iPart = pVars[v]->bParts->index;
452 if ( pNodes[iPart]->bCube == NULL )
453 {
454 pNodes[iPart]->bCube = dd->vars[v];
455 Cudd_Ref( dd->vars[v] );
456 }
457 else
458 {
459 pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] );
460 Cudd_Ref( pNodes[iPart]->bCube );
461 Cudd_RecursiveDeref( dd, bTemp );
462 }
463 // remove these variables
464 Cudd_RecursiveDeref( dd, pVars[v]->bParts );
465 ABC_FREE( pVars[v] );
466 }
467
468 // assign the leaf node images
469 for ( i = 0; i < nParts; i++ )
470 {
471 pNode = pNodes[i];
472 if ( pNode->bCube )
473 {
474 // update the partition
475 pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube );
476 Cudd_Ref( pParts[i]->bFunc );
477 Cudd_RecursiveDeref( dd, bTemp );
478 // update the support the partition
479 pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube );
480 Cudd_Ref( pParts[i]->bSupp );
481 Cudd_RecursiveDeref( dd, bTemp );
482 // update the numbers
483 pParts[i]->nSupp = Extra_bddSuppSize( dd, pParts[i]->bSupp );
484 pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
485 // get rid of the cube
486 // save the last (care set) quantification cube
487 if ( i < nParts - 1 )
488 {
489 Cudd_RecursiveDeref( dd, pNode->bCube );
490 pNode->bCube = NULL;
491 }
492 }
493 // copy the function
494 pNode->bImage = pParts[i]->bFunc; Cudd_Ref( pNode->bImage );
495 }
496 /*
497 for ( i = 0; i < nParts; i++ )
498 {
499 pNode = pNodes[i];
500 ABC_PRB( dd, pNode->bCube );
501 ABC_PRB( dd, pNode->pPart->bFunc );
502 ABC_PRB( dd, pNode->pPart->bSupp );
503 printf( "\n" );
504 }
505 */
506 return pNodes;
507 }
508
509
510 /**Function*************************************************************
511
512 Synopsis [Delete the partitions from the nodes.]
513
514 Description []
515
516 SideEffects []
517
518 SeeAlso []
519
520 ***********************************************************************/
Extra_DeleteParts_rec(Extra_ImageNode_t * pNode)521 void Extra_DeleteParts_rec( Extra_ImageNode_t * pNode )
522 {
523 Extra_ImagePart_t * pPart;
524 if ( pNode->pNode1 )
525 Extra_DeleteParts_rec( pNode->pNode1 );
526 if ( pNode->pNode2 )
527 Extra_DeleteParts_rec( pNode->pNode2 );
528 pPart = pNode->pPart;
529 Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
530 Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
531 ABC_FREE( pNode->pPart );
532 }
533
534 /**Function*************************************************************
535
536 Synopsis [Delete the partitions from the nodes.]
537
538 Description []
539
540 SideEffects []
541
542 SeeAlso []
543
544 ***********************************************************************/
Extra_bddImageTreeDelete_rec(Extra_ImageNode_t * pNode)545 void Extra_bddImageTreeDelete_rec( Extra_ImageNode_t * pNode )
546 {
547 if ( pNode->pNode1 )
548 Extra_bddImageTreeDelete_rec( pNode->pNode1 );
549 if ( pNode->pNode2 )
550 Extra_bddImageTreeDelete_rec( pNode->pNode2 );
551 if ( pNode->bCube )
552 Cudd_RecursiveDeref( pNode->dd, pNode->bCube );
553 if ( pNode->bImage )
554 Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
555 assert( pNode->pPart == NULL );
556 ABC_FREE( pNode );
557 }
558
559 /**Function*************************************************************
560
561 Synopsis [Recompute the image.]
562
563 Description []
564
565 SideEffects []
566
567 SeeAlso []
568
569 ***********************************************************************/
Extra_bddImageCompute_rec(Extra_ImageTree_t * pTree,Extra_ImageNode_t * pNode)570 void Extra_bddImageCompute_rec( Extra_ImageTree_t * pTree, Extra_ImageNode_t * pNode )
571 {
572 DdManager * dd = pNode->dd;
573 DdNode * bTemp;
574 int nNodes;
575
576 // trivial case
577 if ( pNode->pNode1 == NULL )
578 {
579 if ( pNode->bCube )
580 {
581 pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube );
582 Cudd_Ref( pNode->bImage );
583 Cudd_RecursiveDeref( dd, bTemp );
584 }
585 return;
586 }
587
588 // compute the children
589 if ( pNode->pNode1 )
590 Extra_bddImageCompute_rec( pTree, pNode->pNode1 );
591 if ( pNode->pNode2 )
592 Extra_bddImageCompute_rec( pTree, pNode->pNode2 );
593
594 // clean the old image
595 if ( pNode->bImage )
596 Cudd_RecursiveDeref( dd, pNode->bImage );
597 pNode->bImage = NULL;
598
599 // compute the new image
600 if ( pNode->bCube )
601 pNode->bImage = Cudd_bddAndAbstract( dd,
602 pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube );
603 else
604 pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage );
605 Cudd_Ref( pNode->bImage );
606
607 if ( pTree->fVerbose )
608 {
609 nNodes = Cudd_DagSize( pNode->bImage );
610 if ( pTree->nNodesMax < nNodes )
611 pTree->nNodesMax = nNodes;
612 }
613 }
614
615 /**Function*************************************************************
616
617 Synopsis [Builds the tree.]
618
619 Description []
620
621 SideEffects []
622
623 SeeAlso []
624
625 ***********************************************************************/
Extra_BuildTreeNode(DdManager * dd,int nNodes,Extra_ImageNode_t ** pNodes,int nVars,Extra_ImageVar_t ** pVars)626 int Extra_BuildTreeNode( DdManager * dd,
627 int nNodes, Extra_ImageNode_t ** pNodes,
628 int nVars, Extra_ImageVar_t ** pVars )
629 {
630 Extra_ImageNode_t * pNode1, * pNode2;
631 Extra_ImageVar_t * pVar;
632 Extra_ImageNode_t * pNode;
633 DdNode * bCube, * bTemp, * bSuppTemp, * bParts;
634 int iNode1, iNode2;
635 int iVarBest, nSupp, v;
636
637 // find the best variable
638 iVarBest = Extra_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
639 if ( iVarBest == -1 )
640 return 0;
641
642 pVar = pVars[iVarBest];
643
644 // this var cannot appear in one partition only
645 nSupp = Extra_bddSuppSize( dd, pVar->bParts );
646 assert( nSupp == pVar->nParts );
647 assert( nSupp != 1 );
648
649 // if it appears in only two partitions, quantify it
650 if ( pVar->nParts == 2 )
651 {
652 // get the nodes
653 iNode1 = pVar->bParts->index;
654 iNode2 = cuddT(pVar->bParts)->index;
655 pNode1 = pNodes[iNode1];
656 pNode2 = pNodes[iNode2];
657
658 // get the quantification cube
659 bCube = dd->vars[pVar->iNum]; Cudd_Ref( bCube );
660 // add the variables that appear only in these partitions
661 for ( v = 0; v < nVars; v++ )
662 if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts )
663 {
664 // add this var
665 bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] ); Cudd_Ref( bCube );
666 Cudd_RecursiveDeref( dd, bTemp );
667 // clean this var
668 Cudd_RecursiveDeref( dd, pVars[v]->bParts );
669 ABC_FREE( pVars[v] );
670 }
671 // clean the best var
672 Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
673 ABC_FREE( pVars[iVarBest] );
674
675 // combines two nodes
676 pNode = Extra_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
677 Cudd_RecursiveDeref( dd, bCube );
678 }
679 else // if ( pVar->nParts > 2 )
680 {
681 // find two smallest BDDs that have this var
682 Extra_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
683 pNode1 = pNodes[iNode1];
684 pNode2 = pNodes[iNode2];
685
686 // it is not possible that a var appears only in these two
687 // otherwise, it would have a different cost
688 bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts );
689 for ( v = 0; v < nVars; v++ )
690 if ( pVars[v] && pVars[v]->bParts == bParts )
691 assert( 0 );
692 Cudd_RecursiveDeref( dd, bParts );
693
694 // combines two nodes
695 pNode = Extra_CombineTwoNodes( dd, b1, pNode1, pNode2 );
696 }
697
698 // clean the old nodes
699 pNodes[iNode1] = pNode;
700 pNodes[iNode2] = NULL;
701
702 // update the variables that appear in pNode[iNode2]
703 for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
704 {
705 pVar = pVars[bSuppTemp->index];
706 if ( pVar == NULL ) // this variable is not be quantified
707 continue;
708 // quantify this var
709 assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) );
710 pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts );
711 Cudd_RecursiveDeref( dd, bTemp );
712 // add the new var
713 pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts );
714 Cudd_RecursiveDeref( dd, bTemp );
715 // update the score
716 pVar->nParts = Extra_bddSuppSize( dd, pVar->bParts );
717 }
718 return 1;
719 }
720
721
722 /**Function*************************************************************
723
724 Synopsis [Merges the nodes.]
725
726 Description []
727
728 SideEffects []
729
730 SeeAlso []
731
732 ***********************************************************************/
Extra_MergeTopNodes(DdManager * dd,int nNodes,Extra_ImageNode_t ** pNodes)733 Extra_ImageNode_t * Extra_MergeTopNodes(
734 DdManager * dd, int nNodes, Extra_ImageNode_t ** pNodes )
735 {
736 Extra_ImageNode_t * pNode;
737 int n1 = -1, n2 = -1, n;
738
739 // find the first and the second non-empty spots
740 for ( n = 0; n < nNodes; n++ )
741 if ( pNodes[n] )
742 {
743 if ( n1 == -1 )
744 n1 = n;
745 else if ( n2 == -1 )
746 {
747 n2 = n;
748 break;
749 }
750 }
751 assert( n1 != -1 );
752 // check the situation when only one such node is detected
753 if ( n2 == -1 )
754 {
755 // save the node
756 pNode = pNodes[n1];
757 // clean the node
758 pNodes[n1] = NULL;
759 return pNode;
760 }
761
762 // combines two nodes
763 pNode = Extra_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] );
764
765 // clean the old nodes
766 pNodes[n1] = pNode;
767 pNodes[n2] = NULL;
768 return NULL;
769 }
770
771 /**Function*************************************************************
772
773 Synopsis [Merges two nodes.]
774
775 Description []
776
777 SideEffects []
778
779 SeeAlso []
780
781 ***********************************************************************/
Extra_CombineTwoNodes(DdManager * dd,DdNode * bCube,Extra_ImageNode_t * pNode1,Extra_ImageNode_t * pNode2)782 Extra_ImageNode_t * Extra_CombineTwoNodes( DdManager * dd, DdNode * bCube,
783 Extra_ImageNode_t * pNode1, Extra_ImageNode_t * pNode2 )
784 {
785 Extra_ImageNode_t * pNode;
786 Extra_ImagePart_t * pPart;
787
788 // create a new partition
789 pPart = ABC_ALLOC( Extra_ImagePart_t, 1 );
790 memset( pPart, 0, sizeof(Extra_ImagePart_t) );
791 // create the function
792 pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
793 Cudd_Ref( pPart->bFunc );
794 // update the support the partition
795 pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube );
796 Cudd_Ref( pPart->bSupp );
797 // update the numbers
798 pPart->nSupp = Extra_bddSuppSize( dd, pPart->bSupp );
799 pPart->nNodes = Cudd_DagSize( pPart->bFunc );
800 pPart->iPart = -1;
801 /*
802 ABC_PRB( dd, pNode1->pPart->bSupp );
803 ABC_PRB( dd, pNode2->pPart->bSupp );
804 ABC_PRB( dd, pPart->bSupp );
805 */
806 // create a new node
807 pNode = ABC_ALLOC( Extra_ImageNode_t, 1 );
808 memset( pNode, 0, sizeof(Extra_ImageNode_t) );
809 pNode->dd = dd;
810 pNode->pPart = pPart;
811 pNode->pNode1 = pNode1;
812 pNode->pNode2 = pNode2;
813 // compute the image
814 pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube );
815 Cudd_Ref( pNode->bImage );
816 // save the cube
817 if ( bCube != b1 )
818 {
819 pNode->bCube = bCube; Cudd_Ref( bCube );
820 }
821 return pNode;
822 }
823
824 /**Function*************************************************************
825
826 Synopsis [Computes the best variable.]
827
828 Description [The variables is the best if the sum of squares of the
829 BDD sizes of the partitions, in which it participates, is the minimum.]
830
831 SideEffects []
832
833 SeeAlso []
834
835 ***********************************************************************/
Extra_FindBestVariable(DdManager * dd,int nNodes,Extra_ImageNode_t ** pNodes,int nVars,Extra_ImageVar_t ** pVars)836 int Extra_FindBestVariable( DdManager * dd,
837 int nNodes, Extra_ImageNode_t ** pNodes,
838 int nVars, Extra_ImageVar_t ** pVars )
839 {
840 DdNode * bTemp;
841 int iVarBest, v;
842 double CostBest, CostCur;
843
844 CostBest = 100000000000000.0;
845 iVarBest = -1;
846 for ( v = 0; v < nVars; v++ )
847 if ( pVars[v] )
848 {
849 CostCur = 0;
850 for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
851 CostCur += pNodes[bTemp->index]->pPart->nNodes *
852 pNodes[bTemp->index]->pPart->nNodes;
853 if ( CostBest > CostCur )
854 {
855 CostBest = CostCur;
856 iVarBest = v;
857 }
858 }
859 return iVarBest;
860 }
861
862 /**Function*************************************************************
863
864 Synopsis [Computes two smallest partions that have this var.]
865
866 Description []
867
868 SideEffects []
869
870 SeeAlso []
871
872 ***********************************************************************/
Extra_FindBestPartitions(DdManager * dd,DdNode * bParts,int nNodes,Extra_ImageNode_t ** pNodes,int * piNode1,int * piNode2)873 void Extra_FindBestPartitions( DdManager * dd, DdNode * bParts,
874 int nNodes, Extra_ImageNode_t ** pNodes,
875 int * piNode1, int * piNode2 )
876 {
877 DdNode * bTemp;
878 int iPart1, iPart2;
879 int CostMin1, CostMin2, Cost;
880
881 // go through the partitions
882 iPart1 = iPart2 = -1;
883 CostMin1 = CostMin2 = 1000000;
884 for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) )
885 {
886 Cost = pNodes[bTemp->index]->pPart->nNodes;
887 if ( CostMin1 > Cost )
888 {
889 CostMin2 = CostMin1; iPart2 = iPart1;
890 CostMin1 = Cost; iPart1 = bTemp->index;
891 }
892 else if ( CostMin2 > Cost )
893 {
894 CostMin2 = Cost; iPart2 = bTemp->index;
895 }
896 }
897
898 *piNode1 = iPart1;
899 *piNode2 = iPart2;
900 }
901
902 /**Function*************************************************************
903
904 Synopsis [Prints the latch dependency matrix.]
905
906 Description []
907
908 SideEffects []
909
910 SeeAlso []
911
912 ***********************************************************************/
Extra_bddImagePrintLatchDependency(DdManager * dd,DdNode * bCare,int nParts,DdNode ** pbParts,int nVars,DdNode ** pbVars)913 void Extra_bddImagePrintLatchDependency(
914 DdManager * dd, DdNode * bCare, // the care set
915 int nParts, DdNode ** pbParts, // the partitions for image computation
916 int nVars, DdNode ** pbVars ) // the NS and parameter variables (not quantified!)
917 {
918 int i;
919 DdNode * bVarsCs, * bVarsNs;
920
921 bVarsCs = Cudd_Support( dd, bCare ); Cudd_Ref( bVarsCs );
922 bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bVarsNs );
923
924 printf( "The latch dependency matrix:\n" );
925 printf( "Partitions = %d Variables: total = %d non-quantifiable = %d\n",
926 nParts, dd->size, nVars );
927 printf( " : " );
928 for ( i = 0; i < dd->size; i++ )
929 printf( "%d", i % 10 );
930 printf( "\n" );
931
932 for ( i = 0; i < nParts; i++ )
933 Extra_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
934 Extra_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts );
935
936 Cudd_RecursiveDeref( dd, bVarsCs );
937 Cudd_RecursiveDeref( dd, bVarsNs );
938 }
939
940 /**Function*************************************************************
941
942 Synopsis [Prints one row of the latch dependency matrix.]
943
944 Description []
945
946 SideEffects []
947
948 SeeAlso []
949
950 ***********************************************************************/
Extra_bddImagePrintLatchDependencyOne(DdManager * dd,DdNode * bFunc,DdNode * bVarsCs,DdNode * bVarsNs,int iPart)951 void Extra_bddImagePrintLatchDependencyOne(
952 DdManager * dd, DdNode * bFunc, // the function
953 DdNode * bVarsCs, DdNode * bVarsNs, // the current/next state vars
954 int iPart )
955 {
956 DdNode * bSupport;
957 int v;
958 bSupport = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupport );
959 printf( " %3d : ", iPart );
960 for ( v = 0; v < dd->size; v++ )
961 {
962 if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) )
963 {
964 if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) )
965 printf( "c" );
966 else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) )
967 printf( "n" );
968 else
969 printf( "i" );
970 }
971 else
972 printf( "." );
973 }
974 printf( "\n" );
975 Cudd_RecursiveDeref( dd, bSupport );
976 }
977
978
979 /**Function*************************************************************
980
981 Synopsis [Prints the tree for quenstification scheduling.]
982
983 Description []
984
985 SideEffects []
986
987 SeeAlso []
988
989 ***********************************************************************/
Extra_bddImagePrintTree(Extra_ImageTree_t * pTree)990 void Extra_bddImagePrintTree( Extra_ImageTree_t * pTree )
991 {
992 printf( "The quantification scheduling tree:\n" );
993 Extra_bddImagePrintTree_rec( pTree->pRoot, 1 );
994 }
995
996 /**Function*************************************************************
997
998 Synopsis [Prints the tree for quenstification scheduling.]
999
1000 Description []
1001
1002 SideEffects []
1003
1004 SeeAlso []
1005
1006 ***********************************************************************/
Extra_bddImagePrintTree_rec(Extra_ImageNode_t * pNode,int Offset)1007 void Extra_bddImagePrintTree_rec( Extra_ImageNode_t * pNode, int Offset )
1008 {
1009 DdNode * Cube;
1010 int i;
1011
1012 Cube = pNode->bCube;
1013
1014 if ( pNode->pNode1 == NULL )
1015 {
1016 printf( "<%d> ", pNode->pPart->iPart );
1017 if ( Cube != NULL )
1018 {
1019 ABC_PRB( pNode->dd, Cube );
1020 }
1021 else
1022 printf( "\n" );
1023 return;
1024 }
1025
1026 printf( "<*> " );
1027 if ( Cube != NULL )
1028 {
1029 ABC_PRB( pNode->dd, Cube );
1030 }
1031 else
1032 printf( "\n" );
1033
1034 for ( i = 0; i < Offset; i++ )
1035 printf( " " );
1036 Extra_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );
1037
1038 for ( i = 0; i < Offset; i++ )
1039 printf( " " );
1040 Extra_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
1041 }
1042
1043
1044
1045
1046
1047 struct Extra_ImageTree2_t_
1048 {
1049 DdManager * dd;
1050 DdNode * bRel;
1051 DdNode * bCube;
1052 DdNode * bImage;
1053 };
1054
1055 /**Function*************************************************************
1056
1057 Synopsis [Starts the monolithic image computation.]
1058
1059 Description []
1060
1061 SideEffects []
1062
1063 SeeAlso []
1064
1065 ***********************************************************************/
Extra_bddImageStart2(DdManager * dd,DdNode * bCare,int nParts,DdNode ** pbParts,int nVars,DdNode ** pbVars,int fVerbose)1066 Extra_ImageTree2_t * Extra_bddImageStart2(
1067 DdManager * dd, DdNode * bCare,
1068 int nParts, DdNode ** pbParts,
1069 int nVars, DdNode ** pbVars, int fVerbose )
1070 {
1071 Extra_ImageTree2_t * pTree;
1072 DdNode * bCubeAll, * bCubeNot, * bTemp;
1073 int i;
1074
1075 pTree = ABC_ALLOC( Extra_ImageTree2_t, 1 );
1076 pTree->dd = dd;
1077 pTree->bImage = NULL;
1078
1079 bCubeAll = Extra_bddComputeCube( dd, dd->vars, dd->size ); Cudd_Ref( bCubeAll );
1080 bCubeNot = Extra_bddComputeCube( dd, pbVars, nVars ); Cudd_Ref( bCubeNot );
1081 pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
1082 Cudd_RecursiveDeref( dd, bCubeAll );
1083 Cudd_RecursiveDeref( dd, bCubeNot );
1084
1085 // derive the monolithic relation
1086 pTree->bRel = b1; Cudd_Ref( pTree->bRel );
1087 for ( i = 0; i < nParts; i++ )
1088 {
1089 pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
1090 Cudd_RecursiveDeref( dd, bTemp );
1091 }
1092 Extra_bddImageCompute2( pTree, bCare );
1093 return pTree;
1094 }
1095
1096
1097 /**Function*************************************************************
1098
1099 Synopsis []
1100
1101 Description []
1102
1103 SideEffects []
1104
1105 SeeAlso []
1106
1107 ***********************************************************************/
Extra_bddImageCompute2(Extra_ImageTree2_t * pTree,DdNode * bCare)1108 DdNode * Extra_bddImageCompute2( Extra_ImageTree2_t * pTree, DdNode * bCare )
1109 {
1110 if ( pTree->bImage )
1111 Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
1112 pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube );
1113 Cudd_Ref( pTree->bImage );
1114 return pTree->bImage;
1115 }
1116
1117 /**Function*************************************************************
1118
1119 Synopsis []
1120
1121 Description []
1122
1123 SideEffects []
1124
1125 SeeAlso []
1126
1127 ***********************************************************************/
Extra_bddImageTreeDelete2(Extra_ImageTree2_t * pTree)1128 void Extra_bddImageTreeDelete2( Extra_ImageTree2_t * pTree )
1129 {
1130 if ( pTree->bRel )
1131 Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
1132 if ( pTree->bCube )
1133 Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
1134 if ( pTree->bImage )
1135 Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
1136 ABC_FREE( pTree );
1137 }
1138
1139 /**Function*************************************************************
1140
1141 Synopsis [Returns the previously computed image.]
1142
1143 Description []
1144
1145 SideEffects []
1146
1147 SeeAlso []
1148
1149 ***********************************************************************/
Extra_bddImageRead2(Extra_ImageTree2_t * pTree)1150 DdNode * Extra_bddImageRead2( Extra_ImageTree2_t * pTree )
1151 {
1152 return pTree->bImage;
1153 }
1154
1155
1156 ////////////////////////////////////////////////////////////////////////
1157 /// END OF FILE ///
1158 ////////////////////////////////////////////////////////////////////////
1159
1160
1161 ABC_NAMESPACE_IMPL_END
1162
1163