changed.sby

[options]
mode bmc

[engines]
smtbmc

[script]
read -formal changed.v
prep -top changed

[files]
changed.v

changed.v

module changed(i_clk, i_x, o_test);
	parameter	W = 4;
	input	wire	i_clk;
	input	wire	[W-1:0]	i_x;
	output	wire	[3:0]	o_test;

	reg	f_past_valid;
	initial	f_past_valid = 1'b0;
	always @(posedge i_clk)
		f_past_valid <= 1'b1;


	always @(posedge i_clk)
	if (f_past_valid)
	begin
		o_test[0] = ($stable(i_x)  == (i_x == $past(i_x)));
		o_test[1] = ($changed(i_x) == (i_x != $past(i_x)));
		o_test[2] = ($rose(i_x)    == (( i_x)&&(!$past(i_x))));
		o_test[3] = ($fell(i_x)    == ((!i_x)&&( $past(i_x))));

		assert(o_test == 4'hf);
	end

	always @(posedge i_clk)
	if (i_x && 1'b1)
		assert(i_x[0]);
	else
		assert(!i_x[0]);

endmodule