Assertion to check edge triggering

OVM
1

I’m trying to write an assertion to “Verify that the TMS output changes on the falling edge of TCK.” Is this possible? It sounds simple, but I’m running into a few issues.

The most obvious solution in my mind was to just see if it is $stable:

property verify_tms_negedge;
  @(negedge jtag_tck) disable iff(~rstn) $stable(jtag_tms);
endproperty
assert_tms_negedge : assert property(verify_tms_negedge) else $error(“failed assertion verify_tms_negedge”);

But this doesn’t work, and it give me assertion errors with every change of the signal. I suppose it makes sense as every full cycle could include an edge. Really I want to verify that #1ns after the negedge is the same as #1ns before the next negedge. Or I could similarly think of it as at the exact positive edge of the clock, my data should be the same 1 delta cycle later (after the data would have changed in the simulation). Or it could be 1ns later it doesn’t matter much from my perspective. I know assertions let you do #1 but that is in clock cycles- too much time without enough resolution.

I tried working around this issue by checking the posedge and the negedge and verifying that they are the same.

property verify_tms_negedge;
  logic data_val;
  @(posedge jtag_tck) disable iff(~rstn) (1,data_val = jtag_tms) |->
  @(negedge jtag_tck) (jtag_tms == data_val);
assert_tms_negedge : assert property(verify_tms_negedge) else $error(“failed assertion verify_tms_negedge”);

But this doesn’t work either, and still has the same question as to if the values are read before or after the setup time. (When data changes on the negedge, would jtag_tms read the old or new value).

Anyone have any ideas or suggestions?

2

Just a followup, the second part actually worked. It was misleading because I had some outputs that werent supposed to be checked. When a read occurs on a transition from 1->0 or 0->1, it reads the variable BEFORE the assignment, so I can use that to my advantage in the assertion.

My final assertion was:

property verify_tms_negedge;
  logic data_val;
  @(posedge jtag_tck) disable iff(~rstn) (jtag_tms_oe,data_val = jtag_tms) |->
  @(negedge jtag_tck) (jtag_tms == data_val);
assert_tms_negedge : assert property(verify_tms_negedge) else $error(“failed assertion verify_tms_negedge”);

(It also required a bit of RTL modification in the DUT).

3

In reply to spartanthree:

that was helpfull. thank you

4

In reply to spartanthree:

Can you please explain what does jtag_tms_oe,data_val = jtag_tms do ?

Thank you

5

In reply to ML_Burn:

When the expression jtag_tms_oe is true, make an assignment to the local variable data_val.

See section 16.10 Local Variables in the IEEE 1800-2017 SystemVerilog LRM