🔗 What are Concurrent Assertions?#
Concurrent assertions are used to check temporal (time-dependent) behaviors. These assertions are triggered based on a clock or event and check conditions that span over time. They can be defined using property blocks or written inline.
Example (with property block):
property p1;
@(posedge clk) req |=> ack;
endproperty
assert property(p1);
Example (inline property):
assert property (@(posedge clk) req |=> ack);
👉 Note: You don’t have to write the property block separately; writing it inline can simplify the code for shorter expressions. However, for longer or reusable properties, writing a separate block improves readability.
🏗️ Property Blocks#
When writing concurrent assertions, behaviors can be defined using property blocks. A property is basically a temporal expression or a chain of sequential conditions.
Example:
property p_ready;
@(posedge clk) (req ##1 ack);
endproperty
In this example, after the req signal is asserted, the ack signal is expected one cycle later.
🔖 Naming and Asserting the Property#
Property blocks can be named and reused. Assertion calls then refer to this property.
Example:
property p_req_ack;
@(posedge clk) req |=> ack;
endproperty
tag_name : assert property(p_req_ack);
This way:
- The same property can be used in multiple assertions.
- We can use
assume,cover,restrict, etc. to write different control types.
⏲️ Clocking the Property#
Concurrent assertions are clock-sensitive and require a clock definition to synchronize with the design. The clock is defined in the property block using:
@(posedge clk)or@(negedge clk)
Example:
property p_enable_check;
@(posedge clk) disable iff (reset)
(enable |-> ##1 data_valid);
endproperty
⚙️ Default Clock Statement#
If we use multiple properties, instead of specifying the clock each time, we can use default clocking. This provides a global clock definition at the testbench or design level.
Example:
default clocking cb @(posedge clk);
endclocking
property p_example;
req |=> ack;
endproperty
assert property(p_example);
In this case, the p_example property is automatically clocked by the clk signal, simplifying the code.