Writing SystemVerilog assertion for checking "setup/hold time violation" type of conditions

Recently, I gave couple of internal lectures on basic and advanced features of SystemVerilog assertion at the organization that I am working at. After that, quite a few colleague of mine have started asking questions on SVA. Amongst all, the most interesting assertion question is how to write assertion for checking "setup/hold time violation" type of scenarion. To understand these scenario, let's start with a very common example, which can be extended for many similar case.

Problem statement:

Write assertion for checking that the signal "data" is stable for tSetup time before positive edge of clock, and should be stable for tHold time after positive edge of clock. Here tSetup/tHold will be of static delay like 1ns, 30ps or so on. There are no extra inherent assumptions added with it (like clock period, its relationship with tSetup/tHold, or how fast the signal data can toggle.

This is a standard problem, with not so easy solution of writing assertion for it

In Verilog there is a way of checking it, which unfortunately is not an assertion, and hence can't be used with formal tools like Jasper. (via http://www.edaboard.co.uk/requesting-help-on-writing-sv-assertions-t442372.htmlhttp://www.edaboard.co.uk/requesting-help-on-writing-sv-assertions-t442372.html)

module timing_checks (input clk, en); 
  specify 
    specparam clk_high_time = 5; 
    specparam clk_low_time = 5; 
    $setup(en, negedge clk, clk_high_time * 4 / 5); 
    $hold(negedge clk, en, clk_low_time * 4 / 5); 
  endspecify 
endmodule 

Now let's proceed with assumption that we want to write an assertion for checking the same, we are not very much happy with $setup/$hold of Verilog. Here is the solution

module timing_checks_in_sv (input clk, data, ...); 
  ...
  event ev_data_delayed_toggled;
  
  always @(data)
  begin
    fork
    begin
      # tSetup;
      -> ev_data_delayed_toggled;
    end
    join_none
  end

  property setup_hold_time_checker;
    time curr_time;
    @(posedge clk) (1, curr_time = $time) |->
    @(ev_data_delayed_toggled) (($time - curr_time) > (tSetup + tHold));
  endproperty : setup_hold_time_checker

  ASSERT_SETUP_HOLD: assert property setup_hold_time_checker;
endmodule 

In the always block, we are triggering an event called ev_data_delayed_toggled, after tSetup time every time data toggles. Now the "setup/hold time" problem statement can be written as after posedge of clock, ev_data_delayed_toggled shouldn't get triggered within tSetup+tHold time. Now the problem statement has come to a form SVA timing check, which is specified in via the property.

There are many such not so intuitive, interesting use-case scenarios for SVA. Interested readers can have a look at the below link for some more interesting scenarios.

• http://www.verilab.com/files/sva_gate_paper_dvcon2006.pdf