🔗 Property Reuse in SystemVerilog#
In SystemVerilog Assertions (SVA), property reuse is a key technique for writing modular, scalable, and maintainable assertions. By leveraging parameters, arguments, and reusable constructs, you can cover multiple scenarios with a single property definition—greatly improving code readability and efficiency.
🛠️ Properties with Arguments#
Properties can accept inputs (arguments) just like functions, allowing them to adapt dynamically to different signals, clocks, and conditions.
Example:
property p_handshake(req, ack);
@(posedge clk) req |=> ack;
endproperty
Here:
req
andack
are inputs to the property.- You can apply this same property to different signal pairs by passing arguments.
⚡ Using Parameters Inside Properties#
Properties can also use parameters to adjust internal behavior, such as delays or thresholds. As an example delay input as below.
Example:
property p_handshake(logic req, logic ack, int delay);
@(posedge clk)
req |=> ##delay @(posedge clk) ack;
endproperty
Here:
delay
is a parameter that lets you control the wait time betweenreq
andack
.
🔄 Using Properties in Loops with generate
#
To apply a property across multiple instances—such as verifying a bus, channels, or cores—generate blocks are extremely useful.
Example:
generate
genvar i;
for (i = 0; i < NUM_CHANNELS; i++) begin : gen_handshake_check
assert property (p_handshake(req[i], ack[i]));
end
endgenerate
This:
- Applies the same assertion to all channels.
- Reduces code duplication and simplifies maintenance.
🔗 Assertion Binding#
Assertion binding lets you attach assertions to design modules without modifying the RTL source code. This makes it easier to apply reusable properties externally.
Example:
// Modül Tanımı
module my_module (
input wire clk,
input wire rst_n,
input wire [3:0] data
);
// Bir örnek sinyal
wire [3:0] internal_data;
assign internal_data = data + 1;
endmodule
// Assertion Tanımı
module assertion_module (
input wire clk,
input wire rst_n,
input wire [3:0] data,
input wire [3:0] internal_data
);
// Assertion: internal_data, data'dan bir fazla olmalı
assert property (@(posedge clk) disable iff (!rst_n)
(data + 1) == internal_data)
else $error("Assertion failed: internal_data is not equal to data + 1");
endmodule
// Bind İfadesi
module top;
bit clk;
bit rst_n;
bit [3:0] data;
// Saat sinyali oluşturma
always #5 clk = ~clk;
// Reset sinyali oluşturma
initial begin
rst_n = 0;
#10 rst_n = 1;
end
// Örnek veri sinyali
initial begin
data = 4'b0000;
#20 data = 4'b0001;
#20 data = 4'b0010;
#20 $finish;
end
// Modül örneği
my_module my_module_inst (
.clk(clk),
.rst_n(rst_n),
.data(data)
);
// Assertion'ı modüle bağlama
bind my_module_inst assertion_module assertion_inst (
.clk(clk),
.rst_n(rst_n),
.data(data),
.internal_data(my_module_inst.internal_data)
);
endmodule
This:
- Binds the property
p_handshake
to thedut
module’sreq
andack
signals. - Allows adding or removing assertions without changing the design’s internal code.