January 1, 2005 -- Recently, engineers at STMicroelectronics (STM) achieved a verification productivity leap by introducing hybrid-formal verification into their development process. Initially, the STM Cellular Infrastructure Division verification team became interested in formal verification as a means to stress-test designs more thoroughly. They were particularly interested in the ability to use the technology for those portions of the designs with corner-case logic. Those portions had proven hard to exercise with simulation tests alone.

After an evaluation of different formal methods, the STM team decided to use hybrid-formal verification (also known as hybrid RTL formal verification). Using a built-in simulator, this methodology combines traditional formal techniques with dynamic simulation techniques. Hybrid-formal verification was first applied during the development of GreenSIDE, a next-generation wireless product.

By Remi Francard and Franco Toto. (Francard is the Verification Manager of the Cellular Infrastructure Division of ST Microelectronics and Toto is a Verification Engineer in the RTL Formal Verification Research & Development Group at STMicroelectronics.)