mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-26 09:24:37 +00:00
Code Activity
13763 commits 122 branches 59 tags 72 MiB
Commit graph

314 commits

Author SHA1 Message Date
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
Clifford Wolf
3a8f6f0f51 Add verilator support to testbenches generated by yosys-smtbmc 2017-07-21 14:33:29 +02:00
Clifford Wolf
10c7709e68 Generate FSM-style testbenches in smtbmc 2017-07-12 15:57:04 +02:00
Clifford Wolf
3c693b6561 Change s/asserts/assertions/ in yosys-smtbmc log messages 2017-07-07 11:52:25 +02:00
Clifford Wolf
8f7404f82c Add "yosys-smtbmc --presat" 2017-07-07 02:47:30 +02:00
Clifford Wolf
3e0948e16f Remove unneeded delays in smtbmc vlogtb 2017-07-03 15:37:17 +02:00
Clifford Wolf
ea805af6f5 Add "yosys-smtbmc --vlogtb-top" 2017-07-01 18:19:23 +02:00
Clifford Wolf
7d2fb6e2fc Fix smtbmc vlogtb bug in $anyseq handling 2017-07-01 02:13:32 +02:00
Clifford Wolf
8f8baccfde Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand const reg" 2017-06-07 12:30:24 +02:00
Clifford Wolf
d9201b85f3 Change default smt2 solver to yices (Yices 2 has switched its license to GPL) 2017-05-27 11:56:01 +02:00
Clifford Wolf
05cdd58c8d Add $_ANDNOT_ and $_ORNOT_ gates 2017-05-17 09:08:29 +02:00
Clifford Wolf
1a4b7c6bfa Fix boolector support in yosys-smtbmc 2017-05-08 14:33:22 +02:00
Clifford Wolf
106e44f406 Add "write_smt2 -stdt" mode 2017-03-20 12:00:35 +01:00
Clifford Wolf
c855353986 Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg 2017-03-04 23:41:54 +01:00
Clifford Wolf
fbd52ec6dd Use hex addresses in smtbmc vcd mem traces 2017-02-28 13:54:50 +01:00