Commit Graph

14168 Commits

Author SHA1 Message Date
N. Engelhardt 584692d53c
Merge pull request #4281 from YosysHQ/cat/issue-template-wasm
Add WebAssembly as a platform to `ISSUE_TEMPLATE/bug_report.yml`
2024-03-15 10:01:26 +01:00
Miodrag Milanovic 7c09fa572e real number handling and default to string 2024-03-14 10:37:56 +01:00
Miodrag Milanovic 4279cea33a improve handling VHDL constants 2024-03-14 10:37:56 +01:00
Miodrag Milanovic 858eae5572 verific_const: convert VHDL values to RTLIL consts 2024-03-14 10:37:56 +01:00
Catherine 29e3e10378
Add WebAssembly as a platform to ISSUE_TEMPLATE/bug_report.yml. 2024-03-13 10:04:13 +00:00
github-actions[bot] b3124f30e4 Bump version 2024-03-13 00:15:33 +00:00
Miodrag Milanovic 18cec2d9a9 Next dev cycle 2024-03-12 08:57:48 +01:00
Miodrag Milanovic 00338082b0 Release version 0.39 2024-03-12 08:55:10 +01:00
github-actions[bot] 0944664e60 Bump version 2024-03-12 00:15:21 +00:00
Krystine Sherwin 643c9540da
Makefile: reorder CONFIG=none check 2024-03-12 09:39:25 +13:00
Krystine Sherwin e0389436da
Makefile: Remove narrowing from ABCMKARGS 2024-03-12 09:18:38 +13:00
N. Engelhardt 0909c2ef5e
Merge pull request #4268 from jix/smtbmc-track-assumes
smtbmc: Add --track-assumes and --minimize-assumes options
2024-03-11 16:34:30 +01:00
Jannis Harder 42122e240e smtbmc: Add --track-assumes and --minimize-assumes options
The --track-assumes option makes smtbmc keep track of which assumptions
were used by the solver when reaching an unsat case and to output that
set of assumptions. This is particularly useful to debug PREUNSAT
failures.

The --minimize-assumes option can be used in addition to --track-assumes
which will cause smtbmc to spend additional solving effort to produce a
minimal set of assumptions that are sufficient to cause the unsat
result.
2024-03-11 15:13:11 +01:00
N. Engelhardt e4f11eb0a0
Merge pull request #4228 from povik/synth-inject
synth: Introduce `-extra-map` for amending techmap
2024-03-11 14:55:45 +01:00
Martin Povišer d42c04bc48
Merge pull request #4274 from YosysHQ/fix_warning
fix compile warning
2024-03-11 10:58:48 +01:00
Miodrag Milanovic 5e05300e7b fix compile warning 2024-03-11 10:55:09 +01:00
Martin Povišer 206d894c56 check: Omit private wires in loop report 2024-03-11 10:45:36 +01:00
Martin Povišer 5924d97381 tests: Remove part of test involving combinational loops 2024-03-11 10:45:36 +01:00
Martin Povišer d01728aaa5 celledges: Register async FF paths 2024-03-11 10:45:36 +01:00
Martin Povišer 87e72ef86f celledges: Add read ports arst paths 2024-03-11 10:45:17 +01:00
Martin Povišer 4a10e78777 celledges: Emit empty edges for write/init ports 2024-03-11 10:45:17 +01:00
Martin Povišer e4296072c4 check: Rephrase regex for portability 2024-03-11 10:45:17 +01:00
Martin Povišer 4fdcf388d3 check: Assert edges data is not out-of-bounds 2024-03-11 10:45:17 +01:00
Martin Povišer e1e77a7fa9 check: Extend testing 2024-03-11 10:45:17 +01:00
Martin Povišer b6112b3551 check: Consider read ports in loop detection 2024-03-11 10:45:17 +01:00
Martin Povišer 3a1ef44564 celledges: Describe asynchronous read ports 2024-03-11 10:45:17 +01:00
Martin Povišer 3eef6450f1 check: Add coarse-grain false positive test 2024-03-11 10:43:49 +01:00
Martin Povišer fa74d0bd1a check: Use cell edges data in detecting combinational loops 2024-03-11 10:43:49 +01:00
Martin Povišer c5ae74af34 check: Improve found loop logging
Print the detected loop in-order, and include source location for each
node, if available.
2024-03-11 10:43:49 +01:00
Martin Povišer 6e5f40e364 utils: Save detected loops with their nodes in-order 2024-03-11 10:43:49 +01:00
github-actions[bot] 078b876f50 Bump version 2024-03-09 00:14:37 +00:00
Krystine Sherwin 344ca18239
Makefile: Move CXX print to echo-cxx 2024-03-09 10:25:41 +13:00
Krystine Sherwin 56f66596b0
Change default CONFIG to none
- Use default value of `CXX` instead of forcing override to `clang++`.
- Add base `CXXFLAGS` and `ABCMKARGS` in else condition of `ifeq ($(CONFIG),..)`
  block and output the value of `CXX`.
- Change readme to mention `CXX` envvar and that using `make config-clang` etc
  will ignore `CXX`.
2024-03-09 10:25:41 +13:00
Miodrag Milanović 6d528ef808
Merge pull request #4271 from YosysHQ/macos-fix
ci: Fix mac builds
2024-03-08 14:17:32 +01:00
N. Engelhardt d70113a909
Merge pull request #3972 from nakengelhardt/celledges_shift_ops
celledges: support shift ops
2024-03-08 09:35:47 +01:00
Krystine Sherwin b4da6b80f8
ci: Fix mac builds 2024-03-08 11:56:01 +13:00
Martin Povišer 158fbf881e memory_map: Explain `-iattr` better 2024-03-06 15:15:37 +01:00
Martin Povišer 570a8f12b5
synth: Fix out-of-sync help message
Co-authored-by: N. Engelhardt <nakengelhardt@gmail.com>
2024-03-06 14:55:43 +01:00
github-actions[bot] e9cd6ca9e8 Bump version 2024-03-06 00:16:02 +00:00
Catherine f60b77a7f0 cxxrtl: add ability to record/replay diagnostics.
Note that this functionality is only used by diagnostics emitted by
the C++ testbench; diagnostics emitted by the RTL in `eval()` do not
need to be recorded since they will be emitted again during replay.
2024-03-05 17:00:02 +00:00
Jannis Harder 04ecabdd1f
Merge pull request #4222 from jix/pdr-X
write_aiger: Include `$assert` and `$assume` cells in -ywmap output
2024-03-05 15:13:51 +01:00
Jannis Harder 0db76c6ec4 tests/sva: Skip sva tests that use SBY until SBY is compatible again
This commit is part of a PR that requires corresponding changes in SBY.
To prevent CI failures, detect whether those changes already landed and
skip the SBY using tests until then.
2024-03-05 14:37:33 +01:00
github-actions[bot] 1e42b4f0f9 Bump version 2024-03-05 00:15:21 +00:00
Krystine Sherwin 3635f911dc
Docs: Updates from @povik comments 2024-03-05 05:57:27 +13:00
Krystine Sherwin 1455941ab9
Merge branch 'master' into krys/docs 2024-03-05 05:48:46 +13:00
Krystine Sherwin 3596025283
docs: Remove TODOs from output
Remove highlighting of wreduce/opt_clean bug.
2024-03-05 05:44:40 +13:00
Jannis Harder ff6c29ab1e Update abc revision 2024-03-04 16:53:03 +01:00
Jannis Harder 97db1cb745 smtbmc: Cache hierarchy for loading multiple yw files
This will be used by sby/tools/cexenum via the incremental interface.
2024-03-04 16:53:03 +01:00
Jannis Harder d03c5e2a00 smtbmc: Break dependency recursion during unrolling
Previously `unroll_stmt` would recurse over the smtlib expressions as
well as recursively follow not-yet-emitted definitions the current
expression depends on. While the depth of smtlib expressions generated
by yosys seems to be reasonably bounded, the dependency chain of
not-yet-emitted definitions can grow linearly with the size of the
design and linearly in the BMC depth.

This makes `unroll_stmt` use a `list` as stack, using python generators
and `recursion_helper` function to keep the overall code structure of
the previous recursive implementation.
2024-03-04 16:53:03 +01:00
Jannis Harder d8cdc213a6 rename -witness: Bug fix and rename formal cells
Rename formal cells in addition to witness signals. This is required to
reliably track individual property states for the non-smtbmc flows.

Also removes a misplced `break` which resulted in only partial witness
renaming.
2024-03-04 16:53:03 +01:00