SVA BIND 读书笔记

1 Introduction

This paper details some SVA methodology techniques that I highly recommend, especially for design engineers

what should never happen using "not sequence" assertions is even more important than using assertions to describe always true conditions.

Immediate assertions
   execute once and are placed inline with the code

Concurrent assertions
   are the most valuable and most widely used type of assertion

2 Long Labels 

The long labels help to debug the assertions in a waveform display

3 Immediate Assertions 

There are a couple of places where Immediate Assertions can be quite useful
  Dynamic casting with immediate assertion
  Randomization

where user care about success or fail of these SV methods

4 Concurrent Assertions

The most valuable assertion style is Concurrent Assertions

5 Concise Assertion Coding Styles

useful techniques
  (1) to define default clocking blocks and always blocks that will disable
      assertions during reset

  (2) use simple macro definitions
     The concise `assert_clk and `assert_async_reset macros significantly reduce the
     effort required to add assertions to an RTL design

6 SVA Bind Files

bind an SVA file to the golden model that cant be modified
bind can be done with both Verilog and VHDL RTL files

SVA bind files require that:
  the assertions be wrapped in a module that includes port declarations
  // fifo1 u1 (.*);
  // bind fifo1: u1 pLib_fifo p1 (.*);
  // bind fifo1: u1 pLib_fifo p1 (.a(A).b(B));

7 SVA File Methodologies

Using assertions with an RTL file:
  adding
  include
  instanciate
  bind

To preserve the same assertions in the gate-level design after synthesis
  dont use adding

8 Summary & Conclusions

Concised Assertion Style using macro is recommended
Bind Assertion is useful

9 Acknowledgements

10 References

11 Author & Contact Information

12 Appendix

12.1 Synchronous FIFO assertions
  Asynchronous reset assertion
  FIFO full condition assertions 
    ...
  FIFO empty condition assertions 
    ...
  The FIFO cnt (word count) should never be negative
  If read & write occur at the same time, the FIFO should not be full or empty.

12.2 Separate property and assertion style
12.3 Combined assert property style
12.4 Assertion macro style