VF HORIZONS: “Understanding the SVA Engine Using the Fork-Join Model”

This is a detailed analysis of how multi-threaded assertions actually work by modeling them as fork/joined SystemVerilog tasks. This obviously isn’t how the tools actually evaluate the assertions, but by using a mechanism we’re all familiar with, I explain what’s going on under the hood of such tools. https://verificationacademy.com/verification-horizons/july-2020-volume-16-issue-2

This article explains SVA through the modeling of the underlying principles of some of its core elements using SystemVerilog procedural constructs. This modeling style emphasizes the concepts of "threads", as typically demonstrated in debug tools. The focus is in the modeling of threads for properties where both the antecedent and the consequent are sequences with range delays.

This inner-depth of SVA modeling provides a greater understanding of SVA and that appreciation will make you a more efficient SVA coder. It also makes you appreciate the value of SVA short-hand notation and how SVA is more concise and readable when defining design properties. As a bonus, this assertion modeling approach provides more insights when used in the verification process within SystemVerilog classes or to solve complex verification problems that are difficult to implement in SVA.