Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | sim: -hdlname option to preserve flattened hierarchy in sim output | Jannis Harder | 2022-08-16 | 2 | -9/+43 |
| | |||||
* | smtbmc: Set step range for --yw and dont skip steps for --check-witness | Jannis Harder | 2022-08-16 | 1 | -2/+14 |
| | |||||
* | Update CEX minimization patches for abc | Jannis Harder | 2022-08-16 | 1 | -1/+1 |
| | |||||
* | clk2fflogic: Generate less unused logic when using verific | Jannis Harder | 2022-08-16 | 1 | -1/+4 |
| | | | | | | Verific generates a lot of FFs with an unused async load and we cannot always optimize that away before running clk2fflogic, so check for that special case here. | ||||
* | rename: Add -witness mode | Jannis Harder | 2022-08-16 | 2 | -0/+83 |
| | |||||
* | 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 | 3 | -2/+320 |
| | | | | | 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 | 9 | -113/+983 |
| | | | | | | | | | | | | | | | | | | | | 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 |
| | |||||
* | memory_map: Add -formal option | Jannis Harder | 2022-08-16 | 2 | -17/+68 |
| | | | | | | This maps memories for a global clock based formal verification flow. This implies -keepdc, uses $ff cells for ROMs and sets hdlname attributes. | ||||
* | setundef: Do not add anyseq / anyconst to unused memory port clocks | Jannis Harder | 2022-08-16 | 1 | -0/+24 |
| | | | | Instead set those unused clocks to zero. | ||||
* | wreduce: Keep more x-bits with -keepdc | Jannis Harder | 2022-08-16 | 1 | -4/+4 |
| | |||||
* | formalff: New -setundef option | Jannis Harder | 2022-08-16 | 1 | -0/+335 |
| | | | | | | | Find FFs with undefined initialization values for which changing the initialization does not change the observable behavior and initialize them. For -ff2anyinit, this reduces the number of generated $anyinit cells that drive wires with private names. | ||||
* | formalff: Set new replaced_by_gclk attribute on removed dff's clks | Jannis Harder | 2022-08-16 | 4 | -0/+44 |
| | | | | | | 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. | ||||
* | Add the $anyinit cell and the formalff pass | Jannis Harder | 2022-08-16 | 16 | -8/+271 |
| | | | | | | | These can be used to protect undefined flip-flop initialization values from optimizations that are not sound for formal verification and can help mapping all solver-provided values in witness traces for flows that use different backends simultaneously. | ||||
* | Bump version | github-actions[bot] | 2022-08-12 | 1 | -1/+1 |
| | |||||
* | Merge pull request #3425 from YosysHQ/lofty/stat-json | N. Engelhardt | 2022-08-11 | 1 | -38/+109 |
|\ | |||||
| * | stat: add option for machine-readable json output | Lofty | 2022-08-11 | 1 | -38/+109 |
| | | |||||
* | | Merge pull request #3277 from YosysHQ/lofty/rename-scramble_name | N. Engelhardt | 2022-08-11 | 2 | -0/+87 |
|\ \ | |/ |/| | |||||
| * | rename: add -scramble-name option to randomly rename selections | Lofty | 2022-08-08 | 2 | -0/+87 |
| | | |||||
* | | Bump version | github-actions[bot] | 2022-08-11 | 1 | -1/+1 |
| | | |||||
* | | Merge pull request #3443 from YosysHQ/micko/resetall_undefineall | Miodrag Milanović | 2022-08-10 | 1 | -0/+5 |
|\ \ | | | | | | | resetall does not affect text defines, but undefineall does | ||||
| * | | set default_nettype to wire for resetall | Miodrag Milanovic | 2022-08-10 | 1 | -0/+1 |
| | | | |||||
| * | | resetall does not affect text defines, but undefineall does | Miodrag Milanovic | 2022-08-10 | 1 | -0/+4 |
|/ / | |||||
* | | Merge pull request #3322 from Forty-Bot/default_assignment_first | N. Engelhardt | 2022-08-10 | 1 | -10/+38 |
|\ \ | |||||
| * | | Order ports with default assignments first | Sean Anderson | 2022-08-09 | 1 | -10/+38 |
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | Although the current style is allowed by the standard, Icarus verilog doesn't parse default assignments using an implicit net type: techlibs/ice40/cells_sim.v:305: syntax error techlibs/ice40/cells_sim.v:1: Errors in port declarations. Fix this by making sure that ports with default assignments first on their line. Fixes: 46d3f03d2 ("Add default assignments to other SB_* simulation models") Signed-off-by: Sean Anderson <seanga2@gmail.com> | ||||
* | | Bump version | github-actions[bot] | 2022-08-10 | 1 | -1/+1 |
| | | |||||
* | | nexus: Fix BRAM mapping. | Marcelina Kościelnicka | 2022-08-09 | 1 | -18/+56 |
| | | |||||
* | | Merge pull request #3441 from YosysHQ/micko/smtio-utf-8 | Miodrag Milanović | 2022-08-09 | 1 | -2/+2 |
|\ \ | | | | | | | Switched to utf-8 in smtio.py | ||||
| * | | 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 |
| | | |||||
* | | Bump version | github-actions[bot] | 2022-08-09 | 1 | -1/+1 |
| | | |||||
* | | Merge pull request #3439 from YosysHQ/micko/filepath_improve | Miodrag Milanović | 2022-08-08 | 10 | -60/+90 |
|\ \ | |/ |/| | File path encoding improvements | ||||
| * | support file locations containing spaces | Miodrag Milanovic | 2022-08-08 | 6 | -18/+19 |
| | | |||||
| * | Encode filename unprintable chars | Miodrag Milanovic | 2022-08-08 | 4 | -27/+42 |
| | | |||||
| * | verific - make filepath handling compatible with verilog frontend | Miodrag Milanovic | 2022-08-08 | 1 | -15/+29 |
|/ | |||||
* | Bump version | github-actions[bot] | 2022-08-04 | 1 | -1/+1 |
| | |||||
* | Next dev cycle | Miodrag Milanovic | 2022-08-03 | 2 | -2/+5 |
| | |||||
* | Release version 0.20 | Miodrag Milanovic | 2022-08-03 | 2 | -3/+3 |
| | |||||
* | Update Changelog | Miodrag Milanovic | 2022-08-03 | 1 | -0/+7 |
| | |||||
* | update manual to latest | Miodrag Milanovic | 2022-08-03 | 1 | -2/+5 |
| | |||||
* | Merge pull request #3432 from YosysHQ/aki/jny_updates | Miodrag Milanović | 2022-08-03 | 2 | -10/+226 |
|\ | | | | | jny: Added JNY schema and additional information to JNY output file | ||||
| * | misc: Added JNY schema definition | Aki Van Ness | 2022-08-02 | 1 | -0/+193 |
| | | |||||
| * | 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 | ||||
* | | Update manual and changelog | Miodrag Milanovic | 2022-08-03 | 2 | -0/+9 |
| | | |||||
* | | Bump version | github-actions[bot] | 2022-08-03 | 1 | -1/+1 |
| | | |||||
* | | Merge pull request #3433 from jix/fix_smt_shift | Jannis Harder | 2022-08-02 | 1 | -4/+4 |
|\ \ | |/ |/| | smt2: Fix $shift/$shiftx with negative shift ammounts |