riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
14,488 Commits 92 Branches 49 Tags 39 MiB
Commit Graph

1607 Commits

Author SHA1 Message Date
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 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
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
Eddie Hung 4656f202c6 abc9_ops: -reintegrate to not trim box padding anymore 2020-01-14 14:27:29 -08:00
Eddie Hung aaafd784a5 write_xaiger: skip if no arrival times 2020-01-14 13:05:39 -08:00
Eddie Hung 915e7dde73 Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required 2020-01-14 12:57:56 -08:00
Eddie Hung 654247abe9 abc9_ops/write_xaiger: update doc 2020-01-14 12:40:36 -08:00
Eddie Hung 468386d67d abc9_ops: -prep_holes -> -prep_xaiger, move padding to write_xaiger 2020-01-14 12:25:45 -08:00
Eddie Hung 53a99ade9c Merge remote-tracking branch 'origin/master' into eddie/abc9_refactor 2020-01-14 11:46:56 -08:00
Miodrag Milanović 9fbeb57bbd
Merge pull request #1623 from YosysHQ/mmicko/edif_attr 
Export wire properties in EDIF
 2020-01-14 19:19:32 +01:00
Eddie Hung eb7dd7d374 write_xaiger: fix case of PI and CI and (* keep *) 2020-01-13 23:23:21 -08:00
Eddie Hung 2c65e1abac abc9: break SCC by setting (* keep *) on output wires 2020-01-13 21:45:27 -08:00
Eddie Hung a6d4ea7463 abc9: respect (* keep *) on cells 2020-01-13 19:21:11 -08:00
Eddie Hung 9ec948f396 write_xaiger: add support and test for (* keep *) on wires 2020-01-13 19:07:55 -08:00
Eddie Hung 0d2c06ee47 write_xaiger: cache arrival times 2020-01-13 09:50:50 -08:00
Marcin Kościelnicki 55f86eda36 edif: Just ignore connections to 'z 
Connecting a const 'z to a net should be equivalent to not connecting it
at all, so let's just ignore such connections on output.
 2020-01-13 14:49:31 +01:00
Eddie Hung f9aae90e7a Merge remote-tracking branch 'origin/eddie/abc9_refactor' into eddie/abc9_required 2020-01-12 15:19:41 -08:00
Eddie Hung 295e241c07 cleanup 2020-01-11 17:28:24 -08:00
Eddie Hung 79db12f238 Merge remote-tracking branch 'origin/master' into eddie/abc9_refactor 2020-01-11 17:26:25 -08:00
Eddie Hung 58ab9f6021 write_xaiger: create holes_sigmap before modifications 2020-01-11 17:25:32 -08:00
Eddie Hung 1ccee4b95e write_xaiger: sort holes by offset as well as port_id 2020-01-11 11:49:57 -08:00
Eddie Hung f24de88f38 log_debug() for abc9_{arrival,required} times 2020-01-10 17:13:27 -08:00
Miodrag Milanovic 6888799c75 remove whitespace 2020-01-10 12:38:03 +01:00
Miodrag Milanovic 2bcd55f1ae Export wire properties as well in EDIF 2020-01-10 12:33:58 +01:00
Eddie Hung ceabd5bc39 write_xaiger: cleanup 2020-01-09 14:03:43 -08:00
Eddie Hung 3177437224 write_xaiger: cope with abc9_arrival as string of ints 2020-01-09 10:05:03 -08:00
Eddie Hung 7532416cd7 write_xaiger: cleanup holes generation 2020-01-08 18:27:09 -08:00
Eddie Hung 5f7349f26d write_xaiger: holes PIs only if whitebox 2020-01-08 15:40:37 -08:00
Eddie Hung 8d0cc654a4 Stray log_module 2020-01-06 15:14:38 -08:00
Eddie Hung aa58472a29 Revert "write_xaiger to pad, not abc9_ops -prep_holes" 
This reverts commit b5f60e055d.
 2020-01-06 13:34:45 -08:00
Eddie Hung 921ff0f5e3 Merge remote-tracking branch 'origin/xaig_dff' into eddie/abc9_refactor 2020-01-06 12:04:08 -08:00
Eddie Hung 886c5c5883 write_xaiger: make more robust, update doc 2020-01-06 10:23:04 -08:00
Eddie Hung 19ec54f956 write_aiger: make more robust 2020-01-06 10:18:59 -08:00
Eddie Hung b5f60e055d write_xaiger to pad, not abc9_ops -prep_holes 2020-01-05 10:20:24 -08:00
Eddie Hung 6556a1347a Fix when -dff not given 2020-01-04 09:17:01 -08:00
Eddie Hung 930f03e883 Call -prep_holes before aigmap; fix topo ordering 2020-01-03 15:38:18 -08:00
Eddie Hung a819656972 WIP 2020-01-03 14:59:55 -08:00
Eddie Hung 559f3379e8 Preserve topo ordering from -prep_holes to write_xaiger 2020-01-03 14:37:58 -08:00
Eddie Hung bb70915fb8 WIP 2020-01-03 13:21:56 -08:00
Eddie Hung e1f494ab1d WIP 2020-01-03 13:08:52 -08:00
Eddie Hung e62eb02c1d Restore write_xaiger's holes_mode since port_id order causes QoR 
regressions inside abc9
 2020-01-03 12:32:05 -08:00
Eddie Hung dedea5a58d Cleanup 2020-01-02 17:25:14 -08:00
Eddie Hung c28bea0382 Merge remote-tracking branch 'origin/xaig_dff' into eddie/abc9_refactor 2020-01-02 15:57:35 -08:00
Eddie Hung 07feedfa73 write_xaiger: get rid of external_bits dict 2020-01-02 15:32:58 -08:00
Eddie Hung 8e507bd807 abc9 -keepff -> -dff; refactor dff operations 2020-01-02 12:36:54 -08:00
Eddie Hung 11577b46fc Get rid of (* abc9_keep *) in write_xaiger too 2020-01-01 08:38:23 -08:00
Eddie Hung ac808c5e2a attributes.count() -> get_bool_attribute() 2020-01-01 08:33:32 -08:00
Eddie Hung 96db05aaef parse_xaiger to not take box_lookup 2019-12-31 17:06:03 -08:00
Eddie Hung cac7f5d82e Do not re-order carry chain ports, just precompute iteration order 2019-12-31 16:12:40 -08:00
Eddie Hung 134e70e8e7 write_xaiger: be more precise with ff_bits, remove ff_aig_map 2019-12-31 10:21:11 -08:00
Eddie Hung 3798fa3bea Retry getting rid of write_xaiger's holes_mode 2019-12-31 09:59:17 -08:00
Eddie Hung 436c96e2fb Revert "Get rid of holes_mode" 
This reverts commit 7997e2a90f.
 2019-12-30 23:29:14 -08:00
Eddie Hung 7997e2a90f Get rid of holes_mode 2019-12-30 20:15:09 -08:00
Eddie Hung b42b64e8ed Move Pass::call() out of abc9_ops into abc9 2019-12-30 19:23:54 -08:00
Eddie Hung 88334cab89 Cleanup 2019-12-30 18:49:33 -08:00
Eddie Hung 65baefecd3 Rid unnecessary if 2019-12-30 18:26:35 -08:00
Eddie Hung e2bbe33a88 Get rid of holes_mode 2019-12-30 18:24:29 -08:00
Eddie Hung b50de28c04 Add abc9_ops -prep_holes 2019-12-30 18:00:49 -08:00
Eddie Hung 0735572934 write_xaiger to use scratchpad for stats; cleanup abc9 2019-12-30 15:35:33 -08:00
Eddie Hung d1fccd5a2d Remove unused 2019-12-30 14:35:52 -08:00
Eddie Hung 3cbbae251f Call "proc" if processes inside whiteboxes 2019-12-30 14:33:05 -08:00
Eddie Hung 405e974fe5 Merge remote-tracking branch 'origin/master' into xaig_dff 2019-12-30 14:31:42 -08:00
Eddie Hung d7ada66497 Add "synth_xilinx -dff" option, cleanup abc9 2019-12-30 14:13:16 -08:00
Eddie Hung 237415e78c write_xaiger: inherit port ordering from original module 2019-12-27 16:44:18 -08:00
Eddie Hung a56d6970f2 Revert "Merge pull request #1598 from YosysHQ/revert-1588-eddie/xaiger_cleanup" 
This reverts commit 92654f73ea, reversing
changes made to 3e14ff1667.
 2019-12-27 16:05:58 -08:00
Eddie Hung 9e6632c40a Merge branch 'master' of github.com:YosysHQ/yosys 2019-12-27 15:37:26 -08:00
Eddie Hung 3d4644804e write_xaiger: simplify c{i,o}_bits 2019-12-27 15:37:17 -08:00
David Shah df31ade3b3
Revert "write_xaiger: only instantiate each whitebox cell type once" 2019-12-27 23:25:20 +00:00
Eddie Hung dd503a5f3f Really fix it! 2019-12-27 15:18:55 -08:00
Eddie Hung 49881b4468 write_xaiger: fix arrival times for non boxes 2019-12-27 11:30:18 -08:00
Eddie Hung 6eadd4390a write_xaiger to opt instead of just clean whiteboxes 2019-12-23 08:35:53 -08:00
Eddie Hung a75e08c709 write_xaiger: only instantiate each whitebox cell type once 2019-12-20 13:07:24 -08:00
Eddie Hung 10e82e103f
Revert "Optimise write_xaiger" 2019-12-20 12:05:45 -08:00
Eddie Hung 5f50e4f112 Cleanup xaiger, remove unnecessary complexity with inout 2019-12-17 15:45:26 -08:00
Eddie Hung e82a9bc642 Do not sigmap 2019-12-17 00:03:03 -08:00
Eddie Hung 2e71130700 Revert "Use sigmap signal" 
This reverts commit 42f990f3a6.
 2019-12-17 00:00:07 -08:00
Eddie Hung 42f990f3a6 Use sigmap signal 2019-12-16 16:49:42 -08:00
Eddie Hung b19fc8839b Skip $inout transformation if not a PI 2019-12-16 14:39:13 -08:00
Eddie Hung 78c0246d4a Revert "write_xaiger: use sigmap bits more consistently" 
This reverts commit 6c340112fe.
 2019-12-16 14:35:35 -08:00
Eddie Hung 6c340112fe write_xaiger: use sigmap bits more consistently 2019-12-16 10:21:57 -08:00
Eddie Hung 91467938c4 Stray newline 2019-12-06 17:08:19 -08:00
Eddie Hung f2ac36de4a write_xaiger to inst each cell type once, do not call techmap/aigmap 2019-12-06 17:06:10 -08:00
Eddie Hung 1f96de04c9 Fix writing non-whole modules, including inouts and keeps 2019-12-06 16:19:10 -08:00
Eddie Hung a682a3cf93 write_xaiger to support part-selected modules again 2019-12-05 17:54:43 -08:00
Eddie Hung c6ee2fb482 Cleanup 2019-12-03 19:21:47 -08:00
Eddie Hung df52bc80d8 write_xaiger to consume abc9_init attribute for abc9_flops 2019-12-03 18:47:44 -08:00
Eddie Hung 419ca5c207 Revert "Fold loop" 
This reverts commit a30d5e1cc3.
 2019-11-27 21:55:56 -08:00
Eddie Hung 449b1d2c6f Add comment, use sigmap 2019-11-27 13:20:12 -08:00
Eddie Hung 403214f44d Revert "Fold loop" 
This reverts commit da51492dbc.
 2019-11-27 12:35:25 -08:00
Eddie Hung 5e67df38ed latch -> box 2019-11-26 22:59:05 -08:00
Eddie Hung a30d5e1cc3 Fold loop 2019-11-26 21:57:50 -08:00
Eddie Hung 68717dd03b Do not sigmap keep bits inside write_xaiger 2019-11-26 21:57:50 -08:00
Eddie Hung 7136cee6b4 xaiger: do not promote output wires 2019-11-26 21:55:37 -08:00
Eddie Hung 99702efaba xaiger: do not promote output wires 2019-11-26 19:03:02 -08:00
Eddie Hung da51492dbc Fold loop 2019-11-25 15:43:37 -08:00
Eddie Hung 7f0914a408 Do not sigmap keep bits inside write_xaiger 2019-11-25 15:42:07 -08:00
Eddie Hung 81548d1ef9 write_xaiger back to working with whole modules only 2019-11-22 16:52:17 -08:00
Eddie Hung 8ef241c6f4 Revert "write_xaiger to not use module POs but only write outputs if driven" 
This reverts commit 0ab1e496dc.
 2019-11-22 13:24:28 -08:00
Eddie Hung 0ab1e496dc write_xaiger to not use module POs but only write outputs if driven 2019-11-21 16:19:28 -08:00
Eddie Hung 929beda19c abc9 to support async flops $_DFF_[NP][NP][01]_ 2019-11-19 16:57:26 -08:00
Eddie Hung 09ee96e8c2 Merge remote-tracking branch 'origin/master' into xaig_dff 2019-11-19 15:40:39 -08:00
whitequark 3c643c57df write_verilog: add -extmem option, to write split memory init files. 
Some toolchains (in particular Quartus) are pathologically slow if
a large amount of assignments in `initial` blocks are used.
 2019-11-18 01:27:21 +00:00
Clifford Wolf cd44826d50 Use cell name for btor bad state props when it is a public name 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-11-14 11:57:38 +01:00
Makai Mann d88cc139a0 Add an info string symbol for bad states in btor backend 2019-11-11 16:40:51 -08:00
Clifford Wolf 5110a34dd7 Fix write_aiger bug added in 524af21 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-11-04 14:25:13 +01:00
Clifford Wolf 81876a3734
Merge pull request #1393 from whitequark/write_verilog-avoid-init 
write_verilog: do not print (*init*) attributes on regs
 2019-10-27 10:25:01 +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
Eddie Hung b2e34f932a Rename $currQ to $abc9_currQ 2019-10-07 15:31:43 -07:00
Eddie Hung 90a954bb9c Get rid of latch_* in write_xaiger 2019-10-07 13:09:13 -07:00
Eddie Hung 1504ca2cd9 Remove "write_xaiger -zinit" 2019-10-07 11:58:49 -07:00
Eddie Hung e1554b56dd Add comment on default flop init 2019-10-07 11:56:17 -07:00
Eddie Hung d9fba95177 Get rid of output_port lookup 2019-10-07 11:49:06 -07:00
Eddie Hung 3879ca1398 Do not require changes to cells_sim.v; try and work out comb model 2019-10-05 22:55:18 -07:00
Eddie Hung 3c6e5d82a6 Error if $currQ not found 2019-10-05 09:06:13 -07:00
Eddie Hung 7959e9d6b2 Fix merge issues 2019-10-04 17:21:14 -07:00
Eddie Hung 7a45cd5856 Merge remote-tracking branch 'origin/eddie/abc_to_abc9' into xaig_dff 2019-10-04 16:58:55 -07:00
Eddie Hung aae2b9fd9c Rename abc_* names/attributes to more precisely be abc9_* 2019-10-04 11:04:10 -07:00
Eddie Hung 549d6ea467 Merge remote-tracking branch 'origin/master' into xaig_dff 2019-10-03 10:55:23 -07: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
Clifford Wolf a84a2d74c7 Fix btor back-end to use "state" instead of "input" for undef init bits 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-10-02 12:48:04 +02:00
Eddie Hung 1b96d29174 No need to punch ports at all 2019-09-30 17:02:20 -07:00
Eddie Hung e529872b01 Remove need for $currQ port connection 2019-09-30 16:33:40 -07:00
Eddie Hung eecfdda614 Cleanup 2019-09-30 15:24:03 -07:00
Eddie Hung 74678227c7 Use a cell_cache to instantiate once rather than opt_merge call 2019-09-30 13:21:07 -07:00
Eddie Hung a6994c5f16 scc call on active module module only, plus cleanup 2019-09-30 12:57:19 -07:00
Eddie Hung bd8356799a Use derived module 2019-09-30 12:34:28 -07:00
Eddie Hung 1123c09588 Merge remote-tracking branch 'origin/master' into xaig_dff 2019-09-29 19:39:12 -07:00
Eddie Hung 8474c5b366
Merge pull request #1359 from YosysHQ/xc7dsp 
DSP inference for Xilinx (improved for ice40, initial support for ecp5)
 2019-09-29 11:26:22 -07:00
Eddie Hung f3e150d9a5 Merge remote-tracking branch 'origin/master' into xaig_dff 2019-09-29 09:21:51 -07:00
Miodrag Milanović ce0631c371
Merge pull request #1413 from YosysHQ/mmicko/backend_binary_out 
Support binary files for backends, fixes #1407
 2019-09-29 10:37:34 +02:00
Eddie Hung 79b6edb639 Big rework; flop info now mostly in cells_sim.v 2019-09-28 23:48:17 -07:00
Miodrag Milanovic 0c380f0855 Add aiger and protobuf backends binary support 2019-09-28 09:51:48 +02:00
Miodrag Milanovic d0493925ec Support binary files for backends, fixes #1407 2019-09-28 09:36:18 +02:00
Eddie Hung cfa6dd61ef Use abc_mergeability attr for "r" extension 2019-09-27 18:41:43 -07:00
Eddie Hung dc154c39a8 Fix infinite recursion 2019-09-27 17:45:49 -07:00
Eddie Hung 8f5710c464 Merge remote-tracking branch 'origin/master' into xaig_dff 2019-09-27 15:14:31 -07:00
Aman Goel 5eebfabe42 Corrects btor2 backend 2019-09-27 12:40:17 -04:00
Eddie Hung 44374b1b2b "abc_padding" attr for blackbox outputs that were padded, remove them later 2019-09-23 21:58:40 -07:00
Eddie Hung c340fbfab2 Force $inout.out ports to begin with '$' to indicate internal 2019-09-23 21:58:04 -07:00
whitequark 4f426c2ac4 write_verilog: do not print (*init*) attributes on regs. 
If an init value is emitted for a reg, an (*init*) attribute is never
necessary, since it is exactly equivalent. On the other hand, some
tools that consume Verilog (ISE, Vivado, Quartus) complain about
(*init*) attributes because their interpretation differs from Yosys.

All (*init*) attributes that would not become reg init values anyway
are emitted as before.
 2019-09-22 16:52:06 +00:00
Eddie Hung 2d9484c12c When two boxes connect to each other, need not be a (* keep *) 2019-09-19 15:40:28 -07:00
Clifford Wolf 779ce3537f Add "write_aiger -L" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-09-18 13:33:02 +02:00
Clifford Wolf b88d2e5f30 Fix stupid bug in btor back-end 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-09-18 11:56:14 +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 e9bb252e77 Recognise built-in types (e.g. $_DFF_*) 2019-08-30 20:15:09 -07:00
Eddie Hung 3247442bf9 Revert "Revert "Fix omode which inserts an output if none exists (otherwise abc9 breaks)"" 
This reverts commit 8f0c1232d7.
 2019-08-28 17:34:00 -07:00
Eddie Hung 082a01954b Revert "Output "h" extension only if boxes" 
This reverts commit 399ac760ff.
 2019-08-28 17:30:54 -07:00
Eddie Hung 399ac760ff Output "h" extension only if boxes 2019-08-21 11:31:18 -07:00
Eddie Hung 8f0c1232d7 Revert "Fix omode which inserts an output if none exists (otherwise abc9 breaks)" 
This reverts commit 8182cb9d91.
 2019-08-21 11:29:40 -07:00
Eddie Hung 8182cb9d91 Fix omode which inserts an output if none exists (otherwise abc9 breaks) 2019-08-20 21:30:16 -07:00
Eddie Hung 4d123b7638 Revert "Only xaig if GetSize(output_bits) > 0" 
This reverts commit 7b646101e9.
 2019-08-20 21:22:38 -07:00
Eddie Hung 7b646101e9 Only xaig if GetSize(output_bits) > 0 2019-08-20 20:57:13 -07:00
Eddie Hung f1a206ba03 Revert "Remove sequential extension" 
This reverts commit 091bf4a18b.
 2019-08-20 18:17:14 -07:00
Eddie Hung 091bf4a18b Remove sequential extension 2019-08-20 18:16:37 -07:00
Eddie Hung 1b5d2de1d4 Do not sigmap! 2019-08-20 15:23:26 -07:00
Eddie Hung c00d72cdb3 Minor refactor 2019-08-20 14:47:58 -07:00
Eddie Hung 45d4b33f0c Output i/o/h extensions even if no boxes or flops 2019-08-19 13:17:31 -07:00
Eddie Hung 91687d3fea Add (* abc_arrival *) attribute 2019-08-19 12:33:24 -07:00
Eddie Hung 2f4e0a5388 Merge remote-tracking branch 'origin/master' into xaig_dff 2019-08-19 10:07:27 -07:00
Eddie Hung 10c69f71e9 Use %d 2019-08-19 09:16:20 -07:00
Eddie Hung 24c934f1af Merge branch 'eddie/abc9_refactor' into xaig_dff 2019-08-16 16:51:22 -07:00
Eddie Hung 4fe307f1bc Compute abc_scc_break and move CI/CO outside of each abc9 2019-08-16 15:41:17 -07:00
Clifford Wolf 0c5db07cd6 Fix various NDEBUG compiler warnings, closes #1255 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-08-13 13:29:03 +02:00
Clifford Wolf f54bf1631f
Merge pull request #1258 from YosysHQ/eddie/cleanup 
Cleanup a few barnacles across codebase
 2019-08-10 09:52:14 +02:00
Clifford Wolf 05c46a31dc
Merge pull request #1263 from ucb-bar/firrtl_err_on_unsupported_cell 
FIRRTL error on unsupported cell
 2019-08-10 09:47:10 +02:00
Eddie Hung 6d77236f38 substr() -> compare() 2019-08-07 12:20:08 -07:00
Eddie Hung 7164996921 RTLIL::S{0,1} -> State::S{0,1} 2019-08-07 11:12:38 -07:00
Eddie Hung e6d5147214 Merge remote-tracking branch 'origin/master' into eddie/cleanup 2019-08-07 11:11:50 -07:00
Jim Lawson 5e8a98c8fd Merge branch 'master' into firrtl_err_on_unsupported_cell 
# Conflicts:
#	backends/firrtl/firrtl.cc
 2019-08-07 10:14:45 -07:00
Eddie Hung 3090da2d98 Run "clean -purge" on holes_module in its own design 2019-08-07 09:54:27 -07:00
Clifford Wolf 48f7682e32
Merge pull request #1240 from ucb-bar/firrtl-properties+pow+xnor 
Support explicit FIRRTL properties for better accommodation of FIRRTL/Verilog semantic differences.
 2019-08-07 12:31:32 +02:00
David Shah dee8f61781
Merge pull request #1241 from YosysHQ/clifford/jsonfix 
Improved JSON attr/param encoding
 2019-08-07 10:40:38 +01:00
Eddie Hung e38f40af5b Use IdString::begins_with() 2019-08-06 16:42:25 -07:00
Eddie Hung a6bc9265fb RTLIL::S{0,1} -> State::S{0,1} 2019-08-06 16:23:37 -07:00
Eddie Hung 046e1a5214 Use State::S{0,1} 2019-08-06 16:22:47 -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
Clifford Wolf 0917a5cf72
Merge pull request #1238 from mmicko/vsbuild_fix 
Visual Studio build fix
 2019-08-02 17:07:39 +02:00
Miodrag Milanovic 28b7053a01 Fix formatting for msys2 mingw build using GetSize 2019-08-01 17:27:34 +02:00
Clifford Wolf 15fae357f6 Implement improved JSON attr/param encoding 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-08-01 12:34:52 +02:00
Jim Lawson 3b8c917025 Support explicit FIRRTL properties for better accommodation of FIRRTL/Verilog semantic differences. 
Use FIRRTL spec vlaues for definition of FIRRTL widths.
Added support for '$pos`, `$pow` and `$xnor` cells.
Enable tests/simple/operators.v since all operators tested there are now supported.
Disable FIRRTL tests of tests/simple/{defvalue.sv,implicit_ports.v,wandwor.v} since they currently generate FIRRTL compilation errors.
 2019-07-31 09:27:38 -07:00
Miodrag Milanovic 35d28de478 Visual Studio build fix 2019-07-31 09:10:24 +02:00
Jim Lawson 7e298084e4 Call log_error() instead of log_warning() on unsupported cell type in FIRRTL backend. 2019-07-24 13:33:16 -07:00
Clifford Wolf 927f0caa9d
Merge pull request #1203 from whitequark/write_verilog-zero-width-values 
write_verilog: dump zero width constants correctly
 2019-07-18 15:31:27 +02:00
Clifford Wolf 56c00e871f Remove old $pmux_safe code from write_verilog 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-07-17 11:49:04 +02:00
whitequark 4ff44d85a5 write_verilog: dump zero width constants correctly. 
Before this commit, zero width constants were dumped as "" (empty
string). Unfortunately, 1364-2005 5.2.3.3 indicates that an empty
string is equivalent to "\0", and is 8 bits wide, so that's wrong.

After this commit, a replication operation with a count of zero is
used instead, which is explicitly permitted per 1364-2005 5.1.14,
and is defined to have size zero. (Its operand has to have a non-zero
size for it to be legal, though.)

Fixes #948 (again).
 2019-07-16 21:00:09 +00:00
N. Engelhardt ab4b9e8db4 smt: handle failure of setrlimit syscall 2019-07-15 23:33:18 +08:00
Clifford Wolf 9112850800
Merge pull request #1172 from whitequark/write_verilog-Sa-as-qmark 
write_verilog: write RTLIL::Sa aka - as Verilog ?
 2019-07-11 07:25:52 +02:00
Eddie Hung 375fcbe511 abc_flop to also get topologically sorted 2019-07-10 20:26:09 -07:00
Eddie Hung ea6ffea2cd Fix clk_pol for FD*_1 2019-07-10 20:10:20 -07:00
Eddie Hung e603d719d6 Fix spacing 2019-07-10 19:04:22 -07:00
Eddie Hung 4a995c5d80 Change how to specify flops to ABC again 2019-07-10 17:54:56 -07:00
Eddie Hung a092c48f03 Use split_tokens() 2019-07-10 17:34:51 -07:00
Eddie Hung 052060f109 Merge remote-tracking branch 'origin/master' into xaig_dff 2019-07-10 16:05:41 -07:00
Clifford Wolf 6dd33be7ce
Merge pull request #1175 from whitequark/write_verilog-fix-case-attr-position 
write_verilog: fix placement of case attributes
 2019-07-09 22:51:25 +02:00
whitequark 37bb6b5e96 write_verilog: fix placement of case attributes. NFC. 2019-07-09 19:14:03 +00:00
whitequark 6a29e1f5b7 write_verilog: write RTLIL::Sa aka - as Verilog ?. 
Currently, the only ways (determined by grepping for regex \bSa\b) to
end up with RTLIL::Sa in a netlist is by reading a Verilog constant
with ? in it as a part of case, or by running certain FSM passes.
Both of these cases should be round-tripped back to ? in Verilog.
 2019-07-09 18:35:49 +00:00
Eddie Hung 00d8a9dce2
Merge pull request #1170 from YosysHQ/eddie/fix_double_underscore 
Rename __builtin_bswap32 -> bswap32
 2019-07-09 10:22:57 -07:00
Eddie Hung 5a0f2e43c7 Rename __builtin_bswap32 -> bswap32 2019-07-09 09:35:09 -07:00
whitequark 628437b01c verilog_backend: dump attributes on SwitchRule. 
This appears to be an omission.
 2019-07-08 15:11:29 +00:00
whitequark 55c1f40277 verilog_backend: dump attributes on CaseRule, as comments. 
Attributes are not permitted in that position by Verilog grammar.
 2019-07-08 12:48:50 +00:00
whitequark 93bc5affd3 Allow attributes on individual switch cases in RTLIL. 
The parser changes are slightly awkward. Consider the following IL:

    process $0
      <point 1>
      switch \foo
        <point 2>
        case 1'1
          assign \bar \baz
          <point 3>
          ...
        case
      end
    end

Before this commit, attributes are valid in <point 1>, and <point 3>
iff it is immediately followed by a `switch`. (They are essentially
attached to the switch.) But, after this commit, and because switch
cases do not have an ending delimiter, <point 3> becomes ambiguous:
the attribute could attach to either the following `case`, or to
the following `switch`. This isn't expressible in LALR(1) and results
in a reduce/reduce conflict.

To address this, attributes inside processes are now valid anywhere
inside the process: in <point 1> and <point 3> a part of case body,
and in <point 2> as a separate rule. As a consequence, attributes
can now precede `assign`s, which is made illegal in the same way it
is illegal to attach attributes to `connect`.

Attributes are tracked separately from the parser state, so this
does not affect collection of attributes at all, other than allowing
them on `case`s. The grammar change serves purely to allow attributes
in more syntactic places.
 2019-07-08 11:34:58 +00:00
Eddie Hung 10524064e9 write_xaiger to treat unknown cell connections as keep-s 2019-07-02 19:14:30 -07:00
Eddie Hung 69f4c039ce Safe side: all flops have different mergeability class 2019-07-02 12:21:03 -07:00
Eddie Hung a31e17182d Refactor and cope with new abc_flop format 2019-07-01 11:50:34 -07:00
Eddie Hung 699d8e3939 Merge remote-tracking branch 'origin/master' into xaig_dff 2019-07-01 10:44:42 -07:00
Eddie Hung 38d8806bd7 Add generic __builtin_bswap32 function 2019-06-28 09:59:47 -07:00
Eddie Hung 524af21317 Also fix write_aiger for UB 2019-06-28 09:55:07 -07:00
Eddie Hung 36e2eb06bb Fix more potential for undefined behaviour due to container invalidation 2019-06-28 09:51:43 -07:00
Eddie Hung 9398921af1 Refactor for one "abc_carry" attribute on module 2019-06-27 16:07:14 -07:00
Eddie Hung 6c256b8cda Merge origin/master 2019-06-27 11:20:15 -07:00
Eddie Hung 080a5ca536 Improve debugging message for comb loops 2019-06-26 20:02:38 -07:00
Eddie Hung cec2292b0b Merge remote-tracking branch 'origin/master' into xaig 2019-06-24 20:01:43 -07:00
Eddie Hung 7903ebe3e0 Carry in/out box ordering now move to end, not swap with end 2019-06-22 14:18:42 -07:00
Eddie Hung 1abe93e48d Merge remote-tracking branch 'origin/master' into xaig 2019-06-21 17:43:29 -07:00
Eddie Hung fddb027cab Replace assert with error message 2019-06-21 17:18:04 -07:00
Eddie Hung 7074ec9cd5 Add log_push()/log_pop() inside write_xaiger 2019-06-21 17:17:29 -07:00
Eddie Hung 65c1199acd One more workaround for gcc-4.8 2019-06-21 14:36:24 -07:00
Eddie Hung bd7ec673dd No point logging constant bit 2019-06-21 14:31:09 -07:00
Eddie Hung 70c93ea0c4 Move comment 2019-06-21 14:31:09 -07:00
Miodrag Milanovic fde90f7f8e Fix json formatting 2019-06-21 20:01:40 +02:00
Miodrag Milanovic 50e7221077 Add upto and offset to JSON ports 2019-06-21 19:47:25 +02:00
Clifford Wolf f15def325c Added JSON upto and offset 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-06-21 15:22:17 +02:00
Eddie Hung 6a336ca23e Fix spacing 2019-06-20 22:30:20 -07:00
Eddie Hung e21f01d938 Refactor bit2aig for less lookups 2019-06-20 22:10:43 -07:00
Eddie Hung 4422b7311b Fix gcc invalidation behaviour for write_aiger 2019-06-20 22:10:43 -07:00
Eddie Hung 32f8014e12 Fix gcc error, due to dict invalidation during recursion 2019-06-20 22:10:43 -07:00
Eddie Hung c4ea6fff65 Fix gcc invalidation behaviour for write_aiger 2019-06-20 21:56:47 -07:00
Eddie Hung 8e56cfb6bb write_xaiger to flatten 1'bx/1'bz to 1'b0 again 2019-06-20 19:41:27 -07:00
Eddie Hung ad36eb24c0 Fix different abc9 test 2019-06-20 19:41:27 -07:00
Eddie Hung 9faeba7a66 Fix broken abc9.v test due to inout being 1'bx 2019-06-20 19:41:27 -07:00
Eddie Hung e612dade12 Merge remote-tracking branch 'origin/master' into xaig 2019-06-20 19:00:36 -07:00
Eddie Hung 4e5836a5fb Handle COs driven by 1'bx 2019-06-20 17:38:04 -07:00
Eddie Hung f2d541962e write_xaiger to skip POs driven by 1'bx 2019-06-20 17:37:54 -07:00
Ben Widawsky 4a18e19fb8 Support filename rewrite in backends 
Signed-off-by: Ben Widawsky <ben@bwidawsk.net>
 2019-06-18 14:39:52 -07: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
Eddie Hung 0c59bc0b75 Cleanup 2019-06-16 10:42:00 -07:00
Eddie Hung fb90d8c18c Cleanup 2019-06-16 09:34:26 -07:00
Eddie Hung 6852c83bbe Cleanup write_xaiger 2019-06-15 22:50:15 -07:00
Eddie Hung bd2690e9b9 Preserve init of flops, and write into XAIG 2019-06-15 22:41:13 -07:00
Eddie Hung 2309459605 Do not treat $__ABC_FF_ as a user cell 2019-06-15 19:36:55 -07:00
Eddie Hung 0debea25a7 Update comment 2019-06-15 18:24:04 -07:00
Eddie Hung c2f3f116d0 Use $__ABC_FF_ instead of $_FF_ 2019-06-15 18:16:14 -07:00
Eddie Hung 6d74b3e004 Update comment 2019-06-15 09:36:02 -07:00
Eddie Hung 357d36ef4f write_xaiger to treat abc_flop boxes as boxff for ABC 2019-06-15 09:07:03 -07:00
Eddie Hung 7ff8330d1e Leave breadcrumb behind 2019-06-14 13:34:40 -07:00
Eddie Hung 46e69ee934 Remove redundant condition 2019-06-14 13:31:18 -07:00
Eddie Hung 9b55e69755 Revert "Cleanup/optimise toposort in write_xaiger" 
This reverts commit 1948e7c846.

Restores old toposort with optimisations
 2019-06-14 13:29:36 -07:00
Eddie Hung 746f70a9ce Update comment 2019-06-14 13:10:46 -07:00
Eddie Hung 0fa6a441f1 Check that whiteboxes are synthesisable 2019-06-14 13:08:38 -07:00
Eddie Hung 2d85725604 Get rid of compiler warnings 2019-06-14 13:07:56 -07:00
Eddie Hung 7876b5b8be Cover __APPLE__ too for little to big endian 2019-06-14 12:40:51 -07:00
Eddie Hung a48b5bfaa5 Further cleanup based on @daveshah1 2019-06-14 12:25:06 -07:00
Eddie Hung 97d2656375 Resolve comments from @daveshah1 2019-06-14 12:00:02 -07:00
Eddie Hung ee428f73ab Remove WIP ABC9 flop support 2019-06-14 10:37:52 -07:00
Eddie Hung 1656c44373 Cleanup 2019-06-14 10:29:27 -07:00
Eddie Hung 751e640c1d Merge branch 'xaig' of github.com:YosysHQ/yosys into xaig 2019-06-14 10:29:16 -07:00
Eddie Hung 1948e7c846 Cleanup/optimise toposort in write_xaiger 2019-06-14 10:13:17 -07:00
David Shah 9566573054 ecp5: Add abc9 option 
Signed-off-by: David Shah <dave@ds0.me>
 2019-06-14 17:15:02 +01:00
Eddie Hung 8374eb1cb4 Remove unnecessary undriven_bits.insert 2019-06-12 15:55:02 -07:00
Eddie Hung fb2758aade write_xaiger to preserve POs even if driven by constant 2019-06-12 15:44:30 -07:00
Eddie Hung 2e7b3eee40 Add a couple more tests 2019-06-12 15:43:43 -07:00
Eddie Hung 14e870d4c4 More write_xaiger cleanup 2019-06-12 10:00:57 -07:00
Eddie Hung 4be417f6e1 Cleanup write_xaiger 2019-06-12 09:53:14 -07:00
Eddie Hung b21d29598a Consistency 2019-06-12 09:40:51 -07:00
Eddie Hung 7b186740d3 Add log_assert to ensure no loops 2019-06-04 12:01:25 -07:00
Eddie Hung 1b836c93bb Only toposort builtin and abc types 2019-06-04 11:56:58 -07:00
Eddie Hung 257f7ff5f6 When creating new holes cell, inherit parameters too 2019-06-03 12:30:54 -07:00
Eddie Hung 4623177655 ABC9 to understand flops 2019-05-31 15:23:33 -07:00
Eddie Hung eb08e71bd1 Merge branch 'xaig' into xc7mux 2019-05-31 13:03:03 -07:00
Eddie Hung 887c31f33b Fix issue where keep signal became PI, but also box was adding CI driver 2019-05-30 16:03:22 -07:00
Eddie Hung e3c8132d7a Do not re-sort box_module ports 2019-05-30 12:26:51 -07:00
Eddie Hung fdfc18be91 Carry in/out to be the last input/output for chains to be preserved 2019-05-30 01:23:36 -07:00
Eddie Hung 1423384367 Fix abc_test024 2019-05-29 15:24:09 -07:00
Eddie Hung b4321a31bb Fix for abc9_test022 2019-05-28 12:42:17 -07:00
Eddie Hung 13e233217c Small improvement 2019-05-28 11:29:59 -07:00
Eddie Hung 914074a07c Update from master 2019-05-28 09:35:45 -07:00
Eddie Hung 3f60061615 Map file to include boxes not CI/CO 2019-05-27 23:10:59 -07:00
Eddie Hung 234156c01a Instantiate cell type (from sym file) otherwise 'clean' warnings 2019-05-27 12:16:10 -07:00
Eddie Hung 03b289a851 Add 'cinput' and 'coutput' to symbols file for boxes 2019-05-27 11:38:52 -07:00
Eddie Hung 3c8368454f Fix "a" connectivity 2019-05-26 14:14:13 -07:00
Eddie Hung 67f7c64a77 Fix padding, remove CIs from undriven_bits before erasing undriven POs 2019-05-26 11:26:38 -07:00
Eddie Hung 32a4c10c0d Fix "a" extension 2019-05-26 02:44:36 -07:00
Eddie Hung 01684643b6 Fix "write_xaiger", and to write each box contents into holes 2019-05-25 22:34:50 -07:00
Eddie Hung 73c98f2ae2 Merge remote-tracking branch 'origin/master' into xc7mux 2019-05-25 20:50:47 -07:00
Clifford Wolf 6352df42ae Fix handling of offset and upto module ports in write_blif, fixes #1040 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-05-25 17:45:14 +02:00
Clifford Wolf b7dd7c2dcd Add proper error message for btor recursion_guard 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-05-24 16:22:34 +02:00
Eddie Hung 68359bcd6f Merge remote-tracking branch 'origin/eddie/opt_rmdff' into xc7mux 2019-05-23 13:37:53 -07:00
Eddie Hung 0f094fba08 Pad all boxes so that all input/output connections specified 2019-05-21 16:19:23 -07:00
Eddie Hung fb09c6219b Merge remote-tracking branch 'origin/master' into xc7mux 2019-05-21 14:21:00 -07:00
Jim Lawson a5131e2896 Fix static shift operands, neg result type, minor formatting 
Static shift operands must be constants.
The result of FIRRTL's neg operator is signed.
Fix poor indentation for gen_read().
 2019-05-21 13:04:56 -07:00
Clifford Wolf 3870e7cf29
Merge pull request #991 from kristofferkoch/gcc9-warnings 
Fix all warnings that occurred when compiling with gcc9
 2019-05-08 11:25:22 +02:00
Kristoffer Ellersgaard Koch 30c762d3a1 Fix all warnings that occurred when compiling with gcc9 2019-05-08 10:27:14 +02:00
Clifford Wolf 33738c1745 Fix handling of partial init attributes in write_verilog, fixes #997 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-05-07 19:55:36 +02:00
Clifford Wolf 1cd1b5fc1a Add "real" keyword to ilang format 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-05-06 12:00:40 +02:00
Clifford Wolf 87426f5a06 Improve write_verilog specify support 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-05-04 08:46:24 +02:00
Eddie Hung d9c4644e88 Merge remote-tracking branch 'origin/master' into clifford/specify 2019-05-03 15:05:57 -07:00
Eddie Hung 5cd19b52da Merge remote-tracking branch 'origin/master' into xc7mux 2019-05-02 10:44:59 -07:00
Jim Lawson 6ea09caf01 Re-indent firrtl.cc:struct memory - no functional change. 2019-05-01 16:21:13 -07:00
Jim Lawson 38f5424f92 Fix #938 - Crash occurs in case when use write_firrtl command 
Add missing memory initialization.
Sanity-check memory parameters.
Add Cell pointer to memory object (for error reporting).
 2019-05-01 13:16:01 -07:00
Eddie Hung eec314e262 Remove topo sort no-loop assertion, with test 2019-04-24 21:06:53 -07:00
Eddie Hung ac2aff9e28 Fix abc9 with (* keep *) wires 2019-04-23 16:11:39 -07:00
Eddie Hung bfd71e0990 Fix abc9 with (* keep *) wires 2019-04-23 16:11:14 -07:00
Clifford Wolf e807e88b60 Rename T_{RISE,FALL}_AVG to T_{RISE,FALL}_TYP to better match verilog std nomenclature 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-04-23 21:36:59 +02:00
Clifford Wolf 846eb5ea98 Add $specify2/$specify3 support to write_verilog 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-04-23 21:36:59 +02:00
Clifford Wolf 0bf9d0087c Add support for $assert/$assume/$cover to write_verilog 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-04-23 21:36:59 +02:00
Eddie Hung 8f30019b68 Revert "Temporarily remove 'r' extension" 
This reverts commit eaf3c24772.
 2019-04-22 17:41:21 -07:00
Eddie Hung eaf3c24772 Temporarily remove 'r' extension 2019-04-22 11:54:19 -07:00
Eddie Hung b780c0a7de Allow POs to be PIs in XAIG 2019-04-22 11:22:29 -07:00
Eddie Hung 4883391b63 Merge remote-tracking branch 'origin/master' into xaig 2019-04-22 11:19:52 -07:00
Clifford Wolf 0e0c80fac8 Add support for zero-width signals to Verilog back-end, fixes #948 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-04-22 19:44:42 +02:00
Eddie Hung caec7f9d2c Merge remote-tracking branch 'origin/master' into xaig 2019-04-20 12:23:49 -07:00
Clifford Wolf f84a84e3f1
Merge pull request #943 from YosysHQ/clifford/whitebox 
[WIP] Add "whitebox" attribute, add "read_verilog -wb"
 2019-04-20 20:51:54 +02:00
Eddie Hung 76bba49182 Fixes for simple_abc9 tests 2019-04-19 15:47:36 -07:00
Clifford Wolf 148caecca3 Change "ne" to "neq" in btor2 output 
we need to do this because they changed the parser:
e97fc9ceda

Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-04-19 21:17:12 +02:00
Eddie Hung 35f44f3ae8 Do not assume inst_module is always present 2019-04-19 08:44:53 -07:00
Eddie Hung 3544a7cd7b ignore_boxes -> holes_mode 2019-04-19 08:37:10 -07:00
Eddie Hung 8f93999129 Revert "write_json to not write contents (cells/wires) of whiteboxes" 
This reverts commit 4ef03e19a8.
 2019-04-18 23:05:59 -07:00
Eddie Hung 6bdf98d591 Add flop support for write_xaiger 2019-04-18 17:43:13 -07:00
Eddie Hung b531efd6d9 Spelling 2019-04-18 17:35:16 -07:00
Eddie Hung 4c327cf316 Use new -wb flag for ABC flow 2019-04-18 10:32:41 -07:00
Eddie Hung 4ef03e19a8 write_json to not write contents (cells/wires) of whiteboxes 2019-04-18 10:32:00 -07:00
Eddie Hung 79881141e2 write_json to not write contents (cells/wires) of whiteboxes 2019-04-18 10:30:45 -07:00
Eddie Hung 8fe0a961b3 Merge remote-tracking branch 'origin/clifford/whitebox' into xaig 2019-04-18 09:00:06 -07: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
Eddie Hung 23cd2e5de0 Fix $anyseq warning and cleanup 2019-04-17 16:03:29 -07:00
Eddie Hung 1ec5f18346 Cope with inout ports 2019-04-17 14:43:45 -07:00
Eddie Hung 2b860809e9 Stop topological sort at abc_flop_q 2019-04-17 12:28:19 -07:00
Eddie Hung d59185f1d6 Remove init* from xaiger, also topo-sort cells for box flow 2019-04-17 11:08:42 -07:00
Eddie Hung 5c134980c4 Optimise 2019-04-16 21:05:44 -07:00
Eddie Hung e7a8955818 CIs before PIs; also sort each cell's connections before iterating 2019-04-16 16:37:47 -07:00
Eddie Hung 55a3638c71 Port from xc7mux branch 2019-04-16 15:01:45 -07:00
Eddie Hung fe0b421212 Output __const0__ and __const1__ CIs 2019-04-12 18:16:25 -07:00
Eddie Hung 686e772f0b ci_bits and co_bits now a list, order is important for ABC 2019-04-12 16:17:48 -07:00
Eddie Hung c748391730 WIP 2019-04-12 14:13:11 -07:00
Eddie Hung 2217d59e29 Add non-input bits driven by unrecognised cells as ci_bits 2019-04-10 18:06:33 -07:00
Eddie Hung bca3cf6843 Merge branch 'master' into xaig 2019-04-08 16:31:59 -07:00
Jim Lawson 73b87e7807 Refine memory support to deal with general Verilog memory definitions. 2019-04-01 15:02:12 -07:00
Clifford Wolf 1eff8be8f0 Add support for memory initialization to write_btor 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-03-23 14:40:01 +01:00
Clifford Wolf e78f5a3055 Fix BTOR output tags syntax in writye_btor 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-03-23 14:39:42 +01: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
Clifford Wolf 04e920337b Fix a syntax bug in ilang backend related to process case statements 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-03-14 17:50:20 +01:00
Clifford Wolf 53b28b3f01
Merge pull request #869 from cr1901/win-shell 
Install launcher executable when running yosys-smtbmc on Windows.
 2019-03-14 16:43:23 +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 20c6a8c9b0 Improve determinism of IdString DB for similar scripts 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-03-11 20:12:28 +01: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
Jim Lawson d6c4dfb902 Ensure fid() calls make_id() for consistency; tests/simple/dff_init.v fails 
Mark dff_init.v as expected to fail since it uses "initial value".
 2019-03-04 13:37:23 -08:00
Clifford Wolf 03237de686 Fix "write_edif -gndvccy" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-03-01 12:59:07 -08:00
Clifford Wolf 241901461a Add "write_verilog -siminit" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-02-28 15:03:03 -08:00
Larry Doolittle e2fc18f27b Reduce amount of trailing whitespace in code base 2019-02-28 14:58:11 -08:00
Clifford Wolf 6d143c9a01
Merge pull request #827 from ucb-bar/firrtlfixes 
Fix FIRRTL to Verilog process instance subfield assignment.
 2019-02-28 14:45:04 -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
Eddie Hung 8e883d92ed write_xaiger to behave for undriven/unused inouts 2019-02-26 12:17:51 -08:00
Eddie Hung c492a3a1c4 write_xaiger duplicate inout port into out port with $inout.out suffix 2019-02-25 18:39:36 -08:00
Jim Lawson 171c425cf9 Fix FIRRTL to Verilog process instance subfield assignment. 
Don't emit subfield assignments: bits(x, y, z) <= ... - but instead, add them to the reverse-wire-map where they'll be treated at the end of the module.
Enable tests which were disabled due to incorrect treatment of subfields.
Assume the `$firrtl2verilog` variable contains any additional switches to control verilog generation (i.e. `--no-dedup -X mverilog`)
 2019-02-25 16:18:13 -08:00
Eddie Hung 292f80d231 Cleanup abc9 code 2019-02-25 15:20:56 -08:00
Eddie Hung 5180338e80 write_xaiger to write __dummy_o__ for -symbols too 2019-02-21 17:03:18 -08:00
Eddie Hung 085ed9f487 Add attribution 2019-02-21 14:40:13 -08:00
Eddie Hung 2f96a0ed32 write_xaiger to use original bit for co, not sigmap()-ed bit 2019-02-21 11:15:25 -08:00
Eddie Hung 01f8d50ba2 Remove swap file 2019-02-20 16:17:01 -08:00
Eddie Hung f89b112fbf write_aiger: fix CI/CO and symbols 2019-02-20 15:35:32 -08:00
Eddie Hung ef60ca1717 write_xaiger to not write latches, CO/PO fixes 2019-02-20 11:09:13 -08:00
Eddie Hung f9af902532 Merge branch 'master' into xaig 2019-02-19 14:20:04 -08:00
Eddie Hung 11480b4fa3 Instead of INIT param on cells, use initial statement with hier ref as 
per @cliffordwolf
 2019-02-17 12:18:12 -08:00
Eddie Hung 17cd5f759f Merge https://github.com/YosysHQ/yosys into dff_init 2019-02-17 11:49:06 -08:00
Eddie Hung 30f1204721 Cleanup 2019-02-16 22:22:17 -08:00
Eddie Hung 76c35f80f4 Cleanup 2019-02-16 21:09:48 -08:00
Eddie Hung 6a57de9013 write_xaiger to support non-bit cell connections, and cope with COs for -O 2019-02-16 21:00:39 -08:00
Eddie Hung b9a305b85d write_aiger -O to write dummy output as __dummy_o__ 2019-02-16 20:08:59 -08:00
Eddie Hung 0c409e6d8c Tidy up write_xaiger 2019-02-16 08:48:33 -08:00
Eddie Hung 2c1655ae94 write_aiger() to perform CI/CO post-processing and fix symbols 2019-02-16 08:46:25 -08:00
Eddie Hung 486a270415 Fixes needed for DFF circuits 2019-02-15 15:22:18 -08:00
Jim Lawson c245041bfe Removed unused variables, functions. 2019-02-15 12:00:28 -08:00
Eddie Hung 3ac5b65197 write_xaiger to cope with unknown cells by transforming them to CI/CO 2019-02-15 11:51:21 -08:00
Jim Lawson fc1c9aa11f Update cells supported for verilog to FIRRTL conversion. 
Issue warning messages for missing parameterized modules and attempts to set initial values.
Replace simple "if (cell-type)" with "else if" chain.
Fix FIRRTL shift handling.
Add support for parameterized modules, $shift, $shiftx.
Handle default output file.
Deal with no top module.
Automatically run pmuxtree pass.
Allow EXTRA_FLAGS and SEED parameters to be set in the environment for tests/tools/autotest.mk.
Support FIRRTL regression testing in tests/tools/autotest.sh
Add xfirrtl files to test directories to exclude files from FIRRTL regression tests that are known to fail.
 2019-02-15 11:14:17 -08:00
Eddie Hung c69fba8de5 More cleanup 2019-02-14 14:52:47 -08:00
Eddie Hung 7328775584 More cleanup of write_xaiger 2019-02-14 14:48:38 -08:00
Eddie Hung afa4389445 Get rid of formal stuff from xaiger backend 2019-02-14 13:27:26 -08:00
Eddie Hung f0f5d8a5cc Merge remote-tracking branch 'origin/read_aiger' into xaig 2019-02-13 14:09:36 -08:00
Eddie Hung 06cf0555ee Merge https://github.com/YosysHQ/yosys into xaig 2019-02-13 14:08:31 -08:00
Clifford Wolf 1f2548a564
Merge pull request #802 from whitequark/write_verilog_async_mem_ports 
write_verilog: correctly emit asynchronous transparent ports
 2019-02-12 14:41:34 +01:00
Eddie Hung ecd2446132 Add write_xaiger 2019-02-11 15:18:42 -08:00
Eddie Hung db08afe146 Copy backends/aiger/aiger.cc to xaiger.cc 2019-02-08 14:53:12 -08:00
Eddie Hung 20ca795b87 Remove check for cell->name[0] == '$' 2019-02-06 14:53:40 -08:00
Eddie Hung c373640a3a Refactor 2019-02-06 14:28:44 -08:00
Eddie Hung 8241db6960 write_verilog to cope with init attr on q when -noexpr 2019-02-06 14:17:09 -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 da65e1e8d9 write_verilog: correctly emit asynchronous transparent ports. 
This commit fixes two related issues:
  * For asynchronous ports, clock is no longer added to domain list.
    (This would lead to absurd constructs like `always @(posedge 0)`.
  * The logic to distinguish synchronous and asynchronous ports is
    changed to correctly use or avoid clock in all cases.

Before this commit, the following RTLIL snippet (after memory_collect)

    cell $memrd $2
      parameter \MEMID "\\mem"
      parameter \ABITS 2
      parameter \WIDTH 4
      parameter \CLK_ENABLE 0
      parameter \CLK_POLARITY 1
      parameter \TRANSPARENT 1
      connect \CLK 1'0
      connect \EN 1'1
      connect \ADDR \mem_r_addr
      connect \DATA \mem_r_data
    end

would lead to invalid Verilog:

    reg [1:0] _0_;
    always @(posedge 1'h0) begin
      _0_ <= mem_r_addr;
    end
    assign mem_r_data = mem[_0_];

Note that there are two potential pitfalls remaining after this
change:
  * For asynchronous ports, the \EN input and \TRANSPARENT parameter
    are silently ignored. (Per discussion in #760 this is the correct
    behavior.)
  * For synchronous transparent ports, the \EN input is ignored. This
    matches the behavior of the $mem simulation cell. Again, see #760.
 2019-01-29 02:24:00 +00:00
Clifford Wolf 81581f24fc
Merge pull request #800 from whitequark/write_verilog_tribuf 
write_verilog: write $tribuf cell as ternary
 2019-01-27 09:23:41 +01:00
whitequark 3d7925ad9f write_verilog: write $tribuf cell as ternary. 2019-01-27 00:24:06 +00:00
whitequark 42c47a83da write_verilog: escape names that match SystemVerilog keywords. 2019-01-27 00:03:53 +00:00
Clifford Wolf 54dc33b905 Add "write_edif -gndvccy" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-01-17 13:33:11 +01:00
Clifford Wolf 6c5049f016 Fix handling of $shiftx in Verilog back-end 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2019-01-15 10:55:27 +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
Larry Doolittle 99706b3bf4 Squelch a little more trailing whitespace 2018-12-29 12:46:54 +01:00
Clifford Wolf 23bb77867f Minor style fixes 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-18 20:02:39 +01:00
makaimann abf5930a33 Add btor ops for $mul, $div, $mod and $concat 2018-12-17 10:45:17 -08:00
whitequark ca866d384e write_verilog: handle the $shift cell. 
The implementation corresponds to the following Verilog, which is
lifted straight from simlib.v:

    module \\$shift (A, B, Y);

    parameter A_SIGNED = 0;
    parameter B_SIGNED = 0;
    parameter A_WIDTH = 0;
    parameter B_WIDTH = 0;
    parameter Y_WIDTH = 0;

    input [A_WIDTH-1:0] A;
    input [B_WIDTH-1:0] B;
    output [Y_WIDTH-1:0] Y;

    generate
        if (B_SIGNED) begin:BLOCK1
            assign Y = $signed(B) < 0 ? A << -B : A >> B;
        end else begin:BLOCK2
            assign Y = A >> B;
        end
    endgenerate

    endmodule
 2018-12-16 18:46:32 +00:00
Clifford Wolf ddff75b60a
Merge pull request #736 from whitequark/select_assert_list 
select: print selection if a -assert-* flag causes an error
 2018-12-16 16:45:49 +01:00
whitequark fccaa25ec1 write_verilog: add a missing newline. 2018-12-16 15:22:34 +00:00
Clifford Wolf f481ad4d44
Merge pull request #729 from whitequark/write_verilog_initial 
write_verilog: correctly map RTLIL `sync init`
 2018-12-16 15:50:16 +01: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 ed3c57fad3 Fix btor init value handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-08 06:21:31 +01:00
whitequark 7fe770a441 write_verilog: correctly map RTLIL `sync init`. 2018-12-07 18:55:08 +00:00
Clifford Wolf 82aaf6d908 Add "write_aiger -I -O -B" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-11-12 09:27:33 +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
rafaeltp c7770d9eea adding offset info to memories 2018-10-18 16:22:33 -07:00
rafaeltp 609f46eeb7 adding offset info to memories 2018-10-18 16:20:21 -07:00
Clifford Wolf f4ad05e133
Merge pull request #663 from aman-goel/master 
Update to .smv backend
 2018-10-17 12:18:57 +02:00
Aman Goel 749b3ed62a Minor update 2018-10-15 13:54:12 -04:00
Clifford Wolf 115ca57647 Add "write_edif -attrprop" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-10-05 09:41:30 +02:00
Aman Goel 90e0938f9a Update to .smv backend 
Splitting VAR and ASSIGN into IVAR, VAR, DEFINE and ASSIGN. This allows better handling by nuXmv for post-processing (since now only state variables are listed under VAR).
 2018-10-01 19:03:10 -04:00
Miodrag Milanovic 41affeeeb9 added prefix to FDirection constants, fixing windows build 2018-09-21 20:43:49 +02:00
acw1251 efac8a45a6 Fixed typo in "verilog_write" help message 2018-09-18 13:34:30 -04:00
Clifford Wolf 12440fcc8f Add $lut support to Verilog back-end 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-09-06 00:18:01 +02:00
Jim Lawson 380c6f0e97 Remove unused functions. 2018-08-27 10:18:33 -07:00
Jim Lawson 93d19dc2fb Add support for module instances. 
Don't pad logical operands to one bit.
Use operand width and signedness in $reduce_bool.
Shift amounts are unsigned and shouldn't be padded.
Group "is invalid" with the wire declaration, not its use (otherwise it is incorrectly wired to 0).
 2018-08-23 14:35:11 -07: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
Clifford Wolf 1dd156f516 Fix use of signed integers in JSON back-end 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-08-14 23:31:25 +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
Sergiusz Bazanski 1690dafde1 Fix protobuf build 2018-06-20 19:28:43 +01:00
Serge Bazanski 53e9a1549c Add Protobuf backend 
Signed-off-by: Serge Bazanski <q3k@symbioticeda.com>
 2018-06-19 13:34:56 +01:00
Clifford Wolf d9a2b43014 Add $dlatch support to write_verilog 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-04-22 16:03:26 +02:00
Clifford Wolf 5ca91ca019 Add "write_blif -inames -iattr" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-04-15 14:07:21 +02: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
Clifford Wolf 25a864fc73 Fixed -stbv handling in SMT2 back-end 2018-04-04 17:28:07 +02:00
Clifford Wolf dd5fab69c1 Add smtio status msgs when --progress is inactive 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-29 21:59:30 +02:00
Clifford Wolf a48c7e5abf Bugfix in smtio.py VCD file generator 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-29 12:45:31 +02:00
Clifford Wolf 77bd645c35 Add $mem support to SMT2 clock tagging 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-27 02:11:20 +02:00
Clifford Wolf 3f00702475 Improve yosys-smtbmc log output and error handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-17 18:06:17 +01:00
Clifford Wolf 4d4e3a8ca6 Improve handling of invalid check-sat result in smtio.py 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-17 12:17:53 +01:00
Clifford Wolf 3545c0fffb Remove debug prints from yosys-smtbmc VCD writer 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-08 16:24:35 +01:00
Clifford Wolf 8b604004da Check results of (check-sat) in yosys-smtbmc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-07 22:54:19 +01:00
Clifford Wolf cedbc35f4b Imporove yosys-smtbmc error handling, Improve VCD output 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-05 12:17:22 +01:00
Clifford Wolf 8b7602e660 Improve SMT2 encoding of $reduce_{and,or,bool} 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 21:22:20 +01:00
Clifford Wolf 45a6fce92c Fix a hangup in yosys-smtbmc error handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 21:13:30 +01:00
Clifford Wolf ae4e204c76 Improved error handling in yosys-smtbmc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-03 20:00:07 +01:00
Clifford Wolf a44e1edaa3 Terminate running SMT solver when smtbmc is terminated 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-03 14:50:40 +01:00
Clifford Wolf 3ced2cca6e Fix smtbmc smtc/aiw parser for wire names containing [] 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-03 14:15:49 +01:00
Clifford Wolf 90ae426078 Mangle names with square brackets in VCD files to work around issues in gtkwave 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-01 14:15:27 +01:00
Clifford Wolf 675dd5347a Small fixes and improvements in $allconst/$allseq handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-26 11:58:44 +01:00
Clifford Wolf b13e6bd375 Add smtbmc support for exist-forall problems 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-23 19:33:30 +01:00
Clifford Wolf 17583b6a21 Add support for mockup clock signals in yosys-smtbmc vcd output 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-20 17:45:22 +01:00
Clifford Wolf c9672e2e2e Fix handling of zero-length cell connections in SMT2 back-end 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-08 19:12:12 +01:00
Clifford Wolf e4f0218907 Fixed gcc 7.2 "statement will never be executed" warning 2018-02-03 14:31:47 +01:00
Clifford Wolf e97f10b142 Fix smtio.py for large SMT2 S-expressions 2018-01-29 12:34:28 +01:00
Clifford Wolf 54aeca0983 Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output 2018-01-18 14:25:22 +01:00
Clifford Wolf 9804ebedbf Add "no driver for signal bit" error msg to btor back-end 2017-12-24 17:30:36 +01:00
Clifford Wolf 292984896b Simple fix BTOR memory encoding 2017-12-17 18:57:54 +01:00
Clifford Wolf bbdcc1f9d4 Improve BTOR memory encoding 2017-12-17 18:55:17 +01:00
Clifford Wolf 30f23281ed Add array support to btor back-end 2017-12-15 02:19:06 +01:00
Clifford Wolf ad901671c5 Add $anyconst/$anyseq support to btor back-end 2017-12-15 00:40:24 +01:00
Clifford Wolf 162c29bd6b Merge branch 'master' into btor-ng 2017-12-14 03:13:47 +01:00
Clifford Wolf 9419de3e37 Add yosys-smtbmc VCD writer support for memories with async writes 2017-12-14 03:06:00 +01:00
Clifford Wolf a48ec49017 Merge branch 'master' into btor-ng 2017-12-14 02:17:01 +01:00
Clifford Wolf 2625da6440 Add smt2 back-end support for async write memories 2017-12-14 02:07:10 +01:00
Clifford Wolf 546de7fa4f Add "write_btor -s" mode 2017-12-13 00:15:44 +01:00
Clifford Wolf 0881bbf2e7 Add state initval handling to btor back-end 2017-12-12 23:44:08 +01:00
Clifford Wolf f697282246 Add btor back-end support for 'x' constants 2017-12-12 21:48:55 +01:00
Clifford Wolf 82d1fd77de Add btor $shift/$shiftx support 2017-12-11 14:24:19 +01:00
Clifford Wolf cc119b5232 Fix btor back-end shift handling 2017-12-10 08:40:11 +01:00
Clifford Wolf 133a0f4978 Add support for $pmux in btor back-end 2017-12-10 08:11:08 +01:00
Clifford Wolf 83cf736309 Add support for more cell types to btor back-end 2017-12-10 07:16:47 +01:00
Clifford Wolf 63343aeaaa Fix btor concat 2017-12-09 05:58:14 +01:00
Clifford Wolf da91b31bb2 Fixed "yosys-smtbmc -g" handling of no solution 2017-11-27 19:43:36 +01:00
Clifford Wolf b981e5aa69 Fixed "yosys-smtbmc -g" handling of no solution 2017-11-27 17:42:32 +01:00
Clifford Wolf e3a51b3e87 Bugfixes in new BTOR back-end 2017-11-24 18:13:41 +01:00
Clifford Wolf 60d1129506 Progress in new BTOR back-end 2017-11-23 23:44:39 +01:00
Clifford Wolf b3d6b277ea Progress in new BTOR back-end 2017-11-23 18:50:10 +01:00
Clifford Wolf cc2495d48d Progress in new BTOR back-end 2017-11-23 18:14:53 +01:00
Clifford Wolf e41dcaa759 Progress with new BTOR backend 2017-11-23 08:28:29 +01:00
Clifford Wolf 6ee305553a Add skeleton for new BTOR back-end 2017-11-23 06:38:57 +01:00
Clifford Wolf eceacdb9a3 Remove old BTOR back-end 2017-11-23 04:28:51 +01:00
Clifford Wolf 455c1c9d97 Fix SMT2 handling of initstate in sub-modules 2017-10-29 13:21:20 +01:00
Clifford Wolf 1170508264 Improve smtio performance by using reader thread, not writer thread 2017-10-26 01:01:55 +02:00
Clifford Wolf f513494f5f Use separate writer thread for talking to SMT solver to avoid read/write deadlock 2017-10-25 19:59:56 +02:00
Clifford Wolf 76326c163a Improve p_* functions in smtio.py 2017-10-25 15:45:32 +02:00
Clifford Wolf c672c321e3 Capsulate smt-solver read/write in separate functions 2017-10-25 13:37:11 +02:00
Clifford Wolf dd46d76394 Fix a bug in yosys-smtbmc in ROM handling 2017-10-25 13:05:14 +02:00
Clifford Wolf adf1754729 Add $shiftx support to verilog front-end 2017-10-07 13:40:54 +02:00
Clifford Wolf 65f91e5120 Rename "write_verilog -nobasenradix" to "write_verilog -decimal" 2017-10-03 17:31:21 +02:00
dh73 e480847753 Fixed wrong declaration in Verilog backend 2017-10-01 11:11:32 -05:00
dh73 cbaba62401 Adding Cyclone IV (E, GX), Arria 10, Cyclone V and LPM functions (ALTPLL and M9K); M9K is not finished yet. Achronix Speedster also in this commit. Both Arria10 and Speedster-i are still experimental due complexity, but you can experiment around those devices right now 2017-10-01 11:04:17 -05:00
Clifford Wolf c2d737457a Fix bug in write_smt2 (export logic driving hierarchical cells before exporting regs) 2017-08-25 11:44:48 +02:00
Clifford Wolf 48b2b376d0 Add "yosys-smtbmc --smtc-init --smtc-top --noinit" 2017-08-04 17:09:08 +02:00
Clifford Wolf 3a8f6f0f51 Add verilator support to testbenches generated by yosys-smtbmc 2017-07-21 14:33:29 +02:00
Clifford Wolf 10c7709e68 Generate FSM-style testbenches in smtbmc 2017-07-12 15:57:04 +02:00
Clifford Wolf 4a8c131fa7 Fix the fixed handling of x-bits in EDIF back-end 2017-07-11 17:45:29 +02:00
Clifford Wolf 479be3cec7 Fix handling of x-bits in EDIF back-end 2017-07-11 17:38:19 +02:00
Clifford Wolf 9557fd2a36 Add attributes and parameter support to JSON front-end 2017-07-10 13:17:38 +02:00
Clifford Wolf 3c693b6561 Change s/asserts/assertions/ in yosys-smtbmc log messages 2017-07-07 11:52:25 +02:00
Clifford Wolf 8f7404f82c Add "yosys-smtbmc --presat" 2017-07-07 02:47:30 +02:00
Clifford Wolf 5442554e6f Fix generation of multiple outputs for same AIG node in write_aiger 2017-07-05 14:23:54 +02:00
Clifford Wolf 37af6294bd Add write_table command 2017-07-05 12:13:53 +02:00
Clifford Wolf 3e0948e16f Remove unneeded delays in smtbmc vlogtb 2017-07-03 15:37:17 +02:00
Clifford Wolf 287831dca3 Include output ports with constant driver in AIGER output 2017-07-03 14:53:17 +02:00
Clifford Wolf ea805af6f5 Add "yosys-smtbmc --vlogtb-top" 2017-07-01 18:19:23 +02:00
Clifford Wolf 7d2fb6e2fc Fix smtbmc vlogtb bug in $anyseq handling 2017-07-01 02:13:32 +02:00
Clifford Wolf 8f8baccfde Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand const reg" 2017-06-07 12:30:24 +02:00
Clifford Wolf c365e33fd7 Fix AIGER back-end for multiple symbols per input/latch/output/property 2017-05-30 19:09:11 +02:00
Clifford Wolf 9ed4c9d710 Improve write_aiger handling of unconnected nets and constants 2017-05-28 11:31:35 +02:00
Clifford Wolf d9201b85f3 Change default smt2 solver to yices (Yices 2 has switched its license to GPL) 2017-05-27 11:56:01 +02:00
Clifford Wolf 2122ae69b3 Add workaround for CBMC bug to SimpleC back-end 2017-05-17 21:07:54 +02:00
Clifford Wolf 05cdd58c8d Add $_ANDNOT_ and $_ORNOT_ gates 2017-05-17 09:08:29 +02:00
Clifford Wolf 9f4fbc5e74 Add <modname>_init() function generator to simpleC back-end 2017-05-16 19:34:07 +02:00
Clifford Wolf 35be567605 Improve simplec back-end 2017-05-16 08:50:23 +02:00
Clifford Wolf 8d3c706459 Improve simplec back-end 2017-05-15 13:21:59 +02:00
Clifford Wolf 9c397ea78b Improve simplec back-end 2017-05-14 13:14:49 +02:00
Clifford Wolf 628daab277 Improve simplec back-end 2017-05-13 18:47:31 +02:00
Clifford Wolf ef7594ce3d Improve simplec back-end 2017-05-12 22:39:16 +02:00
Clifford Wolf 7931e1ebb4 Added support for more gate types to simplec back-end 2017-05-12 17:42:31 +02:00
Clifford Wolf bd4ed19887 Add first draft of simple C back-end 2017-05-12 14:13:33 +02:00
Clifford Wolf 1a4b7c6bfa Fix boolector support in yosys-smtbmc 2017-05-08 14:33:22 +02:00
Clifford Wolf 106e44f406 Add "write_smt2 -stdt" mode 2017-03-20 12:00:35 +01:00
Clifford Wolf 0ac72e759d Add generation of logic cells to EDIF back-end runtest.py 2017-03-19 14:57:40 +01:00
Clifford Wolf 850f8299a9 Fix EDIF: portRef member 0 is always the MSB bit 2017-03-19 14:53:28 +01:00
Clifford Wolf 1390e9a0a7 Add simple EDIF test case generator and checker 2017-03-18 15:00:03 +01:00
Clifford Wolf c855353986 Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg 2017-03-04 23:41:54 +01:00
Clifford Wolf a6ca28276e Add write_aiger $anyseq support 2017-03-02 16:39:48 +01:00
Clifford Wolf fbd52ec6dd Use hex addresses in smtbmc vcd mem traces 2017-02-28 13:54:50 +01:00
Clifford Wolf 2203562268 Add smtbmc support for memory vcd dumping 2017-02-26 21:26:32 +01:00
Clifford Wolf 80ecd7a26f Fix extra newline bug in write_smt2 2017-02-26 14:41:27 +01:00
Clifford Wolf 6e152f7aa1 Fix bug in smtio unroll code 2017-02-26 14:39:07 +01:00
Clifford Wolf 66a1617b69 Fix assert checking in "yosys-smtbmc -c --append" 2017-02-26 11:06:26 +01:00
Clifford Wolf fd1cc0c73d Improve (and fix for stbv mode) SMT2 memory API 2017-02-26 10:58:34 +01:00
Clifford Wolf 38bf458037 Add support for "yosys-smtbmc -c --append" 2017-02-25 23:41:40 +01:00
Clifford Wolf c7d1286728 Improve "write_edif" help message 2017-02-25 16:35:53 +01:00
Clifford Wolf dfddf391f9 Move EdifNames out of double-private namespace 2017-02-25 16:29:27 +01:00
Clifford Wolf 8c61ecdd6e Clean up edif code, swap bit indexing of "upto" ports 2017-02-25 16:28:34 +01:00
Clifford Wolf b76c89a5dd Merge branch 'master' of https://github.com/klammerj/yosys into klammerj-master 2017-02-25 15:59:02 +01:00
Clifford Wolf dac0842d61 Add $live and $fair support to AIGER back-end. 2017-02-25 13:07:15 +01:00
Clifford Wolf 7af9727f78 Add "write_smt2 -stbv" 2017-02-24 18:24:53 +01:00
Clifford Wolf a9c3acf5a2 Add SMT2 statebv mode (inactive for now) 2017-02-24 14:04:52 +01:00
Johann Klammer 6d7a77dbf6 Did as you requested, /but/... 
Now the nets are wired in reverse again because the netlister still uses zero-based indices.
 2017-02-24 13:18:49 +01:00
Johann Klammer 06df86aae3 add options for edif flavors 
*to force renames on wide ports
*to choose array delimiters
*to choose up or downwards indices
 2017-02-23 19:42:37 +01:00
Clifford Wolf 242c5f01de Add "yosys-smtbmc -S <opt>" 2017-02-19 22:51:29 +01:00
Clifford Wolf 4e80ce97a8 Add warning about x/z bits left unconnected in EDIF output 2017-02-14 12:49:35 +01:00
Adam Izraelevitz 794cec0016 More progress on Firrtl backend. 
Chisel -> Firrtl -> Verilog -> Firrtl -> Verilog is successful for a
simple rocket-chip design.
 2017-02-13 11:17:53 -08:00
Clifford Wolf 5541b42159 Add assert check in "yosys-smtbmc -c" 2017-02-04 21:22:17 +01:00
Clifford Wolf adbecfee66 Improve yosys-smtbmc cover() support 2017-02-04 21:10:24 +01:00
Clifford Wolf 0c0784b6bf Partially implement cover() support in yosys-smtbmc 2017-02-04 18:17:08 +01:00
Clifford Wolf 6abf79eb28 Further improve cover() support 2017-02-04 17:02:13 +01:00
Clifford Wolf 18ea65ef04 Add "yosys-smtbmc --aig <aim_filename>:<aiw_filename>" support 2017-01-30 11:38:43 +01:00
Clifford Wolf e54c355b41 Add "yosys-smtbmc --aig-noheader" and AIGER mem init support 2017-01-28 15:15:02 +01:00
Clifford Wolf b7cfb7dbd2 Fix $initstate handling bug in yosys-smtbmc 2017-01-11 14:14:12 +01:00
Clifford Wolf b9ad91b93e Implicitly set "yosys-smtbmc --noprogress" on windows 2017-01-04 15:23:48 +01:00
Clifford Wolf ed812ea39c Fixed "yosys-smtbmc --noprogress" 2017-01-04 12:03:04 +01:00
Clifford Wolf 81bb952e5d Handle "always 1" like "always -1" in .smtc files 2017-01-02 20:08:03 +01:00
Clifford Wolf 2198948398 Improved write_json help message 2016-12-29 12:13:29 +01:00
Clifford Wolf a61c88f122 Added $anyconst support to AIGER back-end 2016-12-11 13:48:18 +01:00
Clifford Wolf a44cc7a3d1 Added $assert/$assume support to AIGER back-end 2016-12-03 13:20:29 +01:00
Clifford Wolf 37760541bd Improved yosys-smtbmc default -t/--assume-skipped for --cex and --aig 2016-12-03 12:37:20 +01:00
Clifford Wolf 88b9733253 Added "yosys-smtbmc --aig" 2016-12-01 13:16:57 +01:00
Clifford Wolf 52c243cf05 Added support for partially initialized regs to smt2 back-end 2016-12-01 12:00:00 +01:00
Clifford Wolf 5fa1fa1e6f Added "write_aiger -zinit -symbols -vmap" 2016-12-01 11:04:36 +01:00
Clifford Wolf c1f762ca56 Added "write_aiger" command 2016-11-30 21:30:24 +01:00
Clifford Wolf df2e5aad6f Bugfix in smt2 back-end for pure checker modules 2016-11-28 15:15:09 +01:00
Clifford Wolf c17d98f55c Removed shebang line from smtio.py, fixes #279 2016-11-27 12:11:04 +01:00
Clifford Wolf 5c2c78e2dd Added wire start_offset and upto handling BLIF back-end 2016-11-23 13:54:33 +01:00
Clifford Wolf f257ccf22e Added "yosys-smtbmc --append" 2016-11-22 21:21:13 +01:00
Adam Izraelevitz f77dc3bacc Bugfix: include assign to write-mask 2016-11-18 11:49:26 -08:00
Clifford Wolf e01382739d More progress in FIRRTL back-end 2016-11-18 02:41:29 +01:00
Clifford Wolf c051115e03 Progress in FIRRTL back-end 2016-11-18 00:32:35 +01:00
Clifford Wolf 57966a619f Added first draft of FIRRTL back-end 2016-11-17 23:36:47 +01:00
Clifford Wolf ce132cf652 Cleanups and fixed in write_verilog regarding reg init 2016-11-16 12:00:39 +01:00
Clifford Wolf 3db2ac4e00 Added hex constant support to write_verilog 2016-11-03 12:13:23 +01:00
Clifford Wolf caa2fc62ef Adde "write_verilog -renameprefix -v" 2016-11-01 11:30:27 +01:00
Clifford Wolf aa72262330 Added avail params to ilang format, check module params in 'hierarchy -check' 2016-10-22 11:05:49 +02:00
Clifford Wolf 281a977b39 Ignore L_pi nets in "yosys-smtbmc --cex" 2016-10-18 10:54:53 +02:00
Clifford Wolf 9e980a2bb0 Use init value "2" for all uninitialized FFs in BLIF back-end 2016-10-18 10:54:04 +02:00
Clifford Wolf 0bcc617a4f Added "yosys-smtbmc --cex <filename>" 2016-10-17 14:57:28 +02:00
Clifford Wolf 189fbd4cf8 cleanup in write_smt2 log messages (-bv and -mem are now default) 2016-10-16 23:02:51 +02:00
Clifford Wolf bdc316db50 Added $anyseq cell type 2016-10-14 15:24:03 +02:00
Clifford Wolf 53655d173b Added $global_clock verilog syntax support for creating $ff cells 2016-10-14 12:33:56 +02:00
Clifford Wolf 8ebba8a35f Added $ff and $_FF_ cell types 2016-10-12 01:18:39 +02:00
Clifford Wolf 11130d581d Merge branch 'master' of github.com:cliffordwolf/yosys 2016-10-11 03:58:27 +02:00
Clifford Wolf 5f6a838823 Added smtc support for top-level state with [], [N:] syntax 2016-10-08 12:25:34 +02:00
Clifford Wolf 5f7c5e685b Bugfix in yosys-smtbmc --noincr 2016-10-04 00:54:44 +02:00
Clifford Wolf 1114ce9210 yosys-smtbmc: ABC is a QF_BV solver 2016-10-03 20:43:38 +02:00
Clifford Wolf 99b2093bc4 Added "yosys-smtbmc --noincr" 2016-10-03 20:30:38 +02:00
Clifford Wolf 9aec8a1672 yosys-smtbmc: added smtc [...] support for cells 2016-10-02 22:08:30 +02:00
Clifford Wolf 4eb0d6fc0e Added "yosys-smtbmc -s abc" 2016-10-01 13:54:21 +02:00
Clifford Wolf 34e2fb594d Minor improvements in yosys-smtbmc 2016-09-24 20:40:22 +02:00
Clifford Wolf 2e244c2d8e Added yosys-smtbmc --noinfo and --dummy 2016-09-19 20:43:28 +02:00
Clifford Wolf d009cdd6ee Improved handling of SMT2 logics in yosys-smtbmc 2016-09-18 20:48:09 +02:00
Clifford Wolf 7bc88e8101 yosys-smtbmc: added -i support smtc files 2016-09-18 00:48:36 +02:00
Clifford Wolf d39db41df8 Work-around for boolector bug 2016-09-13 13:23:06 +02:00
Clifford Wolf 6f416c1953 Added missing :produce-models setting to smtio.py 2016-09-11 18:17:22 +02:00
Clifford Wolf 5199aafca0 Minor improvements to smtio.py vcd writer 2016-09-10 16:24:08 +02:00
Clifford Wolf b582f11074 fixed write_smt2 for (non-combinatorial) loops through hierarchical cells 2016-09-10 15:14:41 +02:00
Clifford Wolf 3ceba145d5 smt2 mem init bugfix 2016-09-08 18:08:15 +02:00
Clifford Wolf 14bfd3c5c1 yosys-smtbmc meminit support 2016-09-08 11:16:12 +02:00
Clifford Wolf 209a3d9ffc Bugfix in "yosys-smtbmc --unroll" 2016-09-07 21:01:51 +02:00
Clifford Wolf 6770d6e0f8 Added "yosys-smtbmc --unroll" 2016-09-07 20:57:56 +02:00
Clifford Wolf 97b449fe55 yosys-smtbmc: flush stdout after each log msg 2016-09-06 01:40:31 +02:00
Clifford Wolf 372d672c2a Minor bugfix in write_smt2 2016-09-04 16:32:47 +02:00
Clifford Wolf fa5565b606 Added boolector support to yosys-smtbmc 2016-09-03 14:26:00 +02:00
Clifford Wolf 948aac9e1e Don't re-create hex_dict for each value 2016-09-02 13:46:56 +02:00
Kaj Tuomi d88cd0ae7f More PEP 8 fixes. 2016-09-02 13:09:09 +03:00
Kaj Tuomi c4ba1965fd Indentation and PEP 8 fixes. CamelCase and white space after semicolon. 2016-09-02 13:01:31 +03:00
Kaj Tuomi 2343dda946 Use dict lookup instead of many ifs. 2016-09-02 12:50:23 +03:00
Kaj Tuomi 279298c0b8 Fix: Unresolved reference. 2016-09-02 11:12:30 +03:00
Kaj Tuomi 74dd36ad55 Some syntax fixes. Generator and comma separated list modifications. 2016-09-02 11:02:19 +03:00
Clifford Wolf aa25a4cec6 Added $anyconst support to yosys-smtbmc 2016-08-30 19:27:42 +02:00
Clifford Wolf a8124c137e Fixed memory bug in write_smt2 2016-08-30 14:49:47 +02:00
Clifford Wolf b04a40d9fe Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem" 2016-08-30 12:40:09 +02:00
Clifford Wolf 39e4faa2e4 Added $anyconst support to smt2 back-end 2016-08-30 11:26:10 +02:00
Clifford Wolf c417421495 Added "yosys-smtbmc --dump-all" 2016-08-29 22:41:45 +02:00
Clifford Wolf b226893461 More yosys-smtbmc bugfixes 2016-08-29 14:53:32 +02:00
Clifford Wolf a2e2fc5980 Various fixes and improvements in yosys-smtbmc 2016-08-29 13:53:12 +02:00
Clifford Wolf f56dba8e20 Some changes to yosys-smtbmc cmd line options, add --final-only 2016-08-27 22:04:15 +02:00
Clifford Wolf adcda6817e Added smtc "final" statement 2016-08-27 14:30:36 +02:00
Clifford Wolf 17233b11e1 Various fixes and improvements in smt2 back-end 2016-08-26 17:33:02 +02:00
Clifford Wolf ad56ad44c3 More yosys-smtbmc smtc features 2016-08-24 23:18:29 +02:00
Clifford Wolf ee3e7a0e45 yosys-smtbmc --smtc -g 2016-08-24 22:09:50 +02:00
Clifford Wolf 6523023645 Minor yosys-smtbmc bugfix 2016-08-22 17:45:01 +02:00
Clifford Wolf 583ceee6eb Added "yosys-smtbmc --constr" 2016-08-22 17:27:43 +02:00
Clifford Wolf 2bd30e2026 Added "yosys-smtbmc --dump-constr" 2016-08-22 16:48:46 +02:00
Clifford Wolf 7a33b9892a yosys-smtbmc: improved --dump-vlogtb handling of memories 2016-08-21 15:56:22 +02:00
Clifford Wolf f7578b0239 Added "yosys-smtbmc --dump-vlogtb" 2016-08-20 18:43:39 +02:00
Clifford Wolf ed785194de Added support for memories to smtio.py 2016-08-20 18:42:32 +02:00
Clifford Wolf c325bae792 Deprecated "write_smt2 -regs" (by default on now), and some other smt2 back-end improvements 2016-08-20 18:41:57 +02:00
Clifford Wolf 28271e43c9 Added "yosys-smtbmc -g" 2016-08-20 16:32:50 +02:00
Clifford Wolf a889acb897 Added smtbmc longopt support 2016-08-20 16:07:59 +02:00
Clifford Wolf 75bf7416f0 Bugfix in partial mem write handling in verilog back-end 2016-08-20 13:06:06 +02:00