mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-23 00:55:32 +00:00
Code Activity

Merge pull request #3314 from jix/sva_value_change_logic_wide

Browse source 
verific: Use new value change logic also for $stable of wide signals.
This commit is contained in:
Jannis Harder 2022-05-16 16:15:04 +02:00 • committed by GitHub
commit 2864f2826a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 72 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

22
tests/sva/sva_value_change_changed_wide.sv Normal file
View file

@ -0,0 +1,22 @@
module top (
input clk,
input [2:0] a,
input [2:0] b
);
default clocking @(posedge clk); endclocking
assert property (
$changed(a)
);
assert property (
$changed(b) == ($changed(b[0]) || $changed(b[1]) || $changed(b[2]))
);
`ifndef FAIL
assume property (
a !== 'x ##1 $changed(a)
);
`endif
endmodule

23
tests/sva/sva_value_change_sim.sv
View file

@ -7,6 +7,8 @@ reg [7:0] counter = 0;
reg a = 0;
reg b = 1;
reg c;
reg [2:0] wide_a = 3'b10x;
reg [2:0] wide_b = 'x;
wire a_fell; assign a_fell = $fell(a, @(posedge clk));
wire a_rose; assign a_rose = $rose(a, @(posedge clk));
@ -20,6 +22,9 @@ wire c_fell; assign c_fell = $fell(c, @(posedge clk));
wire c_rose; assign c_rose = $rose(c, @(posedge clk));
wire c_stable; assign c_stable = $stable(c, @(posedge clk));
wire wide_a_stable; assign wide_a_stable = $stable(wide_a, @(posedge clk));
wire wide_b_stable; assign wide_b_stable = $stable(wide_b, @(posedge clk));
always @(posedge clk) begin
counter <= counter + 1;
@ -28,13 +33,20 @@ always @(posedge clk) begin
assert property ( $fell(a) && !$rose(a) && !$stable(a));
assert property (!$fell(b) && $rose(b) && !$stable(b));
assert property (!$fell(c) && !$rose(c) && $stable(c));
assert property (!$stable(wide_a));
assert property ($stable(wide_b));
a <= 1; b <= 1; c <= 1;
end
1: begin a <= 0; b <= 1; c <= 'x; end
1: begin
a <= 0; b <= 1; c <= 'x;
wide_a <= 3'b101; wide_b <= 3'bxx0;
end
2: begin
assert property ( $fell(a) && !$rose(a) && !$stable(a));
assert property (!$fell(b) && !$rose(b) && $stable(b));
assert property (!$fell(c) && !$rose(c) && !$stable(c));
assert property (!$stable(wide_a));
assert property (!$stable(wide_b));
a <= 0; b <= 0; c <= 0;
end
3: begin a <= 0; b <= 1; c <= 'x; end
@ -42,9 +54,16 @@ always @(posedge clk) begin
assert property (!$fell(a) && !$rose(a) && $stable(a));
assert property (!$fell(b) && $rose(b) && !$stable(b));
assert property (!$fell(c) && !$rose(c) && !$stable(c));
assert property ($stable(wide_a));
assert property ($stable(wide_b));
a <= 'x; b <= 'x; c <= 'x;
wide_a <= 'x; wide_b <= 'x;
end
5: begin
a <= 0; b <= 1; c <= 'x;
wide_a <= 3'b10x; wide_b <= 'x;
counter <= 0;
end
5: begin a <= 0; b <= 1; c <= 'x; counter <= 0; end
endcase;
end