mirror of
https://github.com/YosysHQ/yosys
synced 2025-11-03 21:09:12 +00:00
a1a0abf52a
Before this fix, equiv_induct only assumed that one of the following is true: - defined value of A is equal to defined value of B - A is undefined This lets through valuations where A is defined, B is undefined, and the defined (meaningless) value of B happens to match the defined value of A. Instead, tighten this up to OR of the following: - defined value of A is equal to defined value of B, and B is not undefined - A is undefined
35 lines
545 B
Text
35 lines
545 B
Text
read_ilang << EOT
|
|
|
|
module \top
|
|
wire $a
|
|
wire $b
|
|
wire input 1 \D
|
|
wire input 2 \EN
|
|
wire output 3 \Q
|
|
cell $mux $x
|
|
parameter \WIDTH 1
|
|
connect \A \Q
|
|
connect \B \D
|
|
connect \S \EN
|
|
connect \Y $a
|
|
end
|
|
cell $ff $y
|
|
parameter \WIDTH 1
|
|
connect \D $a
|
|
connect \Q $b
|
|
end
|
|
cell $and $z
|
|
parameter \A_SIGNED 0
|
|
parameter \A_WIDTH 1
|
|
parameter \B_SIGNED 0
|
|
parameter \B_WIDTH 1
|
|
parameter \Y_WIDTH 1
|
|
connect \A $b
|
|
connect \B 1'x
|
|
connect \Y \Q
|
|
end
|
|
end
|
|
|
|
EOT
|
|
|
|
equiv_opt -assert -undef ls
|