Formal verification coverage: are the RTL-properties covering the design´s architectural intent?

It is essential to formally ascertain whether the RTL validation effort effectively guarantees the correctness with respect to the design´s architectural intent. The design´s architectural intent can be expressed in formal properties. However, due to the capacity limitation of formal verification, these architectural-properties cannot be directly verified on the RTL. As a result, a set of lower level RTL-properties are developed and verified against the RTL. In this paper we present: (1) a method for checking whether the RTL-properties are covering the architectural-properties, that is, whether verifying the RTL-properties guarantee the correctness of the design´s architectural intent; and (2) a method to identify the coverage holes in terms of the architectural properties (or their sub-properties) that are not covered.