From a1a0abf52afe397e11b63bfc67e82aaf7bf9f498 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Mon, 27 Jul 2020 18:28:01 +0200 Subject: equiv_induct: Fix up assumption for $equiv cells in -undef mode. 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 --- tests/various/equiv_opt_undef.ys | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) create mode 100644 tests/various/equiv_opt_undef.ys (limited to 'tests') diff --git a/tests/various/equiv_opt_undef.ys b/tests/various/equiv_opt_undef.ys new file mode 100644 index 000000000..5d2c60d0a --- /dev/null +++ b/tests/various/equiv_opt_undef.ys @@ -0,0 +1,35 @@ +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 -- cgit v1.2.3