yosys.git
4 years agosmtio: Add support for parsing `yosys-smt2-solver-option` info statements.
Alberto Gonzalez [Wed, 1 Jul 2020 20:04:56 +0000 (20:04 +0000)]
smtio: Add support for parsing `yosys-smt2-solver-option` info statements.

4 years agoqbfsat: Add `-solver-option` option.
Alberto Gonzalez [Mon, 29 Jun 2020 04:41:18 +0000 (04:41 +0000)]
qbfsat: Add `-solver-option` option.

4 years agosmt2: Add `-solver-option` option.
Alberto Gonzalez [Wed, 1 Jul 2020 20:51:14 +0000 (20:51 +0000)]
smt2: Add `-solver-option` option.

4 years agoMerge pull request #2282 from YosysHQ/claire/satunsat
clairexen [Mon, 20 Jul 2020 21:06:36 +0000 (23:06 +0200)]
Merge pull request #2282 from YosysHQ/claire/satunsat

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

4 years agocelltypes: Fix EN port name for some FF types.
Marcelina Kościelnicka [Mon, 20 Jul 2020 19:43:05 +0000 (21:43 +0200)]
celltypes: Fix EN port name for some FF types.

4 years agoOnly allow "sat" and "unsat" smt solver responses in yosys-smtbmc
Claire Wolf [Mon, 20 Jul 2020 17:35:32 +0000 (19:35 +0200)]
Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoMerge pull request #2276 from YosysHQ/mwk/satgen-cc
clairexen [Mon, 20 Jul 2020 13:23:14 +0000 (15:23 +0200)]
Merge pull request #2276 from YosysHQ/mwk/satgen-cc

satgen: Move importCell out of the header.

4 years agosatgen: Move importCell out of the header.
Marcelina Kościelnicka [Sat, 18 Jul 2020 22:17:02 +0000 (00:17 +0200)]
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%.

4 years agoMerge pull request #2275 from YosysHQ/mwk/sf2-clkint-fix
Miodrag Milanović [Fri, 17 Jul 2020 13:05:46 +0000 (15:05 +0200)]
Merge pull request #2275 from YosysHQ/mwk/sf2-clkint-fix

sf2: Emit CLKINT even if -clkbuf not passed

4 years agosf2: Emit CLKINT even if -clkbuf not passed
Marcelina Kościelnicka [Fri, 17 Jul 2020 13:01:45 +0000 (15:01 +0200)]
sf2: Emit CLKINT even if -clkbuf not passed

This restores pre #2229 behavior.

4 years agoMerge pull request #2274 from YosysHQ/mwk/anlogic-ff-fix
Miodrag Milanović [Fri, 17 Jul 2020 12:39:31 +0000 (14:39 +0200)]
Merge pull request #2274 from YosysHQ/mwk/anlogic-ff-fix

anlogic: Fix FF mapping.

4 years agoanlogic: Fix FF mapping.
Marcelina Kościelnicka [Fri, 17 Jul 2020 12:03:21 +0000 (14:03 +0200)]
anlogic: Fix FF mapping.

4 years agoMerge pull request #2229 from Ravenslofty/sf2_remove_sf2_iobs
clairexen [Thu, 16 Jul 2020 16:33:56 +0000 (18:33 +0200)]
Merge pull request #2229 from Ravenslofty/sf2_remove_sf2_iobs

sf2: replace sf2_iobs with {clkbuf,iopad}map

4 years agoMerge pull request #2273 from whitequark/write-verilog-always-star-initial
clairexen [Thu, 16 Jul 2020 16:30:50 +0000 (18:30 +0200)]
Merge pull request #2273 from whitequark/write-verilog-always-star-initial

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

4 years agoMerge pull request #2272 from whitequark/write-verilog-sv
clairexen [Thu, 16 Jul 2020 16:28:24 +0000 (18:28 +0200)]
Merge pull request #2272 from whitequark/write-verilog-sv

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

4 years agoMerge pull request #2238 from YosysHQ/mwk/dfflegalize-anlogic
Miodrag Milanović [Thu, 16 Jul 2020 16:07:58 +0000 (18:07 +0200)]
Merge pull request #2238 from YosysHQ/mwk/dfflegalize-anlogic

anlogic: Use dfflegalize.

4 years agoMerge pull request #2226 from YosysHQ/mwk/nuke-efinix-gbuf
Miodrag Milanović [Thu, 16 Jul 2020 16:07:41 +0000 (18:07 +0200)]
Merge pull request #2226 from YosysHQ/mwk/nuke-efinix-gbuf

efinix: Nuke efinix_gbuf in favor of clkbufmap.

4 years agoverilog_backend: in non-SV mode, add a trigger for `always @*`.
whitequark [Thu, 16 Jul 2020 11:26:31 +0000 (11:26 +0000)]
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.

4 years agoverilog_backend: add `-sv` option, make `-o <filename>.sv` work.
whitequark [Thu, 16 Jul 2020 10:34:21 +0000 (10:34 +0000)]
verilog_backend: add `-sv` option, make `-o <filename>.sv` work.

See #2271.

4 years agoMerge pull request #2270 from whitequark/cxxrtl-fix-typo
whitequark [Thu, 16 Jul 2020 09:48:10 +0000 (09:48 +0000)]
Merge pull request #2270 from whitequark/cxxrtl-fix-typo

cxxrtl: fix typo

4 years agoMerge pull request #2269 from YosysHQ/claire/bisonwall
whitequark [Wed, 15 Jul 2020 19:20:33 +0000 (19:20 +0000)]
Merge pull request #2269 from YosysHQ/claire/bisonwall

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

4 years agoTreat all bison warnings as errors in verilog front-end
Claire Wolf [Wed, 15 Jul 2020 09:57:31 +0000 (11:57 +0200)]
Treat all bison warnings as errors in verilog front-end

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoUse %precedence in verilog_parser.y
Claire Wolf [Wed, 15 Jul 2020 09:54:28 +0000 (11:54 +0200)]
Use %precedence in verilog_parser.y

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoFix bison warnings for missing %empty
Claire Wolf [Tue, 14 Jul 2020 22:04:23 +0000 (00:04 +0200)]
Fix bison warnings for missing %empty

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoRun bison with -Wall for verilog front-end
Claire Wolf [Tue, 14 Jul 2020 22:04:04 +0000 (00:04 +0200)]
Run bison with -Wall for verilog front-end

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoMerge pull request #2257 from antmicro/fix-conflicts
clairexen [Wed, 15 Jul 2020 09:49:09 +0000 (11:49 +0200)]
Merge pull request #2257 from antmicro/fix-conflicts

Restore #2203 and #2244 and fix parser conflicts

4 years agoAdd missing semicolons
Kamil Rakoczy [Wed, 15 Jul 2020 08:15:13 +0000 (10:15 +0200)]
Add missing semicolons

Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>
4 years agoopt_merge: Dedup one more use of FF cell type list.
Marcelina Kościelnicka [Wed, 15 Jul 2020 00:30:25 +0000 (02:30 +0200)]
opt_merge: Dedup one more use of FF cell type list.

4 years agoachronix: Use dfflegalize.
Marcelina Kościelnicka [Thu, 2 Jul 2020 22:22:28 +0000 (00:22 +0200)]
achronix: Use dfflegalize.

4 years agocxxrtl: fix typo. NFC.
whitequark [Tue, 14 Jul 2020 16:10:30 +0000 (16:10 +0000)]
cxxrtl: fix typo. NFC.

4 years agoanlogic: Use dfflegalize.
Marcelina Kościelnicka [Thu, 2 Jul 2020 22:22:44 +0000 (00:22 +0200)]
anlogic: Use dfflegalize.

4 years agointel: Use dfflegalize.
Marcelina Kościelnicka [Sun, 5 Jul 2020 02:02:42 +0000 (04:02 +0200)]
intel: Use dfflegalize.

4 years agoRevert "intel_alm: direct M10K instantiation"
Lofty [Mon, 13 Jul 2020 13:08:52 +0000 (14:08 +0100)]
Revert "intel_alm: direct M10K instantiation"

This reverts commit 09ecb9b2cf3ab76841d30712bf70dafc6d47ef67.

4 years agoMerge pull request #2263 from whitequark/cxxrtl-capi-eval-commit
whitequark [Mon, 13 Jul 2020 02:44:36 +0000 (02:44 +0000)]
Merge pull request #2263 from whitequark/cxxrtl-capi-eval-commit

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

4 years agocxxrtl: expose eval() and commit() via the C API.
whitequark [Sun, 12 Jul 2020 23:34:18 +0000 (23:34 +0000)]
cxxrtl: expose eval() and commit() via the C API.

4 years agoxilinx: Fix srl regression.
Marcelina Kościelnicka [Sun, 12 Jul 2020 15:54:07 +0000 (17:54 +0200)]
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.

4 years agoproc_dlatch: Remove init values for combinatorial processes.
Marcelina Kościelnicka [Sun, 12 Jul 2020 13:38:51 +0000 (15:38 +0200)]
proc_dlatch: Remove init values for combinatorial processes.

Fixes #2258.

4 years agodfflegalize: Gather init values from all wires.
Marcelina Kościelnicka [Sun, 12 Jul 2020 13:39:40 +0000 (15:39 +0200)]
dfflegalize: Gather init values from all wires.

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

4 years agoMerge pull request #2256 from YosysHQ/claire/fix2241
clairexen [Fri, 10 Jul 2020 17:07:50 +0000 (19:07 +0200)]
Merge pull request #2256 from YosysHQ/claire/fix2241

Add AST_EDGE support to AstNode::detect_latch()

4 years agoAdd AST_EDGE support to AstNode::detect_latch(), fixes #2241
Claire Wolf [Fri, 10 Jul 2020 16:41:13 +0000 (18:41 +0200)]
Add AST_EDGE support to AstNode::detect_latch(), fixes #2241

Signed-off-by: Claire Wolf <claire@symbioticeda.com>
4 years agoFix S/R conflicts
Kamil Rakoczy [Fri, 10 Jul 2020 12:56:14 +0000 (14:56 +0200)]
Fix S/R conflicts

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

Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>
4 years agoFix R/R conflicts
Kamil Rakoczy [Fri, 10 Jul 2020 08:14:31 +0000 (10:14 +0200)]
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>
4 years agoRevert "Revert PRs #2203 and #2244."
Kamil Rakoczy [Fri, 10 Jul 2020 07:59:48 +0000 (09:59 +0200)]
Revert "Revert PRs #2203 and #2244."

This reverts commit 9c120b89ace6c111aa4677616947d18d980b9c1a.

4 years agosf2: replace sf2_iobs with {clkbuf,iopad}map
Dan Ravensloft [Sat, 4 Jul 2020 20:20:26 +0000 (21:20 +0100)]
sf2: replace sf2_iobs with {clkbuf,iopad}map

4 years agoMerge pull request #2255 from whitequark/bison-Werror-conflicts
whitequark [Thu, 9 Jul 2020 20:17:19 +0000 (20:17 +0000)]
Merge pull request #2255 from whitequark/bison-Werror-conflicts

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

4 years agoMerge pull request #2254 from whitequark/cxxrtl-extern-c
whitequark [Thu, 9 Jul 2020 20:17:12 +0000 (20:17 +0000)]
Merge pull request #2254 from whitequark/cxxrtl-extern-c

cxxrtl: add missing extern "C"

4 years agosf2: Use dfflegalize.
Marcelina Kościelnicka [Thu, 2 Jul 2020 16:22:29 +0000 (18:22 +0200)]
sf2: Use dfflegalize.

4 years agoverilog_parser: turn S/R and R/R conflicts into hard errors.
whitequark [Thu, 9 Jul 2020 19:36:39 +0000 (19:36 +0000)]
verilog_parser: turn S/R and R/R conflicts into hard errors.

Fixes #2253.

4 years agoRevert PRs #2203 and #2244.
whitequark [Thu, 9 Jul 2020 18:13:04 +0000 (18:13 +0000)]
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.

4 years agocxxrtl: add missing extern "C".
whitequark [Thu, 9 Jul 2020 17:52:52 +0000 (17:52 +0000)]
cxxrtl: add missing extern "C".

This bug was hidden if a header was generated.

4 years agoxilinx: Use dfflegalize.
Marcelina Kościelnicka [Tue, 23 Jun 2020 16:51:51 +0000 (18:51 +0200)]
xilinx: Use dfflegalize.

4 years agodfflibmap: Refactor to use dfflegalize internally.
Marcelina Kościelnicka [Thu, 2 Jul 2020 16:22:43 +0000 (18:22 +0200)]
dfflibmap: Refactor to use dfflegalize internally.

4 years agoFix issue #2251 (#2252)
Lucas Castro [Thu, 9 Jul 2020 16:50:26 +0000 (13:50 -0300)]
Fix issue #2251 (#2252)

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

4 years agoclkbufmap: improve input pad handling.
Marcelina Kościelnicka [Sat, 4 Jul 2020 21:09:00 +0000 (23:09 +0200)]
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

4 years agoMerge pull request #2244 from antmicro/logic
clairexen [Thu, 9 Jul 2020 16:39:30 +0000 (18:39 +0200)]
Merge pull request #2244 from antmicro/logic

Add logic type support to parameters

4 years agoclk2fflogic: Consistently treat async control signals as negative hold.
Marcelina Kościelnicka [Tue, 7 Jul 2020 12:22:04 +0000 (14:22 +0200)]
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).

4 years agodfflegalize: Add special support for const-D latches.
Marcelina Kościelnicka [Mon, 6 Jul 2020 20:52:05 +0000 (22:52 +0200)]
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.

4 years agoMerge pull request #2246 from YosysHQ/mwk/dfflegalize-typo
whitequark [Tue, 7 Jul 2020 22:46:37 +0000 (22:46 +0000)]
Merge pull request #2246 from YosysHQ/mwk/dfflegalize-typo

dfflegalize: typo fix

4 years agodfflegalize: typo fix
Marcelina Kościelnicka [Tue, 7 Jul 2020 13:00:52 +0000 (15:00 +0200)]
dfflegalize: typo fix

4 years agoefinix: Use dfflegalize.
Marcelina Kościelnicka [Thu, 2 Jul 2020 22:23:32 +0000 (00:23 +0200)]
efinix: Use dfflegalize.

4 years agogowin: Use dfflegalize.
Marcelina Kościelnicka [Thu, 2 Jul 2020 22:23:18 +0000 (00:23 +0200)]
gowin: Use dfflegalize.

4 years agoAdd logic param and integer bad syntax tests
Kamil Rakoczy [Mon, 6 Jul 2020 07:05:34 +0000 (09:05 +0200)]
Add logic param and integer bad syntax tests

Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>
4 years agoSupport logic typed parameters
Lukasz Dalek [Mon, 18 May 2020 19:02:19 +0000 (21:02 +0200)]
Support logic typed parameters

Signed-off-by: Lukasz Dalek <ldalek@antmicro.com>
4 years agointel_alm: direct M10K instantiation
Dan Ravensloft [Thu, 11 Jun 2020 21:25:04 +0000 (22:25 +0100)]
intel_alm: direct M10K instantiation

4 years agoNaming fixes.
Marcelina Kościelnicka [Sun, 5 Jul 2020 20:21:59 +0000 (22:21 +0200)]
Naming fixes.

4 years agosynth_gowin: ABC9 support
Dan Ravensloft [Wed, 1 Apr 2020 00:07:30 +0000 (01:07 +0100)]
synth_gowin: ABC9 support

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

4 years agointel_alm: add Cyclone 10 GX tests
Dan Ravensloft [Sun, 5 Jul 2020 17:53:14 +0000 (18:53 +0100)]
intel_alm: add Cyclone 10 GX tests

4 years agoMerge pull request #2236 from YosysHQ/mwk/dfflegalize-ice40
Marcelina Kościelnicka [Sun, 5 Jul 2020 16:50:25 +0000 (18:50 +0200)]
Merge pull request #2236 from YosysHQ/mwk/dfflegalize-ice40

ice40: Use dfflegalize.

4 years agoecp5: Use dfflegalize.
Marcelina Kościelnicka [Thu, 2 Jul 2020 22:23:03 +0000 (00:23 +0200)]
ecp5: Use dfflegalize.

4 years agoMerge pull request #2227 from Ravenslofty/ccache
whitequark [Sun, 5 Jul 2020 15:53:41 +0000 (15:53 +0000)]
Merge pull request #2227 from Ravenslofty/ccache

Add option to use ccache when building

4 years agoMerge pull request #2232 from YosysHQ/mwk/gowin-sim-init
Marcelina Kościelnicka [Sun, 5 Jul 2020 10:02:31 +0000 (12:02 +0200)]
Merge pull request #2232 from YosysHQ/mwk/gowin-sim-init

gowin: Fix INIT values in sim library.

4 years agodfflegalize: Prefer mapping dff to sdff before adff
Marcelina Kościelnicka [Sun, 5 Jul 2020 02:57:24 +0000 (04:57 +0200)]
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.

4 years agoopt_expr: Fix crash on $mul optimization with more zeros removed than Y has.
Marcelina Kościelnicka [Sat, 4 Jul 2020 22:55:38 +0000 (00:55 +0200)]
opt_expr: Fix crash on $mul optimization with more zeros removed than Y has.

Fixes #2221.

4 years agointel_alm: DSP inference
Dan Ravensloft [Sat, 25 Apr 2020 16:25:59 +0000 (17:25 +0100)]
intel_alm: DSP inference

4 years agoice40: Use dfflegalize.
Marcelina Kościelnicka [Thu, 2 Jul 2020 22:21:24 +0000 (00:21 +0200)]
ice40: Use dfflegalize.

4 years agogowin: Fix INIT values in sim library.
Marcelina Kościelnicka [Sun, 5 Jul 2020 01:03:48 +0000 (03:03 +0200)]
gowin: Fix INIT values in sim library.

4 years agogowin: replace determine_init with setundef
Dan Ravensloft [Sat, 4 Jul 2020 18:39:40 +0000 (19:39 +0100)]
gowin: replace determine_init with setundef

4 years agosynth_intel_alm: Use dfflegalize.
Marcelina Kościelnicka [Wed, 1 Jul 2020 01:31:34 +0000 (03:31 +0200)]
synth_intel_alm: Use dfflegalize.

4 years agoAdd option to use ccache when building
Dan Ravensloft [Sat, 4 Jul 2020 18:59:39 +0000 (19:59 +0100)]
Add option to use ccache when building

4 years agoefinix: Nuke efinix_gbuf in favor of clkbufmap.
Marcelina Kościelnicka [Sat, 4 Jul 2020 18:49:28 +0000 (20:49 +0200)]
efinix: Nuke efinix_gbuf in favor of clkbufmap.

4 years agoImprove MISTRAL_FF specify rules
Dan Ravensloft [Thu, 28 May 2020 10:33:19 +0000 (11:33 +0100)]
Improve MISTRAL_FF specify rules

Co-authored-by: Eddie Hung <eddie@fpgeh.com>
4 years agotests: update fsm.ys resource count
Eddie Hung [Wed, 27 May 2020 19:49:16 +0000 (12:49 -0700)]
tests: update fsm.ys resource count

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

4 years agoabc9: only techmap (* abc9_flop *) modules
Eddie Hung [Wed, 27 May 2020 16:37:57 +0000 (09:37 -0700)]
abc9: only techmap (* abc9_flop *) modules

4 years agointel_alm: compose $__MISTRAL_FF_SYNCONLY from MISTRAL_FF
Eddie Hung [Tue, 26 May 2020 15:38:11 +0000 (08:38 -0700)]
intel_alm: compose $__MISTRAL_FF_SYNCONLY from MISTRAL_FF

4 years agoabc9: techmap from user design to allow abc9_flop modules to be composed
Eddie Hung [Tue, 26 May 2020 15:37:26 +0000 (08:37 -0700)]
abc9: techmap from user design to allow abc9_flop modules to be composed

from other primitives

4 years agointel_alm: add $__ prefix to MISTRAL_FF_SYNCONLY
Eddie Hung [Mon, 25 May 2020 22:15:20 +0000 (15:15 -0700)]
intel_alm: add $__ prefix to MISTRAL_FF_SYNCONLY

4 years agointel_alm: ABC9 sequential optimisations
Dan Ravensloft [Sat, 23 May 2020 11:52:13 +0000 (12:52 +0100)]
intel_alm: ABC9 sequential optimisations

4 years agoAdd newlines to help text for dfflegalize
Rupert Swarbrick [Fri, 3 Jul 2020 10:12:03 +0000 (11:12 +0100)]
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).

4 years agoMerge pull request #2132 from YosysHQ/eddie/verific_initial
clairexen [Thu, 2 Jul 2020 15:50:22 +0000 (17:50 +0200)]
Merge pull request #2132 from YosysHQ/eddie/verific_initial

verific: rewrite initial assume/asserts prior to elaboration

4 years agoMerge pull request #2208 from boqwxp/qbfsat-cleanup
clairexen [Thu, 2 Jul 2020 15:48:37 +0000 (17:48 +0200)]
Merge pull request #2208 from boqwxp/qbfsat-cleanup

qbfsat: Cleanup and refactoring

4 years agoMerge pull request #2186 from YosysHQ/mwk/dfflegalize
clairexen [Thu, 2 Jul 2020 15:46:11 +0000 (17:46 +0200)]
Merge pull request #2186 from YosysHQ/mwk/dfflegalize

Add dfflegalize pass.

4 years agoMerge pull request #2211 from YosysHQ/mwk/fix-fmcombine-ff
clairexen [Thu, 2 Jul 2020 15:43:48 +0000 (17:43 +0200)]
Merge pull request #2211 from YosysHQ/mwk/fix-fmcombine-ff

fmcombine: use the master ff cell type list

4 years agoMerge pull request #2210 from YosysHQ/mwk/fix-opt_merge
clairexen [Thu, 2 Jul 2020 15:43:34 +0000 (17:43 +0200)]
Merge pull request #2210 from YosysHQ/mwk/fix-opt_merge

opt_merge: use the master FF type list

4 years agoMerge pull request #2195 from YosysHQ/mwk/manual-gates
clairexen [Thu, 2 Jul 2020 15:43:10 +0000 (17:43 +0200)]
Merge pull request #2195 from YosysHQ/mwk/manual-gates

Add a few more gate types to the manual.

4 years agoqbfsat: Remove useless comment and #ifndef guards.
Alberto Gonzalez [Tue, 30 Jun 2020 07:00:14 +0000 (07:00 +0000)]
qbfsat: Remove useless comment and #ifndef guards.

4 years agoqbfsat: Specify default values for some options in the help message.
Alberto Gonzalez [Tue, 30 Jun 2020 06:57:45 +0000 (06:57 +0000)]
qbfsat: Specify default values for some options in the help message.

4 years agoqbfsat: Clean up external executable command lines and update temporary directory...
Alberto Gonzalez [Mon, 29 Jun 2020 23:01:56 +0000 (23:01 +0000)]
qbfsat: Clean up external executable command lines and update temporary directory name.

4 years agoqbfsat: Clean up and refactor data structures into `qbfsat.h`.
Alberto Gonzalez [Mon, 29 Jun 2020 22:06:43 +0000 (22:06 +0000)]
qbfsat: Clean up and refactor data structures into `qbfsat.h`.

4 years agoMerge pull request #2203 from antmicro/fix-grammar
clairexen [Wed, 1 Jul 2020 14:41:32 +0000 (16:41 +0200)]
Merge pull request #2203 from antmicro/fix-grammar

Signed and macro grammar update

4 years agoMerge pull request #2179 from splhack/static-cast
clairexen [Wed, 1 Jul 2020 14:40:20 +0000 (16:40 +0200)]
Merge pull request #2179 from splhack/static-cast

Support SystemVerilog Static Cast