Merge pull request #2018 from boqwxp/qbfsat-timeout

smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.

smtbmc: Remove superfluous `yosys-smt2-timeout` file macro.

Co-Authored-By: clairexen <claire@symbioticeda.com>

Merge pull request #2029 from whitequark/fix-simplify-memory-sv_logic

ast/simplify: don't bitblast async ROMs declared as `logic`

Merge pull request #1885 from Xiretza/mod-rem-cells

Fix modulo/remainder semantics

Merge pull request #2092 from whitequark/rtlil-no-space-control

Restrict RTLIL::IdString to not contain whitespace or control chars

Merge pull request #2017 from boqwxp/qbfsat-cvc4

qbfsat: Add support for CVC4.

Merge pull request #2016 from boqwxp/qbfsat-yices

qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.

Merge pull request #2097 from whitequark/ilang_lexer-fix-erange

ilang_lexer: fix check for out of range literal

ilang_lexer: fix check for out of range literal.

Commit ca70a104 did not use a correct check.

Merge pull request #2033 from boqwxp/cleanup-verilog-lexer

verilog: Move lexer location variables from global namespace to `VERILOG_FRONTEND` namespace.

Restrict RTLIL::IdString to not contain whitespace or control chars.

This is an existing invariant (most backends can't cope with these)
but one that was not checked or documented.

Document division and modulo cells

Update CHANGELOG

Add comments for mod/div semantics to rtlil.h

Expand tests/simple/constmuldivmod.v

Add flooring division operator

The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $divfloor cell provides this flooring division.

This commit also fixes the handling of $div in opt_expr, which was
previously optimized as if it was $divfloor.

Add flooring modulo operator

The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $modfloor cell provides this flooring modulo (also known as "remainder"
in several languages, but this name is ambiguous).

This commit also fixes the handling of $mod in opt_expr, which was
previously optimized as if it was $modfloor.

Merge pull request #2095 from rswarbrick/hier-typo

Fix small typos in documentation for hierarchy command

Fix small typos in documentation for hierarchy command

Merge pull request #2091 from boqwxp/printattrs

Add `printattrs` command to print attributes of currently selected objects.

Merge pull request #2051 from Xiretza/makefile-cd-warning

Suppress warning during initial clone of ABC repo

Merge pull request #2031 from epfl-vlsc/master

Add extmodule support to firrtl backend

Merge pull request #2063 from boqwxp/techmapped-firrtl

firrtl: Accept techmapped cell types in FIRRTL backend.

Merge pull request #2088 from rswarbrick/count-at

Minor optimisation in Module::wire() and Module::cell()

Merge pull request #2087 from rswarbrick/lex-warn

Silence spurious warning in Verilog lexer when compiling with GCC

Merge pull request #2086 from rswarbrick/sigbit

Use default copy constructor for RTLIL::SigBit

Merge pull request #2084 from rswarbrick/c_str

Use c_str(), not str() for IdString/std::string == and != operators

printattrs: Simplify `get_indent_str()`.

Co-Authored-By: Xiretza <xiretza@xiretza.xyz>

printattrs: Refactor indentation string building for clarity.

Co-Authored-By: whitequark <whitequark@whitequark.org>

printattrs: Add test.

printattrs: Use `flags` to pretty-print the `RTLIL::Const` appropriately.

Co-Authored-By: whitequark <whitequark@whitequark.org>

misc: Add `printattrs` command.

Merge pull request #2090 from whitequark/cxxrtl-fixes

Minor fixes for CXXRTL

cxxrtl: make logging a little bit nicer.

cxxrtl: add missing parts of commit 281c9685.

Silence spurious warning in Verilog lexer when compiling with GCC

The chosen value shouldn't have any effect. I considered something
clearly wrong like -1, but there's no checking inside the generated
lexer, and I suspect this will cause even weirder bugs if triggered
than just setting it to INITIAL.

Minor optimisation in Module::wire() and Module::cell()

The existing code does a search to figure out whether id is in the
dict (with the call to count()), and then looks it up again to get the
result (with the call to at()). This version calls find() instead,
avoiding the double lookup.

Code size increases slightly (6kb). I think this is because the
contents of find() are getting inlined, and then inlined into lots of
the callsites for cell() and wire().

Looking at the compiled code before this patch, you just get
a (non-inlined) call to count() followed by a call to at(). After the
patch, the contents of find() have been inlined (so you see do_hash,
then do_lookup). The result for each function is about 30 bytes / 40%
bigger, which presumably also enlarges call-sites that inline it.

Use default copy constructor for RTLIL::SigBit

There was a handwritten copy constructor, which I'm not sure was
actually legal C++ (it unconditionally read from the 'data' member of
a union, which wouldn't have been written if wire was true). It was
also a bit less efficient than the constructor you get from the
compiler by default (which is allowed to just copy the memory).

This gives a marginal (~0.25%) decrease in code size when compiled
with GCC 9.3.

Use c_str(), not str() for IdString/std::string == and != operators

These operators work by fetching the string from the global string
table and then comparing with the std::string that was passed in as
rhs.

Using str() means that we create a std::string (strlen; malloc;
memcpy), compare for equality (another memcmp if they have the same
length) and then finally free the string.

Using c_str() means that we pass the const char* straight to
std::string's equality operator. This ends up as a call to
std::string::compare (the const char* flavour), which is essentially
strcmp.

Merge pull request #2078 from YosysHQ/eddie/xilinx_sim_tidy

xilinx: tidy up cells_sim.v a little

smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.

qbfsat: Add support for CVC4.

qbfsat: Move SMT2 info statements back to the top of the file.

qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.

Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode.

tests: xilinx macc test to have initval, shorten BMC depth for runtime

xilinx: tidy up cells_sim.v a little

Merge pull request #2044 from YosysHQ/eddie/fix2037

verilog: allow attributes on behavioural statements (including null statement)

verilog: move attr from simple_behav_stmt to its children to attach

test: add attribute-before-stmt test from @nakengelhardt

verilog: do not warn for attributes on null statements

tests: add an generate-else test too

verilog: handle empty generate statement by removing gen_stmt_or_null...

... rule which causes a s/r conflict. Now we get an empty genblock,
which should be okay.

verilog: fix #2037 by permitting (and freeing) attributes on null stmt

tests: add #2037 testcase

Merge pull request #2015 from boqwxp/qbfsat-bisection

qbfsat: Add an iterative bisection optimization method and make it the default.

Merge pull request #2075 from YosysHQ/eddie/xaiger_cleanup

xaiger: do not derive cells

xaiger: add testcase

xaiger: do not derive cells

Merge pull request #2074 from YosysHQ/eddie/ecp5_cleanup

ecp5: cleanup unused +/ecp5/abc9_model.v

ecp5: cleanup unused +/ecp5/abc9_model.v

qbfsat: Remove cruft inadvertently left untouched in commit 86fc49a9d60f9ad4cdeec93663e7245a9fdf60c6.

qbfsat: Add bisection mode and make it the default.

Also adds `-nooptimize` and reorganizes `qbfsat.cc` a bit.

Merge pull request #2072 from whitequark/cxxrtl-dont-purge

cxxrtl: get rid of -O5 aka `opt_clean -purge` optimization level

cxxrtl: get rid of -O5 aka `opt_clean -purge` optimization level.

This isn't actually necessary anymore after scheduling was improved,
and `clean -purge` disrupts the mapping between wires in the input
RTLIL netlist and the output CXXRTL code.

abc9_ops: update comment

Merge pull request #2057 from YosysHQ/eddie/fix_task_attr

verilog: support attributes before (not after) task identifier (but 13 s/r conflicts)

Update frontends/verilog/verilog_parser.y

Co-authored-by: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>

Merge pull request #2059 from boqwxp/logger-vector-to-dict

log: Use `dict` instead of `std::vector<std::pair>` for `log_expect_{error, warning, log}` to better express the intent that each element is unique.

Merge pull request #2046 from PeterCrozier/trap

Extend YS_DEBUGTRAP to MacOS.

Merge pull request #2054 from boqwxp/fix-smtbmc

smtbmc: Fix return status handling.

smtbmc: Fix typo in error message.

Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>

Add force_downto and force_upto wire attributes.

Fixes #2058.

Merge pull request #1926 from YosysHQ/eddie/abc9_auto_dff

abc9: support seq synthesis when module has (* abc9_flop *) and bypass non-combinatorial (* abc9_box *)

firrtl: Accept techmapped cell types in FIRRTL backend.

Revert "Add support for non-power-of-two mem chunks in verific importer"

This reverts commit 173aa27ca5ef6e7c0a9277e8da7765adcd63bfe9.

log: Use `dict` instead of `std::vector<std::pair>` for `log_expect_{error, warning, log}` to better express the intent that each element is unique.

abc9: use (* abc9_keep *) instead of (* abc9_scc *); apply to $_DFF_?_

instead of moving them to $__ prefix

verilog: attributes before task enable (but 13 s/r conflicts)

tests: attributes before task enable

Merge pull request #2055 from YosysHQ/eddie/logger_multiple

logger: fix for multiple calls with same pattern

opt_expr: Sx to Sz; spotted by @Xiretza

Merge pull request #1994 from YosysHQ/eddie/fix_bug1758

opt_expr: improve single-bit $and/$or/$xor/$xnor cells; gate cells too

logger: clean up doc

abc9_ops: -prep_hier to create unmap module that removes Q's (* init *)

abc9: preserve $_DFF_?_.Q's (* init *); rely on clean to remove it

Fix broken test when ignoring abc9_flop with init == 1'b1

abc9_ops/xaiger: further reducing Module::derive() calls by ...

replacing _all_ (* abc9_box *) instantiations with their derived types

Cleanup; reduce Module::derive() calls

ecp5: latches_map.v if *not* -asyncprld

ecp5: synth_ecp5 to no longer need +/ecp5/abc9_{,un}map.v

ecp5: fix rebase mistake

abc9: update to =_$abc9_flops pattern which includes whiteboxes

abc9_ops: update docs

xilinx: gate specify/attributes from iverilog

abc9: only do +/abc9_map if `DFF

abc9: rework submod -- since it won't move (* keep *) cells

ecp5: TRELLIS_FF bypass path only in async mode

timinginfo: ignore $specify2 cells if EN is false

xilinx/ice40/ecp5: zinit requires selected wires, so select them all

abc9_ops: move assert