Released on March 18, 2021.
Overview:
Even relatively small IPs can have hundreds of control&status registers, many with customized, unconventional access policies. While testbench simulation-based register verification approaches like UVM_REG can exercise most of the primary use cases, numerous corner-cases can be left uncovered, creating the risk of show-stopper bugs going undetected.
In this session, we will show how to employ an automated, formal-based flow to ensure complete coverage of your registers’ state space – without having to learn formal at all. The benefits of this approach are two-fold: you can exhaustively verify the specified behaviors and the complete absence of any illegal behaviors. Plus, any detected discrepancies are graphically shown in detailed waveforms – i.e. no need to back-track through second-order effects – the results shown are exactly the given issue’s root cause. This will be illustrated in the context of a common, real-world verification task that will be familiar to many – verifying an AMBA AXI3 interface.
Note that this session will be relatively technical: the examples will include timing diagrams and RTL code. Familiarity with Verilog or VHDL is assumed.
What You Will Learn:
- How to exhaustively verify your control&status register behavior against your register specification. This includes both common policies (e.g. R/W, Write to Clear, Read-only, etc.) and user-defined register configuration schemas and access policies
- How to set up the flow to design and verify front or back-door register access
- You will actually NOT learn about formal itself – the formal verification is automated under-the-hood
