| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| ... | |
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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
|
| |/ / / /
| | | |
| | | |
| | | | |
This broke while switching sby's formal flows to always use $_FF_'s.
|
| | | | | |
|
| |\ \ \ \
| | | | |
| | | | | |
Updated formal flow with new witness format
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This verifies that the given constraints force an assertion failure.
This is useful to debug witness trace conversion (and minimization).
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Adds a new json based aiger map file and yosys-witness converters to us
this to convert between native and AIGER witness files.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This maps memories for a global clock based formal verification flow.
This implies -keepdc, uses $ff cells for ROMs and sets hdlname
attributes.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Instead set those unused clocks to zero.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | | |
|
| |\ \ \ \ |
|
| | | | | | |
|
| |\ \ \ \ \
| |/ / / /
|/| | | | |
|
| | | | | | |
|
| | | | | | |
|
| |\ \ \ \ \
| | | | | |
| | | | | | |
resetall does not affect text defines, but undefineall does
|
| | | | | | | |
|
| |/ / / / / |
|
| |\ \ \ \ \ |
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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>
|
| | | | | | |
|
| | | | | | |
|
| |\ \ \ \ \
| | | | | |
| | | | | | |
Switched to utf-8 in smtio.py
|
| |/ / / / / |
|
| | | | | | |
|
| | | | | | |
|
| |\ \ \ \ \
| |/ / / /
|/| | | | |
File path encoding improvements
|
| | | | | | |
|
| | | | | | |
|
| |/ / / / |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
