Hi Ben, thanks for writing the answers in a very easy SVA. Can we write the Q5 assertion this way?
ap5_aa_nob: assert property(@ (posedge clk)
($rose(a) && (state == ACTIVE1))[->2] intersect !b[*1:$] |-> ##[1:3] state == START;
Hi Ben, thanks for writing the answers in a very easy SVA. Can we write the Q5 assertion this way?
ap5_aa_nob: assert property(@ (posedge clk)
($rose(a) && (state == ACTIVE1))[->2] intersect !b[*1:$] |-> ##[1:3] state == START;
Hi @subbireddy can you please share remaining 21 questions.
Hi Ben,
I have some doubts for the solutions for 7th and 8th:
$rose(b) |-> (!a until (b[->1) ##[1:$] c[->1]))
In sol-8, what does 1’b1 intersect a[->1] mean and does b[->1] and a[->1] start and end at same time ?
Will this work for condition mentioned in q-5 ?
$rose(a) ##0 !b throughout (a && (state==active_1))[->2] |-> ##[1:3] start
Thanks in advance
Hi, Can you provide all 30 assertion questions? It will be a very good exercise for practice.
Question: Every sig_a must eventually be acknowledged by sig_b, unless sig_c appears.
Hello,
for the question above, is the below valid? I understand intersect should have same end point for both sequences/events, so i want to know if when b becomes high once, the assertion passes or not?
sig_a |-> sig_b[->1] intersect 1[*0:$] !c
@gundum , wouldn’t a simple solution be using or operator ?
sig_a |-> sig_b[->1] or sig_c[->1];
yeah I agree, simple and clean
trying to understand the intersect operator, does the above property mentioned by me works?