mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-23 00:55:32 +00:00
Merge branch 'master' into struct
This commit is contained in:
Peter Crozier
GitHub
commit
0d3f7ea011
154 changed files with 4100 additions and 2459 deletions
|
|
@ -35,6 +35,7 @@ proc
|
|||
equiv_opt -assert -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)
|
||||
cd mux16 # Constrain all select calls below inside the top module
|
||||
select -assert-count 11 t:SB_LUT4
|
||||
select -assert-min 11 t:SB_LUT4
|
||||
select -assert-max 12 t:SB_LUT4
|
||||
|
||||
select -assert-none t:SB_LUT4 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -1,32 +1,85 @@
|
|||
logger -nowarn "Yosys has only limited support for tri-state logic at the moment\. .*"
|
||||
|
||||
read_verilog <<EOT
|
||||
module top(input C, D, output [7:0] Q);
|
||||
FDRE fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
|
||||
FDSE fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
|
||||
FDCE fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
|
||||
FDPE fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
|
||||
FDRE_1 fd5(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[4]));
|
||||
FDSE_1 fd6(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[5]));
|
||||
FDCE_1 fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6]));
|
||||
FDPE_1 fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7]));
|
||||
FDRE /*#(.INIT(0))*/ fd1(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[0]));
|
||||
FDSE #(.INIT(0)) fd2(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[1]));
|
||||
FDCE #(.INIT(0)) fd3(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[2]));
|
||||
FDPE #(.INIT(0)) fd4(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[3]));
|
||||
FDRE_1 #(.INIT(0)) fd5(.C(C), .CE(1'b1), .D(D), .R(1'b1), .Q(Q[4]));
|
||||
FDSE_1 #(.INIT(0)) fd6(.C(C), .CE(1'b1), .D(D), .S(1'b1), .Q(Q[5]));
|
||||
FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6]));
|
||||
FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7]));
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
|
||||
design -load postopt
|
||||
select -assert-none t:FD*
|
||||
select -assert-count 6 t:FD*
|
||||
select -assert-count 6 c:fd2 c:fd3 c:fd4 c:fd6 c:fd7 c:fd8
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, D, output [7:0] Q);
|
||||
FDRE fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
|
||||
FDSE fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
|
||||
FDCE fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
|
||||
FDPE fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
|
||||
FDRE_1 fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
|
||||
FDSE_1 fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
|
||||
FDCE_1 fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
|
||||
FDPE_1 fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
|
||||
FDRE #(.INIT(0)) fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
|
||||
FDSE #(.INIT(0)) fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
|
||||
FDCE #(.INIT(0)) fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
|
||||
FDPE #(.INIT(0)) fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
|
||||
FDRE_1 /*#(.INIT(0))*/ fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
|
||||
FDSE_1 #(.INIT(0)) fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
|
||||
FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
|
||||
FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
|
||||
endmodule
|
||||
EOT
|
||||
equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
|
||||
design -load postopt
|
||||
select -assert-none t:FD*
|
||||
select -assert-count 4 t:FD*
|
||||
select -assert-count 4 c:fd3 c:fd4 c:fd7 c:fd8
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, D, output [7:0] Q);
|
||||
FDRE #(.INIT(1)) fd1(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[0]));
|
||||
FDSE /*#(.INIT(1))*/ fd2(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[1]));
|
||||
FDCE #(.INIT(1)) fd3(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[2]));
|
||||
FDPE #(.INIT(1)) fd4(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[3]));
|
||||
FDRE_1 #(.INIT(1)) fd5(.C(C), .CE(1'b0), .D(D), .R(1'b0), .Q(Q[4]));
|
||||
FDSE_1 #(.INIT(1)) fd6(.C(C), .CE(1'b0), .D(D), .S(1'b0), .Q(Q[5]));
|
||||
FDCE_1 /*#(.INIT(1))*/ fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6]));
|
||||
FDPE_1 #(.INIT(1)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7]));
|
||||
endmodule
|
||||
EOT
|
||||
logger -expect warning "Module '\$paramod\\FDRE\\INIT=1' contains a \$dff cell .*" 1
|
||||
logger -expect warning "Module '\$paramod\\FDRE_1\\INIT=1' contains a \$dff cell .*" 1
|
||||
logger -expect warning "Module 'FDSE' contains a \$dff cell .*" 1
|
||||
logger -expect warning "Module '\$paramod\\FDSE_1\\INIT=1' contains a \$dff cell .*" 1
|
||||
equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
|
||||
design -load postopt
|
||||
select -assert-count 8 t:FD*
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input clk, clr, pre, output reg q0 = 1'b0, output reg q1 = 1'b1);
|
||||
always @(posedge clk or posedge clr)
|
||||
if (clr)
|
||||
q0 <= 1'b0;
|
||||
else
|
||||
q0 <= ~q0;
|
||||
always @(posedge clk or posedge pre)
|
||||
if (pre)
|
||||
q1 <= 1'b1;
|
||||
else
|
||||
q1 <= ~q1;
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf
|
||||
design -load postopt
|
||||
select -assert-count 1 t:FDCE
|
||||
select -assert-count 1 t:FDPE
|
||||
select -assert-count 2 t:INV
|
||||
select -assert-count 0 t:FD* t:INV %% t:* %D
|
||||
|
||||
logger -expect-no-warnings
|
||||
|
|
|
|||
|
|
@ -1,91 +0,0 @@
|
|||
read_verilog <<EOT
|
||||
module top(input C, CE, D, R, output [1:0] Q);
|
||||
FDRE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[0]));
|
||||
FDRE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .R(R), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDSE
|
||||
select -assert-count 1 t:FDSE_1
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -verify -prove-asserts -show-ports miter
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, CE, D, S, output [1:0] Q);
|
||||
FDSE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[0]));
|
||||
FDSE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .S(S), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDRE
|
||||
select -assert-count 1 t:FDRE_1
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, CE, D, PRE, output [1:0] Q);
|
||||
FDPE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[0]));
|
||||
FDPE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .PRE(PRE), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDCE
|
||||
select -assert-count 1 t:FDCE_1
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
clk2fflogic
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top(input C, CE, D, CLR, output [1:0] Q);
|
||||
FDCE #(.INIT(1'b1)) ff1 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[0]));
|
||||
FDCE_1 #(.INIT(1'b1)) ff2 (.C(C), .CE(CE), .D(D), .CLR(CLR), .Q(Q[1]));
|
||||
endmodule
|
||||
EOT
|
||||
design -save gold
|
||||
|
||||
techmap -map +/xilinx/abc9_map.v -max_iter 1 -D DFF_MODE
|
||||
techmap -map +/xilinx/abc9_unmap.v
|
||||
select -assert-count 1 t:FDPE
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
design -stash gate
|
||||
|
||||
design -import gold -as gold
|
||||
design -import gate -as gate
|
||||
techmap -autoproc -map +/xilinx/cells_sim.v
|
||||
clk2fflogic
|
||||
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -seq 2 -set-init-zero -verify -prove-asserts -show-ports miter
|
||||
|
|
@ -10,10 +10,10 @@ module macc # (parameter SIZEIN = 16, SIZEOUT = 40) (
|
|||
output signed [SIZEOUT-1:0] accum_out
|
||||
);
|
||||
// Declare registers for intermediate values
|
||||
reg signed [SIZEIN-1:0] a_reg, b_reg;
|
||||
reg sload_reg;
|
||||
reg signed [2*SIZEIN-1:0] mult_reg;
|
||||
reg signed [SIZEOUT-1:0] adder_out, old_result;
|
||||
reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0;
|
||||
reg sload_reg = 0;
|
||||
reg signed [2*SIZEIN-1:0] mult_reg = 0;
|
||||
reg signed [SIZEOUT-1:0] adder_out = 0, old_result;
|
||||
always @* /*(adder_out or sload_reg)*/ begin // Modification necessary to fix sim/synth mismatch
|
||||
if (sload_reg)
|
||||
old_result <= 0;
|
||||
|
|
@ -50,10 +50,10 @@ module macc2 # (parameter SIZEIN = 16, SIZEOUT = 40) (
|
|||
output overflow
|
||||
);
|
||||
// Declare registers for intermediate values
|
||||
reg signed [SIZEIN-1:0] a_reg, b_reg, a_reg2, b_reg2;
|
||||
reg signed [SIZEIN-1:0] a_reg = 0, b_reg = 0, a_reg2 = 0, b_reg2 = 0;
|
||||
reg signed [2*SIZEIN-1:0] mult_reg = 0;
|
||||
reg signed [SIZEOUT:0] adder_out = 0;
|
||||
reg overflow_reg;
|
||||
reg overflow_reg = 0;
|
||||
always @(posedge clk) begin
|
||||
//if (ce)
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@ proc
|
|||
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
|
||||
sat -verify -prove-asserts -seq 3 -show-inputs -show-outputs miter
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd macc # Constrain all select calls below inside the top module
|
||||
select -assert-count 1 t:BUFG
|
||||
|
|
@ -20,7 +20,7 @@ proc
|
|||
#equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad ### TODO
|
||||
equiv_opt -run :prove -map +/xilinx/cells_sim.v synth_xilinx -noiopad
|
||||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -seq 10 -show-inputs -show-outputs miter
|
||||
sat -verify -prove-asserts -seq 4 -show-inputs -show-outputs miter
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd macc2 # Constrain all select calls below inside the top module
|
||||
|
||||
|
|
|
|||
|
|
@ -40,8 +40,10 @@ proc
|
|||
equiv_opt -assert -map +/xilinx/cells_sim.v synth_xilinx -noiopad # equivalency check
|
||||
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
|
||||
cd mux16 # Constrain all select calls below inside the top module
|
||||
select -assert-min 5 t:LUT6
|
||||
select -assert-max 2 t:LUT4
|
||||
select -assert-min 4 t:LUT6
|
||||
select -assert-max 7 t:LUT6
|
||||
select -assert-max 2 t:MUXF7
|
||||
dump
|
||||
|
||||
select -assert-none t:LUT6 t:MUXF7 %% t:* %D
|
||||
select -assert-none t:LUT6 t:LUT4 t:MUXF7 %% t:* %D
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
read_verilog -icells <<EOT
|
||||
module \$__XILINX_SHREG_ (input C, input D, input [31:0] L, input E, output Q, output SO);
|
||||
parameter DEPTH = 1;
|
||||
parameter DEPTH = 2;
|
||||
parameter [DEPTH-1:0] INIT = 0;
|
||||
parameter CLKPOL = 1;
|
||||
parameter ENPOL = 2;
|
||||
|
|
|
|||
|
|
@ -29,7 +29,7 @@ endmodule
|
|||
module $__XILINX_SHREG_(input C, D, E, input [1:0] L, output Q);
|
||||
parameter CLKPOL = 1;
|
||||
parameter ENPOL = 1;
|
||||
parameter DEPTH = 1;
|
||||
parameter DEPTH = 2;
|
||||
parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
|
||||
reg [DEPTH-1:0] r = INIT;
|
||||
wire clk = C ^ CLKPOL;
|
||||
|
|
|
|||
|
|
@ -36,9 +36,11 @@ parser.add_argument('-S', '--seed', type = int, help = 'seed for PRNG')
|
|||
parser.add_argument('-c', '--count', type = int, default = 50, help = 'number of test cases to generate')
|
||||
args = parser.parse_args()
|
||||
|
||||
if args.seed is not None:
|
||||
print("PRNG seed: %d" % args.seed)
|
||||
random.seed(args.seed)
|
||||
seed = args.seed
|
||||
if seed is None:
|
||||
seed = random.randrange(sys.maxsize)
|
||||
print("PRNG seed: %d" % seed)
|
||||
random.seed(seed)
|
||||
|
||||
for idx in range(args.count):
|
||||
with open('temp/uut_%05d.v' % idx, 'w') as f:
|
||||
|
|
|
|||
21
tests/opt/bug1758.ys
Normal file
21
tests/opt/bug1758.ys
Normal file
|
|
@ -0,0 +1,21 @@
|
|||
read_verilog -noopt <<EOT
|
||||
module gold(input i, output o);
|
||||
assign o = 1'bx | i;
|
||||
endmodule
|
||||
EOT
|
||||
copy gold coarse
|
||||
copy gold fine
|
||||
|
||||
cd coarse
|
||||
opt_expr
|
||||
select -assert-none c:*
|
||||
|
||||
cd fine
|
||||
opt_expr
|
||||
select -assert-none c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter
|
||||
sat -verify -prove-asserts -show-ports miter
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter2
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
||||
13
tests/opt/opt_clean_init.ys
Normal file
13
tests/opt/opt_clean_init.ys
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
logger -expect warning "Initial value conflict for \\y resolving to 1'0 but with init 1'1" 1
|
||||
logger -expect-no-warnings
|
||||
read_verilog <<EOT
|
||||
module top;
|
||||
(* init=1'b0 *) wire w = 1'b0;
|
||||
(* init=1'bx *) wire x = 1'b0;
|
||||
(* init=1'b1 *) wire y = 1'b0;
|
||||
(* init=1'b0 *) wire z = 1'bx;
|
||||
endmodule
|
||||
EOT
|
||||
clean
|
||||
select -assert-count 1 a:init
|
||||
select -assert-count 1 w:y a:init %i
|
||||
|
|
@ -59,9 +59,8 @@ EOT
|
|||
alumacc
|
||||
equiv_opt -assert opt_expr -fine
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$pos
|
||||
select -assert-count 1 t:$not
|
||||
select -assert-none t:$pos t:$not %% t:* %D
|
||||
select -assert-none t:$not %% t:* %D
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
|
|||
85
tests/opt/opt_expr_and.ys
Normal file
85
tests/opt/opt_expr_and.ys
Normal file
|
|
@ -0,0 +1,85 @@
|
|||
# Single-bit $and
|
||||
read_verilog -noopt <<EOT
|
||||
module gold(input i, output o);
|
||||
assign o = 1'bx & i;
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-count 1 t:$and
|
||||
copy gold coarse
|
||||
copy gold fine
|
||||
copy gold coarse_keepdc
|
||||
copy gold fine_keepdc
|
||||
|
||||
cd coarse
|
||||
opt_expr
|
||||
select -assert-none c:*
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
||||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:*
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
||||
|
||||
|
||||
# Multi-bit $and
|
||||
design -reset
|
||||
read_verilog -noopt <<EOT
|
||||
module gold(input i, output [6:0] o);
|
||||
assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} & {7{i}};
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-count 1 t:$and
|
||||
copy gold coarse
|
||||
copy gold fine
|
||||
copy gold coarse_keepdc
|
||||
copy gold fine_keepdc
|
||||
|
||||
cd coarse
|
||||
opt_expr -fine
|
||||
select -assert-none c:*
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
||||
|
||||
cd coarse_keepdc
|
||||
opt_expr -fine -keepdc
|
||||
select -assert-count 1 c:*
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 2 c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
||||
35
tests/opt/opt_expr_consumex.ys
Normal file
35
tests/opt/opt_expr_consumex.ys
Normal file
|
|
@ -0,0 +1,35 @@
|
|||
read_verilog <<EOT
|
||||
module top(input a, b, output o);
|
||||
wire tmp;
|
||||
assign o = tmp | 1'bx;
|
||||
assign tmp = a & 1'b0;
|
||||
endmodule
|
||||
EOT
|
||||
design -save read
|
||||
select -assert-count 1 t:$and
|
||||
select -assert-count 1 t:$or
|
||||
|
||||
|
||||
opt_expr
|
||||
select -assert-none t:$and t:$or
|
||||
sat -verify -enable_undef -prove o 1'bx
|
||||
|
||||
|
||||
design -load read
|
||||
opt_expr -keepdc
|
||||
select -assert-none t:$and t:$or
|
||||
sat -verify -enable_undef -prove o 1'bx
|
||||
|
||||
|
||||
design -load read
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-none t:$_AND_ t:$_OR_
|
||||
sat -verify -enable_undef -prove o 1'bx
|
||||
|
||||
|
||||
design -load read
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-none t:$_AND_ t:$_OR_
|
||||
sat -verify -enable_undef -prove o 1'bx
|
||||
85
tests/opt/opt_expr_or.ys
Normal file
85
tests/opt/opt_expr_or.ys
Normal file
|
|
@ -0,0 +1,85 @@
|
|||
# Single-bit $or
|
||||
read_verilog -noopt <<EOT
|
||||
module gold(input i, output o);
|
||||
assign o = 1'bx | i;
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-count 1 t:$or
|
||||
copy gold coarse
|
||||
copy gold fine
|
||||
copy gold coarse_keepdc
|
||||
copy gold fine_keepdc
|
||||
|
||||
cd coarse
|
||||
opt_expr
|
||||
select -assert-none c:*
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
||||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:*
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
||||
|
||||
|
||||
# Multi-bit $or
|
||||
design -reset
|
||||
read_verilog -noopt <<EOT
|
||||
module gold(input i, output [6:0] o);
|
||||
assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} | {7{i}};
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-count 1 t:$or
|
||||
copy gold coarse
|
||||
copy gold fine
|
||||
copy gold coarse_keepdc
|
||||
copy gold fine_keepdc
|
||||
|
||||
cd coarse
|
||||
opt_expr -fine
|
||||
select -assert-none c:*
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
||||
|
||||
cd coarse_keepdc
|
||||
opt_expr -fine -keepdc
|
||||
select -assert-count 1 c:*
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 2 c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
||||
131
tests/opt/opt_expr_xnor.ys
Normal file
131
tests/opt/opt_expr_xnor.ys
Normal file
|
|
@ -0,0 +1,131 @@
|
|||
# Single-bit $xnor
|
||||
read_verilog -noopt <<EOT
|
||||
module gold(input i, output o);
|
||||
assign o = 1'bx ~^ i;
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-count 1 t:$xnor
|
||||
copy gold coarse
|
||||
copy gold fine
|
||||
copy gold coarse_keepdc
|
||||
copy gold fine_keepdc
|
||||
|
||||
cd coarse
|
||||
opt_expr
|
||||
select -assert-none t:$xnor
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:t$_XNOR_
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
||||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:*
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 t:$_XOR_
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
||||
|
||||
|
||||
# Multi-bit $xnor
|
||||
design -reset
|
||||
read_verilog -noopt <<EOT
|
||||
module gold(input i, output [6:0] o);
|
||||
assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} ~^ {7{i}};
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-count 1 t:$xnor
|
||||
copy gold coarse
|
||||
copy gold fine
|
||||
copy gold coarse_keepdc
|
||||
copy gold fine_keepdc
|
||||
|
||||
cd coarse
|
||||
opt_expr -fine
|
||||
select -assert-none t:$xnor
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none t:$_XNOR_
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
||||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc -fine
|
||||
select -assert-count 1 t:$xnor
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 0 c:$_XOR_
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
||||
|
||||
|
||||
# Single-bit $xnor extension
|
||||
design -reset
|
||||
read_verilog -noopt <<EOT
|
||||
module gold(input i, output [1:0] o, p, q);
|
||||
assign o = i ~^ i;
|
||||
assign p = 1'b0 ~^ i;
|
||||
assign q = 1'b1 ~^ i;
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-count 3 t:$xnor
|
||||
copy gold coarse
|
||||
copy gold fine
|
||||
copy gold coarse_keepdc
|
||||
copy gold fine_keepdc
|
||||
|
||||
cd coarse
|
||||
opt_expr -fine
|
||||
select -assert-none t:$xnor
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none t:$_XNOR_
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
||||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc -fine
|
||||
select -assert-count 1 t:$xnor
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 0 c:$_XNOR_
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
||||
|
|
@ -50,3 +50,91 @@ assign z = a~^1'b1;
|
|||
endmodule
|
||||
EOT
|
||||
equiv_opt opt_expr
|
||||
|
||||
|
||||
# Single-bit $xor
|
||||
design -reset
|
||||
read_verilog -noopt <<EOT
|
||||
module gold(input i, output o);
|
||||
assign o = 1'bx ^ i;
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-count 1 t:$xor
|
||||
copy gold coarse
|
||||
copy gold fine
|
||||
copy gold coarse_keepdc
|
||||
copy gold fine_keepdc
|
||||
|
||||
cd coarse
|
||||
opt_expr
|
||||
select -assert-none c:*
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
||||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:*
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 1 c:*
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
||||
|
||||
|
||||
# Multi-bit $xor
|
||||
design -reset
|
||||
read_verilog -noopt <<EOT
|
||||
module gold(input i, output [6:0] o);
|
||||
assign o = {1'bx, 1'b0, 1'b0, 1'b1, 1'bx, 1'b1, i} ^ {7{i}};
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-count 1 t:$xor
|
||||
copy gold coarse
|
||||
copy gold fine
|
||||
copy gold coarse_keepdc
|
||||
copy gold fine_keepdc
|
||||
|
||||
cd coarse
|
||||
opt_expr -fine
|
||||
select -assert-count 0 t:$xor
|
||||
|
||||
cd fine
|
||||
simplemap
|
||||
opt_expr
|
||||
select -assert-none t:$_XOR_
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold coarse miter
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse fine miter2
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter2
|
||||
|
||||
cd coarse_keepdc
|
||||
opt_expr -keepdc -fine
|
||||
select -assert-count 1 t:$xor
|
||||
|
||||
cd fine_keepdc
|
||||
simplemap
|
||||
opt_expr -keepdc
|
||||
select -assert-count 3 t:$_XOR_
|
||||
|
||||
cd
|
||||
miter -equiv -flatten -make_assert -make_outputs gold coarse_keepdc miter3
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter3
|
||||
miter -equiv -flatten -make_assert -make_outputs coarse_keepdc fine_keepdc miter4
|
||||
sat -verify -prove-asserts -show-ports -enable_undef miter4
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
module constmuldivmod(input [7:0] A, input [2:0] mode, output reg [7:0] Y);
|
||||
module constmuldivmod(input [7:0] A, input [5:0] mode, output reg [7:0] Y);
|
||||
always @* begin
|
||||
case (mode)
|
||||
0: Y = A / 8'd0;
|
||||
|
|
@ -21,6 +21,46 @@ module constmuldivmod(input [7:0] A, input [2:0] mode, output reg [7:0] Y);
|
|||
13: Y = A % 8'd8;
|
||||
14: Y = A * 8'd8;
|
||||
|
||||
15: Y = $signed(A) / $signed(8'd0);
|
||||
16: Y = $signed(A) % $signed(8'd0);
|
||||
17: Y = $signed(A) * $signed(8'd0);
|
||||
|
||||
18: Y = $signed(A) / $signed(8'd1);
|
||||
19: Y = $signed(A) % $signed(8'd1);
|
||||
20: Y = $signed(A) * $signed(8'd1);
|
||||
|
||||
21: Y = $signed(A) / $signed(8'd2);
|
||||
22: Y = $signed(A) % $signed(8'd2);
|
||||
23: Y = $signed(A) * $signed(8'd2);
|
||||
|
||||
24: Y = $signed(A) / $signed(8'd4);
|
||||
25: Y = $signed(A) % $signed(8'd4);
|
||||
26: Y = $signed(A) * $signed(8'd4);
|
||||
|
||||
27: Y = $signed(A) / $signed(8'd8);
|
||||
28: Y = $signed(A) % $signed(8'd8);
|
||||
29: Y = $signed(A) * $signed(8'd8);
|
||||
|
||||
30: Y = $signed(A) / $signed(-8'd0);
|
||||
31: Y = $signed(A) % $signed(-8'd0);
|
||||
32: Y = $signed(A) * $signed(-8'd0);
|
||||
|
||||
33: Y = $signed(A) / $signed(-8'd1);
|
||||
34: Y = $signed(A) % $signed(-8'd1);
|
||||
35: Y = $signed(A) * $signed(-8'd1);
|
||||
|
||||
36: Y = $signed(A) / $signed(-8'd2);
|
||||
37: Y = $signed(A) % $signed(-8'd2);
|
||||
38: Y = $signed(A) * $signed(-8'd2);
|
||||
|
||||
39: Y = $signed(A) / $signed(-8'd4);
|
||||
40: Y = $signed(A) % $signed(-8'd4);
|
||||
41: Y = $signed(A) * $signed(-8'd4);
|
||||
|
||||
42: Y = $signed(A) / $signed(-8'd8);
|
||||
43: Y = $signed(A) % $signed(-8'd8);
|
||||
44: Y = $signed(A) * $signed(-8'd8);
|
||||
|
||||
default: Y = 8'd16 * A;
|
||||
endcase
|
||||
end
|
||||
|
|
|
|||
3
tests/simple_abc9/abc9.box
Normal file
3
tests/simple_abc9/abc9.box
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
MUXF8 1 0 3 1
|
||||
#I0 I1 S
|
||||
0 0 0 # O
|
||||
|
|
@ -213,7 +213,7 @@ module arbiter (clk, rst, request, acknowledge, grant, grant_valid, grant_encode
|
|||
input rst;
|
||||
endmodule
|
||||
|
||||
(* abc9_box, blackbox *)
|
||||
(* abc9_box_id=1, blackbox *)
|
||||
module MUXF8(input I0, I1, S, output O);
|
||||
specify
|
||||
(I0 => O) = 0;
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v *.sv EXTRA_FLAGS="-n 300 -p
|
|||
synth -run coarse; \
|
||||
opt -full; \
|
||||
techmap; \
|
||||
abc9 -lut 4; \
|
||||
abc9 -lut 4 -box ../abc9.box; \
|
||||
clean; \
|
||||
check -assert; \
|
||||
select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%; \
|
||||
|
|
|
|||
6
tests/svtypes/logic_rom.sv
Normal file
6
tests/svtypes/logic_rom.sv
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
module top(input [3:0] addr, output [7:0] data);
|
||||
logic [7:0] mem[0:15];
|
||||
assign data = mem[addr];
|
||||
integer i;
|
||||
initial for(i = 0; i < 16; i = i + 1) mem[i] = i;
|
||||
endmodule
|
||||
3
tests/svtypes/logic_rom.ys
Normal file
3
tests/svtypes/logic_rom.ys
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
read_verilog -sv logic_rom.sv
|
||||
prep -top top
|
||||
select -assert-count 1 t:$mem r:SIZE=16 %i r:WIDTH=8 %i
|
||||
|
|
@ -45,14 +45,16 @@ sat -seq 10 -verify -prove-asserts -show-ports miter
|
|||
design -reset
|
||||
read_verilog -icells <<EOT
|
||||
module abc9_test036(input clk, d, output q);
|
||||
(* keep *) reg w;
|
||||
$__ABC9_FF_ ff(.D(d), .Q(w));
|
||||
wire \ff.clock = clk;
|
||||
wire \ff.init = 1'b0;
|
||||
(* keep, init=1'b0 *) wire w;
|
||||
$_DFF_P_ ff(.C(clk), .D(d), .Q(w));
|
||||
assign q = w;
|
||||
endmodule
|
||||
EOT
|
||||
abc9 -lut 4 -dff
|
||||
equiv_opt -assert abc9 -lut 4 -dff
|
||||
design -load postopt
|
||||
cd abc9_test036
|
||||
select -assert-count 1 t:$_DFF_P_
|
||||
select -assert-none t:* t:$_DFF_P_ %d
|
||||
|
||||
|
||||
design -reset
|
||||
|
|
@ -67,8 +69,32 @@ specify
|
|||
endspecify
|
||||
endmodule
|
||||
|
||||
module top(input [1:0] i, output o);
|
||||
module abc9_test037(input [1:0] i, output o);
|
||||
LUT2 #(.mask(4'b0)) lut (.i(i), .o(o));
|
||||
endmodule
|
||||
EOT
|
||||
abc9
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog -icells <<EOT
|
||||
module abc9_test038(input clk, output w, x, y, z);
|
||||
(* init=1'b1 *) wire w;
|
||||
$_DFF_N_ ff1(.C(clk), .D(1'b1), .Q(w));
|
||||
(* init=1'bx *) wire x;
|
||||
$_DFF_N_ ff2(.C(clk), .D(1'b0), .Q(x));
|
||||
(* init=1'b0 *) wire y;
|
||||
$_DFF_N_ ff3(.C(clk), .D(1'b0), .Q(y));
|
||||
(* init=1'b0 *) wire z;
|
||||
$_DFF_N_ ff4(.C(clk), .D(1'b1), .Q(z));
|
||||
endmodule
|
||||
EOT
|
||||
simplemap
|
||||
equiv_opt abc9 -lut 4 -dff
|
||||
design -load postopt
|
||||
cd abc9_test038
|
||||
select -assert-count 3 t:$_DFF_N_
|
||||
select -assert-none c:ff1 c:ff2 c:ff4 %% c:* %D
|
||||
clean
|
||||
select -assert-count 2 a:init
|
||||
select -assert-none w:w w:z %% a:init %D
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ module foo(clk, rst, inp_a, inp_b, out);
|
|||
input wire rst;
|
||||
input wire [7:0] inp_a;
|
||||
input wire [7:0] inp_b;
|
||||
output wire [7:0] out;
|
||||
output reg [7:0] out;
|
||||
|
||||
always @(posedge clk)
|
||||
if (rst) out <= 0;
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(* techmap_celltype = "$reduce_or" *)
|
||||
module my_opt_reduce_or(...);
|
||||
parameter A_SIGNED = 0;
|
||||
parameter A_WIDTH = 1;
|
||||
parameter A_WIDTH = 2;
|
||||
parameter Y_WIDTH = 1;
|
||||
|
||||
input [A_WIDTH-1:0] A;
|
||||
|
|
|
|||
14
tests/various/printattr.ys
Normal file
14
tests/various/printattr.ys
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
logger -expect log ".*cells_not_processed=[01]* .*" 1
|
||||
logger -expect log ".*src=.<<EOT:1\.1-9\.10. .*" 1
|
||||
read_verilog <<EOT
|
||||
module mux2(a, b, s, y);
|
||||
input a, b, s;
|
||||
output y;
|
||||
|
||||
wire s_n = ~s;
|
||||
wire t0 = s & a;
|
||||
wire t1 = s_n & b;
|
||||
assign y = t0 | t1;
|
||||
endmodule
|
||||
EOT
|
||||
printattrs
|
||||
|
|
@ -13,7 +13,7 @@ assign q = {shift2[3], shift1[3]};
|
|||
endmodule
|
||||
|
||||
module $__SHREG_DFF_P_(input C, D, output Q);
|
||||
parameter DEPTH = 1;
|
||||
parameter DEPTH = 2;
|
||||
parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
|
||||
reg [DEPTH-1:0] r = INIT;
|
||||
always @(posedge C)
|
||||
|
|
@ -38,7 +38,7 @@ endmodule
|
|||
module $__XILINX_SHREG_(input C, D, input [1:0] L, output Q);
|
||||
parameter CLKPOL = 1;
|
||||
parameter ENPOL = 1;
|
||||
parameter DEPTH = 1;
|
||||
parameter DEPTH = 2;
|
||||
parameter [DEPTH-1:0] INIT = {DEPTH{1'b0}};
|
||||
reg [DEPTH-1:0] r = INIT;
|
||||
wire clk = C ^ CLKPOL;
|
||||
|
|
|
|||
13
tests/various/xaiger.ys
Normal file
13
tests/various/xaiger.ys
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
read_verilog <<EOT
|
||||
module top(input a, b, output c);
|
||||
bb #(1) bb();
|
||||
endmodule
|
||||
|
||||
module bb(input a, b, output c);
|
||||
parameter p = 0;
|
||||
assign c = a ^ b;
|
||||
endmodule
|
||||
EOT
|
||||
blackbox bb
|
||||
hierarchy
|
||||
write_xaiger /dev/null
|
||||
3
tests/verilog/.gitignore
vendored
Normal file
3
tests/verilog/.gitignore
vendored
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
/*.log
|
||||
/*.out
|
||||
/run-test.mk
|
||||
58
tests/verilog/bug2037.ys
Normal file
58
tests/verilog/bug2037.ys
Normal file
|
|
@ -0,0 +1,58 @@
|
|||
logger -expect-no-warnings
|
||||
read_verilog <<EOT
|
||||
module test ();
|
||||
localparam y = 1;
|
||||
always @(*)
|
||||
if (y) (* foo *) ;
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-none a:* a:src %d
|
||||
|
||||
|
||||
design -reset
|
||||
logger -expect-no-warnings
|
||||
read_verilog <<EOT
|
||||
module test ();
|
||||
localparam y = 1;
|
||||
always @(*)
|
||||
if (y) (* foo *) ; else (* bar *) ;
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-none a:* a:src %d
|
||||
|
||||
|
||||
design -reset
|
||||
logger -expect-no-warnings
|
||||
read_verilog <<EOT
|
||||
module test ();
|
||||
localparam y = 1;
|
||||
generate if (y) (* foo *) ; endgenerate
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-none a:*
|
||||
|
||||
|
||||
design -reset
|
||||
logger -expect-no-warnings
|
||||
read_verilog <<EOT
|
||||
module test ();
|
||||
localparam y = 1;
|
||||
generate if (y) (* foo *) ; else (* bar *); endgenerate
|
||||
endmodule
|
||||
EOT
|
||||
select -assert-none a:*
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module test ();
|
||||
localparam y = 1;
|
||||
reg x = 1'b0;
|
||||
always @(*) begin
|
||||
if (y)
|
||||
(* foo *) x <= 1'b1;
|
||||
else
|
||||
(* bar *) x = 1'b0;
|
||||
end
|
||||
endmodule
|
||||
EOT
|
||||
59
tests/verilog/bug2042-sv.ys
Normal file
59
tests/verilog/bug2042-sv.ys
Normal file
|
|
@ -0,0 +1,59 @@
|
|||
read_verilog -sv <<EOT
|
||||
module Task_Test_Top
|
||||
(
|
||||
input a,
|
||||
output reg b
|
||||
);
|
||||
|
||||
task SomeTaskName(a);
|
||||
b = ~a;
|
||||
endtask
|
||||
|
||||
always @*
|
||||
SomeTaskName(a);
|
||||
|
||||
assert property (b == ~a);
|
||||
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
sat -verify -prove-asserts
|
||||
|
||||
|
||||
design -reset
|
||||
read_verilog -sv <<EOT
|
||||
module Task_Test_Top
|
||||
(
|
||||
input a,
|
||||
output b, c
|
||||
);
|
||||
|
||||
task SomeTaskName(x, output y, z);
|
||||
y = ~x;
|
||||
z = x;
|
||||
endtask
|
||||
|
||||
always @*
|
||||
SomeTaskName(a, b, c);
|
||||
|
||||
assert property (b == ~a);
|
||||
assert property (c == a);
|
||||
|
||||
endmodule
|
||||
EOT
|
||||
proc
|
||||
sat -verify -prove-asserts
|
||||
|
||||
|
||||
design -reset
|
||||
logger -expect error "syntax error, unexpected TOK_ENDTASK, expecting ';'" 1
|
||||
read_verilog -sv <<EOT
|
||||
module Task_Test_Top
|
||||
(
|
||||
);
|
||||
|
||||
task SomeTaskName(a)
|
||||
endtask
|
||||
|
||||
endmodule
|
||||
EOT
|
||||
11
tests/verilog/bug2042.ys
Normal file
11
tests/verilog/bug2042.ys
Normal file
|
|
@ -0,0 +1,11 @@
|
|||
logger -expect error "task/function argument direction missing" 1
|
||||
read_verilog <<EOT
|
||||
module Task_Test_Top
|
||||
(
|
||||
);
|
||||
|
||||
task SomeTaskName(a)
|
||||
endtask
|
||||
|
||||
endmodule
|
||||
EOT
|
||||
20
tests/verilog/run-test.sh
Executable file
20
tests/verilog/run-test.sh
Executable file
|
|
@ -0,0 +1,20 @@
|
|||
#!/usr/bin/env bash
|
||||
set -e
|
||||
{
|
||||
echo "all::"
|
||||
for x in *.ys; do
|
||||
echo "all:: run-$x"
|
||||
echo "run-$x:"
|
||||
echo " @echo 'Running $x..'"
|
||||
echo " @../../yosys -ql ${x%.ys}.log $x"
|
||||
done
|
||||
for s in *.sh; do
|
||||
if [ "$s" != "run-test.sh" ]; then
|
||||
echo "all:: run-$s"
|
||||
echo "run-$s:"
|
||||
echo " @echo 'Running $s..'"
|
||||
echo " @bash $s"
|
||||
fi
|
||||
done
|
||||
} > run-test.mk
|
||||
exec ${MAKE:-make} -f run-test.mk
|
||||
28
tests/verilog/task_attr.ys
Normal file
28
tests/verilog/task_attr.ys
Normal file
|
|
@ -0,0 +1,28 @@
|
|||
read_verilog <<EOT
|
||||
module top;
|
||||
task foo;
|
||||
endtask
|
||||
|
||||
always @*
|
||||
(* foo *) foo;
|
||||
|
||||
initial
|
||||
if (0) $info("bar");
|
||||
endmodule
|
||||
EOT
|
||||
# Since task enables are not an RTLIL object,
|
||||
# any attributes on their AST get dropped
|
||||
select -assert-none a:* a:src %d
|
||||
|
||||
|
||||
logger -expect error "syntax error, unexpected ATTR_BEGIN" 1
|
||||
design -reset
|
||||
read_verilog <<EOT
|
||||
module top;
|
||||
task foo;
|
||||
endtask
|
||||
|
||||
always @*
|
||||
foo (* foo *);
|
||||
endmodule
|
||||
EOT
|
||||
4
tests/verilog/upto.ys
Normal file
4
tests/verilog/upto.ys
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
read_verilog <<EOT
|
||||
module top(input [-128:-65] a);
|
||||
endmodule
|
||||
EOT
|
||||
Loading…
Add table
Add a link
Reference in a new issue