aboutsummaryrefslogtreecommitdiffstats
path: root/backends
Commit message (Collapse)AuthorAgeFilesLines
...
| * | | smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, ↵Alberto Gonzalez2020-05-252-5/+35
| | | | | | | | | | | | | | | | and CVC4.
* | | | Merge pull request #1885 from Xiretza/mod-rem-cellsclairexen2020-05-297-9/+116
|\ \ \ \ | | | | | | | | | | Fix modulo/remainder semantics
| * | | | Add flooring division operatorXiretza2020-05-283-3/+58
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | Add flooring modulo operatorXiretza2020-05-287-9/+61
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | Merge pull request #2016 from boqwxp/qbfsat-yicesclairexen2020-05-291-1/+5
|\ \ \ \ \ | |/ / / / |/| / / / | |/ / / qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.
| * | | qbfsat: Move SMT2 info statements back to the top of the file.Alberto Gonzalez2020-05-251-3/+3
| | | |
| * | | qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices ↵Alberto Gonzalez2020-05-251-3/+7
| |/ / | | | | | | | | | | | | | | | 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.
* | | Merge pull request #2031 from epfl-vlsc/masterwhitequark2020-05-281-1/+40
|\ \ \ | | | | | | | | Add extmodule support to firrtl backend
| * | | Formatting fixesSahand Kashani2020-05-061-14/+7
| | | |
| * | | Add extmodule support to firrtl backendSahand Kashani2020-05-061-1/+47
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | Merge pull request #2063 from boqwxp/techmapped-firrtlwhitequark2020-05-281-10/+12
|\ \ \ \ | | | | | | | | | | firrtl: Accept techmapped cell types in FIRRTL backend.
| * | | | firrtl: Accept techmapped cell types in FIRRTL backend.Alberto Gonzalez2020-05-171-10/+12
| | | | |
* | | | | cxxrtl: make logging a little bit nicer.whitequark2020-05-261-2/+10
| | | | |
* | | | | cxxrtl: add missing parts of commit 281c9685.whitequark2020-05-261-5/+3
| |_|/ / |/| | |
* | | | xaiger: do not derive cellsEddie Hung2020-05-241-7/+1
| | | |
* | | | cxxrtl: get rid of -O5 aka `opt_clean -purge` optimization level.whitequark2020-05-221-8/+2
| | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | Merge pull request #2054 from boqwxp/fix-smtbmcN. Engelhardt2020-05-201-3/+3
|\ \ \ \ | | | | | | | | | | smtbmc: Fix return status handling.
| * | | | smtbmc: Fix typo in error message.Alberto Gonzalez2020-05-191-1/+1
| | | | | | | | | | | | | | | | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
| * | | | smtbmc: Fix return status handling.Alberto Gonzalez2020-05-141-2/+2
| |/ / /
* | | | abc9: use (* abc9_keep *) instead of (* abc9_scc *); apply to $_DFF_?_Eddie Hung2020-05-141-5/+5
| | | | | | | | | | | | | | | | instead of moving them to $__ prefix
* | | | abc9_ops/xaiger: further reducing Module::derive() calls by ...Eddie Hung2020-05-141-40/+32
| | | | | | | | | | | | | | | | replacing _all_ (* abc9_box *) instantiations with their derived types
* | | | Cleanup; reduce Module::derive() callsEddie Hung2020-05-141-18/+20
| | | |
* | | | xaiger: no longer use nonstandard even/odd to designate +ve/-ve polarityEddie Hung2020-05-141-16/+5
| | | |
* | | | abc9: not enough to techmap_fail on (* init=1 *), hide them using $__Eddie Hung2020-05-141-0/+1
| | | |
* | | | Revert "Merge pull request #1917 from YosysHQ/eddie/abc9_delay_check"Eddie Hung2020-05-141-4/+0
| | | | | | | | | | | | | | | | | | | | This reverts commit 759283fa65b1195ebe3a5bc6890ec622febca0eb, reversing changes made to f41c7ccfff4bf104c646ca4b85e079a0f91c9151.
* | | | xaiger: always sort input/output bits by port idEddie Hung2020-05-141-12/+10
| | | | | | | | | | | | | | | | redundant for normal design, but necessary for holes
* | | | abc9: generate $abc9_holes design instead of <name>$holesEddie Hung2020-05-141-3/+9
| | | |
* | | | aiger/xaiger: use odd for negedge clk, even for posedgeEddie Hung2020-05-141-6/+10
| | | | | | | | | | | | | | | | Since abc9 doesn't like negative mergeability values
* | | | xaiger: update help textEddie Hung2020-05-141-4/+4
| | | |
* | | | xaiger: do not treat (* init=1'bx *) as 1'b0Eddie Hung2020-05-141-1/+1
| | | |
* | | | xaiger: when -dff use (* init *) for initial stateEddie Hung2020-05-141-3/+15
| | | |
* | | | abc9_ops: add 'dff' label for auto handling of (* abc9_flop *) boxesEddie Hung2020-05-141-8/+2
| | | |
* | | | xaiger: output $_DFF_[NP]_ with mergeability if -dff optionEddie Hung2020-05-141-42/+44
|/ / /
* | | Reorder cases to avoid fall-through warningXiretza2020-05-071-3/+3
| | | | | | | | | | | | | | | | | | 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.
* | | Add YS_FALLTHROUGH macro to mark case fall-throughXiretza2020-05-072-2/+8
|/ / | | | | | | | | 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.
* | aiger: fixes for ports that have start_offset != 0Eddie Hung2020-05-022-9/+8
| |
* | cxxrtl: Round up constant widthDavid Shah2020-04-251-1/+1
| | | | | | | | Signed-off-by: David Shah <dave@ds0.me>
* | cxxrtl: use `cxxrtl_` prefix rather than `cxxrtl.`whitequark2020-04-241-45/+45
| | | | | | | | | | The former prefix does not need to be escaped in Verilog, unlike the latter, and the Yosys convention is to use the former.
* | cxxrtl: improve printing of narrow memories.whitequark2020-04-241-3/+4
| |
* | cxxrtl: fix handling of parametric modules with large parameters.whitequark2020-04-241-1/+1
|/ | | | These have a `$paramod$` prefix, not `$paramod\\`.
* cxxrtl: keep the memory write queue sorted on insertion.Asu2020-04-221-3/+5
| | | | | | | 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.
* Merge pull request #1979 from whitequark/cxxrtl-go-fasterClaire Wolf2020-04-222-184/+396
|\ | | | | cxxrtl: Gas gas gas! I'm gonna step on the gas! Tonight I'll fly!
| * cxxrtl: run edge detectors only once in eval().whitequark2020-04-221-6/+22
| | | | | | | | As a result, Minerva SRAM SoC runs ~15% faster.
| * cxxrtl: add an unsupported knob for manipulating clock trees.whitequark2020-04-221-0/+18
| | | | | | | | | | | | | | | | | | 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.
| * cxxrtl: use log_id() where appropriate. NFC.whitequark2020-04-211-4/+4
| |
| * cxxrtl: add (*cxxrtl.{comb,sync}*) annotations on black box outputs.whitequark2020-04-211-65/+186
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * cxxrtl: s/sync_{wire,type}/edge_{wire,type}/. NFC.whitequark2020-04-211-23/+23
| | | | | | | | | | | | | | 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.
| * cxxrtl: use one delta cycle for immediately converging netlists.whitequark2020-04-212-11/+21
| | | | | | | | | | | | | | | | | | | | | | 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.
| * cxxrtl: add -O6, a shortcut for running `proc; flatten`.whitequark2020-04-211-4/+14
| | | | | | | | | | | | | | 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.
| * cxxrtl: unbuffer module input wires.whitequark2020-04-211-31/+61
| | | | | | | | | | | | | | | | 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.
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-08 05:21:00 +0000