Jannis Harder 0f96ae5990 Add smtmap.v describing the smt2 backend's behavior for undef bits ...

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.

2022-10-20 15:48:18 +02:00

1.5 KiB

Raw Blame History

View Raw