Accelerating Datapath Verification using Formal techniques
DescriptionDatapath Verification has always been the bottleneck in any verification plan because of the possibility of missing some corner cases while verifying colossal number of inputs possible. Conventional methods such as Dynamic Verification(simulations) and Formal Verification have limitations. While, in Dynamic Verification, it is not possible to verify all possible inputs exhaustively, in Formal Verification it is difficult to develop a synthesizable model especially for complex mathematical functions and achieve convergence.

Further Modern day CPU's used in real time microcontrollers are often architected to trade off between speed and accuracy. In cases where speed is the utmost concern we try to settle for a less accurate result but still ensure that the result obtained does not differ greater than a certain threshold called Error Margin. It is important to verify that the difference between the result obtained in our CPU and the most accurate result is not greater than the error margin for every possible input and currently none of the tools are capable of exploring all the inputs exhaustively while achieving convergence within acceptable time.

The cases where accuracy is more important we tend to takes lot more cycles to produce the result which automatically increases the complexity of verification since convergence time increases drastically with the increase in the number of clock cycles.

In this paper, we present methodologies that explain how to verify above mentioned complex scenarios of CPU and accelerate Datapath Verification using JasperC2RTL.
Event Type
Engineering Track Poster
TimeWednesday, July 12th5:07pm - 5:09pm PDT
LocationLevel 2 Exhibit Hall
Back-End Design
Embedded Systems
Front-End Design