Merge branch 'divfloor-in-write_smt2' into smtlib2-expr-support

the smtlib2 support in nmigen needs $divfloor support in its tests:
https://gitlab.com/nmigen/nmigen/-/merge_requests/7

add $divfloor support to write_smt2

Fixes: #3330

Bump version

Merge pull request #3332 from YosysHQ/verific_f

Update Verific command file documentation

fix text to fit 80 columns

Update verific command file documentation

Use analysis mode if set in file

Merge pull request #3331 from YosysHQ/git_rev_fix

work around the new(ish) git safe.directory restrictions

Change way to get commit sha

abc9_ops: Don't leave unused derived modules lying around

These later become accidentally used for techmap replacements for
blackboxes that we don't actually want.

Signed-off-by: gatecat <gatecat@ds0.me>

Bump version

Merge pull request #3324 from jix/confusing-select-errors

select: Fix -assert-none and -assert-any error output and docs

actually test code that was broken

change smtbmc to correctly handle output of $smtlib2_expr

select: Fix -assert-none and -assert-any error output and docs

Both of these options consider a selection containing only empty modules
as non-empty. This wasn't mentioned in the documentation nor did the
error message when using `select -assert-none` list those empty modules,
which produced a very confusing error message complaining about a
non-empty selection followed by an empty listing of the selection.

This fixes the documentation and changes the `-assert-none` and
`-assert-any` assertion error messages to also output fully selected
modules (this includes selected empty modules).

It doesn't change the messages for `-assert-count` etc. as they don't
count modules.

Bump version

Add memory_bmux2rom pass.

Add memory_libmap tests.

gatemate: Use `memory_libmap` pass.

machxo2: Use `memory_libmap` pass.

efinix: Use `memory_libmap` pass.

anlogic: Use `memory_libmap` pass.

ice40: Use `memory_libmap` pass.

xilinx: Use `memory_libmap` pass.

gowin: Use `memory_libmap` pass.

nexus: Use `memory_libmap` pass.

ecp5: Use `memory_libmap` pass.

Add memory_libmap pass.

proc_rom: Add special handling of const-0 address bits.

add $smtlib2_expr

Bump version

Merge pull request #3310 from robinsonb5-PRs/master

Now calls Tcl_Init after creating the interp, fixes clock format.

opt_ffinv: Use ModIndex instead of ModWalker.

This avoids using out-of-data index information.

Use log_warning when Tcl_Init fails, report error with Tcl_ErrnoMsg.

Merge pull request #3314 from jix/sva_value_change_logic_wide

verific: Use new value change logic also for $stable of wide signals.

Bump version

Add opt_ffinv pass.

Bump version

Add proc_rom pass.

verific: Use new value change logic also for $stable of wide signals.

I missed this in the previous PR.

Now calls Tcl_Init after creating the interp, fixes clock format.

Bump version

Merge pull request #3305 from jix/sva_value_change_logic

verific: Improve logic generated for SVA value change expressions

Merge pull request #3297 from jix/sva_nested_clk_else

verific: Fix conditions of SVAs with explicit clocks within procedures

verific: Improve logic generated for SVA value change expressions

The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).

This patch now generates logic that at the same time

a) provides the expected behavior in a 2-valued logic setting, not
   depending on any dont-care optimizations, and

b) properly handles 'x values in yosys simulation

Next dev cycle

Release version 0.17

Update CHANGELOG

Update manual

Merge pull request #3299 from YosysHQ/mmicko/sim_memory

sim pass: support for memories

Fix running sva tests

Bump version

opt_mem: Remove constant-value bit lanes.

Bump version

include latest abc changes

include latest abc changes

Merge pull request #3300 from imhcyx/master

memory_share: fix wrong argidx in extra_args

Include abc change to fix FreeBSD build

Handle possible non-memory indexed data

memory_share: fix wrong argidx in extra_args

Bump version

abc: Use dict/pool instead of std::map/std::set

map memory location to wire value, if memory is converted to FFs

fix crash when no fst input

Start restoring memory state from VCD/FST

Add propagated clock signals into btor info file

verific: Fix conditions of SVAs with explicit clocks within procedures

For SVAs that have an explicit clock and are contained in a procedure
which conditionally executes the assertion, verific expresses this using
a mux with one input connected to constant 1 and the other output
connected to an SVA_AT. The existing code only handled the case where
the first input is connected to 1. This patch also handles the other
case.

Bump version

AIM file could have gaps in or between inputs and inits

Bump version

Merge pull request #3294 from YosysHQ/micko/verific_merge_past_ff

Ignore merging past ffs that we are not properly merging

Ignore merging past ffs that we are not properly merging

Bump version

Add missing parameters for ecp5

Merge pull request #3287 from jix/smt2-conditional-store

smt2: Make write port array stores conditional on nonzero write mask

Merge pull request #3257 from jix/tribuf-formal

tribuf: `-formal` option: convert all to logic and detect conflicts

Merge pull request #3290 from mpasternacki/bugfix/freebsd-build

Fix build on FreeBSD, which has no alloca.h

Merge pull request #3289 from YosysHQ/micko/sim_improve

Simulation improvements

Fix build on FreeBSD, which has no alloca.h

Match $anyseq input if connected to public wire

Treat $anyseq as input from FST

Ignore change on last edge

Last sample from input does not represent change

latches are always set to zero

If not multiclock, output only on clock edges

Set init state for all wires from FST and set past

Fix multiclock for btor2 witness

smt2: Make write port array stores conditional on nonzero write mask

Bump version

Merge pull request #3280 from YosysHQ/micko/fix_readaiw

Fix reading aiw from other solvers

Update abc

verific: allow memories to be inferred in loops (vhdl)

Merge pull request #3282 from nakengelhardt/verific_loop_rams

verific: allow memories to be inferred in loops

Bump version

memory_share: Fix up mismatched address widths.

opt_dff: Fix behavior on $ff with D == Q.

verific: allow memories to be inferred in loops

Fix reading aiw from other solvers

tribuf: `-formal` option: convert all to logic and detect conflicts

Bump version