Commit Graph

1087 Commits

Author SHA1 Message Date
whitequark ba11060e59 cxxrtl: factor out -noproc/-noflatten from -O.
Although these options can be thought of as optimizations, they are
essentially orthogonal to the core of -O, which is managing signal
buffering and scope. Going from -O4 to -O2 means going from limited
to complete design visibility, yet in both cases proc and flatten
are desirable.
2020-06-09 20:18:07 +00:00
whitequark bbfe55a8d0 cxxrtl: fix two buggy split_by functions. 2020-06-09 11:05:35 +00:00
whitequark 74e3ac2449
Merge pull request #2126 from whitequark/cxxrtl-non-ext-logic-ops
cxxrtl: ignore cell input signedness when it is irrelevant
2020-06-09 09:54:09 +00:00
whitequark ef4e159447 cxxrtl: ignore cell input signedness when it is irrelevant.
Before this commit, Verilog expressions like `x && 1` would result in
references to `logic_and_us` in generated CXXRTL code, which would
not compile. After this commit, since cells like that actually behave
the same regardless of signedness attributes, the signedness is
ignored, which also reduces the template instantiation pressure.
2020-06-09 07:26:13 +00:00
whitequark 4e7d837747 cxxrtl: add missing namespace.
Fixes #2124.
2020-06-09 06:26:43 +00:00
whitequark 53688a24b5 cxxrtl: fix format of hdlnames.
The CXXRTL code that handled the `hdlname` attribute implemented
outdated semantics.
2020-06-08 20:19:41 +00:00
whitequark 467152d79f cxxrtl: don't check immutable values for changes in VCD writer.
This commit changes the VCD writer such that for all signals that
have `debug_item.type == VALUE && debug_item.next == nullptr`, it
would only sample the value once.

Commit f2d7a187 added more debug information by including constant
wires, and decreased the performance of VCD writer proportionally
because the constant wires were still repeatedly sampled; this commit
eliminates the performance hit.
2020-06-08 17:38:11 +00:00
whitequark f2d7a18756 cxxrtl: emit debug information for constant wires.
Constant wires can represent a significant chunk of the design in
generic designs or after optimization. Emitting them in VCD files
significantly improves usability because gtkwave removes all traces
that are not present in the VCD file after reload, and iterative
development suffers if switching a varying signal to a constant
disrupts the workflow.
2020-06-08 17:29:08 +00:00
whitequark d5c07e5b6f cxxrtl: track aliases in VCD writer.
This commit changes the VCD writer such that for all signals that
share `debug_item.curr`, it would only emit a single VCD identifier,
and sample the value once.

Commit 9b39c6f7 added redundancy to debug information by including
alias wires, and increased the size of VCD files proportionally; this
commit eliminates the redundancy from VCD files so that their size
is the same as before.
2020-06-08 17:10:45 +00:00
whitequark 9b39c6f744 cxxrtl: emit debug information for alias wires.
Alias wires can represent a significant chunk of the design in highly
hierarchical designs; in Minerva SRAM, there are 273 member wires and
527 alias wires. Showing them in every hierarchy level significantly
improves usability.
2020-06-08 17:09:49 +00:00
whitequark 8262997c4e cxxrtl: fix typo in comment. NFC. 2020-06-08 12:50:35 +00:00
whitequark fb3704c896 cxxrtl: minor debug-related improvements. 2020-06-08 12:50:35 +00:00
whitequark ff5500f11a cxxrtl: rename cxxrtl.cc→cxxrtl_backend.cc.
To avoid confusion with the C++ source files that are a part of
the simulation itself and not a part of Yosys build.
2020-06-07 03:48:40 +00:00
whitequark 31f6c96b1f cxxrtl: add a C API for writing VCD dumps.
This C API is fully featured.
2020-06-07 03:48:00 +00:00
whitequark 68362a9053 cxxrtl: only write VCD values that were actually updated.
On a representative design (Minerva SoC) this reduces VCD file size
by ~20× and runtime by ~3×.
2020-06-07 03:48:00 +00:00
whitequark 9c36102669 cxxrtl: add a VCD writer using debug information. 2020-06-07 03:48:00 +00:00
whitequark c399359ed6 cxxrtl: add a C API for driving and introspecting designs.
Compared to the C++ API, the C API currently has two limitations:
  1. Memories cannot be updated in a race-free way.
  2. Black boxes cannot be implemented in C.
2020-06-06 21:12:55 +00:00
whitequark f6e16e7f4c cxxrtl: generate debug information for non-localized public wires.
Debug information describes values, wires, and memories with a simple
C-compatible layout. It can be emitted on demand into a map, which
has no runtime cost when it is unused, and allows late bound designs.

The `hdlname` attribute is used as the lookup key such that original
names, as emitted by the frontend, can be used for debugging and
introspection.
2020-06-06 21:12:55 +00:00
whitequark 784bfec67c
Merge pull request #2110 from BracketMaster/master
MacOS has even stricter stack limits in catalina.
2020-06-06 12:23:06 +00:00
whitequark bd2ecc2dd3
Merge pull request #2113 from whitequark/cxxrtl-fix-sshr
cxxrtl: fix implementation of $sshr cell
2020-06-05 10:24:25 +00:00
N. Engelhardt 9669e0c7d5
Merge pull request #2109 from nakengelhardt/btor_internal_names
btor backend: make not printing internal names default
2020-06-05 11:36:08 +02:00
whitequark 025663adff cxxrtl: fix implementation of $sshr cell.
Fixes #2111.
2020-06-05 02:04:46 +00:00
Yehowshua Immanuel da0778350b
more reasonable numbers for memory 2020-06-04 17:00:04 -04:00
Yehowshua Immanuel 5d29a9f633
MacOS has even stricter stack limits in catalina.
Invoking sby in macOS Catalina fails because of bizarre stack limits in Catalina.
2020-06-04 14:01:56 -04:00
Eddie Hung 69850204c4
Merge pull request #2077 from YosysHQ/eddie/abc9_dff_improve
abc9: -dff improvements
2020-06-04 08:15:25 -07:00
N. Engelhardt 82798ae575 btor backend: make not printing internal names default 2020-06-04 16:24:16 +02:00
Claire Wolf 5e8a9c61cd Add printf format attributes to btorf/infof helper functions
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-06-04 15:53:28 +02:00
N. Engelhardt 8ceb6686e0 btor backend: add option to not include internal names 2020-06-04 14:00:52 +02:00
whitequark 3bffd09d64
Merge pull request #2006 from jersey99/signed-in-rtlil-wire
Preserve 'signed'-ness of a verilog wire through RTLIL
2020-06-04 11:23:06 +00:00
Eddie Hung 45cd323055
Merge pull request #2082 from YosysHQ/eddie/abc9_scc_fixes
abc9: fixes around handling combinatorial loops
2020-06-03 17:35:46 -07:00
clairexen ea46ed81f9
Merge pull request #2018 from boqwxp/qbfsat-timeout
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.
2020-05-30 15:04:51 +02:00
Alberto Gonzalez ea30465107
smtbmc: Remove superfluous `yosys-smt2-timeout` file macro.
Co-Authored-By: clairexen <claire@symbioticeda.com>
2020-05-29 21:33:00 +00:00
clairexen 94c1035389
Merge pull request #1885 from Xiretza/mod-rem-cells
Fix modulo/remainder semantics
2020-05-29 16:37:23 +02:00
clairexen 1c8d5a08a0
Merge pull request #2016 from boqwxp/qbfsat-yices
qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.
2020-05-29 16:21:45 +02:00
Xiretza edd8ff2c07
Add flooring division operator
The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $divfloor cell provides this flooring division.

This commit also fixes the handling of $div in opt_expr, which was
previously optimized as if it was $divfloor.
2020-05-28 22:59:04 +02:00
Xiretza 17163cf43a
Add flooring modulo operator
The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $modfloor cell provides this flooring modulo (also known as "remainder"
in several languages, but this name is ambiguous).

This commit also fixes the handling of $mod in opt_expr, which was
previously optimized as if it was $modfloor.
2020-05-28 22:59:03 +02:00
whitequark 736ccb2ad5
Merge pull request #2031 from epfl-vlsc/master
Add extmodule support to firrtl backend
2020-05-28 09:59:17 +00:00
whitequark 2974183855
Merge pull request #2063 from boqwxp/techmapped-firrtl
firrtl: Accept techmapped cell types in FIRRTL backend.
2020-05-28 09:42:58 +00:00
whitequark 0bf6b164be cxxrtl: make logging a little bit nicer. 2020-05-26 21:37:32 +00:00
whitequark e9c07e2bda cxxrtl: add missing parts of commit 281c9685. 2020-05-26 21:34:20 +00:00
Eddie Hung 1826370b3a xaiger: promote abc9_keep wires 2020-05-25 16:40:30 -07:00
Alberto Gonzalez 9847a4eea8
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4. 2020-05-25 20:39:30 +00:00
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