riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
4,390 Commits 76 Branches 48 Tags 62 MiB
Commit Graph

178 Commits

Author SHA1 Message Date
Clifford Wolf e112d2fbf5 Add missing blackslash-to-slash convertion to smtio.py (matching Smt2Worker::get_id() behavior) 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-02-06 16:35:59 +01:00
whitequark efa278e232 Fix typographical and grammatical errors and inconsistencies. 
The initial list of hits was generated with the codespell command
below, and each hit was evaluated and fixed manually while taking
context into consideration.

    DIRS="kernel/ frontends/ backends/ passes/ techlibs/"
    DIRS="${DIRS} libs/ezsat/ libs/subcircuit"
    codespell $DIRS -S *.o -L upto,iff,thru,synopsys,uint

More hits were found by looking through comments and strings manually.
 2019-01-02 13:12:17 +00:00
Clifford Wolf 0b9bb852c6 Add yosys-smtbmc support for btor witness 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-10 03:43:07 +01:00
Clifford Wolf 47a5dfdaa4 Add "yosys-smtbmc --btorwit" skeleton 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-08 06:59:27 +01:00
Clifford Wolf 825b4c1aa9
Merge pull request #693 from YosysHQ/rlimit 
improve rlimit handling in smtio.py
 2018-11-07 20:16:40 +01:00
Clifford Wolf b54bf7c0f9 Limit stack size to 16 MB on Darwin 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-11-07 15:32:34 +01:00
Clifford Wolf f6c4485a3a Run solver in non-incremental mode whem smtio.py is configured for non-incremental solving 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-11-06 11:11:05 +01:00
Clifford Wolf 4c50e3abb9 Fix for improved smtio.py rlimit code 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-11-06 10:09:03 +01:00
Clifford Wolf 79075d123f Improve stack rlimit code in smtio.py 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-11-06 10:05:23 +01:00
Arjen Roodselaar 2b93542171 Use conservative stack size for SMT2 on MacOS 2018-11-04 21:58:09 -08:00
Clifford Wolf d0acea4f2e Add proper error message for when smtbmc "append" fails 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-11-04 14:41:28 +01:00
Clifford Wolf b6781c6f4b Add support for signed $shift/$shiftx in smt2 back-end 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-11-01 11:40:58 +01:00
Clifford Wolf 67b1026297
Merge pull request #591 from hzeller/virtual-override 
Consistent use of 'override' for virtual methods in derived classes.
 2018-08-15 14:05:38 +02:00
Clifford Wolf dfc0c8ffc8
Merge pull request #576 from cr1901/no-resource 
Gate POSIX-only signals and resource module to only run on POSIX Pyth…
 2018-08-15 14:00:19 +02:00
jpathy 7db05b2cc1
Use `realpath` 
Use `os.path.realpath` instead to make sure symlinks are followed. This is also required to work for nix package manager.
 2018-08-06 06:51:07 +00:00
Henner Zeller 3aa4484a3c Consistent use of 'override' for virtual methods in derived classes. 
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)
 2018-07-20 23:51:06 -07:00
William D. Jones 0caa62802c Gate POSIX-only signals and resource module to only run on POSIX Python implementations. 2018-07-06 01:44:34 -04:00
Clifford Wolf 4d6af2969c Add smtio.py support for parsing SMT2 (_ bvX n) syntax for BitVec constants 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-04-04 18:12:27 +02:00
Clifford Wolf 25a864fc73 Fixed -stbv handling in SMT2 back-end 2018-04-04 17:28:07 +02:00
Clifford Wolf dd5fab69c1 Add smtio status msgs when --progress is inactive 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-29 21:59:30 +02:00
Clifford Wolf a48c7e5abf Bugfix in smtio.py VCD file generator 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-29 12:45:31 +02:00
Clifford Wolf 77bd645c35 Add $mem support to SMT2 clock tagging 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-27 02:11:20 +02:00
Clifford Wolf 3f00702475 Improve yosys-smtbmc log output and error handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-17 18:06:17 +01:00
Clifford Wolf 4d4e3a8ca6 Improve handling of invalid check-sat result in smtio.py 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-17 12:17:53 +01:00
Clifford Wolf 3545c0fffb Remove debug prints from yosys-smtbmc VCD writer 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-08 16:24:35 +01:00
Clifford Wolf 8b604004da Check results of (check-sat) in yosys-smtbmc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-07 22:54:19 +01:00
Clifford Wolf cedbc35f4b Imporove yosys-smtbmc error handling, Improve VCD output 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-05 12:17:22 +01:00
Clifford Wolf 8b7602e660 Improve SMT2 encoding of $reduce_{and,or,bool} 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 21:22:20 +01:00
Clifford Wolf 45a6fce92c Fix a hangup in yosys-smtbmc error handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 21:13:30 +01:00
Clifford Wolf ae4e204c76 Improved error handling in yosys-smtbmc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-03 20:00:07 +01:00
Clifford Wolf a44e1edaa3 Terminate running SMT solver when smtbmc is terminated 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-03 14:50:40 +01:00
Clifford Wolf 3ced2cca6e Fix smtbmc smtc/aiw parser for wire names containing [] 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-03 14:15:49 +01:00
Clifford Wolf 90ae426078 Mangle names with square brackets in VCD files to work around issues in gtkwave 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-01 14:15:27 +01:00
Clifford Wolf 675dd5347a Small fixes and improvements in $allconst/$allseq handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-26 11:58:44 +01:00
Clifford Wolf b13e6bd375 Add smtbmc support for exist-forall problems 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-23 19:33:30 +01:00
Clifford Wolf 17583b6a21 Add support for mockup clock signals in yosys-smtbmc vcd output 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-20 17:45:22 +01:00
Clifford Wolf c9672e2e2e Fix handling of zero-length cell connections in SMT2 back-end 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-08 19:12:12 +01:00
Clifford Wolf e97f10b142 Fix smtio.py for large SMT2 S-expressions 2018-01-29 12:34:28 +01:00
Clifford Wolf 54aeca0983 Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output 2018-01-18 14:25:22 +01:00
Clifford Wolf 9419de3e37 Add yosys-smtbmc VCD writer support for memories with async writes 2017-12-14 03:06:00 +01:00
Clifford Wolf 2625da6440 Add smt2 back-end support for async write memories 2017-12-14 02:07:10 +01:00
Clifford Wolf da91b31bb2 Fixed "yosys-smtbmc -g" handling of no solution 2017-11-27 19:43:36 +01:00
Clifford Wolf 455c1c9d97 Fix SMT2 handling of initstate in sub-modules 2017-10-29 13:21:20 +01:00
Clifford Wolf 1170508264 Improve smtio performance by using reader thread, not writer thread 2017-10-26 01:01:55 +02:00
Clifford Wolf f513494f5f Use separate writer thread for talking to SMT solver to avoid read/write deadlock 2017-10-25 19:59:56 +02:00
Clifford Wolf 76326c163a Improve p_* functions in smtio.py 2017-10-25 15:45:32 +02:00
Clifford Wolf c672c321e3 Capsulate smt-solver read/write in separate functions 2017-10-25 13:37:11 +02:00
Clifford Wolf dd46d76394 Fix a bug in yosys-smtbmc in ROM handling 2017-10-25 13:05:14 +02:00
Clifford Wolf c2d737457a Fix bug in write_smt2 (export logic driving hierarchical cells before exporting regs) 2017-08-25 11:44:48 +02:00
Clifford Wolf 48b2b376d0 Add "yosys-smtbmc --smtc-init --smtc-top --noinit" 2017-08-04 17:09:08 +02:00