Commit message (Collapse) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
* | Merge pull request #2110 from BracketMaster/master | whitequark | 2020-06-06 | 1 | -1/+1 | |
|\ | | | | | MacOS has even stricter stack limits in catalina. | |||||
| * | more reasonable numbers for memory | Yehowshua Immanuel | 2020-06-04 | 1 | -1/+1 | |
| | | ||||||
| * | MacOS has even stricter stack limits in catalina. | Yehowshua Immanuel | 2020-06-04 | 1 | -1/+1 | |
| | | | | | | Invoking sby in macOS Catalina fails because of bizarre stack limits in Catalina. | |||||
* | | Merge pull request #2113 from whitequark/cxxrtl-fix-sshr | whitequark | 2020-06-05 | 1 | -1/+1 | |
|\ \ | | | | | | | cxxrtl: fix implementation of $sshr cell | |||||
| * | | cxxrtl: fix implementation of $sshr cell. | whitequark | 2020-06-05 | 1 | -1/+1 | |
| | | | | | | | | | | | | Fixes #2111. | |||||
* | | | Merge pull request #2109 from nakengelhardt/btor_internal_names | N. Engelhardt | 2020-06-05 | 1 | -5/+5 | |
|\ \ \ | |_|/ |/| | | btor backend: make not printing internal names default | |||||
| * | | btor backend: make not printing internal names default | N. Engelhardt | 2020-06-04 | 1 | -5/+5 | |
| | | | ||||||
* | | | Merge pull request #2077 from YosysHQ/eddie/abc9_dff_improve | Eddie Hung | 2020-06-04 | 1 | -28/+22 | |
|\ \ \ | |/ / |/| | | abc9: -dff improvements | |||||
| * | | xaiger: cleanup | Eddie Hung | 2020-05-25 | 1 | -28/+22 | |
| | | | ||||||
* | | | Add printf format attributes to btorf/infof helper functions | Claire Wolf | 2020-06-04 | 1 | -3/+3 | |
| | | | | | | | | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com> | |||||
* | | | btor backend: add option to not include internal names | N. Engelhardt | 2020-06-04 | 1 | -33/+42 | |
| | | | ||||||
* | | | Merge pull request #2006 from jersey99/signed-in-rtlil-wire | whitequark | 2020-06-04 | 2 | -0/+6 | |
|\ \ \ | | | | | | | | | Preserve 'signed'-ness of a verilog wire through RTLIL | |||||
| * | | | Preserve 'signed'-ness of a verilog wire through RTLIL | Vamsi K Vytla | 2020-04-27 | 2 | -0/+6 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 | |||||
* | | | | Merge pull request #2082 from YosysHQ/eddie/abc9_scc_fixes | Eddie Hung | 2020-06-03 | 1 | -1/+1 | |
|\ \ \ \ | |_|_|/ |/| | | | abc9: fixes around handling combinatorial loops | |||||
| * | | | xaiger: promote abc9_keep wires | Eddie Hung | 2020-05-25 | 1 | -1/+1 | |
| | |/ | |/| | ||||||
* | | | Merge pull request #2018 from boqwxp/qbfsat-timeout | clairexen | 2020-05-30 | 2 | -5/+31 | |
|\ \ \ | | | | | | | | | smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4. | |||||
| * | | | smtbmc: Remove superfluous `yosys-smt2-timeout` file macro. | Alberto Gonzalez | 2020-05-29 | 1 | -4/+0 | |
| | | | | | | | | | | | | | | | | Co-Authored-By: clairexen <claire@symbioticeda.com> | |||||
| * | | | smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, ↵ | Alberto Gonzalez | 2020-05-25 | 2 | -5/+35 | |
| | | | | | | | | | | | | | | | | and CVC4. | |||||
* | | | | Merge pull request #1885 from Xiretza/mod-rem-cells | clairexen | 2020-05-29 | 7 | -9/+116 | |
|\ \ \ \ | | | | | | | | | | | Fix modulo/remainder semantics | |||||
| * | | | | Add flooring division operator | Xiretza | 2020-05-28 | 3 | -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 operator | Xiretza | 2020-05-28 | 7 | -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-yices | clairexen | 2020-05-29 | 1 | -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 Gonzalez | 2020-05-25 | 1 | -3/+3 | |
| | | | | ||||||
| * | | | qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices ↵ | Alberto Gonzalez | 2020-05-25 | 1 | -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/master | whitequark | 2020-05-28 | 1 | -1/+40 | |
|\ \ \ | | | | | | | | | Add extmodule support to firrtl backend | |||||
| * | | | Formatting fixes | Sahand Kashani | 2020-05-06 | 1 | -14/+7 | |
| | | | | ||||||
| * | | | Add extmodule support to firrtl backend | Sahand Kashani | 2020-05-06 | 1 | -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-firrtl | whitequark | 2020-05-28 | 1 | -10/+12 | |
|\ \ \ \ | | | | | | | | | | | firrtl: Accept techmapped cell types in FIRRTL backend. | |||||
| * | | | | firrtl: Accept techmapped cell types in FIRRTL backend. | Alberto Gonzalez | 2020-05-17 | 1 | -10/+12 | |
| | | | | | ||||||
* | | | | | cxxrtl: make logging a little bit nicer. | whitequark | 2020-05-26 | 1 | -2/+10 | |
| | | | | | ||||||
* | | | | | cxxrtl: add missing parts of commit 281c9685. | whitequark | 2020-05-26 | 1 | -5/+3 | |
| |_|/ / |/| | | | ||||||
* | | | | xaiger: do not derive cells | Eddie Hung | 2020-05-24 | 1 | -7/+1 | |
| | | | | ||||||
* | | | | cxxrtl: get rid of -O5 aka `opt_clean -purge` optimization level. | whitequark | 2020-05-22 | 1 | -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-smtbmc | N. Engelhardt | 2020-05-20 | 1 | -3/+3 | |
|\ \ \ \ | | | | | | | | | | | smtbmc: Fix return status handling. | |||||
| * | | | | smtbmc: Fix typo in error message. | Alberto Gonzalez | 2020-05-19 | 1 | -1/+1 | |
| | | | | | | | | | | | | | | | | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com> | |||||
| * | | | | smtbmc: Fix return status handling. | Alberto Gonzalez | 2020-05-14 | 1 | -2/+2 | |
| |/ / / | ||||||
* | | | | abc9: use (* abc9_keep *) instead of (* abc9_scc *); apply to $_DFF_?_ | Eddie Hung | 2020-05-14 | 1 | -5/+5 | |
| | | | | | | | | | | | | | | | | instead of moving them to $__ prefix | |||||
* | | | | abc9_ops/xaiger: further reducing Module::derive() calls by ... | Eddie Hung | 2020-05-14 | 1 | -40/+32 | |
| | | | | | | | | | | | | | | | | replacing _all_ (* abc9_box *) instantiations with their derived types | |||||
* | | | | Cleanup; reduce Module::derive() calls | Eddie Hung | 2020-05-14 | 1 | -18/+20 | |
| | | | | ||||||
* | | | | xaiger: no longer use nonstandard even/odd to designate +ve/-ve polarity | Eddie Hung | 2020-05-14 | 1 | -16/+5 | |
| | | | | ||||||
* | | | | abc9: not enough to techmap_fail on (* init=1 *), hide them using $__ | Eddie Hung | 2020-05-14 | 1 | -0/+1 | |
| | | | | ||||||
* | | | | Revert "Merge pull request #1917 from YosysHQ/eddie/abc9_delay_check" | Eddie Hung | 2020-05-14 | 1 | -4/+0 | |
| | | | | | | | | | | | | | | | | | | | | This reverts commit 759283fa65b1195ebe3a5bc6890ec622febca0eb, reversing changes made to f41c7ccfff4bf104c646ca4b85e079a0f91c9151. | |||||
* | | | | xaiger: always sort input/output bits by port id | Eddie Hung | 2020-05-14 | 1 | -12/+10 | |
| | | | | | | | | | | | | | | | | redundant for normal design, but necessary for holes | |||||
* | | | | abc9: generate $abc9_holes design instead of <name>$holes | Eddie Hung | 2020-05-14 | 1 | -3/+9 | |
| | | | | ||||||
* | | | | aiger/xaiger: use odd for negedge clk, even for posedge | Eddie Hung | 2020-05-14 | 1 | -6/+10 | |
| | | | | | | | | | | | | | | | | Since abc9 doesn't like negative mergeability values | |||||
* | | | | xaiger: update help text | Eddie Hung | 2020-05-14 | 1 | -4/+4 | |
| | | | | ||||||
* | | | | xaiger: do not treat (* init=1'bx *) as 1'b0 | Eddie Hung | 2020-05-14 | 1 | -1/+1 | |
| | | | | ||||||
* | | | | xaiger: when -dff use (* init *) for initial state | Eddie Hung | 2020-05-14 | 1 | -3/+15 | |
| | | | | ||||||
* | | | | abc9_ops: add 'dff' label for auto handling of (* abc9_flop *) boxes | Eddie Hung | 2020-05-14 | 1 | -8/+2 | |
| | | | | ||||||
* | | | | xaiger: output $_DFF_[NP]_ with mergeability if -dff option | Eddie Hung | 2020-05-14 | 1 | -42/+44 | |
|/ / / |