|
CMU-CS-98-162
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-98-162
Ordered Binary Decision Diagrams and Minimal Trellises
John Lafferty, Alexander Vardy*
July 1998
CMU-CS-98-162.ps
CMU-CS-98-162.pdf
Keywords: Binary decision diagrams, trellises, CAD, coding theory,
formal verification
Ordered binary decision diagrams (OBDDs) are graph-based data structures
for representing Boolean functions. They have found widespread use in
computer-aided design and in formal verification of digital
circuits. Minimal trellises are graphical representations of
error-correcting codes that play a prominent role in coding theory.
This paper establishes a close connection between these two graphical
models, as follows. Let C be a binary code of length n, and let
fc(x\/1,...,,x\/n) be the Boolean function that takes the value)
at x\/1,...,x\/n if and only if (x\/1,...x\/n) element C. Given this
natural one-to-one correspondence between Boolean functions and binary
codes, we prove that the minimal proper trellis for a code C with
minimum distance d > 1 is isomorphic to the single-terminal OBDD for
its Boolean indicator function fc(x\/1,...,x\/n). Prior to this
result, the extensive research during the past decade on
binary decision diagrams -- in computer engineering -- and on
minimal trellises -- in coding theory -- has been carried out
independently. As outlined in this work, the realization that
binary decision diagrams and minimal trellises are essentially
the same data structure opens up a range of promising
possibilities for transfer of ideas between these disciplines.
35 pages
*Coordinated Science Laboratory, Univeristy of Illinois at Urbana-Champaign,
1308 W. Main Street, Urbana, IL 61801
|