I am trying to write an SVA assumption that essentially says that if the audio_enable signal gets deasserted, then there are three signals that should not change for 10 cycles.
It didn’t work as I expected. The codec_dto_base signal gets asserted about 2 clock cycles after the audio_enable signal gets deasserted. Any suggestions?
Updated as local is reserved word.
create the common property
property drive_const(sig) ;
bit local_val ;
@(posedge clk) //
($fell(HDA_audio_stream_data.audio_enable), local_val = sig) |=> (sig == local_val)[*10]
endproperty
assume property(drive_const((HDA_audio_stream_control.codec_dto_base))
assume property(drive_const((HDA_audio_stream_control.codec_dto_multi))
assume property(drive_const((HDA_audio_stream_control.codec_dto_div))
“local” is a SVG reserved word. Try changing “local” to “lcl” or to “local1”.
Whether the compiler accepts it or not, it si not a good idea to use reserved words for variable names; it’s confusing.
Why are you flagging the constraint as an error? Formal is saying that the design cannot be satisfied with this constraint; loosen the constraint or update the design.
??
Sorry Ben. I don’t get what you are saying. The assume directive says to formal that the inputs are constrained. It says nothing about the design cannot be satisfied with the constraint. The counter example shows an input sequence that I have constrained so that it doesn’t happen. The assertion failure is relative to the outputs doing something that I do not expect but the case is not valid because of the illegal input sequence.
Does the entire model only transition on posedge socclk? Maybe you’re seeing glitches on a negedge between posedges in the assume? An SVA assume only controls the specified edges;
if I have an assume like *fell(x) then y[10] there could be a an assertion failure with a sequence shorter than the assumed constraint. For example, (fell(x) |-> y[*3] ##1 c). Having an assumption of y repeated 10 times does not stop a sequence like
fell(x) to be true, y repeated 3 times, and c==0.
In reply to dplumb_amd:
I saw that after the fall of audio_enable the signal codec_dto_base was not repeated.
I consulted with a colleague who is an expert in FV. His take:
I guess that confirms my hypothesis. If stuff can happen between edges of the designated clock, he should modify the assume to act on both edges of the fastest clock : @(fastclk) instead of @(posedge slowclk). Alternatively, SVA also offers the asynchronous reject_on operator if you want to catch such things… but I’m not sure how well tools support this rarely used op.
Hi peter,
The waveform is generated by the formal tool as a counter example for an assertion that I have not shown. But the reason why I am mystified is because the input signals seem to be violating the constraint that I coded in my original question.
