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
53
54
55
|
#!/usr/bin/env 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 'async2sync' \
-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 'async2sync' \
-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 'async2sync' \
-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
|
