d8f2a1fda0
Merge pull request #1922 from whitequark/write_cxxrtl-disconnected-outputs
...
write_cxxrtl: ignore disconnected module ports
2020-04-14 14:37:48 +00:00
7025881a5e
Merge pull request #1921 from whitequark/write_cxxrtl-separate-compilation
...
write_cxxrtl: enable separate compilation
2020-04-14 13:53:52 +00:00
0d0bf9c4a2
write_cxxrtl: ignore disconnected module ports.
...
E.g. port `q` in `submod x(.p(p), .q());`.
Fixes #1920 .
2020-04-14 12:36:20 +00:00
9c64d37a4c
write_verilog: fix precondition check.
2020-04-14 12:12:50 +00:00
102fb5424f
write_cxxrtl: enable separate compilation.
...
This commit makes it possible to use several cxxrtl-generated files
in one application, as well as compiling cxxrtl-generated code as
a separate compilation unit.
2020-04-14 12:07:58 +00:00
0808318d55
xaiger: add check for $__ABC9_DELAY model
2020-04-13 19:11:23 -07:00
0d789c5a3b
Support custom PROGRAM_PREFIX
2020-04-10 10:38:40 +02:00
4737f426ff
write_cxxrtl: add basic documentation.
2020-04-09 04:08:36 +00:00
753e34007d
write_cxxrtl: add support for $dlatch and $dlatchsr cells.
...
Also, fix codegen for $dffe and $adff.
2020-04-09 04:08:36 +00:00
711df56ad0
write_cxxrtl: add support for $sr cell.
...
Also, fix the semantics of SET/CLR inputs of the $dffsr cell, and
fix the scheduling of async FF cells to consider ARST/SET/CLR->Q
as a forward combinatorial arc.
2020-04-09 04:08:36 +00:00
9534b51277
write_cxxrtl: add support for $slice and $concat cells.
2020-04-09 04:08:36 +00:00
01e6850bd3
write_cxxrtl: improve writable memory handling.
...
This commit reduces space and time overhead for writable memories
to O(write port count) in both cases; implements handling for write
port priorities; and simplifies runtime representation of memories.
2020-04-09 04:08:36 +00:00
fb0270b752
write_cxxrtl: add support for hierarchical designs.
...
Hierarchical design simulations are generally much slower, but this
comes with a major increase in flexibility:
1. Since the `flatten` pass currently does not support flattening
of designs with processes, this is the only way to simulate such
designs with cxxrtl.
2. Support for hierarchy paves way for simulation black boxes,
which are necessary for e.g. replacing PHYs with C++ code that
integrates with the host system.
2020-04-09 04:08:36 +00:00
3376dcf37c
write_cxxrtl: avoid undefined behavior on out-of-bounds memory access.
...
After this commit, if NDEBUG is not defined, out-of-bounds accesses
cause assertion failures for reads and writes. If NDEBUG is defined,
out-of-bounds reads return zeroes, and out-of-bounds writes are
ignored.
This commit also adds support for memories that start with a non-zero
index (`Memory::start_offset` in RTLIL).
2020-04-09 04:08:36 +00:00
5157691f0e
write_cxxrtl: statically schedule comb logic and localize wires.
...
This results in further massive gains in performance, modest decrease
in compile time, and, for designs without feedback arcs, makes it
possible to run eval() once per clock edge in certain conditions.
2020-04-09 04:08:36 +00:00
d6d7273421
write_cxxrtl: elide wires for results of comb cells used once.
...
This results in massive gains in performance, equally massive
reduction in compile time, and improved readability.
2020-04-09 04:08:36 +00:00
d20e971725
write_cxxrtl: new backend.
...
This commit adds a basic implementation that isn't very performant
but implements most of the planned features.
2020-04-09 04:08:36 +00:00
956ecd48f7
kernel: big fat patch to use more ID::*, otherwise ID(*)
2020-04-02 09:51:32 -07:00
dde3dfd72e
Update backends/btor/btor.cc; credit @boqwxp
...
Co-Authored-By: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>
2020-04-02 07:14:08 -07:00
fdafb74eb7
kernel: use more ID::*
2020-04-02 07:14:08 -07:00
d1fc4321f0
Merge pull request #1770 from YosysHQ/claire/btor_symbols
...
Improve write_btor symbol handling
2020-04-02 15:38:47 +02:00
104c004e6d
Merge pull request #1765 from YosysHQ/claire/btor_info
...
Add info-file and cover features to write_btor
2020-04-02 15:38:27 +02:00
c23c2c59c1
Update `RTLIL::id2cstr()` usage to `log_id`.
2020-04-01 06:53:28 +00:00
cdb14652be
Clean up pseudo-private member usage in `backends/intersynth/intersynth.cc`.
2020-04-01 06:32:09 +00:00
24ef73904f
Clean up pseudo-private member usage in `backends/blif/blif.cc`.
2020-04-01 05:50:48 +00:00
f657fed24c
Clean up pseudo-private member usage in `backends/verilog/verilog_backend.cc`.
2020-04-01 05:25:10 +00:00
68c0e3562e
Clean up pseudo-private member usage in `backends/spice/spice.cc`.
2020-04-01 04:56:52 +00:00
057976c323
Clean up pseudo-private member usage in `backends/edif/edif.cc`.
2020-04-01 04:37:07 +00:00
68fef4ca7f
Clean up pseudo-private member usage in `backends/ilang/ilang_backend.cc`.
2020-04-01 03:08:39 +00:00
d72cb8ea2a
Do not change solver output parsing for non-exists-forall problems.
2020-03-26 23:00:00 +00:00
5accf08ef9
Skip reading stdout from the solver that if it isn't a line reading only "sat", "unsat", or "unknown".
2020-03-26 01:21:01 +00:00
c9555c9ade
Revert part of 0fda8308 from #1746 that broke other smtbmc flows
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-24 17:33:46 +01:00
b08932cb81
fix typo in `write_smt2` help
2020-03-23 02:14:26 -07:00
020f6d167a
Merge pull request #1768 from boqwxp/smt2_cleanup
...
Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.
2020-03-16 13:49:10 +01:00
a2e340de43
Merge pull request #1746 from boqwxp/optimization
...
Add support for optimizing exists-forall problems.
2020-03-16 12:23:14 +01:00
bf018b184d
Improve write_btor symbol handling
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-14 15:49:43 +01:00
07f0874779
Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.
2020-03-13 21:49:12 +00:00
0fda8308bc
Add support for optimizing exists-forall problems.
...
Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate.
Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al.
Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
2020-03-13 17:10:29 +00:00
746629f18d
remove include where not used
2020-03-13 14:55:53 +01:00
29e2b2dc05
Add info-file and cover features to write_btor
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-13 13:46:32 +01:00
3be7784d0e
xaiger: remove some unnecessary operations ...
...
... since they can not be triggered by (* keep *) anymore
(but could still be triggered by (* abc9_scc *) !?!)
2020-03-06 10:51:47 -08:00
91a7a74ac4
abc9: (* keep *) wires to be PO only, not PI as well; fix scc handling
2020-03-06 10:20:30 -08:00
6bb3d9f9c0
Make TimingInfo::TimingInfo(SigBit) constructor explicit
2020-02-27 10:17:29 -08:00
5ff60d2057
write_xaiger: add comment about arrival times of flop outputs
2020-02-27 10:17:29 -08:00
1ef1ca812b
Get rid of (* abc9_{arrival,required} *) entirely
2020-02-27 10:17:29 -08:00
e22fee6cdd
abc9_ops: ignore (* abc9_flop *) if not '-dff'
2020-02-27 10:17:29 -08:00
12d70ca8fb
xilinx: improve specify functionality
2020-02-27 10:17:29 -08:00
760096e8d2
Merge pull request #1703 from YosysHQ/eddie/specify_improve
...
Improve specify parser
2020-02-21 09:15:17 -08:00
f9f86fd758
Revert "abc9: fix abc9_arrival for flops"
...
This reverts commit f7c0dbecee
2020-02-14 16:08:04 -08:00
b523ecf2f4
specify: system timing checks to accept min:typ:max triple
2020-02-13 12:42:15 -08:00
whitequark
Eddie Hung
Miodrag Milanovic
Claire Wolf
Alberto Gonzalez
Claire Wolf
Teguh Hofstee
N. Engelhardt