aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Gracefully report error when module has nothing to prove.Alberto Gonzalez2020-04-041-5/+8
|
* Suppress `yosys-smtbmc` output unless the new `-show-smtbmc` option is provided.Alberto Gonzalez2020-04-041-5/+14
|
* Fix handling of `-sat` and `-unsat` options when the solver returns `unknown`.Alberto Gonzalez2020-04-041-0/+2
|
* Use `log_push()` and `log_pop()` and show the satisfiable model when ↵Alberto Gonzalez2020-04-041-0/+28
| | | | | | `-specialize` is not specified. Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
* Clean up `qbfsat` command and fix AND-reduction of miter outputs.Alberto Gonzalez2020-04-041-8/+10
|
* Use the `-duplicate` option rather than `-save` and `-load` with an explicit ↵Alberto Gonzalez2020-04-041-2/+2
| | | | | | name. Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
* Use internal `run_command()` API instead of `popen()`.Alberto Gonzalez2020-04-041-49/+15
| | | | Co-Authored-By: Claire Wolf <claire@symbioticeda.com>
* Clean up manual casting.Alberto Gonzalez2020-04-041-2/+2
| | | | Co-Authored-By: David Shah <dave@ds0.me>
* Remove unimplemented `-timeout` option.Alberto Gonzalez2020-04-041-16/+4
|
* Implement the `-assume-outputs`, `-sat`, and -unsat` options for the ↵Alberto Gonzalez2020-04-041-3/+66
| | | | `qbfsat` command.
* Add NDEBUG guards to `qbfsat` assertions.Alberto Gonzalez2020-04-041-0/+18
|
* Implement `-specialize-from-file` option for the `qbfsat` command.Alberto Gonzalez2020-04-041-23/+56
|
* Implement `-write-solution` option for the `qbfsat` command.Alberto Gonzalez2020-04-041-7/+28
|
* Clean up `passes/sat/qbfsat.cc`.Alberto Gonzalez2020-04-041-86/+101
|
* Updated `yosys-smtbmc` to optionally dump raw bit strings, and fixed hole ↵Alberto Gonzalez2020-04-042-32/+54
| | | | value recovery using that mode.
* Hole value recovery and specialization implementation for `qbfsat` command.Alberto Gonzalez2020-04-042-20/+70
|
* Barebones implementation of `qbfsat` command.Alberto Gonzalez2020-04-041-32/+157
|
* Initial skeleton for `qbfsat` command.Alberto Gonzalez2020-04-042-0/+207
|
* Rename `-duplicate` to `-push-copy`.Alberto Gonzalez2020-04-041-6/+6
| | | | Co-Authored-By: whitequark <whitequark@whitequark.org>
* Add `-duplicate` option to the `design` command.Alberto Gonzalez2020-04-031-2/+13
|
* Merge pull request #1783 from boqwxp/astcc_cleanupEddie Hung2020-03-301-13/+20
|\ | | | | Clean up pseudo-private member usage in `frontends/ast/ast.cc`.
| * Add explanatory comment about inefficient wire removal and remove ↵Alberto Gonzalez2020-03-301-4/+8
| | | | | | | | | | | | superfluous call to `fixup_ports()`. Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
| * Revert over-aggressive change to a more modest cleanup.Alberto Gonzalez2020-03-271-2/+3
| |
| * Clean up pseudo-private member usage in `frontends/ast/ast.cc`.Alberto Gonzalez2020-03-191-11/+13
| |
* | Merge pull request #1835 from boqwxp/cleanup_sat_exposeEddie Hung2020-03-301-85/+66
|\ \ | | | | | | Clean up pseudo-private member usage in `passes/sat/expose.cc`.
| * | Remove unused function parameter.Alberto Gonzalez2020-03-301-2/+2
| | |
| * | Simplify iterating over selected modules or cells.Alberto Gonzalez2020-03-301-16/+4
| | | | | | | | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
| * | Clean up more in `passes/sat/expose.cc`.Alberto Gonzalez2020-03-301-64/+59
| | | | | | | | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
| * | Clean up pseudo-private member usage in `passes/sat/expose.cc`.Alberto Gonzalez2020-03-281-11/+9
| | |
* | | Merge pull request #1832 from boqwxp/cleanup_passes_cmds_designEddie Hung2020-03-301-31/+33
|\ \ \ | | | | | | | | Clean up pseudo-private member usage in `passes/cmds/design.cc`.
| * | | Replace `RTLIL::id2cstr()` with `log_id()`.Alberto Gonzalez2020-03-301-1/+1
| | | | | | | | | | | | | | | | Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
| * | | Clean up pseudo-private member usage in `passes/cmds/design.cc`.Alberto Gonzalez2020-03-281-31/+33
| |/ /
* | | Merge pull request #1786 from boqwxp/hierarchycc_cleanupEddie Hung2020-03-301-69/+63
|\ \ \ | | | | | | | | Clean up pseudo-private member usage in `passes/hierarchy/hierarchy.cc`.
| * | | Fix double deletion in `passes/hierarchy/hierarchy.cc`.Alberto Gonzalez2020-03-301-1/+0
| | | | | | | | | | | | | | | | Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
| * | | Clean up pseudo-private member usage in `passes/hierarchy/hierarchy.cc`.Alberto Gonzalez2020-03-191-68/+63
| | |/ | |/|
* | | Merge pull request #1831 from boqwxp/cleanup_sat_evalEddie Hung2020-03-301-46/+44
|\ \ \ | | | | | | | | Clean up pseudo-private member usage in `passes/sat/eval.cc`.
| * | | Further clean up `passes/sat/eval.cc`.Alberto Gonzalez2020-03-301-16/+15
| | | | | | | | | | | | | | | | Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
| * | | Clean up pseudo-private member usage in `passes/sat/eval.cc`.Alberto Gonzalez2020-03-281-35/+34
| | |/ | |/|
* | | Merge pull request #1833 from boqwxp/cleanup_sat_freduceEddie Hung2020-03-301-15/+13
|\ \ \ | | | | | | | | Clean up pseudo-private member usage in `passes/sat/freduce.cc`.
| * | | Further clean up `passes/sat/freduce.cc`.Alberto Gonzalez2020-03-301-3/+2
| | | | | | | | | | | | | | | | Co-Authored-By: Eddie Hung <eddie@fpgeh.com>
| * | | Clean up pseudo-private member usage in `passes/sat/freduce.cc`.Alberto Gonzalez2020-03-281-13/+12
| |/ /
* | | Merge pull request #1811 from PeterCrozier/typedef_scopeN. Engelhardt2020-03-306-43/+88
|\ \ \ | | | | | | | | Support module/package/interface/block scope for typedef names.
| * | | Inline productions to follow house style.Peter Crozier2020-03-271-33/+29
| | | |
| * | | Error duplicate declarations of a typedef name in the same scope.Peter Crozier2020-03-242-3/+11
| | | |
| * | | Support module/package/interface/block scope for typedef names.Peter Crozier2020-03-236-22/+63
| | | |
* | | | Merge pull request #1778 from rswarbrick/sv-definesN. Engelhardt2020-03-3011-151/+636
|\ \ \ \ | | | | | | | | | | Add support for SystemVerilog-style `define to Verilog frontend
| * | | | Add support for SystemVerilog-style `define to Verilog frontendRupert Swarbrick2020-03-2711-151/+636
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch should support things like `define foo(a, b = 3, c) a+b+c `foo(1, ,2) which will evaluate to 1+3+2. It also spots mistakes like `foo(1) (the 3rd argument doesn't have a default value, so a call site is required to set it). Most of the patch is a simple parser for the format in preproc.cc, but I've also taken the opportunity to wrap up the "name -> definition" map in a type, rather than use multiple std::map's. Since this type needs to be visible to code that touches defines, I've pulled it (and the frontend_verilog_preproc declaration) out into a new file at frontends/verilog/preproc.h and included that where necessary. Finally, the patch adds a few tests in tests/various to check that we are parsing everything correctly.
* | | | | Explicit include of csignalMiodrag Milanovic2020-03-281-0/+1
| | | | |
* | | | | windows - there are no stopping signalsMiodrag Milanovic2020-03-281-0/+1
| |_|/ / |/| | |
* | | | Merge pull request #1607 from whitequark/simplify-simplify-meminitClaire Wolf2020-03-271-63/+82
|\ \ \ \ | |/ / / |/| | | ast: avoid intermediate wires/assigns when lowering to AST_MEMINIT
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-12 16:25:28 +0000