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?
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.