| Commit message (Expand) | Author | Age | Files | Lines |
* | smtbmc: Add native json based witness format + smt2 backend support | Jannis Harder | 2022-08-16 | 1 | -3/+117 |
* | smt2: Support $anyinit cells | Jannis Harder | 2022-08-16 | 1 | -10/+11 |
* | formalff: Set new replaced_by_gclk attribute on removed dff's clks | Jannis Harder | 2022-08-16 | 1 | -0/+11 |
* | smt2: Fix $shift/$shiftx with negative shift ammounts | Jannis Harder | 2022-08-02 | 1 | -4/+4 |
* | smt2, btor: Revert calling memory_map -rom-only | Jannis Harder | 2022-06-29 | 1 | -1/+0 |
* | memory_map: -keepdc option for formal | Jannis Harder | 2022-06-27 | 1 | -1/+1 |
* | smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction | Jannis Harder | 2022-06-17 | 1 | -0/+1 |
* | smt2: emit smtlib2_comb_expr outputs after all inputs | Jannis Harder | 2022-06-07 | 1 | -5/+9 |
* | smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions | Jacob Lifshay | 2022-06-02 | 1 | -6/+57 |
* | add $divfloor support to write_smt2 | Jacob Lifshay | 2022-05-24 | 1 | -0/+21 |
* | smt2: Make write port array stores conditional on nonzero write mask | Jannis Harder | 2022-04-20 | 1 | -2/+4 |
* | print cell name for properties in yosys-smtbmc | N. Engelhardt | 2022-02-22 | 1 | -2/+4 |
* | Add $bmux and $demux cells. | Marcelina Kościelnicka | 2022-01-28 | 1 | -0/+5 |
* | 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 |
* | Make a few passes auto-call Mem::narrow instead of rejecting wide ports. | Marcelina Kościelnicka | 2021-05-28 | 1 | -6/+1 |
* | 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 |
* | 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 |
* | 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`. | Alberto Gonzalez | 2020-03-13 | 1 | -5/+5 |
* | | Add support for optimizing exists-forall problems. | Alberto Gonzalez | 2020-03-13 | 1 | -0/+8 |
|/ |
|
* | 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 |
* | Add "whitebox" attribute, add "read_verilog -wb" | Clifford Wolf | 2019-04-18 | 1 | -1/+1 |
* | Fix signed $shift/$shiftx handling in write_smt2 | Clifford Wolf | 2019-03-09 | 1 | -1/+2 |
* | Use SVA label in smt export if available | Clifford Wolf | 2019-03-07 | 1 | -2/+2 |
* | Fix smt2 code generation for partially initialized memowy words, fixes #831 | Clifford Wolf | 2019-02-28 | 1 | -4/+11 |
* | Add support for signed $shift/$shiftx in smt2 back-end | Clifford Wolf | 2018-11-01 | 1 | -1/+3 |
* | Consistent use of 'override' for virtual methods in derived classes. | Henner Zeller | 2018-07-20 | 1 | -2/+2 |
* | 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 |
* | Improve SMT2 encoding of $reduce_{and,or,bool} | Clifford Wolf | 2018-03-04 | 1 | -1/+9 |
* | Add smtbmc support for exist-forall problems | Clifford Wolf | 2018-02-23 | 1 | -10/+72 |
* | Add support for mockup clock signals in yosys-smtbmc vcd output | Clifford Wolf | 2018-02-20 | 1 | -3/+57 |
* | Fix handling of zero-length cell connections in SMT2 back-end | Clifford Wolf | 2018-02-08 | 1 | -0/+8 |
* | 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 |