Interview Questions on Assertions

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:

  1. We use within operator to see a does not go high, but does within operator does not guarantee for the statement from the cycle after sig_b until the cycle before the sigc_c as the sequence on lhs of within can fall anywhere between start and end of rhs. Also, can we use until for this ?
$rose(b) |-> (!a until (b[->1) ##[1:$] c[->1]))
  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 ?

  2. 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.