
Accession Number : ADA296385
Title : Applications of MultiTerminal Binary Decision Diagrams.
Corporate Author : CARNEGIEMELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Clarke, E. ; Fujita, M. ; Zhao, X.
PDF Url : ADA296385
Report Date : APR 1995
Pagination or Media Count : 20
Abstract : Functions that map boolean vectors into the integers are important for the design and verification of arithmetic circuits. MTBDDs and BMDs have been proposed for representing this class of functions. We discuss the relationship between these methods and describe a generalization called hybrid decision diagrams which is often much more concise. The Walsh transform and ReedMuller transform have numerous applications in computeraided design, but the usefulness of these techniques in practice has been limited by the size of the boolean functions that can be transformed. Currently available techniques limit the functions to less than 20 variables. In this paper, we show how to compute concise representations of the Walsh transform and ReedMuller transform for functions with several hundred variables. We show how to implement arithemetic operations efficiently for hybrid decision diagrams. In practice, this is one of the main limitations of BMDs since performing arithmetic operations on functions expressed in this notation can be very expensive. In order to extend symbolic model checking algorithms to handle arithmetic properties, it is essential to be able to compute the BDD for the set of variable assignments that satisfy an arithmetic relation. Bryant and Chen do not provide an algorithm for this. In our paper, we give an efficient algorithm for this purpose. Moreover, we prove that for the class of linear expressions, the time complexity of our algorithm is linear in the number of variables. Our techniques for handling arithmetic operations and relations are used intensively in the verification of an SRT division algorithm similar to the one that is used in the Pentium. (AN)
Descriptors : *ALGORITHMS, *MATHEMATICAL PROGRAMMING, *COMPUTER PROGRAM VERIFICATION, *BINARY ARITHMETIC, MATHEMATICAL MODELS, LINEAR SYSTEMS, COMPUTATIONS, DECISION MAKING, COMPUTER AIDED DESIGN, MATRICES(MATHEMATICS), EFFICIENCY, VARIABLES, LIMITATIONS, HYBRID SYSTEMS, CIRCUITS, SPECIAL FUNCTIONS(MATHEMATICS), MAPPING(TRANSFORMATIONS), FLOATING POINT OPERATION, DIAGRAMS, BOOLEAN ALGEBRA, WALSH TRANSFORMATION.
Subject Categories : Operations Research
Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE