Synthesizable subset of SVA

SystemVerilog
,
1

Hello,

Is there an advertised subset of SVA that is synthesizable? Or is it vendor dependent? In particular are $rose and $fell synthesizable?

Thanks.

2

In reply to a72:

subset of SVA that is synthesizable?

SVA is NOT for logic design or the synthesis of logic designs.
I am not aware of any tool that can go from SVA to RTL.
SVA is for verification. Maybe you meant the following question:
Is there an advertised subset of SVA for formal verification?

  1. The subset is tool dependent (contact vendor). However, there are general guidelines that I believe hold for most vendors. Before getting into this, a quick review and requirements on this topic of formal, particularly model checking.
  2. Model Checking: This is a technique that extracts mathematical equations from the design and the properties and tries to prove/disprove the equations.
    In model checking, properties (written in a property language, like SVA) are used to capture the design intent. A formal verifier reads in an RTL design and builds a state transition graph for the system in a manner similar to an FSM. A first and foremost requirement for Model Checking is that designs need to be synthesizable and cycle-based. A natural limitation of such an approach would be that designs that contain elements such as phase-locked loops (PLLs), behavioral memories, etc. cannot be converted into logic equations, thus they can’t be proven using the formal engines. Typically, a model checker treats non-synthesizable blocks as black-boxes, making the outputs of those blocks free-ranging variables (meaning that they can have any random value), unless built-in models are available for those black boxes.
    The Verifier then reads in the properties and directives. Typically these properties represent the design specification as temporal sequences (such as a request to grant protocol, illegal transitions), and they specify whether these properties hold forever or during a finite time. A Model Checker then checks whether the design implementation obeys these properties by searching the entire state space of the design, and produces counterexamples if the design fails to obey the properties.
    By definition, FV is a complete proof, and hence is the ultimate verification methodology – if applicable. However, FV suffers heavily from the state space explosion problem for larger designs because it needs to search a very large number of states. An acceptable methodology is to limit the analysis to blocks of manageable size by partitions (i.e., smaller blocks) or by imposing constraints via the restrict operator to limit the scenarios for convergence on a proof (see 4.5.1.3). The assume construct should also be used to specify legal input states; this would avoid a failure due to some sequence of inputs that would not happen in the real world.
  3. Types of assertions best for Formal verification. Assertions can be classified as control or data intensive.
    o Control type of assertions deal with operations with regards to the generation of signals such as read/write/enable/invalidate controls, or bus protocol controls, such as request/acknowledge/hold.
    o Data intensive assertions deal with contents of memories or the result of arithmetic operators (i.e., +, -, *, /), matrix operators, fast Fourier transform (FFT), etc.
  4. Model Checking works best for control type of assertion.
    Formal verification is in contrast to simulation-based methodologies that rely on the application of test vectors, and on the observation of results as compared to expected behavior. That observation is typically performed with a verifier model that understands the protocols, transactions, and expected results.
    FPV works in almost the opposite fashion: it tries to “break” the system (or violate the expectations) by applying as many possible legal input combinations, as constrained by the assume statements and/or other constraints. While this approach sounds great, it has its own set of issues: the necessity to eliminate illegal input combinations, and the need to specify the “expected behavior” in a formal manner that can be interpreted by the tools.
    As a general guideline (again, tool dependent), keep the range of delays bounded (e.g., a ##[1:20] b) is generally better than unbounded (e.g., [0:$]). Evaluating the value of data registers should be kept to a minimum or at least to smaller register widths (e.g., 2 bits vs 32 or 54 bits).
    SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy addresses another limitation in using local variables as counters with the first_match() operator. Again, this is tool-dependent, and we don’t address specific tools in this forum. It’s OK to address tools in generalities or trends.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/