Publication
The Future is Hybrid: Next Generation Data Structures for Formal Verification
Rolf Drechsler; Christina Plump; Martha Schnieber
In: Rolf Drechsler; Christina Plump; Martha Schnieber (Hrsg.). 33th IEEE Asian Test Symposium (ATS 2024). Asian Test Symposium (ATS-2025), December 17-20, Ahmedabad, India, 2024.
Abstract
Trust in electronic devices is dependent on their safe
and reliable behavior. An integral part is the correct design of the
hardware. While classically simulation-based approaches have
been applied, only through formal proof techniques complete
correctness can be guaranteed. The core of these formal approaches, and responsible for time and space complexity, is the
choice of the underlying data structure to represent the functional
behavior. A significant class of data structures are graph-based
function representations, like BDDs, KFDDs or *BMDs. These
have shown excellent properties – provability in polynomial time
and space – for some function classes , e.g., adders. Experimental
studies have validated these properties, and formal proofs can
guarantee this behavior. Unfortunately, these properties often
cannot be generalized to varying function classes. One reason is
that graph-based representations are usually tailored for either
bit-level or word-level functions. However, designing hybrid data
structures that can represent both types in parallel might allow
formal proofs for even larger functional classes.
In this paper, we demonstrate how to design these hybrid
data structures, overcoming limitations of current formal verification approaches. We introduce a generalized concept on
decompositions and graph-based function representations based
on Kronecker matrices with an extended element space and
dimension. It is shown how these extensions allow the representation of hybrid function classes, paving the way for more
trust in electronic devices.