In reply to ben@SystemVerilog.us:
Hello Sir, Understood what you described. But I want to know if I have written any wrong assertion . Because it looks okay to me.
In reply to ben@SystemVerilog.us:
Hi, I was just observing your solution. And I think, I got another way to write an assertion for Question:- 05.
// Question - If there are two occurrences of sig a rising with state=ACTIVE1,
// and no sig b occurs between them, then within 3 cycles of the second rise of sig a, START must occur.
property p1;
rose(a) && state == ACTIVE1 ##1 !b[*1:] ##1 $rose(a) && state == ACTIVE1 |-> [1:3]state == start;
endproperty
assert property (p1);
Could you tell me whether I can do it or not?
I got a couple more queries.
- In question - 7, you used two ways to write the code. In the 2nd one, I assume that you
missed writing b |->. Probably after this ( not (!$rose(a) && c) ) fits well.
I got another solution, I guess. Please look into that.
b|-> !$rose(a) until c;
- In question - 8, You have solved it considering "… must appear … ". But the
problem says “… may appear…”. And, I think it’s correct. I tried something. Please look into this too.
!a[*1:$] |-> b[=0:1] ##1 a;