aboutsummaryrefslogtreecommitdiffstats
path: root/tests/various/chparam.sh
blob: 9bb8d81db6adcdf187aaeb28a80a34d4a7464f04 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
#!/bin/bash

trap 'echo "ERROR in chparam.sh" >&2; exit 1' ERR

cat > chparam1.sv << "EOT"
module top #(
        parameter [31:0] X = 0
) (
        input [31:0] din,
        output [31:0] dout
);
        assign dout = X-din;
endmodule

module top_props #(
        parameter [31:0] X = 0
) (
        input [31:0] dout
);
        always @* assert (dout != X);
endmodule

bind top top_props #(.X(123456789)) props (.*);
EOT

cat > chparam2.sv << "EOT"
module top #(
	parameter [31:0] X = 0
) (
	input [31:0] din,
	output [31:0] dout
);
	assign dout = X-din;
	always @* assert (dout != 123456789);
endmodule
EOT

if ../../yosys -q -p 'verific -sv chparam1.sv'; then
	../../yosys -q -p 'verific -sv chparam1.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
			-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
			-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'

	../../yosys -q -p 'verific -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
			-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
			-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
fi
../../yosys -q -p 'read_verilog -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
		-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
		-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'

rm chparam1.sv
rm chparam2.sv