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?

  • hardware26@discuss.tchncs.deEnglish
    1·
    2 months ago

    You can use auxiliary code. It is usually more readable and less error prone that multi-trigger assertions. Something like: always @(negedge adc_sample) true_voltage <= input_channel; assert property(@(posedge clk) adc_data_en |-> adc_data == true_voltage); Note that behaviour is not completely equivalent, for example as long as adc_data_en is highassertion will keep matching, not only once when adc_data_en rises. If you want thevoriginal behaviour you can use $rose(adc_data_en). Auxiliary code also makes it easier for 20 delay case. For example you can clock the always block with posedge clock and use a 20-size shift-register which is conditionally enabled if adc_data_en in low. I am not sure of the intended behaviour so take it with a grain of salt.