Formal and Assertion-Based Verification of MBIST MCPs

In this article we motivate the need to formally verify MBIST MCPs, discuss FishTail’s methodology for MCP verification and the approach used to debug formal MCP verification failures or generate assertions for import into RTL functional simulation. The methodology was applied to a small MBIST IP with 59 MCPs. The MCPs applied to a total of 2090 paths.

The formal verification of MBIST MCPs using RTL input guarantees the correctness of MBIST MCPS at the time they are written, and then ensures that while revisions to RTL and constraints are being made, the MBIST MCPs are continually verified to be good. Customers who receive MBIST IP are able to verify MCPs delivered along with this IP, accounting for any customization they make.

Read more