mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-26 01:14:37 +00:00
Code Activity
10951 commits 122 branches 59 tags 72 MiB
Commit graph

1241 commits

Author SHA1 Message Date
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
Sahand Kashani
018116e478 Refactor to directly call ILANG_BACKEND::dump_const() + directly lookup src attribute 2020-03-24 10:55:21 +01:00
Teguh Hofstee
b08932cb81 fix typo in write_smt2 help 2020-03-23 02:14:26 -07:00
Sahand Kashani
f48fb26c0f Indentation conventions 2020-03-23 09:01:17 +01:00
Sahand Kashani-Akhavan
566e08485a
Const parameter in function (backends/firrtl/firrtl.cc) 
Co-Authored-By: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>
 2020-03-23 08:56:28 +01:00
Sahand Kashani
21492914a2 Strip quotes around fileinfo strings 
Yosys puts quotes around the string that represents the fileinfo whereas
firrtl does not. So when firrtl sees quotes, it escapes them with an extra
backslash which makes it hard to read afterwards.
 2020-03-21 15:57:53 +01:00
Sahand Kashani
c0b2a9af2e Add fileinfo to firrtl backend for assignments and non-instance cells 2020-03-21 12:54:23 +01:00
Sahand Kashani
3e04e29dec Refactor fileinfo emission characters to single location 2020-03-20 18:31:12 +01:00
Sahand Kashani
ed9f8bfe6e Add fileinfo to firrtl backend for instances 2020-03-19 16:24:18 +01:00
Sahand Kashani
59236314f8 Add fileinfo to firrtl backend for modules and wires 2020-03-19 14:59:05 +01:00
Sahand Kashani
bdce9c28c2 Add fileinfo to firrtl backend for top-level circuit 2020-03-19 00:14:27 +01: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
Eddie Hung
0e4285ca0d abc9_ops: generate flop box ids, add abc9_required to FD* cells 2020-01-14 15:05:49 -08:00
Eddie Hung
588a713b54 Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required 2020-01-14 14:28:07 -08:00