mirror of https://github.com/YosysHQ/yosys.git
Add #1135 testcase
This commit is contained in:
parent
7c14678ec0
commit
18acb72c05
|
@ -32,3 +32,13 @@ module pmux2shiftx_test (
|
|||
endcase
|
||||
end
|
||||
endmodule
|
||||
|
||||
module issue01135(input [7:0] i, output o);
|
||||
always @*
|
||||
case (i[6:3])
|
||||
4: o <= i[0];
|
||||
3: o <= i[2];
|
||||
7: o <= i[3];
|
||||
default: o <= 1'b0;
|
||||
endcase
|
||||
endmodule
|
||||
|
|
|
@ -1,4 +1,7 @@
|
|||
read_verilog pmux2shiftx.v
|
||||
design -save read
|
||||
|
||||
hierarchy -top pmux2shiftx_test
|
||||
prep
|
||||
design -save gold
|
||||
|
||||
|
@ -21,8 +24,16 @@ design -import gate -as gate
|
|||
miter -equiv -flatten -make_assert -make_outputs gold gate miter
|
||||
sat -verify -prove-asserts -show-ports miter
|
||||
|
||||
design -load gold
|
||||
stat
|
||||
#design -load gold
|
||||
#stat
|
||||
#
|
||||
#design -load gate
|
||||
#stat
|
||||
|
||||
design -load gate
|
||||
stat
|
||||
design -load read
|
||||
hierarchy -top issue01135
|
||||
proc
|
||||
pmux2shiftx -norange
|
||||
opt -full
|
||||
select -assert-count 0 t:$shift*
|
||||
select -assert-count 1 t:$pmux
|
||||
|
|
Loading…
Reference in New Issue