Project Overview
Formal verification of hardware aims at developing techniques, methods
and software tools that help a designer assess the correctness of his
design. Usually, two broad areas in verification are distinguished:
-
Checking whether a combinational circuit complies with a given (more
abstract) specification.
-
Checking whether a circuit's
behaviour conforms to certain desired properties.
The latter is mostly referred to as model-checking; the former is a
case of an equivalence problem. In both areas, the efficient
representation of logical data such as Boolean functions, relations,
and sets of states is vital to obtain reasonable runtimes of programs
that tackle the aforementioned problems. A favorite choice has been
the use of so-called Binary Decision Diagrams or BDDs for short.
Binary Decision Diagrams (BDDs) - Current research on BDDs
concentrates on innovative implementations that better exploit the
underlying hardware while still maintaining platform independence at
the API level. For instance, a new BDD package has been developed
where the main data structures use indices instead of pointers. For
information can be found in the paper entitled "Design of a
pointerless BDD package."
Reference:
Design of a Pointerless BDD Package
