Lesson 3.1 · SystemVerilog Assertions Essentials

Assert, assume and cover

SystemVerilog Assertions (SVA) is the part of IEEE 1800 SystemVerilog used to describe behaviour over time. In SVA you first describe a property — a statement about signals across clock cycles — and then attach a directive that tells the tool what to do with it.

Directive	Formal tool will…	Simulator will…	Use it for
`assert property`	Try to find a legal trace that violates it	Report an error when it fails	Requirements on the design
`assume property`	Only explore traces where it holds	Check it like an assertion	Rules about the inputs / environment
`cover property`	Try to find a trace where it happens	Count how often it happens	Proving behaviours are reachable

Here is one small handshake rule used three ways. The interface: a requester raises req and must hold it until it receives gnt.

one property, three directives

// Property: once raised, req stays high until gnt arrives
property p_req_held;
  @(posedge clk) disable iff (rst)
    req && !gnt |=> req;
endproperty

// In the ARBITER's proof the requester is outside the design: it is an input rule
m_req_held: assume property (p_req_held);

// In the REQUESTER's proof the same rule is something the design must obey
a_req_held: assert property (p_req_held);

// And we want to SEE that a request can actually wait more than one cycle
c_req_waits: cover property (@(posedge clk) disable iff (rst) req && !gnt ##1 req && !gnt);

Why covers are not optional in formal

In simulation, a passing assertion at least means the test ran. In formal, an assertion can "pass" because the behaviour it checks can never happen — for instance because an assumption accidentally forbids it. Covers are your evidence that the interesting behaviour is reachable in your environment. A good habit: for every important assertion of the form A |-> B, write cover property (A).