ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bbrImage.c
Go to the documentation of this file.
1
20
21#include "bbr.h"
22#include "bdd/mtr/mtr.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
27/*
28 The ideas implemented in this file are inspired by the paper:
29 Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple,
30 Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in
31 Image Computation. ICCAD, 2001.
32*/
33
34/*---------------------------------------------------------------------------*/
35/* Constant declarations */
36/*---------------------------------------------------------------------------*/
37
38/*---------------------------------------------------------------------------*/
39/* Stucture declarations */
40/*---------------------------------------------------------------------------*/
41
42typedef struct Bbr_ImageNode_t_ Bbr_ImageNode_t;
43typedef struct Bbr_ImagePart_t_ Bbr_ImagePart_t;
44typedef struct Bbr_ImageVar_t_ Bbr_ImageVar_t;
45
46struct Bbr_ImageTree_t_
47{
48 Bbr_ImageNode_t * pRoot; // the root of quantification tree
49 Bbr_ImageNode_t * pCare; // the leaf node with the care set
50 DdNode * bCareSupp; // the cube to quantify from the care
51 int fVerbose; // the verbosity flag
52 int nNodesMax; // the max number of nodes in one iter
53 int nNodesMaxT; // the overall max number of nodes
54 int nIter; // the number of iterations with this tree
55 int nBddMax; // the number of node to stop
56};
57
58struct Bbr_ImageNode_t_
59{
60 DdManager * dd; // the manager
61 DdNode * bCube; // the cube to quantify
62 DdNode * bImage; // the partial image
63 Bbr_ImageNode_t * pNode1; // the first branch
64 Bbr_ImageNode_t * pNode2; // the second branch
65 Bbr_ImagePart_t * pPart; // the partition (temporary)
66};
67
68struct Bbr_ImagePart_t_
69{
70 DdNode * bFunc; // the partition
71 DdNode * bSupp; // the support of this partition
72 int nNodes; // the number of BDD nodes
73 short nSupp; // the number of support variables
74 short iPart; // the number of this partition
75};
76
77struct Bbr_ImageVar_t_
78{
79 int iNum; // the BDD index of this variable
80 DdNode * bParts; // the partition numbers
81 int nParts; // the number of partitions
82};
83
84/*---------------------------------------------------------------------------*/
85/* Type declarations */
86/*---------------------------------------------------------------------------*/
87
88/*---------------------------------------------------------------------------*/
89/* Variable declarations */
90/*---------------------------------------------------------------------------*/
91
92/*---------------------------------------------------------------------------*/
93/* Macro declarations */
94/*---------------------------------------------------------------------------*/
95
96#define b0 Cudd_Not((dd)->one)
97#define b1 (dd)->one
98
99#ifndef ABC_PRB
100#define ABC_PRB(dd,f) printf("%s = ", #f); Bbr_bddPrint(dd,f); printf("\n")
101#endif
102
104
105
106/*---------------------------------------------------------------------------*/
107/* Static function prototypes */
108/*---------------------------------------------------------------------------*/
109
110static Bbr_ImagePart_t ** Bbr_CreateParts( DdManager * dd,
111 int nParts, DdNode ** pbParts, DdNode * bCare );
112static Bbr_ImageVar_t ** Bbr_CreateVars( DdManager * dd,
113 int nParts, Bbr_ImagePart_t ** pParts,
114 int nVars, DdNode ** pbVarsNs );
115static Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd,
116 int nParts, Bbr_ImagePart_t ** pParts,
117 int nVars, Bbr_ImageVar_t ** pVars );
118static void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode );
119static int Bbr_BuildTreeNode( DdManager * dd,
120 int nNodes, Bbr_ImageNode_t ** pNodes,
121 int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax );
122static Bbr_ImageNode_t * Bbr_MergeTopNodes( DdManager * dd,
123 int nNodes, Bbr_ImageNode_t ** pNodes );
124static void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode );
125static int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode );
126static int Bbr_FindBestVariable( DdManager * dd,
127 int nNodes, Bbr_ImageNode_t ** pNodes,
128 int nVars, Bbr_ImageVar_t ** pVars );
129static void Bbr_FindBestPartitions( DdManager * dd, DdNode * bParts,
130 int nNodes, Bbr_ImageNode_t ** pNodes,
131 int * piNode1, int * piNode2 );
132static Bbr_ImageNode_t * Bbr_CombineTwoNodes( DdManager * dd, DdNode * bCube,
133 Bbr_ImageNode_t * pNode1, Bbr_ImageNode_t * pNode2 );
134
135static void Bbr_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare,
136 int nParts, DdNode ** pbParts,
137 int nVars, DdNode ** pbVars );
138static void Bbr_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc,
139 DdNode * bVarsCs, DdNode * bVarsNs, int iPart );
140
141static void Bbr_bddImagePrintTree( Bbr_ImageTree_t * pTree );
142static void Bbr_bddImagePrintTree_rec( Bbr_ImageNode_t * pNode, int nOffset );
143
144static void Bbr_bddPrint( DdManager * dd, DdNode * F );
145
147
148
149/*---------------------------------------------------------------------------*/
150/* Definition of exported functions */
151/*---------------------------------------------------------------------------*/
152
168Bbr_ImageTree_t * Bbr_bddImageStart(
169 DdManager * dd, DdNode * bCare, // the care set
170 int nParts, DdNode ** pbParts, // the partitions for image computation
171 int nVars, DdNode ** pbVars, int nBddMax, int fVerbose ) // the NS and parameter variables (not quantified!)
172{
173 Bbr_ImageTree_t * pTree;
174 Bbr_ImagePart_t ** pParts;
175 Bbr_ImageVar_t ** pVars;
176 Bbr_ImageNode_t ** pNodes, * pCare;
177 int fStop, v;
178
179 if ( fVerbose && dd->size <= 80 )
180 Bbr_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
181
182 // create variables, partitions and leaf nodes
183 pParts = Bbr_CreateParts( dd, nParts, pbParts, bCare );
184 pVars = Bbr_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
185 pNodes = Bbr_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
186 pCare = pNodes[nParts];
187
188 // process the nodes
189 while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop, nBddMax ) );
190
191 // consider the case of BDD node blowup
192 if ( fStop )
193 {
194 for ( v = 0; v < dd->size; v++ )
195 if ( pVars[v] )
196 ABC_FREE( pVars[v] );
197 ABC_FREE( pVars );
198 for ( v = 0; v <= nParts; v++ )
199 if ( pNodes[v] )
200 {
201 Bbr_DeleteParts_rec( pNodes[v] );
202 Bbr_bddImageTreeDelete_rec( pNodes[v] );
203 }
204 ABC_FREE( pNodes );
205 ABC_FREE( pParts );
206 return NULL;
207 }
208
209 // make sure the variables are gone
210 for ( v = 0; v < dd->size; v++ )
211 assert( pVars[v] == NULL );
212 ABC_FREE( pVars );
213
214 // create the tree
215 pTree = ABC_ALLOC( Bbr_ImageTree_t, 1 );
216 memset( pTree, 0, sizeof(Bbr_ImageTree_t) );
217 pTree->pCare = pCare;
218 pTree->nBddMax = nBddMax;
219 pTree->fVerbose = fVerbose;
220
221 // merge the topmost nodes
222 while ( (pTree->pRoot = Bbr_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
223
224 // make sure the nodes are gone
225 for ( v = 0; v < nParts + 1; v++ )
226 assert( pNodes[v] == NULL );
227 ABC_FREE( pNodes );
228
229// if ( fVerbose )
230// Bbr_bddImagePrintTree( pTree );
231
232 // set the support of the care set
233 pTree->bCareSupp = Cudd_Support( dd, bCare ); Cudd_Ref( pTree->bCareSupp );
234
235 // clean the partitions
236 Bbr_DeleteParts_rec( pTree->pRoot );
237 ABC_FREE( pParts );
238
239 return pTree;
240}
241
253DdNode * Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare )
254{
255 DdManager * dd = pTree->pCare->dd;
256 DdNode * bSupp, * bRem;
257
258 pTree->nIter++;
259
260 // make sure the supports are okay
261 bSupp = Cudd_Support( dd, bCare ); Cudd_Ref( bSupp );
262 if ( bSupp != pTree->bCareSupp )
263 {
264 bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp ); Cudd_Ref( bRem );
265 if ( bRem != b1 )
266 {
267printf( "Original care set support: " );
268ABC_PRB( dd, pTree->bCareSupp );
269printf( "Current care set support: " );
270ABC_PRB( dd, bSupp );
271 Cudd_RecursiveDeref( dd, bSupp );
272 Cudd_RecursiveDeref( dd, bRem );
273 printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
274 return NULL;
275 }
276 Cudd_RecursiveDeref( dd, bRem );
277 }
278 Cudd_RecursiveDeref( dd, bSupp );
279
280 // remove the previous image
281 Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
282 pTree->pCare->bImage = bCare; Cudd_Ref( bCare );
283
284 // compute the image
285 pTree->nNodesMax = 0;
286 if ( !Bbr_bddImageCompute_rec( pTree, pTree->pRoot ) )
287 return NULL;
288 if ( pTree->nNodesMaxT < pTree->nNodesMax )
289 pTree->nNodesMaxT = pTree->nNodesMax;
290
291// if ( pTree->fVerbose )
292// printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
293 return pTree->pRoot->bImage;
294}
295
307void Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree )
308{
309 if ( pTree->bCareSupp )
310 Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
311 Bbr_bddImageTreeDelete_rec( pTree->pRoot );
312 ABC_FREE( pTree );
313}
314
326DdNode * Bbr_bddImageRead( Bbr_ImageTree_t * pTree )
327{
328 return pTree->pRoot->bImage;
329}
330
331/*---------------------------------------------------------------------------*/
332/* Definition of internal functions */
333/*---------------------------------------------------------------------------*/
334
346void Bbr_bddPrint( DdManager * dd, DdNode * F )
347{
348 DdGen * Gen;
349 int * Cube;
350 CUDD_VALUE_TYPE Value;
351 int nVars = dd->size;
352 int fFirstCube = 1;
353 int i;
354
355 if ( F == NULL )
356 {
357 printf("NULL");
358 return;
359 }
360 if ( F == b0 )
361 {
362 printf("Constant 0");
363 return;
364 }
365 if ( F == b1 )
366 {
367 printf("Constant 1");
368 return;
369 }
370
371 Cudd_ForeachCube( dd, F, Gen, Cube, Value )
372 {
373 if ( fFirstCube )
374 fFirstCube = 0;
375 else
376// Output << " + ";
377 printf( " + " );
378
379 for ( i = 0; i < nVars; i++ )
380 if ( Cube[i] == 0 )
381 printf( "[%d]'", i );
382// printf( "%c'", (char)('a'+i) );
383 else if ( Cube[i] == 1 )
384 printf( "[%d]", i );
385// printf( "%c", (char)('a'+i) );
386 }
387
388// printf("\n");
389}
390
391/*---------------------------------------------------------------------------*/
392/* Definition of static Functions */
393/*---------------------------------------------------------------------------*/
394
406Bbr_ImagePart_t ** Bbr_CreateParts( DdManager * dd,
407 int nParts, DdNode ** pbParts, DdNode * bCare )
408{
409 Bbr_ImagePart_t ** pParts;
410 int i;
411
412 // start the partitions
413 pParts = ABC_ALLOC( Bbr_ImagePart_t *, nParts + 1 );
414 // create structures for each variable
415 for ( i = 0; i < nParts; i++ )
416 {
417 pParts[i] = ABC_ALLOC( Bbr_ImagePart_t, 1 );
418 pParts[i]->bFunc = pbParts[i]; Cudd_Ref( pParts[i]->bFunc );
419 pParts[i]->bSupp = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
420 pParts[i]->nSupp = Cudd_SupportSize( dd, pParts[i]->bSupp );
421 pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
422 pParts[i]->iPart = i;
423 }
424 // add the care set as the last partition
425 pParts[nParts] = ABC_ALLOC( Bbr_ImagePart_t, 1 );
426 pParts[nParts]->bFunc = bCare; Cudd_Ref( pParts[nParts]->bFunc );
427 pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
428 pParts[nParts]->nSupp = Cudd_SupportSize( dd, pParts[nParts]->bSupp );
429 pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc );
430 pParts[nParts]->iPart = nParts;
431 return pParts;
432}
433
445Bbr_ImageVar_t ** Bbr_CreateVars( DdManager * dd,
446 int nParts, Bbr_ImagePart_t ** pParts,
447 int nVars, DdNode ** pbVars )
448{
449 Bbr_ImageVar_t ** pVars;
450 DdNode ** pbFuncs;
451 DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp;
452 int nVarsTotal, iVar, p, Counter;
453
454 // put all the functions into one array
455 pbFuncs = ABC_ALLOC( DdNode *, nParts );
456 for ( p = 0; p < nParts; p++ )
457 pbFuncs[p] = pParts[p]->bSupp;
458 bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts ); Cudd_Ref( bSupp );
459 ABC_FREE( pbFuncs );
460
461 // remove the NS vars
462 bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bCubeNs );
463 bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs ); Cudd_Ref( bSupp );
464 Cudd_RecursiveDeref( dd, bTemp );
465 Cudd_RecursiveDeref( dd, bCubeNs );
466
467 // get the number of I and CS variables to be quantified
468 nVarsTotal = Cudd_SupportSize( dd, bSupp );
469
470 // start the variables
471 pVars = ABC_ALLOC( Bbr_ImageVar_t *, dd->size );
472 memset( pVars, 0, sizeof(Bbr_ImageVar_t *) * dd->size );
473 // create structures for each variable
474 for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
475 {
476 iVar = bSuppTemp->index;
477 pVars[iVar] = ABC_ALLOC( Bbr_ImageVar_t, 1 );
478 pVars[iVar]->iNum = iVar;
479 // collect all the parts this var belongs to
480 Counter = 0;
481 bParts = b1; Cudd_Ref( bParts );
482 for ( p = 0; p < nParts; p++ )
483 if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) )
484 {
485 bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] ); Cudd_Ref( bParts );
486 Cudd_RecursiveDeref( dd, bTemp );
487 Counter++;
488 }
489 pVars[iVar]->bParts = bParts; // takes ref
490 pVars[iVar]->nParts = Counter;
491 }
492 Cudd_RecursiveDeref( dd, bSupp );
493 return pVars;
494}
495
507Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd,
508 int nParts, Bbr_ImagePart_t ** pParts,
509 int nVars, Bbr_ImageVar_t ** pVars )
510{
511 Bbr_ImageNode_t ** pNodes;
512 Bbr_ImageNode_t * pNode;
513 DdNode * bTemp;
514 int i, v, iPart;
515/*
516 DdManager * dd; // the manager
517 DdNode * bCube; // the cube to quantify
518 DdNode * bImage; // the partial image
519 Bbr_ImageNode_t * pNode1; // the first branch
520 Bbr_ImageNode_t * pNode2; // the second branch
521 Bbr_ImagePart_t * pPart; // the partition (temporary)
522*/
523 // start the partitions
524 pNodes = ABC_ALLOC( Bbr_ImageNode_t *, nParts );
525 // create structures for each leaf nodes
526 for ( i = 0; i < nParts; i++ )
527 {
528 pNodes[i] = ABC_ALLOC( Bbr_ImageNode_t, 1 );
529 memset( pNodes[i], 0, sizeof(Bbr_ImageNode_t) );
530 pNodes[i]->dd = dd;
531 pNodes[i]->pPart = pParts[i];
532 }
533 // find the quantification cubes for each leaf node
534 for ( v = 0; v < nVars; v++ )
535 {
536 if ( pVars[v] == NULL )
537 continue;
538 assert( pVars[v]->nParts > 0 );
539 if ( pVars[v]->nParts > 1 )
540 continue;
541 iPart = pVars[v]->bParts->index;
542 if ( pNodes[iPart]->bCube == NULL )
543 {
544 pNodes[iPart]->bCube = dd->vars[v];
545 Cudd_Ref( dd->vars[v] );
546 }
547 else
548 {
549 pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] );
550 Cudd_Ref( pNodes[iPart]->bCube );
551 Cudd_RecursiveDeref( dd, bTemp );
552 }
553 // remove these variables
554 Cudd_RecursiveDeref( dd, pVars[v]->bParts );
555 ABC_FREE( pVars[v] );
556 }
557
558 // assign the leaf node images
559 for ( i = 0; i < nParts; i++ )
560 {
561 pNode = pNodes[i];
562 if ( pNode->bCube )
563 {
564 // update the partition
565 pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube );
566 Cudd_Ref( pParts[i]->bFunc );
567 Cudd_RecursiveDeref( dd, bTemp );
568 // update the support the partition
569 pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube );
570 Cudd_Ref( pParts[i]->bSupp );
571 Cudd_RecursiveDeref( dd, bTemp );
572 // update the numbers
573 pParts[i]->nSupp = Cudd_SupportSize( dd, pParts[i]->bSupp );
574 pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
575 // get rid of the cube
576 // save the last (care set) quantification cube
577 if ( i < nParts - 1 )
578 {
579 Cudd_RecursiveDeref( dd, pNode->bCube );
580 pNode->bCube = NULL;
581 }
582 }
583 // copy the function
584 pNode->bImage = pParts[i]->bFunc; Cudd_Ref( pNode->bImage );
585 }
586/*
587 for ( i = 0; i < nParts; i++ )
588 {
589 pNode = pNodes[i];
590ABC_PRB( dd, pNode->bCube );
591ABC_PRB( dd, pNode->pPart->bFunc );
592ABC_PRB( dd, pNode->pPart->bSupp );
593printf( "\n" );
594 }
595*/
596 return pNodes;
597}
598
599
611void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode )
612{
613 Bbr_ImagePart_t * pPart;
614 if ( pNode->pNode1 )
615 Bbr_DeleteParts_rec( pNode->pNode1 );
616 if ( pNode->pNode2 )
617 Bbr_DeleteParts_rec( pNode->pNode2 );
618 pPart = pNode->pPart;
619 Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
620 Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
621 ABC_FREE( pNode->pPart );
622}
623
635void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode )
636{
637 if ( pNode->pNode1 )
638 Bbr_bddImageTreeDelete_rec( pNode->pNode1 );
639 if ( pNode->pNode2 )
640 Bbr_bddImageTreeDelete_rec( pNode->pNode2 );
641 if ( pNode->bCube )
642 Cudd_RecursiveDeref( pNode->dd, pNode->bCube );
643 if ( pNode->bImage )
644 Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
645 assert( pNode->pPart == NULL );
646 ABC_FREE( pNode );
647}
648
660int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
661{
662 DdManager * dd = pNode->dd;
663 DdNode * bTemp;
664 int nNodes;
665
666 // trivial case
667 if ( pNode->pNode1 == NULL )
668 {
669 if ( pNode->bCube )
670 {
671 pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube );
672 Cudd_Ref( pNode->bImage );
673 Cudd_RecursiveDeref( dd, bTemp );
674 }
675 return 1;
676 }
677
678 // compute the children
679 if ( pNode->pNode1 )
680 if ( !Bbr_bddImageCompute_rec( pTree, pNode->pNode1 ) )
681 return 0;
682 if ( pNode->pNode2 )
683 if ( !Bbr_bddImageCompute_rec( pTree, pNode->pNode2 ) )
684 return 0;
685
686 // clean the old image
687 if ( pNode->bImage )
688 Cudd_RecursiveDeref( dd, pNode->bImage );
689 pNode->bImage = NULL;
690
691 // compute the new image
692 if ( pNode->bCube )
693 pNode->bImage = Cudd_bddAndAbstract( dd,
694 pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube );
695 else
696 pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage );
697 Cudd_Ref( pNode->bImage );
698
699 if ( pTree->fVerbose )
700 {
701 nNodes = Cudd_DagSize( pNode->bImage );
702 if ( pTree->nNodesMax < nNodes )
703 pTree->nNodesMax = nNodes;
704 }
705 if ( dd->keys-dd->dead > (unsigned)pTree->nBddMax )
706 return 0;
707 return 1;
708}
709
721int Bbr_BuildTreeNode( DdManager * dd,
722 int nNodes, Bbr_ImageNode_t ** pNodes,
723 int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax )
724{
725 Bbr_ImageNode_t * pNode1, * pNode2;
726 Bbr_ImageVar_t * pVar;
727 Bbr_ImageNode_t * pNode;
728 DdNode * bCube, * bTemp, * bSuppTemp;//, * bParts;
729 int iNode1, iNode2;
730 int iVarBest, nSupp, v;
731
732 // find the best variable
733 iVarBest = Bbr_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
734 if ( iVarBest == -1 )
735 return 0;
736/*
737for ( v = 0; v < nVars; v++ )
738{
739 DdNode * bSupp;
740 if ( pVars[v] == NULL )
741 continue;
742 printf( "%3d :", v );
743 printf( "%3d ", pVars[v]->nParts );
744 bSupp = Cudd_Support( dd, pVars[v]->bParts ); Cudd_Ref( bSupp );
745 Bbr_bddPrint( dd, bSupp ); printf( "\n" );
746 Cudd_RecursiveDeref( dd, bSupp );
747}
748*/
749 pVar = pVars[iVarBest];
750
751 // this var cannot appear in one partition only
752 nSupp = Cudd_SupportSize( dd, pVar->bParts );
753 assert( nSupp == pVar->nParts );
754 assert( nSupp != 1 );
755//printf( "var = %d supp = %d\n\n", iVarBest, nSupp );
756
757 // if it appears in only two partitions, quantify it
758 if ( pVar->nParts == 2 )
759 {
760 // get the nodes
761 iNode1 = pVar->bParts->index;
762 iNode2 = cuddT(pVar->bParts)->index;
763 pNode1 = pNodes[iNode1];
764 pNode2 = pNodes[iNode2];
765
766 // get the quantification cube
767 bCube = dd->vars[pVar->iNum]; Cudd_Ref( bCube );
768 // add the variables that appear only in these partitions
769 for ( v = 0; v < nVars; v++ )
770 if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts )
771 {
772 // add this var
773 bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] ); Cudd_Ref( bCube );
774 Cudd_RecursiveDeref( dd, bTemp );
775 // clean this var
776 Cudd_RecursiveDeref( dd, pVars[v]->bParts );
777 ABC_FREE( pVars[v] );
778 }
779 // clean the best var
780 Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
781 ABC_FREE( pVars[iVarBest] );
782
783 // combines two nodes
784 pNode = Bbr_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
785 Cudd_RecursiveDeref( dd, bCube );
786 }
787 else // if ( pVar->nParts > 2 )
788 {
789 // find two smallest BDDs that have this var
790 Bbr_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
791 pNode1 = pNodes[iNode1];
792 pNode2 = pNodes[iNode2];
793//printf( "smallest bdds with this var: %d %d\n", iNode1, iNode2 );
794/*
795 // it is not possible that a var appears only in these two
796 // otherwise, it would have a different cost
797 bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts );
798 for ( v = 0; v < nVars; v++ )
799 if ( pVars[v] && pVars[v]->bParts == bParts )
800 assert( 0 );
801 Cudd_RecursiveDeref( dd, bParts );
802*/
803 // combines two nodes
804 pNode = Bbr_CombineTwoNodes( dd, b1, pNode1, pNode2 );
805 }
806
807 // clean the old nodes
808 pNodes[iNode1] = pNode;
809 pNodes[iNode2] = NULL;
810//printf( "Removing node %d (leaving node %d)\n", iNode2, iNode1 );
811
812 // update the variables that appear in pNode[iNode2]
813 for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
814 {
815 pVar = pVars[bSuppTemp->index];
816 if ( pVar == NULL ) // this variable is not be quantified
817 continue;
818 // quantify this var
819 assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) );
820 pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts );
821 Cudd_RecursiveDeref( dd, bTemp );
822 // add the new var
823 pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts );
824 Cudd_RecursiveDeref( dd, bTemp );
825 // update the score
826 pVar->nParts = Cudd_SupportSize( dd, pVar->bParts );
827 }
828
829 *pfStop = 0;
830 if ( dd->keys-dd->dead > (unsigned)nBddMax )
831 {
832 *pfStop = 1;
833 return 0;
834 }
835 return 1;
836}
837
838
850Bbr_ImageNode_t * Bbr_MergeTopNodes(
851 DdManager * dd, int nNodes, Bbr_ImageNode_t ** pNodes )
852{
853 Bbr_ImageNode_t * pNode;
854 int n1 = -1, n2 = -1, n;
855
856 // find the first and the second non-empty spots
857 for ( n = 0; n < nNodes; n++ )
858 if ( pNodes[n] )
859 {
860 if ( n1 == -1 )
861 n1 = n;
862 else if ( n2 == -1 )
863 {
864 n2 = n;
865 break;
866 }
867 }
868 assert( n1 != -1 );
869 // check the situation when only one such node is detected
870 if ( n2 == -1 )
871 {
872 // save the node
873 pNode = pNodes[n1];
874 // clean the node
875 pNodes[n1] = NULL;
876 return pNode;
877 }
878
879 // combines two nodes
880 pNode = Bbr_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] );
881
882 // clean the old nodes
883 pNodes[n1] = pNode;
884 pNodes[n2] = NULL;
885 return NULL;
886}
887
899Bbr_ImageNode_t * Bbr_CombineTwoNodes( DdManager * dd, DdNode * bCube,
900 Bbr_ImageNode_t * pNode1, Bbr_ImageNode_t * pNode2 )
901{
902 Bbr_ImageNode_t * pNode;
903 Bbr_ImagePart_t * pPart;
904
905 // create a new partition
906 pPart = ABC_ALLOC( Bbr_ImagePart_t, 1 );
907 memset( pPart, 0, sizeof(Bbr_ImagePart_t) );
908 // create the function
909 pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
910 Cudd_Ref( pPart->bFunc );
911 // update the support the partition
912 pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube );
913 Cudd_Ref( pPart->bSupp );
914 // update the numbers
915 pPart->nSupp = Cudd_SupportSize( dd, pPart->bSupp );
916 pPart->nNodes = Cudd_DagSize( pPart->bFunc );
917 pPart->iPart = -1;
918/*
919ABC_PRB( dd, pNode1->pPart->bSupp );
920ABC_PRB( dd, pNode2->pPart->bSupp );
921ABC_PRB( dd, pPart->bSupp );
922*/
923 // create a new node
924 pNode = ABC_ALLOC( Bbr_ImageNode_t, 1 );
925 memset( pNode, 0, sizeof(Bbr_ImageNode_t) );
926 pNode->dd = dd;
927 pNode->pPart = pPart;
928 pNode->pNode1 = pNode1;
929 pNode->pNode2 = pNode2;
930 // compute the image
931 pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube );
932 Cudd_Ref( pNode->bImage );
933 // save the cube
934 if ( bCube != b1 )
935 {
936 pNode->bCube = bCube; Cudd_Ref( bCube );
937 }
938 return pNode;
939}
940
953int Bbr_FindBestVariable( DdManager * dd,
954 int nNodes, Bbr_ImageNode_t ** pNodes,
955 int nVars, Bbr_ImageVar_t ** pVars )
956{
957 DdNode * bTemp;
958 int iVarBest, v;
959 double CostBest, CostCur;
960
961 CostBest = 100000000000000.0;
962 iVarBest = -1;
963
964 // check if there are two-variable partitions
965 for ( v = 0; v < nVars; v++ )
966 if ( pVars[v] && pVars[v]->nParts == 2 )
967 {
968 CostCur = 0;
969 for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
970 CostCur += pNodes[bTemp->index]->pPart->nNodes *
971 pNodes[bTemp->index]->pPart->nNodes;
972 if ( CostBest > CostCur )
973 {
974 CostBest = CostCur;
975 iVarBest = v;
976 }
977 }
978 if ( iVarBest >= 0 )
979 return iVarBest;
980
981 // find other partition
982 for ( v = 0; v < nVars; v++ )
983 if ( pVars[v] )
984 {
985 assert( pVars[v]->nParts > 1 );
986 CostCur = 0;
987 for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
988 CostCur += pNodes[bTemp->index]->pPart->nNodes *
989 pNodes[bTemp->index]->pPart->nNodes;
990 if ( CostBest > CostCur )
991 {
992 CostBest = CostCur;
993 iVarBest = v;
994 }
995 }
996 return iVarBest;
997}
998
1010void Bbr_FindBestPartitions( DdManager * dd, DdNode * bParts,
1011 int nNodes, Bbr_ImageNode_t ** pNodes,
1012 int * piNode1, int * piNode2 )
1013{
1014 DdNode * bTemp;
1015 int iPart1, iPart2;
1016 int CostMin1, CostMin2, Cost;
1017
1018 // go through the partitions
1019 iPart1 = iPart2 = -1;
1020 CostMin1 = CostMin2 = 1000000;
1021 for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) )
1022 {
1023 Cost = pNodes[bTemp->index]->pPart->nNodes;
1024 if ( CostMin1 > Cost )
1025 {
1026 CostMin2 = CostMin1; iPart2 = iPart1;
1027 CostMin1 = Cost; iPart1 = bTemp->index;
1028 }
1029 else if ( CostMin2 > Cost )
1030 {
1031 CostMin2 = Cost; iPart2 = bTemp->index;
1032 }
1033 }
1034
1035 *piNode1 = iPart1;
1036 *piNode2 = iPart2;
1037}
1038
1050void Bbr_bddImagePrintLatchDependency(
1051 DdManager * dd, DdNode * bCare, // the care set
1052 int nParts, DdNode ** pbParts, // the partitions for image computation
1053 int nVars, DdNode ** pbVars ) // the NS and parameter variables (not quantified!)
1054{
1055 int i;
1056 DdNode * bVarsCs, * bVarsNs;
1057
1058 bVarsCs = Cudd_Support( dd, bCare ); Cudd_Ref( bVarsCs );
1059 bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars ); Cudd_Ref( bVarsNs );
1060
1061 printf( "The latch dependency matrix:\n" );
1062 printf( "Partitions = %d Variables: total = %d non-quantifiable = %d\n",
1063 nParts, dd->size, nVars );
1064 printf( " : " );
1065 for ( i = 0; i < dd->size; i++ )
1066 printf( "%d", i % 10 );
1067 printf( "\n" );
1068
1069 for ( i = 0; i < nParts; i++ )
1070 Bbr_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
1071 Bbr_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts );
1072
1073 Cudd_RecursiveDeref( dd, bVarsCs );
1074 Cudd_RecursiveDeref( dd, bVarsNs );
1075}
1076
1088void Bbr_bddImagePrintLatchDependencyOne(
1089 DdManager * dd, DdNode * bFunc, // the function
1090 DdNode * bVarsCs, DdNode * bVarsNs, // the current/next state vars
1091 int iPart )
1092{
1093 DdNode * bSupport;
1094 int v;
1095 bSupport = Cudd_Support( dd, bFunc ); Cudd_Ref( bSupport );
1096 printf( " %3d : ", iPart );
1097 for ( v = 0; v < dd->size; v++ )
1098 {
1099 if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) )
1100 {
1101 if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) )
1102 printf( "c" );
1103 else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) )
1104 printf( "n" );
1105 else
1106 printf( "i" );
1107 }
1108 else
1109 printf( "." );
1110 }
1111 printf( "\n" );
1112 Cudd_RecursiveDeref( dd, bSupport );
1113}
1114
1115
1127void Bbr_bddImagePrintTree( Bbr_ImageTree_t * pTree )
1128{
1129 printf( "The quantification scheduling tree:\n" );
1130 Bbr_bddImagePrintTree_rec( pTree->pRoot, 1 );
1131}
1132
1144void Bbr_bddImagePrintTree_rec( Bbr_ImageNode_t * pNode, int Offset )
1145{
1146 DdNode * Cube;
1147 int i;
1148
1149 Cube = pNode->bCube;
1150
1151 if ( pNode->pNode1 == NULL )
1152 {
1153 printf( "<%d> ", pNode->pPart->iPart );
1154 if ( Cube != NULL )
1155 {
1156 ABC_PRB( pNode->dd, Cube );
1157 }
1158 else
1159 printf( "\n" );
1160 return;
1161 }
1162
1163 printf( "<*> " );
1164 if ( Cube != NULL )
1165 {
1166 ABC_PRB( pNode->dd, Cube );
1167 }
1168 else
1169 printf( "\n" );
1170
1171 for ( i = 0; i < Offset; i++ )
1172 printf( " " );
1173 Bbr_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );
1174
1175 for ( i = 0; i < Offset; i++ )
1176 printf( " " );
1177 Bbr_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
1178}
1179
1191DdNode * Bbr_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
1192{
1193 DdNode * bRes;
1194 DdNode * bTemp;
1195 int i;
1196
1197 bRes = b1; Cudd_Ref( bRes );
1198 for ( i = 0; i < nVars; i++ )
1199 {
1200 bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] ); Cudd_Ref( bRes );
1201 Cudd_RecursiveDeref( dd, bTemp );
1202 }
1203
1204 Cudd_Deref( bRes );
1205 return bRes;
1206}
1207
1208
1209
1210
1211
1212struct Bbr_ImageTree2_t_
1213{
1214 DdManager * dd;
1215 DdNode * bRel;
1216 DdNode * bCube;
1217 DdNode * bImage;
1218};
1219
1231Bbr_ImageTree2_t * Bbr_bddImageStart2(
1232 DdManager * dd, DdNode * bCare,
1233 int nParts, DdNode ** pbParts,
1234 int nVars, DdNode ** pbVars, int fVerbose )
1235{
1236 Bbr_ImageTree2_t * pTree;
1237 DdNode * bCubeAll, * bCubeNot, * bTemp;
1238 int i;
1239
1240 pTree = ABC_ALLOC( Bbr_ImageTree2_t, 1 );
1241 pTree->dd = dd;
1242 pTree->bImage = NULL;
1243
1244 bCubeAll = Bbr_bddComputeCube( dd, dd->vars, dd->size ); Cudd_Ref( bCubeAll );
1245 bCubeNot = Bbr_bddComputeCube( dd, pbVars, nVars ); Cudd_Ref( bCubeNot );
1246 pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
1247 Cudd_RecursiveDeref( dd, bCubeAll );
1248 Cudd_RecursiveDeref( dd, bCubeNot );
1249
1250 // derive the monolithic relation
1251 pTree->bRel = b1; Cudd_Ref( pTree->bRel );
1252 for ( i = 0; i < nParts; i++ )
1253 {
1254 pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
1255 Cudd_RecursiveDeref( dd, bTemp );
1256 }
1257 Bbr_bddImageCompute2( pTree, bCare );
1258 return pTree;
1259}
1260
1261
1273DdNode * Bbr_bddImageCompute2( Bbr_ImageTree2_t * pTree, DdNode * bCare )
1274{
1275 if ( pTree->bImage )
1276 Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
1277 pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube );
1278 Cudd_Ref( pTree->bImage );
1279 return pTree->bImage;
1280}
1281
1293void Bbr_bddImageTreeDelete2( Bbr_ImageTree2_t * pTree )
1294{
1295 if ( pTree->bRel )
1296 Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
1297 if ( pTree->bCube )
1298 Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
1299 if ( pTree->bImage )
1300 Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
1301 ABC_FREE( pTree );
1302}
1303
1315DdNode * Bbr_bddImageRead2( Bbr_ImageTree2_t * pTree )
1316{
1317 return pTree->bImage;
1318}
1319
1320
1324
1325
1326ABC_NAMESPACE_IMPL_END
1327
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Bbr_bddImageTreeDelete
void Bbr_bddImageTreeDelete(Bbr_ImageTree_t *pTree)
Definition bbrImage.c:307
Bbr_bddImageCompute2
DdNode * Bbr_bddImageCompute2(Bbr_ImageTree2_t *pTree, DdNode *bCare)
Definition bbrImage.c:1273
b0
#define b0
Definition bbrImage.c:96
Bbr_bddImageTreeDelete2
void Bbr_bddImageTreeDelete2(Bbr_ImageTree2_t *pTree)
Definition bbrImage.c:1293
Bbr_bddImageRead2
DdNode * Bbr_bddImageRead2(Bbr_ImageTree2_t *pTree)
Definition bbrImage.c:1315
Bbr_bddImageStart
Bbr_ImageTree_t * Bbr_bddImageStart(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int nBddMax, int fVerbose)
Definition bbrImage.c:168
b1
#define b1
Definition bbrImage.c:97
Bbr_ImageVar_t
struct Bbr_ImageVar_t_ Bbr_ImageVar_t
Definition bbrImage.c:44
Bbr_bddImageCompute
DdNode * Bbr_bddImageCompute(Bbr_ImageTree_t *pTree, DdNode *bCare)
Definition bbrImage.c:253
Bbr_bddImageRead
DdNode * Bbr_bddImageRead(Bbr_ImageTree_t *pTree)
Definition bbrImage.c:326
Bbr_bddImageStart2
Bbr_ImageTree2_t * Bbr_bddImageStart2(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
Definition bbrImage.c:1231
Bbr_ImageNode_t
typedefABC_NAMESPACE_IMPL_START struct Bbr_ImageNode_t_ Bbr_ImageNode_t
Definition bbrImage.c:42
Bbr_bddComputeCube
DdNode * Bbr_bddComputeCube(DdManager *dd, DdNode **bXVars, int nVars)
Definition bbrImage.c:1191
Bbr_ImagePart_t
struct Bbr_ImagePart_t_ Bbr_ImagePart_t
Definition bbrImage.c:43
ABC_PRB
#define ABC_PRB(dd, f)
Definition bbrImage.c:100
Bbr_ImageTree2_t
struct Bbr_ImageTree2_t_ Bbr_ImageTree2_t
Definition bbr.h:66
Bbr_ImageTree_t
struct Bbr_ImageTree_t_ Bbr_ImageTree_t
FUNCTION DECLARATIONS ///.
Definition bbr.h:58
p
Cube * p
Definition exorList.c:222
Cube
struct cube Cube
Bbr_ImageNode_t_
Definition bbrImage.c:59
Bbr_ImageNode_t_::pNode2
Bbr_ImageNode_t * pNode2
Definition bbrImage.c:64
Bbr_ImageNode_t_::pPart
Bbr_ImagePart_t * pPart
Definition bbrImage.c:65
Bbr_ImageNode_t_::bCube
DdNode * bCube
Definition bbrImage.c:61
Bbr_ImageNode_t_::dd
DdManager * dd
Definition bbrImage.c:60
Bbr_ImageNode_t_::bImage
DdNode * bImage
Definition bbrImage.c:62
Bbr_ImageNode_t_::pNode1
Bbr_ImageNode_t * pNode1
Definition bbrImage.c:63
Bbr_ImagePart_t_
Definition bbrImage.c:69
Bbr_ImagePart_t_::iPart
short iPart
Definition bbrImage.c:74
Bbr_ImagePart_t_::nSupp
short nSupp
Definition bbrImage.c:73
Bbr_ImagePart_t_::bFunc
DdNode * bFunc
Definition bbrImage.c:70
Bbr_ImagePart_t_::nNodes
int nNodes
Definition bbrImage.c:72
Bbr_ImagePart_t_::bSupp
DdNode * bSupp
Definition bbrImage.c:71
Bbr_ImageTree2_t_
Definition bbrImage.c:1213
Bbr_ImageTree2_t_::dd
DdManager * dd
Definition bbrImage.c:1214
Bbr_ImageTree2_t_::bRel
DdNode * bRel
Definition bbrImage.c:1215
Bbr_ImageTree2_t_::bCube
DdNode * bCube
Definition bbrImage.c:1216
Bbr_ImageTree2_t_::bImage
DdNode * bImage
Definition bbrImage.c:1217
Bbr_ImageTree_t_
Definition bbrImage.c:47
Bbr_ImageTree_t_::nNodesMaxT
int nNodesMaxT
Definition bbrImage.c:53
Bbr_ImageTree_t_::pRoot
Bbr_ImageNode_t * pRoot
Definition bbrImage.c:48
Bbr_ImageTree_t_::nNodesMax
int nNodesMax
Definition bbrImage.c:52
Bbr_ImageTree_t_::bCareSupp
DdNode * bCareSupp
Definition bbrImage.c:50
Bbr_ImageTree_t_::pCare
Bbr_ImageNode_t * pCare
Definition bbrImage.c:49
Bbr_ImageTree_t_::fVerbose
int fVerbose
Definition bbrImage.c:51
Bbr_ImageTree_t_::nBddMax
int nBddMax
Definition bbrImage.c:55
Bbr_ImageTree_t_::nIter
int nIter
Definition bbrImage.c:54
Bbr_ImageVar_t_
Definition bbrImage.c:78
Bbr_ImageVar_t_::bParts
DdNode * bParts
Definition bbrImage.c:80
Bbr_ImageVar_t_::nParts
int nParts
Definition bbrImage.c:81
Bbr_ImageVar_t_::iNum
int iNum
Definition bbrImage.c:79
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()