62afe61779
smt2: Directly implement bwmux instead of using bwmuxmap
2023-01-11 18:07:16 +01:00
be752a20dc
Add bwmuxmap pass
2022-11-30 18:50:53 +01:00
f2c531e65f
verilog_backend: Do not run bmuxmap or demuxmap in -noexpr mode.
2022-11-30 18:24:35 +01:00
82b630a246
verilog_backend: Correctly sign extend output of signed `$modfloor`
2022-11-30 18:24:35 +01:00
5cb7d0fe9d
verilog_backend: Add -noparallelcase option
2022-11-30 18:24:35 +01:00
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
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
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
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
7a73133c9f
backends: protobuf: removed protobuf backend
2022-10-10 10:41:11 -04:00
1d40f5e8fa
smtbmc: Avoid unnecessary string copies when parsing solver output
2022-09-02 22:37:08 +02:00
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
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
66f761a8c5
smtbmc: Set step range for --yw and dont skip steps for --check-witness
2022-08-16 13:37:30 +02:00
b156fe903f
yosys-witness: Add stats command
2022-08-16 13:37:30 +02:00
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
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
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
96a1173598
btor: Support $anyinit cells
2022-08-16 13:37:30 +02:00
5893cae647
aiger: Support $anyinit cells
2022-08-16 13:37:30 +02:00
021c3c8da5
smt2: Support $anyinit cells
2022-08-16 13:37:30 +02:00
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
4444d5cf68
Switched to utf-8 in smtio.py
2022-08-09 12:54:48 +02:00
99f1c71582
properly encode string in rtlil
2022-08-09 12:45:32 +02:00
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
6af5e74f95
smt2: Fix $shift/$shiftx with negative shift ammounts
...
Fixes #3431 , fixes #3344
2022-08-02 20:16:41 +02:00
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
24b895778a
Add support for GHDL modfloor operator
2022-07-05 15:15:54 -04:00
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
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
de5c4bf523
btor: add support for $pos cell
2022-06-20 16:40:46 -07:00
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
0c5f62f6ff
smtbmc: noincr: keep solver running for post check-sat unrolling
2022-06-08 13:20:25 +02:00
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
ac22f1764d
smt2: emit smtlib2_comb_expr outputs after all inputs
2022-06-07 19:06:45 +02:00
5f9a97d234
Merge pull request #3319 from programmerjake/smtlib2-expr-support
...
add smtlib2_comb_expr
2022-06-07 16:47:10 +02:00
ab9e887dee
smtbmc: Force nonincremental mode when yices is used with forall
2022-06-03 16:45:23 +02:00
0207d7b0cf
smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
2022-06-03 16:24:09 +02:00
cd57c5adb3
smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions
2022-06-02 22:37:29 -07:00
7ee570a75e
Use proper operator
2022-05-27 10:23:34 +02:00
d53479a0d6
add $divfloor support to write_smt2
...
Fixes : #3330
2022-05-24 01:34:25 -07:00
3fb32540ea
Add propagated clock signals into btor info file
2022-05-04 08:10:18 +02:00
c7ef0f2932
smt2: Make write port array stores conditional on nonzero write mask
2022-04-20 17:49:48 +02:00
1f1a403cce
pass jny: flipped the defaults for the inclusion of various bits of metadata
2022-04-08 08:05:15 +02:00
6053856f91
pass jny: ensured the cell collection is cleared between modules
2022-04-08 08:05:15 +02:00
5a016713cc
pass jny: fixed missing quotes around the type value for the cell sort
2022-04-08 08:05:15 +02:00
2e792857e9
pass jny: fixed the backslash escape for strings
2022-04-08 08:05:15 +02:00
cae5ea8337
pass jny: removed the invalid json escapes
2022-04-08 08:05:15 +02:00
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
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
43b2fc5566
pass jny: fixed the string escape method to be less jank and more proper
2022-04-08 08:05:15 +02:00
52ea944012
pass jny: fixed the signed output for param value output
2022-04-08 08:05:15 +02:00
58e2870261
pass jny: added connection output
2022-04-08 08:05:15 +02:00
167206f2f5
pass jny: added filter options for including connections, attributes, and properties
2022-04-08 08:05:15 +02:00
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
0e20619189
metadata -> jny: migrated to the proper name for the pass
2022-04-08 08:05:15 +02:00
bdf14557ca
pass metadata: added the machinery to write param and attributes
2022-04-08 08:05:15 +02:00
1876ed21e7
pass metadata: removed superfluous `stringf` calls
2022-04-08 08:05:15 +02:00
ca03fbdc6d
pass metadata: some more rough work on dumping the parameters and attributes
2022-04-08 08:05:15 +02:00
6a90b42c48
pass metadata: fixed the MetadataWriter object initializer so GCC 4.8 is happy
2022-04-08 08:05:15 +02:00
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
d8b85e1247
pass metadata: fixed some of the output formatting
2022-04-08 08:05:15 +02:00
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
8b15f3a548
smtbmc: fix bmc with no assertions
...
this was broken by the `--keep-going` changes
2022-03-29 20:41:50 +02:00
8cc8c5efde
Merge pull request #3253 from jix/smtbmc-nodeepcopy
...
smtbmc: Avoid unnecessary deep copies during unrolling
2022-03-28 16:59:26 +02:00
17e2a3048c
Merge pull request #3247 from jix/smtbmc-keepgoing
...
smtbmc `--keep-going`
2022-03-28 16:58:41 +02:00
d25daa6203
smtbmc: Avoid unnecessary deep copies during unrolling
2022-03-28 13:03:48 +02:00
4fd8b38d7a
Add -no-startoffset option to write_aiger
2022-03-25 08:44:45 +01:00
5e4d804e53
yosys-smtbmc: Option to keep going after failed assertions in BMC mode
2022-03-24 16:01:14 +01:00
e43ebf8527
yosys-smtbmc: Fix typo in help text, remove trailing whitespace
2022-03-24 16:01:14 +01:00
a7ee01065a
ignore # comment lines
2022-03-24 10:19:17 +01:00
2f44683f4f
Merge pull request #3226 from YosysHQ/micko/btor2witness
...
Sim support for btor2 witness files
2022-03-11 15:29:34 +01:00
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
ebe2ee431e
handle state names of $anyconst and $anyseq
2022-03-11 14:04:02 +01:00
4ccc2adbda
Merge pull request #3210 from rqou/json-signed
...
json: Add help message for `signed` field
2022-03-07 09:41:25 +01:00
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
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
dc739362c7
print cell name for properties in yosys-smtbmc
2022-02-22 17:00:10 +01:00
2d3a337795
json: Add help message for `signed` field
2022-02-21 21:59:25 -08:00
8fd1b06249
fix handling of escaped chars in json backend and frontend
2022-02-18 17:13:09 +01:00
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
56e7791760
verilog backend: Emit a `wire` for ports as well.
...
Fixes #3177 .
2022-01-31 01:08:41 +01:00
93508d58da
Add $bmux and $demux cells.
2022-01-28 23:34:41 +01:00
fc049e84a9
cxxrtl: don't reset elided wires with \init attribute.
2021-12-25 01:06:10 +00:00
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
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
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
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
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
7c9e498662
cxxrtl: use unique_ptr<value<>[]> to store memory contents.
...
This makes the depth properly immutable.
2021-12-11 14:52:37 +00:00
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
77327b2544
sta: very crude static timing analysis pass
...
Co-authored-by: Eddie Hung <eddie@fpgeh.com>
2021-11-25 17:20:27 +01:00
c081c683a4
Give initial wire unique ID, fixes #2914
2021-11-17 12:19:06 +01:00
ff8e999a71
Split module ports, 20 per line
2021-10-09 13:40:55 +02:00
e7d89e653c
Hook up $aldff support in various passes.
2021-10-02 21:01:21 +02:00
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
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
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
33749f1e3a
yosys-smtbmc: Fix reused loop variable.
...
Fixes #2999 .
2021-09-10 13:34:58 +02:00
e6f3d1c225
kernel/mem: Introduce transparency masks.
2021-08-11 00:04:16 +02:00
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
e9effd58d2
backends/verilog: Support meminit with mask.
2021-07-28 23:18:38 +02:00
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
1a6ddf7892
cxxrtl: treat wires with multiple defs as not inlinable.
...
Fixes #2883 .
2021-07-20 10:30:39 +00:00
225af830c1
cxxrtl: treat assignable internal wires used only for debug as locals.
...
This issue was introduced in commit 4aa65f40#2739 .
Fixes #2882 .
2021-07-20 10:10:42 +00:00
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
948fc10d7b
cxxrtl: add debug_item::{get,set}.
...
Fixes #2877 .
2021-07-18 06:20:45 +00:00
4aa65f406f
cxxrtl: treat internal wires used only for debug as constants.
...
Fixes #2739 (again).
2021-07-17 14:23:57 +00:00
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
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
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
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
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
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
54b6cb645f
cxxrtl: mark dead local wires as unused even with inlining disabled.
...
Fixes #2739 .
2021-07-15 22:27:27 +00:00
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
4379375d89
Add support for the Bitwuzla solver
2021-07-12 22:07:58 +02:00
37506d737c
cxxrtl: Support memory writes in processes.
2021-07-12 18:27:48 +02:00
af7fa62251
cxxrtl: Add support for memory read port reset.
2021-07-12 18:27:48 +02:00
be5cf29699
cxxrtl: Add support for mem read port initial data.
2021-07-12 18:27:48 +02:00
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
2d95a7da9c
Intersynth URL
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-06-09 12:42:52 +02:00
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
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
055ba748bc
backends/verilog: Add support for memory read port reset and init value.
2021-05-27 23:47:42 +02:00
aabe1c382e
backends/verilog: Add wide port support.
2021-05-27 16:15:46 +02:00
64ba3c3842
backends/verilog: Try to preserve mem write port priorities.
2021-05-26 00:19:31 +02:00
69bf5c81c7
Reject wide ports in some passes that will never support them.
2021-05-25 02:07:25 +02:00
b6721aa9d8
backend/firrtl: Convert to use Mem helpers.
2021-05-24 14:00:33 +02:00
33513d923a
btor: Use is_mem_cell in one more place.
2021-05-23 20:34:52 +02:00
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
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
192601385f
rtlil: Fix process memwr roundtrip.
...
Fixes #2646 fallout.
2021-03-23 19:49:47 +01:00
6b2100bf01
json: Improve the "processes in module" message a bit.
2021-03-23 15:53:49 +01:00
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
feff32914b
Merge pull request #2642 from whitequark/cxxrtl-noproc-fixes
...
CXXRTL: some -noproc fixes
2021-03-11 20:01:10 +00:00
83fc5cc28b
Replace assert in xaiger with more useful error message
2021-03-10 22:35:06 +01:00
4e03865d5b
Add support for memory writes in processes.
2021-03-08 20:16:29 +01:00
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
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
9dd813374e
Merge pull request #2635 from whitequark/cxxrtl-memrd-async-addr
...
cxxrtl: follow aliases to outlines when emitting $memrd.ADDR
2021-03-05 05:30:19 -08:00
06da2e0f18
Merge pull request #2634 from whitequark/cxxrtl-debug-wire-types
...
cxxrtl: add pass debug flag to show assigned wire types
2021-03-05 04:57:22 -08:00
14ce8bdaa6
cxxrtl: follow aliases to outlines when emitting $memrd.ADDR.
2021-03-05 12:09:02 +00:00
8471808834
cxxrtl: add pass debug flag to show assigned wire types.
...
Refs #2543 .
2021-03-05 11:58:59 +00:00
a9a873a1d2
cxxrtl: don't crash on empty designs.
2021-03-05 11:05:19 +00:00
979347999f
btor, smt2, smv: Add a hint on how to deal with funny FF types.
2021-02-25 22:04:04 +01:00
a77fa6709b
Merge pull request #2563 from whitequark/cxxrtl-msvc
...
cxxrtl: do not use `->template` for non-dependent names
2021-01-26 21:55:12 +00:00
4b6e764c46
cxxrtl: do not use `->template` for non-dependent names.
...
This breaks build on MSVC but not GCC/Clang.
2021-01-26 18:09:53 +00:00
c8415884d1
Improves the previous commit with a more complete coverage of the cases
2021-01-15 13:59:20 -06:00
86607d0fdc
Handle sliced bits as clock inputs ( fixes #2542 )
2021-01-14 16:36:21 -06:00
Jannis Harder
Emil J
Aki Van Ness
KrystalDelusion
Miodrag Milanovic
Michael Nolan
Kevin Läufer
Jacob Lifshay
Claire Xenia Wolf
N. Engelhardt
Claire Xenia Wolf
R
Marcelina Kościelnicka
Catherine
Lofty
the6p4c
GCHQDeveloper560
Eddie Hung
Iris Johnson