Commit Graph

1448 Commits

Author SHA1 Message Date
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
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
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
Aki Van Ness 7a73133c9f
backends: protobuf: removed protobuf backend 2022-10-10 10:41:11 -04: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
Aki Van Ness 1f1a403cce pass jny: flipped the defaults for the inclusion of various bits of metadata 2022-04-08 08:05:15 +02:00
Aki Van Ness 6053856f91 pass jny: ensured the cell collection is cleared between modules 2022-04-08 08:05:15 +02:00
Aki Van Ness 5a016713cc pass jny: fixed missing quotes around the type value for the cell sort 2022-04-08 08:05:15 +02:00
Aki Van Ness 2e792857e9 pass jny: fixed the backslash escape for strings 2022-04-08 08:05:15 +02:00
Aki Van Ness cae5ea8337 pass jny: removed the invalid json escapes 2022-04-08 08:05:15 +02:00
Aki Van Ness dccc89e8b3 pass jny: added some todo comments about things that need to be done before a proper merge, but it should be enough for the PoC at the moment 2022-04-08 08:05:15 +02:00
Aki Van Ness 1be9bef28b pass jny: changed the constructor initializers to use parens rather than curly-braces to hopefully make GCC 4.8 happy 2022-04-08 08:05:15 +02:00
Aki Van Ness 43b2fc5566 pass jny: fixed the string escape method to be less jank and more proper 2022-04-08 08:05:15 +02:00
Aki Van Ness 52ea944012 pass jny: fixed the signed output for param value output 2022-04-08 08:05:15 +02:00
Aki Van Ness 58e2870261 pass jny: added connection output 2022-04-08 08:05:15 +02:00
Aki Van Ness 167206f2f5 pass jny: added filter options for including connections, attributes, and properties 2022-04-08 08:05:15 +02:00
Aki Van Ness 587f31b9a3 pass jny: large chunk of refactoring to make the JSON output more pretty and the internals less of a spaghetti nightmare 2022-04-08 08:05:15 +02:00
Aki Van Ness 0e20619189 metadata -> jny: migrated to the proper name for the pass 2022-04-08 08:05:15 +02:00
Aki Van Ness bdf14557ca pass metadata: added the machinery to write param and attributes 2022-04-08 08:05:15 +02:00
Aki Van Ness 1876ed21e7 pass metadata: removed superfluous `stringf` calls 2022-04-08 08:05:15 +02:00
Aki Van Ness ca03fbdc6d pass metadata: some more rough work on dumping the parameters and attributes 2022-04-08 08:05:15 +02:00
Aki Van Ness 6a90b42c48 pass metadata: fixed the MetadataWriter object initializer so GCC 4.8 is happy 2022-04-08 08:05:15 +02:00
Aki Van Ness 7a275567df pass metadata: added the output of parameters,
it's kinda dumb at the moment and needs parsing based on type but it's a start
2022-04-08 08:05:15 +02:00
Aki Van Ness d8b85e1247 pass metadata: fixed some of the output formatting 2022-04-08 08:05:15 +02:00
Aki Van Ness f6bb238051 pass metadata: initial commit of the metadata pass for exporting design metadata for yosys assisted tooling 2022-04-08 08:05:15 +02:00
Jannis Harder 8b15f3a548 smtbmc: fix bmc with no assertions
this was broken by the `--keep-going` changes
2022-03-29 20:41:50 +02:00
Jannis Harder 8cc8c5efde
Merge pull request #3253 from jix/smtbmc-nodeepcopy
smtbmc: Avoid unnecessary deep copies during unrolling
2022-03-28 16:59:26 +02:00
Jannis Harder 17e2a3048c
Merge pull request #3247 from jix/smtbmc-keepgoing
smtbmc `--keep-going`
2022-03-28 16:58:41 +02:00
Jannis Harder d25daa6203 smtbmc: Avoid unnecessary deep copies during unrolling 2022-03-28 13:03:48 +02:00
Miodrag Milanovic 4fd8b38d7a Add -no-startoffset option to write_aiger 2022-03-25 08:44:45 +01:00
Jannis Harder 5e4d804e53 yosys-smtbmc: Option to keep going after failed assertions in BMC mode 2022-03-24 16:01:14 +01:00
Jannis Harder e43ebf8527 yosys-smtbmc: Fix typo in help text, remove trailing whitespace 2022-03-24 16:01:14 +01:00
N. Engelhardt a7ee01065a ignore # comment lines 2022-03-24 10:19:17 +01:00
Miodrag Milanović 2f44683f4f
Merge pull request #3226 from YosysHQ/micko/btor2witness
Sim support for btor2 witness files
2022-03-11 15:29:34 +01:00
Claire Xenia Wolf d340f302f6 Fix handling of some formal cells in btor back-end
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-03-11 14:21:12 +01:00
Miodrag Milanovic ebe2ee431e handle state names of $anyconst and $anyseq 2022-03-11 14:04:02 +01:00
Miodrag Milanović 4ccc2adbda
Merge pull request #3210 from rqou/json-signed
json: Add help message for `signed` field
2022-03-07 09:41:25 +01:00
Miodrag Milanović a95e5d505b
Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_id
add argument for printing cell names in yosys-smtbmc
2022-03-04 16:39:12 +01:00
Miodrag Milanović c3124023e4
Merge pull request #3207 from nakengelhardt/json_escape_quotes
fix handling of escaped chars in json backend and frontend (mostly)
2022-03-04 13:57:32 +01:00
N. Engelhardt dc739362c7 print cell name for properties in yosys-smtbmc 2022-02-22 17:00:10 +01:00
R 2d3a337795 json: Add help message for `signed` field 2022-02-21 21:59:25 -08:00
N. Engelhardt 8fd1b06249 fix handling of escaped chars in json backend and frontend 2022-02-18 17:13:09 +01:00
Claire Xenia Wolf 30eb7f8665 Add a bit of flexibilty re trace length when processing aiger witnesses in smtbmc.py
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-02-11 17:24:49 +01:00
Marcelina Kościelnicka 56e7791760 verilog backend: Emit a `wire` for ports as well.
Fixes #3177.
2022-01-31 01:08:41 +01:00
Marcelina Kościelnicka 93508d58da Add $bmux and $demux cells. 2022-01-28 23:34:41 +01:00
Catherine fc049e84a9 cxxrtl: don't reset elided wires with \init attribute. 2021-12-25 01:06:10 +00:00
Catherine 7f2ea7d222 cxxrtl: demote wires not inlinable only in debug_eval to locals.
Fixes #3112.

Co-authored-by: Irides <irides@irides.network>
2021-12-15 09:14:33 +00:00
Marcelina Kościelnicka 0aad88a2fb Add clean_zerowidth pass, use it for Verilog output.
This should remove instances of zero-width sigspecs in the netlist,
avoiding problems in the Verilog backend with emitting them.

See #3103.
2021-12-12 19:56:50 +01:00
Catherine bdc6ba019c
Merge pull request #3105 from whitequark/cxxrtl-reset-memories-2
cxxrtl: preserve interior memory pointers across reset
2021-12-12 01:23:03 +00:00
Marcelina Kościelnicka d019b4e681 rtlil: Dump empty connections when whole module is selected.
Without this, empty connections will be always skipped by `dump`, since
they contain no selected wires.  This makes debugging rather confusing.
2021-12-12 01:22:06 +01:00
Catherine 55c9fb3b18 cxxrtl: preserve interior memory pointers across reset.
Before this commit, values, wires, and memories with an initializer
were value-initialized in emitted C++ code. After this commit, all
values, wires, and memories are default-initialized, and the default
constructor of generated modules calls the reset() method, which
assigns the members that have an initializer.
2021-12-11 16:40:06 +00:00
whitequark 7c9e498662 cxxrtl: use unique_ptr<value<>[]> to store memory contents.
This makes the depth properly immutable.
2021-12-11 14:52:37 +00:00
whitequark 86f2804dc3 write_verilog: dump zero width sigspecs correctly.
Before this commit, zero width sigspecs were dumped as "" (empty
string). Unfortunately, 1364-2005 5.2.3.3 indicates that an empty
string is equivalent to "\0", and is 8 bits wide, so that's wrong.

After this commit, a replication operation with a count of zero is
used instead, which is explicitly permitted per 1364-2005 5.1.14,
and is defined to have size zero. (Its operand has to have a non-zero
size for it to be legal, though.)

PR #1203 has addressed this issue before, but in an incomplete way.
2021-12-11 12:01:52 +00:00
Lofty 77327b2544 sta: very crude static timing analysis pass
Co-authored-by: Eddie Hung <eddie@fpgeh.com>
2021-11-25 17:20:27 +01:00
Miodrag Milanovic c081c683a4 Give initial wire unique ID, fixes #2914 2021-11-17 12:19:06 +01:00
Miodrag Milanovic ff8e999a71 Split module ports, 20 per line 2021-10-09 13:40:55 +02:00
Marcelina Kościelnicka e7d89e653c Hook up $aldff support in various passes. 2021-10-02 21:01:21 +02:00
Marcelina Kościelnicka 63b9df8693 kernel/ff: Refactor FfData to enable FFs with async load.
- *_en is split into *_ce (clock enable) and *_aload (async load aka
  latch gate enable), so both can be present at once
- has_d is removed
- has_gclk is added (to have a clear marker for $ff)
- d_is_const and val_d leftovers are removed
- async2sync, clk2fflogic, opt_dff are updated to operate correctly on
  FFs with async load
2021-10-02 20:19:48 +02:00
Claire Xenia Wolf 89df26e4bc Add optimization to rtlil back-end for all-x parameter values
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-09-27 16:02:20 +02:00
the6p4c c25122e339 Fix protobuf backend build dependencies
backends/protobuf/protobuf.cc depends on the source and header files
generated by protoc, but this dependency wasn't explicitly declared. Add
a rule to the Makefile to fix intermittent build failures when the
protobuf header/source file isn't built before protobuf.cc.
2021-09-17 13:36:39 +10:00
Marcelina Kościelnicka 33749f1e3a yosys-smtbmc: Fix reused loop variable.
Fixes #2999.
2021-09-10 13:34:58 +02:00
Marcelina Kościelnicka e6f3d1c225 kernel/mem: Introduce transparency masks. 2021-08-11 00:04:16 +02:00
Marcelina Kościelnicka ec2a468bd3 backend/verilog: Add alternate mode for transparent read port output.
This mode will be used whenever read port cannot be handled in the
"extract address register" way, ie. whenever it has enable, reset,
init functionality or (in the future) mixed transparency mask.
2021-08-01 19:11:29 +02:00
Marcelina Kościelnicka e9effd58d2 backends/verilog: Support meminit with mask. 2021-07-28 23:18:38 +02:00
whitequark a04844bdf8
Merge pull request #2885 from whitequark/cxxrtl-fix-2883
cxxrtl: treat wires with multiple defs as not inlinable
2021-07-20 13:12:11 +00:00
whitequark 1a6ddf7892 cxxrtl: treat wires with multiple defs as not inlinable.
Fixes #2883.
2021-07-20 10:30:39 +00:00
whitequark 225af830c1 cxxrtl: treat assignable internal wires used only for debug as locals.
This issue was introduced in commit 4aa65f40 while fixing #2739.

Fixes #2882.
2021-07-20 10:10:42 +00:00
whitequark fc84f23001 cxxrtl: escape colon in variable names in VCD writer.
The following VCD file crashes GTKWave's VCD loader:

    $var wire 1 ! x:1 $end
    $enddefinitions $end

In practice, a colon can be a part of a variable name that is
translated from a Verilog function, something like:

    update$func$.../hdl/hazard3_csr.v:350$2534.$result
2021-07-19 16:22:55 +00:00
whitequark 948fc10d7b cxxrtl: add debug_item::{get,set}.
Fixes #2877.
2021-07-18 06:20:45 +00:00
whitequark 4aa65f406f cxxrtl: treat internal wires used only for debug as constants.
Fixes #2739 (again).
2021-07-17 14:23:57 +00:00
whitequark 2db4137514
Merge pull request #2874 from whitequark/cxxrtl-fix-2589
cxxrtl: run hierarchy pass regardless of (*top*) attribute presence
2021-07-16 11:12:19 +00:00
whitequark efc43270fa
Merge pull request #2873 from whitequark/cxxrtl-fix-2500
cxxrtl: emit debug items for unused public wires
2021-07-16 11:01:10 +00:00
whitequark 5b003d6e5c cxxrtl: run hierarchy pass regardless of (*top*) attribute presence.
The hierarchy pass does a lot more than just finding the top module,
mainly resolving implicit (positional, wildcard) module connections.

Fixes #2589.
2021-07-16 10:27:47 +00:00
whitequark 09218896d6 cxxrtl: emit debug items for unused public wires.
This greatly improves debug information coverage.

Fixes #2500.
2021-07-16 10:14:40 +00:00
whitequark b28ca7f5ac cxxrtl: don't expect user cell inputs to be wires.
Ports can be connected to constants, too. (Usually resets.)

Fixes #2521.
2021-07-16 09:51:52 +00:00
whitequark 44a3d924ce cxxrtl: don't mark buffered internal wires as UNUSED for debug.
Public wires may alias buffered internal wires, so keep BUFFERED
wires in debug information even if they are private. Debug items are
only created for public wires, so this does not otherwise affect how
debug information is emitted.

Fixes #2540.
Fixes #2841.
2021-07-16 07:54:49 +00:00
whitequark 54b6cb645f cxxrtl: mark dead local wires as unused even with inlining disabled.
Fixes #2739.
2021-07-15 22:27:27 +00:00
Marcelina Kościelnicka 8bf9cb407d kernel/mem: Add a coalesce_inits helper.
While this helper is already useful to squash sequential initializations
into one in cxxrtl, its main purpose is to squash overlapping masked memory
initializations (when they land) and avoid having to deal with them in
cxxrtl runtime.
2021-07-13 15:59:11 +02:00
GCHQDeveloper560 4379375d89 Add support for the Bitwuzla solver 2021-07-12 22:07:58 +02:00
Marcelina Kościelnicka 37506d737c cxxrtl: Support memory writes in processes. 2021-07-12 18:27:48 +02:00
Marcelina Kościelnicka af7fa62251 cxxrtl: Add support for memory read port reset. 2021-07-12 18:27:48 +02:00
Marcelina Kościelnicka be5cf29699 cxxrtl: Add support for mem read port initial data. 2021-07-12 18:27:48 +02:00
Marcelina Kościelnicka d5c9595668 cxxrtl: Convert to Mem helpers.
This *only* does conversion, but doesn't add any new functionality —
support for memory read port init/reset is still upcoming.
2021-07-12 18:27:48 +02:00
Claire Xenia Wolf 2d95a7da9c Intersynth URL
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-06-09 12:42:52 +02:00
Claire Xenia Wolf 72787f52fc Fixing old e-mail addresses and deadnames
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g;
2021-06-08 00:39:36 +02:00
Marcelina Kościelnicka cbf6b719fe Make a few passes auto-call Mem::narrow instead of rejecting wide ports.
This essentially adds wide port support for free in passes that don't
have a usefully better way of handling wide ports than just breaking
them up to narrow ports, avoiding "please run memory_narrow" annoyance.
2021-05-28 00:40:56 +02:00
Marcelina Kościelnicka 055ba748bc backends/verilog: Add support for memory read port reset and init value. 2021-05-27 23:47:42 +02:00
Marcelina Kościelnicka aabe1c382e backends/verilog: Add wide port support. 2021-05-27 16:15:46 +02:00
Marcelina Kościelnicka 64ba3c3842 backends/verilog: Try to preserve mem write port priorities. 2021-05-26 00:19:31 +02:00
Marcelina Kościelnicka 69bf5c81c7 Reject wide ports in some passes that will never support them. 2021-05-25 02:07:25 +02:00
Marcelina Kościelnicka b6721aa9d8 backend/firrtl: Convert to use Mem helpers. 2021-05-24 14:00:33 +02:00
Marcelina Kościelnicka 33513d923a btor: Use is_mem_cell in one more place. 2021-05-23 20:34:52 +02:00
Marcelina Kościelnicka c4cc888b2c kernel/rtlil: Extract some helpers for checking memory cell types.
There will soon be more (versioned) memory cells, so handle passes that
only care if a cell is memory-related by a simple helper call instead of
a hardcoded list.
2021-05-22 21:43:00 +02:00
Eddie Hung 55dc5a4e4f
abc9: fix SCC issues (#2694)
* xilinx: add SCC test for DSP48E1

* xilinx: Gate DSP48E1 being a whitebox behind ALLOW_WHITEBOX_DSP48E1

Have a test that checks it works through ABC9 when enabled

* abc9 to break SCCs using $__ABC9_SCC_BREAKER module

* Add test

* abc9_ops: remove refs to (* abc9_keep *) on wires

* abc9_ops: do not bypass cells in an SCC

* Add myself to CODEOWNERS for abc9*

* Fix compile

* abc9_ops: run -prep_hier before scc

* Fix tests

* Remove bug reference pending fix

* abc9: fix for -prep_hier -dff

* xaiger: restore PI handling

* abc9_ops: -prep_xaiger sigmap

* abc9_ops: -mark_scc -> -break_scc

* abc9: eliminate hard-coded abc9.box from tests

Also tidy up

* Address review
2021-03-29 22:01:57 -07:00
Marcelina Kościelnicka 192601385f rtlil: Fix process memwr roundtrip.
Fixes #2646 fallout.
2021-03-23 19:49:47 +01:00
Marcelina Kościelnicka 6b2100bf01 json: Improve the "processes in module" message a bit. 2021-03-23 15:53:49 +01:00
Marcelina Kościelnicka 3d9698153f json: Add support for memories.
Previously, memories were silently discarded by the JSON backend, making
round-tripping modules with them crash.

Since there are already some users using JSON to implement custom
external passes that use memories (and infer width/size from memory
ports), let's fix this by just making JSON backend and frontend support
memories as first-class objects.

Processes are still not supported, and will now cause a hard error.

Fixes #1908.
2021-03-15 17:19:19 +01:00
whitequark feff32914b
Merge pull request #2642 from whitequark/cxxrtl-noproc-fixes
CXXRTL: some -noproc fixes
2021-03-11 20:01:10 +00:00
Dan Ravensloft 83fc5cc28b Replace assert in xaiger with more useful error message 2021-03-10 22:35:06 +01:00
Marcelina Kościelnicka 4e03865d5b Add support for memory writes in processes. 2021-03-08 20:16:29 +01:00
whitequark ab76d9cec5 cxxrtl: don't assert on edge sync rules tied to a constant.
These are commonly the result of tying an async reset to an inactive
level.
2021-03-07 14:29:30 +00:00
whitequark d1de08e38a cxxrtl: allow `always` sync rules in debug_eval.
These can be produced from `always @*` processes, if `-noproc`
is used.
2021-03-07 14:28:45 +00:00