From: [ Jim Hogan of Vista Ventures LLC ]
Subject: Where Formal ABV whomps HDL simulation for chip verification
Hi, John
The truth is Formal and Verilog/VHDL simulation go quite well together. While simulation is time-based, and formal is state-space based. Any verification plan that uses both simulation & formal will hit its coverage goals much faster because together they perform a broader range of tests in much less human time.
Anyway, my true goal here is to show your readers how Formal Assertion-Based Verification (F-ABV) has expanded into chip verification — and where it beats old school standalone Verilog/VHDL RTL simulation.
The general rule is:
– FORMAL operates on all states concurrently over short bursts of time. For example, if you have 27 scenarios which must be examined at the same time (e.g. 27 branch conditions), formal works well and will examine each of these branches to a typical depth of 30 clock cycles. And it can go up to 150 clock cycles in, depending on the code.
– SIMULATION can be thought of as operating on limited set of states over large timescales. For example, if you have one sequence going state-by-state over a 1000 clock cycles, simulation is far better.