| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Add "whitebox" attribute, add "read_verilog -wb" | Clifford Wolf | 2019-04-18 | 1 | -1/+1 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix signed $shift/$shiftx handling in write_smt2 | Clifford Wolf | 2019-03-09 | 1 | -1/+2 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Use SVA label in smt export if available | Clifford Wolf | 2019-03-07 | 1 | -2/+2 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix smt2 code generation for partially initialized memowy words, fixes #831 | Clifford Wolf | 2019-02-28 | 1 | -4/+11 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add support for signed $shift/$shiftx in smt2 back-end | Clifford Wolf | 2018-11-01 | 1 | -1/+3 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Consistent use of 'override' for virtual methods in derived classes. | Henner Zeller | 2018-07-20 | 1 | -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-end | Clifford Wolf | 2018-04-04 | 1 | -1/+1 |
| | | |||||
| * | Add $mem support to SMT2 clock tagging | Clifford Wolf | 2018-03-27 | 1 | -0/+18 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Improve SMT2 encoding of $reduce_{and,or,bool} | Clifford Wolf | 2018-03-04 | 1 | -1/+9 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add smtbmc support for exist-forall problems | Clifford Wolf | 2018-02-23 | 1 | -10/+72 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Add support for mockup clock signals in yosys-smtbmc vcd output | Clifford Wolf | 2018-02-20 | 1 | -3/+57 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | Fix handling of zero-length cell connections in SMT2 back-end | Clifford Wolf | 2018-02-08 | 1 | -0/+8 |
| | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
| * | 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 |
| | | |||||
| * | Fix SMT2 handling of initstate in sub-modules | Clifford Wolf | 2017-10-29 | 1 | -0/+3 |
| | | |||||
| * | Fix bug in write_smt2 (export logic driving hierarchical cells before ↵ | Clifford Wolf | 2017-08-25 | 1 | -34/+34 |
| | | | | | exporting regs) | ||||
| * | Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand ↵ | Clifford Wolf | 2017-06-07 | 1 | -2/+4 |
| | | | | | const reg" | ||||
| * | Add $_ANDNOT_ and $_ORNOT_ gates | Clifford Wolf | 2017-05-17 | 1 | -0/+2 |
| | | |||||
| * | Add "write_smt2 -stdt" mode | Clifford Wolf | 2017-03-20 | 1 | -9/+47 |
| | | |||||
| * | Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg | Clifford Wolf | 2017-03-04 | 1 | -31/+85 |
| | | |||||
| * | Fix extra newline bug in write_smt2 | Clifford Wolf | 2017-02-26 | 1 | -1/+1 |
| | | |||||
| * | Improve (and fix for stbv mode) SMT2 memory API | Clifford Wolf | 2017-02-26 | 1 | -25/+24 |
| | | |||||
| * | Add "write_smt2 -stbv" | Clifford Wolf | 2017-02-24 | 1 | -44/+174 |
| | | |||||
| * | Add SMT2 statebv mode (inactive for now) | Clifford Wolf | 2017-02-24 | 1 | -20/+47 |
| | | |||||
| * | Partially implement cover() support in yosys-smtbmc | Clifford Wolf | 2017-02-04 | 1 | -2/+6 |
| | | |||||
| * | Further improve cover() support | Clifford Wolf | 2017-02-04 | 1 | -3/+5 |
| | | |||||
| * | Added support for partially initialized regs to smt2 back-end | Clifford Wolf | 2016-12-01 | 1 | -3/+15 |
| | | |||||
| * | Bugfix in smt2 back-end for pure checker modules | Clifford Wolf | 2016-11-28 | 1 | -0/+4 |
| | | |||||
| * | cleanup in write_smt2 log messages (-bv and -mem are now default) | Clifford Wolf | 2016-10-16 | 1 | -1/+1 |
| | | |||||
| * | Added $anyseq cell type | Clifford Wolf | 2016-10-14 | 1 | -1/+1 |
| | | |||||
| * | Added $ff and $_FF_ cell types | Clifford Wolf | 2016-10-12 | 1 | -5/+5 |
| | | |||||
| * | Improved handling of SMT2 logics in yosys-smtbmc | Clifford Wolf | 2016-09-18 | 1 | -1/+7 |
| | | |||||
| * | fixed write_smt2 for (non-combinatorial) loops through hierarchical cells | Clifford Wolf | 2016-09-10 | 1 | -17/+34 |
| | | |||||
| * | smt2 mem init bugfix | Clifford Wolf | 2016-09-08 | 1 | -4/+6 |
| | | |||||
| * | yosys-smtbmc meminit support | Clifford Wolf | 2016-09-08 | 1 | -3/+23 |
| | | |||||
| * | Minor bugfix in write_smt2 | Clifford Wolf | 2016-09-04 | 1 | -3/+3 |
| | | |||||
| * | Added boolector support to yosys-smtbmc | Clifford Wolf | 2016-09-03 | 1 | -9/+21 |
| | | |||||
| * | Added $anyconst support to yosys-smtbmc | Clifford Wolf | 2016-08-30 | 1 | -1/+3 |
| | | |||||
| * | Fixed memory bug in write_smt2 | Clifford Wolf | 2016-08-30 | 1 | -9/+23 |
| | | |||||
| * | Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem" | Clifford Wolf | 2016-08-30 | 1 | -14/+18 |
| | | |||||
| * | Added $anyconst support to smt2 back-end | Clifford Wolf | 2016-08-30 | 1 | -0/+17 |
| | | |||||
| * | Various fixes and improvements in smt2 back-end | Clifford Wolf | 2016-08-26 | 1 | -80/+116 |
| | | |||||
| * | yosys-smtbmc: improved --dump-vlogtb handling of memories | Clifford Wolf | 2016-08-21 | 1 | -2/+6 |
| | | |||||
| * | Deprecated "write_smt2 -regs" (by default on now), and some other smt2 ↵ | Clifford Wolf | 2016-08-20 | 1 | -28/+26 |
| | | | | | back-end improvements | ||||
| * | Added printing of code loc of failed asserts to yosys-smtbmc | Clifford Wolf | 2016-08-17 | 1 | -1/+3 |
| | | |||||
| * | Added $initstate support to smtbmc flow | Clifford Wolf | 2016-07-27 | 1 | -1/+14 |
| | | |||||
| * | Moved smt2 yosys info parsing from smtbmc.py to smtio.py | Clifford Wolf | 2016-07-11 | 1 | -0/+4 |
| | | |||||
| * | Support for hierarchical designs in smt2 back-end | Clifford Wolf | 2016-07-10 | 1 | -18/+130 |
| | | |||||
| * | Added "yosys -D" feature | Clifford Wolf | 2016-04-21 | 1 | -1/+1 |
| | | |||||
| * | Import more std:: stuff into Yosys namespace | Clifford Wolf | 2015-10-25 | 1 | -2/+2 |
| | | |||||
 |
index : iCE40/yosys | |
| [no description] |
| aboutsummaryrefslogtreecommitdiffstats |