Symbolic Simulation, Model Checking and Abstraction with Partially Ordered Boolean Functional Vectors

Boolean Functional Vectors (BFVs) are a symbolic representation for sets of bit-vectors that can be exponentially more compact than the corresponding characteristic functions with BDDs. Additionally, BFVs are the natural representation of bit-vector sets for Symbolic Simulation. Recently, we developed set manipulation algorithms for canonical BFVs by interpreting them as totally ordered selections. In this paper we generalize BFVs by defining them with respect to a partial order. We show that partially ordered BFVs can serve as abstractions for bit-vector sets and can be used to compute over-approximations in reachability analysis. In the special case when the underlying graph of the partial order is a forest, we can efficiently compute an abstract interpretation in a symbolic simulation framework. We present circuit examples where we leverage the exponential gap in the representations and inherent structure in the state-space to demonstrate the usefulness of Partially Ordered Boolean Functional Vectors.