mirror of
https://github.com/YosysHQ/yosys
synced 2025-11-04 05:19:11 +00:00
ca5b910296
The `-keepdc` option prevents merging flipflops with dont-care bits in their initial value, as, in general, this is not a valid transform for formal verification. The keepdc option of `opt` is passed along to `opt_merge` now.
127 lines
1.9 KiB
Text
127 lines
1.9 KiB
Text
read_verilog -icells <<EOT
|
|
module top(input clk, i, (* init = 1'b0 *) output o, p);
|
|
\$dff #(
|
|
.CLK_POLARITY(1'h1),
|
|
.WIDTH(32'd1)
|
|
) ffo (
|
|
.CLK(clk),
|
|
.D(i),
|
|
.Q(o)
|
|
);
|
|
\$dff #(
|
|
.CLK_POLARITY(1'h1),
|
|
.WIDTH(32'd1)
|
|
) ffp (
|
|
.CLK(clk),
|
|
.D(i),
|
|
.Q(p)
|
|
);
|
|
endmodule
|
|
EOT
|
|
|
|
opt_merge
|
|
select -assert-count 1 t:$dff
|
|
select -assert-count 1 a:init=1'0
|
|
|
|
|
|
design -reset
|
|
read_verilog -icells <<EOT
|
|
module top(input clk, i, (* init = 2'b11 *) output [1:0] o);
|
|
\$dff #(
|
|
.CLK_POLARITY(1'h1),
|
|
.WIDTH(32'd1)
|
|
) ff1 (
|
|
.CLK(clk),
|
|
.D(i),
|
|
.Q(o[1])
|
|
);
|
|
\$dff #(
|
|
.CLK_POLARITY(1'h1),
|
|
.WIDTH(32'd1)
|
|
) ff0 (
|
|
.CLK(clk),
|
|
.D(i),
|
|
.Q(o[0])
|
|
);
|
|
endmodule
|
|
EOT
|
|
|
|
opt_merge
|
|
select -assert-count 1 t:$dff
|
|
select -assert-count 1 a:init=2'bx1 a:init=2'b1x
|
|
|
|
|
|
design -reset
|
|
read_verilog -icells <<EOT
|
|
module top(input clk, i, (* init = 1'b0 *) output o, /* NB: no init here! */ output p);
|
|
\$dff #(
|
|
.CLK_POLARITY(1'h1),
|
|
.WIDTH(32'd1)
|
|
) ffo (
|
|
.CLK(clk),
|
|
.D(i),
|
|
.Q(o)
|
|
);
|
|
\$dff #(
|
|
.CLK_POLARITY(1'h1),
|
|
.WIDTH(32'd1)
|
|
) ffp (
|
|
.CLK(clk),
|
|
.D(i),
|
|
.Q(p)
|
|
);
|
|
endmodule
|
|
EOT
|
|
|
|
opt_merge
|
|
select -assert-count 2 t:$dff
|
|
|
|
design -reset
|
|
read_verilog -icells <<EOT
|
|
module top(input clk, i, (* init = 1'b0 *) output o, p);
|
|
\$dff #(
|
|
.CLK_POLARITY(1'h1),
|
|
.WIDTH(32'd1)
|
|
) ffo (
|
|
.CLK(clk),
|
|
.D(i),
|
|
.Q(o)
|
|
);
|
|
\$dff #(
|
|
.CLK_POLARITY(1'h1),
|
|
.WIDTH(32'd1)
|
|
) ffp (
|
|
.CLK(clk),
|
|
.D(i),
|
|
.Q(p)
|
|
);
|
|
endmodule
|
|
EOT
|
|
|
|
opt_merge -keepdc
|
|
select -assert-count 1 t:$dff
|
|
|
|
design -reset
|
|
read_verilog -icells <<EOT
|
|
module top(input clk, i, output o, p);
|
|
\$dff #(
|
|
.CLK_POLARITY(1'h1),
|
|
.WIDTH(32'd1)
|
|
) ffo (
|
|
.CLK(clk),
|
|
.D(i),
|
|
.Q(o)
|
|
);
|
|
\$dff #(
|
|
.CLK_POLARITY(1'h1),
|
|
.WIDTH(32'd1)
|
|
) ffp (
|
|
.CLK(clk),
|
|
.D(i),
|
|
.Q(p)
|
|
);
|
|
endmodule
|
|
EOT
|
|
|
|
opt_merge -keepdc
|
|
select -assert-count 2 t:$dff
|