add hierarchy -smtcheck

like -simcheck, but allow smtlib2_module modules.

Bump version

Adding expected error message.

Adding testcase for issue 3374

Add check for BLIF with no model name

Revert "use new verific extensions library"

This reverts commit 607e957657fc56625de5c28ea9cd43c859017d96.

Merge pull request #3387 from ekiwi/btor-pos-cell

btor: add support for $pos cell

Bump version

btor: add support for $pos cell

codeowners: adopt ABC9 and update intel_alm username

Bump version

Merge pull request #3383 from jix/write_formal_map_roms

smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction

smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction

This avoids provability regressions now that we infer more ROMs.

This fixes #3378

memory_map: Add -rom-only option.

Merge pull request #3382 from YosysHQ/micko/verific_extensions

use new verific extensions library

use new verific extensions library

memory_map: Use const drivers instead of FFs for ROMs.

Bump version

memory_libmap: Fix wrprio handling.

memory_libmap: Fix params emitted for unused ports for consistency.

Bump version

Add a check for packed memory MEMID uniqueness

Merge pull request #3196 from bfg86/bfg86/rename

Add -suffix option to rename -wire

opt_ffinv: Fix use after free.

removed deprecated features code

Updating help-text with nakengelhardts suggestion.

Bump version

Merge pull request #3368 from jix/smtbmc-unroll-noincr-traces-fix

smtbmc: noincr: keep solver running for post check-sat unrolling

Next dev cycle

Release version 0.18

Update manual

Updated CHANGELOG

Bump version

Merge pull request #3349 from nakengelhardt/select_count_scratchpad

Make 'stat' and 'select -count' save counts to scratchpad

Merge pull request #3359 from jix/fmcombine-memid

fmcombine: Add _gold/_gate suffix to memids

Use compiler-generated default constructor for RTLIL::Const::Const

No need for a manual implementation.
While at it: have the constructor that takes a string take a
const string reference instead to avoid a copy.

Avoid unnecessary copy of a potential large constant value.

The local variable is used just to iterate through the values, so
a const reference is all we need.

verific: Added "-vlog-libext" option to specify search extension for libraries

Bump version

wreduce: Introduce -mux_undef option (aligned with opt_expr).

smtbmc: noincr: keep solver running for post check-sat unrolling

Merge pull request #3357 from jix/smtbmc-cvc5

smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5

More updates on CHANGELOG

Update changelog and manual

sta: warn on unrecognised cells only once

Bump version

Merge pull request #3367 from jix/smtlib2-module-fixes

smt2: emit smtlib2_comb_expr outputs after all inputs

smt2: emit smtlib2_comb_expr outputs after all inputs

Merge pull request #3319 from programmerjake/smtlib2-expr-support

add smtlib2_comb_expr

Merge pull request #3358 from jix/smtbmc-yices-forall

smtbmc: Force nonincremental mode when yices is used with forall

opt_ffinv: Harden against simple ff/inv loop.

iopadmap: Fix z assignment removal.

Fixes #3360.

Bump version

verific: proper file location for readmem commands

Bump version

fmcombine: Add _gold/_gate suffix to memids

smtbmc: Force nonincremental mode when yices is used with forall

smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5

don't use sed -i because it won't work on macos

Fix preventing show crashing with newer graphviz

smtlib2_module: try to fix test on macos

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.

also make 'stat' save counts to scratchpad

have 'select -count' save the count to scratchpad entry 'select.count'

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