intel_alm: Add multiply signedness to cells

Quartus assumes unsigned multiplication by default, breaking signed
multiplies, so add an input signedness parameter to the MISTRAL_MUL*
cells to propagate to Quartus' <family>_mac cells.

Merge pull request #2355 from YosysHQ/verific_improvements

Add formal apps and template generators

Add formal apps and template generators

Merge pull request #2351 from pbsds/proc_nomux

Add -nomux switch to proc

Bump version

Merge pull request #2349 from nmoroze/smt2-bugfix

Ensure smt2 comments are associated with accessors

Bump version

synth_intel: Remove incomplete Arria 10 GX support.

The techmap rules for this target do not work in the first place (note
lack of >2-input LUT mappings), and if proper support is ever added,
it'd be better placed in the synth_intel_alm backend.

proc: Add -nomux switch

running proc -nomux will ommit the proc_mux pass

Ensure smt2 comments are associated with accessors

intel: move Cyclone V support to intel_alm

Merge pull request #2347 from YosysHQ/mwk/techmap-shift-fixes

techmap/shift_shiftx: Remove the "shiftx2mux" special path.

Merge pull request #2344 from YosysHQ/mwk/opt_share-fixes

opt_share: Refactor, fix some bugs.

Merge pull request #2337 from YosysHQ/mwk/clean-keep-wire

opt_clean: Fix module keep rules.

Merge pull request #2333 from YosysHQ/mwk/peepopt-shiftmul-signed

peeopt.shiftmul: Add a signedness check.

Merge pull request #2328 from YosysHQ/mwk/opt_dff-cleanup

Remove passes redundant with opt_dff

Merge pull request #2327 from YosysHQ/mwk/techmap-constmap-fix

techmap.CONSTMAP: Handle outputs before inputs.

Merge pull request #2326 from YosysHQ/mwk/peeopt-muldiv-sign

peepopt.muldiv: Add a signedness check.

Merge pull request #2319 from YosysHQ/mwk/techmap-celltype-pattern

techmap: Add support for [] wildcards in techmap_celltype.

techmap/shift_shiftx: Remove the "shiftx2mux" special path.

Our techmap rules for $shift and $shiftx cells contained a special path
that aimed to decompose the shift LSB-first instead of MSB-first in
select cases that come up in pmux lowering.  This path was needlessly
overcomplicated and contained bugs.

Instead of doing that, just switch over the main path to iterate
LSB-first (except for the specially-handled MSB for signed shifts
and overflow handling).  This also makes the code consistent with
shl/shr/sshl/sshr cells, which are already decomposed LSB-first.

Fixes #2346.

Bump version

Merge pull request #2122 from PeterCrozier/struct_array2

Support 2D bit arrays in structures. Optimise array indexing.

Bump version

Ensure \A_SIGNED is never used with $shiftx

It has no effect on the output ($shiftx doesn't perform any sign
extension whatsoever), so an attempt to use it should be caught early.

Respect \A_SIGNED for $shift

This reflects the behaviour of $shr/$shl, which sign-extend their A
operands to the size of their output, then do a logical shift (shift in
0-bits).

include both power-of-two and non-power-of-two testcases

Merge pull request #2339 from zachjs/display-format-0s

Allow %0s $display format specifier

Merge pull request #2338 from zachjs/const-branch-finish

Propagate const_fold through generate blocks and branches

Merge pull request #2317 from zachjs/expand-genblock

Fix generate scoping issues

Merge branch 'zachjs-const-func-block-var'

Merge branch 'const-func-block-var' of https://github.com/zachjs/yosys into zachjs-const-func-block-var

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

Merge pull request #2281 from zachjs/const-real

Allow reals as constant function parameters

opt_share: Refactor, fix some bugs.

Fixes #2334.
Fixes #2335.
Fixes #2336.

Bump version

intel_alm: fix typo in MISTRAL_MUL27X27 cell name

Bump version

Merge pull request #2340 from andy-knowles/cxxrtl-fix-alu-carryout

cxxrtl.h: Fix incorrect CarryOut in alu when Bits % 32 != 0 && Invert == False

cxxrtl.h: Fix incorrect CarryOut in alu()

intel_alm: add more megafunctions. NFC.

cxxrtl.h: Fix incorrect CarryOut in alu when Bits % 32 != 0 && Invert == False

Bump version

Propagate const_fold through generate blocks and branches

Allow %0s $display format specifier

opt_clean: Fix module keep rules.

- wires with keep attribute now force a module to be kept
- presence of $memwr and $meminit cells no longer forces a module to be
  kept

Remove now-redundant dff2dffe pass.

Remove now-redundant dff2dffs pass.

peepopt: Remove now-redundant dffmux pattern.

Remove now-redundant opt_rmdff pass.

Replace opt_rmdff with opt_dff.

peeopt.shiftmul: Add a signedness check.

Fixes #2332.

techmap.CONSTMAP: Handle outputs before inputs.

Fixes #2321.

peepopt.muldiv: Add a signedness check.

Fixes #2318.

techmap: Add support for [] wildcards in techmap_celltype.

Fixes #1826.

Fix generate scoping issues

- expand_genblock defers prefixing of items within named sub-blocks
- Allow partially-qualified references to local scopes
- Handle shadowing within generate blocks
- Resolve generate scope references within tasks and functions
- Apply generate scoping to genvars
- Resolves #2214, resolves #1456

Bump YOSYS_VER

Signed-off-by: Claire Wolf <claire@symbioticeda.com>

Add dffunmap pass.

To be used with backends that cannot deal with fancy FF types (like blif
or smt).

opt_expr: Remove -clkinv option, make it the default.

Adds -noclkinv option just in case the old behavior was actually useful
to someone.

synth_ice40: Use opt_dff.

The main part is converting ice40_dsp to recognize the new FF types
created in opt_dff instead of trying to recognize the mux patterns on
its own.

The fsm call has been moved upwards because the passes cannot deal with
$dffe/$sdff*, and other optimizations don't help it much anyway.

synth_xilinx: Use opt_dff.

The main part is converting xilinx_dsp to recognize the new FF types
created in opt_dff instead of trying to recognize the patterns on its
own.

The fsm call has been moved upwards because the passes cannot deal with
$dffe/$sdff*, and other optimizations don't help it much anyway.

async2sync: Support all FF types.

Add opt_dff pass.

verilog_backend: Add handling for all FF types.

Merge pull request #2314 from YosysHQ/verifix_errorfix

Verific - prevent exit yosys due to stored error

Clear last error message

opt_expr: Fix handling of $_XNOR_ cells with A = B.

Fixes #2311.

ffinit: Fortify the code a bit.

This fixes handling of messy cases involving repeatedly setting and
removing the same init bit.

Merge pull request #2301 from zachjs/for-loop-errors

Clearer for loop error messages

Merge pull request #2306 from YosysHQ/mwk/equiv_induct-undef

equiv_induct: Fix up assumption for $equiv cells in -undef mode.

equiv_induct: Fix up assumption for $equiv cells in -undef mode.

Before this fix, equiv_induct only assumed that one of the following is
true:

- defined value of A is equal to defined value of B
- A is undefined

This lets through valuations where A is defined, B is undefined, and
the defined (meaningless) value of B happens to match the defined value
of A.  Instead, tighten this up to OR of the following:

- defined value of A is equal to defined value of B, and B is not
  undefined
- A is undefined

intel_alm: direct M10K instantiation

This reverts commit a3a90f6377f251d3b6c5898eb1543f8832493bb8.

intel_alm: increase abc9 -W

Merge pull request #2299 from zachjs/arg-loop

Avoid generating wires for function args which are constant

Clearer for loop error messages

Allow blocks with declarations within constant functions

Avoid generating wires for function args which are constant

async2sync: Refactor to use FfInitVals.

memory_dff: Refactor to use FfInitVals.

proc_dlatch: Refactor to use FfInitVals.

pmux2shift: Refactor to use FfInitVals.

wreduce: Refactor to use FfInitVals.

techmap: Refactor to use FfInitVals.

shregmap: Refactor to use FfInitVals.

abc: Refactor to use FfInitVals.

dffinit: Refactor to use FfInitVals.

zinit: Refactor to use FfInitVals.

dfflegalize: Refactor to use FfInitVals.

clk2fflogic: Support all FF types.

satgen: Add support for dffe, sdff, sdffe, sdffce cells.

Add utility module for representing flip-flops.

memory_dff: recognize more dff cells

Add utility module for dealing with init attributes.

Merge pull request #2285 from YosysHQ/mwk/techmap-cellname

techmap: Add _TECHMAP_CELLNAME_ special parameter.

Merge pull request #2294 from Ravenslofty/intel_alm_timings

intel_alm: add additional ABC9 timings

intel_alm: add additional ABC9 timings

Remove EXPLICIT_CARRY logic.

The symbiflow-arch-defs tool chain no longer needs the EXPLICIT_CARRY
within yosys itself.

Signed-off-by: Keith Rothman <537074+litghost@users.noreply.github.com>

techmap: Add _TECHMAP_CELLNAME_ special parameter.

This parameter will resolve to the name of the cell being mapped.  The
first user of this parameter will be synth_intel_alm's Quartus output,
which requires a unique (and preferably descriptive) name passed as
a cell parameter for the memory cells.

Merge pull request #2215 from boqwxp/qbfsat-solver-options

qbfsat, smt2, smtio: Add `-solver-option` to allow specifying SMT-LIBv2 `(set-option ...)` commands

smtio: Emit `mode: start` options before `set-logic` command and any other options after it.

Refer to the SMT-LIB specification, section 4.1.7.  According to the spec, some options can only be specified in `start` mode.  Once the solver sees `set-logic`, it moves to `assert` mode.

smtio: Add support for parsing `yosys-smt2-solver-option` info statements.

qbfsat: Add `-solver-option` option.