Verilog: fix the constant-expression interpreter for the conditional operator and zero-width replication

[kroening]

Fixes the three KNOWNBUG tests added in #2086.

1. The conditional operator is not short-circuited (1800-2017 11.4.11)

Root cause. verilog_simplifier_rec (src/verilog/verilog_simplifier.cpp), which
implements the constant-expression interpreter, recursed into all operands of an
expression and gave up as soon as any operand failed to simplify to a constant. For
ID_if, that meant both arms were evaluated even when the condition was known. The
CBMC simplifier deliberately refuses to fold a division by zero, so

wire [(0 ? 1/0 : 3)-1:0] x;

failed with expected constant expression, but got `(0 ? 1 / 0 : 3) - 1'. This is
the usual idiom for guarding a width computation against a degenerate parameter value.

Fix. verilog_simplifier_rec now simplifies the condition of an ID_if first, and,
if the condition is a definite true/false, returns the simplified taken arm without
touching the other one — exactly what 11.4.11 mandates.

Short-circuiting vs. x-propagation

#2086 notes that a fix could equally come from propagating x out of a division by
zero (11.4.4). I chose short-circuiting, for three reasons:

• 11.4.11 requires it independently of 11.4.4. Short-circuiting fixes the whole
  class of guarded width computations, not just the division-by-zero instance: e.g.
  0 ? f(...) : 3 or 0 ? p[i] : 3 with an out-of-range i are guarded too, and no
  amount of x-propagation would help there.
• X-propagation from division by zero is not implemented anywhere in the tool
  today — not just in the constant-expression interpreter. wire [3:0] y = 4'd1/4'd0;
  currently synthesises to 0, not 4'bxxxx. Making 11.4.4 work would mean touching
  the aval/bval encoding and synthesis as well, which is a separate, larger change,
  and it would still leave 11.4.11 unimplemented.
• X-propagation alone would additionally have to introduce a four-valued type into
  what may be a two-state constant expression, which the conditional operator would
  then have to merge back.

So the two are complementary rather than alternatives; this PR does the 11.4.11 half.
11.4.4 remains unimplemented and is called out as a limitation below.

2. Zero-width replication is not a constant expression (1800-2017 11.4.12.1)

Root cause. verilog_simplifier_rec lowered a replication to a concatenation of
times copies of the operand. For times == 0 that produced an empty
concatenation, which is neither a constant nor something the simplifier can fold, so
the enclosing concatenation was given up on as well. Hence

localparam [3:0] p = {2'b10, {0{1'b1}}, 2'b01};  // rejected
wire      [3:0] x = {2'b10, {0{1'b1}}, 2'b01};  // accepted

(As an aside, simplify_concatenation computes operands().size() - 1 unsigned, so
feeding it an empty concatenation was undefined behaviour.)

Fix.

• Zero-width operands of a concatenation are dropped before the operands are
  simplified, since per 11.4.12.1 they contribute nothing. (An empty concatenation is
  never created.)
• A replication with a zero replication constant now yields a zero-width constant
  instead of an empty concatenation.

3. Zero replication outside a concatenation is now diagnosed properly

11.4.12.1 only permits a zero replication constant inside a concatenation that has
at least one operand of nonzero size. Before this PR, a standalone
wire [3:0] x = {0{1'b1}}; was silently accepted, while the same in a constant
context gave a confusing "expected constant expression" (with an ireprinted
zero-width concatenation in the message).

convert_replication_expr now takes a zero_allowed flag, set only for operands that
appear directly within a concatenation, and convert_expr_concatenation rejects a
concatenation whose total width is zero. New tests replication5 and replication6
cover the two error cases.

Tests

regression/verilog/expressions/conditional_operator_short_circuit{1,2}.desc and
replication4.desc flipped from KNOWNBUG to CORE; replication4 asserts the
resulting value of both p and x. Two new error tests added.

Verified locally (Clang, macOS, MiniSat + Z3 4.16.0):

• make -C regression/verilog test — All tests were successful, 220 tests skipped
• make -C regression/verilog test-z3 — All tests were successful, 227 tests skipped
• make -C regression/ebmc test — All tests were successful, 9 tests skipped
• make -C regression/ebmc test-z3 — All tests were successful, 12 tests skipped
• make -C regression/smv test — All tests were successful, 32 tests skipped
• make -C regression/vlindex test — All tests were successful
• make -C unit — All tests passed (190 assertions in 45 test cases)

Known limitations

• 11.4.4 (division/modulo by zero yielding x) is still not implemented, in neither
  the constant-expression interpreter nor synthesis. A bare localparam p = 1/0; still
  reports "expected constant expression" rather than elaborating to x.
• The short-circuiting applies to the two-valued conditional operator. A conditional
  operator with a four-valued result is rewritten into the aval/bval encoding by
  verilog_lowering before the interpreter sees it, so both arms are still elaborated
  in that case — which is what 11.4.11 asks for when the condition is ambiguous, but
  is more conservative than necessary when a four-valued condition happens to be
  unambiguous.

[tautschnig]

Suggested change

	exprt::operandst ops;
	ops.reserve(times);
	for(std::size_t i = 0; i < times; i++)
	ops.push_back(replication.op());
	expr = concatenation_exprt{ops, expr.type()};
	exprt::operandst ops{times, replication.op()};
	expr = concatenation_exprt{std::move(ops), expr.type()};