Commit Graph

1417 Commits

Author SHA1 Message Date
N. Engelhardt d87bd7ca3f
Merge pull request #3887 from kivikakk/env-bash
tests: use /usr/bin/env for bash.
2023-12-18 16:33:35 +01:00
Jannis Harder 94d7c22714 yosys-witness: Add aiw2yw --present-only to omit unused signals 2023-12-14 16:45:19 +01:00
Jannis Harder 3fab4d42ec smtbmc: Allow raw SMT-LIBv2 comamnds and expressions for --incremental 2023-12-14 16:44:21 +01:00
Jannis Harder 111085669b smtbmc: Use fewer smt commands while writing .yw traces
Depending on the used solver and design this can be a signficant
performance improvement.
2023-12-14 16:42:48 +01:00
Martin Povišer 449e3dbbd3 cxxrtl: Mask `bmux` result appropriately 2023-12-14 06:57:28 +00:00
Merry d7cb6981b5 cxxrtl: Fix value::ctlz 2023-12-13 12:21:44 +00:00
Merry ded63bedd5 cxxrtl: Fix value::sshr 2023-12-13 12:11:57 +00:00
Merry ff53f3d2b6 cxxrtl: Fix value::shl 2023-12-13 12:02:30 +00:00
Henri Nurmi 1c8e58a736 cxxrtl: Fix formating 2023-12-13 06:08:01 +00:00
Henri Nurmi 79c0bfcb22 cxxrtl: Remove unnecessary length check 2023-12-13 06:08:01 +00:00
Henri Nurmi dbff694e3d cxxrtl: Use the base name of the interface file for the include directive
Prior to this fix, the `CxxrtlBackend` used the entire path for the include
directive when a separated interface file is generated (via the `-header`
option). This commit updates the code to use the base name of the interface
file.

Since the C++11 standard is used by default, we cannot take advantage of
the `std::filesystem` to get the basename.
2023-12-13 06:08:01 +00:00
Martin Povišer 18d1907fa8 cxxrtl: Assert well-formedness of input to `udivmod` 2023-12-12 10:08:12 +01:00
Martin Povišer 6206a3af30 cxxrtl: Handle case of `Bits < 4` in formatting of values 2023-12-12 09:51:17 +01:00
Martin Povišer c848d98d91 cxxrtl: Fix `udivmod` logic 2023-12-11 22:11:35 +01:00
Martin Povišer bcf5e92389 cxxrtl: Fix `ctlz` implementation 2023-12-11 22:10:51 +01:00
Merry 0681baae19 cxxrtl: Extract divmod algorithm into value 2023-12-09 19:23:04 +00:00
Merry 99c8143ded cxxrtl: Remove redundant divmod 2023-12-09 19:23:04 +00:00
Catherine 62bbd086b1 cxxrtl: reorganize runtime component files.
In preparation for substantial expansion of CXXRTL's runtime, this commit
reorganizes the files used by the implementation. Only minimal changes are
required in a consumer.

First, change:
  -I$(yosys-config --datdir)/include
to:
  -I$(yosys-config --datdir)/include/backends/cxxrtl/runtime

Second, change:
  #include <backends/cxxrtl/cxxrtl.h>
to:
  #include <cxxrtl/cxxrtl.h>
(and do the same for cxxrtl_vcd.h, etc.)
2023-11-28 15:32:36 +00:00
Jannis Harder e319606ec9 smtbmc: Add --incremental mode 2023-11-16 13:22:17 +01:00
Catherine 6ffc315936 cxxrtl: export wire attributes through the C API.
Co-authored-by: Charlotte <charlotte@lottia.net>
2023-10-25 16:01:48 +00:00
Wanda c36cf9c5ac write_verilog: avoid emitting empty cases.
The Verilog grammar does not allow an empty case.  Most synthesis tools
are quite permissive about this, but Quartus is not.  This causes
problems for amaranth with Quartus (see amaranth-lang/amaranth#931).
2023-10-08 01:11:30 +02:00
Miodrag Milanović c6caadfed4
Merge pull request #3902 from YosysHQ/krys/yw_join
yosys-witness concat yw trace files
2023-08-25 15:21:44 +02:00
Asherah Connor 4a475fa7a2 cxxrtl: include iostream when prints are used 2023-08-17 07:08:22 +02:00
Charlotte d130f7fca2 tests: use /usr/bin/env for bash. 2023-08-12 11:59:39 +10:00
Charlotte 2829cd9caa cxxrtl_backend: move sync $print grouping out of dump into analyze 2023-08-11 04:46:52 +02:00
Charlotte ce245b5105 cxxrtl_backend: respect sync `$print` priority
We add a new flow graph node type, PRINT_SYNC, as they don't get handled
with regular CELL_EVALs.  We could probably move this grouping out of
the dump method.
2023-08-11 04:46:52 +02:00
Charlotte 04582f2fb7 verilog_backend: emit sync `$print` cells with same triggers together
Sort by PRIORITY, ensuring output order.
2023-08-11 04:46:52 +02:00
Charlotte 4ffdee65e0 cxxrtl: store comb $print cell last EN/ARGS in module
statics were obviously wrong -- may be multiple instantiations of any
given module.  Extend test to cover this.
2023-08-11 04:46:52 +02:00
Charlotte 843ad9331b cxxrtl: WIP: adjust comb display cells to only fire on change
Naming and use of statics to be possibly revised.
2023-08-11 04:46:52 +02:00
Charlotte 7f7c61c9f0 fmt: remove lzero by lowering during Verilog parse
See https://github.com/YosysHQ/yosys/pull/3721#issuecomment-1502037466
-- this reduces logic within the cell, and makes the rules that apply
much more clear.
2023-08-11 04:46:52 +02:00
Charlotte fc0acd0ad1 cxxrtl: restrict -print-output to cout, cerr 2023-08-11 04:46:52 +02:00
Charlotte f9b149fa7b cxxrtl: add "-print-output" option, test in fmt 2023-08-11 04:46:52 +02:00
Charlotte bfa8b631bf cxxrtl: remove unused signedDivideWithRemainder 2023-08-11 04:46:52 +02:00
Charlotte 3571bf2c2d fmt: fuzz, remove some unnecessary busywork
Removing some signed checks and logic where we've already guaranteed the
values to be positive.  Indeed, in these cases, if a negative value got
through (per my realisation in the signed fuzz harness), it would cause
an infinite loop due to flooring division.
2023-08-11 04:46:52 +02:00
Charlotte 2ae551c0af fmt: fuzz, fix (remove extraneous + incorrect fill)
"blk + chunks" is often an overrun, plus the fill is unnecessary; we
throw blk away immediately.
2023-08-11 04:46:52 +02:00
Charlotte c382d7d3ac fmt: %t/$time support 2023-08-11 04:46:52 +02:00
Charlotte 52dc397a50 cxxrtl: don't use signed divide with unsigned/pos values
Incorrect for unsigned, wasted effort for positive signed.
2023-08-11 04:46:52 +02:00
Charlotte 095b093f4a cxxrtl: first pass of $print impl 2023-08-11 04:46:52 +02:00
whitequark 3f8eab15bb write_verilog: translate $print cells to $write tasks in always blocks. 2023-08-11 04:46:52 +02:00
Jannis Harder 77c7355d53 smtbmc: Avoid quadratic behavior when scanning s-exprs
The previous implementation for finding the end of a top-level s-expr
exhibited quadratic behavior as it would re-scan the complete input for
the current expression for every new line. For large designs with
trivial properties this could easily take seconds and dominate the
runtime over the actual solving.

This change remembers the current nesting level between lines, avoiding
the re-scanning.
2023-08-01 17:19:29 +02:00
N. Engelhardt 43780c9812
Merge pull request #3838 from povik/various-cleanup 2023-07-24 16:24:23 +02:00
Martin Povišer 51ef942547 verilog_backend: Use hashlib dict for `auto_name_map`
This is most likely faster.
2023-07-20 21:00:33 +01:00
Martin Povišer 596743a6b6 verilog_backend: Make the keywords pool static
Do not recreate the keywords pool on every lookup of an identifier.
2023-07-20 21:00:33 +01:00
Martin Povišer 78d13d1956 Mention 'bwmuxmap' in 'write_firrtl' help
The FIRRTL backend does call into the 'bwmuxmap' pass but omits it in
the help message.
2023-07-10 12:45:03 +02:00
Martin Povišer c0b1a7daa4 Drop stray 'cellaigs.h' include from backend passes
This include seems to have been copied over from the JSON backend where
AIG models are sometimes inserted into the JSON output, but these other
backends don't do anything with AIG.
2023-07-10 12:45:03 +02:00
Martin Povišer 06256c0c00 Slightly adjust the wording of "write_blif" help 2023-07-10 12:41:43 +02:00
Charlotte eb397592f0 cxxrtl: add `$divfloor`. 2023-06-28 15:27:06 +01:00
Jannis Harder 596da3f2a6
Merge pull request #3815 from charlottia/py312-syntax 2023-06-26 16:36:58 +02:00
Jannis Harder f9744fdfcd smtbmc: Make cover mode respect --keep-going
As cover mode by default stops looking for further traces when an
assertion fails, it should respect --keep-going.
2023-06-23 10:27:38 +02:00
Charlotte 3f29bdbbc5 smt2: py3.12+: avoid SyntaxWarning.
Python 3.12 emits a SyntaxWarning when encountering invalid escape
sequences.  They still parse as expected.  Marking these raw produces
the same result without the warnings.
2023-06-23 14:40:02 +10:00