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 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.
Thanks for your reply, that certainly a method I will try using.
But in the case of my problem I think it won’t work. Since adc_data is in the consequent of the implication, it will again be sampled in the prepone region and so take on the value before adc_data_en was asserted high, don’t you think?
In my code I set adc_data to its new value and at the same time set adc_data_en high. Perhaps I’m not supposed to do things this way? Is the usual practice to set something like adc_data to it’s new value some time before the enable is asserted?
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.