SVA check for glitch/noise

SystemVerilog
,
2

In reply to VerifEx:
One major problem I see in your assertion is your misuse of the $stable.

$stable returns true if the sampled value of the expression did not change between the sampled value at the previous cycle and the sampled value at the current cycle. Otherwise, it returns false. $changed is a complement to $stable; $changed returns true if the sampled value of the expression changed. Otherwise, it returns false.

With ($stable(tx_rx)[*16])[*20] you are expressing that tx_rx is stable the whole 20 data bits; not what you want. I suggest the following, but I also have addinonal comments.


ap_1: assert property (@(posedge sample_clk) (state == start_bit) |-> check_glitch); 
sequence check_glitch;
   @(posedge sample_clk) (1'b1 ##1 $stable(tx_rx)[*15])[*20];
// Thus, tx_rx can change value 
endsequence

There is one major issue with your assertion of a UART-like data transmission: There could be jitter in the data stream, or essentially, an uncertainty in the syncing of the data between the transmission and the reception. This is why you have this 16x clock. The point here is that the data transmission could be correct, but there could be regions of uncertainties. One option to satisfy this uncertainty zone could be to test your stability region in a narrower zone. For example:


ap_2: assert property (@(posedge sample_clk) (state == start_bit) |-> check_glitch); 
sequence check_glitch;
   @(posedge sample_clk) (1'b1 ##3 $stable(tx_rx)[*13])[*20];
// Thus, tx_rx can change value 
endsequence

I wrote the following paper that uses the UART as a model:
Assertions Instead of FSMs/logic for Scoreboarding and Verification
https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3/Assertions-Instead-of-FSMs/logic-for-Scoreboarding-and-Verification

Assertions with function calls from sequence match items can be used to generate that bit-clock as extracted using the 16x-clock and the start frame synchronization information; this novel application of assertion statements is demonstrated in http://systemverilog.us/uart_bit_clk_gen.pdf
All test code and test results can be downloaded from http://systemverilog.us/uart4hz.tar
The generation of bit-clock is the uart_if.sv file.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr