Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge pull request #3624 from jix/sim_yw | Miodrag Milanović | 2023-01-23 | 5 | -72/+373 |
|\ | | | | | Changes to support SBY trace generation with the sim command | ||||
| * | sim/formalff: Clock handling for yw cosim | Jannis Harder | 2023-01-11 | 2 | -10/+26 |
| | | |||||
| * | sim: Improvements and fixes for yw cosim | Jannis Harder | 2023-01-11 | 3 | -47/+50 |
| | | | | | | | | | | | | * Fixed $cover handling * Improved sparse memory handling when writing traces * JSON summary output | ||||
| * | Support for BTOR witness to Yosys witness conversion | Jannis Harder | 2023-01-11 | 3 | -8/+287 |
| | | |||||
| * | aiger: Use new JSON code for writing aiger witness map files | Jannis Harder | 2023-01-11 | 1 | -49/+49 |
| | | |||||
| * | smt2: Treat bweqx as xnor | Jannis Harder | 2023-01-11 | 1 | -0/+1 |
| | | | | | | | | Without x-bits they are equivalent | ||||
| * | smt2: Directly implement bwmux instead of using bwmuxmap | Jannis Harder | 2023-01-11 | 1 | -2/+4 |
| | | |||||
* | | Fixes for some of clang scan-build detected issues | Miodrag Milanovic | 2023-01-17 | 4 | -6/+12 |
|/ | |||||
* | Add bwmuxmap pass | Jannis Harder | 2022-11-30 | 5 | -0/+5 |
| | |||||
* | verilog_backend: Do not run bmuxmap or demuxmap in -noexpr mode. | Jannis Harder | 2022-11-30 | 1 | -2/+4 |
| | |||||
* | verilog_backend: Correctly sign extend output of signed `$modfloor` | Jannis Harder | 2022-11-30 | 1 | -2/+2 |
| | |||||
* | verilog_backend: Add -noparallelcase option | Jannis Harder | 2022-11-30 | 1 | -7/+31 |
| | |||||
* | smtbmc: Do not assume skipped assertions when loading a witness trace | Jannis Harder | 2022-10-20 | 1 | -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 J | 2022-10-19 | 1 | -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 failures | Jannis Harder | 2022-10-18 | 1 | -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 FFs | Jannis Harder | 2022-10-12 | 3 | -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 backend | Aki Van Ness | 2022-10-10 | 3 | -383/+0 |
| | |||||
* | smtbmc: Avoid unnecessary string copies when parsing solver output | Jannis Harder | 2022-09-02 | 1 | -12/+9 |
| | |||||
* | Fitting help messages to 80 character width | KrystalDelusion | 2022-08-24 | 4 | -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_ FFs | Jannis Harder | 2022-08-18 | 1 | -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-witness | Jannis Harder | 2022-08-16 | 1 | -2/+14 |
| | |||||
* | yosys-witness: Add stats command | Jannis Harder | 2022-08-16 | 1 | -0/+18 |
| | |||||
* | smtbmc: Add --check-witness mode | Jannis Harder | 2022-08-16 | 1 | -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 support | Jannis Harder | 2022-08-16 | 2 | -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 support | Jannis Harder | 2022-08-16 | 6 | -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 cells | Jannis Harder | 2022-08-16 | 1 | -1/+1 |
| | |||||
* | aiger: Support $anyinit cells | Jannis Harder | 2022-08-16 | 1 | -0/+11 |
| | |||||
* | smt2: Support $anyinit cells | Jannis Harder | 2022-08-16 | 1 | -10/+11 |
| | |||||
* | formalff: Set new replaced_by_gclk attribute on removed dff's clks | Jannis Harder | 2022-08-16 | 2 | -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.py | Miodrag Milanovic | 2022-08-09 | 1 | -2/+2 |
| | |||||
* | properly encode string in rtlil | Miodrag Milanovic | 2022-08-09 | 1 | -1/+1 |
| | |||||
* | Merge pull request #3432 from YosysHQ/aki/jny_updates | Miodrag Milanović | 2022-08-03 | 1 | -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 Ness | 2022-08-02 | 1 | -10/+33 |
| | | | | | | | | well as a "$schema" entry to point to the location the schema will be at | ||||
* | | smt2: Fix $shift/$shiftx with negative shift ammounts | Jannis Harder | 2022-08-02 | 1 | -4/+4 |
|/ | | | | Fixes #3431, fixes #3344 | ||||
* | Add support for GHDL modfloor operator | Michael Nolan | 2022-07-05 | 2 | -1/+22 |
| | |||||
* | smt2, btor: Revert calling memory_map -rom-only | Jannis Harder | 2022-06-29 | 2 | -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 formal | Jannis Harder | 2022-06-27 | 2 | -2/+2 |
| | | | | Use it when invoking memory_map -rom-only from write_{smt2,btor}. | ||||
* | btor: add support for $pos cell | Kevin Läufer | 2022-06-20 | 1 | -8/+11 |
| | |||||
* | smt2, btor: Use memory_map -rom-only to make ROMs usable for k-induction | Jannis Harder | 2022-06-17 | 2 | -0/+2 |
| | | | | | | This avoids provability regressions now that we infer more ROMs. This fixes #3378 | ||||
* | smtbmc: noincr: keep solver running for post check-sat unrolling | Jannis Harder | 2022-06-08 | 1 | -2/+7 |
| | |||||
* | Merge pull request #3357 from jix/smtbmc-cvc5 | Jannis Harder | 2022-06-08 | 1 | -3/+13 |
|\ | | | | | smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5 | ||||
| * | smtbmc: recognize cvc5 and fix unrolling for cvc4/cvc5 | Jannis Harder | 2022-06-03 | 1 | -3/+13 |
| | | |||||
* | | smt2: emit smtlib2_comb_expr outputs after all inputs | Jannis Harder | 2022-06-07 | 1 | -5/+9 |
| | | |||||
* | | Merge pull request #3319 from programmerjake/smtlib2-expr-support | Jannis Harder | 2022-06-07 | 1 | -6/+57 |
|\ \ | | | | | | | add smtlib2_comb_expr | ||||
| * | | smt2: Add smtlib2_comb_expr attribute to allow user-selected smtlib2 expressions | Jacob Lifshay | 2022-06-02 | 1 | -6/+57 |
| |/ | |||||
* / | smtbmc: Force nonincremental mode when yices is used with forall | Jannis Harder | 2022-06-03 | 1 | -1/+4 |
|/ | |||||
* | Use proper operator | Miodrag Milanovic | 2022-05-27 | 1 | -4/+4 |
| | |||||
* | add $divfloor support to write_smt2 | Jacob Lifshay | 2022-05-24 | 1 | -0/+21 |
| | | | | Fixes: #3330 | ||||
* | Add propagated clock signals into btor info file | Claire Xenia Wolf | 2022-05-04 | 1 | -0/+2 |
| | |||||
* | smt2: Make write port array stores conditional on nonzero write mask | Jannis Harder | 2022-04-20 | 1 | -2/+4 |
| |