Using Formal Tools to Improve the Productivity of Verification at STMicroelectronics

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:

1. To close verification projects with appreciably less time and effort than that required by a constrained random approach;
2. To promote a greater use of assertions by encouraging designers to develop formal properties for their blocks;
3. 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.

Verification Challenges and the Benefits of Formal

ST’s sub-system verification strategy is based on three levels of abstraction. Unit-tests provide a means to determine that a block is ready to enter verification. In previous projects, unit-testing was performed by designers using HDL test-benches. These test-benches require a significant amount of development effort and are often not re-usable when the block enters verification. Thus, one challenge was to reduce this effort and to re-use the output in subsequent design phases. In addition, a further challenge was to determine how they could detect bugs faster.

Using formal, they unit-tested the Sensor Control Block (see Figure 1) in 1 man/weeks, whereas, they required 2 man/weeks to develop an HDL test-harness. This saving came from not having to develop test-bench code. Using formal, properties can be tested with little setup. Thus, testing began immediately and this provided results quickly. Furthermore, the formal properties that were written were re-used as the basis of the block-level verification. These properties can also be embedded into the RTL and so will continue to add value throughout the IPs life-cycle.

Once the unit-tests have been completed, each IP enters block-level verification. One challenge at this level is for formal to close verification faster than constrained random. For the Sensor Control Block, ST closed their formal verification in 4 man/weeks, whereas, they required 7 man /weeks to complete the constrained random equivalent. This time saving came (again) from not having to develop test-bench code and also from the re-use of the properties written for the unit-testing. In terms of results, ST discovered 3 bugs in the first week of using the formal tool. After 7 man/weeks of constrained random development, ST discovered only one further issue.

Block-level verification ensures that each block conforms to its specification in isolation. In the team, sub-system integration is performed by hand and so ST require a flow to detect errors in the wiring. Previously, ST had developed a Specman based approach. While this had worked, the flow required regular maintenance and was not bug free. Using Jasper, ST was able to develop a point-to-point connectivity flow that was driven from the project’s documentation. Within 2 man/weeks, they had proved 2568 connectivity properties.

Conclusion

How do formal methods deliver in the context of our aims and challenges? ST has achieved their cost, time and effort reduction goals. They have also achieved their property reuse goals and have transformed legacy aspects of their flow into more comprehensive and robust approaches. The full presentation will expand on these findings and will describe ST’s additional results in the areas of low-power verification, control status register checking and sequential equivalence.

To register to see this presentation at ChipEx, go to http://www.chipex.com/il.

Tags: ChipEx, Jasper, STMicroelectronics, Verification

Category: Jasper

This entry was posted on Tuesday, April 9th, 2013 at 8:44 am. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.