3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-08-11 13:40:53 +00:00

verific: Improve logic generated for SVA value change expressions

The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).

This patch now generates logic that at the same time

	a) provides the expected behavior in a 2-valued logic setting, not
	   depending on any dont-care optimizations, and

	b) properly handles 'x values in yosys simulation
This commit is contained in:
Jannis Harder 2022-05-09 15:04:01 +02:00
parent 58b23954e8
commit a855d62b42
8 changed files with 121 additions and 11 deletions

View file

@ -0,0 +1,51 @@
module top (
input clk
);
reg [7:0] counter = 0;
reg a = 0;
reg b = 1;
reg c;
wire a_fell; assign a_fell = $fell(a, @(posedge clk));
wire a_rose; assign a_rose = $rose(a, @(posedge clk));
wire a_stable; assign a_stable = $stable(a, @(posedge clk));
wire b_fell; assign b_fell = $fell(b, @(posedge clk));
wire b_rose; assign b_rose = $rose(b, @(posedge clk));
wire b_stable; assign b_stable = $stable(b, @(posedge clk));
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));
always @(posedge clk) begin
counter <= counter + 1;
case (counter)
0: 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));
a <= 1; b <= 1; c <= 1;
end
1: begin a <= 0; b <= 1; c <= 'x; 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));
a <= 0; b <= 0; c <= 0;
end
3: begin a <= 0; b <= 1; c <= 'x; end
4: 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));
a <= 'x; b <= 'x; c <= 'x;
end
5: begin a <= 0; b <= 1; c <= 'x; counter <= 0; end
endcase;
end
endmodule