aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Consistent $mux undef handlingJannis Harder2022-10-245-15/+38
| | | | | | | | | | | | | | | | | | | * Change simlib's $mux cell to use the ternary operator as $_MUX_ already does * Stop opt_expr -keepdc from changing S=x to S=0 * Change const eval of $mux and $pmux to match the updated simlib (fixes sim) * The sat behavior of $mux already matches the updated simlib The verilog frontend uses $mux for the ternary operators and this changes all interpreations of the $mux cell (that I found) to match the verilog simulation behavior for the ternary operator. For 'if' and 'case' expressions the frontend may also use $mux but uses $eqx if the verilog simulation behavior is requested with the '-ifx' option. For $pmux there is a remaining mismatch between the sat behavior and the simlib behavior. Resolving this requires more discussion, as the $pmux cell does not directly correspond to a specific verilog construct.
* Bump versiongithub-actions[bot]2022-10-211-1/+1
|
* Add missing log_dump handler for std::vector<>Claire Xenia Wolf2022-10-201-0/+12
| | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* Bump versiongithub-actions[bot]2022-10-201-1/+1
|
* Temporal induction counterexample loop detection (#3504)Emil J2022-10-191-1/+36
| | | I have added an optional flag to smtbmc that causes failed temporal induction counterexample traces to be checked for duplicate states and reported to the user, since loops in the counterexample mean that increasing the induction depth won't help prove a design's safety properties.
* Merge pull request #3514 from jix/smtbmc-kind-witness-fixJannis Harder2022-10-191-1/+1
|\ | | | | smtbmc: Fix witness handling for k-induction failures
| * smtbmc: Fix witness handling for k-induction failuresJannis Harder2022-10-181-1/+1
| | | | | | | | | | The "uninitialized" value is a _list_ of chunks that are part of the initial state for the witness trace.
* | Bump versiongithub-actions[bot]2022-10-151-1/+1
| |
* | Merge pull request #3511 from YosysHQ/improve_edifMiodrag Milanović2022-10-141-1/+31
|\ \ | |/ |/| verific: enable import all cells
| * Skip verific primitives and operators import by defaultMiodrag Milanovic2022-10-141-0/+1
| |
| * Add option to import all cells from all librariesMiodrag Milanovic2022-10-141-1/+30
|/
* Bump versiongithub-actions[bot]2022-10-131-1/+1
|
* Merge pull request #3510 from jix/ff_witness_fixesJannis Harder2022-10-124-12/+29
|\ | | | | smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
| * smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFsJannis Harder2022-10-124-12/+29
|/ | | | | | | The witness metadata was missing fine grained FFs completely and for coarse grained FFs where the output connection has multiple chunks it lacked the offset of the chunk within the SMT expression. This fixes both, the later by adding an "smtoffset" field to the metadata.
* github: issues: added an OS dropdown to the issue templateAki Van Ness2022-10-121-1/+13
|
* Merge pull request #3502 from jix/equiv_opt_fixesJannis Harder2022-10-1128-267/+207
|\ | | | | equiv_opt and clk2fflogic fixes
| * Reenable existing equiv_opt testsJannis Harder2022-10-0713-54/+52
| |
| * Fix tests for check in equiv_optJannis Harder2022-10-0713-15/+31
| |
| * Add "check -assert" to equiv_optClaire Xenia Wolf2022-10-071-1/+13
| | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
| * Re-enable opt_dff_sr equiv_opt checksClaire Xenia Wolf2022-10-071-13/+12
| | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
| * Exclude primary inputs from quiv_make rewiringClaire Xenia Wolf2022-10-071-0/+7
| | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
| * Revert "Merge pull request #641 from tklam/master"Claire Xenia Wolf2022-10-071-81/+5
| | | | | | | | | | | | | | | | | | | | This reverts commit 08be796cb8b1890923e459cda92211fda763f0c1, reversing changes made to 38dbb44fa0815b1fe80e68e17798aaa341d998cd. This fixes #2728. PR #641 did not actually "fix" #639. The actual issue in #639 is not equiv_make, but assumptions in equiv_simple that are not true for the test case provided in #639.
| * clk2fflogic: Always correctly handle simultaneously changing signalsJannis Harder2022-10-071-103/+87
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a complete rewrite of the FF replacing code. The previous implementation tried to implement the negative hold time by wrapping async control signals individually with pulse stretching. This did not correctly model the interaction between different simultaneously changing inputs (e.g. a falling ALOAD together with a changing AD would load the changed AD instead of the value AD had when ALOAD was high; a falling CLR could mask a raising SET for one cycle; etc.). The new approach first has the logic for all updates using only sampled values followed by the logic for all updates using only current values. That way, e.g., a falling ALOAD will load the sampled AD value but a still active ALOAD will load the current AD value. The new code also has deterministic behavior for the initial state: no operation is active when that operation would depend on a specific previous signal value. This also means clk2fflogic will no longer generate any additional uninitialized FFs. I also documented the negative hold time behavior in the help message, copying the relevant part from async2sync's help messages.
* | Bump versiongithub-actions[bot]2022-10-111-1/+1
| |
* | Merge pull request #3508 from YosysHQ/aki/rm_protobufMiodrag Milanović2022-10-105-562/+0
|\ \ | | | | | | backends: protobuf: removed protobuf backend
| * | backends: protobuf: removed protobuf backendAki Van Ness2022-10-105-562/+0
|/ /
* | fix whitespaceMiodrag Milanovic2022-10-101-1/+1
| |
* | Merge pull request #3452 from ALGCDG/masterMiodrag Milanović2022-10-102-1/+17
|\ \ | | | | | | Add BLIF names command input plane size check
| * | Changing error reason string to be based on lut input plane limit constant.Archie2022-10-021-1/+1
| | |
| * | Adding check for BLIF names command input plane size.Archie2022-08-212-1/+17
| | |
| * | Merge branch 'master' of https://github.com/ALGCDG/yosysArchie2022-08-2181-737/+4859
| |\ \
| * | | Adding expected error message.Archie2022-06-201-0/+1
| | | |
| * | | Adding testcase for issue 3374Archie2022-06-171-0/+3
| | | |
| * | | Add check for BLIF with no model nameArchie2022-06-141-1/+4
| | | |
* | | | Merge pull request #3507 from YosysHQ/claire/verificliboptMiodrag Milanović2022-10-101-0/+14
|\ \ \ \ | | | | | | | | | | Fix handling of verific -L options, add implicit "-L work"
| * | | | Fix handling of verific -L options, add implicit "-L work"Claire Xenia Wolf2022-10-101-0/+14
|/ / / / | | | | | | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* | | | Bump versiongithub-actions[bot]2022-10-081-1/+1
| | | |
* | | | Merge pull request #3503 from jix/abort_on_log_errorJannis Harder2022-10-072-0/+7
|\ \ \ \ | |_|_|/ |/| | | Add YOSYS_ABORT_ON_LOG_ERROR environment variable for debugging.
| * | | Add YOSYS_ABORT_ON_LOG_ERROR environment variable for debugging.Jannis Harder2022-10-072-0/+7
|/ / /
* | | Bump versiongithub-actions[bot]2022-10-061-1/+1
| | |
* | | Next dev cycleMiodrag Milanovic2022-10-052-2/+5
| | |
* | | Release version 0.22Miodrag Milanovic2022-10-052-3/+3
| | |
* | | Update CHANGELOGMiodrag Milanovic2022-10-051-0/+8
| | |
* | | Merge pull request #3500 from nakengelhardt/mutate_warn_not_enoughMiodrag Milanović2022-10-051-0/+2
|\ \ \ | | | | | | | | mutate: warn if less mutations possible than number requested
| * | | mutate: warn if less mutations possible than number requestedN. Engelhardt2022-10-051-0/+2
|/ / /
* | | Merge pull request #3499 from YosysHQ/micko/verific_edifMiodrag Milanović2022-10-052-1/+52
|\ \ \ | | | | | | | | Add support for EDIF file reading using Verific
| * | | Add support for EDIF file reading using VerificMiodrag Milanovic2022-10-042-1/+52
| | | |
* | | | Bump versiongithub-actions[bot]2022-10-051-1/+1
|/ / /
* | | Merge pull request #3494 from YosysHQ/micko/verific_attributesMiodrag Milanović2022-10-041-19/+91
|\ \ \ | | | | | | | | Handle attributes imported from verific
| * | | support file content redirection for verific frontenedMiodrag Milanovic2022-09-281-14/+60
| | | |
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-08 10:53:36 +0000