| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Hook up $aldff support in various passes. | Marcelina Kościelnicka | 2021-10-02 | 1 | -1/+1 |
| | | |||||
| * | Fixing old e-mail addresses and deadnames | Claire Xenia Wolf | 2021-06-08 | 1 | -1/+1 |
| | | | | | | | | | s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi; s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi; s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi; s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi; s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g; | ||||
| * | Make a few passes auto-call Mem::narrow instead of rejecting wide ports. | Marcelina Kościelnicka | 2021-05-28 | 1 | -6/+1 |
| | | | | | | | This essentially adds wide port support for free in passes that don't have a usefully better way of handling wide ports than just breaking them up to narrow ports, avoiding "please run memory_narrow" annoyance. | ||||
| * | Reject wide ports in some passes that will never support them. | Marcelina Kościelnicka | 2021-05-25 | 1 | -0/+6 |
| | | |||||
| * | kernel/rtlil: Extract some helpers for checking memory cell types. | Marcelina Kościelnicka | 2021-05-22 | 1 | -2/+2 |
| | | | | | | | There will soon be more (versioned) memory cells, so handle passes that only care if a cell is memory-related by a simple helper call instead of a hardcoded list. | ||||
| * | btor, smt2, smv: Add a hint on how to deal with funny FF types. | Marcelina Kościelnicka | 2021-02-25 | 1 | -0/+12 |
| | | |||||
| * | smt2: Use Mem helper. | Marcelina Kościelnicka | 2020-10-21 | 1 | -186/+244 |
| | | |||||
| * | use the new isPublic() in a few places | N. Engelhardt | 2020-09-14 | 1 | -2/+2 |
| | | |||||
| * | write_smt2: fix SMT-LIB tutorial URL | whitequark | 2020-08-29 | 1 | -1/+1 |
| | | |||||
| * | Ensure smt2 comments are associated with accessors | Noah Moroze | 2020-08-20 | 1 | -9/+20 |
| | | |||||
| * | smt2: Add `-solver-option` option. | Alberto Gonzalez | 2020-07-20 | 1 | -0/+13 |
| | | |||||
| * | Use C++11 final/override keywords. | whitequark | 2020-06-18 | 1 | -2/+2 |
| | | |||||
| * | Add flooring modulo operator | Xiretza | 2020-05-28 | 1 | -0/+10 |
| | | | | | | | | | | | | 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. | ||||
| * | kernel: big fat patch to use more ID::*, otherwise ID(*) | Eddie Hung | 2020-04-02 | 1 | -135/+135 |
| | | |||||
| * | kernel: use more ID::* | Eddie Hung | 2020-04-02 | 1 | -37/+37 |
| | | |||||
| * | Update `RTLIL::id2cstr()` usage to `log_id`. | Alberto Gonzalez | 2020-04-01 | 1 | -2/+2 |
| | | |||||
| * | fix typo in `write_smt2` help | Teguh Hofstee | 2020-03-23 | 1 | -1/+1 |
| | | |||||
| * | Merge pull request #1768 from boqwxp/smt2_cleanup | N. Engelhardt | 2020-03-16 | 1 | -5/+5 |
| |\ | | | | | Clean up pseudo-private member usage in `backends/smt2/smt2.cc`. | ||||
| | * | Clean up pseudo-private member usage in `backends/smt2/smt2.cc`. | Alberto Gonzalez | 2020-03-13 | 1 | -5/+5 |
| | | | |||||
| * | | Add support for optimizing exists-forall problems. | Alberto Gonzalez | 2020-03-13 | 1 | -0/+8 |
| |/ | | | | | | 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. | ||||
| * | substr() -> compare() | Eddie Hung | 2019-08-07 | 1 | -1/+1 |
| | | |||||
| * | Make liberal use of IdString.in() | Eddie Hung | 2019-08-06 | 1 | -1/+1 |
| | | |||||
| * | Add $_NMUX_, add "abc -g cmos", add proper cmos cell costs | Clifford Wolf | 2019-08-06 | 1 | -0/+1 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add "whitebox" attribute, add "read_verilog -wb" | Clifford Wolf | 2019-04-18 | 1 | -1/+1 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix signed $shift/$shiftx handling in write_smt2 | Clifford Wolf | 2019-03-09 | 1 | -1/+2 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Use SVA label in smt export if available | Clifford Wolf | 2019-03-07 | 1 | -2/+2 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix smt2 code generation for partially initialized memowy words, fixes #831 | Clifford Wolf | 2019-02-28 | 1 | -4/+11 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add support for signed $shift/$shiftx in smt2 back-end | Clifford Wolf | 2018-11-01 | 1 | -1/+3 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Consistent use of 'override' for virtual methods in derived classes. | Henner Zeller | 2018-07-20 | 1 | -2/+2 |
| | | | | | | | | | | 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) | ||||
| * | Fixed -stbv handling in SMT2 back-end | Clifford Wolf | 2018-04-04 | 1 | -1/+1 |
| | | |||||
| * | Add $mem support to SMT2 clock tagging | Clifford Wolf | 2018-03-27 | 1 | -0/+18 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Improve SMT2 encoding of $reduce_{and,or,bool} | Clifford Wolf | 2018-03-04 | 1 | -1/+9 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add smtbmc support for exist-forall problems | Clifford Wolf | 2018-02-23 | 1 | -10/+72 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add support for mockup clock signals in yosys-smtbmc vcd output | Clifford Wolf | 2018-02-20 | 1 | -3/+57 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix handling of zero-length cell connections in SMT2 back-end | Clifford Wolf | 2018-02-08 | 1 | -0/+8 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add yosys-smtbmc VCD writer support for memories with async writes | Clifford Wolf | 2017-12-14 | 1 | -2/+2 |
| | | |||||
| * | Add smt2 back-end support for async write memories | Clifford Wolf | 2017-12-14 | 1 | -14/+53 |
| | | |||||
| * | Fix SMT2 handling of initstate in sub-modules | Clifford Wolf | 2017-10-29 | 1 | -0/+3 |
| | | |||||
| * | Fix bug in write_smt2 (export logic driving hierarchical cells before ↵ | Clifford Wolf | 2017-08-25 | 1 | -34/+34 |
| | | | | | exporting regs) | ||||
| * | Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand ↵ | Clifford Wolf | 2017-06-07 | 1 | -2/+4 |
| | | | | | const reg" | ||||
| * | Add $_ANDNOT_ and $_ORNOT_ gates | Clifford Wolf | 2017-05-17 | 1 | -0/+2 |
| | | |||||
| * | Add "write_smt2 -stdt" mode | Clifford Wolf | 2017-03-20 | 1 | -9/+47 |
| | | |||||
| * | Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg | Clifford Wolf | 2017-03-04 | 1 | -31/+85 |
| | | |||||
| * | Fix extra newline bug in write_smt2 | Clifford Wolf | 2017-02-26 | 1 | -1/+1 |
| | | |||||
| * | Improve (and fix for stbv mode) SMT2 memory API | Clifford Wolf | 2017-02-26 | 1 | -25/+24 |
| | | |||||
| * | Add "write_smt2 -stbv" | Clifford Wolf | 2017-02-24 | 1 | -44/+174 |
| | | |||||
| * | Add SMT2 statebv mode (inactive for now) | Clifford Wolf | 2017-02-24 | 1 | -20/+47 |
| | | |||||
| * | Partially implement cover() support in yosys-smtbmc | Clifford Wolf | 2017-02-04 | 1 | -2/+6 |
| | | |||||
| * | Further improve cover() support | Clifford Wolf | 2017-02-04 | 1 | -3/+5 |
| | | |||||
| * | Added support for partially initialized regs to smt2 back-end | Clifford Wolf | 2016-12-01 | 1 | -3/+15 |
| | | |||||
 |
index : iCE40/yosys | |
| [no description] |
| aboutsummaryrefslogtreecommitdiffstats |