Commit Graph

959 Commits

Author SHA1 Message Date
Sahand Kashani ac388859e3 Remove dependency on ilang backend since we no longer use it 2020-04-08 23:59:22 +02:00
Sahand Kashani 9edf8869c1 Merge branch 'master' of github.com:YosysHQ/yosys into firrtl_backend_fileinfo 2020-04-08 23:50:37 +02:00
Sahand Kashani 820e3d1dad Remove unnecessary pruning of double-quoting
In the past I was calling the ILANG_BACKEND::dump_const() to dump
values to an output stream. When these values were strings, the
function used to add quotes around them. The firrtl compiler, in turn,
escaped these quotes and the result was double-quoted strings which
were hard to read.

However I'm now calling design_entity->get_src_attribute() directly
and there is no additional quote being put around it, so we can
safely remove the unnecessary call to str.erase() here.
2020-04-08 23:20:56 +02:00
Eddie Hung 956ecd48f7 kernel: big fat patch to use more ID::*, otherwise ID(*) 2020-04-02 09:51:32 -07:00
Eddie Hung dde3dfd72e Update backends/btor/btor.cc; credit @boqwxp
Co-Authored-By: Alberto Gonzalez <61295559+boqwxp@users.noreply.github.com>
2020-04-02 07:14:08 -07:00
Eddie Hung fdafb74eb7 kernel: use more ID::* 2020-04-02 07:14:08 -07:00
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
Sahand Kashani 6c2b220af5 Remove use of auto for simple types + simplify src attribute computation 2020-03-24 21:07:08 +01: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
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