Sequential equivalence checking supports ESL flow

Philippe Georgelin and Pascal Urard, STMicroelectronics
(05/15/2006 9:00 AM EDT), EE Times

The complexity of digital-signal-processing-oriented applications is continually increasing. In the past, our group in STMicroelectronics developed our own Matlab-to-RTL design and verification methodology.

We validated this methodology on a pilot project using a satellite forward-error correction codec design[1][2][3]. Since then we have used our findings to refine an ESL (electronic system level) design flow based on formal verification between high-level system descriptions and RTL implementation.

Applications such as digital communication are becoming more and more complex. They have reached the point where the applications are too difficult to efficiently describe at the RTL level while achieving reasonable time-to-model and time-to-validation goals.

This added complexity results from the proliferation of features (for example, new standards for satellite transmission have a multitude of complex modes) and from challenges to reliability caused by the added time needed to test all the new features. In the past this might have taken several weeks to model and validate, but with new satellite transmission standards this could take substantially longer.

At the same time, we have observed the rapid evolution of standards that ultimately dictate the functionality required in our designs. Without a similar evolution in the efficiency and productivity of design and verification methods, it is conceivable that the implementation of a given standard takes longer than the time separating two generations of standards for a specific market.

Due to these issues, it becomes critical to develop a design and verification methodology at a higher level of abstraction. A crucial facet of such a methodology is the extent to which an implementation model (such as RTL) is kept coherent with a model of the functional behavior. Functional models are used to define algorithms and measure BER (bit-error-rate). A successful methodology would keep these models in sync at all stages of development.

Click here to read more ...