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

943 Commits

Author SHA1 Message Date
Claire Wolf d1fc4321f0
Merge pull request #1770 from YosysHQ/claire/btor_symbols 
Improve write_btor symbol handling
 2020-04-02 15:38:47 +02:00
Claire Wolf 104c004e6d
Merge pull request #1765 from YosysHQ/claire/btor_info 
Add info-file and cover features to write_btor
 2020-04-02 15:38:27 +02:00
Alberto Gonzalez c23c2c59c1
Update `RTLIL::id2cstr()` usage to `log_id`. 2020-04-01 06:53:28 +00:00
Alberto Gonzalez cdb14652be
Clean up pseudo-private member usage in `backends/intersynth/intersynth.cc`. 2020-04-01 06:32:09 +00:00
Alberto Gonzalez 24ef73904f
Clean up pseudo-private member usage in `backends/blif/blif.cc`. 2020-04-01 05:50:48 +00:00
Alberto Gonzalez f657fed24c
Clean up pseudo-private member usage in `backends/verilog/verilog_backend.cc`. 2020-04-01 05:25:10 +00:00
Alberto Gonzalez 68c0e3562e
Clean up pseudo-private member usage in `backends/spice/spice.cc`. 2020-04-01 04:56:52 +00:00
Alberto Gonzalez 057976c323
Clean up pseudo-private member usage in `backends/edif/edif.cc`. 2020-04-01 04:37:07 +00:00
Alberto Gonzalez 68fef4ca7f
Clean up pseudo-private member usage in `backends/ilang/ilang_backend.cc`. 2020-04-01 03:08:39 +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
N. Engelhardt a2e340de43
Merge pull request #1746 from boqwxp/optimization 
Add support for optimizing exists-forall problems.
 2020-03-16 12:23:14 +01:00
Claire Wolf bf018b184d Improve write_btor symbol handling 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
 2020-03-14 15:49:43 +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
Miodrag Milanovic 746629f18d remove include where not used 2020-03-13 14:55:53 +01:00
Claire Wolf 29e2b2dc05 Add info-file and cover features to write_btor 
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
 2020-03-13 13:46:32 +01:00
Eddie Hung 3be7784d0e xaiger: remove some unnecessary operations ... 
... since they can not be triggered by (* keep *) anymore
(but could still be triggered by (* abc9_scc *) !?!)
 2020-03-06 10:51:47 -08:00
Eddie Hung 91a7a74ac4 abc9: (* keep *) wires to be PO only, not PI as well; fix scc handling 2020-03-06 10:20:30 -08:00
Eddie Hung 6bb3d9f9c0 Make TimingInfo::TimingInfo(SigBit) constructor explicit 2020-02-27 10:17:29 -08:00
Eddie Hung 5ff60d2057 write_xaiger: add comment about arrival times of flop outputs 2020-02-27 10:17:29 -08:00
Eddie Hung 1ef1ca812b Get rid of (* abc9_{arrival,required} *) entirely 2020-02-27 10:17:29 -08:00
Eddie Hung e22fee6cdd abc9_ops: ignore (* abc9_flop *) if not '-dff' 2020-02-27 10:17:29 -08:00
Eddie Hung 12d70ca8fb xilinx: improve specify functionality 2020-02-27 10:17:29 -08:00
Eddie Hung 760096e8d2
Merge pull request #1703 from YosysHQ/eddie/specify_improve 
Improve specify parser
 2020-02-21 09:15:17 -08:00
Eddie Hung f9f86fd758 Revert "abc9: fix abc9_arrival for flops" 
This reverts commit f7c0dbecee.
 2020-02-14 16:08:04 -08:00
Eddie Hung b523ecf2f4 specify: system timing checks to accept min:typ:max triple 2020-02-13 12:42:15 -08:00
Eddie Hung f5cc8cfa79 write_xaiger: default value for abc9_init 2020-02-13 12:37:17 -08:00
Eddie Hung f7c0dbecee abc9: fix abc9_arrival for flops 2020-02-13 12:34:09 -08:00
R. Ou 20ce4118da json: Change compat mode to directly emit ints <= 32 bits 
This increases compatibility with certain older parsers in some cases
that worked before commit 15fae357 but do not work with the current
compat-int mode
 2020-02-09 01:01:18 -08:00
whitequark 6f67dd8df5
Merge pull request #1683 from whitequark/write_verilog-memattrs 
write_verilog: dump $mem cell attributes
 2020-02-07 02:54:04 +00:00
Marcin Kościelnicki 8f559b070a edif: more resilience to mismatched port connection sizes. 
Fixes #1653.
 2020-02-06 18:45:03 +01:00
whitequark e95a8ba763 write_verilog: dump $mem cell attributes. 
The Verilog backend already dumps attributes on RTLIL::Memory objects
but not on `$mem` cells.
 2020-02-06 16:22:42 +00:00
Eddie Hung 0671ae7d79
Merge pull request #1661 from YosysHQ/eddie/abc9_required 
abc9: add support for required times
 2020-02-05 18:59:40 +01:00
Marcin Kościelnicki 00fba62711 json: remove the 32-bit parameter special case 
Before, the rules for encoding parameters in JSON were as follows:

- if the parameter is not a string:

  - if it is exactly 32 bits long and there are no z or x bits, emit it
    as an int
  - otherwise, emit it as a string made of 0/1/x/z characters

- if the parameter is a string:

  - if it contains only 0/1/x/z characters, append a space at the end
    to distinguish it from a non-string
  - otherwise, emit it directly

However, this caused a problem in the json11 parser used in nextpnr:
yosys emits unsigned ints, and nextpnr parses them as signed, using
the value of INT_MIN for values that overflow the signed int range.
This caused destruction of LUT5 initialization values.  Since both
nextpnr and yosys parser can also accept 32-bit parameters in the
same encoding as other widths, let's just remove that special case.
The old behavior is still left behind a `-compat-int` flag, in case
someone relies on it.
 2020-02-01 16:16:26 +01:00
Claire Wolf 50d70288d0 Preserve wires with keep attribute in EDIF back-end 
Signed-off-by: Claire Wolf <clifford@clifford.at>
 2020-01-29 14:07:11 +01:00
Eddie Hung 48f3f5213e
Merge pull request #1619 from YosysHQ/eddie/abc9_refactor 
Refactor `abc9` pass
 2020-01-27 13:29:15 -08:00
Eddie Hung f2576c096c Merge branch 'eddie/abc9_refactor' into eddie/abc9_required 2020-01-27 12:29:28 -08: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
Eddie Hung 3d9737c1bd Merge remote-tracking branch 'origin/master' into eddie/abc9_refactor 2020-01-21 16:27:40 -08:00
Eddie Hung cd8f55a911 write_xaiger: fix for (* keep *) on flop output 2020-01-21 09:43:04 -08:00
Claire Wolf 30642e9570
Merge pull request #1629 from YosysHQ/mwk/edif-z 
edif: Just ignore connections to 'z
 2020-01-21 18:35:15 +01:00
Eddie Hung 38aa248385 Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required 2020-01-15 11:26:11 -08:00
Eddie Hung d6da9c0c0f write_xaiger: skip abc9_flop only if abc_box_seq present 2020-01-15 11:25:20 -08:00
Eddie Hung 485e08e436 abc9_ops: cope with (* abc9_flop *) in place of (* abc9_box_id *) 2020-01-14 16:33:41 -08:00
Eddie Hung 48984a7605 Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required 2020-01-14 16:32:46 -08:00
Eddie Hung 1c41dc6b95 write_xaiger: do not export flop inputs as POs 2020-01-14 16:17:27 -08:00