Commit Graph

1545 Commits

Author SHA1 Message Date
Catherine b74d33d1b8 fmt: rename TIME to VLOG_TIME.
The behavior of these format specifiers is highly specific to Verilog
(`$time` and `$realtime` are only defined relative to `$timescale`)
and may not fit other languages well, if at all. If they choose to use
it, it is now clear what they are opting into.

This commit also simplifies the CXXRTL code generation for these format
specifiers.
2024-01-19 15:12:05 +00:00
Catherine 08d7f54726 cxxrtl: move a definition around. NFC 2024-01-19 15:12:05 +00:00
Jannis Harder ac6fcb2547 write_aiger: Detect and error out on combinational loops
Without this it will overflow the stack when loops are present.
2024-01-19 15:36:14 +01:00
Catherine 5a1fcdea13 cxxrtl: include attributes in `performer::on_print` callback.
This is useful primarily to determine the source location, but can also
be used for any other purpose.
2024-01-16 16:39:11 +00:00
Catherine 905f07c03f cxxrtl: introduce `performer`, a context object for `eval()`. (breaking change)
At the moment the only thing it allows is redirecting `$print` cell
output in a context-dependent manner. In the future, it will allow
customizing handling of `$check` cells (where the default is to abort),
of out-of-range memory accesses, and other runtime conditions with
effects.

This context object also allows a suitably written testbench to add
Verilog-compliant `$time`/`$realtime` handling, albeit it involves
the ceremony of defining a `performer` subclass. Most people will
want something like this to customize `$time`:

    int64_t time = 0;
    struct : public performer {
      int64_t *time_ptr;
      int64_t time() const override { return *time_ptr; }
    } performer = { &time };

    p_top.step(&performer);
2024-01-16 16:37:07 +00:00
Catherine 02e3d508fa cxxrtl: remove `module::steps`. (breaking change)
This approach to tracking simulation time was a mistake that I did not
catch in review. It has several issues:
1. There is absolutely no requirement to call `step()`, as it is
   a convenience function. In particular, `steps` will not be
   incremented in submodules if `-noflatten` is used.
2. The semantics of `steps` does not match that of the Verilog `$time`
   construct.
3. There is no way to make the semantics of `%t` match that of Verilog.
4. The `module` interface is intentionally very barebones. It is little
   more than a container for three method pointers, `reset`, `eval`,
   and `commit`. Adding ancillary data to it goes against this.

If similar functionality is introduced again it should probably be
a variable that is global per toplevel design using some object that is
unique for an entire hierarchy of modules, and ideally exposed via
the C API. For now, it is being removed (in this commit) and (in next
commit) the capability is being reintroduced through a context object
that can be specified for `eval()`.
2024-01-16 16:35:51 +00:00
Catherine a33acb7cd9 cxxrtl: refactor the formatter and use a closure.
This commit achieves three roughly equally important goals:
1. To bring the rendering code in kernel/fmt.cc and in cxxrtl.h as close
   together as possible, with an ideal of only having the bigint library
   as the difference between the render functions.
2. To make the treatment of `$time` and `$realtime` in CXXRTL closer to
   the Verilog semantics, at least in the formatting code.
3. To change the code generator so that all of the `$print`-to-`string`
   conversion code is contained inside of a closure.

There are two reasons to aim for goal (3):
a. Because output redirection through definition of a global ostream
   object is neither convenient nor useful for environments where
   the output is consumed by other code rather than being printed on
   a terminal.
b. Because it may be desirable to, in some cases, ignore the `$print`
   cells that are present in the netlist based on a runtime decision.
   This is doubly true for an upcoming `$check` cell implementing
   assertions, since failing a `$check` would by default cause a crash.
2024-01-16 16:35:51 +00:00
Catherine bf1a99da09 cxxrtl: make observer methods non-virtual. (breaking change)
This avoids having to devirtualize them later to get performance back,
and simplifies the code a bit.

The change is prompted by the desire to add a similar observer object
to `eval()`, and a repeated consideration of whether the dispatch on
these should be virtual in first place.
2024-01-16 09:58:21 +00:00
Catherine ed81cc5f81 cxxrtl: rename observer::{on_commit→on_update}. (breaking change)
The name `on_commit` was terrible since it would not be called, as one
may conclude from the name, on each `commit()`, but only whenever that
method actually updates a value.
2024-01-16 09:58:21 +00:00
Catherine 7142e20dab write_cxxrtl: support initial `$print` cells. 2024-01-11 15:27:21 +01:00
Catherine d493225313 write_cxxrtl: reset state value of comb `$print` cells. 2024-01-11 15:17:06 +01:00
Catherine 1159e48721 write_verilog: emit `initial $display` correctly. 2024-01-11 13:13:04 +01:00
Catherine 0486f61a35 write_verilog: emit zero width parameters as `.PARAM()`. 2024-01-11 13:13:04 +01:00
Catherine bc9206f0f5 write_verilog: emit `casez` as `if/elif/else` whenever possible. 2024-01-09 14:49:20 +00:00
Catherine f6e36f0e54 cxxrtl: implement a generic record/replay interface.
This commit adds a reader/writer implementation for a file format
optimized for fast, single-pass storage and retrieval of design state
changes, as well as a recorder/replayer that integrate with the eval
and commit simulation steps to create replay logs and reproduce them
later.

This feature makes it possible to run a simulation once, recording
the stimulus as well as changes to the registers, and navigate to
a past time point in the simulation later without rerunning it.
Both the changes in inputs (stimulus) and changes in state are saved
so that navigation does not require calling `eval()` or `commit()`;
only a series of memory copy operations.

On a representative example of a SoC netlist, saving the replay log
while simulating it takes 150% of the time it would take to simulate
the same design without logging, which is a much lower overhead than
writing an equivalent full view (including memories) VCD waveform dump.
The replay log is also several times smaller than the VCD dump, and
more space savings are available as low hanging fruit.

Replaying the log has not been optimized and currently takes about
the same time as running the simulation in first place. However, it
is still useful since it provides fast navigation to an arbitrary time
point, something that rerunning the simulation does not allow for.

The current file format should be considered preliminary. It is not
very space-efficient, and my testing shows that a lot of time is spent
in the write() syscall in the kernel. Most likely, compression and/or
writing in another thread could improve performance by 10-20%. This
may be done at a later time.
2024-01-09 13:48:36 +00:00
Catherine a59d477098 cxxrtl: improve robustness of `cxxrtl::time`.
Avoid overflow during conversion for any representable raw value.
2024-01-09 13:44:39 +00:00
Catherine 5aaf1f1d39 cxxrtl: implement `value.get()` and `value.set()` for signed types. 2024-01-09 13:44:39 +00:00
Martin Povišer 82fca50309 write_verilog: Handle edge case with non-pruned processes
This change only matters for processes that weren't processed by
`proc_rmdead` for which follow-up cases after a default case are treated
differently in Verilog and RTLIL semantics.
2024-01-06 17:05:02 +01:00
Catherine f9dc1a2184 cxxrtl: fix comment wording. NFC 2024-01-05 20:41:16 +00:00
Catherine 3e358d9bfa cxxrtl: add a way to observe state changes during the commit step.
The commit observer is a structure containing a callback that is invoked
whenever the `commit()` method changes a wire or a memory. This allows
code external to the compiled netlist to react to changes in the design
state in a very efficient way. One example of how this feature can be
used is an efficient implementation of record/replay.

Note that the VCD writer does not benefit from this feature because it
must be able to react to changes in any debug items and not just those
that contain design state.
2024-01-05 19:02:00 +00:00
Catherine a94fafa8fe cxxrtl: add a representation of simulation timestamps.
While the VCD format separates the timescale and the timestep (likely
to allow representing the timestep with a small integer type), time in
CXXRTL is represented using a uniform 96-bit number, which allows for
a ±100 year range at femtosecond resolution.

The implementation uses `value<96>`, which provides fast arithmetic and
comparison operations, as well as conversion to/from a more common
representation of integer seconds plus femtoseconds.
2024-01-05 19:01:45 +00:00
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
Clifford Wolf cff3195caa Improve EDIF lib_cell_ports scan 2023-06-20 10:42:05 +02:00
Clifford Wolf fb9e12761b Add "write_edif -lsbidx" 2023-06-20 10:40:15 +02:00
Charlotte Connor c9d31c3c87 smt2: abits needs to be at least 1 for BitVec
BitVecs need a minimum length of 1; we zero-fill any extra bits in the
extend_u0() calls which works perfectly.
2023-06-13 15:01:45 +10:00
Jannis Harder 06f06c7be2
Merge pull request #3801 from jix/witness-aiw2yw-xbits 2023-06-12 16:12:39 +02:00
Jannis Harder dcc4d6e90b yosys-witness: Don't treat aiw x-bits as don't change
While treating initialization only bits as don't change during later
cycles is correct, actual x-bits should be kept as x-bits.
2023-06-09 15:21:22 +02:00
N. Engelhardt 6f5d984bdb
Merge pull request #3778 from jix/yw_clk2fflogic 2023-06-05 16:15:04 +02:00
Claire Xenia Wolf d7f25165a5 Add ninitff line to aiger .aim files
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2023-06-03 14:38:22 +02:00
Jannis Harder e36c71b5b7 Use clk2fflogic attr on cells to track original FF names in witnesses
This makes clk2fflogic add an attr to $ff cells that carry the state of
the emulated async FF. The $ff output doesn't have any async updates
that happened in the current cycle, but the $ff input does, so the $ff
input corresponds to the async FF's output in the original design.

Hence this patch also makes the following changes to passes besides
clk2fflogic (but only for FFs with the clk2fflogic attr set):

  * opt_clean treats the input as a register name (instead of the
    output)

  * rename -witness ensures that the input has a public name

  * the formal backends (smt2, btor, aiger) will use the input's
    name for the initial state of the FF in witness files

  * when sim reads a yw witness that assigns an initial value to the
    input signal, the state update is redirected to the output

This ensures that yosys witness files for clk2fflogic designs have
useful and stable public signal names. It also makes it possible to
simulate a clk2fflogic witness on the original design (with some
limitations when the original design is already using $ff cells).

It might seem like setting the output of a clk2fflogic FF to update the
input's initial value might not work in general, but it works fine for
these reasons:

  * Witnesses for FFs are only present in the initial cycle, so we do
    not care about any later cycles.

  * The logic that clk2fflogic generates loops the output of the
    genreated FF back to the input, with muxes in between to apply any
    edge or level sensitive updates. So when there are no active updates
    in the current gclk cycle, there is a combinational path from the
    output back to the input.

  * The logic clk2fflogic generates makes sure that an edge sensitive
    update cannot be active in the first cycle (i.e. the past initial
    value is assumed to be whatever it needs to be to avoid an edge).

  * When a level sensitive update is active in the first gclk cycle, it
    is actively driving the output for the whole gclk cycle, so ignoring
    any witness initialization is the correct behavior.
2023-05-25 12:48:02 +02:00
Jannis Harder 4f3d1be96a
Merge pull request #3767 from YosysHQ/krys/yw_fix
Assign wires an smtoffset
2023-05-22 16:10:55 +02:00
Jannis Harder 5fb1223861
Merge pull request #3733 from AdamHillier/aiger-inputs
Add outputs before inputs to the sigmap in the AIGER backend.
2023-05-22 16:09:15 +02:00
Krystine Sherwin 18b44a1e84
yosys-witness: add append option to yw2yw
Can now append a user defined number of steps to input traces when joining.
If the number of steps is +ve, inputs are all set to 0.
If -ve then steps are skipped.
If all of steps are skipped (including init step) then the input trace will not be copied.
If more than one input trace is provided, the append option will need to be provided the same number of times as there are input traces.
2023-05-22 11:44:19 +12:00
Krystine Sherwin 8c9a0b51d4
yosys-witness concat yw trace files
Intended for use with SCY to combine sequential cover traces.
Arbitrary number of inputs, will load all and attempt to join them.  Each trace will be replayed one after the other, in the same order as the files are provided.
Mismatch in init_only fields seems to work fine, with values in subsequent traces being assigned in the initial only if they weren't previously defined.
Uncertain if a mismatch in non init_only fields will cause problems.
Fixes WitnessSig.__eq__().
Adds helper functions to WitnessValues and ReadWitness classes.
2023-05-22 10:13:17 +12:00
Jannis Harder e6f3914800 smt2: Use smt bv offset for `$any*`'s smtoffset
While not setting the smtoffset here was clearly a bug, I think using
`chunk.offset` only worked incidentally. The `smtoffset` is an offset
into the `smtname, smtid` pair (here `"", idcounter`) which corresponds
to the smt bitvector `stringf("%s#%d", get_id(module), idcounter)` which
contains all the chunks this loop is iterating over.

Thus using an incrementing `smtoffset` (like the `$ff`/`$dff` case above
already does) should be the correct fix.
2023-05-18 11:58:09 +02:00
Krystine Sherwin 52ad7a47f3
Assign wires an smtoffset
Wires weren't being assigned an smtoffset value so when generating a yosys witness trace it would also use an offset of 0.
Not sure if this has any other effects, but it fixes the bug I was having.
@jix could you take a look at this?
2023-05-18 10:37:55 +12:00
Benjamin Barzen 8611429237
ABC9: Cell Port Bug Patch (#3670)
* ABC9: RAMB36E1 Bug Patch

* Add simplified testcase

* Also fix xaiger writer for under-width output ports

* Remove old testcase

* Missing top-level input port

* Fix tabs

---------

Co-authored-by: Eddie Hung <eddie@fpgeh.com>
2023-04-22 16:24:36 -07:00
AdamHillier 3861cc31f0 Add outputs before inputs to the sigmap in the AIGER backend. 2023-04-19 11:00:51 +00:00
Catherine 4bb173e256 yosys-smtbmc: support -h/--help (and exit with code 0). 2023-02-27 20:31:00 +00:00
Jannis Harder 160eeab2bb verilog_backend: Do not run bwmuxmap even if in expr mode
While bwmuxmap generates equivalent logic, it doesn't propagate x bits
in the same way, which can be relevant when writing verilog.
2023-02-13 14:00:38 +01:00
Aki Van Ness a90f940615 backends/firrtl: Ensure `modInstance` is valid
This should fix #3648 where when calling `emit_elaborated_extmodules` it
checks to see if a module is a black-box, however there was no
validation that the cell type was actually known, and it just always
assumed that we would get a valid instance, causing a segfault.
2023-02-03 08:27:52 -05:00
Jannis Harder 0f2cb80a26
Merge pull request #3655 from jix/smt2_fix_b_op_width
smt2: Fix operation width computation for boolean producing cells
2023-02-01 18:06:59 +01:00
Jannis Harder 5e82638408 smt2: Fix operation width computation for boolean producing cells
The output width for the boolean value should not influence the
operation width. The previous incorrect width extension would still
produce correct results, but could produce invalid smt2 output for
reduction operators when the output width was larger than the width of
the vector to which the reduction was applied.

This fixes #3654
2023-02-01 12:34:35 +01:00
Jannis Harder b08a880704 backends/rtlil: Do not shorten a value with z bits to 'x 2023-01-29 14:02:25 +01:00
Miodrag Milanović 8180cc4325
Merge pull request #3624 from jix/sim_yw
Changes to support SBY trace generation with the sim command
2023-01-23 16:55:17 +01:00
Miodrag Milanovic 6574553189 Fixes for some of clang scan-build detected issues 2023-01-17 12:58:08 +01:00
Jannis Harder d6c7aa0e3d sim/formalff: Clock handling for yw cosim 2023-01-11 18:07:16 +01:00
Jannis Harder 7ddec5093f sim: Improvements and fixes for yw cosim
* Fixed $cover handling
  * Improved sparse memory handling when writing traces
  * JSON summary output
2023-01-11 18:07:16 +01:00
Jannis Harder 636b9f2705 Support for BTOR witness to Yosys witness conversion 2023-01-11 18:07:16 +01:00
Jannis Harder 3e25e61778 aiger: Use new JSON code for writing aiger witness map files 2023-01-11 18:07:16 +01:00
Jannis Harder 673ad561b8 smt2: Treat bweqx as xnor
Without x-bits they are equivalent
2023-01-11 18:07:16 +01:00
Jannis Harder 62afe61779 smt2: Directly implement bwmux instead of using bwmuxmap 2023-01-11 18:07:16 +01:00
Jannis Harder be752a20dc Add bwmuxmap pass 2022-11-30 18:50:53 +01:00
Jannis Harder f2c531e65f verilog_backend: Do not run bmuxmap or demuxmap in -noexpr mode. 2022-11-30 18:24:35 +01:00
Jannis Harder 82b630a246 verilog_backend: Correctly sign extend output of signed `$modfloor` 2022-11-30 18:24:35 +01:00
Jannis Harder 5cb7d0fe9d verilog_backend: Add -noparallelcase option 2022-11-30 18:24:35 +01:00
Emil J 15d41041d8
Merge branch 'YosysHQ:master' into master 2022-11-08 22:02:23 +01:00
Emil J 6936394eed
Merge branch 'YosysHQ:master' into master 2022-10-20 19:36:03 +02:00
Emil Jiří Tywoniak 2ba435b6bc bugfix for mathsat counterexample vcd dump 2022-10-20 19:31:16 +02:00
Jannis Harder 96029400cb smtbmc: Do not assume skipped assertions when loading a witness trace
This is not valid when the prefix of a trace already violates
assertions. This can happen when the trace generating solver doesn't
look for a minimal length counterexample.
2022-10-20 13:49:47 +02:00
Emil J 8859d801c8
Temporal induction counterexample loop detection (#3504)
I have added an optional flag to smtbmc that causes failed temporal induction counterexample traces to be checked for duplicate states and reported to the user, since loops in the counterexample mean that increasing the induction depth won't help prove a design's safety properties.
2022-10-19 12:20:12 +02:00
Emil Jiří Tywoniak 083ca6ab06 bugfix 2022-10-18 22:58:54 +02:00
Jannis Harder 8838b1eaa4 smtbmc: Fix witness handling for k-induction failures
The "uninitialized" value is a _list_ of chunks that are part of the
initial state for the witness trace.
2022-10-18 19:51:36 +02:00
Jannis Harder 4d334fd3e3 smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
The witness metadata was missing fine grained FFs completely and for
coarse grained FFs where the output connection has multiple chunks it
lacked the offset of the chunk within the SMT expression. This fixes
both, the later by adding an "smtoffset" field to the metadata.
2022-10-12 19:48:36 +02:00
Emil Jiří Tywoniak 8d4000a9b7 include memory in state 2022-10-11 19:52:44 +02:00
Emil Jiří Tywoniak 0dbebea939 include memory in state 2022-10-11 19:48:16 +02:00
Aki Van Ness 7a73133c9f
backends: protobuf: removed protobuf backend 2022-10-10 10:41:11 -04:00
Emil Jiří Tywoniak 3e816e9922 experimental temporal induction counterexample loop detection 2022-10-09 18:24:43 +02:00
Jannis Harder 1d40f5e8fa smtbmc: Avoid unnecessary string copies when parsing solver output 2022-09-02 22:37:08 +02:00
KrystalDelusion 9465b2af95 Fitting help messages to 80 character width
Uses the regex below to search (using vscode):
	^\t\tlog\("(.{10,}(?<!\\n)|.{81,}\\n)"\);

Finds any log messages double indented (which help messages are)
and checks if *either* there are is no newline character at the end,
*or* the number of characters before the newline is more than 80.
2022-08-24 10:40:57 +12:00
Jannis Harder 5142fb3b5c write_aiger: Fix non-$_FF_ FFs
This broke while switching sby's formal flows to always use $_FF_'s.
2022-08-18 13:56:22 +02:00
Jannis Harder 66f761a8c5 smtbmc: Set step range for --yw and dont skip steps for --check-witness 2022-08-16 13:37:30 +02:00
Jannis Harder b156fe903f yosys-witness: Add stats command 2022-08-16 13:37:30 +02:00
Jannis Harder 475267ac25 smtbmc: Add --check-witness mode
This verifies that the given constraints force an assertion failure.
This is useful to debug witness trace conversion (and minimization).
2022-08-16 13:37:30 +02:00
Jannis Harder efd5b86eb9 aiger: Add yosys-witness support
Adds a new json based aiger map file and yosys-witness converters to us
this to convert between native and AIGER witness files.
2022-08-16 13:37:30 +02:00
Jannis Harder f041e36c6e smtbmc: Add native json based witness format + smt2 backend support
This adds a native json based witness trace format. By having a common
format that includes everything we support, and providing a conversion
utility (yosys-witness) we no longer need to implement every format for
every tool that deals with witness traces, avoiding a quadratic
opportunity to introduce subtle bugs.

Included:

  * smt2: New yosys-smt2-witness info lines containing full hierarchical
    paths without lossy escaping.
  * yosys-smtbmc --dump-yw trace.yw: Dump results in the new format.
  * yosys-smtbmc --yw trace.yw: Read new format as constraints.
  * yosys-witness: New tool to convert witness formats.
    Currently this can only display traces in a human-readable-only
    format and do a passthrough read/write of the new format.
  * ywio.py: Small python lib for reading and writing the new format.
    Used by yosys-smtbmc and yosys-witness to avoid duplication.
2022-08-16 13:37:30 +02:00
Jannis Harder 96a1173598 btor: Support $anyinit cells 2022-08-16 13:37:30 +02:00
Jannis Harder 5893cae647 aiger: Support $anyinit cells 2022-08-16 13:37:30 +02:00
Jannis Harder 021c3c8da5 smt2: Support $anyinit cells 2022-08-16 13:37:30 +02:00
Jannis Harder a5e1d3b997 formalff: Set new replaced_by_gclk attribute on removed dff's clks
This attribute can be used by formal backends to indicate which clocks
were mapped to the global clock. Update the btor and smt2 backend which
already handle clock inputs to understand this attribute.
2022-08-16 13:37:30 +02:00
Miodrag Milanovic 4444d5cf68 Switched to utf-8 in smtio.py 2022-08-09 12:54:48 +02:00
Miodrag Milanovic 99f1c71582 properly encode string in rtlil 2022-08-09 12:45:32 +02:00
Miodrag Milanović 3705d8414e
Merge pull request #3432 from YosysHQ/aki/jny_updates
jny: Added JNY schema and additional information to JNY output file
2022-08-03 13:33:10 +02:00
Jannis Harder 6af5e74f95 smt2: Fix $shift/$shiftx with negative shift ammounts
Fixes #3431, fixes #3344
2022-08-02 20:16:41 +02:00
Aki Van Ness 4f0ee383c9
backend: jny: updated the `JnyWriter` to emite a new "invocation" entry as well as a "$schema" entry to point to the location the schema will be at 2022-08-02 06:58:41 -04:00
Michael Nolan 24b895778a Add support for GHDL modfloor operator 2022-07-05 15:15:54 -04:00
Jannis Harder 930bcf0e75 smt2, btor: Revert calling memory_map -rom-only
This approach had major issues with ROMs whose initialization was not
fully defined. If required, memory_map -rom-only -keepdc should be
called early in a formal flow instead. (This does require a careful
choice of optimization passes though. Sby's scripts will be updated
accordingly.)
2022-06-29 18:28:34 +02:00
Jannis Harder d78d807a7f memory_map: -keepdc option for formal
Use it when invoking memory_map -rom-only from write_{smt2,btor}.
2022-06-27 15:47:55 +02:00
Kevin Läufer de5c4bf523 btor: add support for $pos cell 2022-06-20 16:40:46 -07:00
Jannis Harder 4adef63cd4 smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction
This avoids provability regressions now that we infer more ROMs.

This fixes #3378
2022-06-17 17:23:13 +02:00
Jannis Harder 0c5f62f6ff smtbmc: noincr: keep solver running for post check-sat unrolling 2022-06-08 13:20:25 +02:00
Jannis Harder 6db2948938
Merge pull request #3357 from jix/smtbmc-cvc5
smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
2022-06-08 12:52:51 +02:00
Jannis Harder ac22f1764d smt2: emit smtlib2_comb_expr outputs after all inputs 2022-06-07 19:06:45 +02:00
Jannis Harder 5f9a97d234
Merge pull request #3319 from programmerjake/smtlib2-expr-support
add smtlib2_comb_expr
2022-06-07 16:47:10 +02:00
Jannis Harder ab9e887dee smtbmc: Force nonincremental mode when yices is used with forall 2022-06-03 16:45:23 +02:00
Jannis Harder 0207d7b0cf smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5 2022-06-03 16:24:09 +02:00
Jacob Lifshay cd57c5adb3 smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions 2022-06-02 22:37:29 -07:00
Miodrag Milanovic 7ee570a75e Use proper operator 2022-05-27 10:23:34 +02:00
Jacob Lifshay d53479a0d6 add $divfloor support to write_smt2
Fixes: #3330
2022-05-24 01:34:25 -07:00
Claire Xenia Wolf 3fb32540ea Add propagated clock signals into btor info file 2022-05-04 08:10:18 +02:00
Jannis Harder c7ef0f2932 smt2: Make write port array stores conditional on nonzero write mask 2022-04-20 17:49:48 +02:00