riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
9,657 Commits 81 Branches 48 Tags 64 MiB
Commit Graph

210 Commits

Author SHA1 Message Date
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 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
Eddie Hung 6d77236f38 substr() -> compare() 2019-08-07 12:20:08 -07:00
Eddie Hung 3486235338 Make liberal use of IdString.in() 2019-08-06 16:18:18 -07:00
Clifford Wolf 023086bd46 Add $_NMUX_, add "abc -g cmos", add proper cmos cell costs 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-08-06 04:47:55 +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 f4abc21d8a Add "whitebox" attribute, add "read_verilog -wb" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-04-18 17:45:47 +02:00
Clifford Wolf bacca57537 Fix smtbmc.py handling of zero appended steps 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-03-14 22:04:42 +01:00
William D. Jones ff15cf9b1f Install launcher executable when running yosys-smtbmc on Windows. 
Signed-off-by: William D. Jones <thor0505@comcast.net>
 2019-03-13 13:49:16 -04:00
Clifford Wolf 94f995ee37 Fix signed $shift/$shiftx handling in write_smt2 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-03-09 13:19:41 -08:00
Clifford Wolf 5dfc7becca Use SVA label in smt export if available 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-03-07 11:31:46 -08:00
Clifford Wolf f570aa5e1d Fix smt2 code generation for partially initialized memowy words, fixes #831 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-02-28 12:15:58 -08: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
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