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

Merge pull request #3275 from YosysHQ/micko/clk2fflogic_fix

Use wrap_async_control_gate if ff is fine

Use wrap_async_control_gate if ff is fine

Merge pull request #3273 from modwizcode/fix-build

Do not enable features that require the support of compression compiled in

pass jny: flipped the defaults for the inclusion of various bits of metadata

pass jny: ensured the cell collection is cleared between modules

pass jny: fixed missing quotes around the type value for the cell sort

pass jny: fixed the backslash escape for strings

pass jny: removed the invalid json escapes

pass jny: added some todo comments about things that need to be done before a proper merge, but it should be enough for the PoC at the moment

pass jny: changed the constructor initializers to use parens rather than curly-braces to hopefully make GCC 4.8 happy

pass jny: fixed the string escape method to be less jank and more proper

pass jny: fixed the signed output for param value output

pass jny: added connection output

pass jny: added filter options for including connections, attributes, and properties

pass jny: large chunk of refactoring to make the JSON output more pretty and the internals less of a spaghetti nightmare

metadata -> jny: migrated to the proper name for the pass

pass metadata: added the machinery to write param and attributes

pass metadata: removed superfluous `stringf` calls

pass metadata: some more rough work on dumping the parameters and attributes

pass metadata: fixed the MetadataWriter object initializer so GCC 4.8 is happy

pass metadata: added the output of parameters,

it's kinda dumb at the moment and needs parsing based on type but it's a start

pass metadata: fixed some of the output formatting

pass metadata: initial commit of the metadata pass for exporting design metadata for yosys assisted tooling

Makefile: properly conditionalize features requiring compression.

Bump version

Merge pull request #3269 from YosysHQ/micko/fix_autotop

Reorder steps in -auto-top to fix synth command, fixes #3261

abc: Add support for FFs with reset in -dff

Bump version

sv: fix always_comb auto nosync for nested and function blocks

Reorder steps in -auto-top to fix synth command, fixes #3261

Next dev cycle

Release version 0.16

Bump version

show: Fix width labels.

See #3266.

Update CHANGELOG and manual

Merge pull request #3265 from YosysHQ/micko/sim_improvements

Improve sim by setting proper past D and AD signals

past_ad initial value setting

setInitState can be only one altering values

Set past_d value for init state

Merge pull request #3264 from jix/invalid_ff_dcinit_merge

opt_merge: Add `-keepdc` option required for formal verification

Bump version

opt_merge: Add `-keepdc` option required for formal verification

The `-keepdc` option prevents merging flipflops with dont-care bits in
their initial value, as, in general, this is not a valid transform for
formal verification.

The keepdc option of `opt` is passed along to `opt_merge` now.