Chapter 3 quiz

Check yourself: SystemVerilog Assertions Essentials

Pick one answer per question, then press Check answers. Explanations appear after checking. Your best score is saved in this browser.

Q1 Which directive tells a formal tool to only explore traces where a property holds? assert property assume property cover property restrict property is never allowed

assume constrains the search. (restrict also constrains formal but is ignored by simulation.)

Q2 The spec says "gnt must be asserted one cycle after req". Which property is correct? req |-> gnt req |=> gnt gnt |=> req req ##1 gnt (as an assertion on its own)

|=> checks the consequent one tick after the antecedent. req ##1 gnt as an assertion would require req to be true on every tick.

Q3 What does ack[->2] mean? ack is high for 2 consecutive cycles. ack is high for exactly 2 cycles in total, ever. Wait until ack has been seen twice (not necessarily consecutively); the match ends on the 2nd ack. ack is delayed by 2 cycles.

This is the goto repetition. [*2] is the consecutive form.

Q4 An assertion of the form A |-> B is proven, but a cover of A is unreachable. What is the right conclusion? The design is correct. The proof is vacuous — B was never checked. Investigate the antecedent and assumptions. The cover is wrong and can be deleted. Increase the proof depth.

Q5 Why does a concurrent assertion see the "old" value of a signal that changes exactly at the clock edge? Because assertions are evaluated at the falling edge. Because concurrent assertions sample values in the Preponed region, before the edge updates them. Because of a simulator bug. Because of disable iff.

Q6 In the arbiter lab, why is a_fair written as ##[0:N-1] and not ##[0:N-2]? Because the arbiter is not fair. Because the cover c_wait_max shows a requester can wait exactly N-1 cycles, so the tighter bound is false. Because N-2 would be negative for N = 1. Because formal tools cannot handle ##[0:N-2].

Was this page helpful?

Tip: select any text on the page before clicking Report and it will be quoted in your report.