Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge pull request #591 from hzeller/virtual-override | Clifford Wolf | 2018-08-15 | 15 | -36/+36 |
|\ | | | | | Consistent use of 'override' for virtual methods in derived classes. | ||||
| * | Consistent use of 'override' for virtual methods in derived classes. | Henner Zeller | 2018-07-20 | 15 | -36/+36 |
| | | | | | | | | | | | | | | | | | | 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) | ||||
* | | Merge pull request #576 from cr1901/no-resource | Clifford Wolf | 2018-08-15 | 1 | -9/+12 |
|\ \ | | | | | | | Gate POSIX-only signals and resource module to only run on POSIX Pyth… | ||||
| * | | Gate POSIX-only signals and resource module to only run on POSIX Python ↵ | William D. Jones | 2018-07-06 | 1 | -9/+12 |
| |/ | | | | | | | implementations. | ||||
* | | Fix use of signed integers in JSON back-end | Clifford Wolf | 2018-08-14 | 1 | -1/+3 |
| | | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | | Use `realpath` | jpathy | 2018-08-06 | 1 | -1/+1 |
|/ | | | Use `os.path.realpath` instead to make sure symlinks are followed. This is also required to work for nix package manager. | ||||
* | Fix protobuf build | Sergiusz Bazanski | 2018-06-20 | 1 | -1/+1 |
| | |||||
* | Add Protobuf backend | Serge Bazanski | 2018-06-19 | 3 | -0/+380 |
| | | | | Signed-off-by: Serge Bazanski <q3k@symbioticeda.com> | ||||
* | Add $dlatch support to write_verilog | Clifford Wolf | 2018-04-22 | 1 | -0/+38 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Add "write_blif -inames -iattr" | Clifford Wolf | 2018-04-15 | 1 | -22/+46 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants | Clifford Wolf | 2018-04-04 | 1 | -0/+3 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Fixed -stbv handling in SMT2 back-end | Clifford Wolf | 2018-04-04 | 1 | -1/+1 |
| | |||||
* | Add smtio status msgs when --progress is inactive | Clifford Wolf | 2018-03-29 | 1 | -2/+23 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Bugfix in smtio.py VCD file generator | Clifford Wolf | 2018-03-29 | 1 | -1/+1 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Add $mem support to SMT2 clock tagging | Clifford Wolf | 2018-03-27 | 1 | -0/+18 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Improve yosys-smtbmc log output and error handling | Clifford Wolf | 2018-03-17 | 1 | -5/+14 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Improve handling of invalid check-sat result in smtio.py | Clifford Wolf | 2018-03-17 | 1 | -1/+2 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Remove debug prints from yosys-smtbmc VCD writer | Clifford Wolf | 2018-03-08 | 1 | -2/+0 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Check results of (check-sat) in yosys-smtbmc | Clifford Wolf | 2018-03-07 | 1 | -0/+2 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Imporove yosys-smtbmc error handling, Improve VCD output | Clifford Wolf | 2018-03-05 | 2 | -23/+49 |
| | | | | 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> | ||||
* | Fix a hangup in yosys-smtbmc error handling | Clifford Wolf | 2018-03-04 | 1 | -3/+5 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Improved error handling in yosys-smtbmc | Clifford Wolf | 2018-03-03 | 1 | -1/+3 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Terminate running SMT solver when smtbmc is terminated | Clifford Wolf | 2018-03-03 | 1 | -1/+31 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Fix smtbmc smtc/aiw parser for wire names containing [] | Clifford Wolf | 2018-03-03 | 1 | -1/+1 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Mangle names with square brackets in VCD files to work around issues in gtkwave | Clifford Wolf | 2018-03-01 | 1 | -2/+8 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Small fixes and improvements in $allconst/$allseq handling | Clifford Wolf | 2018-02-26 | 1 | -12/+18 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Add smtbmc support for exist-forall problems | Clifford Wolf | 2018-02-23 | 3 | -87/+334 |
| | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at> | ||||
* | Add support for mockup clock signals in yosys-smtbmc vcd output | Clifford Wolf | 2018-02-20 | 3 | -6/+111 |
| | | | | 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> | ||||
* | Fixed gcc 7.2 "statement will never be executed" warning | Clifford Wolf | 2018-02-03 | 1 | -1/+1 |
| | |||||
* | Fix smtio.py for large SMT2 S-expressions | Clifford Wolf | 2018-01-29 | 1 | -1/+12 |
| | |||||
* | Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output | Clifford Wolf | 2018-01-18 | 1 | -3/+3 |
| | |||||
* | Add "no driver for signal bit" error msg to btor back-end | Clifford Wolf | 2017-12-24 | 1 | -0/+2 |
| | |||||
* | Simple fix BTOR memory encoding | Clifford Wolf | 2017-12-17 | 1 | -2/+2 |
| | |||||
* | Improve BTOR memory encoding | Clifford Wolf | 2017-12-17 | 1 | -2/+16 |
| | |||||
* | Add array support to btor back-end | Clifford Wolf | 2017-12-15 | 1 | -6/+169 |
| | |||||
* | Add $anyconst/$anyseq support to btor back-end | Clifford Wolf | 2017-12-15 | 1 | -13/+51 |
| | |||||
* | Merge branch 'master' into btor-ng | Clifford Wolf | 2017-12-14 | 3 | -7/+11 |
|\ | |||||
| * | Add yosys-smtbmc VCD writer support for memories with async writes | Clifford Wolf | 2017-12-14 | 3 | -7/+11 |
| | | |||||
* | | Merge branch 'master' into btor-ng | Clifford Wolf | 2017-12-14 | 1 | -14/+53 |
|\| | |||||
| * | Add smt2 back-end support for async write memories | Clifford Wolf | 2017-12-14 | 1 | -14/+53 |
| | | |||||
| * | Fixed "yosys-smtbmc -g" handling of no solution | Clifford Wolf | 2017-11-27 | 1 | -1/+1 |
| | | |||||
* | | Add "write_btor -s" mode | Clifford Wolf | 2017-12-13 | 1 | -6/+50 |
| | | |||||
* | | Add state initval handling to btor back-end | Clifford Wolf | 2017-12-12 | 1 | -0/+25 |
| | | |||||
* | | Add btor back-end support for 'x' constants | Clifford Wolf | 2017-12-12 | 1 | -1/+54 |
| | | |||||
* | | Add btor $shift/$shiftx support | Clifford Wolf | 2017-12-11 | 2 | -7/+37 |
| | | |||||
* | | Fix btor back-end shift handling | Clifford Wolf | 2017-12-10 | 2 | -5/+7 |
| | | |||||
* | | Add support for $pmux in btor back-end | Clifford Wolf | 2017-12-10 | 1 | -0/+23 |
| | | |||||
* | | Add support for more cell types to btor back-end | Clifford Wolf | 2017-12-10 | 2 | -6/+245 |
| | |