smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions

Bump version

Add -no-rw-check option to memory_dff + memory + synth_{ice40,ecp5,gowin}.

memory_dff: Add support for no_rw_check attribute.

Merge pull request #3348 from zachjs/func-tern-hint

verilog: fix width/sign detection for functions

Bump version

verilog: fix width/sign detection for functions

Merge pull request #3347 from DanielHuisman/fix-3053

Fix typo in emcc flags (typo introduced by #3053)

Fix typo in emcc flags (typo introduced by #3053)

verilog: fix size and signedness of array querying functions

genrtlil.cc and simplify.cc had inconsistent and slightly broken
handling of signedness for array querying functions. These functions are
defined to return a signed result. Simplify always produced an unsigned
and genrtlil always a signed 32-bit result ignoring the context.

Includes tests for the the relvant edge cases for context dependent
conversions.

Bump version

gatemate: Fix minor issues with `memory_libmap` (#3343)

Merge pull request #3333 from mohamed/feature/tmpdir

Observe $TMPDIR variable when creating tmp files

Cleanup, and fix windows

Observe $TMPDIR variable when creating tmp files

POSIX defines $TMPDIR as containing the pathname of the directory where
programs can create temporary files. On most systems, this variable points to
"/tmp". However, on some systems it can point to a different location.
Without respecting this variable, yosys fails to run on such systems.

Signed-off-by: Mohamed A. Bamakhrama <mohamed@alumni.tum.de>

Merge pull request #3341 from mmicko/unused_vars

Remove set but unused variable

Upload emscripten artifact

Remove set but unused variable

Add emcc build (stuck if all cpus used on GH)

Proper std::move

Use proper operator

Merge pull request #3053 from DanielHuisman/pr-2

Fix emcc warnings for WebAssembly build

Bump version

verilog: fix $past's signedness

Merge pull request #3011 from DanielHuisman/pr-1

Update WaveDrom script URLs in YosysJS demo

Merge pull request #3335 from programmerjake/divfloor-in-write_smt2

add $divfloor support to write_smt2

Merge pull request #3138 from DanielG/fix-git-rev

Make GIT_REV logic work in release tarballs

Make GIT_REV logic work in release tarballs

Currently GIT_REV doesn't get set properly when building a release
tarball. To fix this we arrange for .gitcommit to contain the (short)
commit hash in tarballs generated with git-archive(1) using export-subst in
gitattributes. This way the correct commit hash is (reproducibly) included
in the release tarballs while not burdening the maintainers with updating
it in the git repo.

Please note this even works on Github and similar forges as they use
git-archive for generating tarballs so this works out quite nicely.

verilog: fix signedness when removing unreachable cases

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

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.

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