for a non-overlap sequence detector of 1101,
I wanna have 2 assertions to test it
1: upon seeing 1101 sequence, detected should be asserted.
2: if detected is asserted, past sequence should be 1101.
question1:
for a sequence of 1101101, since it’s non-overlap, detected will only asserted on 1101(detcted)101, but assertion will fail on the latter part of the sequence, meaning this property actually describes 1101(detcted)101(detected). how can I prevent this issue?
property upon_det_seq1101;
@(posedge clk) @rose(detected) |-> // past sequence should be 1101.
endproperty
question2:
My initial feeling is to finish this assertion with $past function, but I don’t know how to implement it, or maybe there’re some nicer way?
A useful comment by a colleague.
Should you shift it into log from the right?
Also, I am not sure about the actual requirement. Is it to detect the sequence to be used somewhere, or fail any time it does not match?
I think for detection it would be better to use a cover and use the action block to signal it to whatever needs this info.
[Ben] I agree with the use of the cover instead of the assert.
As to the direction of the shift, you are correct.
In any case, the approach is correct.
upon detected assertion, sequence detector fsm would return to initial stage, so it’s safe to kill current thread and make it vacuous I think
bit detected;
@(posedge clk) sync_accept(detected) sequence_in ##1 sequence_in ##1 !sequence_in ##1 sequence_in |=> detected;
I presume that you have an FSM that sets/resets the bit detected.
The assertion as you wrote would not compile because the ! in !sequence_in is a logical operator. You cannot use the not in … ##1 sequence_in ##1 not(sequence_in) because the not is a property operator. To fix that you can write
Now on the accept_on. !800’2017 says:
*The accept_on/reject_on family of operators just terminates the property as an accept (true vacuously, with no contribution to the pass statistics) or reject (false vacuously, with contributions to the failed statistics).
The accept_on (expression_or_dist) property_expr accepts the property as true if the expression_or_dist (called the abort condition) is true. Otherwise, with the abort condition as false, the property expression evaluates to completion. The abort condition with the accept_on is asynchronous, whereas the sync_accept_on is synchronous to the clock under current consideration for the property. Unlike disable iff, the synchronous abort condition is sampled during the Preponed sampling region for properties.*
You do not need it in this case, as it does nothing for you. All it does for you is kill the first attempt after detected==1. At every clocking event you start evaluating the sequence: sequence_in ##1 sequence_in ##4 !sequence_in.triggered ##1 sequence_in
Here is an example of the accept_on. Note that when done occurs at any time, even within the repetition cycles, the assertion is true.