At STMicroelectronics, we recently investigated using formal methods as a complement to the constrained random testing of our ARM based CPU subsystems. Our motivations were to:
- Achieve verification closure with appreciably less time and effort than that required by a constrained random approach
- Encourage designers to develop formal properties for their blocks. Functional insights can be expressed as PSL or SVA assertions in the RTL. These properties then provide follow-on benefits in the subsequent design stages
- Augment or replace legacy in-house flows with mature industry tools. This reduces maintenance overhead and promotes a more robust approach
- To address the engineersí reservations about formalís ease of use, we took a stepwise approach that would enable them to accumulate expertise incrementally. This approach also significantly reduced the projectís risk.
Accordingly, we applied formal methods in parallel with constrained random testing to three designs, each more complex than the previous one, each yielding different insights into the effectiveness of formal methods.
Along the way, we found that, using a formal approach, we verified in four engineering weeks what had taken six engineer weeks of constrained random test-bench development effort. We could understand the functionality of a block for which the functional specification was not available; we found errors in blocks that had been verified by other means and we clarified ambiguities in specifications quickly and efficiently. This process steadily built our confidence that formal methods could deliver a return that was worth the investment.
This article describes our work and the results that we achieved.
Our verification challenge
We are responsible for the CPU subsystem side in a CPU/GPU design team. We develop ARM based subsystems that are integrated into a wide range of system-on-chip (SoC) design platforms (see Figure 1). The SoCs are targeted at a wide range of applications from mobile devices to Big Data, Cloud and High Performance Computing.
Figure 1: Example of an ST ARM based CPU subsystem
Our subsystem verification strategy is focused on three levels of abstraction:
Unit testing: The objective of unit testing is to ensure that the blocks developed by ST are ready to enter verification. Unit testing is typically performed by the designers, using HDL-based test-benches. These test-benches are often not reusable or of limited use when the block enters verification.
Block-level verification: The objective is to ensure that each block conforms to its specification in isolation from the rest of the system. Block-level projects are typically conducted by verification engineers using a constrained random approach.
System-level testing: Once the individual blocks have been verified in isolation, they are integrated into a subsystem. Point-to-point connectivity checks are performed to detect wiring errors in both the functional design and the power management circuitry. This is followed by functional testing to ensure that the subsystem operates as a whole. Functional testing is performed using both constrained random and directed tests. The subsystem may also undergo performance testing, for example using approaches defined by the Embedded Processor Benchmark Consortium (EEMBC) .
We used a three-step process to apply formal methods to each of these verification challenges.