DocumentCode :
341493
Title :
Grouping heuristics for word-level decision diagrams
Author :
Drechsler, Rolf ; Herbstritt, Marc ; Becker, Bernd
Author_Institution :
Inst. of Comput. Sci., Albert-Ludwigs-Univ., Freiburg, Germany
Volume :
1
fYear :
1999
fDate :
36342
Firstpage :
411
Abstract :
Word-level decision diagrams (WLDDs), like EVBDDs, *BMDs, HDDs, K*BMDs, are powerful tools in circuit verification. For some arithmetic circuits, like multipliers, formal verification was possible for the first time using WLDDs. Besides a good variable ordering and the decomposition types the size of a WLDD essentially depends on the grouping of the outputs. In this paper we study output grouping in more detail. We give examples showing that an exponential reduction or an exponential blow-up can be obtained dependent on grouping. We describe efficient heuristics for output grouping given a circuit description in the form of a netlist. Experimental results are given to demonstrate the efficiency of our approach
Keywords :
Boolean functions; circuit CAD; computational complexity; data structures; decision diagrams; formal verification; logic CAD; circuit verification; decomposition types; efficiency; exponential blow-up; exponential reduction; formal verification; heuristics; netlist; output grouping; variable ordering; word-level decision diagrams; Algorithm design and analysis; Arithmetic; Boolean functions; Circuit analysis; Computer science; Data structures; Heuristic algorithms; NP-complete problem; Registers; Uninterruptible power systems;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Circuits and Systems, 1999. ISCAS '99. Proceedings of the 1999 IEEE International Symposium on
Conference_Location :
Orlando, FL
Print_ISBN :
0-7803-5471-0
Type :
conf
DOI :
10.1109/ISCAS.1999.777893
Filename :
777893
Link To Document :
بازگشت