
CMUCS98162
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS98162
Ordered Binary Decision Diagrams and Minimal Trellises
John Lafferty, Alexander Vardy*
July 1998
CMUCS98162.ps
CMUCS98162.pdf
Keywords: Binary decision diagrams, trellises, CAD, coding theory,
formal verification
Ordered binary decision diagrams (OBDDs) are graphbased data structures
for representing Boolean functions. They have found widespread use in
computeraided design and in formal verification of digital
circuits. Minimal trellises are graphical representations of
errorcorrecting 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 onetoone 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 singleterminal 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 UrbanaChampaign,
1308 W. Main Street, Urbana, IL 61801
