Removing some signed checks and logic where we've already guaranteed the
values to be positive. Indeed, in these cases, if a negative value got
through (per my realisation in the signed fuzz harness), it would cause
an infinite loop due to flooring division.
e.g. `$displayh(8'ha)` won't have a padding set, because it just gets
`lzero` set instead by `compute_required_decimal_places`.
It also doesn't have a width. In this case, we can just fill in a dummy
(unused) padding. Either space or zero would work, but space is a bit
more distinct given the width field follows.
Also omit writing the width if it's zero. This makes the emitted ilang
a little cleaner in places; `{8:> h0u}` is the output for this example,
now. The other possible extreme would be `{8:>00h0u}`.
For input like "{", "{1", etc., we would exit the loop due to
`i < fmt.size()` no longer being the case, and then check if
`++i == fmt.size()`. That would increment i to `fmt.size() + 1`,
and so execution continues.
The intention is to move i beyond the ':', so we do it only in that
case instead.
We need to invoke "read_verilog" manually, since the default action on
input files is to defer processing. Under such conditions, we never
simplify the AST, and initial $prints never execute.
Group the reconnections, so that instead of producing
connect $auto$wreduce.cc:455:run$24 [0] 1'0
connect $auto$wreduce.cc:455:run$23 [31] 1'0
connect $auto$wreduce.cc:455:run$23 [30] 1'0
... (40 more lines)
we produce
connect $auto$wreduce.cc:461:run$23 [31:11] 21'000000000000000000000
connect $auto$wreduce.cc:461:run$24 [31:10] 22'0000000000000000000000
.
The previous implementation for finding the end of a top-level s-expr
exhibited quadratic behavior as it would re-scan the complete input for
the current expression for every new line. For large designs with
trivial properties this could easily take seconds and dominate the
runtime over the actual solving.
This change remembers the current nesting level between lines, avoiding
the re-scanning.
If the `$ge` cell we are replacing has wide output port, the upper bits
on the port should be driven to zero. That's not what a `$not` cell with
a single-bit input does. Instead opt for a `$logic_not` cell, which does
zero-pad its output.
Fixes#3867.
Extend the aigmap.ys test with SAT-based comparison of the original
cells and their AIG implementations.
This tests both the usual cells and the single-bit Yosys gates.