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

1069 Commits

Author SHA1 Message Date
whitequark 784bfec67c
Merge pull request #2110 from BracketMaster/master 
MacOS has even stricter stack limits in catalina.
 2020-06-06 12:23:06 +00:00
whitequark bd2ecc2dd3
Merge pull request #2113 from whitequark/cxxrtl-fix-sshr 
cxxrtl: fix implementation of $sshr cell
 2020-06-05 10:24:25 +00:00
N. Engelhardt 9669e0c7d5
Merge pull request #2109 from nakengelhardt/btor_internal_names 
btor backend: make not printing internal names default
 2020-06-05 11:36:08 +02:00
whitequark 025663adff cxxrtl: fix implementation of $sshr cell. 
Fixes #2111.
 2020-06-05 02:04:46 +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
Eddie Hung 69850204c4
Merge pull request #2077 from YosysHQ/eddie/abc9_dff_improve 
abc9: -dff improvements
 2020-06-04 08:15:25 -07:00
N. Engelhardt 82798ae575 btor backend: make not printing internal names default 2020-06-04 16:24:16 +02:00
Claire Wolf 5e8a9c61cd Add printf format attributes to btorf/infof helper functions 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
 2020-06-04 15:53:28 +02:00
N. Engelhardt 8ceb6686e0 btor backend: add option to not include internal names 2020-06-04 14:00:52 +02:00
whitequark 3bffd09d64
Merge pull request #2006 from jersey99/signed-in-rtlil-wire 
Preserve 'signed'-ness of a verilog wire through RTLIL
 2020-06-04 11:23:06 +00:00
Eddie Hung 45cd323055
Merge pull request #2082 from YosysHQ/eddie/abc9_scc_fixes 
abc9: fixes around handling combinatorial loops
 2020-06-03 17:35:46 -07: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
clairexen 1c8d5a08a0
Merge pull request #2016 from boqwxp/qbfsat-yices 
qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.
 2020-05-29 16:21:45 +02:00
Xiretza edd8ff2c07
Add flooring division 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 $divfloor cell provides this flooring division.

This commit also fixes the handling of $div in opt_expr, which was
previously optimized as if it was $divfloor.
 2020-05-28 22:59:04 +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
whitequark 736ccb2ad5
Merge pull request #2031 from epfl-vlsc/master 
Add extmodule support to firrtl backend
 2020-05-28 09:59:17 +00:00
whitequark 2974183855
Merge pull request #2063 from boqwxp/techmapped-firrtl 
firrtl: Accept techmapped cell types in FIRRTL backend.
 2020-05-28 09:42:58 +00:00
whitequark 0bf6b164be cxxrtl: make logging a little bit nicer. 2020-05-26 21:37:32 +00:00
whitequark e9c07e2bda cxxrtl: add missing parts of commit 281c9685. 2020-05-26 21:34:20 +00:00
Eddie Hung 1826370b3a xaiger: promote abc9_keep wires 2020-05-25 16:40:30 -07: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
Eddie Hung 9e6c288e5a xaiger: cleanup 2020-05-25 08:43:33 -07:00
Eddie Hung d64df21630 xaiger: do not derive cells 2020-05-24 08:17:30 -07:00
whitequark 281c96856a cxxrtl: get rid of -O5 aka `opt_clean -purge` optimization level. 
This isn't actually necessary anymore after scheduling was improved,
and `clean -purge` disrupts the mapping between wires in the input
RTLIL netlist and the output CXXRTL code.
 2020-05-22 19:08:30 +00:00
N. Engelhardt 7c4e580f8f
Merge pull request #2054 from boqwxp/fix-smtbmc 
smtbmc: Fix return status handling.
 2020-05-20 08:55:36 +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 049e4caceb
firrtl: Accept techmapped cell types in FIRRTL backend. 2020-05-17 10:03:11 +00:00
Eddie Hung 67fc0c3698 abc9: use (* abc9_keep *) instead of (* abc9_scc *); apply to $_DFF_?_ 
instead of moving them to $__ prefix
 2020-05-14 16:44:35 -07:00
Eddie Hung 97a0a04314 abc9_ops/xaiger: further reducing Module::derive() calls by ... 
replacing _all_ (* abc9_box *) instantiations with their derived types
 2020-05-14 10:33:57 -07:00
Eddie Hung e79127fceb Cleanup; reduce Module::derive() calls 2020-05-14 10:33:57 -07:00
Eddie Hung e357b40e7a xaiger: no longer use nonstandard even/odd to designate +ve/-ve polarity 2020-05-14 10:33:56 -07:00
Eddie Hung 722540dbf9 abc9: not enough to techmap_fail on (* init=1 *), hide them using $__ 2020-05-14 10:33:56 -07:00
Eddie Hung 63246a5c0e Revert "Merge pull request #1917 from YosysHQ/eddie/abc9_delay_check" 
This reverts commit 759283fa65, reversing
changes made to f41c7ccfff.
 2020-05-14 10:33:56 -07:00
Eddie Hung 4c6647a469 xaiger: always sort input/output bits by port id 
redundant for normal design, but necessary for holes
 2020-05-14 10:33:56 -07:00
Eddie Hung ec4bbb1444 abc9: generate $abc9_holes design instead of <name>$holes 2020-05-14 10:33:56 -07:00
Eddie Hung 6f4f795953 aiger/xaiger: use odd for negedge clk, even for posedge 
Since abc9 doesn't like negative mergeability values
 2020-05-14 10:33:56 -07:00
Eddie Hung f975cf39cb xaiger: update help text 2020-05-14 10:33:56 -07:00
Eddie Hung 90cd49995b xaiger: do not treat (* init=1'bx *) as 1'b0 2020-05-14 10:33:56 -07:00
Eddie Hung 77f3abcdc3 xaiger: when -dff use (* init *) for initial state 2020-05-14 10:33:56 -07:00
Eddie Hung 95763c8d18 abc9_ops: add 'dff' label for auto handling of (* abc9_flop *) boxes 2020-05-14 10:33:56 -07:00
Eddie Hung ffa52738fb xaiger: output $_DFF_[NP]_ with mergeability if -dff option 2020-05-14 10:33:56 -07:00
Alberto Gonzalez 299ab76a09
smtbmc: Fix return status handling. 2020-05-14 17:07:59 +00:00
Xiretza d86fc791f9
Reorder cases to avoid fall-through warning 
log_assert(false) never returns and thus can't fall through, but gcc
doesn't seem to think that far. Making it the last case avoids the
problem entirely.
 2020-05-07 13:39:34 +02:00
Xiretza 695150b037
Add YS_FALLTHROUGH macro to mark case fall-through 
C++17 introduced [[fallthrough]], GCC and clang had their own vendored
attributes before that. MSVC doesn't seem to have such a warning at all.
 2020-05-07 13:39:34 +02:00
Sahand Kashani 1688a62500 Formatting fixes 2020-05-06 21:15:32 +02:00