Interview Questions on Assertions

SystemVerilog
,
21

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;
22

Hi @subbireddy can you please share remaining 21 questions.

23

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

24

Hi, Can you provide all 30 assertion questions? It will be a very good exercise for practice.

25

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

26

@gundum , wouldn’t a simple solution be using or operator ?

sig_a |-> sig_b[->1] or sig_c[->1];
27

yeah I agree, simple and clean
trying to understand the intersect operator, does the above property mentioned by me works?