aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smt2.cc
Commit message (Expand)AuthorAgeFilesLines
* 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
* 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
* Deprecated "write_smt2 -regs" (by default on now), and some other smt2 back-e...Clifford Wolf2016-08-201-28/+26
* Added printing of code loc of failed asserts to yosys-smtbmcClifford Wolf2016-08-171-1/+3
* Added $initstate support to smtbmc flowClifford Wolf2016-07-271-1/+14
* Moved smt2 yosys info parsing from smtbmc.py to smtio.pyClifford Wolf2016-07-111-0/+4
* Support for hierarchical designs in smt2 back-endClifford Wolf2016-07-101-18/+130
* Added "yosys -D" featureClifford Wolf2016-04-211-1/+1
* Import more std:: stuff into Yosys namespaceClifford Wolf2015-10-251-2/+2
* renamed SigSpec::to_single_sigbit() to SigSpec::as_bit(), added is_bit()Clifford Wolf2015-10-241-2/+2
* Improvements in yosys-smtbmcClifford Wolf2015-10-151-0/+1
* Added write_smt2 -wiresClifford Wolf2015-10-131-7/+15
* Added "yosys-smt2-wire" tag support to smt2 back-endClifford Wolf2015-08-311-0/+2
* Fixed generation of smt2 concat statementsClifford Wolf2015-08-151-3/+5
* Added "write_smt2 -regs"Clifford Wolf2015-08-121-7/+36
* Use MEMID as name for $mem cellClifford Wolf2015-08-091-1/+6
* Fixed trailing whitespacesClifford Wolf2015-07-021-2/+2