ICLAB Bonus Lab Note

Week 13

LAB Description

Topic of this week

1. Introduction to Formal Analysis
2. Introduction to SVA
3. JasperGold — Setup / Formal Coverage Analysis / Assertion Based Verification IP & Scoreboard
4. Bound Analysis

Design

Formal Verification

Description

Use ABCIP to verify the offered Customized I/O to AXI4-Lite bridge with build-in scoreboard and customized SVA by Formal Verification tool — JasperGold.

What did I learn?

1. Concepts of Formal Verification

Lecture Note

Formal Analysis

• Ensure the consistency with specification for all possible stimulus (inputs/undriven wires/unitialized registers)(100% coverage).
• Input restrictions with constraints assume (what never happens).
• Checker property with assert (what should not happen).
• Stimulus coverage with cover (what should happen).
• Benefits :
  1. Systematic method : More deterministic than random.
  2. Less testbench effort required : Much simplier than simulation testbench.
  3. Leads to higher quality : Often reveals bugs that simulation would never catch.
  4. Improves productivity and schedule : Can replace some block-level testbenches.

SystemVerilog Assertion, SVA

• SVA Properties are embedded in Verilog or SystemVerilog code.
• Includes assertions, covers, and assumptions.
• SVA Example :

• Sequences

• Built-In Function
  Combinational Functions : $onehot $onehot0 $countones $countzeros
  Temporal Functions : $stable $past $rose $fell

Glue Logic in SVA

• Auxiliary logic to observe and track events.
• Simplify coding.
• Come with no extra price.

Coverage Models

• Function Coverage (Lab10) : Property related covers / Covergroups.
  Pro. : Realizable.
  Con. : Corner cases, time consuming.
• Code Coverage : Branch / Statement / Expression.
  Pro. : Automatically generated, fully covered.
  Con. : False alarm issue.

Measuring Coverage

• Stimuli Coverage : Reachability analysis applies to all coverage models.
• Checker Coverage : Completeness of checking by the assertion set.
• Formal Coverage : Consolidation of Stimuli/Checker Coverage results.

Assertion Based Verification Intellectual Properties, ABVIPs

• Comprehensive set of checkers that check for protocol compliance.
• 3 modes of AMVIP :
  1. Master Mode : ABVIP (Master) ← → DUV (Slave)
  2. Slave Mode : DUV (Master) ← →ABVIP (Slave)
  3. Monitor Mode : DUV (Master) ← ABVIP (Monitor) → DUV (Slave)

上一篇：ICLAB Lab10 Note
下一篇：ICLAB Lab11 Note