The Future is Hybrid: Next Generation Data Structures for Formal Verification

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.