Alberto Gonzalez
903456c267
qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.
...
Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode.
2020-05-25 20:38:29 +00:00
Eddie Hung
721283ac2a
blackbox: re-use existing Module::makeblackbox() method
2020-05-25 10:53:49 -07:00
Eddie Hung
08221edbc1
tests: xilinx macc test to have initval, shorten BMC depth for runtime
2020-05-25 10:09:05 -07:00
Eddie Hung
60aa804915
tests: fix some test warnings
2020-05-25 10:07:58 -07:00
Eddie Hung
5b81df57c8
xilinx: tidy up cells_sim.v a little
2020-05-25 09:48:11 -07:00
Eddie Hung
59b355fb85
Merge pull request #2044 from YosysHQ/eddie/fix2037
...
verilog: allow attributes on behavioural statements (including null statement)
2020-05-25 09:14:00 -07:00
Eddie Hung
9c6d216a06
tests: add test for abc9 -dff removing a redundant flop entirely
2020-05-25 08:43:33 -07:00
Eddie Hung
7bad23f19c
abc9_ops: -reintegrate to preserve flop names
2020-05-25 08:43:33 -07:00
Eddie Hung
8dd93e389e
tests: add testcase for abc9 -dff preserving flop names
2020-05-25 08:43:33 -07:00
Eddie Hung
1ebf7155a7
aiger: cleanup
2020-05-25 08:43:33 -07:00
Eddie Hung
9e6c288e5a
xaiger: cleanup
2020-05-25 08:43:33 -07:00
Eddie Hung
c5a9abba11
verilog: move attr from simple_behav_stmt to its children to attach
2020-05-25 07:36:53 -07:00
Eddie Hung
95dcd7e785
test: add attribute-before-stmt test from @nakengelhardt
2020-05-25 07:36:53 -07:00
Eddie Hung
1c117ac023
verilog: do not warn for attributes on null statements
2020-05-25 07:36:53 -07:00
Eddie Hung
29d84339bf
tests: add an generate-else test too
2020-05-25 07:36:53 -07:00
Eddie Hung
88bddb37c9
verilog: handle empty generate statement by removing gen_stmt_or_null...
...
... rule which causes a s/r conflict. Now we get an empty genblock,
which should be okay.
2020-05-25 07:36:53 -07:00
Eddie Hung
d21a07c7b5
verilog: fix #2037 by permitting (and freeing) attributes on null stmt
2020-05-25 07:36:53 -07:00
Eddie Hung
589775538c
tests: add #2037 testcase
2020-05-25 07:36:53 -07:00
clairexen
ae11156c90
Merge pull request #2015 from boqwxp/qbfsat-bisection
...
qbfsat: Add an iterative bisection optimization method and make it the default.
2020-05-25 15:50:18 +02:00
Eddie Hung
89ed34fe55
Merge pull request #2075 from YosysHQ/eddie/xaiger_cleanup
...
xaiger: do not derive cells
2020-05-24 10:10:50 -07:00
Eddie Hung
33b03ce904
xaiger: add testcase
2020-05-24 08:48:23 -07:00
Eddie Hung
d64df21630
xaiger: do not derive cells
2020-05-24 08:17:30 -07:00
Eddie Hung
227c3ff310
Merge pull request #2074 from YosysHQ/eddie/ecp5_cleanup
...
ecp5: cleanup unused +/ecp5/abc9_model.v
2020-05-23 09:28:42 -07:00
Eddie Hung
76e0cc8276
ecp5: cleanup unused +/ecp5/abc9_model.v
2020-05-23 08:17:40 -07:00
Alberto Gonzalez
ac41f8a9c7
qbfsat: Remove cruft inadvertently left untouched in commit 86fc49a9d6
.
2020-05-23 00:53:09 +00:00
Alberto Gonzalez
aea0fd5ed4
qbfsat: Add bisection mode and make it the default.
...
Also adds `-nooptimize` and reorganizes `qbfsat.cc` a bit.
2020-05-23 00:53:09 +00:00
whitequark
721040df76
Merge pull request #2072 from whitequark/cxxrtl-dont-purge
...
cxxrtl: get rid of -O5 aka `opt_clean -purge` optimization level
2020-05-22 20:08:39 +00:00
whitequark
281c96856a
cxxrtl: get rid of -O5 aka `opt_clean -purge` optimization level.
...
This isn't actually necessary anymore after scheduling was improved,
and `clean -purge` disrupts the mapping between wires in the input
RTLIL netlist and the output CXXRTL code.
2020-05-22 19:08:30 +00:00
Eddie Hung
4f0f321169
abc9_ops: update comment
2020-05-21 21:39:13 -07:00
Eddie Hung
574812d9a5
Merge pull request #2057 from YosysHQ/eddie/fix_task_attr
...
verilog: support attributes before (not after) task identifier (but 13 s/r conflicts)
2020-05-21 11:00:36 -07:00
Eddie Hung
38e858af8d
Update frontends/verilog/verilog_parser.y
...
Co-authored-by: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>
2020-05-21 09:10:56 -07:00
Miodrag Milanović
637650597b
Merge pull request #2059 from boqwxp/logger-vector-to-dict
...
log: Use `dict` instead of `std::vector<std::pair>` for `log_expect_{error, warning, log}` to better express the intent that each element is unique.
2020-05-21 15:36:30 +02:00
N. Engelhardt
026fed3135
Merge pull request #2046 from PeterCrozier/trap
...
Extend YS_DEBUGTRAP to MacOS.
2020-05-20 10:12:24 +02:00
N. Engelhardt
7c4e580f8f
Merge pull request #2054 from boqwxp/fix-smtbmc
...
smtbmc: Fix return status handling.
2020-05-20 08:55:36 +02:00
Alberto Gonzalez
6eea4b3d79
kernel: Try an order-independent approach to hashing `dict`.
...
Co-Authored-By: David Shah <dave@ds0.me>
Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
2020-05-19 23:32:53 +00:00
Alberto Gonzalez
1053032a81
smtbmc: Fix typo in error message.
...
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
2020-05-19 16:13:44 +00:00
Martin
ae887c49f9
Merge branch 'master' of https://github.com/hackfin/yosys
2020-05-19 11:14:51 +02:00
Martin
43c34a7828
idict handling in wrapper
...
- Also, re-applied no-line-break workaround to rtlil.h to make parser
catch all methods.
2020-05-19 11:13:49 +02:00
Marcelina Kościelnicka
aee439360b
Add force_downto and force_upto wire attributes.
...
Fixes #2058 .
2020-05-19 01:42:40 +02:00
Eddie Hung
2d573a0ff6
Merge pull request #1926 from YosysHQ/eddie/abc9_auto_dff
...
abc9: support seq synthesis when module has (* abc9_flop *) and bypass non-combinatorial (* abc9_box *)
2020-05-18 08:06:50 -07:00
Alberto Gonzalez
049e4caceb
firrtl: Accept techmapped cell types in FIRRTL backend.
2020-05-17 10:03:11 +00:00
Claire Wolf
fa8cb3e35d
Revert "Add support for non-power-of-two mem chunks in verific importer"
...
This reverts commit 173aa27ca5
.
2020-05-17 11:31:11 +02:00
Eddie Hung
39fa1e160d
verific: rewrite initial assume/asserts prior to elaboration
2020-05-15 14:05:28 -07:00
Alberto Gonzalez
8297afe925
log: Use `dict` instead of `std::vector<std::pair>` for `log_expect_{error, warning, log}` to better express the intent that each element is unique.
2020-05-15 00:55:32 +00:00
Eddie Hung
67fc0c3698
abc9: use (* abc9_keep *) instead of (* abc9_scc *); apply to $_DFF_?_
...
instead of moving them to $__ prefix
2020-05-14 16:44:35 -07:00
Eddie Hung
7101ef550b
verilog: attributes before task enable (but 13 s/r conflicts)
2020-05-14 16:10:11 -07:00
Eddie Hung
e7fd8912f0
tests: attributes before task enable
2020-05-14 16:09:41 -07:00
Eddie Hung
07eecff9cc
Merge pull request #2055 from YosysHQ/eddie/logger_multiple
...
logger: fix for multiple calls with same pattern
2020-05-14 15:30:08 -07:00
Alberto Gonzalez
976edb7597
kernel: Ensure `dict` always hashes to the same value given the same contents.
2020-05-14 20:06:55 +00:00
Alberto Gonzalez
35b94d1f66
kernel: Re-implement `dict` hash code as a `dict` member function instead of a specialized template for `hash_ops`.
2020-05-14 20:06:55 +00:00