FPGA

245 readers

1 users here now

A community for programmable hardware, including topics such as: * FPGA * CPLD * Verilog * VHDL

Related communities:

founded 2 years ago

MODERATORS

hardwareteams@lemmy.ml

How can I improve this hacky SV assertion? (programming.dev)

submitted 1 month ago by iliketurtiles@programming.dev to c/fpga@lemmy.ml

3 comments fedilink hide all child comments

This is for an ADC. What I'm trying to do: when adc_sample goes low, grab hold of a value. Then when adc_data_en goes high, compare it with adc_data. Here's what I have so far:

    property adc_deduces_voltage;
        bit [7:0] true_voltage;

        @(negedge adc_sample) (`true,true_voltage=input_channel) 
        ##1 @(posedge adc_data_en) 
        // Values are sampled in the prepond region. This would be before
        // adc_data_en is high, giving us old values. To make up for this, wait
        // for one more clock cycle so that sampled values will be just after
        // adc_data_en is high.
        ##1 @(posedge clock) (adc_data == true_voltage, $display("Pass. Actual: %d, ADC: %d", true_voltage, adc_data);
    endproperty
    assert property (adc_deduces_voltage);

Note the comment I inserted. The hacky bit of my code is waiting for the next rising edge of the clock so that I can avoid the issue of things being sampled in the prepone region.

Any thoughts on improving this? Is there a better way to do this?

Also, what if I wanted to do something like: wait for negedge adc_sample, then posedge adc_data_en then 20 clock cycles later carry out checks?

you are viewing a single comment's thread
view the rest of the comments

[–] hardware26@discuss.tchncs.de 1 points 3 weeks ago* (last edited 3 weeks ago)

Both antecedent and consequent are sampled at preponed region. So assertion will not trigger at the edge where adc_data_en rises. This is the intention, since the value of adc_data or adc_data_en do not matter at the edge where adc_data_en rises, but they do matter in the following edge where the D for the flops calculated based on adc_data and adc_data_en are registered. All these are assuming adc_data_en and adc_data are synchronous to the clock. Edit: Adding to this, if you want adc_data_en to be evaluated in observed region, you can do something like this: property(@(posedge clk) disable iff (!adc_data_en) adc_data==true_data); However I would not recommend this. One reason is that, at the cycle where adc_data_en falls this checker will not fire, but it probably should. Second reason is that, at the edge where adc_data_en rises, this assertion may work in RTL sim with no timing delays or hold/setup time, but it will fail in a realistic gatevlevel simulation. As a rule of thumb synchronous signals should be used inside property where they are evaluated in preponed region.