riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
11,010 Commits 75 Branches 48 Tags 61 MiB
Commit Graph

1245 Commits

Author SHA1 Message Date
Alberto Gonzalez 54570a3978
qbfsat: Move SMT2 info statements back to the top of the file. 2020-05-25 20:38:29 +00:00
Alberto Gonzalez 903456c267
qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default. 
Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode.
 2020-05-25 20:38:29 +00:00
Eddie Hung 9e6c288e5a xaiger: cleanup 2020-05-25 08:43:33 -07:00
Eddie Hung d64df21630 xaiger: do not derive cells 2020-05-24 08:17:30 -07:00
whitequark 281c96856a cxxrtl: get rid of -O5 aka `opt_clean -purge` optimization level. 
This isn't actually necessary anymore after scheduling was improved,
and `clean -purge` disrupts the mapping between wires in the input
RTLIL netlist and the output CXXRTL code.
 2020-05-22 19:08:30 +00:00
N. Engelhardt 7c4e580f8f
Merge pull request #2054 from boqwxp/fix-smtbmc 
smtbmc: Fix return status handling.
 2020-05-20 08:55:36 +02:00
Alberto Gonzalez 1053032a81
smtbmc: Fix typo in error message. 
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
 2020-05-19 16:13:44 +00:00
Alberto Gonzalez 049e4caceb
firrtl: Accept techmapped cell types in FIRRTL backend. 2020-05-17 10:03:11 +00:00
Eddie Hung 67fc0c3698 abc9: use (* abc9_keep *) instead of (* abc9_scc *); apply to $_DFF_?_ 
instead of moving them to $__ prefix
 2020-05-14 16:44:35 -07:00
Eddie Hung 97a0a04314 abc9_ops/xaiger: further reducing Module::derive() calls by ... 
replacing _all_ (* abc9_box *) instantiations with their derived types
 2020-05-14 10:33:57 -07:00
Eddie Hung e79127fceb Cleanup; reduce Module::derive() calls 2020-05-14 10:33:57 -07:00
Eddie Hung e357b40e7a xaiger: no longer use nonstandard even/odd to designate +ve/-ve polarity 2020-05-14 10:33:56 -07:00
Eddie Hung 722540dbf9 abc9: not enough to techmap_fail on (* init=1 *), hide them using $__ 2020-05-14 10:33:56 -07:00
Eddie Hung 63246a5c0e Revert "Merge pull request #1917 from YosysHQ/eddie/abc9_delay_check" 
This reverts commit 759283fa65, reversing
changes made to f41c7ccfff.
 2020-05-14 10:33:56 -07:00
Eddie Hung 4c6647a469 xaiger: always sort input/output bits by port id 
redundant for normal design, but necessary for holes
 2020-05-14 10:33:56 -07:00
Eddie Hung ec4bbb1444 abc9: generate $abc9_holes design instead of <name>$holes 2020-05-14 10:33:56 -07:00
Eddie Hung 6f4f795953 aiger/xaiger: use odd for negedge clk, even for posedge 
Since abc9 doesn't like negative mergeability values
 2020-05-14 10:33:56 -07:00
Eddie Hung f975cf39cb xaiger: update help text 2020-05-14 10:33:56 -07:00
Eddie Hung 90cd49995b xaiger: do not treat (* init=1'bx *) as 1'b0 2020-05-14 10:33:56 -07:00
Eddie Hung 77f3abcdc3 xaiger: when -dff use (* init *) for initial state 2020-05-14 10:33:56 -07:00
Eddie Hung 95763c8d18 abc9_ops: add 'dff' label for auto handling of (* abc9_flop *) boxes 2020-05-14 10:33:56 -07:00
Eddie Hung ffa52738fb xaiger: output $_DFF_[NP]_ with mergeability if -dff option 2020-05-14 10:33:56 -07:00
Alberto Gonzalez 299ab76a09
smtbmc: Fix return status handling. 2020-05-14 17:07:59 +00:00
Xiretza d86fc791f9
Reorder cases to avoid fall-through warning 
log_assert(false) never returns and thus can't fall through, but gcc
doesn't seem to think that far. Making it the last case avoids the
problem entirely.
 2020-05-07 13:39:34 +02:00
Xiretza 695150b037
Add YS_FALLTHROUGH macro to mark case fall-through 
C++17 introduced [[fallthrough]], GCC and clang had their own vendored
attributes before that. MSVC doesn't seem to have such a warning at all.
 2020-05-07 13:39:34 +02:00
Sahand Kashani 1688a62500 Formatting fixes 2020-05-06 21:15:32 +02:00
Sahand Kashani 1f1b64b880 Add extmodule support to firrtl backend 
The current firrtl backend emits blackboxes as standard modules
with an empty body, but this causes the firrtl compiler to
optimize out entire circuits due to the absence of any drivers.

Yosys already tags blackboxes with a (*blackbox*) attribute, so this
commit just propagates this change to firrtl's syntax for blackboxes.
 2020-05-06 01:01:14 +02:00
Eddie Hung a0afa1787e aiger: fixes for ports that have start_offset != 0 2020-05-02 10:00:32 -07:00
Vamsi K Vytla 5f9cd2e2f6 Preserve 'signed'-ness of a verilog wire through RTLIL 
As per suggestion made in https://github.com/YosysHQ/yosys/pull/1987, now:

RTLIL::wire holds an is_signed field.
This is exported in JSON backend
This is exported via dump_rtlil command
This is read in via ilang_parser
 2020-04-27 09:44:24 -07:00
David Shah 1b93dda037 cxxrtl: Round up constant width 
Signed-off-by: David Shah <dave@ds0.me>
 2020-04-25 10:42:21 +01:00
whitequark a0e658d412 cxxrtl: use `cxxrtl_` prefix rather than `cxxrtl.` 
The former prefix does not need to be escaped in Verilog, unlike
the latter, and the Yosys convention is to use the former.
 2020-04-24 18:35:53 +00:00
whitequark f88378ae61 cxxrtl: improve printing of narrow memories. 2020-04-24 05:50:36 +00:00
whitequark 3738391bdd cxxrtl: fix handling of parametric modules with large parameters. 
These have a `$paramod$` prefix, not `$paramod\\`.
 2020-04-24 05:44:39 +00:00
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