Skip to content

Y
yosys-tests
Commit 7a0d0c6d by Miodrag Milanovic
Options

Added properly handled regression tests

parent c7e05d2b
Showing with 561 additions and 911 deletions
generate-new.py 0 → 100644
import os
is_heavy_enabled = int(os.getenv('ENABLE_HEAVY_TESTS', '0')) == 1
for root, dirs, files in sorted(os.walk(".")):
for file in files:
if file.endswith('.ys') or file.endswith('run-test.sh'):
dir = os.path.basename(root)
work = os.path.splitext(file)[0]
heavy = os.path.exists(os.path.join(dir, "heavy_test"))
is_disabled = os.path.exists(os.path.join(dir, work + ".disable"))
print("all: {0}/work_{1}/.stamp\n"
"{0}/work_{1}/.stamp:".format(dir, work))
if (is_disabled):
print("\t@echo 'Skipping disabled test {0}..'".format(dir, work))
continue
if (heavy and not is_heavy_enabled):
print("\t@echo 'Skipping heavy test {0}..'".format(dir, work))
continue
print("\t@echo 'Running {2}{1}..'\n"
"\t@../run-new.sh {0} {1}\n"
"clean::\n"
"\t@echo 'Cleaning {1}..'\n"
"\t@rm -rf {0}/work_{1}".format(dir, work, "heavy " if heavy else ""))
print(".PHONY: all clean")
\ No newline at end of file
regression/Makefile
PYTHON_EXECUTABLE := $(shell if python3 -c ""; then echo "python3"; else echo "python"; fi)
all:
all: run-test.mk
run-test.mk: ../generate.py
@$(PYTHON_EXECUTABLE) ../generate.py > run-test.mk
run-test.mk: ../generate-new.py
@$(PYTHON_EXECUTABLE) ../generate-new.py > run-test.mk
include run-test.mk
clean::
@rm -rf run-test.mk
@echo 'Cleaning run-test.mk..'
.PHONY: all clean
regression/common.v deleted 100644 → 0
module assert_dff(input clk, input test, input pat);
always @(posedge clk)
begin
#2
if (test != pat)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time);
$stop;
end
end
endmodule
module assert_tri(input en, input A, input B);
always @(posedge en)
begin
//#1;
if (A !== B)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
$stop;
end
end
endmodule
module assert_Z(input clk, input A);
always @(posedge clk)
begin
//#1;
if (A === 1'bZ)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
$stop;
end
end
endmodule
module assert_X(input clk, input A);
always @(posedge clk)
begin
//#1;
if (A === 1'bX)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time," ",A);
$stop;
end
end
endmodule
module assert_comb(input A, input B);
always @(*)
begin
#1;
if (A !== B)
begin
$display("ERROR: ASSERTION FAILED in %m:",$time," ",A," ",B);
$stop;
end
end
endmodule
regression/issue_00018/issue_00018.ys
read_verilog ../top.v
read_verilog top.v
synth -top d
regression/issue_00041/issue_00041.ys
read_verilog ../top.v
read_verilog top.v
synth -top top
write_verilog synth.v
regression/issue_00059/issue_00059.ys
read_verilog ../top.v
read_verilog top.v
#Myname: added some comment with a colon
synth -top top
regression/issue_00065/issue_00065.ys
read_verilog ../top.v
read_verilog top.v
synth -top top
regression/issue_00067/issue_00067.ys
read_verilog ../top.v
read_verilog top.v
freduce
regression/issue_00071/issue_00071.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00078/top.v → regression/issue_00078/is28.v
/* Generated by Yosys 0.5+284 (git sha1 f40d1b7, gcc 5.2.1-15 -fPIC -Os) */
(* src = "test.v:1" *)
module top(X, Y);
module is28(X, Y);
wire _0000_;
wire _0001_;
wire _0002_;
......
regression/issue_00078/issue_00078.pat deleted 100644 → 0
\\\X\[0\] , \\\X\[1\] , \\\X\[2\] ,
regression/issue_00078/issue_00078.ys
read_verilog ../top.v
read_verilog is28.v
hierarchy
splitnets -ports
write_verilog result.out
!mkdir -p work_issue_00078
write_verilog work_issue_00078/synth.v
!grep "(\\\X\[0\] , \\\X\[1\] , \\\X\[2\] ," work_issue_00078/synth.v > /dev/null
\ No newline at end of file
regression/issue_00081/issue_00081.ys
logger -expect error "syntax error" 1
read_verilog ../top.v
read_verilog top.v
regression/issue_00082/issue_00082.ys 0 → 100644
logger -expect error "no AST_WIRE node" 1
read_verilog top.v
regression/issue_00083/issue_00083_fail.ys
read_verilog ../top.v
logger -expect warning "Deep recursion in AST simplifier." 1
read_verilog top.v
regression/issue_00084/issue_00084.ys
read_verilog ../top.v
read_verilog top.v
synth_xilinx -top top
cd top
select -assert-count 1 t:RAMB18E1
\ No newline at end of file
regression/issue_00085/issue_00085.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00086/issue_00086.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00088/issue_00088.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00089/issue_00089.ys 0 → 100644
logger -expect error "syntax error, unexpected \$undefined" 1
read_verilog top.v
regression/issue_00091/issue_00091.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00093/issue_00093.ys 0 → 100644
logger -expect error "syntax error, unexpected '\+'" 1
read_verilog top.v
regression/issue_00093/issue_00093_fail.ys deleted 100644 → 0
read_verilog ../top.v
synth -top top
regression/issue_00095/issue_00095.ys 0 → 100644
logger -expect error "syntax error, unexpected '#'" 1
read_verilog top.v
regression/issue_00095/issue_00095_fail.ys deleted 100644 → 0
read_verilog ../top.v
synth -top top
regression/issue_00096/issue_00096.ys 0 → 100644
logger -expect error "syntax error, unexpected TOK_INOUT" 1
read_verilog top.v
regression/issue_00096/issue_00096_fail.ys deleted 100644 → 0
read_verilog ../top.v
synth -top top
regression/issue_00098/issue_00098.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00099/issue_00099.ys 0 → 100644
logger -expect error "syntax error, unexpected ','" 1
read_verilog top.v
regression/issue_00102/issue_00102.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00111/issue_00111.ys
read_verilog ../top.v
read_verilog top.v
synth -top top
splitnets -ports
hierarchy -check
regression/issue_00114/issue_00114.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00126/issue_00126.ys
read_verilog ../top.v
read_verilog top.v
hierarchy -top test
write_verilog -noexpr -norename result.out
logger -expect warning "Module test contains unmapped RTLIL processes" 1
write_verilog -noexpr -norename
regression/issue_00128/issue_00128.ys
read_verilog ../top.v
read_verilog top.v
synth -top top
regression/issue_00132/issue_00132.ys
read_verilog -defer ../top.v
chparam -set incr 42 topmod
read_verilog -defer top.v
chparam -set incr 42 top
prep -flatten
sat -verify -prove-asserts -show-ports -set a[7:0] 1 -prove y[7:0] 43
regression/issue_00133/issue_00133.ys
read_verilog ../top.v
synth -top top
read_verilog top.v
prep -flatten
sat -verify -prove-asserts -show-ports -prove y a
regression/issue_00134/issue_00134.ys
read_verilog ../top.v
read_verilog top.v
hierarchy -top task_bug
proc; opt; memory; dff2dffe; wreduce; clean; opt
write_verilog -noexpr -norename result.out
proc
sat -verify -prove-asserts -show-ports -prove do in_data
regression/issue_00160/issue_00160.ys
read_verilog ../top.v
read_verilog top.v
#equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
equiv_opt -map +/ice40/cells_sim.v synth_ice40 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
......
regression/issue_00171/issue_00171.ys
read_verilog ../top.v
read_verilog top.v
proc; opt; fsm; opt; memory; opt; techmap; opt
scc -all_cell_types
#and then put each found SCC into a module using submod.
......
regression/issue_00173/issue_00173.ys
read_verilog ../top.v
read_verilog top.v
proc
sat -verify -prove-asserts -show-ports -prove co bi
#TODO: check if we should take care of order or not
\ No newline at end of file
regression/issue_00174/issue_00174.ys
read_verilog ../top.v
read_verilog top.v
hierarchy -top top
write_verilog -noattr t1.v
proc
opt -full
techmap
......
regression/issue_00175/issue_00175.ys
read_verilog ../top.v
read_verilog top.v
hierarchy
proc
opt
......
regression/issue_00182/issue_00182.ys
read_verilog ../top.v
synth_ice40 -blif litescope.bli -top top
read_verilog top.v
synth_ice40 -top top
regression/issue_00183/issue_00183.ys
read_verilog ../top.v
synth_ice40 -top top -blif test.blif
read_verilog top.v
synth_ice40 -top top
regression/issue_00186/issue_00186.pat deleted 100644 → 0
assign _07_\[0\] = adr\[0\] ? \\ram\[3\] \[0\] : \\ram\[2\] \[0\];
assign _07_\[1\] = adr\[0\] ? \\ram\[3\] \[1\] : \\ram\[2\] \[1\];
regression/issue_00186/issue_00186.ys
read_verilog -DTEST_1 ../top.v
read_verilog -DTEST_1 top.v
hierarchy -top top
proc; memory
opt -full
techmap
write_verilog -noattr result.out
synth
rename -top gold
design -save gold
design -reset
read_verilog -DTEST_2 top.v
hierarchy -top top
proc; memory
opt -full
synth
rename -top gate
design -copy-from gold gold
equiv_make gold gate equiv
equiv_induct
equiv_status -assert equiv
\ No newline at end of file
regression/issue_00194/issue_00194.ys
read_verilog ../top.v
read_verilog top.v
proc
prep -flatten
sat -verify -prove-asserts -show-ports -prove y a
regression/issue_00195/issue_00195.ys
read_verilog ../top.v
read_verilog top.v
synth -top top
write_verilog synth.v
sat -verify -prove-asserts -show-ports -prove b 123456
regression/issue_00195/testbench.v deleted 100644 → 0
module testbench;
reg clk;
initial begin
// $dumpfile("testbench.vcd");
// $dumpvars(0, testbench);
#0 clk = 0;
repeat (10000) begin
#5 clk = 1;
#5 clk = 0;
end
$display("OKAY");
end
top uut (
.b (clk )
);
endmodule
regression/issue_00195/top.v
module top(b);
input b;
module top(output [17:0] b);
wire a = 100_000.0;
assign b = 123_456.0;
endmodule
regression/issue_00196/issue_00196.ys 0 → 100644
logger -expect error "Found posedge/negedge event on a signal that is not 1 bit wide!" 1
read_verilog top.v
regression/issue_00196/issue_00196_fail.pat deleted 100644 → 0
ERROR: Found posedge/negedge event on a signal that is not 1 bit wide!
regression/issue_00196/issue_00196_fail.ys deleted 100644 → 0
read_verilog ../top.v
synth_greenpak4 -json 3pdrive.json
regression/issue_00210/issue_00210.ys
read_verilog ../top.v
read_verilog top.v
sat -verify -prove-asserts -show-ports -set-any-undef 0 -prove result 2
regression/issue_00282/issue_00282.ys
read_verilog ../top.v
read_verilog top.v
synth -top top
#synth_ice40 -top top
# Next will fail if synth_ice40 is executed
select -assert-count 1 t:$_DFF_P_
regression/issue_00283/issue_00283.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00283/top.v
module top
#(parameter WIDTH = 64, C_WIDTH = 8, DE = 4)
(
input clk,
input reset,
input [C_WIDTH*WIDTH-1:0] c_data_in_port,
input [DE*C_WIDTH -1:0] d_one_hot,
input [C_WIDTH -1:0] c_data_in_en,
module top(input clk, enable, output reg y);
output reg [DE*WIDTH-1:0] d_data_out_port,
output reg [DE-1:0] d_data_out_en
);
wire [1:0] foo [1:0];
integer i;
reg [ WIDTH-1:0] clients_data_in [ C_WIDTH-1:0];
reg [ C_WIDTH-1:0] devices_one_hot_client_sel [ DE-1:0];
reg [ WIDTH-1:0] devices_data_out [ DE-1:0];
reg [ WIDTH-1:0] clients_data_in_s [ C_WIDTH-1:0];
reg [ C_WIDTH-1:0] devices_one_hot_client_sel_s [ DE-1:0];
wire [ WIDTH-1:0] devices_data_out_p [ DE-1:0];
wire [ C_WIDTH-1:0] clients_data_rotate [ WIDTH-1:0];
wire [ DE-1:0] devices_data_rotate [ WIDTH-1:0];
reg [ DE-1:0] clients_one_hot_device_sel [ C_WIDTH-1:0];
wire [ DE-1:0] dev_en;
wire [ DE-1:0] data_out_en;
integer client, device;
always @*
begin
for(client = 0; client < C_WIDTH; client = client + 1) begin
clients_data_in[client] = c_data_in_port[client*WIDTH+:WIDTH];
end
end
always @*
begin
for(client = 0; client < C_WIDTH; client = client + 1) begin
clients_one_hot_device_sel[client] = d_one_hot[client*DE+:DE];
end
end
always @*
begin
for (device = 0; device < DE; device = device + 1) begin
for(client = 0; client < C_WIDTH; client = client + 1) begin
devices_one_hot_client_sel[device][client] = clients_one_hot_device_sel[client][device];
end
end
end
genvar k;
integer rowsel;
genvar i, j, nw;
always @(posedge clk or negedge reset)
if (!reset)
for (rowsel = 0; rowsel < DE; rowsel=rowsel+1)
devices_data_out[rowsel][WIDTH-1:1] <= 'b0;
else begin
for (rowsel = 0; rowsel < DE; rowsel=rowsel+1)
if (dev_en[rowsel]==1'b1)
devices_data_out[rowsel][WIDTH-1:1] <= devices_data_out_p[rowsel][WIDTH-1:1];
end
always @(posedge clk or negedge reset)
if (!reset)
for (rowsel = 0; rowsel < DE; rowsel=rowsel+1)
devices_data_out[rowsel][0] <= 1'b0;
else
for (rowsel = 0; rowsel < DE; rowsel=rowsel+1)
devices_data_out[rowsel][0] <= devices_data_out_p[rowsel][0];
always @*
begin
for(rowsel = 0; rowsel < C_WIDTH; rowsel=rowsel+1) begin
clients_data_in_s[rowsel][WIDTH-1:0] = clients_data_in[rowsel];
end
end
always @*
begin
for(rowsel = 0; rowsel < DE; rowsel=rowsel+1) begin
devices_one_hot_client_sel_s[rowsel][C_WIDTH-1:0] = devices_one_hot_client_sel[rowsel][C_WIDTH-1:0];
end
end
generate
for (i = 0; i < DE; i=i+1) begin:gen_i3
assign dev_en[i] = |devices_one_hot_client_sel_s[i][C_WIDTH-1:0];
end
endgenerate
generate
for (i = 0; i < DE; i=i+1) begin:gen_i4
assign data_out_en[i] = |devices_one_hot_client_sel[i][C_WIDTH-1:0];
end
endgenerate
always @(posedge clk or negedge reset)
if (!reset)
for (rowsel = 0; rowsel < DE; rowsel=rowsel+1)
d_data_out_en[rowsel] <= 1'b0;
else
for (rowsel = 0; rowsel < DE; rowsel=rowsel+1)
d_data_out_en[rowsel] <= data_out_en[rowsel];
generate
for (i = 0; i < C_WIDTH; i=i+1) begin:gen_i
for (j = 0; j < WIDTH; j=j+1) begin:gen_j
assign clients_data_rotate[j][i] = clients_data_in_s[i][j];
end
end
endgenerate
generate
for (nw = 0; nw < WIDTH; nw=nw+1) begin : gen_nw
for (i = 0; i < DE; i=i+1) begin:gen_label
assign devices_data_rotate[nw][i] = |(clients_data_rotate[nw] & devices_one_hot_client_sel_s[i]);
end
end
endgenerate
generate
for (i = 0; i < WIDTH; i=i+1) begin:gen_i2
for (j = 0; j < DE; j=j+1) begin:gen_j2
assign devices_data_out_p[j][i] = devices_data_rotate[i][j];
end
end
endgenerate
always @*
begin
for (device = 0; device < DE; device = device + 1) begin
d_data_out_port[device*WIDTH+:WIDTH] = devices_data_out[device];
end
end
always @(posedge clk)
if (enable)
for (i = 0; i < 2; i=i+1)
y <= foo[0][0];
endmodule
regression/issue_00287/issue_00287.ys
tee -o result.out read_verilog -sv ../top.v
logger -werror "is implicitly declared at"
read_verilog -sv top.v
regression/issue_00289/issue_00289.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
regression/issue_00291/issue_00291.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
synth -top top
regression/issue_00300/issue_00300.ys
read_verilog ../top.v
read_verilog top.v
proc
opt
......@@ -7,9 +7,9 @@ dump
write_ilang foo.ilang
memory_collect
stat
#dump t:$mem
design -reset
read_ilang foo.ilang
stat
memory_collect
tee -o result.out dump t:$mem
select -assert-count 1 r:OFFSET=0
!rm foo.ilang
\ No newline at end of file
regression/issue_00306/issue_00306.ys
read_verilog ../top.v
proc
opt -full
read_verilog top.v
synth
regression/issue_00314/issue_00314.ys
read_verilog ../top.v
read_verilog top.v
synth -top top
regression/issue_00317/issue_00317.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00341/issue_00341.ys
read_verilog ../top.v
read_verilog top.v
equiv_make gold top_w equiv
hierarchy -top equiv
opt -purge
......
regression/issue_00342/issue_00342.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
regression/issue_00349/issue_00349.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
regression/issue_00350/issue_00350.ys
read_verilog -sv ../top.v
read_verilog top.v
synth
abc -dff -g AND
opt
write_aiger -ascii -symbols <file.out>
design -reset
read_aiger <file.out>
write_verilog result.out
abc -clk clk -g AND
opt_clean
select -assert-count 2 a:init
regression/issue_00350/top.v
module test
( input clk
, input in
, output out
);
reg [1:0] state = 0;
always @(posedge clk)
case (state)
0:
if (!in || in)
state <= 1;
else
state <= state;
1:
if (in)
state <= 1;
else
if (!in)
state <= 1;
else
state <= state;
endcase
always @(*)
case (state)
0:
out = 0;
1:
begin
if (in)
out = 1;
if (!in)
out = 0;
end
endcase
module demo (input clk, input i, output o);
reg q = 0;
always @(posedge clk) q <= 1;
assign o = q & i;
endmodule
\ No newline at end of file
regression/issue_00361/issue_00361.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
prep
alumacc
select -assert-count 63 t:$add
select -assert-count 2 t:$macc
select -assert-count 65 t:$mul
regression/issue_00362/issue_00362.ys 0 → 100644
read_verilog -sv top.v
logger -expect error "Output port top.inst.b \(inst\) is connected to constants: 1'1" 1
synth -top top
regression/issue_00362/issue_00362_fail.pat deleted 100644 → 0
ERROR: Output port top.inst.b (inst) is connected to constants: 1'1
regression/issue_00362/issue_00362_fail.ys deleted 100644 → 0
read_verilog -sv ../top.v
synth -top top
regression/issue_00372/issue_00372.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
synth -top top
select -assert-count 1 t:$_DFF_P_
regression/issue_00432/issue_00432.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
write_verilog result.v
select -assert-count 1 t:$shiftx
design -reset
read_verilog result.v
hierarchy -check
select -assert-count 1 t:$shiftx
!rm result.v
\ No newline at end of file
regression/issue_00444/issue_00444.ys
read_verilog -formal ../top.v
read_verilog -formal top.v
prep -top top
regression/issue_00449/issue_00449.ys
read_verilog -formal ../top.v
read_verilog -formal top.v
synth -top top
regression/issue_00457/issue_00457.ys
read_verilog -formal ../top.v
read_verilog -formal top.v
synth -top top
regression/issue_00481/issue_00481.ys
read_verilog ../top.v
synth_ice40 -blif tlt.blif
read_verilog top.v
synth_ice40
regression/issue_00502/issue_00502.ys
read_verilog ../top.v
read_verilog top.v
select -assert-any n:\\SUM/N10
regression/issue_00524/issue_00524.ys
read_verilog ../top.v
read_verilog top.v
synth_greenpak4 -part SLG46621V
select -assert-count 1 t:GP_INV
regression/issue_00527/issue_00527.ys
......@@ -3,7 +3,7 @@
#yosys -import
#set libfile osu018_stdcells_edit.lib
read_verilog -sv ../sd_rrmux.v
read_verilog -sv sd_rrmux.v
# Vanilla synth flow
hierarchy
......@@ -13,9 +13,9 @@ opt
techmap
opt
dfflibmap -liberty ../osu018_stdcells_edit.lib
dfflibmap -liberty osu018_stdcells_edit.lib
abc -liberty ../osu018_stdcells_edit.lib
abc -liberty osu018_stdcells_edit.lib
clean
......
regression/issue_00567/issue_00567.ys
read_verilog ../top.v
read_verilog top.v
synth_ice40 -nocarry
opt_clean
write_blif -attr -cname -param lut.eblif
select -assert-count 1 t:SB_LUT4
regression/issue_00582/issue_00582.ys 0 → 100644
logger -expect error "Failed to detect width for identifier \\valid!" 1
read_verilog top.v
synth_ice40 -top main
regression/issue_00582/issue_00582_fail.pat deleted 100644 → 0
ERROR: Failed to detect width for identifier \\valid!
regression/issue_00582/issue_00582_fail.ys deleted 100644 → 0
read_verilog ../top.v
synth_ice40 -top main -blif stencil.blif
regression/issue_00589/issue_00589.ys
read_verilog -lib +/ice40/cells_sim.v
read_verilog ../top.v
read_verilog top.v
hierarchy -top main
proc
flatten
......
regression/issue_00594/issue_00594.ys 0 → 100644
logger -expect error "Single range expected." 1
read_verilog top.v
regression/issue_00603/issue_00603.ys 0 → 100644
logger -expect error "syntax error, unexpected ',', expecting '='" 1
read_verilog top.v
regression/issue_00623/issue_00623.ys
read_verilog ../top.v
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
......
regression/issue_00628/issue_00628.ys
read_verilog ../top.v
read_verilog top.v
hierarchy
proc -global_arst reset
flatten; techmap
ice40_opt
#-unlut
opt_clean
abc -script +strash
#ifraig
#scorr
#retime
#strash
clean
#write_blif
select -assert-count 16 t:SB_LUT4
regression/issue_00630/issue_00630.ys
read_verilog ../top.v
read_verilog top.v
hierarchy
tee -o result.out synth_ice40 -blif demo.blif
logger -expect-no-warnings
synth_ice40
regression/issue_00630/issue_00630_n.pat deleted 100644 → 0
Warning: wire '$func$\func$demo.v:8$2$\arg' is assigned in a block at demo.v:4.
regression/issue_00635/dff.sv 0 → 100644
module dff(
input clk,
input rstn,
input en,
input d,
output logic q
);
always @(posedge clk or negedge rstn)
begin
if(!rstn)
q <= 0;
else
begin
if(en)
q <= d;
else
q <= q; //prevents the creation of latches
end
end
endmodule
regression/issue_00635/issue_00635.ys 0 → 100644
read_verilog -sv dff.sv
read_verilog -sv register.sv
synth
select -assert-count 4 t:dff
regression/issue_00635/top.v → regression/issue_00635/register.sv
module top
module register #(
XLEN = 4
)
(
input clk,
input rstn,
......@@ -6,4 +9,14 @@ module top
input [XLEN-1:0] d,
output [XLEN-1:0] q
);
parameter XLEN = 4;
genvar i;
generate
for(i = 0; i < XLEN; i++)
begin: r
dff r(.clk(clk), .rstn(rstn), .en(en), .d(d[i]), .q(q[i]));
end
endgenerate
endmodule
regression/issue_00639/issue_00639_fail.ys → regression/issue_00639/issue_00639.ys
read_verilog -ignore_redef -nooverwrite ../top.v
read_verilog -ignore_redef -nooverwrite top.v
hierarchy -check -top top
rename top netlist_v1
hierarchy -check -top netlist_v1
......@@ -6,7 +6,7 @@ prep
splitnets -ports
design -save netlist_v1
read_verilog -ignore_redef -overwrite ../top_new.v
read_verilog -ignore_redef -overwrite top_new.v
hierarchy -check -top top
rename top netlist_v2
hierarchy -check -top netlist_v2
......@@ -20,5 +20,6 @@ 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 -assert
logger -expect error "Found 3 unproven \$equiv cells in 'equiv_status -assert'." 1
equiv_status -assert
regression/issue_00639/issue_00639_fail.pat deleted 100644 → 0
ERROR: Found 3 unproven \$equiv cells in 'equiv_status -assert'.
regression/issue_00642/issue_00642.ys
read_verilog -formal ../top.v
read_verilog -formal top.v
regression/issue_00644/issue_00644.ys
tee -o result.log read_verilog -formal ../top.v
synth -top top
write_verilog synth.v
read_verilog -formal top.v
hierarchy; proc; opt
sat -verify -prove-asserts -tempinduct
regression/issue_00656/issue_00656.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_00675/issue_00675.ys
read_verilog ../top.v; rename -top gold;
read_verilog top.v; rename -top gold;
design -stash gold;
read_verilog ../top.v;
read_verilog top.v;
rename -top gate; design -stash gate;
design -copy-from gold -as gold gold;
design -copy-from gate -as gate gate;
......
regression/issue_00685/issue_00685.ys
read_liberty ../lib.lib
read_liberty lib.lib
regression/issue_00689/issue_00689.ys
tee -o result.log read_verilog -sv ../top.v
read_verilog -sv top.v
synth -top top
sat -verify -prove-asserts -tempinduct
regression/issue_00699/issue_00699.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
regression/issue_00708/issue_00708.ys
tee -o result.out read_verilog ../top.v
read_verilog top.v
sat -verify -prove-asserts -show-ports -prove a 0
regression/issue_00708/top.v
module top;
`define MAX(_a, _b) ((_a) > (_b) ? (_a) : (_b))
localparam integer X = `MAX($clog2(1 << 17) - 18, 0);
initial $display("X = %d", X);
wire a = X;
endmodule
regression/issue_00737/issue_00737.ys
tee -o result.out read_verilog -dump_ast1 ../top.v
read_verilog top.v
select -assert-count 1 a:A
select -assert-count 1 a:B
regression/issue_00763/issue_00763.ys 0 → 100644
logger -expect error "Invalid nesting of always blocks and/or initializations." 1
read_verilog top.v
regression/issue_00763/issue_00763_fail.pat deleted 100644 → 0
ERROR: Invalid nesting of always blocks and/or initializations.
regression/issue_00774/issue_00774.ys
read_verilog ../yosys_rocket/AsyncResetReg.v ../yosys_rocket/EICG_wrapper.v ../yosys_rocket/freechips.rocketchip.system.LowRiscConfig.v ../yosys_rocket/freechips.rocketchip.system.LowRiscConfig.behav_srams.v ../yosys_rocket/plusarg_reader.v ../yosys_rocket/SimDTM.v
synth_ecp5 -blif foo.blif
read_verilog yosys_rocket/AsyncResetReg.v yosys_rocket/EICG_wrapper.v yosys_rocket/freechips.rocketchip.system.LowRiscConfig.v yosys_rocket/freechips.rocketchip.system.LowRiscConfig.behav_srams.v yosys_rocket/plusarg_reader.v yosys_rocket/SimDTM.v
synth_ecp5
regression/issue_00781/issue_00781.ys
read_verilog ../top.v
synth_ice40 -blif test.blif
read_verilog top.v
synth_ice40
regression/issue_00785/issue_00785.ys
read_verilog ../top.v
read_verilog top.v
synth_ice40
regression/issue_00785/top.v
......@@ -8,7 +8,7 @@ module f16_prom (
reg [15:0] do;
initial
$readmemh("../bootrom.hex", rom);
$readmemh("bootrom.hex", rom);
always @(posedge clk)
do <= rom[addr[3:0]];
......
regression/issue_00790/issue_00790.ys
read -formal ../top.v
read -formal top.v
prep -top mcve
select -assert-count 5 t:$assert
sat -verify -prove-asserts -tempinduct
regression/issue_00807/issue_00807.ys
read_verilog ../top.v
read_verilog top.v
synth -top top
regression/issue_00809/issue_00809.ys deleted 100644 → 0
read_verilog ../top.v
hierarchy -check -top top
proc; opt; memory; opt; fsm; opt; techmap; opt
abc
opt_clean
write_verilog result.out
regression/issue_00809/issue_00809_n.pat deleted 100644 → 0
wire _12_;
wire _13_;
wire _14_;
wire _15_;
wire _16_;
wire _17_;
wire _18_;
wire _19_;
wire _20_;
wire _21_;
wire _22_;
wire _23_;
wire _24_;
regression/issue_00809/top.v deleted 100644 → 0
module top(C, O, A, B);
input [3:0] A;
input [3:0] B;
output [3:0] O;
output C;
assign {C, O} = A + B;
endmodule
regression/issue_00810/issue_00810.ys
# running in master_axi/src/
read_verilog -formal ../src/faxi_master.v
read_verilog -formal ../src/pulse_to_level.v
read_verilog -formal ../src/posedge_pulse_generator.v
read_verilog -formal ../src/Delay_Line.v
read_verilog -formal ../src/Annuller.v
read_verilog -formal ../src/Down_Counter_Zero.v
read_verilog -formal ../src/Master_AXI_Address_Channel.v
read_verilog -formal ../src/Master_AXI_Read_Data_Channel.v
read_verilog -formal ../src/Master_AXI_Read_Sequencer.v
read_verilog -formal ../src/Master_AXI_Transactor.v
read_verilog -formal ../src/Master_AXI_Write_Data_Channel.v
read_verilog -formal ../src/Master_AXI_Write_Response_Channel.v
read_verilog -formal ../src/Master_AXI_Write_Sequencer.v
read_verilog -formal ../src/skid_buffer_datapath.v
read_verilog -formal ../src/skid_buffer_fsm.v
read_verilog -formal ../src/skid_buffer.v
read_verilog -formal src/faxi_master.v
read_verilog -formal src/pulse_to_level.v
read_verilog -formal src/posedge_pulse_generator.v
read_verilog -formal src/Delay_Line.v
read_verilog -formal src/Annuller.v
read_verilog -formal src/Down_Counter_Zero.v
read_verilog -formal src/Master_AXI_Address_Channel.v
read_verilog -formal src/Master_AXI_Read_Data_Channel.v
read_verilog -formal src/Master_AXI_Read_Sequencer.v
read_verilog -formal src/Master_AXI_Transactor.v
read_verilog -formal src/Master_AXI_Write_Data_Channel.v
read_verilog -formal src/Master_AXI_Write_Response_Channel.v
read_verilog -formal src/Master_AXI_Write_Sequencer.v
read_verilog -formal src/skid_buffer_datapath.v
read_verilog -formal src/skid_buffer_fsm.v
read_verilog -formal src/skid_buffer.v
prep -top Master_AXI_Transactor
memory_nordff
......@@ -26,4 +26,5 @@ setundef -anyseq
opt -keepdc -fast
check
hierarchy -simcheck
tee -o result.log write_ilang design.il
write_ilang design.il
!rm design.il
regression/issue_00814/issue_00814.ys 0 → 100644
logger -expect error "UNDEFINED' is implicitly declared and" 1
read_verilog -formal top.v
regression/issue_00814/issue_00814_fail.ys deleted 100644 → 0
tee -o result.out read_verilog -formal ../top.v
regression/issue_00823/issue_00823.ys
read_ilang ../t2.ilang
read_ilang t2.ilang
synth -run coarse
regression/issue_00826/issue_00826.ys
read_verilog ../top.v
read_verilog top.v
synth
regression/issue_00835/issue_00835.ys
read_verilog ../top.v
logger -expect warning "Replacing memory \\counters with list of registers." 1
read_verilog top.v
prep
select -assert-count 4 t:$dff
regression/issue_00857/issue_00857.ys
read_verilog ../top.v
read_verilog top.v
synth -top top
select -assert-count 1 t:$_DFF_P_
select -assert-none t:$_DFF_P_ %% t:* %D
regression/issue_00862/issue_00862.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
regression/issue_00865/issue_00865.ys
read_verilog ../top.v
read_verilog top.v
write_verilog temp.v
proc
opt
......@@ -8,3 +8,4 @@ memory
opt
synth_xilinx -top tc
select -assert-count 12 t:FDRE
!rm temp.v
regression/issue_00867/issue_00867.ys
read_verilog ../top.v
read_verilog top.v
synth_xilinx -flatten
select -assert-count 1 t:RAMB36E1
regression/issue_00870/issue_00870.ys
read_verilog ../top.v
read_verilog top.v
hierarchy -auto-top -check;
proc; clean;
memory;
......@@ -11,3 +11,5 @@ write_verilog multimux_out_2.v
delete;
read_verilog multimux_out_2.v
!rm multimux_out_1.v
!rm multimux_out_2.v
\ No newline at end of file
regression/issue_00873/issue_00873.ys
read_verilog ../top.v
read_verilog top.v
logger -werror "neg_clk=1.q has an unprocessed"
synth_xilinx
flatten
stat
select -assert-count 1 t:BUFG
select -assert-count 1 t:FDRE
select -assert-count 1 t:FDRE_1
regression/issue_00888/issue_00888.ys
read_verilog -DBROKEN ../top.v
read_verilog top.v
synth_xilinx
select -assert-count 4 t:FDRE
select -assert-count 2 t:FDRE
regression/issue_00888/top.v
module top (CLK, CE, SEL, SI, DO);
parameter SELWIDTH = 1;
parameter DATAWIDTH = 2;
input CLK, CE;
input [DATAWIDTH-1:0] SI;
input [SELWIDTH-1:0] SEL;
output [DATAWIDTH-1:0] DO;
localparam DATADEPTH = 2**SELWIDTH;
reg [0:DATADEPTH-1] data1 [DATAWIDTH-1:0];
reg [DATADEPTH-1:0] data2 [DATAWIDTH-1:0];
generate
genvar i;
for (i = 0; i < DATAWIDTH; i=i+1) begin
always @(posedge CLK)
begin
if (CE == 1'b1) begin
`ifdef BROKEN
data1[i] <= {SI[i], data1[i][0:DATADEPTH-2]};
`else
data2[i] <= {data2[i][DATADEPTH-2:0], SI[i]};
`endif
end
end
`ifdef BROKEN
assign DO[i] = data1[i][SEL];
`else
assign DO[i] = data2[i][SEL];
`endif
end
endgenerate
module top (input clk, sel, di, output do);
reg [0:1] data [0:0];
always @(posedge clk)
data[0] <= {di, data[0][0]};
assign do = data[0][sel];
endmodule
\ No newline at end of file
regression/issue_00896/issue_00896.ys
read_verilog ../outreg.v
read_verilog outreg.v
hierarchy -top dut
proc
memory -nomap
......
regression/issue_00922/issue_00922.ys
read_verilog ../top.v
read_verilog top.v
proc
memory_dff -nordff
memory_collect
opt_reduce
clean
write_firrtl firrtl.firrtl
write_firrtl out.firrtl
!rm out.firrtl
\ No newline at end of file
regression/issue_00931/issue_00931.ys
read_verilog ../top.v
read_verilog top.v
prep
select -assert-none t:$dlatch
regression/issue_00935/issue_00935.ys
read_verilog ../top.v
read_verilog top.v
prep -top picorv32 -nordff
opt -fast
write_smt2 picorv32.smt2
!rm picorv32.smt2
regression/issue_00938/issue_00938.ys
read_verilog ../top.v
read_verilog top.v
proc
memory_dff -nordff
opt_reduce
clean
write_firrtl firrtl.firrtl
write_firrtl out.firrtl
!rm out.firrtl
regression/issue_00940/TopEntity.v
......@@ -6636,7 +6636,7 @@ module TopEntity
reg [14:0] RAM [0:256-1];
initial begin
$readmemb("../SinusTableInit.txt",RAM);
$readmemb("SinusTableInit.txt",RAM);
end
always @(posedge \$d(%,%) [1:1]) begin : TopEntity_blockRamFile
......@@ -6661,7 +6661,7 @@ module TopEntity
reg [14:0] RAM_0 [0:256-1];
initial begin
$readmemb("../SinusTableInit_.txt",RAM_0);
$readmemb("SinusTableInit_.txt",RAM_0);
end
always @(posedge \$d(%,%) [1:1]) begin : TopEntity_blockRamFile_0
......@@ -8334,7 +8334,7 @@ module TopEntity
reg [2:0] RAM_1 [0:1024-1];
initial begin
$readmemb("../LEDMatrixInitial.txt",RAM_1);
$readmemb("LEDMatrixInitial.txt",RAM_1);
end
always @(posedge \$d(%,%) [1:1]) begin : TopEntity_blockRamFile_1
......
regression/issue_00940/issue_00940.ys
read_verilog ../*.v
synth_ice40 -top SuperTopEntity -json TopEntity.json
read_verilog SuperTopEntity.v TopEntity.v
synth_ice40 -top SuperTopEntity
regression/issue_00948/issue_00948.ys
read_ilang ../bug.rtlil
read_ilang bug.rtlil
synth
opt_expr
write_verilog bug.v
delete
read_verilog bug.v
!rm bug.v
regression/issue_00954/issue_00954.ys
read_verilog ../top.v
read_verilog top.v
synth
abc
logger -expect log "Eval result: \\out = 4'1000." 2
eval -set addr 24
aigmap
tee -a result.out eval -set addr 24
eval -set addr 24
regression/issue_00955/issue_00955.pat deleted 100644 → 0
Eval result: \\out = 8'00001000.
regression/issue_00955/issue_00955.ys
read_verilog ../top.v
read_verilog top.v
synth
tee -a result1.out eval -set addr 24
logger -expect log "Eval result: \\out = 8'00001000." 2
eval -set addr 24
abc
tee -a result.out eval -set addr 24
eval -set addr 24
regression/issue_00956/issue_00956.ys
read_verilog ../top.v
tee -a result.log synth_ice40 -top inivalue
read_verilog top.v
logger -expect-no-warnings
synth_ice40 -top inivalue
regression/issue_00961/issue_00961.ys
read_verilog ../top.v
read_verilog top.v
proc
regression/issue_00968/issue_00968.pat deleted 100644 → 0
assign o_value = { 4'hx, i_value }
regression/issue_00968/issue_00968.ys
read -sv ../top.v
read_verilog -sv top.v
hierarchy -top mcve1
synth
write_verilog result.out
sat -verify -prove-asserts -enable_undef -show-ports -prove o_value[3:0] i_value -prove o_value[7:4] 4'bxxxx
regression/issue_00981/issue_00981.ys
read_verilog ../top.v
tee -a result.out synth_ice40
read_verilog top.v
synth_ice40
regression/issue_00982/issue_00982.ys
read_verilog ../top.v
read_verilog top.v
synth_xilinx
select -assert-count 3 t:FDRE
tee -a result.out dump t:FDRE
select -assert-count 3 r:INIT=1'0
regression/issue_00987/issue_00987.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
regression/issue_00993/issue_00993.ys
read -formal ../top.v
read_verilog -formal top.v
hierarchy -top top
synth
#write_verilog rtl_yosys.v
regression/issue_00997/issue_00997.ys deleted 100644 → 0
read -formal ../top.v
hierarchy -top top
synth
write_verilog -noattr result.out
regression/issue_00997/top.v deleted 100644 → 0
module top (y, clk, wire4);
output wire [1:0] y;
input clk;
input signed wire4;
reg [1:0] reg10 = 0;
always @(posedge clk) begin
reg10 <= wire4;
end
assign y = reg10;
endmodule
regression/issue_01014/issue_01014.ys
read_verilog ../top.v
read_verilog top.v
synth
regression/issue_01016/issue_01016.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
proc
wreduce -keepdc
select -assert-count 1 t:$mux
regression/issue_01022/issue_01022.ys
read_verilog -sv ../top.v
tee -a result.log dump
read_verilog -sv top.v
synth -top test
sat -verify -prove-asserts -show-ports -prove b 32'hffffffff
regression/issue_01023/issue_01023.ys
read_verilog -icells ../top.v
read_verilog -icells top.v
techmap
regression/issue_01033/issue_01033.ys
read_verilog ../top.v
read_verilog top.v
synth_xilinx
select -assert-none t:RAM64X1D
regression/issue_01034/issue_01034.ys
read_verilog -DUNPACKED ../top.v
read_verilog -DUNPACKED top.v
synth_xilinx -nodram
select -assert-none t:FDRE
regression/issue_01047/issue_01047.ys
read -formal ../top.v
read -formal top.v
hierarchy -top top
synth
select -assert-count 1 t:$_NOR_
select -assert-none t:$_NOR_ %% t:* %D
sat -verify -prove-asserts -show-ports -set w 3'b100 -prove y 1'b1
\ No newline at end of file
regression/issue_01063/issue_01063_fail.ys → regression/issue_01063/issue_01063.ys
read_verilog ../top.v
read_verilog top.v
proc
logger -expect error "Gate cell u_mid8 not found in module top." 1
fmcombine top u_mid1 u_mid8
regression/issue_01063/issue_01063_fail.pat deleted 100644 → 0
ERROR: Gate cell u_mid8 not found in module top.
regression/issue_01065/issue_01065.ys
read_verilog ../top.v
read_verilog top.v
proc
tee -o result.out opt -fast
logger -werror "Driver-driver conflict"
opt -fast
regression/issue_01065/issue_01065_n.pat deleted 100644 → 0
Warning: Driver-driver conflict for \\q between cell u.i and constant 1'0 in top: Resolved using constant.
regression/issue_01070/issue_01070.ys
read_verilog ../top.v
read_verilog top.v
proc
dff2dffe
simplemap
......
regression/issue_01084/issue_01084.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_01091/issue_01091.ys
read_verilog ../top.v
read_verilog top.v
proc
opt
techmap
......
regression/issue_01093/issue_01093_fail.ys → regression/issue_01093/issue_01093.ys
read_verilog ../top.v
read_verilog top.v
logger -expect error "Design has no top module, use the 'hierarchy' command to specify one." 1
proc
sim
regression/issue_01093/issue_01093_fail.pat deleted 100644 → 0
ERROR: Design has no top module, use the 'hierarchy' command to specify one.
regression/issue_01115/issue_01115.pat deleted 100644 → 0
connect \\\o 33'xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
regression/issue_01115/issue_01115.ys
read_verilog ../top.v
read_verilog -sv top.v
proc
tee -o result.out dump
sat -verify -prove-asserts -show-ports -enable_undef -prove o 33'bxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
\ No newline at end of file
regression/issue_01118/issue_01118.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_01128/issue_01128.ys
read_verilog ../top.v
read_verilog top.v
insbuf
# select just the $_BUF_ from w1 to w2 as @buf
select -set buf w:w1 %coe1 w:w1 %d
......
regression/issue_01131/issue_01131.ys 0 → 100644
logger -expect error "syntax error" 1
read_verilog top.v
regression/issue_01132/issue_01132.ys
read_verilog ../top.v
read_verilog top.v
proc; opt; wreduce; simplemap; muxcover -mux4=150
select -assert-count 1 t:$_MUX4_
regression/issue_01135/issue_01135.ys
read_verilog ../top.v
read_verilog top.v
proc; pmux2shiftx -norange; opt -full
select -assert-count 1 t:$pmux
select -assert-count 3 t:$eq
regression/issue_01144/issue_01144.ys 0 → 100644
read_verilog -specify top.v
regression/issue_01145/issue_01145.ys
read_verilog -sv ../top.sv
read_verilog -sv top.sv
hierarchy -check -top TopModule
proc
flatten
regression/issue_01193/issue_01193.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
logger -expect error "Latch inferred for signal" 1
proc
select -assert-count 0 t:$dlatch
regression/issue_01206/issue_01206.ys
read_ilang ../top.il
read_ilang top.il
proc_init
regression/issue_01216/issue_01216.ys
read_verilog ../top.v
read_verilog top.v
synth_ice40 -top top
write_blif test.blif
regression/issue_01216/top.v
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;
// Empty top module
reg [4:0] op;
reg [31:0] save;
reg [31:0] entry;
reg [31:0] nextresult;
module top (hz100, reset, pb, ss7, ss6, ss5, ss4, ss3, ss2, ss1, ss0, left, right, red, green, blue);
input hz100, reset;
input [20:0] pb;
output [7:0] ss7, ss6, ss5, ss4, ss3, ss2, ss1, ss0, left, right;
output red, green, blue;
wire [31:0] source = displaysave ? save : entry;
assign {left,right} = source[15:0];
reg [31:0] entry; // value being entered
reg [31:0] saved; // saved value to use as a second operand
reg [4:0] op; // the selected operation
reg displaysaved; // show entry or saved?
reg equalpressed; // has equal been pressed?
wire [4:0] key; // outkey of scankey module
wire pressed; // strobe of scankey module
wire [4:0] key;
wire pressed;
scankey sk(.clk(hz100), .strobe(pressed), .out(key), .in(pb));
scankey sk(.clk(hz100), .reset(reset), .inkeys(pb), .strobe(pressed), .outkey(key));
always @ (posedge pressed)
/********************************************************************************/
// This is the mux that causes the same error
reg [31:0] nextresult;
always @(*) begin
case (op)
0: nextresult <= entry;
19: nextresult <= saved + entry;
18: nextresult <= saved - entry;
default: nextresult <= saved;
endcase
end
/********************************************************************************/
always @(posedge pressed, posedge reset)
begin
casez (key)
5'b0????: begin
if (reset) begin
entry <= 0;
saved <= 0;
op <= 0;
displaysaved <= 0;
equalpressed <= 0;
end
else if (key == 5'b10001 && displaysaved == 0) begin
entry <= entry >> 4;
end
else if (key == 5'b10000) begin
saved <= nextresult;
displaysaved <= 1;
equalpressed <= 1;
end
else if (key[4] == 0) begin
if (equalpressed) begin
entry <= {28'b0,key[3:0]};
saved <= 0;
op <= 0;
displaysaved <= 0;
equalpressed <= 0;
end
5'b1????: begin
save <= nextresult;
else begin
if (entry[31:28] == 0)
entry <= entry << 4 | key;
displaysaved <= 0;
end
end
else if (key[4] && key[1]) begin
if (equalpressed == 0)
saved <= nextresult;
op <= key;
displaysaved <= 1;
entry <= 0;
equalpressed <= 0;
end
endcase
end
assign right = num [31:24];
always @(*)
case (op)
0: nextresult = entry;
default: nextresult = save;
endcase
wire [31:0] num = displaysaved ? saved : entry;
ssdec s7(.in(num[31:28]), .enable(1'b1), .out(ss7));
ssdec s6(.in(num[27:24]), .enable(1'b1), .out(ss6));
ssdec s5(.in(num[23:20]), .enable(1'b1), .out(ss5));
ssdec s4(.in(num[19:16]), .enable(1'b1), .out(ss4));
ssdec s3(.in(num[15:12]), .enable(1'b1), .out(ss3));
ssdec s2(.in(num[11:8]), .enable(1'b1), .out(ss2));
ssdec s1(.in(num[7:4]), .enable(1'b1), .out(ss1));
ssdec s0(.in(num[3:0]), .enable(1'b1), .out(ss0));
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;
// Add more modules down here...
module ssdec (in, enable, out);
input [3:0] in;
input enable;
output [7:0] out;
assign out = enable ? in == 4'hF ? 8'b01110001 :
in == 4'hE ? 8'b01111001 :
in == 4'hd ? 8'b01011110 :
in == 4'hC ? 8'b00111001 :
in == 4'hB ? 8'b01111100 :
in == 4'hA ? 8'b01110111 :
in == 4'h9 ? 8'b01101111 :
in == 4'h8 ? 8'b01111111 :
in == 4'h7 ? 8'b00000111 :
in == 4'h6 ? 8'b01111101 :
in == 4'h5 ? 8'b01101101 :
in == 4'h4 ? 8'b01100110 :
in == 4'h3 ? 8'b01001111 :
in == 4'h2 ? 8'b01011011 :
in == 4'h1 ? 8'b00000110 : 8'b00111111 : 8'b0;
endmodule
module scankey (clk, reset, inkeys, strobe, outkey);
input clk, reset;
input [19:0] inkeys;
output strobe;
output [4:0] outkey;
reg [1:0] delay;
always @(posedge clk)
delay <= delay<<1 | active;
assign strobe = delay[1];
always @(posedge clk, posedge reset)
if (reset)
delay <= 0;
else
delay <= delay << 1 | |inkeys;
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;
assign strobe = delay[1];
assign outkey = inkeys [19] ? 5'd19 :
inkeys [18] ? 5'd18 :
inkeys [17] ? 5'd17 :
inkeys [16] ? 5'd16 :
inkeys [15] ? 5'd15 :
inkeys [14] ? 5'd14 :
inkeys [13] ? 5'd13 :
inkeys [12] ? 5'd12 :
inkeys [11] ? 5'd11 :
inkeys [10] ? 5'd10 :
inkeys [ 9] ? 5'd9 :
inkeys [ 8] ? 5'd8 :
inkeys [ 7] ? 5'd7 :
inkeys [ 6] ? 5'd6 :
inkeys [ 5] ? 5'd5 :
inkeys [ 4] ? 5'd4 :
inkeys [ 3] ? 5'd3 :
inkeys [ 2] ? 5'd2 :
inkeys [ 1] ? 5'd1 : 5'd0;
endmodule
\ No newline at end of file
regression/issue_01217/issue_01217.ys
tee -o result.out read_verilog ../top.v
logger -warn "is implicitly declared."
logger -nowarn "is assigned in a block at"
logger -expect-no-warnings
read_verilog top.v
regression/issue_01220/issue_01220.ys
read_verilog ../top.v
read_verilog top.v
hierarchy -top top
proc
flatten
regression/issue_01223/issue_01223.ys
read_verilog ../top.v
read_verilog top.v
synth_xilinx
regression/issue_01225/issue_01225.ys
read_verilog ../top.v
read_verilog top.v
synth_xilinx
select -assert-count 1 t:BUFT
select -assert-count 1 t:IOBUF
regression/issue_01231/issue_01231.ys
read -formal ../top.v
read -formal top.v
regression/issue_01243/issue_01243.ys
read_verilog ../top.v
read_verilog top.v
synth
write_verilog -noattr result.out
cd top
select -assert-none y reg_assign %a %d
regression/issue_01259/issue_01259.ys
read_verilog ../top.v
read_verilog top.v
hierarchy -top top
write_smt2
regression/issue_01273/issue_01273.ys
read_verilog ../top.v
read_verilog top.v
synth -top top
muxcover -mux8
select -assert-count 9 t:$_MUX8_
regression/issue_01284/issue_01284.ys
read_verilog ../top.v
read_verilog top.v
proc
synth -top top
equiv_opt -assert extract_fa -ha -v
......
regression/issue_01329/dff.v deleted 100644 → 0
// Design
// D flip-flop
// https://www.edaplayground.com/x/5dzJ
// If (asynchronous 'reset_sync' & enable') are true on the same clock,
// and then 'reset_sync' is low on the next clock,
// then the asynchronous 'reset_sync' gets ignored and the 'enable' applied
module dff (clk, reset, enable, d, q);
input clk;
input reset;
input enable;
input d;
output reg q;
always @(posedge clk or posedge reset_sync)
begin
if (reset_sync) begin
// Asynchronous reset when reset goes high
q <= 1'b0;
end
else if(enable)
begin
// Assign D to Q on positive clock edge
q <= d;
end
end
wire reset_sync;
synchronizer #(.RESET_STATE(1)) reset_synchronizer(
.clk(clk),
.reset(reset),
.data_i(0),
.data_o(reset_sync));
`ifdef FORMAL
always @($global_clock) assume(clk != $past(clk));
localparam MAX_CNT = 16;
reg[$clog2(MAX_CNT)-1:0] counter;
initial counter = 0;
always @(posedge clk) counter <= counter + 1;
initial assume(reset);
initial assume(enable);
always @(posedge clk) if(counter == (MAX_CNT >> 1)) assume(reset != $past(reset));
//always @(*) assume(d == 1'b1);
always @(clk)
begin
if(clk) assume(d == 1'b0);
else assume(d == 1'b1);
end
always @(clk)
begin
if(clk) assume(!enable);
else assume(enable);
end
always @(posedge clk)
begin
if(reset_sync) assert(q == 0);
else if(enable) assert(q == d);
else assert(q == $past(q));
end
always @(posedge clk) cover(reset && enable && d && !clk);
`endif
endmodule
regression/issue_01329/issue_01329.ys deleted 100644 → 0
# read design
read_verilog ../dff.v
read_verilog -sv ../synchronizer.sv
hierarchy -check
# high-level synthesis
proc; opt; fsm; opt; memory; opt
flatten
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
regression/issue_01329/synchronizer.sv deleted 100644 → 0
// https://github.com/jbush001/NyuziProcessor/blob/master/hardware/core/synchronizer.sv
//
// Copyright 2011-2015 Jeff Bush
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
//
//
// Transfer a signal into a clock domain, avoiding metastability and
// race conditions due to propagation delay.
//
module synchronizer
#(parameter WIDTH = 1,
parameter RESET_STATE = 0)
(input clk,
input reset,
output logic[WIDTH - 1:0] data_o,
input [WIDTH - 1:0] data_i);
logic[WIDTH - 1:0] sync0;
logic[WIDTH - 1:0] sync1;
always_ff @(posedge clk, posedge reset)
begin
if (reset)
begin
sync0 <= {WIDTH{RESET_STATE}};
sync1 <= {WIDTH{RESET_STATE}};
data_o <= {WIDTH{RESET_STATE}};
end
else
begin
sync0 <= data_i;
sync1 <= sync0;
data_o <= sync1;
end
end
endmodule
\ No newline at end of file
regression/issue_01360/issue_01360.ys
read_verilog -sv ../top.v
read_verilog -sv top.v
synth_ice40 -blif out.blif
!rm out.blif
regression/issue_01364/issue_01364.ys
read_verilog ../top.v
read_verilog top.v
regression/issue_01372/issue_01372.ys
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
read_verilog top.v
prep -top test
equiv_opt -assert prep
regression/issue_01372/top.v
////////////////////////////////////////////////////////////////////////////////
//
////////////////////////////////////////////////////////////////////////////////
//
`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;
module test (output reg [3:0] out);
integer k;
initial begin
out = 0;
for(k=0; k<16; k=k+1)
if (k[0]) out = out + 1;
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
\ No newline at end of file
run-new.sh 0 → 100755
#!/bin/bash
#set -x
test -d $1
test -f $2.ys
rm -rf $1/work_$2
mkdir $1/work_$2
cd $1
touch work_$2/.start
if [[ $2 =~ "_fail" ]]; then
#4 - An error expected
if yosys -ql work_$2/yosys.log $2.ys; then
echo FAIL > work_$2/${2}.status
else
echo PASS > work_$2/${2}.status
fi
else
#2 - All asserts in .ys script
yosys -ql work_$2/yosys.log $2.ys
if [ $? != 0 ] ; then
echo FAIL > work_$2/${2}.status
else
echo PASS > work_$2/${2}.status
fi
fi
touch work_$2/.stamp
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