mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-12 20:18:20 +00:00
Code Activity
9754 commits 97 branches 53 tags 41 MiB
Commit graph

92 commits

Author SHA1 Message Date
Yehowshua Immanuel 5d29a9f633
MacOS has even stricter stack limits in catalina. 
Invoking sby in macOS Catalina fails because of bizarre stack limits in Catalina.
 2020-06-04 14:01:56 -04:00
Alberto Gonzalez ea30465107
smtbmc: Remove superfluous yosys-smt2-timeout file macro. 
Co-Authored-By: clairexen <claire@symbioticeda.com>
 2020-05-29 21:33:00 +00:00
Alberto Gonzalez 9847a4eea8
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4. 2020-05-25 20:39:30 +00:00
Alberto Gonzalez 54570a3978
qbfsat: Move SMT2 info statements back to the top of the file. 2020-05-25 20:38:29 +00:00
Alberto Gonzalez 903456c267
qbfsat: Add -solver option and allow choice of Z3 or Yices, making Yices the default. 
Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode.
 2020-05-25 20:38:29 +00:00
Alberto Gonzalez d72cb8ea2a
Do not change solver output parsing for non-exists-forall problems. 2020-03-26 23:00:00 +00:00
Alberto Gonzalez 5accf08ef9
Skip reading stdout from the solver that if it isn't a line reading only "sat", "unsat", or "unknown". 2020-03-26 01:21:01 +00:00
Claire Wolf c9555c9ade Revert part of 0fda8308 from #1746 that broke other smtbmc flows 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
 2020-03-24 17:33:46 +01:00
Alberto Gonzalez 0fda8308bc Add support for optimizing exists-forall problems. 
Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate.
Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al.
Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
 2020-03-13 17:10:29 +00:00
Claire Wolf 485f31f681 Improve yosys-smtbmc "solver not found" handling 
Signed-off-by: Claire Wolf <clifford@clifford.at>
 2020-01-27 17:48:56 +01:00
Clifford Wolf f02623abb5 Bugfix in smtio vcd handling of $-identifiers 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-10-23 00:04:34 +02:00
N. Engelhardt ab4b9e8db4 smt: handle failure of setrlimit syscall 2019-07-15 23:33:18 +08:00
Clifford Wolf b3c36b4448 Escape scope names starting with dollar sign in smtio.py 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-06-26 10:58:39 +02:00
Clifford Wolf c23bbc4291 Add timescale and generated-by header to yosys-smtbmc MkVcd 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-06-16 23:12:03 +02:00
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
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
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 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 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 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 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 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 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 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 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 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 6e152f7aa1 Fix bug in smtio unroll code 2017-02-26 14:39:07 +01:00
Clifford Wolf fd1cc0c73d Improve (and fix for stbv mode) SMT2 memory API 2017-02-26 10:58:34 +01:00