1 /**CFile***********************************************************************
7 Synopsis [A very simple reachability analysis program.]
13 Author [Fabio Somenzi]
15 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
19 Redistribution and use in source and binary forms, with or without
20 modification, are permitted provided that the following conditions
23 Redistributions of source code must retain the above copyright
24 notice, this list of conditions and the following disclaimer.
26 Redistributions in binary form must reproduce the above copyright
27 notice, this list of conditions and the following disclaimer in the
28 documentation and/or other materials provided with the distribution.
30 Neither the name of the University of Colorado nor the names of its
31 contributors may be used to endorse or promote products derived from
32 this software without specific prior written permission.
34 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
35 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
36 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
37 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
38 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
39 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
40 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
41 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
42 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
43 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
44 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
45 POSSIBILITY OF SUCH DAMAGE.]
47 ******************************************************************************/
51 /*---------------------------------------------------------------------------*/
52 /* Constant declarations */
53 /*---------------------------------------------------------------------------*/
55 #define NTR_MAX_DEP_SIZE 20
57 /*---------------------------------------------------------------------------*/
58 /* Stucture declarations */
59 /*---------------------------------------------------------------------------*/
61 /*---------------------------------------------------------------------------*/
62 /* Type declarations */
63 /*---------------------------------------------------------------------------*/
65 /*---------------------------------------------------------------------------*/
66 /* Variable declarations */
67 /*---------------------------------------------------------------------------*/
70 static char rcsid
[] UTIL_UNUSED
= "$Id: ntr.c,v 1.27 2009/02/21 06:00:31 fabio Exp fabio $";
73 static const char *onames
[] = { "T", "R" }; /* names of functions to be dumped */
74 static double *signatures
; /* signatures for all variables */
75 static BnetNetwork
*staticNet
; /* pointer to network used by qsort
76 ** comparison function */
77 static DdNode
**staticPart
; /* pointer to parts used by qsort
78 ** comparison function */
80 /*---------------------------------------------------------------------------*/
81 /* Macro declarations */
82 /*---------------------------------------------------------------------------*/
84 /**AutomaticStart*************************************************************/
86 /*---------------------------------------------------------------------------*/
87 /* Static function prototypes */
88 /*---------------------------------------------------------------------------*/
90 static DdNode
* makecube (DdManager
*dd
, DdNode
**x
, int n
);
91 static void ntrInitializeCount (BnetNetwork
*net
, NtrOptions
*option
);
92 static void ntrCountDFS (BnetNetwork
*net
, BnetNode
*node
);
93 static DdNode
* ntrImage (DdManager
*dd
, NtrPartTR
*TR
, DdNode
*from
, NtrOptions
*option
);
94 static DdNode
* ntrPreimage (DdManager
*dd
, NtrPartTR
*T
, DdNode
*from
);
95 static DdNode
* ntrChooseFrom (DdManager
*dd
, DdNode
*neW
, DdNode
*reached
, NtrOptions
*option
);
96 static DdNode
* ntrUpdateReached (DdManager
*dd
, DdNode
*oldreached
, DdNode
*to
);
97 static int ntrLatchDependencies (DdManager
*dd
, DdNode
*reached
, BnetNetwork
*net
, NtrOptions
*option
);
98 static NtrPartTR
* ntrEliminateDependencies (DdManager
*dd
, NtrPartTR
*TR
, DdNode
**states
, NtrOptions
*option
);
99 static int ntrUpdateQuantificationSchedule (DdManager
*dd
, NtrPartTR
*T
);
100 static int ntrSignatureCompare (int * ptrX
, int * ptrY
);
101 static int ntrSignatureCompare2 (int * ptrX
, int * ptrY
);
102 static int ntrPartCompare (int * ptrX
, int * ptrY
);
103 static char ** ntrAllocMatrix (int nrows
, int ncols
);
104 static void ntrFreeMatrix (char **matrix
);
105 static void ntrPermuteParts (DdNode
**a
, DdNode
**b
, int *comesFrom
, int *goesTo
, int size
);
107 /**AutomaticEnd***************************************************************/
109 /*---------------------------------------------------------------------------*/
110 /* Definition of exported functions */
111 /*---------------------------------------------------------------------------*/
114 /**Function********************************************************************
116 Synopsis [Builds DDs for a network outputs and next state
119 Description [Builds DDs for a network outputs and next state
120 functions. The method is really brain-dead, but it is very simple.
121 Returns 1 in case of success; 0 otherwise. Some inputs to the network
122 may be shared with another network whose DDs have already been built.
123 In this case we want to share the DDs as well.]
125 SideEffects [the dd fields of the network nodes are modified. Uses the
126 count fields of the nodes.]
130 ******************************************************************************/
133 BnetNetwork
* net
/* network for which DDs are to be built */,
134 DdManager
* dd
/* DD manager */,
135 NtrOptions
* option
/* option structure */,
136 BnetNetwork
* net2
/* companion network with which inputs may be shared */)
138 int pr
= option
->verb
;
141 BnetNode
*node
, *node2
;
143 /* If some inputs or present state variables are shared with
144 ** another network, we initialize their BDDs from that network.
147 for (i
= 0; i
< net
->npis
; i
++) {
148 if (!st_lookup(net
->hash
,net
->inputs
[i
],&node
)) {
151 if (!st_lookup(net2
->hash
,net
->inputs
[i
],&node2
)) {
152 /* This input is not shared. */
153 result
= Bnet_BuildNodeBDD(dd
,node
,net
->hash
,
154 option
->locGlob
,option
->nodrop
);
155 if (result
== 0) return(0);
157 if (node2
->dd
== NULL
) return(0);
158 node
->dd
= node2
->dd
;
160 node
->var
= node2
->var
;
161 node
->active
= node2
->active
;
164 for (i
= 0; i
< net
->nlatches
; i
++) {
165 if (!st_lookup(net
->hash
,net
->latches
[i
][1],&node
)) {
168 if (!st_lookup(net2
->hash
,net
->latches
[i
][1],&node2
)) {
169 /* This present state variable is not shared. */
170 result
= Bnet_BuildNodeBDD(dd
,node
,net
->hash
,
171 option
->locGlob
,option
->nodrop
);
172 if (result
== 0) return(0);
174 if (node2
->dd
== NULL
) return(0);
175 node
->dd
= node2
->dd
;
177 node
->var
= node2
->var
;
178 node
->active
= node2
->active
;
182 /* First assign variables to inputs if the order is provided.
183 ** (Either in the .blif file or in an order file.)
185 if (option
->ordering
== PI_PS_FROM_FILE
) {
186 /* Follow order given in input file. First primary inputs
187 ** and then present state variables.
189 for (i
= 0; i
< net
->npis
; i
++) {
190 if (!st_lookup(net
->hash
,net
->inputs
[i
],&node
)) {
193 result
= Bnet_BuildNodeBDD(dd
,node
,net
->hash
,
194 option
->locGlob
,option
->nodrop
);
195 if (result
== 0) return(0);
197 for (i
= 0; i
< net
->nlatches
; i
++) {
198 if (!st_lookup(net
->hash
,net
->latches
[i
][1],&node
)) {
201 result
= Bnet_BuildNodeBDD(dd
,node
,net
->hash
,
202 option
->locGlob
,option
->nodrop
);
203 if (result
== 0) return(0);
205 } else if (option
->ordering
== PI_PS_GIVEN
) {
206 result
= Bnet_ReadOrder(dd
,option
->orderPiPs
,net
,option
->locGlob
,
208 if (result
== 0) return(0);
210 result
= Bnet_DfsVariableOrder(dd
,net
);
211 if (result
== 0) return(0);
214 /* At this point the BDDs of all primary inputs and present state
215 ** variables have been built. */
217 /* Currently noBuild doesn't do much. */
218 if (option
->noBuild
== TRUE
)
221 if (option
->locGlob
== BNET_LOCAL_DD
) {
223 while (node
!= NULL
) {
224 result
= Bnet_BuildNodeBDD(dd
,node
,net
->hash
,BNET_LOCAL_DD
,TRUE
);
229 (void) fprintf(stdout
,"%s",node
->name
);
230 Cudd_PrintDebug(dd
,node
->dd
,Cudd_ReadSize(dd
),pr
);
234 } else { /* option->locGlob == BNET_GLOBAL_DD */
235 /* Create BDDs with DFS from the primary outputs and the next
236 ** state functions. If the inputs had not been ordered yet,
237 ** this would result in a DFS order for the variables.
240 ntrInitializeCount(net
,option
);
242 if (option
->node
!= NULL
&&
243 option
->closestCube
== FALSE
&& option
->dontcares
== FALSE
) {
244 if (!st_lookup(net
->hash
,option
->node
,&node
)) {
247 result
= Bnet_BuildNodeBDD(dd
,node
,net
->hash
,BNET_GLOBAL_DD
,
249 if (result
== 0) return(0);
251 if (option
->stateOnly
== FALSE
) {
252 for (i
= 0; i
< net
->npos
; i
++) {
253 if (!st_lookup(net
->hash
,net
->outputs
[i
],&node
)) {
256 result
= Bnet_BuildNodeBDD(dd
,node
,net
->hash
,
257 BNET_GLOBAL_DD
,option
->nodrop
);
258 if (result
== 0) return(0);
259 if (option
->progress
) {
260 (void) fprintf(stdout
,"%s\n",node
->name
);
263 Cudd_PrintDebug(dd
,node
->dd
,net
->ninputs
,option
->verb
);
267 for (i
= 0; i
< net
->nlatches
; i
++) {
268 if (!st_lookup(net
->hash
,net
->latches
[i
][0],&node
)) {
271 result
= Bnet_BuildNodeBDD(dd
,node
,net
->hash
,BNET_GLOBAL_DD
,
273 if (result
== 0) return(0);
274 if (option
->progress
) {
275 (void) fprintf(stdout
,"%s\n",node
->name
);
278 Cudd_PrintDebug(dd
,node
->dd
,net
->ninputs
,option
->verb
);
282 /* Make sure all inputs have a DD and dereference the DDs of
283 ** the nodes that are not reachable from the outputs.
285 for (i
= 0; i
< net
->npis
; i
++) {
286 if (!st_lookup(net
->hash
,net
->inputs
[i
],&node
)) {
289 result
= Bnet_BuildNodeBDD(dd
,node
,net
->hash
,BNET_GLOBAL_DD
,
291 if (result
== 0) return(0);
292 if (node
->count
== -1) Cudd_RecursiveDeref(dd
,node
->dd
);
294 for (i
= 0; i
< net
->nlatches
; i
++) {
295 if (!st_lookup(net
->hash
,net
->latches
[i
][1],&node
)) {
298 result
= Bnet_BuildNodeBDD(dd
,node
,net
->hash
,BNET_GLOBAL_DD
,
300 if (result
== 0) return(0);
301 if (node
->count
== -1) Cudd_RecursiveDeref(dd
,node
->dd
);
304 /* Dispose of the BDDs of the internal nodes if they have not
305 ** been dropped already.
307 if (option
->nodrop
== TRUE
) {
308 for (node
= net
->nodes
; node
!= NULL
; node
= node
->next
) {
309 if (node
->dd
!= NULL
&& node
->count
!= -1 &&
310 (node
->type
== BNET_INTERNAL_NODE
||
311 node
->type
== BNET_INPUT_NODE
||
312 node
->type
== BNET_PRESENT_STATE_NODE
)) {
313 Cudd_RecursiveDeref(dd
,node
->dd
);
314 if (node
->type
== BNET_INTERNAL_NODE
) node
->dd
= NULL
;
322 } /* end of buildDD */
325 /**Function********************************************************************
327 Synopsis [Builds the transition relation for a network.]
329 Description [Builds the transition relation for a network. Returns a
330 pointer to the transition relation structure if successful; NULL
337 ******************************************************************************/
340 DdManager
* dd
/* manager */,
341 BnetNetwork
* net
/* network */,
342 NtrOptions
* option
/* options */,
343 int image
/* image type: monolithic ... */)
346 DdNode
*T
, *delta
, *support
, *scan
, *tmp
, *preiabs
, *prepabs
;
347 DdNode
**part
, **absicubes
, **abspcubes
, **nscube
, *mnscube
;
356 /* Initialize transition relation structure. */
357 TR
= ALLOC(NtrPartTR
,1);
358 if (TR
== NULL
) goto endgame
;
359 TR
->nlatches
= net
->nlatches
;
360 if (image
== NTR_IMAGE_MONO
) {
362 } else if (image
== NTR_IMAGE_PART
|| image
== NTR_IMAGE_CLIP
||
363 image
== NTR_IMAGE_DEPEND
) {
364 TR
->nparts
= net
->nlatches
;
366 (void) fprintf(stderr
,"Unrecognized image method (%d). Using part.\n",
368 TR
->nparts
= net
->nlatches
;
370 TR
->factors
= Ntr_InitHeap(TR
->nlatches
);
371 if (TR
->factors
== NULL
) goto endgame
;
372 /* Allocate arrays for present state and next state variables. */
373 TR
->x
= x
= ALLOC(DdNode
*,TR
->nlatches
);
374 if (x
== NULL
) goto endgame
;
375 TR
->y
= y
= ALLOC(DdNode
*,TR
->nlatches
);
376 if (y
== NULL
) goto endgame
;
377 /* Allocate array for primary input variables. */
378 pi
= ALLOC(DdNode
*,net
->npis
);
379 if (pi
== NULL
) goto endgame
;
380 /* Allocate array for partitioned transition relation. */
381 part
= ALLOC(DdNode
*,net
->nlatches
);
382 if (part
== NULL
) goto endgame
;
383 /* Allocate array of next state cubes. */
384 nscube
= ALLOC(DdNode
*,net
->nlatches
);
385 if (nscube
== NULL
) goto endgame
;
386 /* Allocate array for quantification schedule and initialize it. */
387 schedule
= ALLOC(int,Cudd_ReadSize(dd
));
388 if (schedule
== NULL
) goto endgame
;
389 for (i
= 0; i
< Cudd_ReadSize(dd
); i
++) {
393 /* Create partitioned transition relation from network. */
394 TR
->xw
= Cudd_ReadOne(dd
);
396 for (i
= 0; i
< net
->nlatches
; i
++) {
397 if (!st_lookup(net
->hash
,net
->latches
[i
][1],&node
)) {
402 /* Add present state variable to cube TR->xw. */
403 tmp
= Cudd_bddAnd(dd
,TR
->xw
,x
[i
]);
404 if (tmp
== NULL
) return(NULL
); Cudd_Ref(tmp
);
405 Cudd_RecursiveDeref(dd
,TR
->xw
);
407 /* Create new y variable immediately above the x variable. */
408 xlevel
= Cudd_ReadPerm(dd
,x
[i
]->index
);
409 y
[i
] = Cudd_bddNewVarAtLevel(dd
,xlevel
);
411 /* Initialize cube of next state variables for this part. */
414 /* Group present and next state variable if so requested. */
415 if (option
->groupnsps
!= NTR_GROUP_NONE
) {
416 int method
= option
->groupnsps
== NTR_GROUP_DEFAULT
?
417 MTR_DEFAULT
: MTR_FIXED
;
418 if (Cudd_MakeTreeNode(dd
,y
[i
]->index
,2,method
) == NULL
)
421 /* Get next state function and create transition relation part. */
422 if (!st_lookup(net
->hash
,net
->latches
[i
][0],&node
)) {
426 if (image
!= NTR_IMAGE_DEPEND
) {
427 part
[i
] = Cudd_bddXnor(dd
,delta
,y
[i
]);
428 if (part
[i
] == NULL
) goto endgame
;
433 /* Collect scheduling info for this delta. At the end of this loop
434 ** schedule[i] == j means that the variable of index i does not
435 ** appear in any part with index greater than j, unless j == -1,
436 ** in which case the variable appears in no part.
438 support
= Cudd_Support(dd
,delta
);
441 while (!Cudd_IsConstant(scan
)) {
442 schedule
[scan
->index
] = i
;
445 Cudd_RecursiveDeref(dd
,support
);
448 /* Collect primary inputs. */
449 for (i
= 0; i
< net
->npis
; i
++) {
450 if (!st_lookup(net
->hash
,net
->inputs
[i
],&node
)) {
454 tmp
= Cudd_bddAnd(dd
,TR
->xw
,pi
[i
]);
455 if (tmp
== NULL
) goto endgame
; Cudd_Ref(tmp
);
456 Cudd_RecursiveDeref(dd
,TR
->xw
);
460 /* Build abstraction cubes. First primary input variables that go
461 ** in the abstraction cubes for both monolithic and partitioned
462 ** transition relations. */
463 absicubes
= ALLOC(DdNode
*, net
->nlatches
);
464 if (absicubes
== NULL
) goto endgame
;
465 abspcubes
= ALLOC(DdNode
*, net
->nlatches
);
466 if (abspcubes
== NULL
) goto endgame
;
468 for (i
= 0; i
< net
->nlatches
; i
++) {
469 absicubes
[i
] = Cudd_ReadOne(dd
);
470 Cudd_Ref(absicubes
[i
]);
472 preiabs
= Cudd_ReadOne(dd
);
475 for (i
= 0; i
< net
->npis
; i
++) {
476 int j
= pi
[i
]->index
;
479 tmp
= Cudd_bddAnd(dd
,absicubes
[k
],pi
[i
]);
480 if (tmp
== NULL
) return(NULL
); Cudd_Ref(tmp
);
481 Cudd_RecursiveDeref(dd
,absicubes
[k
]);
484 tmp
= Cudd_bddAnd(dd
,preiabs
,pi
[i
]);
485 if (tmp
== NULL
) return(NULL
); Cudd_Ref(tmp
);
486 Cudd_RecursiveDeref(dd
,preiabs
);
492 /* Build preimage abstraction cubes from image abstraction cubes. */
493 for (i
= 0; i
< net
->nlatches
; i
++) {
494 abspcubes
[i
] = Cudd_bddAnd(dd
,absicubes
[i
],nscube
[i
]);
495 if (abspcubes
[i
] == NULL
) return(NULL
);
496 Cudd_Ref(abspcubes
[i
]);
498 Cudd_Ref(prepabs
= preiabs
);
500 /* For partitioned transition relations we add present state variables
501 ** to the image abstraction cubes. */
502 if (image
!= NTR_IMAGE_MONO
) {
503 for (i
= 0; i
< net
->nlatches
; i
++) {
507 tmp
= Cudd_bddAnd(dd
,absicubes
[k
],x
[i
]);
508 if (tmp
== NULL
) return(NULL
); Cudd_Ref(tmp
);
509 Cudd_RecursiveDeref(dd
,absicubes
[k
]);
512 tmp
= Cudd_bddAnd(dd
,preiabs
,x
[i
]);
513 if (tmp
== NULL
) return(NULL
); Cudd_Ref(tmp
);
514 Cudd_RecursiveDeref(dd
,preiabs
);
521 if (image
!= NTR_IMAGE_MONO
) {
523 TR
->icube
= absicubes
;
524 TR
->pcube
= abspcubes
;
526 TR
->preiabs
= preiabs
;
527 TR
->prepabs
= prepabs
;
531 /* Here we are building a monolithic TR. */
533 /* Reinitialize the cube of variables to be quantified before
534 ** image computation. */
535 Cudd_RecursiveDeref(dd
,preiabs
);
536 preiabs
= Cudd_ReadOne(dd
);
539 if (option
->imageClip
!= 1.0) {
540 depth
= (int) ((double) Cudd_ReadSize(dd
) * option
->imageClip
);
543 /* Collapse transition relation. */
544 T
= Cudd_ReadOne(dd
);
546 mnscube
= Cudd_ReadOne(dd
);
548 for (i
= 0; i
< net
->nlatches
; i
++) {
549 /* Eliminate the primary inputs that do not appear in other parts. */
551 tmp
= Cudd_bddClippingAndAbstract(dd
,T
,part
[i
],absicubes
[i
],
552 depth
,option
->approx
);
554 tmp
= Cudd_bddAndAbstract(dd
,T
,part
[i
],absicubes
[i
]);
557 Cudd_RecursiveDeref(dd
,T
);
558 Cudd_RecursiveDeref(dd
,part
[i
]);
559 Cudd_RecursiveDeref(dd
,absicubes
[i
]);
560 Cudd_RecursiveDeref(dd
,abspcubes
[i
]);
561 if (option
->threshold
>= 0) {
562 if (option
->approx
) {
563 T
= Cudd_RemapOverApprox(dd
,tmp
,2*net
->nlatches
,
564 option
->threshold
,option
->quality
);
566 T
= Cudd_RemapUnderApprox(dd
,tmp
,2*net
->nlatches
,
567 option
->threshold
,option
->quality
);
572 if (T
== NULL
) return(NULL
);
574 Cudd_RecursiveDeref(dd
,tmp
);
575 /* Add the next state variables of this part to the cube of all
576 ** next state variables. */
577 tmp
= Cudd_bddAnd(dd
,mnscube
,nscube
[i
]);
578 if (tmp
== NULL
) return(NULL
);
580 Cudd_RecursiveDeref(dd
,mnscube
);
582 Cudd_RecursiveDeref(dd
,nscube
[i
]);
583 (void) printf("@"); fflush(stdout
);
587 (void) printf("T"); Cudd_PrintDebug(dd
,T
,2*net
->nlatches
,2);
596 TR
->part
= part
= ALLOC(DdNode
*,1);
597 if (part
== NULL
) goto endgame
;
600 /* Build cube of x (present state) variables for abstraction. */
601 TR
->icube
= absicubes
= ALLOC(DdNode
*,1);
602 if (absicubes
== NULL
) goto endgame
;
603 absicubes
[0] = makecube(dd
,x
,TR
->nlatches
);
604 if (absicubes
[0] == NULL
) return(0);
605 Cudd_Ref(absicubes
[0]);
606 /* Build cube of y (next state) variables for abstraction. */
607 TR
->pcube
= abspcubes
= ALLOC(DdNode
*,1);
608 if (abspcubes
== NULL
) goto endgame
;
609 abspcubes
[0] = makecube(dd
,y
,TR
->nlatches
);
610 if (abspcubes
[0] == NULL
) return(0);
611 Cudd_Ref(abspcubes
[0]);
612 TR
->preiabs
= preiabs
;
613 TR
->prepabs
= prepabs
;
615 TR
->nscube
= ALLOC(DdNode
*,1);
616 if (TR
->nscube
== NULL
) return(NULL
);
617 TR
->nscube
[0] = mnscube
;
625 } /* end of Ntr_buildTR */
628 /**Function********************************************************************
630 Synopsis [Frees the transition relation for a network.]
638 ******************************************************************************/
645 for (i
= 0; i
< TR
->nlatches
; i
++) {
646 Cudd_RecursiveDeref(dd
,TR
->x
[i
]);
647 Cudd_RecursiveDeref(dd
,TR
->y
[i
]);
651 for (i
= 0; i
< TR
->nparts
; i
++) {
652 Cudd_RecursiveDeref(dd
,TR
->part
[i
]);
653 Cudd_RecursiveDeref(dd
,TR
->icube
[i
]);
654 Cudd_RecursiveDeref(dd
,TR
->pcube
[i
]);
655 Cudd_RecursiveDeref(dd
,TR
->nscube
[i
]);
661 Cudd_RecursiveDeref(dd
,TR
->preiabs
);
662 Cudd_RecursiveDeref(dd
,TR
->prepabs
);
663 Cudd_RecursiveDeref(dd
,TR
->xw
);
664 for (i
= 0; i
< TR
->factors
->nslots
; i
++) {
665 Cudd_RecursiveDeref(dd
, (DdNode
*) TR
->factors
->slots
[i
].item
);
667 Ntr_FreeHeap(TR
->factors
);
672 } /* end of Ntr_freeTR */
675 /**Function********************************************************************
677 Synopsis [Makes a copy of a transition relation.]
679 Description [Makes a copy of a transition relation. Returns a pointer
680 to the copy if successful; NULL otherwise.]
684 SeeAlso [Ntr_buildTR Ntr_freeTR]
686 ******************************************************************************/
692 int nparts
, nlatches
, i
;
694 T
= ALLOC(NtrPartTR
,1);
695 if (T
== NULL
) return(NULL
);
696 nparts
= T
->nparts
= TR
->nparts
;
697 nlatches
= T
->nlatches
= TR
->nlatches
;
698 T
->part
= ALLOC(DdNode
*,nparts
);
699 if (T
->part
== NULL
) {
703 T
->icube
= ALLOC(DdNode
*,nparts
);
704 if (T
->icube
== NULL
) {
709 T
->pcube
= ALLOC(DdNode
*,nparts
);
710 if (T
->pcube
== NULL
) {
716 T
->x
= ALLOC(DdNode
*,nlatches
);
724 T
->y
= ALLOC(DdNode
*,nlatches
);
733 T
->nscube
= ALLOC(DdNode
*,nparts
);
734 if (T
->nscube
== NULL
) {
743 T
->factors
= Ntr_HeapClone(TR
->factors
);
744 if (T
->factors
== NULL
) {
754 for (i
= 0; i
< T
->factors
->nslots
; i
++) {
755 Cudd_Ref((DdNode
*) T
->factors
->slots
[i
].item
);
757 for (i
= 0; i
< nparts
; i
++) {
758 T
->part
[i
] = TR
->part
[i
];
759 Cudd_Ref(T
->part
[i
]);
760 T
->icube
[i
] = TR
->icube
[i
];
761 Cudd_Ref(T
->icube
[i
]);
762 T
->pcube
[i
] = TR
->pcube
[i
];
763 Cudd_Ref(T
->pcube
[i
]);
764 T
->nscube
[i
] = TR
->nscube
[i
];
765 Cudd_Ref(T
->nscube
[i
]);
767 T
->preiabs
= TR
->preiabs
;
768 Cudd_Ref(T
->preiabs
);
769 T
->prepabs
= TR
->prepabs
;
770 Cudd_Ref(T
->prepabs
);
773 for (i
= 0; i
< nlatches
; i
++) {
782 } /* end of Ntr_cloneTR */
785 /**Function********************************************************************
787 Synopsis [Poor man's traversal procedure.]
789 Description [Poor man's traversal procedure. based on the monolithic
790 transition relation. Returns 1 in case of success; 0 otherwise.]
794 SeeAlso [Ntr_ClosureTrav]
796 ******************************************************************************/
799 DdManager
* dd
/* DD manager */,
800 BnetNetwork
* net
/* network */,
801 NtrOptions
* option
/* options */)
803 NtrPartTR
*TR
; /* Transition relation */
804 DdNode
*init
; /* initial state(s) */
812 int pr
= option
->verb
;
813 int initReord
= Cudd_ReadReorderings(dd
);
815 if (option
->traverse
== FALSE
|| net
->nlatches
== 0) return(1);
816 (void) printf("Building transition relation. Time = %s\n",
817 util_print_time(util_cpu_time() - option
->initialTime
));
818 one
= Cudd_ReadOne(dd
);
819 zero
= Cudd_Not(one
);
821 /* Build transition relation and initial states. */
822 TR
= Ntr_buildTR(dd
,net
,option
,option
->image
);
823 if (TR
== NULL
) return(0);
824 retval
= Cudd_SetVarMap(dd
,TR
->x
,TR
->y
,TR
->nlatches
);
825 (void) printf("Transition relation: %d parts %d latches %d nodes\n",
826 TR
->nparts
, TR
->nlatches
,
827 Cudd_SharingSize(TR
->part
, TR
->nparts
));
828 (void) printf("Traversing. Time = %s\n",
829 util_print_time(util_cpu_time() - option
->initialTime
));
830 init
= Ntr_initState(dd
,net
,option
);
831 if (init
== NULL
) return(0);
833 /* Initialize From. */
834 Cudd_Ref(from
= init
);
835 (void) printf("S0"); Cudd_PrintDebug(dd
,from
,TR
->nlatches
,pr
);
837 /* Initialize Reached. */
838 Cudd_Ref(reached
= from
);
840 /* Start traversal. */
841 for (depth
= 0; ; depth
++) {
842 /* Image computation. */
843 to
= ntrImage(dd
,TR
,from
,option
);
845 Cudd_RecursiveDeref(dd
,reached
);
846 Cudd_RecursiveDeref(dd
,from
);
849 Cudd_RecursiveDeref(dd
,from
);
851 /* Find new states. */
852 neW
= Cudd_bddAnd(dd
,to
,Cudd_Not(reached
));
854 Cudd_RecursiveDeref(dd
,reached
);
855 Cudd_RecursiveDeref(dd
,to
);
859 Cudd_RecursiveDeref(dd
,to
);
861 /* Check for convergence. */
862 if (neW
== zero
) break;
864 /* Dump current reached states if requested. */
865 if (option
->store
== depth
) {
866 int ok
= Dddmp_cuddBddStore(dd
, NULL
, reached
, NULL
,
867 NULL
, DDDMP_MODE_TEXT
, DDDMP_VARIDS
,
868 option
->storefile
, NULL
);
869 if (ok
== 0) return(0);
870 (void) printf("Storing reached in %s after %i iterations.\n",
871 option
->storefile
, depth
);
875 /* Update reached. */
876 reached
= ntrUpdateReached(dd
,reached
,neW
);
877 if (reached
== NULL
) {
878 Cudd_RecursiveDeref(dd
,neW
);
882 /* Prepare for new iteration. */
883 from
= ntrChooseFrom(dd
,neW
,reached
,option
);
885 Cudd_RecursiveDeref(dd
,reached
);
886 Cudd_RecursiveDeref(dd
,neW
);
889 Cudd_RecursiveDeref(dd
,neW
);
890 (void) printf("From[%d]",depth
+1);
891 Cudd_PrintDebug(dd
,from
,TR
->nlatches
,pr
);
892 (void) printf("Reached[%d]",depth
+1);
893 Cudd_PrintDebug(dd
,reached
,TR
->nlatches
,pr
);
895 if (!Cudd_ApaPrintMinterm(stdout
, dd
, reached
, TR
->nlatches
))
897 if (!Cudd_ApaPrintMintermExp(stdout
, dd
, reached
, TR
->nlatches
, 6))
904 /* Print out result. */
905 (void) printf("depth = %d\n", depth
);
906 (void) printf("R"); Cudd_PrintDebug(dd
,reached
,TR
->nlatches
,pr
);
908 /* Dump to file if requested. */
909 if (option
->bdddump
) {
910 DdNode
*dfunc
[2]; /* addresses of the functions to be dumped */
911 char *onames
[2]; /* names of the functions to be dumped */
912 dfunc
[0] = TR
->part
[0]; onames
[0] = (char *) "T";
913 dfunc
[1] = reached
; onames
[1] = (char *) "R";
914 retval
= Bnet_bddArrayDump(dd
, net
, option
->dumpfile
, dfunc
,
915 onames
, 2, option
->dumpFmt
);
916 if (retval
== 0) return(0);
919 if (option
->depend
) {
920 retval
= ntrLatchDependencies(dd
, reached
, net
, option
);
921 if (retval
== -1) return(0);
922 (void) printf("%d latches are redundant\n", retval
);
925 Cudd_RecursiveDeref(dd
,reached
);
926 Cudd_RecursiveDeref(dd
,neW
);
927 Cudd_RecursiveDeref(dd
,init
);
930 if (Cudd_ReadReorderings(dd
) > initReord
) {
931 (void) printf("Order at the end of reachability analysis\n");
932 retval
= Bnet_PrintOrder(net
,dd
);
933 if (retval
== 0) return(0);
937 } /* end of Ntr_Trav */
940 /**Function********************************************************************
942 Synopsis [Computes the SCCs of the STG.]
944 Description [Computes the strongly connected components of the state
945 transition graph. Only the first 10 SCCs are computed. Returns 1 in
946 case of success; 0 otherwise.]
952 ******************************************************************************/
955 DdManager
* dd
/* DD manager */,
956 BnetNetwork
* net
/* network */,
957 NtrOptions
* option
/* options */)
959 NtrPartTR
*TR
; /* Transition relation */
960 DdNode
*init
; /* initial state(s) */
963 DdNode
*reached
, *reaching
;
966 DdNode
*states
, *scc
;
972 int pr
= option
->verb
;
975 if (option
->scc
== FALSE
|| net
->nlatches
== 0) return(1);
976 (void) printf("Building transition relation. Time = %s\n",
977 util_print_time(util_cpu_time() - option
->initialTime
));
978 one
= Cudd_ReadOne(dd
);
979 zero
= Cudd_Not(one
);
981 /* Build transition relation and initial states. */
982 TR
= Ntr_buildTR(dd
,net
,option
,option
->image
);
983 if (TR
== NULL
) return(0);
984 retval
= Cudd_SetVarMap(dd
,TR
->x
,TR
->y
,TR
->nlatches
);
985 (void) printf("Transition relation: %d parts %d latches %d nodes\n",
986 TR
->nparts
, TR
->nlatches
,
987 Cudd_SharingSize(TR
->part
, TR
->nparts
));
988 (void) printf("Computing SCCs. Time = %s\n",
989 util_print_time(util_cpu_time() - option
->initialTime
));
991 /* Consider all SCCs, including those not reachable. */
995 while (states
!= zero
) {
997 tmp
= Ntr_initState(dd
,net
,option
);
998 if (tmp
== NULL
) return(0);
999 init
= Cudd_bddPickOneMinterm(dd
,tmp
,TR
->x
,TR
->nlatches
);
1001 init
= Cudd_bddPickOneMinterm(dd
,states
,TR
->x
,TR
->nlatches
);
1003 if (init
== NULL
) return(0);
1006 Cudd_RecursiveDeref(dd
,tmp
);
1008 /* Initialize From. */
1009 Cudd_Ref(from
= init
);
1010 (void) printf("S0"); Cudd_PrintDebug(dd
,from
,TR
->nlatches
,pr
);
1012 /* Initialize Reached. */
1013 Cudd_Ref(reached
= from
);
1015 /* Start forward traversal. */
1016 for (depth
= 0; ; depth
++) {
1017 /* Image computation. */
1018 to
= ntrImage(dd
,TR
,from
,option
);
1022 Cudd_RecursiveDeref(dd
,from
);
1024 /* Find new states. */
1025 tmp
= Cudd_bddAnd(dd
,to
,states
);
1026 if (tmp
== NULL
) return(0); Cudd_Ref(tmp
);
1027 Cudd_RecursiveDeref(dd
,to
);
1028 neW
= Cudd_bddAnd(dd
,tmp
,Cudd_Not(reached
));
1029 if (neW
== NULL
) return(0); Cudd_Ref(neW
);
1030 Cudd_RecursiveDeref(dd
,tmp
);
1032 /* Check for convergence. */
1033 if (neW
== zero
) break;
1035 /* Update reached. */
1036 reached
= ntrUpdateReached(dd
,reached
,neW
);
1037 if (reached
== NULL
) {
1041 /* Prepare for new iteration. */
1042 from
= ntrChooseFrom(dd
,neW
,reached
,option
);
1046 Cudd_RecursiveDeref(dd
,neW
);
1047 (void) printf("From[%d]",depth
+1);
1048 Cudd_PrintDebug(dd
,from
,TR
->nlatches
,pr
);
1049 (void) printf("Reached[%d]",depth
+1);
1050 Cudd_PrintDebug(dd
,reached
,TR
->nlatches
,pr
);
1052 (void) printf("\n");
1055 Cudd_RecursiveDeref(dd
,neW
);
1057 /* Express reached in terms of y variables. This allows us to
1058 ** efficiently test for termination during the backward traversal. */
1059 tmp
= Cudd_bddVarMap(dd
,reached
);
1060 if (tmp
== NULL
) return(0);
1062 Cudd_RecursiveDeref(dd
,reached
);
1065 /* Initialize from and reaching. */
1066 from
= Cudd_bddVarMap(dd
,init
);
1068 (void) printf("S0"); Cudd_PrintDebug(dd
,from
,TR
->nlatches
,pr
);
1069 Cudd_Ref(reaching
= from
);
1071 /* Start backward traversal. */
1072 for (depth
= 0; ; depth
++) {
1073 /* Preimage computation. */
1074 to
= ntrPreimage(dd
,TR
,from
);
1078 Cudd_RecursiveDeref(dd
,from
);
1080 /* Find new states. */
1081 tmp
= Cudd_bddAnd(dd
,to
,reached
);
1082 if (tmp
== NULL
) return(0); Cudd_Ref(tmp
);
1083 Cudd_RecursiveDeref(dd
,to
);
1084 neW
= Cudd_bddAnd(dd
,tmp
,Cudd_Not(reaching
));
1085 if (neW
== NULL
) return(0); Cudd_Ref(neW
);
1086 Cudd_RecursiveDeref(dd
,tmp
);
1088 /* Check for convergence. */
1089 if (neW
== zero
) break;
1091 /* Update reaching. */
1092 reaching
= ntrUpdateReached(dd
,reaching
,neW
);
1093 if (reaching
== NULL
) {
1097 /* Prepare for new iteration. */
1098 from
= ntrChooseFrom(dd
,neW
,reaching
,option
);
1102 Cudd_RecursiveDeref(dd
,neW
);
1103 (void) printf("From[%d]",depth
+1);
1104 Cudd_PrintDebug(dd
,from
,TR
->nlatches
,pr
);
1105 (void) printf("Reaching[%d]",depth
+1);
1106 Cudd_PrintDebug(dd
,reaching
,TR
->nlatches
,pr
);
1108 (void) printf("\n");
1112 scc
= Cudd_bddAnd(dd
,reached
,reaching
);
1117 SCCs
[nscc
] = Cudd_bddVarMap(dd
,scc
);
1118 if (SCCs
[nscc
] == NULL
) return(0);
1119 Cudd_Ref(SCCs
[nscc
]);
1120 Cudd_RecursiveDeref(dd
,scc
);
1121 /* Print out result. */
1122 (void) printf("SCC[%d]",nscc
);
1123 Cudd_PrintDebug(dd
,SCCs
[nscc
],TR
->nlatches
,pr
);
1124 tmp
= Cudd_bddAnd(dd
,states
,Cudd_Not(SCCs
[nscc
]));
1129 Cudd_RecursiveDeref(dd
,states
);
1131 Cudd_RecursiveDeref(dd
,reached
);
1132 Cudd_RecursiveDeref(dd
,reaching
);
1133 Cudd_RecursiveDeref(dd
,neW
);
1134 Cudd_RecursiveDeref(dd
,init
);
1136 if (nscc
> 9) break;
1139 if (states
!= zero
) {
1140 (void) fprintf(stdout
,"More than 10 SCCs. Only the first 10 are computed.\n");
1143 /* Dump to file if requested. */
1144 if (option
->bdddump
) {
1145 char *sccnames
[10]; /* names of the SCCs */
1146 sccnames
[0] = (char *) "SCC0";
1147 sccnames
[1] = (char *) "SCC1";
1148 sccnames
[2] = (char *) "SCC2";
1149 sccnames
[3] = (char *) "SCC3";
1150 sccnames
[4] = (char *) "SCC4";
1151 sccnames
[5] = (char *) "SCC5";
1152 sccnames
[6] = (char *) "SCC6";
1153 sccnames
[7] = (char *) "SCC7";
1154 sccnames
[8] = (char *) "SCC8";
1155 sccnames
[9] = (char *) "SCC9";
1156 retval
= Bnet_bddArrayDump(dd
, net
, option
->dumpfile
, SCCs
,
1157 sccnames
, nscc
, option
->dumpFmt
);
1158 if (retval
== 0) return(0);
1161 /* Verify that the SCCs form a partition of the universe. */
1164 for (i
= 0; i
< nscc
; i
++) {
1165 assert(Cudd_bddLeq(dd
,SCCs
[i
],Cudd_Not(scc
)));
1166 tmp
= Cudd_bddOr(dd
,SCCs
[i
],scc
);
1167 if (tmp
== NULL
) return(0);
1169 Cudd_RecursiveDeref(dd
,scc
);
1171 Cudd_RecursiveDeref(dd
,SCCs
[i
]);
1173 assert(scc
== Cudd_Not(states
));
1176 Cudd_RecursiveDeref(dd
,scc
);
1177 Cudd_RecursiveDeref(dd
,states
);
1182 } /* end of Ntr_SCC */
1185 /**Function********************************************************************
1187 Synopsis [Transitive closure traversal procedure.]
1189 Description [Traversal procedure. based on the transitive closure of the
1190 transition relation. Returns 1 in case of success; 0 otherwise.]
1196 ******************************************************************************/
1199 DdManager
* dd
/* DD manager */,
1200 BnetNetwork
* net
/* network */,
1201 NtrOptions
* option
/* options */)
1207 int pr
= option
->verb
; /* verbosity level */
1208 DdNode
*dfunc
[2]; /* addresses of the functions to be dumped */
1209 char *onames
[2]; /* names of the functions to be dumped */
1210 DdNode
*reached
, *reachedy
, *reachedx
;
1212 /* Traverse if requested and if the circuit is sequential. */
1213 if (option
->closure
== FALSE
|| net
->nlatches
== 0) return(1);
1215 TR
= Ntr_buildTR(dd
,net
,option
,NTR_IMAGE_MONO
);
1216 if (TR
== NULL
) return(0);
1217 (void) printf("TR"); Cudd_PrintDebug(dd
,TR
->part
[0],2*TR
->nlatches
,pr
);
1218 T
= Ntr_TransitiveClosure(dd
,TR
,option
);
1219 if (T
== NULL
) return(0);
1221 (void) printf("TC"); Cudd_PrintDebug(dd
,T
,2*TR
->nlatches
,pr
);
1223 init
= Ntr_initState(dd
,net
,option
);
1224 if (init
== NULL
) return(0);
1225 (void) printf("S0"); Cudd_PrintDebug(dd
,init
,TR
->nlatches
,pr
);
1227 /* Image computation. */
1228 if (option
->closureClip
!= 1.0) {
1229 int depth
= (int) ((double) Cudd_ReadSize(dd
) * option
->closureClip
);
1230 reachedy
= Cudd_bddClippingAndAbstract(dd
,T
,init
,TR
->icube
[0],
1231 depth
,option
->approx
);
1233 reachedy
= Cudd_bddAndAbstract(dd
,T
,init
,TR
->icube
[0]);
1235 if (reachedy
== NULL
) return(0);
1238 /* Express in terms of present state variables. */
1239 reachedx
= Cudd_bddSwapVariables(dd
,reachedy
,TR
->x
,TR
->y
,TR
->nlatches
);
1240 if (reachedx
== NULL
) return(0);
1242 Cudd_RecursiveDeref(dd
,reachedy
);
1244 /* Add initial state. */
1245 reached
= Cudd_bddOr(dd
,reachedx
,init
);
1246 if (reached
== NULL
) return(0);
1248 Cudd_RecursiveDeref(dd
,reachedx
);
1250 /* Print out result. */
1251 (void) printf("R"); Cudd_PrintDebug(dd
,reached
,TR
->nlatches
,pr
);
1253 /* Dump to file if requested. */
1254 if (option
->bdddump
) {
1255 dfunc
[0] = T
; onames
[0] = (char *) "TC";
1256 dfunc
[1] = reached
; onames
[1] = (char *) "R";
1257 retval
= Bnet_bddArrayDump(dd
, net
, option
->dumpfile
, dfunc
,
1258 onames
, 2, option
->dumpFmt
);
1259 if (retval
== 0) return(0);
1263 Cudd_RecursiveDeref(dd
,reached
);
1264 Cudd_RecursiveDeref(dd
,init
);
1265 Cudd_RecursiveDeref(dd
,T
);
1270 } /* end of Ntr_ClosureTrav */
1273 /**Function********************************************************************
1275 Synopsis [Builds the transitive closure of a transition relation.]
1277 Description [Builds the transitive closure of a transition relation.
1278 Returns a BDD if successful; NULL otherwise. Uses a simple squaring
1285 ******************************************************************************/
1287 Ntr_TransitiveClosure(
1290 NtrOptions
* option
)
1292 DdNode
*T
,*oldT
,*Txz
,*Tzy
,*Tred
,*square
,*zcube
;
1299 if (option
->image
!= NTR_IMAGE_MONO
) return(NULL
);
1301 /* Create array of auxiliary variables. */
1302 z
= ALLOC(DdNode
*,TR
->nlatches
);
1305 for (i
= 0; i
< TR
->nlatches
; i
++) {
1306 ylevel
= Cudd_ReadIndex(dd
,TR
->y
[i
]->index
);
1307 z
[i
] = Cudd_bddNewVarAtLevel(dd
,ylevel
);
1311 /* Build cube of auxiliary variables. */
1312 zcube
= makecube(dd
,z
,TR
->nlatches
);
1313 if (zcube
== NULL
) return(NULL
);
1316 if (option
->closureClip
!= 1.0) {
1317 depth
= (int) ((double) Cudd_ReadSize(dd
) * option
->imageClip
);
1322 for (i
= 0; ; i
++) {
1323 if (option
->threshold
>= 0) {
1324 if (option
->approx
) {
1325 Tred
= Cudd_RemapOverApprox(dd
,T
,TR
->nlatches
*2,
1329 Tred
= Cudd_RemapUnderApprox(dd
,T
,TR
->nlatches
*2,
1336 if (Tred
== NULL
) return(NULL
);
1338 /* Express T in terms of z and y variables. */
1339 Tzy
= Cudd_bddSwapVariables(dd
,Tred
,TR
->x
,z
,TR
->nlatches
);
1340 if (Tzy
== NULL
) return(NULL
);
1342 /* Express T in terms of x and z variables. */
1343 Txz
= Cudd_bddSwapVariables(dd
,Tred
,TR
->y
,z
,TR
->nlatches
);
1344 if (Txz
== NULL
) return(NULL
);
1346 Cudd_RecursiveDeref(dd
,Tred
);
1349 square
= Cudd_bddAndAbstract(dd
,Txz
,Tzy
,zcube
);
1351 square
= Cudd_bddClippingAndAbstract(dd
,Txz
,Tzy
,zcube
,depth
,
1354 if (square
== NULL
) return(NULL
);
1356 Cudd_RecursiveDeref(dd
,Tzy
);
1357 Cudd_RecursiveDeref(dd
,Txz
);
1359 T
= Cudd_bddOr(dd
,square
,TR
->part
[0]);
1360 if (T
== NULL
) return(NULL
);
1362 Cudd_RecursiveDeref(dd
,square
);
1364 Cudd_RecursiveDeref(dd
,oldT
);
1366 (void) fprintf(stdout
,"@"); fflush(stdout
);
1368 (void) fprintf(stdout
, "\n");
1370 Cudd_RecursiveDeref(dd
,zcube
);
1375 } /* end of Ntr_TransitiveClosure */
1378 /**Function********************************************************************
1380 Synopsis [Builds the BDD of the initial state(s).]
1382 Description [Builds the BDD of the initial state(s). Returns a BDD
1383 if successful; NULL otherwise.]
1389 ******************************************************************************/
1394 NtrOptions
* option
)
1396 DdNode
*res
, *x
, *w
, *one
;
1401 res
= Dddmp_cuddBddLoad(dd
, DDDMP_VAR_MATCHIDS
, NULL
, NULL
, NULL
,
1402 DDDMP_MODE_DEFAULT
, option
->loadfile
, NULL
);
1404 one
= Cudd_ReadOne(dd
);
1405 Cudd_Ref(res
= one
);
1407 if (net
->nlatches
== 0) return(res
);
1409 for (i
= 0; i
< net
->nlatches
; i
++) {
1410 if (!st_lookup(net
->hash
,net
->latches
[i
][1],&node
)) {
1414 switch (net
->latches
[i
][2][0]) {
1416 w
= Cudd_bddAnd(dd
,res
,Cudd_Not(x
));
1419 w
= Cudd_bddAnd(dd
,res
,x
);
1421 default: /* don't care */
1427 Cudd_RecursiveDeref(dd
,res
);
1431 Cudd_RecursiveDeref(dd
,res
);
1441 } /* end of Ntr_initState */
1444 /**Function********************************************************************
1446 Synopsis [Reads a state cube from a file or creates a random one.]
1448 Description [Reads a state cube from a file or create a random one.
1449 Returns a pointer to the BDD of the sink nodes if successful; NULL
1456 *****************************************************************************/
1474 cube
= Cudd_ReadOne(dd
);
1475 if (net
->nlatches
== 0) {
1480 state
= ALLOC(char,net
->nlatches
+1);
1483 state
[net
->nlatches
] = 0;
1485 if (filename
== NULL
) {
1486 /* Pick one random minterm. */
1487 for (i
= 0; i
< net
->nlatches
; i
++) {
1488 state
[i
] = (char) ((Cudd_Random() & 0x2000) ? '1' : '0');
1491 if ((fp
= fopen(filename
,"r")) == NULL
) {
1492 (void) fprintf(stderr
,"Unable to open %s\n",filename
);
1496 /* Read string from file. Allow arbitrary amount of white space. */
1497 for (i
= 0; !feof(fp
); i
++) {
1498 err
= fscanf(fp
, "%1s", c
);
1500 if (err
== EOF
|| i
== net
->nlatches
- 1) {
1502 } else if (err
!= 1 || strchr("012xX-", c
[0]) == NULL
) {
1514 /* Echo the chosen state(s). */
1515 if (pr
> 0) {(void) fprintf(stdout
,"%s\n", state
);}
1518 for (i
= 0; i
< net
->nlatches
; i
++) {
1519 if (!st_lookup(net
->hash
,net
->latches
[i
][1],&node
)) {
1520 Cudd_RecursiveDeref(dd
,cube
);
1527 w
= Cudd_bddAnd(dd
,cube
,Cudd_Not(x
));
1530 w
= Cudd_bddAnd(dd
,cube
,x
);
1532 default: /* don't care */
1538 Cudd_RecursiveDeref(dd
,cube
);
1543 Cudd_RecursiveDeref(dd
,cube
);
1550 } /* end of Ntr_getStateCube */
1553 /**Function********************************************************************
1555 Synopsis [Poor man's outer envelope computation.]
1557 Description [ Poor man's outer envelope computation based on the
1558 monolithic transition relation. Returns 1 in case of success; 0
1565 ******************************************************************************/
1568 DdManager
* dd
/* DD manager */,
1569 NtrPartTR
* TR
/* transition relation */,
1570 FILE * dfp
/* pointer to file for DD dump */,
1571 NtrOptions
* option
/* program options */)
1573 DdNode
**x
; /* array of x variables */
1574 DdNode
**y
; /* array of y variables */
1575 int ns
; /* number of x and y variables */
1576 DdNode
*dfunc
[2]; /* addresses of the functions to be dumped */
1577 DdNode
*envelope
, *oldEnvelope
;
1581 int pr
= option
->verb
;
1582 int dumpFmt
= option
->dumpFmt
;
1588 one
= Cudd_ReadOne(dd
);
1589 retval
= Cudd_SetVarMap(dd
,x
,y
,ns
);
1591 /* Initialize From. */
1593 if (envelope
== NULL
) return(0);
1595 (void) printf("S0"); Cudd_PrintDebug(dd
,envelope
,ns
,pr
);
1597 /* Start traversal. */
1598 for (depth
= 0; ; depth
++) {
1599 oldEnvelope
= envelope
;
1600 /* Image computation. */
1601 envelope
= ntrImage(dd
,TR
,oldEnvelope
,option
);
1602 if (envelope
== NULL
) {
1603 Cudd_RecursiveDeref(dd
,oldEnvelope
);
1607 /* Check for convergence. */
1608 if (envelope
== oldEnvelope
) break;
1610 /* Prepare for new iteration. */
1611 Cudd_RecursiveDeref(dd
,oldEnvelope
);
1612 (void) fprintf(stdout
,"Envelope[%d]%s",depth
+1,(pr
>0)? "" : "\n");
1613 Cudd_PrintDebug(dd
,envelope
,ns
,pr
);
1617 Cudd_RecursiveDeref(dd
,oldEnvelope
);
1619 /* Print out result. */
1620 (void) printf("depth = %d\n", depth
);
1621 (void) printf("Envelope"); Cudd_PrintDebug(dd
,envelope
,ns
,pr
);
1623 /* Write dump file if requested. */
1625 dfunc
[0] = TR
->part
[0];
1626 dfunc
[1] = envelope
;
1628 retval
= Cudd_DumpBlif(dd
,2,dfunc
,NULL
,(char **)onames
,NULL
,dfp
,0);
1629 } else if (dumpFmt
== 2) {
1630 retval
= Cudd_DumpDaVinci(dd
,2,dfunc
,NULL
,(char **)onames
,dfp
);
1631 } else if (dumpFmt
== 3) {
1632 retval
= Cudd_DumpDDcal(dd
,2,dfunc
,NULL
,(char **)onames
,dfp
);
1633 } else if (dumpFmt
== 4) {
1634 retval
= Cudd_DumpFactoredForm(dd
,2,dfunc
,NULL
,
1635 (char **)onames
,dfp
);
1636 } else if (dumpFmt
== 5) {
1637 retval
= Cudd_DumpBlif(dd
,2,dfunc
,NULL
,(char **)onames
,NULL
,dfp
,1);
1639 retval
= Cudd_DumpDot(dd
,2,dfunc
,NULL
,(char **)onames
,dfp
);
1642 (void) fprintf(stderr
,"abnormal termination\n");
1649 Cudd_RecursiveDeref(dd
,envelope
);
1653 } /* end of Ntr_Envelope */
1656 /**Function********************************************************************
1658 Synopsis [Maximum 0-1 flow between source and sink states.]
1660 Description [Maximum 0-1 flow between source and sink
1661 states. Returns 1 in case of success; 0 otherwise.]
1663 SideEffects [Creates two new sets of variables.]
1667 ******************************************************************************/
1672 NtrOptions
* option
)
1693 TR
= Ntr_buildTR(dd
,net
,option
,NTR_IMAGE_MONO
);
1699 /* Create array of auxiliary variables. */
1700 z
= ALLOC(DdNode
*,n
);
1703 for (i
= 0; i
< n
; i
++) {
1704 ylevel
= Cudd_ReadIndex(dd
,y
[i
]->index
);
1705 z
[i
] = Cudd_bddNewVarAtLevel(dd
,ylevel
);
1710 /* Create BDDs for source and sink. */
1711 sx
= Ntr_initState(dd
,net
,option
);
1714 if (pr
> 0) (void) fprintf(stdout
, "Sink(s): ");
1715 tx
= Ntr_getStateCube(dd
,net
,option
->sinkfile
,pr
);
1718 ty
= Cudd_bddSwapVariables(dd
,tx
,x
,y
,n
);
1722 Cudd_RecursiveDeref(dd
,tx
);
1725 flow
= Ntr_maximum01Flow(dd
, sx
, ty
, E
, &F
, &cut
, x
, y
, z
, n
, pr
);
1729 (void) fprintf(stdout
,"Maximum flow = %g\n", flow
);
1730 (void) fprintf(stdout
,"E"); Cudd_PrintDebug(dd
,E
,2*n
,pr
);
1731 (void) fprintf(stdout
,"F"); Cudd_PrintDebug(dd
,F
,2*n
,pr
);
1732 (void) fprintf(stdout
,"cut"); Cudd_PrintDebug(dd
,cut
,2*n
,pr
);
1736 if (TR
!= NULL
) Ntr_freeTR(dd
,TR
);
1737 for (i
= 0; i
< n
; i
++) {
1738 if (z
!= NULL
&& z
[i
] != NULL
) Cudd_RecursiveDeref(dd
,z
[i
]);
1740 if (z
!= NULL
) FREE(z
);
1741 if (F
!= NULL
) Cudd_RecursiveDeref(dd
,F
);
1742 if (cut
!= NULL
) Cudd_RecursiveDeref(dd
,cut
);
1743 if (sx
!= NULL
) Cudd_RecursiveDeref(dd
,sx
);
1744 if (ty
!= NULL
) Cudd_RecursiveDeref(dd
,ty
);
1747 } /* end of Ntr_Maxflow */
1749 /*---------------------------------------------------------------------------*/
1750 /* Definition of internal functions */
1751 /*---------------------------------------------------------------------------*/
1753 /*---------------------------------------------------------------------------*/
1754 /* Definition of static functions */
1755 /*---------------------------------------------------------------------------*/
1758 /**Function********************************************************************
1760 Synopsis [Builds a positive cube of all the variables in x.]
1762 Description [Builds a positive cube of all the variables in x. Returns
1763 a BDD for the cube if successful; NULL otherwise.]
1769 ******************************************************************************/
1776 DdNode
*res
, *w
, *one
;
1779 one
= Cudd_ReadOne(dd
);
1780 Cudd_Ref(res
= one
);
1782 for (i
= n
-1; i
>= 0; i
--) {
1783 w
= Cudd_bddAnd(dd
,res
,x
[i
]);
1785 Cudd_RecursiveDeref(dd
,res
);
1789 Cudd_RecursiveDeref(dd
,res
);
1795 } /* end of makecube */
1798 /**Function********************************************************************
1800 Synopsis [Initializes the count fields used to drop DDs.]
1802 Description [Initializes the count fields used to drop DDs.
1803 Before actually building the BDDs, we perform a DFS from the outputs
1804 to initialize the count fields of the nodes. The initial value of the
1805 count field will normally coincide with the fanout of the node.
1806 However, if there are nodes with no path to any primary output or next
1807 state variable, then the initial value of count for some nodes will be
1808 less than the fanout. For primary outputs and next state functions we
1809 add 1, so that we will never try to free their DDs. The count fields
1810 of the nodes that are not reachable from the outputs are set to -1.]
1812 SideEffects [Changes the count fields of the network nodes. Uses the
1817 ******************************************************************************/
1821 NtrOptions
* option
)
1826 if (option
->node
!= NULL
&&
1827 option
->closestCube
== FALSE
&& option
->dontcares
== FALSE
) {
1828 if (!st_lookup(net
->hash
,option
->node
,&node
)) {
1829 (void) fprintf(stdout
, "Warning: node %s not found!\n",
1832 ntrCountDFS(net
,node
);
1836 if (option
->stateOnly
== FALSE
) {
1837 for (i
= 0; i
< net
->npos
; i
++) {
1838 if (!st_lookup(net
->hash
,net
->outputs
[i
],&node
)) {
1839 (void) fprintf(stdout
,
1840 "Warning: output %s is not driven!\n",
1844 ntrCountDFS(net
,node
);
1848 for (i
= 0; i
< net
->nlatches
; i
++) {
1849 if (!st_lookup(net
->hash
,net
->latches
[i
][0],&node
)) {
1850 (void) fprintf(stdout
,
1851 "Warning: latch input %s is not driven!\n",
1855 ntrCountDFS(net
,node
);
1860 /* Clear visited flags. */
1862 while (node
!= NULL
) {
1863 if (node
->visited
== 0) {
1871 } /* end of ntrInitializeCount */
1874 /**Function********************************************************************
1876 Synopsis [Does a DFS from a node setting the count field.]
1880 SideEffects [Changes the count and visited fields of the nodes it
1883 SeeAlso [ntrLevelDFS]
1885 ******************************************************************************/
1896 if (node
->visited
== 1) {
1902 for (i
= 0; i
< node
->ninp
; i
++) {
1903 if (!st_lookup(net
->hash
, node
->inputs
[i
], &auxnd
)) {
1906 ntrCountDFS(net
,auxnd
);
1909 } /* end of ntrCountDFS */
1912 /**Function********************************************************************
1914 Synopsis [Computes the image of a set given a transition relation.]
1916 Description [Computes the image of a set given a transition relation.
1917 Returns a pointer to the result if successful; NULL otherwise. The image is
1918 returned in terms of the present state variables; its reference count is
1925 ******************************************************************************/
1931 NtrOptions
* option
)
1939 if (option
->image
== NTR_IMAGE_CLIP
) {
1940 depth
= (int) ((double) Cudd_ReadSize(dd
) * option
->imageClip
);
1943 /* Existentially quantify the present state variables that are not
1944 ** in the support of any next state function. */
1945 image
= Cudd_bddExistAbstract(dd
,from
,TR
->preiabs
);
1946 if (image
== NULL
) return(NULL
);
1948 if (option
->image
== NTR_IMAGE_DEPEND
) {
1949 /* Simplify the transition relation based on dependencies
1950 ** and build the conjuncts from the deltas. */
1951 T
= ntrEliminateDependencies(dd
,TR
,&image
,option
);
1955 if (T
== NULL
) return(NULL
);
1956 for (i
= 0; i
< T
->nparts
; i
++) {
1958 (void) printf(" Intermediate product[%d]: %d nodes\n",
1959 i
,Cudd_DagSize(image
));
1961 if (option
->image
== NTR_IMAGE_CLIP
) {
1962 to
= Cudd_bddClippingAndAbstract(dd
,T
->part
[i
],image
,T
->icube
[i
],
1963 depth
,option
->approx
);
1965 to
= Cudd_bddAndAbstract(dd
,T
->part
[i
],image
,T
->icube
[i
]);
1967 if (to
== NULL
) return(NULL
);
1969 if (option
->image
== NTR_IMAGE_DEPEND
) {
1970 /* Extract dependencies from intermediate product. */
1971 DdNode
*abs
, *positive
, *absabs
, *phi
, *exnor
, *tmp
;
1972 abs
= Cudd_bddExistAbstract(dd
,to
,T
->xw
);
1973 if (abs
== NULL
) return(NULL
); Cudd_Ref(abs
);
1974 if (Cudd_bddVarIsDependent(dd
,abs
,T
->nscube
[i
]) &&
1975 Cudd_EstimateCofactor(dd
,abs
,T
->nscube
[i
]->index
,1) <=
1978 positive
= Cudd_Cofactor(dd
,abs
,T
->nscube
[i
]);
1979 if (positive
== NULL
) return(NULL
); Cudd_Ref(positive
);
1980 absabs
= Cudd_bddExistAbstract(dd
,abs
,T
->nscube
[i
]);
1981 if (absabs
== NULL
) return(NULL
); Cudd_Ref(absabs
);
1982 Cudd_RecursiveDeref(dd
,abs
);
1983 phi
= Cudd_bddLICompaction(dd
,positive
,absabs
);
1984 if (phi
== NULL
) return(NULL
); Cudd_Ref(phi
);
1985 Cudd_RecursiveDeref(dd
,positive
);
1986 Cudd_RecursiveDeref(dd
,absabs
);
1987 exnor
= Cudd_bddXnor(dd
,T
->nscube
[i
],phi
);
1988 if (exnor
== NULL
) return(NULL
); Cudd_Ref(exnor
);
1989 Cudd_RecursiveDeref(dd
,phi
);
1990 sizex
= Cudd_DagSize(exnor
);
1991 (void) printf("new factor of %d nodes\n", sizex
);
1992 retval
= Ntr_HeapInsert(T
->factors
,exnor
,sizex
);
1993 if (retval
== 0) return(NULL
);
1994 tmp
= Cudd_bddExistAbstract(dd
,to
,T
->nscube
[i
]);
1995 if (tmp
== NULL
) return(NULL
); Cudd_Ref(tmp
);
1996 Cudd_RecursiveDeref(dd
,to
);
1999 Cudd_RecursiveDeref(dd
,abs
);
2002 Cudd_RecursiveDeref(dd
,image
);
2005 if (option
->image
== NTR_IMAGE_DEPEND
) {
2007 DdNode
*factor1
, *factor2
, *tmp
;
2009 size1
= Cudd_DagSize(image
);
2010 retval
= Ntr_HeapInsert(T
->factors
,image
,size1
);
2011 if (retval
== 0) return(NULL
);
2012 (void) printf("Merging %d factors. Independent image: %d nodes\n",
2013 Ntr_HeapCount(T
->factors
), size1
);
2014 while (Ntr_HeapCount(T
->factors
) > 1) {
2015 retval
= Ntr_HeapExtractMin(T
->factors
,&factor1
,&size1
);
2016 if (retval
== 0) return(NULL
);
2017 retval
= Ntr_HeapExtractMin(T
->factors
,&factor2
,&size2
);
2018 if (retval
== 0) return(NULL
);
2019 tmp
= Cudd_bddAnd(dd
,factor1
,factor2
);
2020 if (tmp
== NULL
) return(NULL
); Cudd_Ref(tmp
);
2021 size1
= Cudd_DagSize(tmp
);
2022 (void) printf("new factor %d nodes\n", size1
);
2023 Cudd_RecursiveDeref(dd
,factor1
);
2024 Cudd_RecursiveDeref(dd
,factor2
);
2025 retval
= Ntr_HeapInsert(T
->factors
,tmp
,size1
);
2026 if (retval
== 0) return(NULL
);
2028 retval
= Ntr_HeapExtractMin(T
->factors
,&image
,&size1
);
2029 if (retval
== 0) return(NULL
);
2033 /* Express image in terms of x variables. */
2034 to
= Cudd_bddVarMap(dd
,image
);
2036 Cudd_RecursiveDeref(dd
,image
);
2040 Cudd_RecursiveDeref(dd
,image
);
2043 } /* end of ntrImage */
2046 /**Function********************************************************************
2048 Synopsis [Computes the preimage of a set given a transition relation.]
2050 Description [Computes the preimage of a set given a transition relation.
2051 Returns a pointer to the result if successful; NULL otherwise. The preimage
2052 is returned in terms of the next state variables; its reference count is
2057 SeeAlso [ntrImage Ntr_SCC]
2059 ******************************************************************************/
2070 /* Existentially quantify the present state variables that are not
2071 ** in the support of any next state function. */
2072 preimage
= Cudd_bddExistAbstract(dd
,from
,T
->prepabs
);
2073 if (preimage
== NULL
) return(NULL
);
2075 for (i
= 0; i
< T
->nparts
; i
++) {
2077 (void) printf(" Intermediate product[%d]: %d nodes\n",
2078 i
,Cudd_DagSize(preimage
));
2080 to
= Cudd_bddAndAbstract(dd
,T
->part
[i
],preimage
,T
->pcube
[i
]);
2081 if (to
== NULL
) return(NULL
);
2083 Cudd_RecursiveDeref(dd
,preimage
);
2087 /* Express preimage in terms of x variables. */
2088 to
= Cudd_bddVarMap(dd
,preimage
);
2090 Cudd_RecursiveDeref(dd
,preimage
);
2094 Cudd_RecursiveDeref(dd
,preimage
);
2097 } /* end of ntrPreimage */
2100 /**Function********************************************************************
2102 Synopsis [Chooses the initial states for a BFS step.]
2104 Description [Chooses the initial states for a BFS step. Returns a
2105 pointer to the chose set if successful; NULL otherwise. The
2106 reference count of the result is already incremented.]
2112 ******************************************************************************/
2118 NtrOptions
* option
)
2123 switch (option
->from
) {
2127 case NTR_FROM_REACHED
:
2130 case NTR_FROM_RESTRICT
:
2131 c
= Cudd_bddOr(dd
, neW
, Cudd_Not(reached
));
2132 if (c
== NULL
) return(NULL
);
2134 min
= Cudd_bddRestrict(dd
,neW
,c
);
2136 Cudd_RecursiveDeref(dd
, c
);
2140 Cudd_RecursiveDeref(dd
, c
);
2142 case NTR_FROM_COMPACT
:
2143 c
= Cudd_bddOr(dd
, neW
, Cudd_Not(reached
));
2144 if (c
== NULL
) return(NULL
);
2146 min
= Cudd_bddLICompaction(dd
,neW
,c
);
2148 Cudd_RecursiveDeref(dd
, c
);
2152 Cudd_RecursiveDeref(dd
, c
);
2154 case NTR_FROM_SQUEEZE
:
2155 min
= Cudd_bddSqueeze(dd
,neW
,reached
);
2156 if (min
== NULL
) return(NULL
);
2159 case NTR_FROM_UNDERAPPROX
:
2160 threshold
= (option
->threshold
< 0) ? 0 : option
->threshold
;
2161 min
= Cudd_RemapUnderApprox(dd
,neW
,Cudd_SupportSize(dd
,neW
),
2162 threshold
,option
->quality
);
2163 if (min
== NULL
) return(NULL
);
2166 case NTR_FROM_OVERAPPROX
:
2167 threshold
= (option
->threshold
< 0) ? 0 : option
->threshold
;
2168 min
= Cudd_RemapOverApprox(dd
,neW
,Cudd_SupportSize(dd
,neW
),
2169 threshold
,option
->quality
);
2170 if (min
== NULL
) return(NULL
);
2177 } /* end of ntrChooseFrom */
2180 /**Function********************************************************************
2182 Synopsis [Updates the reached states after a traversal step.]
2184 Description [Updates the reached states after a traversal
2185 step. Returns a pointer to the new reached set if successful; NULL
2186 otherwise. The reference count of the result is already incremented.]
2188 SideEffects [The old reached set is dereferenced.]
2192 ******************************************************************************/
2195 DdManager
* dd
/* manager */,
2196 DdNode
* oldreached
/* old reached state set */,
2197 DdNode
* to
/* result of last image computation */)
2201 reached
= Cudd_bddOr(dd
,oldreached
,to
);
2202 if (reached
== NULL
) {
2203 Cudd_RecursiveDeref(dd
,oldreached
);
2207 Cudd_RecursiveDeref(dd
,oldreached
);
2210 } /* end of ntrUpdateReached */
2213 /**Function********************************************************************
2215 Synopsis [Analyzes the reached states after traversal to find
2218 Description [Analyzes the reached states after traversal to find
2219 dependent latches. Returns the number of latches that can be
2220 eliminated because they are stuck at a constant value or are
2221 dependent on others if successful; -1 otherwise. The algorithm is
2222 greedy and determines a local optimum, not a global one.]
2228 ******************************************************************************/
2230 ntrLatchDependencies(
2237 int howMany
; /* number of latches that can be eliminated */
2238 DdNode
*var
, *newreached
, *abs
, *positive
, *phi
;
2241 int initVars
, finalVars
;
2242 double initStates
, finalStates
;
2245 int howManySmall
= 0;
2250 (void) printf("Analyzing latch dependencies\n");
2251 roots
= ALLOC(DdNode
*, net
->nlatches
);
2252 if (roots
== NULL
) return(-1);
2253 onames
= ALLOC(char *, net
->nlatches
);
2254 if (onames
== NULL
) return(-1);
2256 candidates
= ALLOC(int,net
->nlatches
);
2257 if (candidates
== NULL
) return(-1);
2258 for (i
= 0; i
< net
->nlatches
; i
++) {
2261 /* The signatures of the variables in a function are the number
2262 ** of minterms of the positive cofactors with respect to the
2263 ** variables themselves. */
2264 newreached
= reached
;
2265 Cudd_Ref(newreached
);
2266 signatures
= Cudd_CofMinterm(dd
,newreached
);
2267 if (signatures
== NULL
) return(-1);
2268 /* We now extract a positive quantity which is higher for those
2269 ** variables that are closer to being essential. */
2270 totalVars
= Cudd_ReadSize(dd
);
2271 minStates
= signatures
[totalVars
];
2273 (void) printf("Raw signatures (minStates = %g)\n", minStates
);
2274 for (i
= 0; i
< net
->nlatches
; i
++) {
2275 int j
= candidates
[i
];
2276 if (!st_lookup(net
->hash
,net
->latches
[j
][1],(char **) &node
)) {
2279 (void) printf("%s -> %g\n", node
->name
, signatures
[node
->dd
->index
]);
2282 for (i
= 0; i
< totalVars
; i
++) {
2283 double z
= signatures
[i
] / minStates
- 1.0;
2284 signatures
[i
] = (z
>= 0.0) ? z
: -z
; /* make positive */
2287 qsort((void *)candidates
,net
->nlatches
,sizeof(int),
2288 (DD_QSFP
)ntrSignatureCompare2
);
2290 (void) printf("Cooked signatures\n");
2291 for (i
= 0; i
< net
->nlatches
; i
++) {
2292 int j
= candidates
[i
];
2293 if (!st_lookup(net
->hash
,net
->latches
[j
][1],(char **) &node
)) {
2296 (void) printf("%s -> %g\n", node
->name
, signatures
[node
->dd
->index
]);
2301 /* Extract simple dependencies. */
2302 for (i
= 0; i
< net
->nlatches
; i
++) {
2303 int j
= candidates
[i
];
2304 if (!st_lookup(net
->hash
,net
->latches
[j
][1],&node
)) {
2309 if (Cudd_bddVarIsDependent(dd
,newreached
,var
)) {
2310 positive
= Cudd_Cofactor(dd
,newreached
,var
);
2311 if (positive
== NULL
) return(-1); Cudd_Ref(positive
);
2312 abs
= Cudd_bddExistAbstract(dd
,newreached
,var
);
2313 if (abs
== NULL
) return(-1); Cudd_Ref(abs
);
2314 phi
= Cudd_bddLICompaction(dd
,positive
,abs
);
2315 if (phi
== NULL
) return(-1); Cudd_Ref(phi
);
2316 Cudd_RecursiveDeref(dd
,positive
);
2317 if (Cudd_DagSize(phi
) < NTR_MAX_DEP_SIZE
) {
2318 if (Cudd_bddLeq(dd
,newreached
,var
)) {
2319 (void) printf("%s is stuck at 1\n",name
);
2320 } else if (Cudd_bddLeq(dd
,newreached
,Cudd_Not(var
))) {
2321 (void) printf("%s is stuck at 0\n",name
);
2323 (void) printf("%s depends on the other variables\n",name
);
2325 roots
[howManySmall
] = phi
;
2326 onames
[howManySmall
] = util_strsav(name
);
2327 Cudd_RecursiveDeref(dd
,newreached
);
2330 candidates
[i
] = -1; /* do not reconsider */
2332 Cudd_RecursiveDeref(dd
,abs
);
2333 Cudd_RecursiveDeref(dd
,phi
);
2336 candidates
[i
] = -1; /* do not reconsider */
2339 /* Now remove remaining dependent variables. */
2340 howMany
= howManySmall
;
2341 for (i
= 0; i
< net
->nlatches
; i
++) {
2342 int j
= candidates
[i
];
2343 if (j
== -1) continue;
2344 if (!st_lookup(net
->hash
,net
->latches
[j
][1],&node
)) {
2349 if (Cudd_bddVarIsDependent(dd
,newreached
,var
)) {
2350 if (Cudd_bddLeq(dd
,newreached
,var
)) {
2351 (void) printf("%s is stuck at 1\n",name
);
2352 } else if (Cudd_bddLeq(dd
,newreached
,Cudd_Not(var
))) {
2353 (void) printf("%s is stuck at 0\n",name
);
2355 (void) printf("%s depends on the other variables\n",name
);
2357 abs
= Cudd_bddExistAbstract(dd
,newreached
,var
);
2358 if (abs
== NULL
) return(-1); Cudd_Ref(abs
);
2359 Cudd_RecursiveDeref(dd
,newreached
);
2365 if (howManySmall
> 0) {
2366 if (!Bnet_bddArrayDump(dd
,net
,(char *)"-",roots
,onames
,howManySmall
,1))
2369 for (i
= 0; i
< howManySmall
; i
++) {
2370 Cudd_RecursiveDeref(dd
,roots
[i
]);
2376 initVars
= net
->nlatches
;
2377 initStates
= Cudd_CountMinterm(dd
,reached
,initVars
);
2378 finalVars
= initVars
- howMany
;
2379 finalStates
= Cudd_CountMinterm(dd
,newreached
,finalVars
);
2380 if (initStates
!= finalStates
) {
2381 (void) printf("Error: the number of states changed from %g to %g\n",
2382 initStates
, finalStates
);
2385 (void) printf("new reached");
2386 Cudd_PrintDebug(dd
,newreached
,finalVars
,option
->verb
);
2387 Cudd_RecursiveDeref(dd
,newreached
);
2390 } /* end of ntrLatchDependencies */
2393 /**Function********************************************************************
2395 Synopsis [Eliminates dependent variables from a transition relation.]
2397 Description [Eliminates dependent variables from a transition
2398 relation. Returns a simplified copy of the given transition
2399 relation if successful; NULL otherwise.]
2401 SideEffects [The modified set of states is returned as a side effect.]
2405 ******************************************************************************/
2407 ntrEliminateDependencies(
2413 NtrPartTR
*T
; /* new TR without dependent vars */
2414 int pr
= option
->verb
;
2416 int howMany
= 0; /* number of latches that can be eliminated */
2417 DdNode
*var
, *newstates
, *abs
, *positive
, *phi
;
2418 DdNode
*support
, *scan
, *tmp
;
2419 int finalSize
; /* size of the TR after substitutions */
2420 int nvars
; /* vars in the support of the state set */
2421 int *candidates
; /* vars to be considered for elimination */
2425 /* Initialize the new transition relation by copying the old one. */
2426 T
= Ntr_cloneTR(TR
);
2427 if (T
== NULL
) return(NULL
);
2428 newstates
= *states
;
2429 Cudd_Ref(newstates
);
2431 /* Find and rank the candidate variables. */
2432 support
= Cudd_Support(dd
,newstates
);
2433 if (support
== NULL
) {
2438 nvars
= Cudd_DagSize(support
) - 1;
2439 candidates
= ALLOC(int,nvars
);
2440 if (candidates
== NULL
) {
2441 Cudd_RecursiveDeref(dd
,support
);
2446 for (i
= 0; i
< nvars
; i
++) {
2447 candidates
[i
] = scan
->index
;
2448 scan
= Cudd_T(scan
);
2450 Cudd_RecursiveDeref(dd
,support
);
2451 /* The signatures of the variables in a function are the number
2452 ** of minterms of the positive cofactors with respect to the
2453 ** variables themselves. */
2454 signatures
= Cudd_CofMinterm(dd
,newstates
);
2455 if (signatures
== NULL
) {
2460 /* We now extract a positive quantity which is higher for those
2461 ** variables that are closer to being essential. */
2462 totalVars
= Cudd_ReadSize(dd
);
2463 minStates
= signatures
[totalVars
];
2464 for (i
= 0; i
< totalVars
; i
++) {
2465 double z
= signatures
[i
] / minStates
- 1.0;
2466 signatures
[i
] = (z
< 0.0) ? -z
: z
; /* make positive */
2468 /* Sort candidates in decreasing order of signature. */
2469 qsort((void *)candidates
,nvars
,sizeof(int),
2470 (DD_QSFP
)ntrSignatureCompare
);
2473 /* Now process the candidates in the given order. */
2474 for (i
= 0; i
< nvars
; i
++) {
2475 var
= Cudd_bddIthVar(dd
,candidates
[i
]);
2476 if (Cudd_bddVarIsDependent(dd
,newstates
,var
)) {
2477 abs
= Cudd_bddExistAbstract(dd
,newstates
,var
);
2478 if (abs
== NULL
) return(NULL
); Cudd_Ref(abs
);
2479 positive
= Cudd_Cofactor(dd
,newstates
,var
);
2480 if (positive
== NULL
) return(NULL
); Cudd_Ref(positive
);
2481 phi
= Cudd_bddLICompaction(dd
,positive
,abs
);
2482 if (phi
== NULL
) return(NULL
); Cudd_Ref(phi
);
2483 Cudd_RecursiveDeref(dd
,positive
);
2486 (void) printf("Phi");
2487 Cudd_PrintDebug(dd
,phi
,T
->nlatches
,pr
);
2490 if (Cudd_DagSize(phi
) < NTR_MAX_DEP_SIZE
) {
2492 for (j
= 0; j
< T
->nparts
; j
++) {
2493 tmp
= Cudd_bddCompose(dd
,T
->part
[j
],phi
,candidates
[i
]);
2494 if (tmp
== NULL
) return(NULL
); Cudd_Ref(tmp
);
2495 Cudd_RecursiveDeref(dd
,T
->part
[j
]);
2498 Cudd_RecursiveDeref(dd
,newstates
);
2501 Cudd_RecursiveDeref(dd
,abs
);
2503 Cudd_RecursiveDeref(dd
,phi
);
2509 finalSize
= Cudd_SharingSize(T
->part
,T
->nparts
);
2510 (void) printf("Eliminated %d vars. Transition function %d nodes.\n",
2514 if (!ntrUpdateQuantificationSchedule(dd
,T
)) return(NULL
);
2516 /* Quantify out of states variables that no longer appear in any part. */
2517 Cudd_RecursiveDeref(dd
,*states
);
2518 *states
= Cudd_bddExistAbstract(dd
,newstates
,T
->preiabs
);
2519 if (*states
== NULL
) return(NULL
); Cudd_Ref(*states
);
2520 Cudd_RecursiveDeref(dd
,newstates
);
2523 } /* end of ntrEliminateDependencies */
2526 /**Function********************************************************************
2528 Synopsis [Updates the quantification schedule of a transition relation.]
2530 Description [Updates the quantification schedule of a transition relation.
2531 Returns 1 if successful; 0 otherwise.]
2535 SeeAlso [ntrEliminateDependencies]
2537 ******************************************************************************/
2539 ntrUpdateQuantificationSchedule(
2545 DdNode
*one
, *support
, *scan
, *var
, *tmp
;
2547 int *position
, *row
;
2556 nvars
= Cudd_ReadSize(dd
);
2557 one
= Cudd_ReadOne(dd
);
2559 /* Reinitialize the abstraction cubes. */
2560 Cudd_RecursiveDeref(dd
,T
->preiabs
);
2563 for (i
= 0; i
< nparts
; i
++) {
2564 Cudd_RecursiveDeref(dd
,T
->icube
[i
]);
2569 /* Initialize row permutations to the identity. */
2570 position
= ALLOC(int,nparts
);
2571 if (position
== NULL
) return(0);
2572 for (i
= 0; i
< nparts
; i
++) {
2575 /* Sort parts so that parts that differ only
2576 ** in the index of the next state variable are contiguous. */
2577 staticPart
= T
->part
;
2578 qsort((void *)position
,nparts
,sizeof(int), (DD_QSFP
)ntrPartCompare
);
2579 /* Extract repeated parts. */
2581 for (i
= 0; i
< nparts
- 1; i
+= j
) {
2588 pij
= position
[i
+j
];
2589 while (Cudd_Regular(staticPart
[pij
]) == Cudd_Regular(staticPart
[pi
])) {
2590 int comple
= staticPart
[pij
] != staticPart
[pi
];
2591 DdNode
*xnor
= Cudd_bddXnor(dd
,T
->nscube
[pi
],
2592 Cudd_NotCond(T
->nscube
[pij
],comple
));
2593 if (xnor
== NULL
) return(0); Cudd_Ref(xnor
);
2594 tmp
= Cudd_bddAnd(dd
,xnor
,eq
);
2595 if (tmp
== NULL
) return(0); Cudd_Ref(tmp
);
2596 Cudd_RecursiveDeref(dd
,xnor
);
2597 Cudd_RecursiveDeref(dd
,eq
);
2599 Cudd_RecursiveDeref(dd
,T
->part
[pij
]);
2600 Cudd_RecursiveDeref(dd
,T
->icube
[pij
]);
2601 Cudd_RecursiveDeref(dd
,T
->nscube
[pij
]);
2602 T
->part
[pij
] = NULL
;
2604 if (i
+j
== nparts
) break;
2605 pij
= position
[i
+j
];
2608 int retval
= Ntr_HeapInsert(T
->factors
,eq
,Cudd_DagSize(eq
));
2609 if (retval
== 0) return(0);
2612 Cudd_RecursiveDeref(dd
,eq
);
2615 /* Compact the part array by removing extracted parts. */
2616 for (i
= 0, j
= 0; i
< nparts
; i
++) {
2617 if (T
->part
[i
] != NULL
) {
2618 T
->part
[j
] = T
->part
[i
];
2619 T
->icube
[j
] = T
->icube
[i
];
2620 T
->nscube
[j
] = T
->nscube
[i
];
2624 nparts
= T
->nparts
-= extracted
;
2625 (void) printf("Extracted %d repeated parts in %d factors.\n",
2626 extracted
, Ntr_HeapCount(T
->factors
));
2628 /* Build the support matrix. Each row corresponds to a part of the
2629 ** transition relation; each column corresponds to a variable in
2630 ** the manager. A 1 in position (i,j) means that Part i depends
2631 ** on Variable j. */
2632 matrix
= ntrAllocMatrix(nparts
,nvars
);
2633 if (matrix
== NULL
) return(0);
2635 /* Allocate array for quantification schedule and initialize it. */
2636 schedule
= ALLOC(int,nvars
);
2637 if (schedule
== NULL
) return(0);
2638 for (i
= 0; i
< nvars
; i
++) {
2641 /* Collect scheduling info for this part. At the end of this loop
2642 ** schedule[i] == j means that the variable of index i does not
2643 ** appear in any part with index greater than j, unless j == -1,
2644 ** in which case the variable appears in no part.
2646 for (i
= 0; i
< nparts
; i
++) {
2647 support
= Cudd_Support(dd
,T
->part
[i
]);
2648 if (support
== NULL
) return(0); Cudd_Ref(support
);
2650 while (!Cudd_IsConstant(scan
)) {
2651 int index
= scan
->index
;
2652 schedule
[index
] = i
;
2653 matrix
[i
][index
] = 1;
2654 scan
= Cudd_T(scan
);
2656 Cudd_RecursiveDeref(dd
,support
);
2659 (void) printf("Initial schedule:");
2661 for (i
= 0; i
< nvars
; i
++) {
2662 (void) printf(" %d", schedule
[i
]);
2663 if (schedule
[i
] != -1) schedcost
+= schedule
[i
];
2665 (void) printf("\nCost = %d\n", schedcost
);
2668 /* Initialize direct and inverse row permutations to the identity
2670 row
= ALLOC(int,nparts
);
2671 if (row
== NULL
) return(0);
2672 for (i
= 0; i
< nparts
; i
++) {
2673 position
[i
] = row
[i
] = i
;
2676 /* Sift the matrix. */
2677 flags
= ALLOC(char,nvars
);
2678 if (flags
== NULL
) return(0);
2679 for (i
= 0; i
< nparts
; i
++) {
2680 int cost
= 0; /* cost of moving the row */
2682 int posn
= position
[i
];
2683 int bestposn
= posn
;
2685 /* Initialize the flags to one is for the variables that are
2686 ** currently scheduled to be quantified after this part gets
2687 ** multiplied. When we cross a row of a part that depends on
2688 ** a variable whose flag is 1, we know that the row being sifted
2689 ** is no longer responsible for that variable. */
2690 for (k
= 0; k
< nvars
; k
++) {
2691 flags
[k
] = (char) (schedule
[k
] == i
);
2693 for (j
= posn
- 1; j
>= 0; j
--) {
2694 for (k
= 0; k
< nvars
; k
++) {
2695 if (schedule
[k
] == row
[j
]) {
2698 flags
[k
] &= matrix
[row
[j
]][k
] == 0;
2702 if (cost
< bestcost
) {
2708 /* Reinitialize the flags. (We are implicitly undoing the sift
2710 for (k
= 0; k
< nvars
; k
++) {
2711 flags
[k
] = (char) (schedule
[k
] == i
);
2713 for (j
= posn
+ 1; j
< nparts
; j
++) {
2714 for (k
= 0; k
< nvars
; k
++) {
2715 if (schedule
[k
] == row
[j
]) {
2716 flags
[k
] |= matrix
[i
][k
] == 1;
2717 cost
-= flags
[k
] == 0;
2722 if (cost
< bestcost
) {
2727 /* Move to best position. */
2728 if (bestposn
< posn
) {
2729 for (j
= posn
; j
>= bestposn
; j
--) {
2731 if (j
> 0) row
[j
] = row
[j
-1];
2735 for (j
= posn
; j
<= bestposn
; j
++) {
2737 if (j
< nparts
- 1) row
[j
] = row
[j
+1];
2741 position
[i
] = bestposn
;
2743 /* Fix the schedule. */
2744 for (k
= 0; k
< nvars
; k
++) {
2745 if (matrix
[i
][k
] == 1) {
2746 if (position
[schedule
[k
]] < bestposn
) {
2749 for (j
= nparts
- 1; j
>= position
[i
]; j
--) {
2750 if (matrix
[row
[j
]][k
] == 1) break;
2752 schedule
[k
] = row
[j
];
2757 ntrFreeMatrix(matrix
);
2760 /* Update schedule to account for the permutation. */
2761 for (i
= 0; i
< nvars
; i
++) {
2762 if (schedule
[i
] >= 0) {
2763 schedule
[i
] = position
[schedule
[i
]];
2767 ntrPermuteParts(T
->part
,T
->nscube
,row
,position
,nparts
);
2771 (void) printf("New schedule:");
2773 for (i
= 0; i
< nvars
; i
++) {
2774 (void) printf(" %d", schedule
[i
]);
2775 if (schedule
[i
] != -1) schedcost
+= schedule
[i
];
2777 (void) printf("\nCost = %d\n", schedcost
);
2780 /* Mark the next state varibles so that they do not go in the
2781 ** abstraction cubes. */
2782 for (i
= 0; i
< T
->nlatches
; i
++) {
2783 schedule
[T
->y
[i
]->index
] = -2;
2786 /* Rebuild the cubes from the schedule. */
2787 for (i
= 0; i
< nvars
; i
++) {
2789 var
= Cudd_bddIthVar(dd
,i
);
2791 tmp
= Cudd_bddAnd(dd
,T
->icube
[k
],var
);
2792 if (tmp
== NULL
) return(0); Cudd_Ref(tmp
);
2793 Cudd_RecursiveDeref(dd
,T
->icube
[k
]);
2795 } else if (k
!= -2) {
2796 tmp
= Cudd_bddAnd(dd
,T
->preiabs
,var
);
2797 if (tmp
== NULL
) return(0); Cudd_Ref(tmp
);
2798 Cudd_RecursiveDeref(dd
,T
->preiabs
);
2804 /* Build the conjuncts. */
2805 for (i
= 0; i
< nparts
; i
++) {
2806 tmp
= Cudd_bddXnor(dd
,T
->nscube
[i
],T
->part
[i
]);
2807 if (tmp
== NULL
) return(0); Cudd_Ref(tmp
);
2808 Cudd_RecursiveDeref(dd
,T
->part
[i
]);
2814 } /* end of ntrUpdateQuantificationSchedule */
2817 /**Function********************************************************************
2819 Synopsis [Comparison function used by qsort.]
2821 Description [Comparison function used by qsort to order the
2822 variables according to their signatures.]
2826 ******************************************************************************/
2828 ntrSignatureCompare(
2832 if (signatures
[*ptrY
] > signatures
[*ptrX
]) return(1);
2833 if (signatures
[*ptrY
] < signatures
[*ptrX
]) return(-1);
2836 } /* end of ntrSignatureCompare */
2839 /**Function********************************************************************
2841 Synopsis [Comparison function used by qsort.]
2843 Description [Comparison function used by qsort to order the
2844 variables according to their signatures.]
2848 ******************************************************************************/
2850 ntrSignatureCompare2(
2856 if (!st_lookup(staticNet
->hash
,staticNet
->latches
[*ptrX
][1],&node
)) {
2859 x
= node
->dd
->index
;
2860 if (!st_lookup(staticNet
->hash
,staticNet
->latches
[*ptrY
][1],&node
)) {
2863 y
= node
->dd
->index
;
2864 if (signatures
[x
] < signatures
[y
]) return(1);
2865 if (signatures
[x
] > signatures
[y
]) return(-1);
2868 } /* end of ntrSignatureCompare2 */
2871 /**Function********************************************************************
2873 Synopsis [Comparison function used by qsort.]
2875 Description [Comparison function used by qsort to order the
2876 parts according to the BDD addresses.]
2880 ******************************************************************************/
2886 if (staticPart
[*ptrY
] > staticPart
[*ptrX
]) return(1);
2887 if (staticPart
[*ptrY
] < staticPart
[*ptrX
]) return(-1);
2890 } /* end of ntrPartCompare */
2893 /**Function********************************************************************
2895 Synopsis [Allocates a matrix.]
2897 Description [Allocates a matrix of char's. Returns a pointer to the matrix
2898 if successful; NULL otherwise.]
2904 ******************************************************************************/
2913 matrix
= ALLOC(char *,nrows
);
2914 if (matrix
== NULL
) return(NULL
);
2915 matrix
[0] = ALLOC(char,nrows
* ncols
);
2916 if (matrix
[0] == NULL
) {
2920 for (i
= 1; i
< nrows
; i
++) {
2921 matrix
[i
] = matrix
[i
-1] + ncols
;
2923 for (i
= 0; i
< nrows
* ncols
; i
++) {
2928 } /* end of ntrAllocMatrix */
2931 /**Function********************************************************************
2933 Synopsis [Frees a matrix of char's.]
2941 ******************************************************************************/
2950 } /* end of ntrFreeMatrix */
2953 /**Function********************************************************************
2955 Synopsis [Sorts parts according to given permutation.]
2959 SideEffects [The permutation arrays are turned into the identity
2964 ******************************************************************************/
2976 for (i
= 0; i
< size
; i
++) {
2977 if (comesFrom
[i
] == i
) continue;
2979 tmp
= a
[i
]; a
[i
] = a
[j
]; a
[j
] = tmp
;
2980 tmp
= b
[i
]; b
[i
] = b
[j
]; b
[j
] = tmp
;
2981 comesFrom
[goesTo
[i
]] = j
;
2983 goesTo
[j
] = goesTo
[i
];
2988 } /* end of ntrPermuteParts */