riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Simplify opt_expr tests using equiv_opt

This commit is contained in:
Eddie Hung 2019-08-09 10:08:17 -07:00
parent ac2fc3a144
commit d9c1664462
1 changed files with 23 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

95
tests/opt/opt_expr.ys
View File

@ -6,24 +6,16 @@ endmodule
EOT EOT
hierarchy -auto-top hierarchy -auto-top
proc
design -save gold
opt_expr -fine equiv_opt -assert opt_expr -fine
design -load postopt
wreduce wreduce
select -assert-count 1 t:$add r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i select -assert-count 1 t:$add r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
########## ##########
design -reset
read_verilog <<EOT read_verilog <<EOT
module opt_expr_add_signed_test(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o); module opt_expr_add_signed_test(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
assign o = (i << 4) + j; assign o = (i << 4) + j;
@ -31,24 +23,16 @@ endmodule
EOT EOT
hierarchy -auto-top hierarchy -auto-top
proc
design -save gold
opt_expr -fine equiv_opt -assert opt_expr -fine
design -load postopt
wreduce wreduce
select -assert-count 1 t:$add r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i select -assert-count 1 t:$add r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
########## ##########
design -reset
read_verilog <<EOT read_verilog <<EOT
module opt_expr_sub_test1(input [3:0] i, input [7:0] j, output [8:0] o); module opt_expr_sub_test1(input [3:0] i, input [7:0] j, output [8:0] o);
assign o = j - (i << 4); assign o = j - (i << 4);
@ -56,24 +40,16 @@ endmodule
EOT EOT
hierarchy -auto-top hierarchy -auto-top
proc
design -save gold
opt_expr -fine equiv_opt -assert opt_expr -fine
design -load postopt
wreduce wreduce
select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
########## ##########
design -reset
read_verilog <<EOT read_verilog <<EOT
module opt_expr_sub_signed_test1(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o); module opt_expr_sub_signed_test1(input signed [3:0] i, input signed [7:0] j, output signed [8:0] o);
assign o = j - (i << 4); assign o = j - (i << 4);
@ -81,24 +57,16 @@ endmodule
EOT EOT
hierarchy -auto-top hierarchy -auto-top
proc
design -save gold
opt_expr -fine equiv_opt -assert opt_expr -fine
design -load postopt
wreduce wreduce
select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i select -assert-count 1 t:$sub r:A_WIDTH=4 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
########## ##########
design -reset
read_verilog <<EOT read_verilog <<EOT
module opt_expr_sub_test2(input [3:0] i, input [7:0] j, output [8:0] o); module opt_expr_sub_test2(input [3:0] i, input [7:0] j, output [8:0] o);
assign o = (i << 4) - j; assign o = (i << 4) - j;
@ -106,24 +74,16 @@ endmodule
EOT EOT
hierarchy -auto-top hierarchy -auto-top
proc
design -save gold
opt_expr -fine equiv_opt -assert opt_expr -fine
design -load postopt
wreduce wreduce
select -assert-count 1 t:$sub r:A_WIDTH=8 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i select -assert-count 1 t:$sub r:A_WIDTH=8 r:B_WIDTH=8 r:Y_WIDTH=9 %i %i %i
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
########## ##########
design -reset
read_verilog <<EOT read_verilog <<EOT
module opt_expr_sub_test4(input [3:0] i, output [8:0] o); module opt_expr_sub_test4(input [3:0] i, output [8:0] o);
assign o = 5'b00010 - i; assign o = 5'b00010 - i;
@ -131,18 +91,9 @@ endmodule
EOT EOT
hierarchy -auto-top hierarchy -auto-top
proc
design -save gold
opt_expr -fine equiv_opt -assert opt_expr -fine
design -load postopt
wreduce wreduce
select -assert-count 1 t:$sub r:A_WIDTH=2 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i select -assert-count 1 t:$sub r:A_WIDTH=2 r:B_WIDTH=4 r:Y_WIDTH=5 %i %i %i
design -stash gate
design -import gold -as gold
design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter