Commit Graph

1153 Commits

Author SHA1 Message Date
Marcelina Kościelnicka 2d340cd355 btor: Use Mem helper. 2020-10-21 17:51:20 +02:00
Marcelina Kościelnicka f272c8b407 smt2: Use Mem helper. 2020-10-21 17:51:20 +02:00
Marcelina Kościelnicka ec483b7c3b verilog_backend: Use Mem helper. 2020-10-21 17:51:20 +02:00
Jakob Wenzel 54166ae0c5 smtbmc: escape identifiers in verilog testbench 2020-10-06 11:27:14 +02:00
N. Engelhardt 8f1d53e66f write_verilog: emit intermediate wire for constant values in sensitivity list 2020-09-28 18:11:18 +02:00
N. Engelhardt ed5790382a
Merge pull request #2372 from nakengelhardt/name_is_public
add IdString::isPublic()
2020-09-21 15:18:06 +02:00
N. Engelhardt 3238190797 use the new isPublic() in a few places 2020-09-14 12:43:18 +02:00
Miodrag Milanović da3002e580
Merge pull request #2369 from Xiretza/gitignores
Add missing gitignores for test artifacts
2020-09-10 13:37:49 +02:00
whitequark 691418e13a cxxrtl: expose driver kind in debug information.
This can be useful to determine whether the wire should be a part of
a design checkpoint, whether it can be used to override design state,
and whether driving it may cause a conflict.
2020-09-02 18:00:12 +00:00
whitequark c7b2f07edf cxxrtl: improve handling of FFs with async inputs (other than CLK).
Before this commit, the meaning of "sync def" included some flip-flop
cells but not others. There was no actual reason for this; it was
just poorly defined.

After this commit, a "sync def" means that a wire holds design state
because it is connected directly to a flip-flop output, and may never
be unbuffered. This is not affected by presence of async inputs.
2020-09-02 18:00:12 +00:00
whitequark b025ee0aa6 cxxrtl: expose port direction in debug information.
This can be useful to distinguish e.g. a combinatorially driven wire
with type `CXXRTL_VALUE` from a module input with the same type, as
well as general introspection.
2020-09-02 17:19:11 +00:00
whitequark 8d6e5c6391 cxxrtl: fix typo in comment. NFC. 2020-09-02 15:23:49 +00:00
whitequark d880f6eda2 cxxrtl: fix inaccuracy in CXXRTL_ALIAS documentation. NFC.
Nodes driven by a constant value have type CXXRTL_VALUE and their
`next` pointer set to NULL. (This is already documented.)
2020-09-02 15:23:47 +00:00
Xiretza 6224fd9055
Add missing gitignores for test artifacts 2020-08-31 19:43:51 +02:00
whitequark c1fff52477
write_smt2: fix SMT-LIB tutorial URL 2020-08-29 20:02:35 +00:00
whitequark 00e7dec7f5 Replace "ILANG" with "RTLIL" everywhere.
The only difference between "RTLIL" and "ILANG" is that the latter is
the text representation of the former, as opposed to the in-memory
graph representation. This distinction serves no purpose but confuses
people: it is not obvious that the ILANG backend writes RTLIL graphs.

Passes `write_ilang` and `read_ilang` are provided as aliases to
`write_rtlil` and `read_rtlil` for compatibility.
2020-08-26 17:29:32 +00:00
Noah Moroze 91682d189e Ensure smt2 comments are associated with accessors 2020-08-20 16:00:05 -04:00
Xiretza 928fd40c2e Respect \A_SIGNED for $shift
This reflects the behaviour of $shr/$shl, which sign-extend their A
operands to the size of their output, then do a logical shift (shift in
0-bits).
2020-08-18 19:36:24 +02:00
Andy Knowles 5829d16fcd
cxxrtl.h: Fix incorrect CarryOut in alu() 2020-08-12 21:04:34 +02:00
Andy Knowles 1227c3681b cxxrtl.h: Fix incorrect CarryOut in alu when Bits % 32 != 0 && Invert == False 2020-08-12 11:32:57 +02:00
Marcelina Kościelnicka 8fd43515c5 verilog_backend: Add handling for all FF types. 2020-07-30 18:22:36 +02:00
Alberto Gonzalez 42fb75c570
smtio: Emit `mode: start` options before `set-logic` command and any other options after it.
Refer to the SMT-LIB specification, section 4.1.7.  According to the spec, some options can only be specified in `start` mode.  Once the solver sees `set-logic`, it moves to `assert` mode.
2020-07-20 22:09:44 +00:00
Alberto Gonzalez 654864658f
smtio: Add support for parsing `yosys-smt2-solver-option` info statements. 2020-07-20 21:54:56 +00:00
Alberto Gonzalez f037985337
smt2: Add `-solver-option` option. 2020-07-20 21:54:56 +00:00
Claire Wolf a207cb362c Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-07-20 19:35:32 +02:00
clairexen f3d7e9a1df
Merge pull request #2273 from whitequark/write-verilog-always-star-initial
verilog_backend: in non-SV mode, add a trigger for `always @*`
2020-07-16 18:30:50 +02:00
clairexen c49344b262
Merge pull request #2272 from whitequark/write-verilog-sv
verilog_backend: add `-sv` option, make `-o <filename>.sv` work
2020-07-16 18:28:24 +02:00
whitequark 128522f173 verilog_backend: in non-SV mode, add a trigger for `always @*`.
This commit only affects translation of RTLIL processes (for which
there is limited support).

Due to the event-driven nature of Verilog, processes like

    reg x;
    always @*
        x <= 1;

may never execute. This can be fixed in SystemVerilog code by using
`always_comb` instead of `always @*`, but in Verilog-2001 the options
are limited. This commit implements the following workaround:

    reg init = 0;
    reg x;
    always @* begin
        if (init) begin end
        x <= 1;
    end

Fixes #2271.
2020-07-16 11:30:14 +00:00
whitequark d9f680b236 verilog_backend: add `-sv` option, make `-o <filename>.sv` work.
See #2271.
2020-07-16 10:44:08 +00:00
whitequark a5cf000377 cxxrtl: fix typo. NFC. 2020-07-14 16:10:30 +00:00
whitequark 5349a922e4 cxxrtl: expose eval() and commit() via the C API. 2020-07-12 23:34:18 +00:00
whitequark ab59e33b2b cxxrtl: add missing extern "C".
This bug was hidden if a header was generated.
2020-07-09 17:52:52 +00:00
whitequark a746c4b605 cxxrtl: update help text. 2020-06-26 08:30:44 +00:00
clairexen c7d71f436d
Merge pull request #2168 from whitequark/assert-unused-exprs
Use (and ignore) the expression provided to log_assert in NDEBUG builds
2020-06-25 18:21:51 +02:00
Marcelina Kościelnicka cb9a8ad0f2 cxxrtl: Add support for the new FF types. 2020-06-24 02:15:08 +02:00
whitequark 2ffdb74fb1 Use (and ignore) the expression provided to log_assert in NDEBUG builds.
This avoids warnings in NDEBUG builds emitted when a variable is only
used in log_assert, but is always defined.
2020-06-19 15:48:58 +00:00
whitequark ede4b10da8
Merge pull request #2173 from whitequark/use-cxx11-final-override
Use C++11 final/override/[[noreturn]]
2020-06-19 06:15:33 +00:00
whitequark 962a2f3bff cxxrtl: add .get() and .set() accessors on value<> and wire<>.
For several reasons:
  * They're more convenient than accessing .data.
  * They accommodate variably-sized types like size_t transparently.
  * They statically ensure that no out of range conversions happen.

For now these are only provided for unsigned integers, but eventually
they should be provided for signed integers too. (Annoyingly this
affects conversions to/from `char` at the moment.)

Fixes #2127.
2020-06-19 02:31:35 +00:00
whitequark 7191dd16f9 Use C++11 final/override keywords. 2020-06-18 23:34:52 +00:00
whitequark 8344846787
Merge pull request #2167 from whitequark/cxxrtl-fix-ndebug
cxxrtl: don't compute vital values in log_assert()
2020-06-18 16:57:51 +00:00
whitequark 3c4e974d7b cxxrtl: don't compute vital values in log_assert().
This breaks NDEBUG builds.

Fixes #2166.
2020-06-17 19:27:47 +00:00
whitequark c4f20f744b
Merge pull request #2163 from jfng/cxxrtl-blackbox-debuginfo
cxxrtl: restrict the debug info of a blackbox to its ports.
2020-06-17 06:07:41 +00:00
whitequark eaf66037a5
Merge pull request #2160 from whitequark/cxxrtl-fix-warning
cxxrtl: avoid unused variable warning for transparent $memrd ports
2020-06-17 06:06:58 +00:00
Jean-François Nguyen 8d98c3861d cxxrtl: restrict the debug info of a blackbox to its ports. 2020-06-16 15:30:56 +02:00
whitequark 334ec5fa0a
Merge pull request #2159 from MerryMage/cxxrtl-mul
cxxrtl: Implement chunk-wise multiplication
2020-06-15 06:08:17 +00:00
whitequark 8d70f7abf9 cxxrtl: avoid unused variable warning for transparent $memrd ports. NFC. 2020-06-15 06:00:16 +00:00
MerryMage f7ae9b0851 cxxrtl: Implement chunk-wise multiplication 2020-06-15 05:54:57 +01:00
whitequark 9d0f1aa222
Merge pull request #2158 from miek/sshr-sign-extension
cxxrtl: fix sshr sign-extension.
2020-06-15 01:37:05 +00:00
Mike Walters 66a2de2912 cxxrtl: fix sshr sign-extension. 2020-06-15 01:01:49 +01:00
whitequark 971a765155
Merge pull request #2151 from whitequark/cxxrtl-fix-rzext
cxxrtl: fix rzext()
2020-06-13 22:18:35 +00:00