aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smt2.cc
Commit message (Expand)AuthorAgeFilesLines
* smt2: Fix operation width computation for boolean producing cellsJannis Harder2023-02-011-1/+4
* sim/formalff: Clock handling for yw cosimJannis Harder2023-01-111-1/+1
* smt2: Treat bweqx as xnorJannis Harder2023-01-111-0/+1
* smt2: Directly implement bwmux instead of using bwmuxmapJannis Harder2023-01-111-2/+4
* Add bwmuxmap passJannis Harder2022-11-301-0/+1
* smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFsJannis Harder2022-10-121-3/+10
* smtbmc: Add native json based witness format + smt2 backend supportJannis Harder2022-08-161-3/+117
* smt2: Support $anyinit cellsJannis Harder2022-08-161-10/+11
* formalff: Set new replaced_by_gclk attribute on removed dff's clksJannis Harder2022-08-161-0/+11
* smt2: Fix $shift/$shiftx with negative shift ammountsJannis Harder2022-08-021-4/+4
* smt2, btor: Revert calling memory_map -rom-onlyJannis Harder2022-06-291-1/+0
* memory_map: -keepdc option for formalJannis Harder2022-06-271-1/+1
* smt2, btor: Use memory_map -rom-only to make ROMs usable for k-inductionJannis Harder2022-06-171-0/+1
* smt2: emit smtlib2_comb_expr outputs after all inputsJannis Harder2022-06-071-5/+9
* smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressionsJacob Lifshay2022-06-021-6/+57
* add $divfloor support to write_smt2Jacob Lifshay2022-05-241-0/+21
* smt2: Make write port array stores conditional on nonzero write maskJannis Harder2022-04-201-2/+4
* print cell name for properties in yosys-smtbmcN. Engelhardt2022-02-221-2/+4
* Add $bmux and $demux cells.Marcelina Kościelnicka2022-01-281-0/+5
* Hook up $aldff support in various passes.Marcelina Kościelnicka2021-10-021-1/+1
* Fixing old e-mail addresses and deadnamesClaire Xenia Wolf2021-06-081-1/+1
* Make a few passes auto-call Mem::narrow instead of rejecting wide ports.Marcelina Kościelnicka2021-05-281-6/+1
* Reject wide ports in some passes that will never support them.Marcelina Kościelnicka2021-05-251-0/+6
* kernel/rtlil: Extract some helpers for checking memory cell types.Marcelina Kościelnicka2021-05-221-2/+2
* btor, smt2, smv: Add a hint on how to deal with funny FF types.Marcelina Kościelnicka2021-02-251-0/+12
* smt2: Use Mem helper.Marcelina Kościelnicka2020-10-211-186/+244
* use the new isPublic() in a few placesN. Engelhardt2020-09-141-2/+2
* write_smt2: fix SMT-LIB tutorial URLwhitequark2020-08-291-1/+1
* Ensure smt2 comments are associated with accessorsNoah Moroze2020-08-201-9/+20
* smt2: Add `-solver-option` option.Alberto Gonzalez2020-07-201-0/+13
* Use C++11 final/override keywords.whitequark2020-06-181-2/+2
* Add flooring modulo operatorXiretza2020-05-281-0/+10
* kernel: big fat patch to use more ID::*, otherwise ID(*)Eddie Hung2020-04-021-135/+135
* kernel: use more ID::*Eddie Hung2020-04-021-37/+37
* Update `RTLIL::id2cstr()` usage to `log_id`.Alberto Gonzalez2020-04-011-2/+2
* fix typo in `write_smt2` helpTeguh Hofstee2020-03-231-1/+1
* Merge pull request #1768 from boqwxp/smt2_cleanupN. Engelhardt2020-03-161-5/+5
|\
| * Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.Alberto Gonzalez2020-03-131-5/+5
* | Add support for optimizing exists-forall problems.Alberto Gonzalez2020-03-131-0/+8
|/
* substr() -> compare()Eddie Hung2019-08-071-1/+1
* Make liberal use of IdString.in()Eddie Hung2019-08-061-1/+1
* Add $_NMUX_, add "abc -g cmos", add proper cmos cell costsClifford Wolf2019-08-061-0/+1
* Add "whitebox" attribute, add "read_verilog -wb"Clifford Wolf2019-04-181-1/+1
* Fix signed $shift/$shiftx handling in write_smt2Clifford Wolf2019-03-091-1/+2
* Use SVA label in smt export if availableClifford Wolf2019-03-071-2/+2
* Fix smt2 code generation for partially initialized memowy words, fixes #831Clifford Wolf2019-02-281-4/+11
* Add support for signed $shift/$shiftx in smt2 back-endClifford Wolf2018-11-011-1/+3
* Consistent use of 'override' for virtual methods in derived classes.Henner Zeller2018-07-201-2/+2
* Fixed -stbv handling in SMT2 back-endClifford Wolf2018-04-041-1/+1
* Add $mem support to SMT2 clock taggingClifford Wolf2018-03-271-0/+18
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-19 00:20:04 +0000