mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 03:32:29 +00:00
331ac5285f
Right now neither `sat` nor `sim` have support for the `$check` cell. For formal verification it is a good idea to always run either async2sync or clk2fflogic which will (in a future commit) lower `$check` to `$assert`, etc. While `sim` should eventually support `$check` directly, using `async2sync` is ok for the current tests that use `sim`, so this commit also runs `async2sync` before running sim on designs containing assertions.
55 lines
1.4 KiB
Bash
55 lines
1.4 KiB
Bash
#!/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
|