Unverified Commit bb79f23b by Miodrag Milanović Committed by GitHub

Merge pull request #68 from SergeyDegtyar/SergeyDegtyar/issues_automation

New tests for closed issues and open bugs. Not grepping strings where it is possible.
parents 3b0a6a67 39190375
......@@ -493,6 +493,58 @@ $(eval $(call template,issue_01284,issue_01284))
#issue_01329
$(eval $(call template,issue_01329,issue_01329))
#issue_01364
$(eval $(call template,issue_01364,issue_01364))
#issue_01372
$(eval $(call template,issue_01372,issue_01372))
#Still open bugs (should be failed):
#issue_00329
$(eval $(call template,issue_00329,issue_00329))
#issue_00623
$(eval $(call template,issue_00623,issue_00623))
#issue_00656
$(eval $(call template,issue_00656,issue_00656))
#issue_01014
$(eval $(call template,issue_01014,issue_01014))
#issue_01126
$(eval $(call template,issue_01126,issue_01126))
#issue_01161
$(eval $(call template,issue_01161,issue_01161))
#issue_01193
$(eval $(call template,issue_01193,issue_01193))
#issue_01206
$(eval $(call template,issue_01206,issue_01206))
#issue_01216
$(eval $(call template,issue_01216,issue_01216))
#issue_01217
$(eval $(call template,issue_01217,issue_01217))
#issue_01225
$(eval $(call template,issue_01225,issue_01225))
#issue_01259
$(eval $(call template,issue_01259,issue_01259))
#issue_01291
$(eval $(call template,issue_01291,issue_01291))
#issue_01360
$(eval $(call template,issue_01360,issue_01360))
......
module hb_exp
#(parameter
HRQW=32,
HRSW=32,
RSTRT=0,
REND=7,
ADDRW = 3,
NTGT=REND-RSTRT+1,
ADDR_COMP = 0,
BASE_ADDR_VEC = 0,
ADDR_MASK_VEC = 0,
DFF_SAMPLES = 1
)(
input clk,
input areset_n,
input init_exp_rq,
input [ADDRW-1:0] init_exp_addr,
input [HRQW-1:0] init_exp_data,
input [NTGT-1:0] tgt_exp_ack,
input [NTGT-1:0] tgt_exp_err,
input [NTGT*HRSW-1:0] tgt_exp_data
);
wire [NTGT-1:0] exp_tgt_rq_samp_int ;
wire [NTGT-1:0] tgt_sel;
generate
if(ADDR_COMP==0) begin: GEN_IND_TREE
assign tgt_sel = addr_dec(init_hb_addr_ff);
end
else begin: GEN_REG_TREE
assign tgt_sel = addr_dec_comp(init_hb_addr_ff,BASE_ADDR_VEC,ADDR_MASK_VEC);
end
endgenerate
assign exp_tgt_rq_samp_int = {NTGT{init_exp_rq_ff}} & tgt_sel;
////////////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////////////
// Functions
function [NTGT-1:0] addr_dec(input [ADDRW-1:0] f_addr);
integer i_tgt;
reg [NTGT-1:0] tgt_tmp;
begin
tgt_tmp={NTGT{1'b0}};
for(i_tgt=RSTRT;i_tgt<=REND;i_tgt=i_tgt+1) begin
if(f_addr==i_tgt) begin
tgt_tmp[i_tgt]=1'b1;
end
end
addr_dec=tgt_tmp;
end
endfunction
function [NTGT-1:0] addr_dec_comp(input [ADDRW-1:0] f_addr,input [NTGT*ADDRW-1:0] base_addr_in,input [NTGT*ADDRW-1:0] mask_in);
integer i_tgt;
reg [NTGT-1:0] tgt_tmp;
reg [ADDRW-1:0] base_addr_arr [NTGT-1:0];
reg [ADDRW-1:0] addr_mask_arr [NTGT-1:0];
reg [ADDRW-1:0] end_addr_arr [NTGT-1:0];
begin
for(i_tgt=RSTRT;i_tgt<=REND;i_tgt=i_tgt+1) begin
base_addr_arr[i_tgt]=base_addr_in[i_tgt*ADDRW +: ADDRW];
addr_mask_arr[i_tgt]=mask_in[i_tgt*ADDRW +: ADDRW];
end_addr_arr[i_tgt]=base_addr_arr[i_tgt] + addr_mask_arr[i_tgt];
end
tgt_tmp={NTGT{1'b0}};
for(i_tgt=RSTRT;i_tgt<=REND;i_tgt=i_tgt+1) begin
if((f_addr>=base_addr_arr[i_tgt])&&(f_addr<=end_addr_arr[i_tgt])) begin
tgt_tmp[i_tgt]=1'b1;
end
end
addr_dec_comp=tgt_tmp;
end
endfunction
endmodule
module bidirtest (
A, EO, Q, BI
);
inout BI;
output Q;
input A;
input EO;
assign BI = (EO == 1'b1) ? A : 1'bz;
assign Q = BI;
endmodule
module yosys_genblk_scoping #(
parameter WIDTH = 6
)
(
input [WIDTH-1:0] a_i,
input [WIDTH-1:0] b_i,
output [WIDTH-1:0] z_o
);
genvar g;
generate
for (g = 0; g < WIDTH; g = g + 1) begin
if(g > 2) begin//: blk_true
wire tmp;
assign tmp = a_i[g] || b_i[g];
assign z_o[g] = tmp;
end
else begin
assign z_o[g] = a_i[g] && b_i[g];
end
end
endgenerate
endmodule
module top (input [7:0] data, output [7:0] out);
genvar n;
generate
for (n=7; n>=0; n=n-1) begin
assign out[n] = data[7-n];
end
endgenerate
endmodule
module test(c);
input [9:0] c;
function integer a(input integer b);
begin
a = b+1;
end
endfunction
localparam f = 5;
wire [a(f)-1:0] d;
//wire [a(f)-1:0] d1;
assign d = c[a(f)-1:0]; // wrong behavior
localparam e = a(f);
//assign d1 = c[e-1:0]; // correct behavior
endmodule
module error_design(a, b, z0, z1);
input a;
input b;
output z0, z1;
assign z0 = a;
assign z0 = b;
assign z1 = b;
endmodule
module test (input e, a, output reg b);
always_comb
if (e)
b = a;
endmodule
autoidx 1
attribute \top 1
module \top
wire width 1073741824 $1
wire width 1073741824 $2
process $group_0
sync init
end
connect $1 $2
end
module top (hz100, pb, ss7, ss6, ss5, ss4, ss3, ss2, ss1, ss0, left, right, red, green, blue);
input hz100;
input [20:0] pb;
output [7:0] ss7;
output [7:0] ss6;
output [7:0] ss5;
output [7:0] ss4;
output [7:0] ss3;
output [7:0] ss2;
output [7:0] ss1;
output [7:0] ss0;
output [7:0] left;
output [7:0] right;
output red;
output green;
output blue;
reg [4:0] op;
reg [31:0] save;
reg [31:0] entry;
reg [31:0] nextresult;
wire [31:0] source = displaysave ? save : entry;
assign {left,right} = source[15:0];
wire [4:0] key;
wire pressed;
scankey sk(.clk(hz100), .strobe(pressed), .out(key), .in(pb));
always @ (posedge pressed)
begin
casez (key)
5'b0????: begin
entry <= {28'b0,key[3:0]};
end
5'b1????: begin
save <= nextresult;
op <= key;
end
endcase
end
always @(*)
case (op)
0: nextresult = entry;
default: nextresult = save;
endcase
endmodule
module scankey(clk, in, out, strobe);
input wire clk;
output wire [4:0] out;
output wire strobe;
input wire [20:0] in;
wire active;
reg [4:0] highest;
reg [1:0] delay;
always @(posedge clk)
delay <= delay<<1 | active;
assign strobe = delay[1];
assign {active,out} = in[20] == 1 ? 6'b110100 :
in[19] == 1 ? 6'b110011 :
in[18] == 1 ? 6'b110010 :
in[17] == 1 ? 6'b110001 :
in[16] == 1 ? 6'b110000 :
in[15] == 1 ? 6'b101111 :
in[14] == 1 ? 6'b101110 :
in[13] == 1 ? 6'b101101 :
in[12] == 1 ? 6'b101100 :
in[11] == 1 ? 6'b101011 :
in[10] == 1 ? 6'b101010 :
in[ 9] == 1 ? 6'b101001 :
in[ 8] == 1 ? 6'b101000 :
in[ 7] == 1 ? 6'b100111 :
in[ 6] == 1 ? 6'b100110 :
in[ 5] == 1 ? 6'b100101 :
in[ 4] == 1 ? 6'b100100 :
in[ 3] == 1 ? 6'b100011 :
in[ 2] == 1 ? 6'b100010 :
in[ 1] == 1 ? 6'b100001 :
in[ 0] == 1 ? 6'b100000 : 6'b000000;
endmodule
`default_nettype none
module mcve2(david);
output reg david;
always @(*)
goliath = 4;
always @(*)
david = goliath;
endmodule
`default_nettype wire
module top(inout pin, input dout, sel, output din);
assign pin = sel ? dout : 1'bz;
assign din = pin;
endmodule
module top();
parameter W = 10;
wire [W-1:0] x;
empty #(.W(W)) empty_inst(.x(x));
endmodule
module empty#(parameter W = 0)(output wire [W-1:0] x);
endmodule
module frozen(clk, out);
input clk;
output reg out;
always @(posedge clk) begin
out <= out;
end
endmodule // frozen
module top(input clk);
MyInterface MyInterfaceInstance();
endmodule
interface MyInterface();
logic not_an_empty_interface;
endinterface
module top();
wire o;
wire a;
wire b;
wire [3:0] i;
assign o = i == 4'hb ? a:b;
endmodule
////////////////////////////////////////////////////////////////////////////////
//
////////////////////////////////////////////////////////////////////////////////
//
`default_nettype none
//
module mcvesix(i_clk, i_bits, o_char);
input wire i_clk;
input wire [6:0] i_bits;
output reg [7:0] o_char;
reg [6:0] remap [0:127];
integer k, newv;
always @(*) begin
for(k=0; k<128; k=k+1)
begin
newv = 0;
// `define BROKEN_CODE
`ifdef BROKEN_CODE
if (k[6])
`else
if (k >= 64)
`endif
newv = 7'h0a;
else
newv = k;
remap[k] = newv;
end
end
initial o_char = 8'h00;
always @(posedge i_clk)
o_char <= { 1'b0, remap[i_bits] };
`ifdef FORMAL
reg [7:0] f_char;
//
// Here's the old encoding that "worked"
//
initial f_char = 8'h00;
always @(posedge i_clk)
begin
if (i_bits[6])
f_char <= 8'h0a;
else
f_char <= i_bits[6:0];
end
//
// Now let's prove that the two encodings are equivalent
always @(*)
assert(f_char == o_char);
`endif
endmodule
read_verilog -mem2reg ../top.v
write_verilog result.log
read_verilog ../top.v
select n:\\SUM/N10
tee -o result.log select -list
select -assert-any n:\\SUM/N10
read_verilog ../top.v
synth_greenpak4 -part SLG46621V
select GP_INV
tee -o result.log select -list
select -assert-count 1 t:GP_INV
......@@ -19,6 +19,5 @@ abc -liberty ../osu018_stdcells_edit.lib
clean
select DFFSR
tee -o result.log select -list
select -assert-count 0 t:DFFSR
read_verilog ../top.v
tribuf -logic
synth -top bidirtest
iopadmap -bits -inpad IBUF O:PAD -outpad OBUF I:PAD -tinoutpad IOBUF ENA:O:I:PAD bidirtest
select -assert-count 0 t:IOBUF
......@@ -20,5 +20,5 @@ design -copy-from netlist_v2 -as netlist_new netlist_v2
equiv_make -inames netlist_old netlist_new miter_netlist
equiv_simple -undef -seq 10
equiv_induct -undef -seq 10
tee -o result.log equiv_status
tee -o result.log equiv_status -assert
tee -o result.log read_verilog ../top.v
......@@ -4,4 +4,4 @@ read_verilog ../top.v;
rename -top gate; design -stash gate;
design -copy-from gold -as gold gold;
design -copy-from gate -as gate gate;
tee -o result.log equiv_make gold gate equiv
equiv_make gold gate equiv
tee -o result.log read_liberty ../lib.lib
write_verilog synth.v
read_liberty ../lib.lib
tee -o result.log read_verilog ../top.v
read_verilog ../top.v
prep
write_verilog synth.v
select -assert-count 4 t:$dff
read_verilog ../top.v
tee -o result.log synth -top top
write_verilog synth.v
synth -top top
select -assert-count 1 t:$_DFF_P_
select -assert-none t:$_DFF_P_ %% t:* %D
......@@ -6,4 +6,5 @@ fsm
opt
memory
opt
tee -o result.log synth_xilinx -top tc
synth_xilinx -top tc
select -assert-count 12 t:FDRE
read_verilog ../top.v
synth_xilinx -flatten
tee -o result.log stat
select -assert-count 1 t:RAMB36E1
tee -a result.log read_verilog ../top.v
tee -a result.log synth_xilinx
tee -a result.log flatten
tee -a result.log dump top
read_verilog ../top.v
synth_xilinx
flatten
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-count 1 t:FDRE_1
read_verilog ../top.v
tee -a result.log synth_xilinx
synth_xilinx
select -assert-count 4 t:FDRE
......@@ -4,4 +4,4 @@ memory_dff -nordff
memory_collect
opt_reduce
clean
tee -a result.log write_firrtl firrtl.firrtl
write_firrtl firrtl.firrtl
read_verilog ../top.v
tee -a result.log prep
prep
select -assert-none t:$dlatch
read_verilog ../top.v
prep -top picorv32 -nordff
opt -fast
tee -a result.log write_smt2 picorv32.smt2
write_smt2 picorv32.smt2
......@@ -3,4 +3,4 @@ proc
memory_dff -nordff
opt_reduce
clean
tee -a result.log write_firrtl firrtl.firrtl
write_firrtl firrtl.firrtl
read_verilog ../*.v
tee -a result.log synth_ice40 -top SuperTopEntity -json TopEntity.json
synth_ice40 -top SuperTopEntity -json TopEntity.json
read_verilog ../top.v
synth
read_verilog -sv ../top.v
proc
wreduce -keepdc
tee -a result.log dump
select -assert-count 1 t:$mux
read_verilog ../top.v
tee -a result.log synth_xilinx
synth_xilinx
select -assert-none t:RAM64X1D
read_verilog ../top.v
tee -a result.log synth_xilinx -nodram
synth_xilinx -nodram
select -assert-none t:FDRE
read -formal ../top.v
hierarchy -top top
synth
write_verilog -noattr result.log
select -assert-count 1 t:$_NOR_
select -assert-none t:$_NOR_ %% t:* %D
......@@ -4,5 +4,5 @@ dff2dffe
simplemap
opt
opt_rmdff
stat
tee -o result.log dump
select -assert-count 1 t:$_DFF_N_
select -assert-none t:$_DFF_N_ %% t:* %D
......@@ -3,4 +3,6 @@ proc
opt
techmap
muxcover -nopartial
tee -o result.log stat
stat
select -assert-count 1 t:$_MUX4_
select -assert-none t:$_MUX4_ %% t:* %D
read_verilog ../top.v
write_verilog result.log
#write_json test_synth.json
......@@ -5,4 +5,4 @@ select -set buf w:w1 %coe1 w:w1 %d
# set the keep attribute for the $_BUF_ from w1 to w2
setattr -set keep 1 @buf
opt_clean
tee -o result.log stat
select -assert-count 1 t:$_BUF_
read_verilog ../top.v
proc; opt; wreduce; simplemap; muxcover -mux4=150
tee -o result.log stat
select -assert-count 1 t:$_MUX4_
read_verilog ../top.v
proc; pmux2shiftx -norange; opt -full
tee -o result.log stat
select -assert-count 1 t:$pmux
select -assert-count 3 t:$eq
read_verilog -sv ../top.sv
hierarchy -check -top TopModule
proc
tee -o result.log flatten
flatten
read_verilog ../top.v
hierarchy
proc
write_verilog result_no_opt.log
equiv_opt -assert opt_clean
opt_clean
write_verilog result.log
read_verilog -sv ../top.v
proc
select -assert-count 0 t:$dlatch
tee -o result.log dump
read_ilang ../top.il
tee -o result.log proc_init
read_verilog ../top.v
tee -o result.log synth_ice40 -top top
tee -o result.log write_blif test.blif
tee -o result.log read_verilog ../top.v
read_verilog ../top.v
hierarchy -top top
proc
tee -o result.log flatten
flatten
read_verilog ../top.v
tee -o result.log synth_xilinx
synth_xilinx
read_verilog ../top.v
synth_xilinx
select -assert-count 1 t:BUFT
tee -o result.log read -formal ../top.v
read -formal ../top.v
tee -o result.log read_verilog ../top.v
hierarchy -top top
tee -o result.log write_smt2
read_verilog ../top.v
synth -top top
muxcover -mux8
tee -o result.log stat
select -assert-count 9 t:$_MUX8_
tee -o result.log read_verilog ../top.v
proc
equiv_opt -assert prep
prep -top frozen
tee -o result.log dump
......@@ -10,5 +10,3 @@ cd dff # Constrain all select calls below inside the top module
select -assert-count 4 t:$adff
select -assert-count 1 t:$mux
select -assert-none t:$adff t:$mux %% t:* %D
tee -o result.log stat
read_verilog -sv ../top.v
synth_ice40 -blif out.blif
read -define BROKEN_CODE
read -formal ../top.v
prep -top mcvesix
tee -o result.log equiv_opt -assert prep # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd mcvesix # Constrain all select calls below inside the top module
select -assert-count 2 w:k s:32
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment