Asu
dc77563a6a
cxxrtl: keep the memory write queue sorted on insertion.
...
Strategically inserting the pending memory write in memory::update to keep the
queue sorted allows us to skip the queue sort in memory::commit.
The Minerva SRAM SoC runs ~7% faster as a result.
2020-04-22 20:53:12 +02:00
Claire Wolf
95c74b319b
Merge pull request #1979 from whitequark/cxxrtl-go-faster
...
cxxrtl: Gas gas gas! I'm gonna step on the gas! Tonight I'll fly!
2020-04-22 16:50:45 +02:00
whitequark
93288b8eae
cxxrtl: run edge detectors only once in eval().
...
As a result, Minerva SRAM SoC runs ~15% faster.
2020-04-22 12:47:28 +00:00
whitequark
1d5b6ac253
cxxrtl: add an unsupported knob for manipulating clock trees.
...
This is quite possibly the worst way to implement this, but it does
work for a subset of well-behaved designs, and can be used to measure
how much performance is lost simulating the inactive edge of a clock.
It should be replaced with a clock tree analyzer generating safe
code once it is clear how should such a thing look like.
2020-04-22 01:15:27 +00:00
whitequark
5f17e0ced5
cxxrtl: use log_id() where appropriate. NFC.
2020-04-21 23:42:56 +00:00
whitequark
d22a8d157d
cxxrtl: add (*cxxrtl.{comb,sync}*) annotations on black box outputs.
...
If the annotations are not used, this commit does not alter semantics
at all, other than removing elision of outputs of black box cells.
(Elision of such outputs is expected to be too rare to have any
noticeable benefit, and the implementation was somewhat of a hack.)
The (* cxxrtl.comb *) annotation alters the semantics of the output
of the black box it is applied to such that, if the black box
converges immediately, no additional delta cycle is necessary to
propagate the computed combinatorial value upwards in hierarchy.
The (* cxxrtl.sync *) annotation alters the semantics of the output
of the black box it is applied to such as to remove any uses of
the black box by the wires connected to this output, and break false
feedback arcs arising from conservative modeling of dependencies of
the black box.
Although currently these attributes are only recognized on black
boxes, if separate compilation is added in the future, it could also
emit and consume them.
2020-04-21 22:08:36 +00:00
whitequark
164b0746d2
cxxrtl: s/sync_{wire,type}/edge_{wire,type}/. NFC.
...
The attribute for this is called (* cxxrtl.edge *), and there is
a planned attribute (* cxxrtl.sync *) that would cause blackbox
cell outputs to be added to sync defs rather than comb defs.
Rename the edge detector related stuff to avoid confusion.
2020-04-21 18:46:36 +00:00
Marcelina Kościelnicka
02f1c7b9af
write_json: dump default parameter values
...
Fixes #1823 .
This will allow nextpnr to reuse the default value information already
present in yosys cells_sim.v and avoid duplicating (and probably
desyncing) this information.
2020-04-21 19:09:00 +02:00
Marcelina Kościelnicka
06a344efcb
ilang, ast: Store parameter order and default value information.
...
Fixes #1819 , #1820 .
2020-04-21 19:09:00 +02:00
Claire Wolf
a6f9e28680
Merge pull request #1971 from YosysHQ/claire/edifkeep
...
Ignore conflicting keep attributes, unless asked not to
2020-04-21 19:04:55 +02:00
whitequark
4aa0f450f5
cxxrtl: use one delta cycle for immediately converging netlists.
...
If it is statically known that eval() will converge in one delta
cycle (that is, the second commit() will always return `false`)
because the design contains no feedback or buffered wires, then
there is no need to run the second delta cycle at all.
After this commit, the case where eval() always converges immediately
is detected and the second delta cycle is omitted. As a result,
Minerva SRAM SoC runs ~25% faster.
2020-04-21 16:14:45 +00:00
whitequark
7f5313e6c3
cxxrtl: add -O6, a shortcut for running `proc; flatten`.
...
People judge a compiler backend by the first impression, and
the metric they judge it for is speed. -O6 does severely impact
debuggability, but it provides equally massive gains in performance,
so use it by default.
2020-04-21 15:33:12 +00:00
whitequark
06985c3afd
cxxrtl: unbuffer module input wires.
...
Module input wires are never set by the module, so it is unnecessary
to buffer them. Although important for all inputs, this is especially
critical for clocks, since after this commit, hierarchy levels no
longer add delta cycles. As a result, Minerva SRAM SoC runs ~73%
faster when flattened, and ~264% (!!) faster when hierarchical.
2020-04-21 15:27:19 +00:00
whitequark
12c5e9275c
cxxrtl: simplify generated edge detection logic.
...
This commit changes the way edge detectors are represented in
generated code from a variable that is set in commit() and reset in
eval() to a function that considers .curr and .next of the clock
wire. Behavior remains the same. Besides being simpler to generate
and providing more opportunities for optimization, this commit paves
way for unbuffering module inputs.
2020-04-21 13:59:42 +00:00
whitequark
757cbb3c80
cxxrtl: localize wires with multiple comb drivers, too.
...
Before this commit, any wire that was not driven by an output port of
exactly one comb cell would not be localized, even if there were no
feedback arcs through that wire. This would cause the wire to become
buffered and require (often quite a few) extraneous delta cycles
during evaluation. To alleviate this problem, -O5 was running
`splitnets -driver`.
However, this solution was mistaken. Because `splitnets -driver`
followed by `opt_clean -purge` would produce more nets with multiple
drivers, it would have to be iterated to fixpoint. Moreover, even if
this was done, it would not be sufficient because `opt_clean -purge`
does not currently remove wires with the `\init` attribute (and it
is not desirable to remove such wires, since they correspond to
registers and may be useful for debugging).
The proper solution is to consider the condition in which a wire
may be localized. Specifically, if there are no feedback arcs through
this wire, and no part of the wire is driven by an output of a sync
cell, then the wire holds no state and is localizable.
After this commit, the original condition for not localizing a wire
is replaced by a check for any sync cell driving it. This makes it
unnecessary to run `splitnets -driver` in the majority of cases
to get a design with no buffered wires, and -O5 no longer includes
that pass. As a result, Minerva SRAM SoC no longer has any buffered
wires, and runs ~27% faster.
In addition, this commit prepares the flow graph for introduction
of sync outputs of black boxes.
Co-authored-by: Jean-François Nguyen <jf@lambdaconcept.com>
2020-04-21 13:36:50 +00:00
whitequark
f24fb4ae82
cxxrtl: detect buffered comb wires, not just feedback wires.
...
Any buffered combinatorial wires (including, as a subset, feedback
wires) will prevent the design from always converging in one delta
cycle. Before this commit, only feedback wires were detected. After
this commit, any buffered combinatorial wires, including feedback
wires, are detected.
Co-authored-by: Jean-François Nguyen <jf@lambdaconcept.com>
2020-04-21 13:36:50 +00:00
Claire Wolf
27506d2aeb
Improve net priorities in EDIF back-end
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-04-21 12:35:25 +02:00
whitequark
abc8f1fcb6
Merge pull request #1961 from whitequark/paramod-original-name
...
ast, rpc: record original name of $paramod\* as \hdlname attribute
2020-04-21 01:43:20 +00:00
Claire Wolf
ee5067e864
Ignore conflicting keep attributes, unless asked not to. Fixes #1733
...
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-04-20 16:00:37 +02:00
whitequark
bf0f96b847
cxxrtl: provide attributes to black box factories, too.
...
Both parameters and attributes are necessary because the parameters
have to be the same between every instantiation of the cell, but
attributes may well vary. For example, for an UART PHY, the type
of the PHY (tty, pty, socket) would be a parameter, but configuration
of the implementation specified by the type (socket address) would
be an attribute.
2020-04-19 16:30:54 +00:00
whitequark
63d2a30857
cxxrtl: add templated black box support.
2020-04-18 08:04:57 +00:00
whitequark
ab4297c326
cxxrtl: make eval() and commit() inline in blackboxes.
...
This change is a preparation for template blackboxes. It has no
effect on current generated code.
2020-04-18 04:38:50 +00:00
whitequark
2b88d9a3fe
cxxrtl: add simple black box support.
...
This commit adds support for replacing RTLIL modules with CXXRTL
black boxes. Black box port widths may not depend on the parameters
with which it is instantiated (yet); the parameters may only be used
to change the behavior of the black box.
2020-04-18 04:35:10 +00:00
whitequark
8bc3cd30dc
cxxrtl: use ID::X instead of ID(X). NFC.
2020-04-18 04:35:10 +00:00
whitequark
41421f5dca
ast, rpc: record original name of $paramod\* as \hdlname attribute.
...
The $paramod name mangling is not invertible (the \ character, which
separates the module name from the parameters, is valid in the module
name itself), which does not stop people from trying to invert it.
This commit makes it easy to invert the name mangling by storing
the original name explicitly, and fixes the firrtl backend to use
the newly introduced attribute.
2020-04-18 03:47:28 +00:00
whitequark
e7ad209b15
cxxrtl: correctly handle `sync always` rules.
...
Fixes #1948 .
2020-04-17 09:43:13 +00:00
whitequark
b4b2345a10
Merge pull request #1947 from whitequark/cxxrtl-usability
...
cxxrtl: minor documentation and usability improvements
2020-04-16 21:28:13 +00:00
Claire Wolf
7a434cdd7b
Merge pull request #1797 from epfl-vlsc/firrtl_backend_fileinfo
...
Keep file information when emitting firrtl
2020-04-16 18:50:43 +02:00
whitequark
06c0338f2c
cxxrtl: make ROMs writable, document memory::operator[].
...
There is no practical benefit from using `const memory` for ROMs;
it uses an std::vector internally, which prevents contemporary
compilers from constant-propagating ROM contents. (It is not clear
whether they are permitted to do so.)
However, there is a major benefit from using non-const `memory` for
ROMs, which is the ability to dynamically fill the ROM for each
individual simulation.
2020-04-16 16:45:54 +00:00
whitequark
9043632dcc
cxxrtl: fix misleading example, caution about race conditions.
...
Fixes #1944 .
2020-04-16 16:45:54 +00:00
whitequark
58e89cd368
cxxrtl: remove inaccurate comment. NFC.
2020-04-16 16:45:54 +00:00
N. Engelhardt
0b7a5879e5
Merge pull request #1830 from boqwxp/qbfsat
...
Add `qbfsat` command to integrate exists-forall solving and specialization
2020-04-15 17:33:50 +02:00
Marcelina Kościelnicka
3611e7c864
json: Update format documentation.
...
Fixes #1693 .
2020-04-15 16:12:14 +02:00
David Shah
3b85b7c57a
cxxrtl: Fix handling of unclocked memory read ports
...
Signed-off-by: David Shah <dave@ds0.me>
2020-04-14 20:39:13 +01:00
whitequark
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
whitequark
7025881a5e
Merge pull request #1921 from whitequark/write_cxxrtl-separate-compilation
...
write_cxxrtl: enable separate compilation
2020-04-14 13:53:52 +00:00
whitequark
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
whitequark
9c64d37a4c
write_verilog: fix precondition check.
2020-04-14 12:12:50 +00:00
whitequark
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
Eddie Hung
0808318d55
xaiger: add check for $__ABC9_DELAY model
2020-04-13 19:11:23 -07:00
Miodrag Milanovic
0d789c5a3b
Support custom PROGRAM_PREFIX
2020-04-10 10:38:40 +02:00
Sahand Kashani
959a00a46f
Fix indentation
2020-04-09 21:16:02 +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
Sahand Kashani
ac388859e3
Remove dependency on ilang backend since we no longer use it
2020-04-08 23:59:22 +02:00
Sahand Kashani
9edf8869c1
Merge branch 'master' of github.com:YosysHQ/yosys into firrtl_backend_fileinfo
2020-04-08 23:50:37 +02:00
Sahand Kashani
820e3d1dad
Remove unnecessary pruning of double-quoting
...
In the past I was calling the ILANG_BACKEND::dump_const() to dump
values to an output stream. When these values were strings, the
function used to add quotes around them. The firrtl compiler, in turn,
escaped these quotes and the result was double-quoted strings which
were hard to read.
However I'm now calling design_entity->get_src_attribute() directly
and there is no additional quote being put around it, so we can
safely remove the unnecessary call to str.erase() here.
2020-04-08 23:20:56 +02:00
Alberto Gonzalez
437afa1f0c
Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole value recovery using that mode.
2020-04-04 22:13:25 +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
Sahand Kashani
6c2b220af5
Remove use of auto for simple types + simplify src attribute computation
2020-03-24 21:07:08 +01: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
Sahand Kashani
018116e478
Refactor to directly call ILANG_BACKEND::dump_const() + directly lookup src attribute
2020-03-24 10:55:21 +01:00
Teguh Hofstee
b08932cb81
fix typo in `write_smt2` help
2020-03-23 02:14:26 -07:00
Sahand Kashani
f48fb26c0f
Indentation conventions
2020-03-23 09:01:17 +01:00
Sahand Kashani-Akhavan
566e08485a
Const parameter in function (backends/firrtl/firrtl.cc)
...
Co-Authored-By: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>
2020-03-23 08:56:28 +01:00
Sahand Kashani
21492914a2
Strip quotes around fileinfo strings
...
Yosys puts quotes around the string that represents the fileinfo whereas
firrtl does not. So when firrtl sees quotes, it escapes them with an extra
backslash which makes it hard to read afterwards.
2020-03-21 15:57:53 +01:00
Sahand Kashani
c0b2a9af2e
Add fileinfo to firrtl backend for assignments and non-instance cells
2020-03-21 12:54:23 +01:00
Sahand Kashani
3e04e29dec
Refactor fileinfo emission characters to single location
2020-03-20 18:31:12 +01:00
Sahand Kashani
ed9f8bfe6e
Add fileinfo to firrtl backend for instances
2020-03-19 16:24:18 +01:00
Sahand Kashani
59236314f8
Add fileinfo to firrtl backend for modules and wires
2020-03-19 14:59:05 +01:00
Sahand Kashani
bdce9c28c2
Add fileinfo to firrtl backend for top-level circuit
2020-03-19 00:14:27 +01: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
Eddie Hung
0671ae7d79
Merge pull request #1661 from YosysHQ/eddie/abc9_required
...
abc9: add support for required times
2020-02-05 18:59:40 +01:00
Marcin Kościelnicki
00fba62711
json: remove the 32-bit parameter special case
...
Before, the rules for encoding parameters in JSON were as follows:
- if the parameter is not a string:
- if it is exactly 32 bits long and there are no z or x bits, emit it
as an int
- otherwise, emit it as a string made of 0/1/x/z characters
- if the parameter is a string:
- if it contains only 0/1/x/z characters, append a space at the end
to distinguish it from a non-string
- otherwise, emit it directly
However, this caused a problem in the json11 parser used in nextpnr:
yosys emits unsigned ints, and nextpnr parses them as signed, using
the value of INT_MIN for values that overflow the signed int range.
This caused destruction of LUT5 initialization values. Since both
nextpnr and yosys parser can also accept 32-bit parameters in the
same encoding as other widths, let's just remove that special case.
The old behavior is still left behind a `-compat-int` flag, in case
someone relies on it.
2020-02-01 16:16:26 +01:00
Claire Wolf
50d70288d0
Preserve wires with keep attribute in EDIF back-end
...
Signed-off-by: Claire Wolf <clifford@clifford.at>
2020-01-29 14:07:11 +01:00
Eddie Hung
48f3f5213e
Merge pull request #1619 from YosysHQ/eddie/abc9_refactor
...
Refactor `abc9` pass
2020-01-27 13:29:15 -08:00
Eddie Hung
f2576c096c
Merge branch 'eddie/abc9_refactor' into eddie/abc9_required
2020-01-27 12:29:28 -08:00
Claire Wolf
485f31f681
Improve yosys-smtbmc "solver not found" handling
...
Signed-off-by: Claire Wolf <clifford@clifford.at>
2020-01-27 17:48:56 +01:00
Eddie Hung
3d9737c1bd
Merge remote-tracking branch 'origin/master' into eddie/abc9_refactor
2020-01-21 16:27:40 -08:00
Eddie Hung
cd8f55a911
write_xaiger: fix for (* keep *) on flop output
2020-01-21 09:43:04 -08:00
Claire Wolf
30642e9570
Merge pull request #1629 from YosysHQ/mwk/edif-z
...
edif: Just ignore connections to 'z
2020-01-21 18:35:15 +01:00
Eddie Hung
38aa248385
Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required
2020-01-15 11:26:11 -08:00
Eddie Hung
d6da9c0c0f
write_xaiger: skip abc9_flop only if abc_box_seq present
2020-01-15 11:25:20 -08:00
Eddie Hung
485e08e436
abc9_ops: cope with (* abc9_flop *) in place of (* abc9_box_id *)
2020-01-14 16:33:41 -08:00
Eddie Hung
48984a7605
Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required
2020-01-14 16:32:46 -08:00
Eddie Hung
1c41dc6b95
write_xaiger: do not export flop inputs as POs
2020-01-14 16:17:27 -08:00
Eddie Hung
0e4285ca0d
abc9_ops: generate flop box ids, add abc9_required to FD* cells
2020-01-14 15:05:49 -08:00
Eddie Hung
588a713b54
Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required
2020-01-14 14:28:07 -08:00
Eddie Hung
4656f202c6
abc9_ops: -reintegrate to not trim box padding anymore
2020-01-14 14:27:29 -08:00
Eddie Hung
aaafd784a5
write_xaiger: skip if no arrival times
2020-01-14 13:05:39 -08:00
Eddie Hung
915e7dde73
Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required
2020-01-14 12:57:56 -08:00
Eddie Hung
654247abe9
abc9_ops/write_xaiger: update doc
2020-01-14 12:40:36 -08:00
Eddie Hung
468386d67d
abc9_ops: -prep_holes -> -prep_xaiger, move padding to write_xaiger
2020-01-14 12:25:45 -08:00
Eddie Hung
53a99ade9c
Merge remote-tracking branch 'origin/master' into eddie/abc9_refactor
2020-01-14 11:46:56 -08:00
Miodrag Milanović
9fbeb57bbd
Merge pull request #1623 from YosysHQ/mmicko/edif_attr
...
Export wire properties in EDIF
2020-01-14 19:19:32 +01:00
Eddie Hung
eb7dd7d374
write_xaiger: fix case of PI and CI and (* keep *)
2020-01-13 23:23:21 -08:00
Eddie Hung
2c65e1abac
abc9: break SCC by setting (* keep *) on output wires
2020-01-13 21:45:27 -08:00
Eddie Hung
a6d4ea7463
abc9: respect (* keep *) on cells
2020-01-13 19:21:11 -08:00
Eddie Hung
9ec948f396
write_xaiger: add support and test for (* keep *) on wires
2020-01-13 19:07:55 -08:00
Eddie Hung
0d2c06ee47
write_xaiger: cache arrival times
2020-01-13 09:50:50 -08:00
Marcin Kościelnicki
55f86eda36
edif: Just ignore connections to 'z
...
Connecting a const 'z to a net should be equivalent to not connecting it
at all, so let's just ignore such connections on output.
2020-01-13 14:49:31 +01:00
Eddie Hung
f9aae90e7a
Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required
2020-01-12 15:19:41 -08:00
Eddie Hung
295e241c07
cleanup
2020-01-11 17:28:24 -08:00
Eddie Hung
79db12f238
Merge remote-tracking branch 'origin/master' into eddie/abc9_refactor
2020-01-11 17:26:25 -08:00
Eddie Hung
58ab9f6021
write_xaiger: create holes_sigmap before modifications
2020-01-11 17:25:32 -08:00
Eddie Hung
1ccee4b95e
write_xaiger: sort holes by offset as well as port_id
2020-01-11 11:49:57 -08:00
Eddie Hung
f24de88f38
log_debug() for abc9_{arrival,required} times
2020-01-10 17:13:27 -08:00
Miodrag Milanovic
6888799c75
remove whitespace
2020-01-10 12:38:03 +01:00
Miodrag Milanovic
2bcd55f1ae
Export wire properties as well in EDIF
2020-01-10 12:33:58 +01:00
Eddie Hung
ceabd5bc39
write_xaiger: cleanup
2020-01-09 14:03:43 -08:00
Eddie Hung
3177437224
write_xaiger: cope with abc9_arrival as string of ints
2020-01-09 10:05:03 -08:00
Eddie Hung
7532416cd7
write_xaiger: cleanup holes generation
2020-01-08 18:27:09 -08:00
Eddie Hung
5f7349f26d
write_xaiger: holes PIs only if whitebox
2020-01-08 15:40:37 -08:00
Eddie Hung
8d0cc654a4
Stray log_module
2020-01-06 15:14:38 -08:00
Eddie Hung
aa58472a29
Revert "write_xaiger to pad, not abc9_ops -prep_holes"
...
This reverts commit b5f60e055d
.
2020-01-06 13:34:45 -08:00
Eddie Hung
921ff0f5e3
Merge remote-tracking branch 'origin/xaig_dff' into eddie/abc9_refactor
2020-01-06 12:04:08 -08:00
Eddie Hung
886c5c5883
write_xaiger: make more robust, update doc
2020-01-06 10:23:04 -08:00
Eddie Hung
19ec54f956
write_aiger: make more robust
2020-01-06 10:18:59 -08:00
Eddie Hung
b5f60e055d
write_xaiger to pad, not abc9_ops -prep_holes
2020-01-05 10:20:24 -08:00
Eddie Hung
6556a1347a
Fix when -dff not given
2020-01-04 09:17:01 -08:00
Eddie Hung
930f03e883
Call -prep_holes before aigmap; fix topo ordering
2020-01-03 15:38:18 -08:00
Eddie Hung
a819656972
WIP
2020-01-03 14:59:55 -08:00
Eddie Hung
559f3379e8
Preserve topo ordering from -prep_holes to write_xaiger
2020-01-03 14:37:58 -08:00
Eddie Hung
bb70915fb8
WIP
2020-01-03 13:21:56 -08:00
Eddie Hung
e1f494ab1d
WIP
2020-01-03 13:08:52 -08:00
Eddie Hung
e62eb02c1d
Restore write_xaiger's holes_mode since port_id order causes QoR
...
regressions inside abc9
2020-01-03 12:32:05 -08:00
Eddie Hung
dedea5a58d
Cleanup
2020-01-02 17:25:14 -08:00
Eddie Hung
c28bea0382
Merge remote-tracking branch 'origin/xaig_dff' into eddie/abc9_refactor
2020-01-02 15:57:35 -08:00
Eddie Hung
07feedfa73
write_xaiger: get rid of external_bits dict
2020-01-02 15:32:58 -08:00
Eddie Hung
8e507bd807
abc9 -keepff -> -dff; refactor dff operations
2020-01-02 12:36:54 -08:00
Eddie Hung
11577b46fc
Get rid of (* abc9_keep *) in write_xaiger too
2020-01-01 08:38:23 -08:00
Eddie Hung
ac808c5e2a
attributes.count() -> get_bool_attribute()
2020-01-01 08:33:32 -08:00
Eddie Hung
96db05aaef
parse_xaiger to not take box_lookup
2019-12-31 17:06:03 -08:00
Eddie Hung
cac7f5d82e
Do not re-order carry chain ports, just precompute iteration order
2019-12-31 16:12:40 -08:00
Eddie Hung
134e70e8e7
write_xaiger: be more precise with ff_bits, remove ff_aig_map
2019-12-31 10:21:11 -08:00
Eddie Hung
3798fa3bea
Retry getting rid of write_xaiger's holes_mode
2019-12-31 09:59:17 -08:00
Eddie Hung
436c96e2fb
Revert "Get rid of holes_mode"
...
This reverts commit 7997e2a90f
.
2019-12-30 23:29:14 -08:00
Eddie Hung
7997e2a90f
Get rid of holes_mode
2019-12-30 20:15:09 -08:00
Eddie Hung
b42b64e8ed
Move Pass::call() out of abc9_ops into abc9
2019-12-30 19:23:54 -08:00
Eddie Hung
88334cab89
Cleanup
2019-12-30 18:49:33 -08:00
Eddie Hung
65baefecd3
Rid unnecessary if
2019-12-30 18:26:35 -08:00
Eddie Hung
e2bbe33a88
Get rid of holes_mode
2019-12-30 18:24:29 -08:00
Eddie Hung
b50de28c04
Add abc9_ops -prep_holes
2019-12-30 18:00:49 -08:00
Eddie Hung
0735572934
write_xaiger to use scratchpad for stats; cleanup abc9
2019-12-30 15:35:33 -08:00
Eddie Hung
d1fccd5a2d
Remove unused
2019-12-30 14:35:52 -08:00
Eddie Hung
3cbbae251f
Call "proc" if processes inside whiteboxes
2019-12-30 14:33:05 -08:00
Eddie Hung
405e974fe5
Merge remote-tracking branch 'origin/master' into xaig_dff
2019-12-30 14:31:42 -08:00
Eddie Hung
d7ada66497
Add "synth_xilinx -dff" option, cleanup abc9
2019-12-30 14:13:16 -08:00
Eddie Hung
237415e78c
write_xaiger: inherit port ordering from original module
2019-12-27 16:44:18 -08:00
Eddie Hung
a56d6970f2
Revert "Merge pull request #1598 from YosysHQ/revert-1588-eddie/xaiger_cleanup"
...
This reverts commit 92654f73ea
, reversing
changes made to 3e14ff1667
.
2019-12-27 16:05:58 -08:00
Eddie Hung
9e6632c40a
Merge branch 'master' of github.com:YosysHQ/yosys
2019-12-27 15:37:26 -08:00
Eddie Hung
3d4644804e
write_xaiger: simplify c{i,o}_bits
2019-12-27 15:37:17 -08:00
David Shah
df31ade3b3
Revert "write_xaiger: only instantiate each whitebox cell type once"
2019-12-27 23:25:20 +00:00
Eddie Hung
dd503a5f3f
Really fix it!
2019-12-27 15:18:55 -08:00
Eddie Hung
49881b4468
write_xaiger: fix arrival times for non boxes
2019-12-27 11:30:18 -08:00
Eddie Hung
6eadd4390a
write_xaiger to opt instead of just clean whiteboxes
2019-12-23 08:35:53 -08:00
Eddie Hung
a75e08c709
write_xaiger: only instantiate each whitebox cell type once
2019-12-20 13:07:24 -08:00
Eddie Hung
10e82e103f
Revert "Optimise write_xaiger"
2019-12-20 12:05:45 -08:00
Eddie Hung
5f50e4f112
Cleanup xaiger, remove unnecessary complexity with inout
2019-12-17 15:45:26 -08:00
Eddie Hung
e82a9bc642
Do not sigmap
2019-12-17 00:03:03 -08:00
Eddie Hung
2e71130700
Revert "Use sigmap signal"
...
This reverts commit 42f990f3a6
.
2019-12-17 00:00:07 -08:00
Eddie Hung
42f990f3a6
Use sigmap signal
2019-12-16 16:49:42 -08:00
Eddie Hung
b19fc8839b
Skip $inout transformation if not a PI
2019-12-16 14:39:13 -08:00
Eddie Hung
78c0246d4a
Revert "write_xaiger: use sigmap bits more consistently"
...
This reverts commit 6c340112fe
.
2019-12-16 14:35:35 -08:00
Eddie Hung
6c340112fe
write_xaiger: use sigmap bits more consistently
2019-12-16 10:21:57 -08:00
Eddie Hung
91467938c4
Stray newline
2019-12-06 17:08:19 -08:00
Eddie Hung
f2ac36de4a
write_xaiger to inst each cell type once, do not call techmap/aigmap
2019-12-06 17:06:10 -08:00
Eddie Hung
1f96de04c9
Fix writing non-whole modules, including inouts and keeps
2019-12-06 16:19:10 -08:00
Eddie Hung
a682a3cf93
write_xaiger to support part-selected modules again
2019-12-05 17:54:43 -08:00
Eddie Hung
c6ee2fb482
Cleanup
2019-12-03 19:21:47 -08:00
Eddie Hung
df52bc80d8
write_xaiger to consume abc9_init attribute for abc9_flops
2019-12-03 18:47:44 -08:00
Eddie Hung
419ca5c207
Revert "Fold loop"
...
This reverts commit a30d5e1cc3
.
2019-11-27 21:55:56 -08:00
Eddie Hung
449b1d2c6f
Add comment, use sigmap
2019-11-27 13:20:12 -08:00
Eddie Hung
403214f44d
Revert "Fold loop"
...
This reverts commit da51492dbc
.
2019-11-27 12:35:25 -08:00
Eddie Hung
5e67df38ed
latch -> box
2019-11-26 22:59:05 -08:00
Eddie Hung
a30d5e1cc3
Fold loop
2019-11-26 21:57:50 -08:00
Eddie Hung
68717dd03b
Do not sigmap keep bits inside write_xaiger
2019-11-26 21:57:50 -08:00
Eddie Hung
7136cee6b4
xaiger: do not promote output wires
2019-11-26 21:55:37 -08:00
Eddie Hung
99702efaba
xaiger: do not promote output wires
2019-11-26 19:03:02 -08:00
Eddie Hung
da51492dbc
Fold loop
2019-11-25 15:43:37 -08:00
Eddie Hung
7f0914a408
Do not sigmap keep bits inside write_xaiger
2019-11-25 15:42:07 -08:00
Eddie Hung
81548d1ef9
write_xaiger back to working with whole modules only
2019-11-22 16:52:17 -08:00
Eddie Hung
8ef241c6f4
Revert "write_xaiger to not use module POs but only write outputs if driven"
...
This reverts commit 0ab1e496dc
.
2019-11-22 13:24:28 -08:00
Eddie Hung
0ab1e496dc
write_xaiger to not use module POs but only write outputs if driven
2019-11-21 16:19:28 -08:00
Eddie Hung
929beda19c
abc9 to support async flops $_DFF_[NP][NP][01]_
2019-11-19 16:57:26 -08:00
Eddie Hung
09ee96e8c2
Merge remote-tracking branch 'origin/master' into xaig_dff
2019-11-19 15:40:39 -08:00
whitequark
3c643c57df
write_verilog: add -extmem option, to write split memory init files.
...
Some toolchains (in particular Quartus) are pathologically slow if
a large amount of assignments in `initial` blocks are used.
2019-11-18 01:27:21 +00:00
Clifford Wolf
cd44826d50
Use cell name for btor bad state props when it is a public name
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-14 11:57:38 +01:00
Makai Mann
d88cc139a0
Add an info string symbol for bad states in btor backend
2019-11-11 16:40:51 -08:00
Clifford Wolf
5110a34dd7
Fix write_aiger bug added in 524af21
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-04 14:25:13 +01:00
Clifford Wolf
81876a3734
Merge pull request #1393 from whitequark/write_verilog-avoid-init
...
write_verilog: do not print (*init*) attributes on regs
2019-10-27 10:25:01 +01:00
Clifford Wolf
f02623abb5
Bugfix in smtio vcd handling of $-identifiers
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-10-23 00:04:34 +02:00
Eddie Hung
b2e34f932a
Rename $currQ to $abc9_currQ
2019-10-07 15:31:43 -07:00
Eddie Hung
90a954bb9c
Get rid of latch_* in write_xaiger
2019-10-07 13:09:13 -07:00
Eddie Hung
1504ca2cd9
Remove "write_xaiger -zinit"
2019-10-07 11:58:49 -07:00
Eddie Hung
e1554b56dd
Add comment on default flop init
2019-10-07 11:56:17 -07:00
Eddie Hung
d9fba95177
Get rid of output_port lookup
2019-10-07 11:49:06 -07:00
Eddie Hung
3879ca1398
Do not require changes to cells_sim.v; try and work out comb model
2019-10-05 22:55:18 -07:00
Eddie Hung
3c6e5d82a6
Error if $currQ not found
2019-10-05 09:06:13 -07:00
Eddie Hung
7959e9d6b2
Fix merge issues
2019-10-04 17:21:14 -07:00
Eddie Hung
7a45cd5856
Merge remote-tracking branch 'origin/eddie/abc_to_abc9' into xaig_dff
2019-10-04 16:58:55 -07:00
Eddie Hung
aae2b9fd9c
Rename abc_* names/attributes to more precisely be abc9_*
2019-10-04 11:04:10 -07:00
Eddie Hung
549d6ea467
Merge remote-tracking branch 'origin/master' into xaig_dff
2019-10-03 10:55:23 -07:00
Clifford Wolf
2ed2e9c3e8
Change smtbmc "Warmup failed" status to "PREUNSAT"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-10-03 14:59:07 +02:00
Clifford Wolf
a84a2d74c7
Fix btor back-end to use "state" instead of "input" for undef init bits
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-10-02 12:48:04 +02:00
Eddie Hung
1b96d29174
No need to punch ports at all
2019-09-30 17:02:20 -07:00
Eddie Hung
e529872b01
Remove need for $currQ port connection
2019-09-30 16:33:40 -07:00
Eddie Hung
eecfdda614
Cleanup
2019-09-30 15:24:03 -07:00
Eddie Hung
74678227c7
Use a cell_cache to instantiate once rather than opt_merge call
2019-09-30 13:21:07 -07:00
Eddie Hung
a6994c5f16
scc call on active module module only, plus cleanup
2019-09-30 12:57:19 -07:00
Eddie Hung
bd8356799a
Use derived module
2019-09-30 12:34:28 -07:00
Eddie Hung
1123c09588
Merge remote-tracking branch 'origin/master' into xaig_dff
2019-09-29 19:39:12 -07:00
Eddie Hung
8474c5b366
Merge pull request #1359 from YosysHQ/xc7dsp
...
DSP inference for Xilinx (improved for ice40, initial support for ecp5)
2019-09-29 11:26:22 -07:00
Eddie Hung
f3e150d9a5
Merge remote-tracking branch 'origin/master' into xaig_dff
2019-09-29 09:21:51 -07:00
Miodrag Milanović
ce0631c371
Merge pull request #1413 from YosysHQ/mmicko/backend_binary_out
...
Support binary files for backends, fixes #1407
2019-09-29 10:37:34 +02:00
Eddie Hung
79b6edb639
Big rework; flop info now mostly in cells_sim.v
2019-09-28 23:48:17 -07:00
Miodrag Milanovic
0c380f0855
Add aiger and protobuf backends binary support
2019-09-28 09:51:48 +02:00
Miodrag Milanovic
d0493925ec
Support binary files for backends, fixes #1407
2019-09-28 09:36:18 +02:00
Eddie Hung
cfa6dd61ef
Use abc_mergeability attr for "r" extension
2019-09-27 18:41:43 -07:00
Eddie Hung
dc154c39a8
Fix infinite recursion
2019-09-27 17:45:49 -07:00
Eddie Hung
8f5710c464
Merge remote-tracking branch 'origin/master' into xaig_dff
2019-09-27 15:14:31 -07:00
Aman Goel
5eebfabe42
Corrects btor2 backend
2019-09-27 12:40:17 -04:00
Eddie Hung
44374b1b2b
"abc_padding" attr for blackbox outputs that were padded, remove them later
2019-09-23 21:58:40 -07:00
Eddie Hung
c340fbfab2
Force $inout.out ports to begin with '$' to indicate internal
2019-09-23 21:58:04 -07:00
whitequark
4f426c2ac4
write_verilog: do not print (*init*) attributes on regs.
...
If an init value is emitted for a reg, an (*init*) attribute is never
necessary, since it is exactly equivalent. On the other hand, some
tools that consume Verilog (ISE, Vivado, Quartus) complain about
(*init*) attributes because their interpretation differs from Yosys.
All (*init*) attributes that would not become reg init values anyway
are emitted as before.
2019-09-22 16:52:06 +00:00
Eddie Hung
2d9484c12c
When two boxes connect to each other, need not be a (* keep *)
2019-09-19 15:40:28 -07:00
Clifford Wolf
779ce3537f
Add "write_aiger -L"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-09-18 13:33:02 +02:00
Clifford Wolf
b88d2e5f30
Fix stupid bug in btor back-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-09-18 11:56:14 +02:00
Sean Cross
c1b628508d
backends: smt2: use $(CXX) variable for compiler
...
The Makefile assumes the compiler is called `gcc`, which isn't always
true. In fact, if we're building on msys2 or msys2-64, the compiler
is called `i686-w64-mingw32-g++` or `x86_64-w64-mingw32-g++`.
Use the variable instead of hardcoding the name, to fix building on
these systems.
Signed-off-by: Sean Cross <sean@xobs.io>
2019-09-08 15:47:09 +08:00
Eddie Hung
e9bb252e77
Recognise built-in types (e.g. $_DFF_*)
2019-08-30 20:15:09 -07:00
Eddie Hung
3247442bf9
Revert "Revert "Fix omode which inserts an output if none exists (otherwise abc9 breaks)""
...
This reverts commit 8f0c1232d7
.
2019-08-28 17:34:00 -07:00
Eddie Hung
082a01954b
Revert "Output "h" extension only if boxes"
...
This reverts commit 399ac760ff
.
2019-08-28 17:30:54 -07:00
Eddie Hung
399ac760ff
Output "h" extension only if boxes
2019-08-21 11:31:18 -07:00
Eddie Hung
8f0c1232d7
Revert "Fix omode which inserts an output if none exists (otherwise abc9 breaks)"
...
This reverts commit 8182cb9d91
.
2019-08-21 11:29:40 -07:00
Eddie Hung
8182cb9d91
Fix omode which inserts an output if none exists (otherwise abc9 breaks)
2019-08-20 21:30:16 -07:00
Eddie Hung
4d123b7638
Revert "Only xaig if GetSize(output_bits) > 0"
...
This reverts commit 7b646101e9
.
2019-08-20 21:22:38 -07:00
Eddie Hung
7b646101e9
Only xaig if GetSize(output_bits) > 0
2019-08-20 20:57:13 -07:00
Eddie Hung
f1a206ba03
Revert "Remove sequential extension"
...
This reverts commit 091bf4a18b
.
2019-08-20 18:17:14 -07:00
Eddie Hung
091bf4a18b
Remove sequential extension
2019-08-20 18:16:37 -07:00
Eddie Hung
1b5d2de1d4
Do not sigmap!
2019-08-20 15:23:26 -07:00
Eddie Hung
c00d72cdb3
Minor refactor
2019-08-20 14:47:58 -07:00
Eddie Hung
45d4b33f0c
Output i/o/h extensions even if no boxes or flops
2019-08-19 13:17:31 -07:00
Eddie Hung
91687d3fea
Add (* abc_arrival *) attribute
2019-08-19 12:33:24 -07:00
Eddie Hung
2f4e0a5388
Merge remote-tracking branch 'origin/master' into xaig_dff
2019-08-19 10:07:27 -07:00
Eddie Hung
10c69f71e9
Use %d
2019-08-19 09:16:20 -07:00
Eddie Hung
24c934f1af
Merge branch 'eddie/abc9_refactor' into xaig_dff
2019-08-16 16:51:22 -07:00
Eddie Hung
4fe307f1bc
Compute abc_scc_break and move CI/CO outside of each abc9
2019-08-16 15:41:17 -07:00
Clifford Wolf
0c5db07cd6
Fix various NDEBUG compiler warnings, closes #1255
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-08-13 13:29:03 +02:00
Clifford Wolf
f54bf1631f
Merge pull request #1258 from YosysHQ/eddie/cleanup
...
Cleanup a few barnacles across codebase
2019-08-10 09:52:14 +02:00
Clifford Wolf
05c46a31dc
Merge pull request #1263 from ucb-bar/firrtl_err_on_unsupported_cell
...
FIRRTL error on unsupported cell
2019-08-10 09:47:10 +02:00
Eddie Hung
6d77236f38
substr() -> compare()
2019-08-07 12:20:08 -07:00
Eddie Hung
7164996921
RTLIL::S{0,1} -> State::S{0,1}
2019-08-07 11:12:38 -07:00
Eddie Hung
e6d5147214
Merge remote-tracking branch 'origin/master' into eddie/cleanup
2019-08-07 11:11:50 -07:00
Jim Lawson
5e8a98c8fd
Merge branch 'master' into firrtl_err_on_unsupported_cell
...
# Conflicts:
# backends/firrtl/firrtl.cc
2019-08-07 10:14:45 -07:00
Eddie Hung
3090da2d98
Run "clean -purge" on holes_module in its own design
2019-08-07 09:54:27 -07:00
Clifford Wolf
48f7682e32
Merge pull request #1240 from ucb-bar/firrtl-properties+pow+xnor
...
Support explicit FIRRTL properties for better accommodation of FIRRTL/Verilog semantic differences.
2019-08-07 12:31:32 +02:00
David Shah
dee8f61781
Merge pull request #1241 from YosysHQ/clifford/jsonfix
...
Improved JSON attr/param encoding
2019-08-07 10:40:38 +01:00
Eddie Hung
e38f40af5b
Use IdString::begins_with()
2019-08-06 16:42:25 -07:00
Eddie Hung
a6bc9265fb
RTLIL::S{0,1} -> State::S{0,1}
2019-08-06 16:23:37 -07:00
Eddie Hung
046e1a5214
Use State::S{0,1}
2019-08-06 16:22:47 -07:00
Eddie Hung
3486235338
Make liberal use of IdString.in()
2019-08-06 16:18:18 -07:00
Clifford Wolf
023086bd46
Add $_NMUX_, add "abc -g cmos", add proper cmos cell costs
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-08-06 04:47:55 +02:00
Clifford Wolf
0917a5cf72
Merge pull request #1238 from mmicko/vsbuild_fix
...
Visual Studio build fix
2019-08-02 17:07:39 +02:00
Miodrag Milanovic
28b7053a01
Fix formatting for msys2 mingw build using GetSize
2019-08-01 17:27:34 +02:00
Clifford Wolf
15fae357f6
Implement improved JSON attr/param encoding
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-08-01 12:34:52 +02:00
Jim Lawson
3b8c917025
Support explicit FIRRTL properties for better accommodation of FIRRTL/Verilog semantic differences.
...
Use FIRRTL spec vlaues for definition of FIRRTL widths.
Added support for '$pos`, `$pow` and `$xnor` cells.
Enable tests/simple/operators.v since all operators tested there are now supported.
Disable FIRRTL tests of tests/simple/{defvalue.sv,implicit_ports.v,wandwor.v} since they currently generate FIRRTL compilation errors.
2019-07-31 09:27:38 -07:00
Miodrag Milanovic
35d28de478
Visual Studio build fix
2019-07-31 09:10:24 +02:00
Jim Lawson
7e298084e4
Call log_error() instead of log_warning() on unsupported cell type in FIRRTL backend.
2019-07-24 13:33:16 -07:00
Clifford Wolf
927f0caa9d
Merge pull request #1203 from whitequark/write_verilog-zero-width-values
...
write_verilog: dump zero width constants correctly
2019-07-18 15:31:27 +02:00
Clifford Wolf
56c00e871f
Remove old $pmux_safe code from write_verilog
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-07-17 11:49:04 +02:00
whitequark
4ff44d85a5
write_verilog: dump zero width constants correctly.
...
Before this commit, zero width constants 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.)
Fixes #948 (again).
2019-07-16 21:00:09 +00:00
N. Engelhardt
ab4b9e8db4
smt: handle failure of setrlimit syscall
2019-07-15 23:33:18 +08:00
Clifford Wolf
9112850800
Merge pull request #1172 from whitequark/write_verilog-Sa-as-qmark
...
write_verilog: write RTLIL::Sa aka - as Verilog ?
2019-07-11 07:25:52 +02:00
Eddie Hung
375fcbe511
abc_flop to also get topologically sorted
2019-07-10 20:26:09 -07:00
Eddie Hung
ea6ffea2cd
Fix clk_pol for FD*_1
2019-07-10 20:10:20 -07:00
Eddie Hung
e603d719d6
Fix spacing
2019-07-10 19:04:22 -07:00
Eddie Hung
4a995c5d80
Change how to specify flops to ABC again
2019-07-10 17:54:56 -07:00
Eddie Hung
a092c48f03
Use split_tokens()
2019-07-10 17:34:51 -07:00
Eddie Hung
052060f109
Merge remote-tracking branch 'origin/master' into xaig_dff
2019-07-10 16:05:41 -07:00
Clifford Wolf
6dd33be7ce
Merge pull request #1175 from whitequark/write_verilog-fix-case-attr-position
...
write_verilog: fix placement of case attributes
2019-07-09 22:51:25 +02:00
whitequark
37bb6b5e96
write_verilog: fix placement of case attributes. NFC.
2019-07-09 19:14:03 +00:00
whitequark
6a29e1f5b7
write_verilog: write RTLIL::Sa aka - as Verilog ?.
...
Currently, the only ways (determined by grepping for regex \bSa\b) to
end up with RTLIL::Sa in a netlist is by reading a Verilog constant
with ? in it as a part of case, or by running certain FSM passes.
Both of these cases should be round-tripped back to ? in Verilog.
2019-07-09 18:35:49 +00:00
Eddie Hung
00d8a9dce2
Merge pull request #1170 from YosysHQ/eddie/fix_double_underscore
...
Rename __builtin_bswap32 -> bswap32
2019-07-09 10:22:57 -07:00
Eddie Hung
5a0f2e43c7
Rename __builtin_bswap32 -> bswap32
2019-07-09 09:35:09 -07:00
whitequark
628437b01c
verilog_backend: dump attributes on SwitchRule.
...
This appears to be an omission.
2019-07-08 15:11:29 +00:00
whitequark
55c1f40277
verilog_backend: dump attributes on CaseRule, as comments.
...
Attributes are not permitted in that position by Verilog grammar.
2019-07-08 12:48:50 +00:00
whitequark
93bc5affd3
Allow attributes on individual switch cases in RTLIL.
...
The parser changes are slightly awkward. Consider the following IL:
process $0
<point 1>
switch \foo
<point 2>
case 1'1
assign \bar \baz
<point 3>
...
case
end
end
Before this commit, attributes are valid in <point 1>, and <point 3>
iff it is immediately followed by a `switch`. (They are essentially
attached to the switch.) But, after this commit, and because switch
cases do not have an ending delimiter, <point 3> becomes ambiguous:
the attribute could attach to either the following `case`, or to
the following `switch`. This isn't expressible in LALR(1) and results
in a reduce/reduce conflict.
To address this, attributes inside processes are now valid anywhere
inside the process: in <point 1> and <point 3> a part of case body,
and in <point 2> as a separate rule. As a consequence, attributes
can now precede `assign`s, which is made illegal in the same way it
is illegal to attach attributes to `connect`.
Attributes are tracked separately from the parser state, so this
does not affect collection of attributes at all, other than allowing
them on `case`s. The grammar change serves purely to allow attributes
in more syntactic places.
2019-07-08 11:34:58 +00:00
Eddie Hung
10524064e9
write_xaiger to treat unknown cell connections as keep-s
2019-07-02 19:14:30 -07:00
Eddie Hung
69f4c039ce
Safe side: all flops have different mergeability class
2019-07-02 12:21:03 -07:00
Eddie Hung
a31e17182d
Refactor and cope with new abc_flop format
2019-07-01 11:50:34 -07:00
Eddie Hung
699d8e3939
Merge remote-tracking branch 'origin/master' into xaig_dff
2019-07-01 10:44:42 -07:00
Eddie Hung
38d8806bd7
Add generic __builtin_bswap32 function
2019-06-28 09:59:47 -07:00
Eddie Hung
524af21317
Also fix write_aiger for UB
2019-06-28 09:55:07 -07:00
Eddie Hung
36e2eb06bb
Fix more potential for undefined behaviour due to container invalidation
2019-06-28 09:51:43 -07:00
Eddie Hung
9398921af1
Refactor for one "abc_carry" attribute on module
2019-06-27 16:07:14 -07:00
Eddie Hung
6c256b8cda
Merge origin/master
2019-06-27 11:20:15 -07:00
Eddie Hung
080a5ca536
Improve debugging message for comb loops
2019-06-26 20:02:38 -07:00
Eddie Hung
cec2292b0b
Merge remote-tracking branch 'origin/master' into xaig
2019-06-24 20:01:43 -07:00
Eddie Hung
7903ebe3e0
Carry in/out box ordering now move to end, not swap with end
2019-06-22 14:18:42 -07:00
Eddie Hung
1abe93e48d
Merge remote-tracking branch 'origin/master' into xaig
2019-06-21 17:43:29 -07:00
Eddie Hung
fddb027cab
Replace assert with error message
2019-06-21 17:18:04 -07:00
Eddie Hung
7074ec9cd5
Add log_push()/log_pop() inside write_xaiger
2019-06-21 17:17:29 -07:00
Eddie Hung
65c1199acd
One more workaround for gcc-4.8
2019-06-21 14:36:24 -07:00
Eddie Hung
bd7ec673dd
No point logging constant bit
2019-06-21 14:31:09 -07:00
Eddie Hung
70c93ea0c4
Move comment
2019-06-21 14:31:09 -07:00
Miodrag Milanovic
fde90f7f8e
Fix json formatting
2019-06-21 20:01:40 +02:00
Miodrag Milanovic
50e7221077
Add upto and offset to JSON ports
2019-06-21 19:47:25 +02:00
Clifford Wolf
f15def325c
Added JSON upto and offset
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-21 15:22:17 +02:00
Eddie Hung
6a336ca23e
Fix spacing
2019-06-20 22:30:20 -07:00
Eddie Hung
e21f01d938
Refactor bit2aig for less lookups
2019-06-20 22:10:43 -07:00
Eddie Hung
4422b7311b
Fix gcc invalidation behaviour for write_aiger
2019-06-20 22:10:43 -07:00
Eddie Hung
32f8014e12
Fix gcc error, due to dict invalidation during recursion
2019-06-20 22:10:43 -07:00
Eddie Hung
c4ea6fff65
Fix gcc invalidation behaviour for write_aiger
2019-06-20 21:56:47 -07:00
Eddie Hung
8e56cfb6bb
write_xaiger to flatten 1'bx/1'bz to 1'b0 again
2019-06-20 19:41:27 -07:00
Eddie Hung
ad36eb24c0
Fix different abc9 test
2019-06-20 19:41:27 -07:00
Eddie Hung
9faeba7a66
Fix broken abc9.v test due to inout being 1'bx
2019-06-20 19:41:27 -07:00
Eddie Hung
e612dade12
Merge remote-tracking branch 'origin/master' into xaig
2019-06-20 19:00:36 -07:00
Eddie Hung
4e5836a5fb
Handle COs driven by 1'bx
2019-06-20 17:38:04 -07:00
Eddie Hung
f2d541962e
write_xaiger to skip POs driven by 1'bx
2019-06-20 17:37:54 -07:00
Ben Widawsky
4a18e19fb8
Support filename rewrite in backends
...
Signed-off-by: Ben Widawsky <ben@bwidawsk.net>
2019-06-18 14:39:52 -07:00
Clifford Wolf
c23bbc4291
Add timescale and generated-by header to yosys-smtbmc MkVcd
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-16 23:12:03 +02:00
Eddie Hung
0c59bc0b75
Cleanup
2019-06-16 10:42:00 -07:00
Eddie Hung
fb90d8c18c
Cleanup
2019-06-16 09:34:26 -07:00
Eddie Hung
6852c83bbe
Cleanup write_xaiger
2019-06-15 22:50:15 -07:00
Eddie Hung
bd2690e9b9
Preserve init of flops, and write into XAIG
2019-06-15 22:41:13 -07:00
Eddie Hung
2309459605
Do not treat $__ABC_FF_ as a user cell
2019-06-15 19:36:55 -07:00
Eddie Hung
0debea25a7
Update comment
2019-06-15 18:24:04 -07:00
Eddie Hung
c2f3f116d0
Use $__ABC_FF_ instead of $_FF_
2019-06-15 18:16:14 -07:00
Eddie Hung
6d74b3e004
Update comment
2019-06-15 09:36:02 -07:00
Eddie Hung
357d36ef4f
write_xaiger to treat abc_flop boxes as boxff for ABC
2019-06-15 09:07:03 -07:00
Eddie Hung
7ff8330d1e
Leave breadcrumb behind
2019-06-14 13:34:40 -07:00
Eddie Hung
46e69ee934
Remove redundant condition
2019-06-14 13:31:18 -07:00
Eddie Hung
9b55e69755
Revert "Cleanup/optimise toposort in write_xaiger"
...
This reverts commit 1948e7c846
.
Restores old toposort with optimisations
2019-06-14 13:29:36 -07:00
Eddie Hung
746f70a9ce
Update comment
2019-06-14 13:10:46 -07:00
Eddie Hung
0fa6a441f1
Check that whiteboxes are synthesisable
2019-06-14 13:08:38 -07:00
Eddie Hung
2d85725604
Get rid of compiler warnings
2019-06-14 13:07:56 -07:00
Eddie Hung
7876b5b8be
Cover __APPLE__ too for little to big endian
2019-06-14 12:40:51 -07:00
Eddie Hung
a48b5bfaa5
Further cleanup based on @daveshah1
2019-06-14 12:25:06 -07:00
Eddie Hung
97d2656375
Resolve comments from @daveshah1
2019-06-14 12:00:02 -07:00
Eddie Hung
ee428f73ab
Remove WIP ABC9 flop support
2019-06-14 10:37:52 -07:00
Eddie Hung
1656c44373
Cleanup
2019-06-14 10:29:27 -07:00
Eddie Hung
751e640c1d
Merge branch 'xaig' of github.com:YosysHQ/yosys into xaig
2019-06-14 10:29:16 -07:00
Eddie Hung
1948e7c846
Cleanup/optimise toposort in write_xaiger
2019-06-14 10:13:17 -07:00
David Shah
9566573054
ecp5: Add abc9 option
...
Signed-off-by: David Shah <dave@ds0.me>
2019-06-14 17:15:02 +01:00
Eddie Hung
8374eb1cb4
Remove unnecessary undriven_bits.insert
2019-06-12 15:55:02 -07:00
Eddie Hung
fb2758aade
write_xaiger to preserve POs even if driven by constant
2019-06-12 15:44:30 -07:00
Eddie Hung
2e7b3eee40
Add a couple more tests
2019-06-12 15:43:43 -07:00
Eddie Hung
14e870d4c4
More write_xaiger cleanup
2019-06-12 10:00:57 -07:00
Eddie Hung
4be417f6e1
Cleanup write_xaiger
2019-06-12 09:53:14 -07:00
Eddie Hung
b21d29598a
Consistency
2019-06-12 09:40:51 -07:00
Eddie Hung
7b186740d3
Add log_assert to ensure no loops
2019-06-04 12:01:25 -07:00
Eddie Hung
1b836c93bb
Only toposort builtin and abc types
2019-06-04 11:56:58 -07:00
Eddie Hung
257f7ff5f6
When creating new holes cell, inherit parameters too
2019-06-03 12:30:54 -07:00
Eddie Hung
4623177655
ABC9 to understand flops
2019-05-31 15:23:33 -07:00
Eddie Hung
eb08e71bd1
Merge branch 'xaig' into xc7mux
2019-05-31 13:03:03 -07:00
Eddie Hung
887c31f33b
Fix issue where keep signal became PI, but also box was adding CI driver
2019-05-30 16:03:22 -07:00
Eddie Hung
e3c8132d7a
Do not re-sort box_module ports
2019-05-30 12:26:51 -07:00
Eddie Hung
fdfc18be91
Carry in/out to be the last input/output for chains to be preserved
2019-05-30 01:23:36 -07:00
Eddie Hung
1423384367
Fix abc_test024
2019-05-29 15:24:09 -07:00
Eddie Hung
b4321a31bb
Fix for abc9_test022
2019-05-28 12:42:17 -07:00
Eddie Hung
13e233217c
Small improvement
2019-05-28 11:29:59 -07:00
Eddie Hung
914074a07c
Update from master
2019-05-28 09:35:45 -07:00
Eddie Hung
3f60061615
Map file to include boxes not CI/CO
2019-05-27 23:10:59 -07:00
Eddie Hung
234156c01a
Instantiate cell type (from sym file) otherwise 'clean' warnings
2019-05-27 12:16:10 -07:00
Eddie Hung
03b289a851
Add 'cinput' and 'coutput' to symbols file for boxes
2019-05-27 11:38:52 -07:00
Eddie Hung
3c8368454f
Fix "a" connectivity
2019-05-26 14:14:13 -07:00
Eddie Hung
67f7c64a77
Fix padding, remove CIs from undriven_bits before erasing undriven POs
2019-05-26 11:26:38 -07:00
Eddie Hung
32a4c10c0d
Fix "a" extension
2019-05-26 02:44:36 -07:00
Eddie Hung
01684643b6
Fix "write_xaiger", and to write each box contents into holes
2019-05-25 22:34:50 -07:00
Eddie Hung
73c98f2ae2
Merge remote-tracking branch 'origin/master' into xc7mux
2019-05-25 20:50:47 -07:00
Clifford Wolf
6352df42ae
Fix handling of offset and upto module ports in write_blif, fixes #1040
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-05-25 17:45:14 +02:00
Clifford Wolf
b7dd7c2dcd
Add proper error message for btor recursion_guard
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-05-24 16:22:34 +02:00
Eddie Hung
68359bcd6f
Merge remote-tracking branch 'origin/eddie/opt_rmdff' into xc7mux
2019-05-23 13:37:53 -07:00
Eddie Hung
0f094fba08
Pad all boxes so that all input/output connections specified
2019-05-21 16:19:23 -07:00
Eddie Hung
fb09c6219b
Merge remote-tracking branch 'origin/master' into xc7mux
2019-05-21 14:21:00 -07:00
Jim Lawson
a5131e2896
Fix static shift operands, neg result type, minor formatting
...
Static shift operands must be constants.
The result of FIRRTL's neg operator is signed.
Fix poor indentation for gen_read().
2019-05-21 13:04:56 -07:00
Clifford Wolf
3870e7cf29
Merge pull request #991 from kristofferkoch/gcc9-warnings
...
Fix all warnings that occurred when compiling with gcc9
2019-05-08 11:25:22 +02:00
Kristoffer Ellersgaard Koch
30c762d3a1
Fix all warnings that occurred when compiling with gcc9
2019-05-08 10:27:14 +02:00
Clifford Wolf
33738c1745
Fix handling of partial init attributes in write_verilog, fixes #997
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-05-07 19:55:36 +02:00
Clifford Wolf
1cd1b5fc1a
Add "real" keyword to ilang format
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-05-06 12:00:40 +02:00
Clifford Wolf
87426f5a06
Improve write_verilog specify support
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-05-04 08:46:24 +02:00
Eddie Hung
d9c4644e88
Merge remote-tracking branch 'origin/master' into clifford/specify
2019-05-03 15:05:57 -07:00
Eddie Hung
5cd19b52da
Merge remote-tracking branch 'origin/master' into xc7mux
2019-05-02 10:44:59 -07:00
Jim Lawson
6ea09caf01
Re-indent firrtl.cc:struct memory - no functional change.
2019-05-01 16:21:13 -07:00
Jim Lawson
38f5424f92
Fix #938 - Crash occurs in case when use write_firrtl command
...
Add missing memory initialization.
Sanity-check memory parameters.
Add Cell pointer to memory object (for error reporting).
2019-05-01 13:16:01 -07:00
Eddie Hung
eec314e262
Remove topo sort no-loop assertion, with test
2019-04-24 21:06:53 -07:00
Eddie Hung
ac2aff9e28
Fix abc9 with (* keep *) wires
2019-04-23 16:11:39 -07:00
Eddie Hung
bfd71e0990
Fix abc9 with (* keep *) wires
2019-04-23 16:11:14 -07:00
Clifford Wolf
e807e88b60
Rename T_{RISE,FALL}_AVG to T_{RISE,FALL}_TYP to better match verilog std nomenclature
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-04-23 21:36:59 +02:00
Clifford Wolf
846eb5ea98
Add $specify2/$specify3 support to write_verilog
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-04-23 21:36:59 +02:00
Clifford Wolf
0bf9d0087c
Add support for $assert/$assume/$cover to write_verilog
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-04-23 21:36:59 +02:00
Eddie Hung
8f30019b68
Revert "Temporarily remove 'r' extension"
...
This reverts commit eaf3c24772
.
2019-04-22 17:41:21 -07:00
Eddie Hung
eaf3c24772
Temporarily remove 'r' extension
2019-04-22 11:54:19 -07:00
Eddie Hung
b780c0a7de
Allow POs to be PIs in XAIG
2019-04-22 11:22:29 -07:00
Eddie Hung
4883391b63
Merge remote-tracking branch 'origin/master' into xaig
2019-04-22 11:19:52 -07:00
Clifford Wolf
0e0c80fac8
Add support for zero-width signals to Verilog back-end, fixes #948
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-04-22 19:44:42 +02:00
Eddie Hung
caec7f9d2c
Merge remote-tracking branch 'origin/master' into xaig
2019-04-20 12:23:49 -07:00
Clifford Wolf
f84a84e3f1
Merge pull request #943 from YosysHQ/clifford/whitebox
...
[WIP] Add "whitebox" attribute, add "read_verilog -wb"
2019-04-20 20:51:54 +02:00
Eddie Hung
76bba49182
Fixes for simple_abc9 tests
2019-04-19 15:47:36 -07:00
Clifford Wolf
148caecca3
Change "ne" to "neq" in btor2 output
...
we need to do this because they changed the parser:
e97fc9ceda
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-04-19 21:17:12 +02:00
Eddie Hung
35f44f3ae8
Do not assume inst_module is always present
2019-04-19 08:44:53 -07:00
Eddie Hung
3544a7cd7b
ignore_boxes -> holes_mode
2019-04-19 08:37:10 -07:00
Eddie Hung
8f93999129
Revert "write_json to not write contents (cells/wires) of whiteboxes"
...
This reverts commit 4ef03e19a8
.
2019-04-18 23:05:59 -07:00
Eddie Hung
6bdf98d591
Add flop support for write_xaiger
2019-04-18 17:43:13 -07:00
Eddie Hung
b531efd6d9
Spelling
2019-04-18 17:35:16 -07:00
Eddie Hung
4c327cf316
Use new -wb flag for ABC flow
2019-04-18 10:32:41 -07:00
Eddie Hung
4ef03e19a8
write_json to not write contents (cells/wires) of whiteboxes
2019-04-18 10:32:00 -07:00
Eddie Hung
79881141e2
write_json to not write contents (cells/wires) of whiteboxes
2019-04-18 10:30:45 -07:00
Eddie Hung
8fe0a961b3
Merge remote-tracking branch 'origin/clifford/whitebox' into xaig
2019-04-18 09:00:06 -07:00
Clifford Wolf
f4abc21d8a
Add "whitebox" attribute, add "read_verilog -wb"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-04-18 17:45:47 +02:00
Eddie Hung
23cd2e5de0
Fix $anyseq warning and cleanup
2019-04-17 16:03:29 -07:00
Eddie Hung
1ec5f18346
Cope with inout ports
2019-04-17 14:43:45 -07:00
Eddie Hung
2b860809e9
Stop topological sort at abc_flop_q
2019-04-17 12:28:19 -07:00
Eddie Hung
d59185f1d6
Remove init* from xaiger, also topo-sort cells for box flow
2019-04-17 11:08:42 -07:00
Eddie Hung
5c134980c4
Optimise
2019-04-16 21:05:44 -07:00
Eddie Hung
e7a8955818
CIs before PIs; also sort each cell's connections before iterating
2019-04-16 16:37:47 -07:00
Eddie Hung
55a3638c71
Port from xc7mux branch
2019-04-16 15:01:45 -07:00
Eddie Hung
fe0b421212
Output __const0__ and __const1__ CIs
2019-04-12 18:16:25 -07:00
Eddie Hung
686e772f0b
ci_bits and co_bits now a list, order is important for ABC
2019-04-12 16:17:48 -07:00
Eddie Hung
c748391730
WIP
2019-04-12 14:13:11 -07:00
Eddie Hung
2217d59e29
Add non-input bits driven by unrecognised cells as ci_bits
2019-04-10 18:06:33 -07:00
Eddie Hung
bca3cf6843
Merge branch 'master' into xaig
2019-04-08 16:31:59 -07:00
Jim Lawson
73b87e7807
Refine memory support to deal with general Verilog memory definitions.
2019-04-01 15:02:12 -07:00
Clifford Wolf
1eff8be8f0
Add support for memory initialization to write_btor
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-23 14:40:01 +01:00
Clifford Wolf
e78f5a3055
Fix BTOR output tags syntax in writye_btor
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-23 14:39:42 +01:00
Clifford Wolf
bacca57537
Fix smtbmc.py handling of zero appended steps
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 22:04:42 +01:00
Clifford Wolf
04e920337b
Fix a syntax bug in ilang backend related to process case statements
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-14 17:50:20 +01:00
Clifford Wolf
53b28b3f01
Merge pull request #869 from cr1901/win-shell
...
Install launcher executable when running yosys-smtbmc on Windows.
2019-03-14 16:43:23 +01:00
William D. Jones
ff15cf9b1f
Install launcher executable when running yosys-smtbmc on Windows.
...
Signed-off-by: William D. Jones <thor0505@comcast.net>
2019-03-13 13:49:16 -04:00
Clifford Wolf
20c6a8c9b0
Improve determinism of IdString DB for similar scripts
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-11 20:12:28 +01:00
Clifford Wolf
94f995ee37
Fix signed $shift/$shiftx handling in write_smt2
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-09 13:19:41 -08:00
Clifford Wolf
5dfc7becca
Use SVA label in smt export if available
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-07 11:31:46 -08:00
Jim Lawson
d6c4dfb902
Ensure fid() calls make_id() for consistency; tests/simple/dff_init.v fails
...
Mark dff_init.v as expected to fail since it uses "initial value".
2019-03-04 13:37:23 -08:00
Clifford Wolf
03237de686
Fix "write_edif -gndvccy"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-01 12:59:07 -08:00
Clifford Wolf
241901461a
Add "write_verilog -siminit"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-28 15:03:03 -08:00
Larry Doolittle
e2fc18f27b
Reduce amount of trailing whitespace in code base
2019-02-28 14:58:11 -08:00
Clifford Wolf
6d143c9a01
Merge pull request #827 from ucb-bar/firrtlfixes
...
Fix FIRRTL to Verilog process instance subfield assignment.
2019-02-28 14:45:04 -08:00
Clifford Wolf
f570aa5e1d
Fix smt2 code generation for partially initialized memowy words, fixes #831
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-28 12:15:58 -08:00
Eddie Hung
8e883d92ed
write_xaiger to behave for undriven/unused inouts
2019-02-26 12:17:51 -08:00
Eddie Hung
c492a3a1c4
write_xaiger duplicate inout port into out port with $inout.out suffix
2019-02-25 18:39:36 -08:00
Jim Lawson
171c425cf9
Fix FIRRTL to Verilog process instance subfield assignment.
...
Don't emit subfield assignments: bits(x, y, z) <= ... - but instead, add them to the reverse-wire-map where they'll be treated at the end of the module.
Enable tests which were disabled due to incorrect treatment of subfields.
Assume the `$firrtl2verilog` variable contains any additional switches to control verilog generation (i.e. `--no-dedup -X mverilog`)
2019-02-25 16:18:13 -08:00
Eddie Hung
292f80d231
Cleanup abc9 code
2019-02-25 15:20:56 -08:00
Eddie Hung
5180338e80
write_xaiger to write __dummy_o__ for -symbols too
2019-02-21 17:03:18 -08:00
Eddie Hung
085ed9f487
Add attribution
2019-02-21 14:40:13 -08:00
Eddie Hung
2f96a0ed32
write_xaiger to use original bit for co, not sigmap()-ed bit
2019-02-21 11:15:25 -08:00
Eddie Hung
01f8d50ba2
Remove swap file
2019-02-20 16:17:01 -08:00
Eddie Hung
f89b112fbf
write_aiger: fix CI/CO and symbols
2019-02-20 15:35:32 -08:00
Eddie Hung
ef60ca1717
write_xaiger to not write latches, CO/PO fixes
2019-02-20 11:09:13 -08:00
Eddie Hung
f9af902532
Merge branch 'master' into xaig
2019-02-19 14:20:04 -08:00
Eddie Hung
11480b4fa3
Instead of INIT param on cells, use initial statement with hier ref as
...
per @cliffordwolf
2019-02-17 12:18:12 -08:00
Eddie Hung
17cd5f759f
Merge https://github.com/YosysHQ/yosys into dff_init
2019-02-17 11:49:06 -08:00
Eddie Hung
30f1204721
Cleanup
2019-02-16 22:22:17 -08:00
Eddie Hung
76c35f80f4
Cleanup
2019-02-16 21:09:48 -08:00
Eddie Hung
6a57de9013
write_xaiger to support non-bit cell connections, and cope with COs for -O
2019-02-16 21:00:39 -08:00
Eddie Hung
b9a305b85d
write_aiger -O to write dummy output as __dummy_o__
2019-02-16 20:08:59 -08:00
Eddie Hung
0c409e6d8c
Tidy up write_xaiger
2019-02-16 08:48:33 -08:00
Eddie Hung
2c1655ae94
write_aiger() to perform CI/CO post-processing and fix symbols
2019-02-16 08:46:25 -08:00
Eddie Hung
486a270415
Fixes needed for DFF circuits
2019-02-15 15:22:18 -08:00
Jim Lawson
c245041bfe
Removed unused variables, functions.
2019-02-15 12:00:28 -08:00
Eddie Hung
3ac5b65197
write_xaiger to cope with unknown cells by transforming them to CI/CO
2019-02-15 11:51:21 -08:00
Jim Lawson
fc1c9aa11f
Update cells supported for verilog to FIRRTL conversion.
...
Issue warning messages for missing parameterized modules and attempts to set initial values.
Replace simple "if (cell-type)" with "else if" chain.
Fix FIRRTL shift handling.
Add support for parameterized modules, $shift, $shiftx.
Handle default output file.
Deal with no top module.
Automatically run pmuxtree pass.
Allow EXTRA_FLAGS and SEED parameters to be set in the environment for tests/tools/autotest.mk.
Support FIRRTL regression testing in tests/tools/autotest.sh
Add xfirrtl files to test directories to exclude files from FIRRTL regression tests that are known to fail.
2019-02-15 11:14:17 -08:00
Eddie Hung
c69fba8de5
More cleanup
2019-02-14 14:52:47 -08:00
Eddie Hung
7328775584
More cleanup of write_xaiger
2019-02-14 14:48:38 -08:00
Eddie Hung
afa4389445
Get rid of formal stuff from xaiger backend
2019-02-14 13:27:26 -08:00
Eddie Hung
f0f5d8a5cc
Merge remote-tracking branch 'origin/read_aiger' into xaig
2019-02-13 14:09:36 -08:00
Eddie Hung
06cf0555ee
Merge https://github.com/YosysHQ/yosys into xaig
2019-02-13 14:08:31 -08:00
Clifford Wolf
1f2548a564
Merge pull request #802 from whitequark/write_verilog_async_mem_ports
...
write_verilog: correctly emit asynchronous transparent ports
2019-02-12 14:41:34 +01:00
Eddie Hung
ecd2446132
Add write_xaiger
2019-02-11 15:18:42 -08:00
Eddie Hung
db08afe146
Copy backends/aiger/aiger.cc to xaiger.cc
2019-02-08 14:53:12 -08:00
Eddie Hung
20ca795b87
Remove check for cell->name[0] == '$'
2019-02-06 14:53:40 -08:00
Eddie Hung
c373640a3a
Refactor
2019-02-06 14:28:44 -08:00
Eddie Hung
8241db6960
write_verilog to cope with init attr on q when -noexpr
2019-02-06 14:17:09 -08:00
Clifford Wolf
e112d2fbf5
Add missing blackslash-to-slash convertion to smtio.py (matching Smt2Worker::get_id() behavior)
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-06 16:35:59 +01:00
whitequark
da65e1e8d9
write_verilog: correctly emit asynchronous transparent ports.
...
This commit fixes two related issues:
* For asynchronous ports, clock is no longer added to domain list.
(This would lead to absurd constructs like `always @(posedge 0)`.
* The logic to distinguish synchronous and asynchronous ports is
changed to correctly use or avoid clock in all cases.
Before this commit, the following RTLIL snippet (after memory_collect)
cell $memrd $2
parameter \MEMID "\\mem"
parameter \ABITS 2
parameter \WIDTH 4
parameter \CLK_ENABLE 0
parameter \CLK_POLARITY 1
parameter \TRANSPARENT 1
connect \CLK 1'0
connect \EN 1'1
connect \ADDR \mem_r_addr
connect \DATA \mem_r_data
end
would lead to invalid Verilog:
reg [1:0] _0_;
always @(posedge 1'h0) begin
_0_ <= mem_r_addr;
end
assign mem_r_data = mem[_0_];
Note that there are two potential pitfalls remaining after this
change:
* For asynchronous ports, the \EN input and \TRANSPARENT parameter
are silently ignored. (Per discussion in #760 this is the correct
behavior.)
* For synchronous transparent ports, the \EN input is ignored. This
matches the behavior of the $mem simulation cell. Again, see #760 .
2019-01-29 02:24:00 +00:00
Clifford Wolf
81581f24fc
Merge pull request #800 from whitequark/write_verilog_tribuf
...
write_verilog: write $tribuf cell as ternary
2019-01-27 09:23:41 +01:00
whitequark
3d7925ad9f
write_verilog: write $tribuf cell as ternary.
2019-01-27 00:24:06 +00:00
whitequark
42c47a83da
write_verilog: escape names that match SystemVerilog keywords.
2019-01-27 00:03:53 +00:00
Clifford Wolf
54dc33b905
Add "write_edif -gndvccy"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-17 13:33:11 +01:00
Clifford Wolf
6c5049f016
Fix handling of $shiftx in Verilog back-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-15 10:55:27 +01:00
whitequark
efa278e232
Fix typographical and grammatical errors and inconsistencies.
...
The initial list of hits was generated with the codespell command
below, and each hit was evaluated and fixed manually while taking
context into consideration.
DIRS="kernel/ frontends/ backends/ passes/ techlibs/"
DIRS="${DIRS} libs/ezsat/ libs/subcircuit"
codespell $DIRS -S *.o -L upto,iff,thru,synopsys,uint
More hits were found by looking through comments and strings manually.
2019-01-02 13:12:17 +00:00
Larry Doolittle
99706b3bf4
Squelch a little more trailing whitespace
2018-12-29 12:46:54 +01:00
Clifford Wolf
23bb77867f
Minor style fixes
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-18 20:02:39 +01:00
makaimann
abf5930a33
Add btor ops for $mul, $div, $mod and $concat
2018-12-17 10:45:17 -08:00
whitequark
ca866d384e
write_verilog: handle the $shift cell.
...
The implementation corresponds to the following Verilog, which is
lifted straight from simlib.v:
module \\$shift (A, B, Y);
parameter A_SIGNED = 0;
parameter B_SIGNED = 0;
parameter A_WIDTH = 0;
parameter B_WIDTH = 0;
parameter Y_WIDTH = 0;
input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
output [Y_WIDTH-1:0] Y;
generate
if (B_SIGNED) begin:BLOCK1
assign Y = $signed(B) < 0 ? A << -B : A >> B;
end else begin:BLOCK2
assign Y = A >> B;
end
endgenerate
endmodule
2018-12-16 18:46:32 +00:00
Clifford Wolf
ddff75b60a
Merge pull request #736 from whitequark/select_assert_list
...
select: print selection if a -assert-* flag causes an error
2018-12-16 16:45:49 +01:00
whitequark
fccaa25ec1
write_verilog: add a missing newline.
2018-12-16 15:22:34 +00:00
Clifford Wolf
f481ad4d44
Merge pull request #729 from whitequark/write_verilog_initial
...
write_verilog: correctly map RTLIL `sync init`
2018-12-16 15:50:16 +01:00
Clifford Wolf
0b9bb852c6
Add yosys-smtbmc support for btor witness
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-10 03:43:07 +01:00
Clifford Wolf
47a5dfdaa4
Add "yosys-smtbmc --btorwit" skeleton
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-08 06:59:27 +01:00
Clifford Wolf
ed3c57fad3
Fix btor init value handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-08 06:21:31 +01:00
whitequark
7fe770a441
write_verilog: correctly map RTLIL `sync init`.
2018-12-07 18:55:08 +00:00
Clifford Wolf
82aaf6d908
Add "write_aiger -I -O -B"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-12 09:27:33 +01:00
Clifford Wolf
825b4c1aa9
Merge pull request #693 from YosysHQ/rlimit
...
improve rlimit handling in smtio.py
2018-11-07 20:16:40 +01:00
Clifford Wolf
b54bf7c0f9
Limit stack size to 16 MB on Darwin
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-07 15:32:34 +01:00
Clifford Wolf
f6c4485a3a
Run solver in non-incremental mode whem smtio.py is configured for non-incremental solving
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-06 11:11:05 +01:00
Clifford Wolf
4c50e3abb9
Fix for improved smtio.py rlimit code
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-06 10:09:03 +01:00
Clifford Wolf
79075d123f
Improve stack rlimit code in smtio.py
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-06 10:05:23 +01:00
Arjen Roodselaar
2b93542171
Use conservative stack size for SMT2 on MacOS
2018-11-04 21:58:09 -08:00
Clifford Wolf
d0acea4f2e
Add proper error message for when smtbmc "append" fails
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-04 14:41:28 +01:00
Clifford Wolf
b6781c6f4b
Add support for signed $shift/$shiftx in smt2 back-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-01 11:40:58 +01:00
rafaeltp
c7770d9eea
adding offset info to memories
2018-10-18 16:22:33 -07:00
rafaeltp
609f46eeb7
adding offset info to memories
2018-10-18 16:20:21 -07:00
Clifford Wolf
f4ad05e133
Merge pull request #663 from aman-goel/master
...
Update to .smv backend
2018-10-17 12:18:57 +02:00
Aman Goel
749b3ed62a
Minor update
2018-10-15 13:54:12 -04:00
Clifford Wolf
115ca57647
Add "write_edif -attrprop"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-10-05 09:41:30 +02:00
Aman Goel
90e0938f9a
Update to .smv backend
...
Splitting VAR and ASSIGN into IVAR, VAR, DEFINE and ASSIGN. This allows better handling by nuXmv for post-processing (since now only state variables are listed under VAR).
2018-10-01 19:03:10 -04:00
Miodrag Milanovic
41affeeeb9
added prefix to FDirection constants, fixing windows build
2018-09-21 20:43:49 +02:00
acw1251
efac8a45a6
Fixed typo in "verilog_write" help message
2018-09-18 13:34:30 -04:00
Clifford Wolf
12440fcc8f
Add $lut support to Verilog back-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-09-06 00:18:01 +02:00
Jim Lawson
380c6f0e97
Remove unused functions.
2018-08-27 10:18:33 -07:00
Jim Lawson
93d19dc2fb
Add support for module instances.
...
Don't pad logical operands to one bit.
Use operand width and signedness in $reduce_bool.
Shift amounts are unsigned and shouldn't be padded.
Group "is invalid" with the wire declaration, not its use (otherwise it is incorrectly wired to 0).
2018-08-23 14:35:11 -07:00
Clifford Wolf
67b1026297
Merge pull request #591 from hzeller/virtual-override
...
Consistent use of 'override' for virtual methods in derived classes.
2018-08-15 14:05:38 +02:00
Clifford Wolf
dfc0c8ffc8
Merge pull request #576 from cr1901/no-resource
...
Gate POSIX-only signals and resource module to only run on POSIX Pyth…
2018-08-15 14:00:19 +02:00
Clifford Wolf
1dd156f516
Fix use of signed integers in JSON back-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-08-14 23:31:25 +02:00
jpathy
7db05b2cc1
Use `realpath`
...
Use `os.path.realpath` instead to make sure symlinks are followed. This is also required to work for nix package manager.
2018-08-06 06:51:07 +00:00
Henner Zeller
3aa4484a3c
Consistent use of 'override' for virtual methods in derived classes.
...
o Not all derived methods were marked 'override', but it is a great
feature of C++11 that we should make use of.
o While at it: touched header files got a -*- c++ -*- for emacs to
provide support for that language.
o use YS_OVERRIDE for all override keywords (though we should probably
use the plain keyword going forward now that C++11 is established)
2018-07-20 23:51:06 -07:00
William D. Jones
0caa62802c
Gate POSIX-only signals and resource module to only run on POSIX Python implementations.
2018-07-06 01:44:34 -04:00
Sergiusz Bazanski
1690dafde1
Fix protobuf build
2018-06-20 19:28:43 +01:00
Serge Bazanski
53e9a1549c
Add Protobuf backend
...
Signed-off-by: Serge Bazanski <q3k@symbioticeda.com>
2018-06-19 13:34:56 +01:00
Clifford Wolf
d9a2b43014
Add $dlatch support to write_verilog
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-22 16:03:26 +02:00
Clifford Wolf
5ca91ca019
Add "write_blif -inames -iattr"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-15 14:07:21 +02:00
Clifford Wolf
4d6af2969c
Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-04 18:12:27 +02:00
Clifford Wolf
25a864fc73
Fixed -stbv handling in SMT2 back-end
2018-04-04 17:28:07 +02:00
Clifford Wolf
dd5fab69c1
Add smtio status msgs when --progress is inactive
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 21:59:30 +02:00
Clifford Wolf
a48c7e5abf
Bugfix in smtio.py VCD file generator
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 12:45:31 +02:00
Clifford Wolf
77bd645c35
Add $mem support to SMT2 clock tagging
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-27 02:11:20 +02:00
Clifford Wolf
3f00702475
Improve yosys-smtbmc log output and error handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-17 18:06:17 +01:00
Clifford Wolf
4d4e3a8ca6
Improve handling of invalid check-sat result in smtio.py
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-17 12:17:53 +01:00
Clifford Wolf
3545c0fffb
Remove debug prints from yosys-smtbmc VCD writer
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-08 16:24:35 +01:00
Clifford Wolf
8b604004da
Check results of (check-sat) in yosys-smtbmc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-07 22:54:19 +01:00
Clifford Wolf
cedbc35f4b
Imporove yosys-smtbmc error handling, Improve VCD output
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-05 12:17:22 +01:00
Clifford Wolf
8b7602e660
Improve SMT2 encoding of $reduce_{and,or,bool}
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-04 21:22:20 +01:00
Clifford Wolf
45a6fce92c
Fix a hangup in yosys-smtbmc error handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-04 21:13:30 +01:00
Clifford Wolf
ae4e204c76
Improved error handling in yosys-smtbmc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-03 20:00:07 +01:00
Clifford Wolf
a44e1edaa3
Terminate running SMT solver when smtbmc is terminated
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-03 14:50:40 +01:00
Clifford Wolf
3ced2cca6e
Fix smtbmc smtc/aiw parser for wire names containing []
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-03 14:15:49 +01:00
Clifford Wolf
90ae426078
Mangle names with square brackets in VCD files to work around issues in gtkwave
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-01 14:15:27 +01:00
Clifford Wolf
675dd5347a
Small fixes and improvements in $allconst/$allseq handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-26 11:58:44 +01:00
Clifford Wolf
b13e6bd375
Add smtbmc support for exist-forall problems
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-23 19:33:30 +01:00
Clifford Wolf
17583b6a21
Add support for mockup clock signals in yosys-smtbmc vcd output
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-20 17:45:22 +01:00
Clifford Wolf
c9672e2e2e
Fix handling of zero-length cell connections in SMT2 back-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-02-08 19:12:12 +01:00
Clifford Wolf
e4f0218907
Fixed gcc 7.2 "statement will never be executed" warning
2018-02-03 14:31:47 +01:00
Clifford Wolf
e97f10b142
Fix smtio.py for large SMT2 S-expressions
2018-01-29 12:34:28 +01:00
Clifford Wolf
54aeca0983
Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output
2018-01-18 14:25:22 +01:00
Clifford Wolf
9804ebedbf
Add "no driver for signal bit" error msg to btor back-end
2017-12-24 17:30:36 +01:00
Clifford Wolf
292984896b
Simple fix BTOR memory encoding
2017-12-17 18:57:54 +01:00
Clifford Wolf
bbdcc1f9d4
Improve BTOR memory encoding
2017-12-17 18:55:17 +01:00
Clifford Wolf
30f23281ed
Add array support to btor back-end
2017-12-15 02:19:06 +01:00
Clifford Wolf
ad901671c5
Add $anyconst/$anyseq support to btor back-end
2017-12-15 00:40:24 +01:00
Clifford Wolf
162c29bd6b
Merge branch 'master' into btor-ng
2017-12-14 03:13:47 +01:00
Clifford Wolf
9419de3e37
Add yosys-smtbmc VCD writer support for memories with async writes
2017-12-14 03:06:00 +01:00
Clifford Wolf
a48ec49017
Merge branch 'master' into btor-ng
2017-12-14 02:17:01 +01:00
Clifford Wolf
2625da6440
Add smt2 back-end support for async write memories
2017-12-14 02:07:10 +01:00
Clifford Wolf
546de7fa4f
Add "write_btor -s" mode
2017-12-13 00:15:44 +01:00
Clifford Wolf
0881bbf2e7
Add state initval handling to btor back-end
2017-12-12 23:44:08 +01:00
Clifford Wolf
f697282246
Add btor back-end support for 'x' constants
2017-12-12 21:48:55 +01:00
Clifford Wolf
82d1fd77de
Add btor $shift/$shiftx support
2017-12-11 14:24:19 +01:00
Clifford Wolf
cc119b5232
Fix btor back-end shift handling
2017-12-10 08:40:11 +01:00
Clifford Wolf
133a0f4978
Add support for $pmux in btor back-end
2017-12-10 08:11:08 +01:00
Clifford Wolf
83cf736309
Add support for more cell types to btor back-end
2017-12-10 07:16:47 +01:00
Clifford Wolf
63343aeaaa
Fix btor concat
2017-12-09 05:58:14 +01:00
Clifford Wolf
da91b31bb2
Fixed "yosys-smtbmc -g" handling of no solution
2017-11-27 19:43:36 +01:00
Clifford Wolf
b981e5aa69
Fixed "yosys-smtbmc -g" handling of no solution
2017-11-27 17:42:32 +01:00
Clifford Wolf
e3a51b3e87
Bugfixes in new BTOR back-end
2017-11-24 18:13:41 +01:00
Clifford Wolf
60d1129506
Progress in new BTOR back-end
2017-11-23 23:44:39 +01:00
Clifford Wolf
b3d6b277ea
Progress in new BTOR back-end
2017-11-23 18:50:10 +01:00
Clifford Wolf
cc2495d48d
Progress in new BTOR back-end
2017-11-23 18:14:53 +01:00
Clifford Wolf
e41dcaa759
Progress with new BTOR backend
2017-11-23 08:28:29 +01:00
Clifford Wolf
6ee305553a
Add skeleton for new BTOR back-end
2017-11-23 06:38:57 +01:00
Clifford Wolf
eceacdb9a3
Remove old BTOR back-end
2017-11-23 04:28:51 +01:00
Clifford Wolf
455c1c9d97
Fix SMT2 handling of initstate in sub-modules
2017-10-29 13:21:20 +01:00
Clifford Wolf
1170508264
Improve smtio performance by using reader thread, not writer thread
2017-10-26 01:01:55 +02:00
Clifford Wolf
f513494f5f
Use separate writer thread for talking to SMT solver to avoid read/write deadlock
2017-10-25 19:59:56 +02:00
Clifford Wolf
76326c163a
Improve p_* functions in smtio.py
2017-10-25 15:45:32 +02:00
Clifford Wolf
c672c321e3
Capsulate smt-solver read/write in separate functions
2017-10-25 13:37:11 +02:00
Clifford Wolf
dd46d76394
Fix a bug in yosys-smtbmc in ROM handling
2017-10-25 13:05:14 +02:00
Clifford Wolf
adf1754729
Add $shiftx support to verilog front-end
2017-10-07 13:40:54 +02:00
Clifford Wolf
65f91e5120
Rename "write_verilog -nobasenradix" to "write_verilog -decimal"
2017-10-03 17:31:21 +02:00
dh73
e480847753
Fixed wrong declaration in Verilog backend
2017-10-01 11:11:32 -05:00
dh73
cbaba62401
Adding Cyclone IV (E, GX), Arria 10, Cyclone V and LPM functions (ALTPLL and M9K); M9K is not finished yet. Achronix Speedster also in this commit. Both Arria10 and Speedster-i are still experimental due complexity, but you can experiment around those devices right now
2017-10-01 11:04:17 -05:00
Clifford Wolf
c2d737457a
Fix bug in write_smt2 (export logic driving hierarchical cells before exporting regs)
2017-08-25 11:44:48 +02:00
Clifford Wolf
48b2b376d0
Add "yosys-smtbmc --smtc-init --smtc-top --noinit"
2017-08-04 17:09:08 +02:00
Clifford Wolf
3a8f6f0f51
Add verilator support to testbenches generated by yosys-smtbmc
2017-07-21 14:33:29 +02:00
Clifford Wolf
10c7709e68
Generate FSM-style testbenches in smtbmc
2017-07-12 15:57:04 +02:00
Clifford Wolf
4a8c131fa7
Fix the fixed handling of x-bits in EDIF back-end
2017-07-11 17:45:29 +02:00
Clifford Wolf
479be3cec7
Fix handling of x-bits in EDIF back-end
2017-07-11 17:38:19 +02:00
Clifford Wolf
9557fd2a36
Add attributes and parameter support to JSON front-end
2017-07-10 13:17:38 +02:00
Clifford Wolf
3c693b6561
Change s/asserts/assertions/ in yosys-smtbmc log messages
2017-07-07 11:52:25 +02:00
Clifford Wolf
8f7404f82c
Add "yosys-smtbmc --presat"
2017-07-07 02:47:30 +02:00
Clifford Wolf
5442554e6f
Fix generation of multiple outputs for same AIG node in write_aiger
2017-07-05 14:23:54 +02:00
Clifford Wolf
37af6294bd
Add write_table command
2017-07-05 12:13:53 +02:00
Clifford Wolf
3e0948e16f
Remove unneeded delays in smtbmc vlogtb
2017-07-03 15:37:17 +02:00
Clifford Wolf
287831dca3
Include output ports with constant driver in AIGER output
2017-07-03 14:53:17 +02:00
Clifford Wolf
ea805af6f5
Add "yosys-smtbmc --vlogtb-top"
2017-07-01 18:19:23 +02:00
Clifford Wolf
7d2fb6e2fc
Fix smtbmc vlogtb bug in $anyseq handling
2017-07-01 02:13:32 +02:00
Clifford Wolf
8f8baccfde
Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand const reg"
2017-06-07 12:30:24 +02:00
Clifford Wolf
c365e33fd7
Fix AIGER back-end for multiple symbols per input/latch/output/property
2017-05-30 19:09:11 +02:00
Clifford Wolf
9ed4c9d710
Improve write_aiger handling of unconnected nets and constants
2017-05-28 11:31:35 +02:00
Clifford Wolf
d9201b85f3
Change default smt2 solver to yices (Yices 2 has switched its license to GPL)
2017-05-27 11:56:01 +02:00
Clifford Wolf
2122ae69b3
Add workaround for CBMC bug to SimpleC back-end
2017-05-17 21:07:54 +02:00
Clifford Wolf
05cdd58c8d
Add $_ANDNOT_ and $_ORNOT_ gates
2017-05-17 09:08:29 +02:00
Clifford Wolf
9f4fbc5e74
Add <modname>_init() function generator to simpleC back-end
2017-05-16 19:34:07 +02:00
Clifford Wolf
35be567605
Improve simplec back-end
2017-05-16 08:50:23 +02:00
Clifford Wolf
8d3c706459
Improve simplec back-end
2017-05-15 13:21:59 +02:00
Clifford Wolf
9c397ea78b
Improve simplec back-end
2017-05-14 13:14:49 +02:00
Clifford Wolf
628daab277
Improve simplec back-end
2017-05-13 18:47:31 +02:00
Clifford Wolf
ef7594ce3d
Improve simplec back-end
2017-05-12 22:39:16 +02:00
Clifford Wolf
7931e1ebb4
Added support for more gate types to simplec back-end
2017-05-12 17:42:31 +02:00
Clifford Wolf
bd4ed19887
Add first draft of simple C back-end
2017-05-12 14:13:33 +02:00
Clifford Wolf
1a4b7c6bfa
Fix boolector support in yosys-smtbmc
2017-05-08 14:33:22 +02:00
Clifford Wolf
106e44f406
Add "write_smt2 -stdt" mode
2017-03-20 12:00:35 +01:00
Clifford Wolf
0ac72e759d
Add generation of logic cells to EDIF back-end runtest.py
2017-03-19 14:57:40 +01:00
Clifford Wolf
850f8299a9
Fix EDIF: portRef member 0 is always the MSB bit
2017-03-19 14:53:28 +01:00
Clifford Wolf
1390e9a0a7
Add simple EDIF test case generator and checker
2017-03-18 15:00:03 +01:00
Clifford Wolf
c855353986
Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg
2017-03-04 23:41:54 +01:00
Clifford Wolf
a6ca28276e
Add write_aiger $anyseq support
2017-03-02 16:39:48 +01:00
Clifford Wolf
fbd52ec6dd
Use hex addresses in smtbmc vcd mem traces
2017-02-28 13:54:50 +01:00