Add nonexcl case test, comment out two others

This commit is contained in:
Eddie Hung 2019-06-07 15:35:15 -07:00
parent ba52d9b471
commit b959bf79c0
2 changed files with 57 additions and 22 deletions

View File

@ -179,3 +179,21 @@ module cliffordwolf_freduce (
if (s == 2) o = d;
end
endmodule
module case_nonexclusive_select (
input wire [1:0] x, y,
input wire a, b, c, d, e,
output reg o
);
always @* begin
case (x)
0, 2: o = b;
1: o = c;
default: begin
o = a;
if (y == 0) o = d;
if (y == 1) o = e;
end
endcase
end
endmodule

View File

@ -1,5 +1,6 @@
read_verilog muxpack.v
design -save read
hierarchy -top mux_if_unbal_4_1
prep
design -save gold
@ -29,20 +30,21 @@ design -import gate -as gate
miter -equiv -flatten -make_assert -make_outputs gold gate miter
sat -verify -prove-asserts -show-ports miter
design -load read
hierarchy -top mux_if_unbal_5_3_invert
prep
design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
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
# TODO: Currently ExclusiveDatabase only analyses $eq cells
#design -load read
#hierarchy -top mux_if_unbal_5_3_invert
#prep
#design -save gold
#muxpack
#opt
#stat
#select -assert-count 0 t:$mux
#select -assert-count 1 t:$pmux
#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 -load read
hierarchy -top mux_if_unbal_5_3_width_mismatch
@ -156,8 +158,8 @@ design -save gold
muxpack
opt
stat
select -assert-count 2 t:$mux
select -assert-count 1 t:$pmux
select -assert-count 4 t:$mux
select -assert-count 0 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate
@ -171,25 +173,40 @@ design -save gold
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
select -assert-count 3 t:$mux
select -assert-count 0 t:$pmux
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 -load read
#hierarchy -top cliffordwolf_freduce
#prep
#design -save gold
#proc; opt; freduce; opt
#show
#muxpack
#opt
#stat
#select -assert-count 0 t:$mux
#select -assert-count 1 t:$pmux
#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 -load read
hierarchy -top cliffordwolf_freduce
hierarchy -top case_nonexclusive_select
prep
design -save gold
proc; opt; freduce; opt
write_verilog -noexpr -norename
muxpack
opt
stat
select -assert-count 0 t:$mux
select -assert-count 1 t:$pmux
select -assert-count 2 t:$pmux
design -stash gate
design -import gold -as gold
design -import gate -as gate