A low risk, high reward approach to adopting formal methods

James Pascoe – STMicroelectronics R&D Ltd.
April 8, 2013
EE Times

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:

  1. Achieve verification closure with appreciably less time and effort than that required by a constrained random approach
  2. 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
  3. 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. More …