# Generation Of A Complete Set Of Properties

arXiv: https://arxiv.org/abs/2004.05853 · HTML: https://mlsanity.com/paper/2004.05853/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Apr 2020.

## Built on by (most cited first, 1 of 1)

- [AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL](https://mlsanity.com/paper/2503.19174/) (2025)

## Abstract (arXiv)

One of the problems of formal verification is that it is not functionally complete due the incompleteness of specifications. An implementation meeting an incomplete specification may still have a lot of bugs. In testing, this issue is addressed by replacing functional completeness with mathitstructural one. The latter is achieved by generating a set of tests probing every piece of a design implementation. We show that a similar approach can be used in formal verification. The idea here is to generate a property of the implementation at hand that is not implied by the specification. Finding such a property means that the specification is not complete. If this is an mathitunwanted property, the implementation is buggy. Otherwise, a new specification property needs to be added. Generation of implementation properties related to different parts of the design followed by adding new specification properties produces a mathitstructurally-mathitcomplete:specification. Implementation properties are built by mathitpartial: quantifier:elimination, a technique where only a part of the formula is taken out of the scope of quantifiers. An implementation property is generated by applying partial quantifier elimination to a formula defining the "truth table" of the implementation. We show how our approach works on specifications of combinational and sequential circuits.