aboutsummaryrefslogtreecommitdiffstats
path: root/backends
Commit message (Collapse)AuthorAgeFilesLines
* ABC9: Cell Port Bug Patch (#3670)Benjamin Barzen2023-04-221-1/+5
| | | | | | | | | | | | | | | | | * ABC9: RAMB36E1 Bug Patch * Add simplified testcase * Also fix xaiger writer for under-width output ports * Remove old testcase * Missing top-level input port * Fix tabs --------- Co-authored-by: Eddie Hung <eddie@fpgeh.com>
* yosys-smtbmc: support -h/--help (and exit with code 0).Catherine2023-02-271-4/+13
|
* verilog_backend: Do not run bwmuxmap even if in expr modeJannis Harder2023-02-131-1/+0
| | | | | While bwmuxmap generates equivalent logic, it doesn't propagate x bits in the same way, which can be relevant when writing verilog.
* backends/firrtl: Ensure `modInstance` is validAki Van Ness2023-02-031-0/+6
| | | | | | | This should fix #3648 where when calling `emit_elaborated_extmodules` it checks to see if a module is a black-box, however there was no validation that the cell type was actually known, and it just always assumed that we would get a valid instance, causing a segfault.
* Merge pull request #3655 from jix/smt2_fix_b_op_widthJannis Harder2023-02-011-1/+4
|\ | | | | smt2: Fix operation width computation for boolean producing cells
| * smt2: Fix operation width computation for boolean producing cellsJannis Harder2023-02-011-1/+4
| | | | | | | | | | | | | | | | | | | | The output width for the boolean value should not influence the operation width. The previous incorrect width extension would still produce correct results, but could produce invalid smt2 output for reduction operators when the output width was larger than the width of the vector to which the reduction was applied. This fixes #3654
* | backends/rtlil: Do not shorten a value with z bits to 'xJannis Harder2023-01-291-1/+1
|/
* Merge pull request #3624 from jix/sim_ywMiodrag Milanović2023-01-235-72/+373
|\ | | | | Changes to support SBY trace generation with the sim command
| * sim/formalff: Clock handling for yw cosimJannis Harder2023-01-112-10/+26
| |
| * sim: Improvements and fixes for yw cosimJannis Harder2023-01-113-47/+50
| | | | | | | | | | | | * Fixed $cover handling * Improved sparse memory handling when writing traces * JSON summary output
| * Support for BTOR witness to Yosys witness conversionJannis Harder2023-01-113-8/+287
| |
| * aiger: Use new JSON code for writing aiger witness map filesJannis Harder2023-01-111-49/+49
| |
| * smt2: Treat bweqx as xnorJannis Harder2023-01-111-0/+1
| | | | | | | | Without x-bits they are equivalent
| * smt2: Directly implement bwmux instead of using bwmuxmapJannis Harder2023-01-111-2/+4
| |
* | Fixes for some of clang scan-build detected issuesMiodrag Milanovic2023-01-174-6/+12
|/
* Add bwmuxmap passJannis Harder2022-11-305-0/+5
|
* verilog_backend: Do not run bmuxmap or demuxmap in -noexpr mode.Jannis Harder2022-11-301-2/+4
|
* verilog_backend: Correctly sign extend output of signed `$modfloor`Jannis Harder2022-11-301-2/+2
|
* verilog_backend: Add -noparallelcase optionJannis Harder2022-11-301-7/+31
|
* smtbmc: Do not assume skipped assertions when loading a witness traceJannis Harder2022-10-201-3/+0
| | | | | | This is not valid when the prefix of a trace already violates assertions. This can happen when the trace generating solver doesn't look for a minimal length counterexample.
* 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.
* 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.
* smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFsJannis Harder2022-10-123-5/+22
| | | | | | | 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.
* backends: protobuf: removed protobuf backendAki Van Ness2022-10-103-383/+0
|
* smtbmc: Avoid unnecessary string copies when parsing solver outputJannis Harder2022-09-021-12/+9
|
* Fitting help messages to 80 character widthKrystalDelusion2022-08-244-9/+10
| | | | | | | | | Uses the regex below to search (using vscode): ^\t\tlog\("(.{10,}(?<!\\n)|.{81,}\\n)"\); Finds any log messages double indented (which help messages are) and checks if *either* there are is no newline character at the end, *or* the number of characters before the newline is more than 80.
* write_aiger: Fix non-$_FF_ FFsJannis Harder2022-08-181-1/+1
| | | | This broke while switching sby's formal flows to always use $_FF_'s.
* smtbmc: Set step range for --yw and dont skip steps for --check-witnessJannis Harder2022-08-161-2/+14
|
* yosys-witness: Add stats commandJannis Harder2022-08-161-0/+18
|
* smtbmc: Add --check-witness modeJannis Harder2022-08-161-1/+22
| | | | | This verifies that the given constraints force an assertion failure. This is useful to debug witness trace conversion (and minimization).
* aiger: Add yosys-witness supportJannis Harder2022-08-162-2/+317
| | | | | Adds a new json based aiger map file and yosys-witness converters to us this to convert between native and AIGER witness files.
* smtbmc: Add native json based witness format + smt2 backend supportJannis Harder2022-08-166-113/+968
| | | | | | | | | | | | | | | | | | | | This adds a native json based witness trace format. By having a common format that includes everything we support, and providing a conversion utility (yosys-witness) we no longer need to implement every format for every tool that deals with witness traces, avoiding a quadratic opportunity to introduce subtle bugs. Included: * smt2: New yosys-smt2-witness info lines containing full hierarchical paths without lossy escaping. * yosys-smtbmc --dump-yw trace.yw: Dump results in the new format. * yosys-smtbmc --yw trace.yw: Read new format as constraints. * yosys-witness: New tool to convert witness formats. Currently this can only display traces in a human-readable-only format and do a passthrough read/write of the new format. * ywio.py: Small python lib for reading and writing the new format. Used by yosys-smtbmc and yosys-witness to avoid duplication.
* btor: Support $anyinit cellsJannis Harder2022-08-161-1/+1
|
* aiger: Support $anyinit cellsJannis Harder2022-08-161-0/+11
|
* smt2: Support $anyinit cellsJannis Harder2022-08-161-10/+11
|
* formalff: Set new replaced_by_gclk attribute on removed dff's clksJannis Harder2022-08-162-0/+21
| | | | | | This attribute can be used by formal backends to indicate which clocks were mapped to the global clock. Update the btor and smt2 backend which already handle clock inputs to understand this attribute.
* Switched to utf-8 in smtio.pyMiodrag Milanovic2022-08-091-2/+2
|
* properly encode string in rtlilMiodrag Milanovic2022-08-091-1/+1
|
* Merge pull request #3432 from YosysHQ/aki/jny_updatesMiodrag Milanović2022-08-031-10/+33
|\ | | | | jny: Added JNY schema and additional information to JNY output file
| * backend: jny: updated the `JnyWriter` to emite a new "invocation" entry as ↵Aki Van Ness2022-08-021-10/+33
| | | | | | | | well as a "$schema" entry to point to the location the schema will be at
* | smt2: Fix $shift/$shiftx with negative shift ammountsJannis Harder2022-08-021-4/+4
|/ | | | Fixes #3431, fixes #3344
* Add support for GHDL modfloor operatorMichael Nolan2022-07-052-1/+22
|
* smt2, btor: Revert calling memory_map -rom-onlyJannis Harder2022-06-292-2/+0
| | | | | | | | This approach had major issues with ROMs whose initialization was not fully defined. If required, memory_map -rom-only -keepdc should be called early in a formal flow instead. (This does require a careful choice of optimization passes though. Sby's scripts will be updated accordingly.)
* memory_map: -keepdc option for formalJannis Harder2022-06-272-2/+2
| | | | Use it when invoking memory_map -rom-only from write_{smt2,btor}.
* btor: add support for $pos cellKevin Läufer2022-06-201-8/+11
|
* smt2, btor: Use memory_map -rom-only to make ROMs usable for k-inductionJannis Harder2022-06-172-0/+2
| | | | | | This avoids provability regressions now that we infer more ROMs. This fixes #3378
* smtbmc: noincr: keep solver running for post check-sat unrollingJannis Harder2022-06-081-2/+7
|
* Merge pull request #3357 from jix/smtbmc-cvc5Jannis Harder2022-06-081-3/+13
|\ | | | | smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5
| * smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5Jannis Harder2022-06-031-3/+13
| |
* | smt2: emit smtlib2_comb_expr outputs after all inputsJannis Harder2022-06-071-5/+9
| |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 08:22:14 +0000