mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-30 19:22:31 +00:00
Code Activity
12380 commits 122 branches 59 tags 72 MiB
Commit graph

290 commits

Author SHA1 Message Date
Miodrag Milanović
a95e5d505b
Merge pull request #3186 from nakengelhardt/smtbmc_sby_print_id 
add argument for printing cell names in yosys-smtbmc
 2022-03-04 16:39:12 +01:00
N. Engelhardt
dc739362c7 print cell name for properties in yosys-smtbmc 2022-02-22 17:00:10 +01:00
Claire Xenia Wolf
30eb7f8665 Add a bit of flexibilty re trace length when processing aiger witnesses in smtbmc.py 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2022-02-11 17:24:49 +01:00
Marcelina Kościelnicka
93508d58da Add $bmux and $demux cells. 2022-01-28 23:34:41 +01:00
Marcelina Kościelnicka
e7d89e653c Hook up $aldff support in various passes. 2021-10-02 21:01:21 +02:00
Marcelina Kościelnicka
33749f1e3a yosys-smtbmc: Fix reused loop variable. 
Fixes #2999.
 2021-09-10 13:34:58 +02:00
GCHQDeveloper560
4379375d89 Add support for the Bitwuzla solver 2021-07-12 22:07:58 +02:00
Claire Xenia Wolf
72787f52fc Fixing old e-mail addresses and deadnames 
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g;
 2021-06-08 00:39:36 +02:00
Marcelina Kościelnicka
cbf6b719fe Make a few passes auto-call Mem::narrow instead of rejecting wide ports. 
This essentially adds wide port support for free in passes that don't
have a usefully better way of handling wide ports than just breaking
them up to narrow ports, avoiding "please run memory_narrow" annoyance.
 2021-05-28 00:40:56 +02:00
Marcelina Kościelnicka
69bf5c81c7 Reject wide ports in some passes that will never support them. 2021-05-25 02:07:25 +02:00
Marcelina Kościelnicka
c4cc888b2c kernel/rtlil: Extract some helpers for checking memory cell types. 
There will soon be more (versioned) memory cells, so handle passes that
only care if a cell is memory-related by a simple helper call instead of
a hardcoded list.
 2021-05-22 21:43:00 +02:00
Marcelina Kościelnicka
979347999f btor, smt2, smv: Add a hint on how to deal with funny FF types. 2021-02-25 22:04:04 +01:00
Marcelina Kościelnicka
f272c8b407 smt2: Use Mem helper. 2020-10-21 17:51:20 +02:00
Jakob Wenzel
54166ae0c5 smtbmc: escape identifiers in verilog testbench 2020-10-06 11:27:14 +02:00
N. Engelhardt
3238190797 use the new isPublic() in a few places 2020-09-14 12:43:18 +02:00
whitequark
c1fff52477
write_smt2: fix SMT-LIB tutorial URL 2020-08-29 20:02:35 +00:00
Noah Moroze
91682d189e Ensure smt2 comments are associated with accessors 2020-08-20 16:00:05 -04:00
Alberto Gonzalez
42fb75c570
smtio: Emit mode: start options before set-logic command and any other options after it. 
Refer to the SMT-LIB specification, section 4.1.7.  According to the spec, some options can only be specified in `start` mode.  Once the solver sees `set-logic`, it moves to `assert` mode.
 2020-07-20 22:09:44 +00:00
Alberto Gonzalez
654864658f
smtio: Add support for parsing yosys-smt2-solver-option info statements. 2020-07-20 21:54:56 +00:00
Alberto Gonzalez
f037985337
smt2: Add -solver-option option. 2020-07-20 21:54:56 +00:00
Claire Wolf
a207cb362c Only allow "sat" and "unsat" smt solver responses in yosys-smtbmc 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
 2020-07-20 19:35:32 +02:00
whitequark
7191dd16f9 Use C++11 final/override keywords. 2020-06-18 23:34:52 +00:00
Yehowshua Immanuel
da0778350b
more reasonable numbers for memory 2020-06-04 17:00:04 -04:00
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
clairexen
ea46ed81f9
Merge pull request #2018 from boqwxp/qbfsat-timeout 
smtbmc and qbfsat: Add timeout option to set solver timeouts for Z3, Yices, and CVC4.
 2020-05-30 15:04:51 +02: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
clairexen
94c1035389
Merge pull request #1885 from Xiretza/mod-rem-cells 
Fix modulo/remainder semantics
 2020-05-29 16:37:23 +02:00
Xiretza
17163cf43a
Add flooring modulo operator 
The $div and $mod cells use truncating division semantics (rounding
towards 0), as defined by e.g. Verilog. Another rounding mode, flooring
(rounding towards negative infinity), can be used in e.g. VHDL. The
new $modfloor cell provides this flooring modulo (also known as "remainder"
in several languages, but this name is ambiguous).

This commit also fixes the handling of $mod in opt_expr, which was
previously optimized as if it was $modfloor.
 2020-05-28 22:59:03 +02: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
1053032a81
smtbmc: Fix typo in error message. 
Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
 2020-05-19 16:13:44 +00:00
Alberto Gonzalez
299ab76a09
smtbmc: Fix return status handling. 2020-05-14 17:07:59 +00:00
N. Engelhardt
0b7a5879e5
Merge pull request #1830 from boqwxp/qbfsat 
Add `qbfsat` command to integrate exists-forall solving and specialization
 2020-04-15 17:33:50 +02:00
Miodrag Milanovic
0d789c5a3b Support custom PROGRAM_PREFIX 2020-04-10 10:38:40 +02:00
Alberto Gonzalez
437afa1f0c
Updated yosys-smtbmc to optionally dump raw bit strings, and fixed hole value recovery using that mode. 2020-04-04 22:13:25 +00:00
Eddie Hung
956ecd48f7 kernel: big fat patch to use more ID::*, otherwise ID(*) 2020-04-02 09:51:32 -07:00
Eddie Hung
fdafb74eb7 kernel: use more ID::* 2020-04-02 07:14:08 -07:00
Alberto Gonzalez
c23c2c59c1
Update RTLIL::id2cstr() usage to log_id. 2020-04-01 06:53:28 +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
Teguh Hofstee
b08932cb81 fix typo in write_smt2 help 2020-03-23 02:14:26 -07:00
N. Engelhardt
020f6d167a
Merge pull request #1768 from boqwxp/smt2_cleanup 
Clean up pseudo-private member usage in `backends/smt2/smt2.cc`.
 2020-03-16 13:49:10 +01:00
Alberto Gonzalez
07f0874779 Clean up pseudo-private member usage in backends/smt2/smt2.cc. 2020-03-13 21:49:12 +00: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
Clifford Wolf
2ed2e9c3e8 Change smtbmc "Warmup failed" status to "PREUNSAT" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-10-03 14:59:07 +02:00
Sean Cross
c1b628508d backends: smt2: use $(CXX) variable for compiler 
The Makefile assumes the compiler is called `gcc`, which isn't always
true.  In fact, if we're building on msys2 or msys2-64, the compiler
is called `i686-w64-mingw32-g++` or `x86_64-w64-mingw32-g++`.

Use the variable instead of hardcoding the name, to fix building on
these systems.

Signed-off-by: Sean Cross <sean@xobs.io>
 2019-09-08 15:47:09 +08:00