At this year’s ChipEx, STMicroelectronics (ST) will discuss how they used formal methods as a means to improve the productivity of their verification. In particular, they had three key aims:
- To close verification projects with appreciably less time and effort than that required by a constrained random approach;
- To promote a greater use of assertions by encouraging designers to develop formal properties for their blocks;
- To augment or replace legacy in-house flows with mature industry tools. This reduces maintenance overhead and promotes a more robust approach.
They applied formal methods at the unit-level, block-level and the system-level of an ARM based CPU sub-system (see Figure 1). Each project gave different insights into the effectiveness of the formal approach. In order to make an effective evaluation, they developed constrained random alternatives. This allowed them to make direct comparisons and reduced the project’s risk.
A paper at ChipEx will be presented that describes the productivity improvements they experienced using formal methods to verify a critical CPU sub-system that is targeted at mobile applications. In particular, they describe the challenges involved and how a formal tool (Jasper) delivered benefits in terms of effort savings, re-use and insight into IP that was not fully characterized in the context of a new design. The full presentation will also describe their experiences using formal in the context of low-power verification, control status register checking and sequential equivalence.
Figure 1: An ST ARM based CPU sub-system. The shaded blocks were verified using Jasper.
