Alberto Gonzalez
42fb75c570
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.
2020-07-20 22:09:44 +00:00
Alberto Gonzalez
654864658f
smtio: Add support for parsing `yosys-smt2-solver-option` info statements.
2020-07-20 21:54:56 +00:00
Alberto Gonzalez
2f786fcfac
qbfsat: Add `-solver-option` option.
2020-07-20 21:54:56 +00:00
Alberto Gonzalez
f037985337
smt2: Add `-solver-option` option.
2020-07-20 21:54:56 +00:00
clairexen
856d40973d
Merge pull request #2282 from YosysHQ/claire/satunsat
...
Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc
2020-07-20 23:06:36 +02:00
Marcelina Kościelnicka
3cb401db8c
celltypes: Fix EN port name for some FF types.
2020-07-20 23:04:10 +02:00
Claire Wolf
a207cb362c
Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-20 19:35:32 +02:00
clairexen
be6638e55b
Merge pull request #2276 from YosysHQ/mwk/satgen-cc
...
satgen: Move importCell out of the header.
2020-07-20 15:23:14 +02:00
Zachary Snow
f285f7b769
Allow reals as constant function parameters
2020-07-19 20:27:09 -06:00
Marcelina Kościelnicka
85a1bb17ed
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%.
2020-07-19 00:17:02 +02:00
Miodrag Milanović
eed05953f8
Merge pull request #2275 from YosysHQ/mwk/sf2-clkint-fix
...
sf2: Emit CLKINT even if -clkbuf not passed
2020-07-17 15:05:46 +02:00
Marcelina Kościelnicka
1b95b0e570
sf2: Emit CLKINT even if -clkbuf not passed
...
This restores pre #2229 behavior.
2020-07-17 15:01:47 +02:00
Miodrag Milanović
10bc0967e2
Merge pull request #2274 from YosysHQ/mwk/anlogic-ff-fix
...
anlogic: Fix FF mapping.
2020-07-17 14:39:31 +02:00
Marcelina Kościelnicka
a4f7777e9d
anlogic: Fix FF mapping.
2020-07-17 14:03:21 +02:00
clairexen
9a5d6e1789
Merge pull request #2229 from Ravenslofty/sf2_remove_sf2_iobs
...
sf2: replace sf2_iobs with {clkbuf,iopad}map
2020-07-16 18:33:56 +02:00
clairexen
f3d7e9a1df
Merge pull request #2273 from whitequark/write-verilog-always-star-initial
...
verilog_backend: in non-SV mode, add a trigger for `always @*`
2020-07-16 18:30:50 +02:00
clairexen
c49344b262
Merge pull request #2272 from whitequark/write-verilog-sv
...
verilog_backend: add `-sv` option, make `-o <filename>.sv` work
2020-07-16 18:28:24 +02:00
Miodrag Milanović
910f421324
Merge pull request #2238 from YosysHQ/mwk/dfflegalize-anlogic
...
anlogic: Use dfflegalize.
2020-07-16 18:07:58 +02:00
Miodrag Milanović
b74eb598bc
Merge pull request #2226 from YosysHQ/mwk/nuke-efinix-gbuf
...
efinix: Nuke efinix_gbuf in favor of clkbufmap.
2020-07-16 18:07:41 +02:00
whitequark
128522f173
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 .
2020-07-16 11:30:14 +00:00
whitequark
d9f680b236
verilog_backend: add `-sv` option, make `-o <filename>.sv` work.
...
See #2271 .
2020-07-16 10:44:08 +00:00
whitequark
a87e338381
Merge pull request #2270 from whitequark/cxxrtl-fix-typo
...
cxxrtl: fix typo
2020-07-16 09:48:10 +00:00
whitequark
cb757b28b4
Merge pull request #2269 from YosysHQ/claire/bisonwall
...
Use "bison -Wall -Werror" for verilog front-end
2020-07-15 19:20:33 +00:00
Claire Wolf
51ee0b683f
Treat all bison warnings as errors in verilog front-end
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-15 11:57:31 +02:00
Claire Wolf
7a79843cc3
Use %precedence in verilog_parser.y
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-15 11:54:28 +02:00
Claire Wolf
24540291c7
Fix bison warnings for missing %empty
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-15 11:50:59 +02:00
Claire Wolf
1f4e452609
Run bison with -Wall for verilog front-end
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-15 11:49:36 +02:00
clairexen
021ce8e596
Merge pull request #2257 from antmicro/fix-conflicts
...
Restore #2203 and #2244 and fix parser conflicts
2020-07-15 11:49:09 +02:00
Kamil Rakoczy
02c071888b
Add missing semicolons
...
Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>
2020-07-15 10:15:13 +02:00
Marcelina Kościelnicka
61a7ec4768
opt_merge: Dedup one more use of FF cell type list.
2020-07-15 06:19:18 +02:00
Marcelina Kościelnicka
a786091b46
achronix: Use dfflegalize.
2020-07-14 23:12:16 +02:00
whitequark
a5cf000377
cxxrtl: fix typo. NFC.
2020-07-14 16:10:30 +00:00
Marcelina Kościelnicka
3050454d6e
anlogic: Use dfflegalize.
2020-07-14 05:02:50 +02:00
Marcelina Kościelnicka
3209c0762a
intel: Use dfflegalize.
2020-07-13 19:21:05 +02:00
Lofty
a3a90f6377
Revert "intel_alm: direct M10K instantiation"
...
This reverts commit 09ecb9b2cf
.
2020-07-13 18:05:38 +02:00
whitequark
38b814b525
Merge pull request #2263 from whitequark/cxxrtl-capi-eval-commit
...
cxxrtl: expose eval() and commit() via the C API
2020-07-13 02:44:36 +00:00
whitequark
5349a922e4
cxxrtl: expose eval() and commit() via the C API.
2020-07-12 23:34:18 +00:00
Marcelina Kościelnicka
347dd01c2f
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.
2020-07-12 23:41:27 +02:00
Marcelina Kościelnicka
b33744b03a
proc_dlatch: Remove init values for combinatorial processes.
...
Fixes #2258 .
2020-07-12 18:50:30 +02:00
Marcelina Kościelnicka
240351c44e
dfflegalize: Gather init values from all wires.
...
Skipping non-selected wires is unsound in an obvious way.
2020-07-12 17:39:13 +02:00
clairexen
eef0ec6aed
Merge pull request #2256 from YosysHQ/claire/fix2241
...
Add AST_EDGE support to AstNode::detect_latch()
2020-07-10 19:07:50 +02:00
Claire Wolf
f9ed09423e
Add AST_EDGE support to AstNode::detect_latch(), fixes #2241
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-10 18:41:13 +02:00
Kamil Rakoczy
d77b3305d8
Fix S/R conflicts
...
This commit fixes S/R conflicts introduced by commit 6f9be93
.
Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>
2020-07-10 15:03:53 +02:00
Kamil Rakoczy
0ffaddee5e
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>
2020-07-10 15:03:01 +02:00
Kamil Rakoczy
de649b9194
Revert "Revert PRs #2203 and #2244."
...
This reverts commit 9c120b89ac
.
2020-07-10 09:59:48 +02:00
Dan Ravensloft
7dc0439de4
sf2: replace sf2_iobs with {clkbuf,iopad}map
2020-07-09 21:28:52 +01:00
whitequark
c0bcbe1f62
Merge pull request #2255 from whitequark/bison-Werror-conflicts
...
verilog_parser: turn S/R and R/R conflicts into hard errors
2020-07-09 20:17:19 +00:00
whitequark
0e9b889b77
Merge pull request #2254 from whitequark/cxxrtl-extern-c
...
cxxrtl: add missing extern "C"
2020-07-09 20:17:12 +00:00
Marcelina Kościelnicka
edbaf2fdf6
sf2: Use dfflegalize.
2020-07-09 21:56:14 +02:00
whitequark
dc35ef05f9
verilog_parser: turn S/R and R/R conflicts into hard errors.
...
Fixes #2253 .
2020-07-09 19:36:59 +00:00