yosys/tests/sva/sva_value_change_changed.sv

module top (
	input clk,
	input a, b
);
	default clocking @(posedge clk); endclocking

	assert property (
		$changed(b)
	);

	wire x = 'x;

`ifndef FAIL
	assume property (
		b !== x ##1 $changed(b)
	);
`endif

endmodule
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 2022-05-09 08:04:01 -05:00			`module top (`
			`input clk,`
			`input a, b`
			`);`
			`default clocking @(posedge clk); endclocking`

			`assert property (`
			`$changed(b)`
			`);`

Fix sva_value_change_changed test for updated verific 2023-10-03 04:46:43 -05:00			`wire x = 'x;`

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 2022-05-09 08:04:01 -05:00			`ifndef FAIL
			`assume property (`
Fix sva_value_change_changed test for updated verific 2023-10-03 04:46:43 -05:00			`b !== x ##1 $changed(b)`
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 2022-05-09 08:04:01 -05:00			`);`
			`endif

			`endmodule`