Assume statement

The assume statement allows properties to be considered as assumptions for dynamic simulation tools and formal analysis.

For a simulation environment, assume the statement is the same as an assert statement that checks assumed property and reports success or failure.

For formal analysis, an assumed property can be considered as a hypothesis to prove asserted property without having any bound.

Syntax:

<assume_label>: assume <property>

Assume in Simulation and Formal Verification

In simulation, an assumption is checked like a concurrent assertion. A violation indicates that the stimulus did not follow the expected rule.
In formal verification, an assumption restricts the traces that the formal engine considers. Only behavior satisfying the assumption is used while proving assertions.
Assume only environment behavior. Assuming a DUT result can hide a real design bug by removing the failing trace.

In simulation, an assumption failure often points to invalid testbench stimulus. In formal analysis, an assumption that is too strong can make a proof pass for the wrong reason.

Assume stememt example

Whenever req1 is high, the environment must make req2 high two clock cycles later.

property prop;
  @(posedge clk) req1 |-> ##2 req2;
endproperty

assume_a2: assume property (prop);

// Equivalent inline form
assume_a1: assume property (
  @(posedge clk) req1 |-> ##2 req2
);

The named and inline forms express the same rule. The named property is easier to reuse, while the inline form keeps a short one-time rule close to its assumption label.

Cover statement

The cover statement is used to gather coverage information for the specified sequences or properties.

A cover property statement observes a sequence or property and records a hit when it succeeds. It does not require the behavior to occur, so the absence of a hit is not an assertion failure.

Syntax:

cover property (<sequence>) <statement_or_null>

In simulation, coverage reports typically show attempts and successful matches. In formal verification, a cover property asks the engine to find a trace that reaches the covered behavior.

The result of the coverage statement shall include

For a property	For a sequence
The number of times property attempted, failed, or succeeded (even due to vacuity which is applicable only for implication operator).	The number of times a sequence attempted and matched.
For a successful property, statement_or_null is executed every time.	For every match, statement_or_null gets executed.

Cover statement example

A coverage hit is recorded when a request is followed by a response on the next clock.

property prop;
  @(posedge clk) req1 ##1 req2;
endproperty

cover_prop: cover property (prop)
  $display("The prop property is hit");

The direct sequence requires req1 to occur before a hit is counted. When prop succeeds, the coverage count increases and $display runs. If the behavior never occurs, the cover remains unhit and no failure message is generated.

Cover Property and Functional Coverage

Use cover property for temporal scenarios such as a request followed by a response. Use covergroups and coverpoints when the goal is to measure sampled values, ranges, transitions, and crosses. These two coverage mechanisms answer different verification questions.