The default mapping rules for division-like operations (div/divfloor/
mod/modfloor) invoke subtractions which can get mapped to carry chains
in FPGA flows. Optimizations across carry chains are weak, so in
practice this ends up too costly compared to implementing the division
purely in soft logic.
For this reason arrange for `techmap.v` ignoring division operations
under `-D NODIV`, and use this mode in `synth_quicklogic` to avoid carry
chains for divisions.
The new bitwise case equality (`$bweqx`) and bitwise mux (`$bwmux`)
cells enable compact encoding and decoding of 3-valued logic signals
using multiple 2-valued signals.
iverilog complains about implicitly truncating LUT when connecting it to
the `$bmux` A input. This explicitly truncates it to avoid that warning
without changing the behaviour otherwise.
* Change simlib's $mux cell to use the ternary operator as $_MUX_
already does
* Stop opt_expr -keepdc from changing S=x to S=0
* Change const eval of $mux and $pmux to match the updated simlib
(fixes sim)
* The sat behavior of $mux already matches the updated simlib
The verilog frontend uses $mux for the ternary operators and this
changes all interpreations of the $mux cell (that I found) to match the
verilog simulation behavior for the ternary operator. For 'if' and
'case' expressions the frontend may also use $mux but uses $eqx if the
verilog simulation behavior is requested with the '-ifx' option.
For $pmux there is a remaining mismatch between the sat behavior and the
simlib behavior. Resolving this requires more discussion, as the $pmux
cell does not directly correspond to a specific verilog construct.
Some builtin cells have an undefined (x) output even when all inputs are
defined. This is not natively supported by the formal backends which
will produce a fully defined value instead. This can lead to issues when
combining different backends in a formal flow. To work around these,
this adds a file containing verilog implementation of cells matching the
fully defined behavior implemented by the smt2 backend.
These can be used to protect undefined flip-flop initialization values
from optimizations that are not sound for formal verification and can
help mapping all solver-provided values in witness traces for flows that
use different backends simultaneously.
* xilinx: add SCC test for DSP48E1
* xilinx: Gate DSP48E1 being a whitebox behind ALLOW_WHITEBOX_DSP48E1
Have a test that checks it works through ABC9 when enabled
* abc9 to break SCCs using $__ABC9_SCC_BREAKER module
* Add test
* abc9_ops: remove refs to (* abc9_keep *) on wires
* abc9_ops: do not bypass cells in an SCC
* Add myself to CODEOWNERS for abc9*
* Fix compile
* abc9_ops: run -prep_hier before scc
* Fix tests
* Remove bug reference pending fix
* abc9: fix for -prep_hier -dff
* xaiger: restore PI handling
* abc9_ops: -prep_xaiger sigmap
* abc9_ops: -mark_scc -> -break_scc
* abc9: eliminate hard-coded abc9.box from tests
Also tidy up
* Address review
Martin Povišer
Claire Xenia Wolf
NachtSpyder04
Saish Karole
Emil J. Tywoniak
Miodrag Milanović
Jannis Harder
Catherine
andyfox-rushc
Charlotte
Marcelina Kościelnicka
Eddie Hung