Miodrag Milanovic
0d789c5a3b
Support custom PROGRAM_PREFIX
2020-04-10 10:38:40 +02:00
whitequark
4737f426ff
write_cxxrtl: add basic documentation.
2020-04-09 04:08:36 +00:00
whitequark
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
whitequark
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
whitequark
9534b51277
write_cxxrtl: add support for $slice and $concat cells.
2020-04-09 04:08:36 +00:00
whitequark
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
whitequark
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
whitequark
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
whitequark
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
whitequark
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
whitequark
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
Eddie Hung
956ecd48f7
kernel: big fat patch to use more ID::*, otherwise ID(*)
2020-04-02 09:51:32 -07:00
Eddie Hung
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
Eddie Hung
fdafb74eb7
kernel: use more ID::*
2020-04-02 07:14:08 -07:00
Claire Wolf
d1fc4321f0
Merge pull request #1770 from YosysHQ/claire/btor_symbols
...
Improve write_btor symbol handling
2020-04-02 15:38:47 +02:00
Claire Wolf
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
Alberto Gonzalez
c23c2c59c1
Update `RTLIL::id2cstr()` usage to `log_id`.
2020-04-01 06:53:28 +00:00
Alberto Gonzalez
cdb14652be
Clean up pseudo-private member usage in `backends/intersynth/intersynth.cc`.
2020-04-01 06:32:09 +00:00
Alberto Gonzalez
24ef73904f
Clean up pseudo-private member usage in `backends/blif/blif.cc`.
2020-04-01 05:50:48 +00:00
Alberto Gonzalez
f657fed24c
Clean up pseudo-private member usage in `backends/verilog/verilog_backend.cc`.
2020-04-01 05:25:10 +00:00
Alberto Gonzalez
68c0e3562e
Clean up pseudo-private member usage in `backends/spice/spice.cc`.
2020-04-01 04:56:52 +00:00
Alberto Gonzalez
057976c323
Clean up pseudo-private member usage in `backends/edif/edif.cc`.
2020-04-01 04:37:07 +00:00
Alberto Gonzalez
68fef4ca7f
Clean up pseudo-private member usage in `backends/ilang/ilang_backend.cc`.
2020-04-01 03:08:39 +00:00
Alberto Gonzalez
d72cb8ea2a
Do not change solver output parsing for non-exists-forall problems.
2020-03-26 23:00:00 +00:00
Alberto Gonzalez
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
Claire Wolf
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
Teguh Hofstee
b08932cb81
fix typo in `write_smt2` help
2020-03-23 02:14:26 -07:00
N. Engelhardt
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
N. Engelhardt
a2e340de43
Merge pull request #1746 from boqwxp/optimization
...
Add support for optimizing exists-forall problems.
2020-03-16 12:23:14 +01:00
Claire Wolf
bf018b184d
Improve write_btor symbol handling
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-14 15:49:43 +01:00
Alberto Gonzalez
07f0874779
Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.
2020-03-13 21:49:12 +00:00
Alberto Gonzalez
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
Miodrag Milanovic
746629f18d
remove include where not used
2020-03-13 14:55:53 +01:00
Claire Wolf
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
Eddie Hung
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
Eddie Hung
91a7a74ac4
abc9: (* keep *) wires to be PO only, not PI as well; fix scc handling
2020-03-06 10:20:30 -08:00
Eddie Hung
6bb3d9f9c0
Make TimingInfo::TimingInfo(SigBit) constructor explicit
2020-02-27 10:17:29 -08:00
Eddie Hung
5ff60d2057
write_xaiger: add comment about arrival times of flop outputs
2020-02-27 10:17:29 -08:00
Eddie Hung
1ef1ca812b
Get rid of (* abc9_{arrival,required} *) entirely
2020-02-27 10:17:29 -08:00
Eddie Hung
e22fee6cdd
abc9_ops: ignore (* abc9_flop *) if not '-dff'
2020-02-27 10:17:29 -08:00
Eddie Hung
12d70ca8fb
xilinx: improve specify functionality
2020-02-27 10:17:29 -08:00
Eddie Hung
760096e8d2
Merge pull request #1703 from YosysHQ/eddie/specify_improve
...
Improve specify parser
2020-02-21 09:15:17 -08:00
Eddie Hung
f9f86fd758
Revert "abc9: fix abc9_arrival for flops"
...
This reverts commit f7c0dbecee
.
2020-02-14 16:08:04 -08:00
Eddie Hung
b523ecf2f4
specify: system timing checks to accept min:typ:max triple
2020-02-13 12:42:15 -08:00
Eddie Hung
f5cc8cfa79
write_xaiger: default value for abc9_init
2020-02-13 12:37:17 -08:00
Eddie Hung
f7c0dbecee
abc9: fix abc9_arrival for flops
2020-02-13 12:34:09 -08:00
R. Ou
20ce4118da
json: Change compat mode to directly emit ints <= 32 bits
...
This increases compatibility with certain older parsers in some cases
that worked before commit 15fae357
but do not work with the current
compat-int mode
2020-02-09 01:01:18 -08:00
whitequark
6f67dd8df5
Merge pull request #1683 from whitequark/write_verilog-memattrs
...
write_verilog: dump $mem cell attributes
2020-02-07 02:54:04 +00:00
Marcin Kościelnicki
8f559b070a
edif: more resilience to mismatched port connection sizes.
...
Fixes #1653 .
2020-02-06 18:45:03 +01:00
whitequark
e95a8ba763
write_verilog: dump $mem cell attributes.
...
The Verilog backend already dumps attributes on RTLIL::Memory objects
but not on `$mem` cells.
2020-02-06 16:22:42 +00:00