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