Thesis Topic Details

Topic ID:
155
Title:
Multi-valued Decision Diagram Package
Supervisor:
Ron van der Meyden
Research Area:
Formal Methods, Algorithms
Associated Staff
Assessor:
Kai Engelhardt
Topic Details
Status:
Active
Type:
Development
Programs:
CS CE BIOM BINF SE
Group Suitable:
No
Industrial:
Pre-requisites:
knowledge of algorithms, some logic, C/C++ programming
Description:
(Ordered) Binary Decision Diagrams (BDDs) are a succinct representation of boolean functions (from n boolean inputs to a boolean output value) that play a critical role in algorithms for verification and hardware synthesis. Operations on boolean functions can be efficiently computed at the level of this representation, e.g. from the representation Rep(f) of f:{0,1}^n -> {0,1}
and Rep(g) of g:{0,1}^n -> {0,1}, one can (in practice) efficiently compute
Rep(f/g), where f/g is the function defined by

(f/g)(x_1...x_n) = f(x_1...x_n) / g(x_1...x_n)

Significantly, Rep(f/g) can be computed as Rep(f) / Rep(g) _without_ iterating over the 2^n input values for x_1...x_n.

One of the well-known open source packages
for handling the BDD representation is CUDD. See
http://vlsi.colorado.edu/~fabio/CUDD/

We are developing a tool for synthesis of distributed systems that requires
a generalization of binary decision diagrams to multi-value decision diagrams, which represent functions f: V_1 x ... x V_n -> {0,1}. There is no freely available package comparable to CUDD for this generalization.

The project will be to develop such a package. This will involve:
-- generalization of the standard algorithms for BDD operations to the
multi-value case, including heuristic optimizations. (this should be
straightforward, but some research may be required.)
-- implementation of these algorithms.
Comments:
--
Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.