aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smt2.cc
Commit message (Expand)AuthorAgeFilesLines
* 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
* Improve SMT2 encoding of $reduce_{and,or,bool}Clifford Wolf2018-03-041-1/+9
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-231-10/+72
* Add support for mockup clock signals in yosys-smtbmc vcd outputClifford Wolf2018-02-201-3/+57
* Fix handling of zero-length cell connections in SMT2 back-endClifford Wolf2018-02-081-0/+8
* Add yosys-smtbmc VCD writer support for memories with async writesClifford Wolf2017-12-141-2/+2
* Add smt2 back-end support for async write memoriesClifford Wolf2017-12-141-14/+53
* Fix SMT2 handling of initstate in sub-modulesClifford Wolf2017-10-291-0/+3
* Fix bug in write_smt2 (export logic driving hierarchical cells before exporti...Clifford Wolf2017-08-251-34/+34
* Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand cons...Clifford Wolf2017-06-071-2/+4
* Add $_ANDNOT_ and $_ORNOT_ gatesClifford Wolf2017-05-171-0/+2
* Add "write_smt2 -stdt" modeClifford Wolf2017-03-201-9/+47
* Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msgClifford Wolf2017-03-041-31/+85
* Fix extra newline bug in write_smt2Clifford Wolf2017-02-261-1/+1
* Improve (and fix for stbv mode) SMT2 memory APIClifford Wolf2017-02-261-25/+24
* Add "write_smt2 -stbv"Clifford Wolf2017-02-241-44/+174
* Add SMT2 statebv mode (inactive for now)Clifford Wolf2017-02-241-20/+47