mirror of https://github.com/YosysHQ/yosys.git
47 lines
1.4 KiB
Plaintext
47 lines
1.4 KiB
Plaintext
# Regression test for a xilinx_srl bug where a fixed shift register inferred
|
|
# from FDRE cells dropped the clock enable. FDRE has an active high clock
|
|
# enable but run_fixed assigned it ENPOL 2 (no enable) instead of ENPOL 1,
|
|
# so the resulting shift register shifted every cycle and ignored stalls.
|
|
read_verilog <<EOT
|
|
module xilinx_srl_enable_test(input i, clk, ce, output q);
|
|
reg [3:0] shift = 4'b0000;
|
|
always @(posedge clk)
|
|
if (ce)
|
|
shift <= {shift[2:0], i};
|
|
assign q = shift[3];
|
|
endmodule
|
|
|
|
module $__XILINX_SHREG_(input C, D, E, input [1:0] L, output Q);
|
|
parameter CLKPOL = 1;
|
|
parameter ENPOL = 1;
|
|
parameter DEPTH = 2;
|
|
parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
|
|
reg [DEPTH-1:0] r = INIT;
|
|
wire ce = (ENPOL == 2) ? 1'b1 : (ENPOL == 1) ? E : ~E;
|
|
always @(posedge C)
|
|
if (ce)
|
|
r <= { r[DEPTH-2:0], D };
|
|
assign Q = r[L];
|
|
endmodule
|
|
EOT
|
|
design -copy-to model $__XILINX_SHREG_
|
|
hierarchy -top xilinx_srl_enable_test
|
|
prep
|
|
design -save gold
|
|
|
|
synth_xilinx -noiopad -noclkbuf -run begin:map_luts
|
|
opt_expr -mux_undef -noclkinv
|
|
techmap -map +/xilinx/ff_map.v
|
|
xilinx_srl -fixed
|
|
opt
|
|
|
|
select -assert-count 1 t:$__XILINX_SHREG_
|
|
|
|
design -stash gate
|
|
design -import gold -as gold
|
|
design -import gate -as gate
|
|
design -copy-from model -as $__XILINX_SHREG_ \$__XILINX_SHREG_
|
|
prep
|
|
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
|
sat -verify -prove-asserts -show-ports -seq 6 miter
|