aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
| * | | ast: avoid intermediate wires/assigns when lowering to AST_MEMINIT.whitequark2020-02-071-65/+84
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Before this commit, every initial assignment to a memory generated two wires and four assigns in a process. For unknown reasons (I did not investigate), large amounts of assigns cause quadratic slowdown later in the AST frontend, in processAst/removeSignalFromCaseTree. As a consequence, common and reasonable Verilog code, such as: reg [`WIDTH:0] mem [0:`DEPTH]; integer i; initial for (i = 0; i <= `DEPTH; i++) mem[i] = 0; took extremely long time to be processed; around 80 s for a 8-wide, 8192-deep memory. After this commit, initial assignments where address and/or data are constant (after `generate`) do not incur the cost of intermediate wires; expressions like `mem[i+1]=i^(i<<1)` are considered constant. This results in speedups of orders of magnitude for common memory sizes; it now takes merely 0.4 s to process a 8-wide, 8192-deep memory, and only 5.8 s to process a 8-wide, 131072-deep one. As a bonus, this change also results in nontrivial speedups later in the synthesis pipeline, since pass sequencing issues meant that all of these intermediate wires were subject to transformations such as width reduction, even though they existed solely to be constant folded away in `memory_collect`.
* | | | Merge pull request #1815 from boqwxp/fix-ef-optimizeClaire Wolf2020-03-271-1/+7
|\ \ \ \ | | | | | | | | | | Fix solver output parsing for exists-forall optimization
| * | | | Do not change solver output parsing for non-exists-forall problems.Alberto Gonzalez2020-03-261-2/+6
| | | | |
| * | | | Skip reading stdout from the solver that if it isn't a line reading only ↵Alberto Gonzalez2020-03-261-1/+3
| | | | | | | | | | | | | | | | | | | | "sat", "unsat", or "unknown".
* | | | | Merge pull request #1806 from YosysHQ/mwk/techmap-replace-fixClaire Wolf2020-03-262-1/+19
|\ \ \ \ \ | |/ / / / |/| | | | techmap: Fix cell names with _TECHMAP_REPLACE_.*
| * | | | techmap: Fix cell names with _TECHMAP_REPLACE_.*Marcin Kościelnicki2020-03-232-1/+19
| | | | | | | | | | | | | | | | | | | | Fixes #1804.
* | | | | Revert part of 0fda8308 from #1746 that broke other smtbmc flowsClaire Wolf2020-03-241-3/+1
| | | | | | | | | | | | | | | | | | | | Signed-off-by: Claire Wolf <claire@symbioticeda.com>
* | | | | Merge pull request #1763 from boqwxp/issue1762N. Engelhardt2020-03-238-12/+73
|\ \ \ \ \ | |_|_|/ / |/| | | | Closes #1762. Adds warnings for `select` arguments not matching any object and for `add` command when no modules selected
| * | | | Do not warn on empty selection with prefixed `arg_memb`.Alberto Gonzalez2020-03-232-1/+7
| | | | | | | | | | | | | | | | | | | | Co-Authored-By: N. Engelhardt <nak@symbioticeda.com>
| * | | | Suppress warnings for empty `select` arguments when `-count` or `-assert-*` ↵Alberto Gonzalez2020-03-232-4/+7
| | | | | | | | | | | | | | | | | | | | options are set.
| * | | | Add tests for `select` command warnings.Alberto Gonzalez2020-03-234-0/+13
| | | | |
| * | | | Warn on empty selection for `add` command.Alberto Gonzalez2020-03-232-6/+40
| | | | |
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-23 11:02:39 +0000