Design intent coverage is a formal methodology for analyzing the gap between a formal architectural specification of a design and the formal functional specifications of the component RTL blocks of the design. In this article we extend the design intent coverage methodology to hybrid specifications containing both state-machines and formal properties. We demonstrate the benefits of this extension in two domains of considerable recent interest, namely (a) the use of auxiliary state-machines in formal specifications, and (b) the use of modest sized RTL blocks in the design intent coverage analysis.

We present a new approach to bias random test generation for accelerating assertion coverage. The novelty of the proposed approach is that it treats the design under test as a black box and attempts to steer the simulation toward coverage points that are relevant for targeted assertions purely through external control. We present this approach over three different models with varying degrees of observability and control. The results demonstrate a significant speedup in assertion coverage as compared to randomized simulation.

In this paper, we present methods for automatic test generation from formal specifications. These are used to create intelligent test benches that are able to cover corner case behaviors in much less time. We have developed a prototype tool for intelligent test generation within the layered test bench architecture proposed in RVM. We present results on verification IPs of standard bus protocols to show the effectiveness of our approach.

A typical verification IP (VIP) of a bus protocol such as ARM AMBA or PCI consists of a set of assertions and associated verification aids like test-benches and coverage metrics. While, several languages have been formalized for specifying assertions (examples include OVA, Sugar, ForSpec, SVA, etc), the tasks of writing test-benches that produce protocol compliant stimuli and coverage monitors that reflect the coverage of the protocol functionality are also of significant importance. This paper presents a platform for high-level specification of a bus protocol and an automated methodology for generating a variety of verification aids that must supplement the set of assertions in a VIP.