aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smt2.cc
Commit message (Collapse)AuthorAgeFilesLines
* 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`.
| * 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
|/ | | | | | 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 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
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "whitebox" attribute, add "read_verilog -wb"Clifford Wolf2019-04-181-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix signed $shift/$shiftx handling in write_smt2Clifford Wolf2019-03-091-1/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Use SVA label in smt export if availableClifford Wolf2019-03-071-2/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix smt2 code generation for partially initialized memowy words, fixes #831Clifford Wolf2019-02-281-4/+11
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for signed $shift/$shiftx in smt2 back-endClifford Wolf2018-11-011-1/+3
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Consistent use of 'override' for virtual methods in derived classes.Henner Zeller2018-07-201-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-endClifford Wolf2018-04-041-1/+1
|
* Add $mem support to SMT2 clock taggingClifford Wolf2018-03-271-0/+18
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improve SMT2 encoding of $reduce_{and,or,bool}Clifford Wolf2018-03-041-1/+9
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add smtbmc support for exist-forall problemsClifford Wolf2018-02-231-10/+72
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for mockup clock signals in yosys-smtbmc vcd outputClifford Wolf2018-02-201-3/+57
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix handling of zero-length cell connections in SMT2 back-endClifford Wolf2018-02-081-0/+8
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* 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 ↵Clifford Wolf2017-08-251-34/+34
| | | | exporting regs)
* Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand ↵Clifford Wolf2017-06-071-2/+4
| | | | const reg"
* 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
|
* Partially implement cover() support in yosys-smtbmcClifford Wolf2017-02-041-2/+6
|
* Further improve cover() supportClifford Wolf2017-02-041-3/+5
|
* Added support for partially initialized regs to smt2 back-endClifford Wolf2016-12-011-3/+15
|
* Bugfix in smt2 back-end for pure checker modulesClifford Wolf2016-11-281-0/+4
|
* cleanup in write_smt2 log messages (-bv and -mem are now default)Clifford Wolf2016-10-161-1/+1
|
* Added $anyseq cell typeClifford Wolf2016-10-141-1/+1
|
* Added $ff and $_FF_ cell typesClifford Wolf2016-10-121-5/+5
|
* Improved handling of SMT2 logics in yosys-smtbmcClifford Wolf2016-09-181-1/+7
|
* fixed write_smt2 for (non-combinatorial) loops through hierarchical cellsClifford Wolf2016-09-101-17/+34
|
* smt2 mem init bugfixClifford Wolf2016-09-081-4/+6
|
* yosys-smtbmc meminit supportClifford Wolf2016-09-081-3/+23
|
* Minor bugfix in write_smt2Clifford Wolf2016-09-041-3/+3
|
* Added boolector support to yosys-smtbmcClifford Wolf2016-09-031-9/+21
|
* Added $anyconst support to yosys-smtbmcClifford Wolf2016-08-301-1/+3
|
* Fixed memory bug in write_smt2Clifford Wolf2016-08-301-9/+23
|
* Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"Clifford Wolf2016-08-301-14/+18
|
* Added $anyconst support to smt2 back-endClifford Wolf2016-08-301-0/+17
|
* Various fixes and improvements in smt2 back-endClifford Wolf2016-08-261-80/+116
|
* yosys-smtbmc: improved --dump-vlogtb handling of memoriesClifford Wolf2016-08-211-2/+6
|