SVA with combinatorial gates with delay

SystemVerilog
, ,
1

Hi,
I am trying to write my first set of assertions and I can’t figure out a good way to describe the intended behaviour. The design is an error detection and correction flip-flop, that should detect timing violations. The timing behaviour can be seen here: https://www.researchgate.net/figure/Timing-behavior-of-the-proposed-EDACFF_fig3_340603856
So one sets up a detection window(dw) where no change of the input of the flipflop(Data) is allowed. Changing the value of the ff triggers a rise in “edge”. If edge is high while dw rises error should go up. ERR and SW should go up afterwards triggered by negedge clk_gated and posedge clk_sw respectively and stay high for one cycle of the metioned clks. SW being high supresses the next high phase on both clk and dw. Since assertions should be written as abstract as possible I would like to write 2 Assertions. The first one should assert that if sw is high neither dw nor clk should be. This is easy (I think) and should be dealt with by assert((!(SW&&DW))&&(!(SW&&CLK))). Or that is what i hope.
But the second one really drives me crazy: if data changes time x before clk_gated Final Error should rise after clk_gated rose. I have 0 idea how to incorporate the timespan. The only idea I had so far is to write: assert property @(posedge DW) Edge |-> ERR,SW; endproperty. But this would require Edge and dw to work correctly in the first place, so I think it is not ideal. Or should I just write two more assertions to ensure Edge and DW are working? I would appreciate any help pointing me in the right direction.
Thanks, Fabian

2

In reply to Balerion:
Looking at your definition of the assertion // if data changes time x before clk_gated Final Error should rise after clk_gated rose I see the following method of construction for the assertion. SVA is not going to work here because of the samplings and clocks.


    realtime t1, diff=2ns; 
    always @(data) begin 
      t1=$realtime; 
      @(posedge clk_gated) if (($realtime-t1) > diff) 
        #1 am_ferror: assert(final_err); // The #1 is to account for a delay till final_err rises
    end

Basically, you’need to build your own model.
Instead of the always I started with a task that is fork-join_none with a trigger, as I explain in my paper Understanding the SVA Engine (see link below).
However, I could not think of an appropriate trigger since the @(data) would work.
Anyway, this may provide you with some possible approaches, particularly since you understand the problem better than me.

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

** 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 | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
3

In reply to ben@SystemVerilog.us:

Hi Ben,
thanks for the informations. I tried something different and even more abstract. This is esentially a D-FlipFlop. All it should do is write the input into the output at the rising clokc edge. So I am thinking about a construct like this: @posedge of clk store the value of Data and next posedge Q should match my stored Data. Or Q should match the Data from previous cycle. Since only the rising edge of the clock can change my data of the output it has to stay the same until my next posedge. And if I write an assertion it will take the stored value of Q to test my assertion, meaning if Q changes at that rising edge it will take the “old” value right? I will try to write this and simulate it. As soon as I have results I will post them

4

In reply to Balerion:
You are correct in expressing the assertions from a requirementspoint of view rather than an implementation viewpoint. In my response, I was addressing your requirements of if data changes time x before clk_gated Final Error should rise after clk_gated rose.
I do prefer your new approach.
Ben SystemVerilog.us