Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc

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

Merge pull request #2276 from YosysHQ/mwk/satgen-cc

satgen: Move importCell out of the header.

satgen: Move importCell out of the header.

This function has no hope of ever getting inlined anyway, and it speeds
up yosys compile time by 7%.

Merge pull request #2275 from YosysHQ/mwk/sf2-clkint-fix

sf2: Emit CLKINT even if -clkbuf not passed

sf2: Emit CLKINT even if -clkbuf not passed

This restores pre #2229 behavior.

Merge pull request #2274 from YosysHQ/mwk/anlogic-ff-fix

anlogic: Fix FF mapping.

anlogic: Fix FF mapping.

Merge pull request #2229 from Ravenslofty/sf2_remove_sf2_iobs

sf2: replace sf2_iobs with {clkbuf,iopad}map

Merge pull request #2273 from whitequark/write-verilog-always-star-initial

verilog_backend: in non-SV mode, add a trigger for `always @*`

Merge pull request #2272 from whitequark/write-verilog-sv

verilog_backend: add `-sv` option, make `-o <filename>.sv` work

Merge pull request #2238 from YosysHQ/mwk/dfflegalize-anlogic

anlogic: Use dfflegalize.

Merge pull request #2226 from YosysHQ/mwk/nuke-efinix-gbuf

efinix: Nuke efinix_gbuf in favor of clkbufmap.

verilog_backend: in non-SV mode, add a trigger for `always @*`.

This commit only affects translation of RTLIL processes (for which
there is limited support).

Due to the event-driven nature of Verilog, processes like

    reg x;
    always @*
        x <= 1;

may never execute. This can be fixed in SystemVerilog code by using
`always_comb` instead of `always @*`, but in Verilog-2001 the options
are limited. This commit implements the following workaround:

    reg init = 0;
    reg x;
    always @* begin
        if (init) begin end
        x <= 1;
    end

Fixes #2271.

verilog_backend: add `-sv` option, make `-o <filename>.sv` work.

See #2271.

Merge pull request #2270 from whitequark/cxxrtl-fix-typo

cxxrtl: fix typo

Merge pull request #2269 from YosysHQ/claire/bisonwall

Use "bison -Wall -Werror" for verilog front-end

Treat all bison warnings as errors in verilog front-end

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

Use %precedence in verilog_parser.y

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

Fix bison warnings for missing %empty

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

Run bison with -Wall for verilog front-end

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

Merge pull request #2257 from antmicro/fix-conflicts

Restore #2203 and #2244 and fix parser conflicts

Add missing semicolons

Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>

opt_merge: Dedup one more use of FF cell type list.

achronix: Use dfflegalize.

cxxrtl: fix typo. NFC.

anlogic: Use dfflegalize.

intel: Use dfflegalize.

Revert "intel_alm: direct M10K instantiation"

This reverts commit 09ecb9b2cf3ab76841d30712bf70dafc6d47ef67.

Merge pull request #2263 from whitequark/cxxrtl-capi-eval-commit

cxxrtl: expose eval() and commit() via the C API

cxxrtl: expose eval() and commit() via the C API.

xilinx: Fix srl regression.

Of standard yosys cells, xilinx_srl only works on $_DFF_?_ and
$_DFFE_?P_, which get upgraded to $_SDFFE_?P?P_ by dfflegalize at the
point where xilinx_srl is called for non-abc9.  Fix this by running
ff_map.v first, resulting in FDRE cells, which are handled correctly.

proc_dlatch: Remove init values for combinatorial processes.

Fixes #2258.

dfflegalize: Gather init values from all wires.

Skipping non-selected wires is unsound in an obvious way.

Merge pull request #2256 from YosysHQ/claire/fix2241

Add AST_EDGE support to AstNode::detect_latch()

Add AST_EDGE support to AstNode::detect_latch(), fixes #2241

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

Fix S/R conflicts

This commit fixes S/R conflicts introduced by commit 6f9be93.

Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>

Fix R/R conflicts

This commit fixes R/R conflicts introduced by commit 7e83a51.
Parameter logic is already defined as part of `param_range_type` rule.

Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>

Revert "Revert PRs #2203 and #2244."

This reverts commit 9c120b89ace6c111aa4677616947d18d980b9c1a.

sf2: replace sf2_iobs with {clkbuf,iopad}map

Merge pull request #2255 from whitequark/bison-Werror-conflicts

verilog_parser: turn S/R and R/R conflicts into hard errors

Merge pull request #2254 from whitequark/cxxrtl-extern-c

cxxrtl: add missing extern "C"

sf2: Use dfflegalize.

verilog_parser: turn S/R and R/R conflicts into hard errors.

Fixes #2253.

Revert PRs #2203 and #2244.

This reverts commit 7e83a51fc96495c558a31fc3ca6c1a5ba4764f15.
This reverts commit b422f2e4d0b8d5bfa97913d6b9dee488b59fc405.
This reverts commit 7cb56f34b06de666935fbda315ce7c7bd45048b3.
This reverts commit 6f9be939bd7653b0bdcae93a1033a086a4561b68.
This reverts commit 76a34dc5f3a60c89efeaa3378ca0e2700a8aebd2.

cxxrtl: add missing extern "C".

This bug was hidden if a header was generated.

xilinx: Use dfflegalize.

dfflibmap: Refactor to use dfflegalize internally.

Fix issue #2251 (#2252)

* Fix #2251 - YosysJS ReferenceError: _memset is not defined.
Add '_memset' in emcc EXPORTED_FUNCTIONS in Makefile.

clkbufmap: improve input pad handling.

- allow inserting only the input pad cell
- do not insert the usual buffer if the input pad already acts as a
  buffer

Merge pull request #2244 from antmicro/logic

Add logic type support to parameters

clk2fflogic: Consistently treat async control signals as negative hold.

This fixes some dfflegalize equivalence checks, and breaks others — and
I strongly suspect the others are due to bad support for multiple
async inputs in `proc` (in particular, lack of proper support for
dlatchsr and sketchy circuits on dffsr control inputs).

dfflegalize: Add special support for const-D latches.

Those can be created by `opt_dff` when optimizing `$adff` with const
clock, or with D == Q.  Make dfflegalize do the opposite transform
when such dlatches would be otherwise unimplementable.

Merge pull request #2246 from YosysHQ/mwk/dfflegalize-typo

dfflegalize: typo fix

dfflegalize: typo fix

efinix: Use dfflegalize.

gowin: Use dfflegalize.

Add logic param and integer bad syntax tests

Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>

Support logic typed parameters

Signed-off-by: Lukasz Dalek <ldalek@antmicro.com>

intel_alm: direct M10K instantiation

Naming fixes.

synth_gowin: ABC9 support

This adds ABC9 support for synth_gowin; drastically improving
synthesis quality.

intel_alm: add Cyclone 10 GX tests

Merge pull request #2236 from YosysHQ/mwk/dfflegalize-ice40

ice40: Use dfflegalize.

ecp5: Use dfflegalize.

Merge pull request #2227 from Ravenslofty/ccache

Add option to use ccache when building

Merge pull request #2232 from YosysHQ/mwk/gowin-sim-init

gowin: Fix INIT values in sim library.

dfflegalize: Prefer mapping dff to sdff before adff

This ensures that, when both sync and async FFs are available and abc9
is involved, the sync FFs will be used, and will thus remain available
for sequential synthesis.

opt_expr: Fix crash on $mul optimization with more zeros removed than Y has.

Fixes #2221.

intel_alm: DSP inference

ice40: Use dfflegalize.

gowin: Fix INIT values in sim library.

gowin: replace determine_init with setundef

synth_intel_alm: Use dfflegalize.

Add option to use ccache when building

efinix: Nuke efinix_gbuf in favor of clkbufmap.

Improve MISTRAL_FF specify rules

Co-authored-by: Eddie Hung <eddie@fpgeh.com>

tests: update fsm.ys resource count

Suspect it is to do with map/set ordering in techmap; should
be fixed by #1862?

abc9: only techmap (* abc9_flop *) modules

intel_alm: compose $__MISTRAL_FF_SYNCONLY from MISTRAL_FF

abc9: techmap from user design to allow abc9_flop modules to be composed

from other primitives

intel_alm: add $__ prefix to MISTRAL_FF_SYNCONLY

intel_alm: ABC9 sequential optimisations

Add newlines to help text for dfflegalize

I think these were probably missed by accident. Spotted because GCC
spits out lots of messages like this:

passes/techmap/dfflegalize.cc:114:7: warning: zero-length gnu_printf format string [-Wformat-zero-length]
  114 |   log("");
      |       ^~

(because we tell GCC that the first argument to log() looks like a
printf control string in log.h, and a zero length such string triggers
a warning).

Merge pull request #2132 from YosysHQ/eddie/verific_initial

verific: rewrite initial assume/asserts prior to elaboration

Merge pull request #2208 from boqwxp/qbfsat-cleanup

qbfsat: Cleanup and refactoring

Merge pull request #2186 from YosysHQ/mwk/dfflegalize

Add dfflegalize pass.

Merge pull request #2211 from YosysHQ/mwk/fix-fmcombine-ff

fmcombine: use the master ff cell type list

Merge pull request #2210 from YosysHQ/mwk/fix-opt_merge

opt_merge: use the master FF type list

Merge pull request #2195 from YosysHQ/mwk/manual-gates

Add a few more gate types to the manual.

qbfsat: Remove useless comment and #ifndef guards.

qbfsat: Specify default values for some options in the help message.

qbfsat: Clean up external executable command lines and update temporary directory name.

qbfsat: Clean up and refactor data structures into `qbfsat.h`.

Merge pull request #2203 from antmicro/fix-grammar

Signed and macro grammar update

Merge pull request #2179 from splhack/static-cast

Support SystemVerilog Static Cast

Merge pull request #2138 from boqwxp/qbfsat-oflag

qbfsat: Add `-O[012]` options to control pre-solving simplification with ABC

Merge pull request #2206 from boqwxp/qbfsat-fix-name-specialization

qbfsat: Fix name-based hole specialization

dfflegalize: Add tests.

Add dfflegalize pass.

fmcombine: use the master ff cell type list