SystemVerilog Assertions (SVA) provide a structured way to express design requirements and protocol behaviour.
In a large verification programme, many requirements appear repeatedly across different blocks.
Examples include valid-ready handshakes, reset behaviour, request-grant protocols and FIFO control.
Developing reusable property templates can improve consistency and reduce repetitive work.
Example: Valid-ready handshake
Consider a valid-ready interface.
When valid is high and ready is low, the sender is generally expected to keep valid asserted and maintain the payload until the receiver accepts the transfer.
An illustrative property is:
property p_valid_stable; @(posedge clk) disable iff (!rst_n) (valid && !ready) |=> (valid && $stable(payload)); endproperty assert property (p_valid_stable);
This checks that, after a cycle in which valid is high and ready is low, valid remains high and payload remains stable in the next sampled cycle.
The exact property must be adapted to the interface specification, reset architecture and sampling requirements.
The disable iff construct provides an asynchronous assertion-disable condition. It should not be treated as a substitute for understanding the design's reset behaviour.
What makes a property reusable?
A reusable property should have:
- Clearly defined input and output signals
- Documented protocol assumptions
- Configurable clock and reset handling
- Defined sampling behaviour
- A clear assertion or assumption role
- Known limitations and supported use cases
A template should not be copied into every block without checking the local interface contract.
Assertions and assumptions must be distinguished
The same protocol condition can be an assumption in one verification environment and an assertion in another.
For example, when verifying a receiver, the sender's behaviour may be constrained by assumptions.
When verifying the sender, the receiver's behaviour may be constrained instead.
The verification boundary determines which conditions are assumed and which are checked.
Build a property library progressively
A useful library can begin with common interface requirements:
- Reset behaviour
- Valid-ready handshakes
- Request-grant protocols
- FIFO overflow and underflow prevention
- Arbitration requirements
- State-machine transition checks
- Counter and timer behaviour
- Interrupt and status conditions
Each property should include a description, intended use, assumptions and a simple example.
Review and maintenance
Reusable properties still require review.
Engineers should check:
- Whether the property matches the specification
- Whether its antecedent is reachable
- Whether assumptions are justified
- Whether the property is compatible with the selected formal engine
- Whether reset and clocking semantics are correct
A property library should be version-controlled and updated when protocol definitions or verification requirements change.
Conclusion
Reusable SVA libraries can improve consistency and reduce repetitive assertion development.
Their value comes not simply from reusing code, but from reusing reviewed verification intent while adapting each property to the actual design specification.
