aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
Commit message (Collapse)AuthorAgeFilesLines
* sim: For yw cosim, drive parent module's signals for input portsJannis Harder2023-02-131-1/+25
|
* formalff: Fix crash with _NOT_ gates in -hierarchy modeJannis Harder2023-01-251-1/+1
|
* sim/formalff: Clock handling for yw cosimJannis Harder2023-01-112-21/+246
|
* sim: Improvements and fixes for yw cosimJannis Harder2023-01-111-4/+91
| | | | | | * Fixed $cover handling * Improved sparse memory handling when writing traces * JSON summary output
* sim: New -append option for Yosys witness cosimJannis Harder2023-01-111-5/+14
| | | | This is needed to support SBY's append option.
* sim: Add Yosys witness (.yw) cosimulationJannis Harder2023-01-111-3/+194
|
* sim: Only check formal cells during gclk simulation updatesJannis Harder2023-01-111-16/+19
| | | | This is required for compatibility with non-multiclock formal semantics.
* sim: Internal API to set $initstateJannis Harder2023-01-111-0/+11
| | | | This is not yet added to any of the simulation drivers.
* sim: Emit used memory addresses as signals to output tracesJannis Harder2023-01-111-17/+122
| | | | | | | | This matches the behavior of smtbmc. This also updates the sim internal memory API to allow masked writes where State::Sa bits (internal don't care - not a valid value for a signal) leave the memory content unchanged.
* Merge branch 'master' into claire/eqystuffClaire Xen2023-01-112-28/+28
|\
| * Merge pull request #3537 from jix/xpropJannis Harder2023-01-113-13/+30
| |\ | | | | | | New xprop pass
| * | Deprecate gcc-4.8Miodrag Milanovic2023-01-112-28/+28
| | |
* | | Merge branch 'master' of github.com:YosysHQ/yosys into claire/eqystuffClaire Xenia Wolf2023-01-113-3/+10
|\| |
| * | qbfsat support for cvc5, fixes #3608Miodrag Milanovic2023-01-092-3/+7
| | |
| * | formalff: Proper error messages on async inputs for the -clk2ff modeJannis Harder2022-12-091-0/+3
| | |
* | | Allow non-unique modules without state in sim writeback-modeClaire Xenia Wolf2022-12-211-4/+5
| | | | | | | | | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* | | Add gold-x handing to miter cross port handlingClaire Xenia Wolf2022-12-081-1/+9
| |/ |/| | | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* | miter: Add -make_cover option to cover each output pair differenceJannis Harder2022-11-301-0/+14
| |
* | formalff: Fix -ff2anyinit assertion error for fine FFsJannis Harder2022-11-301-0/+2
| |
* | sim: Improved global clock handlingJannis Harder2022-11-301-13/+14
|/
* sat: Add -set-def-formal option to force defined $any* outputsJannis Harder2022-11-281-6/+22
|
* Rst docs conversion (#3496)KrystalDelusion2022-11-151-1/+1
| | | Rst docs conversion
* sim: Run a comb-only update step to set past values during FST cosimJannis Harder2022-11-071-12/+11
| | | | | | | | The previous approach only initialized past_d and past_ad while for FST cosim we also need to initialize the other past values like past_clk, etc. Also to properly initialize them, we need to run a combinational update step in case any of the wires feeding into the FF are private or otherwise not part of the FST.
* Add extra time at the end of a sat VCD traceClaire Xenia Wolf2022-11-011-0/+1
| | | | | | | Otherwise the final values will not show up in gtkwave waveforms when looking at the generated traces. Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* Add miter -cross optionClaire Xenia Wolf2022-10-241-4/+32
|
* 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.
* mutate: warn if less mutations possible than number requestedN. Engelhardt2022-10-051-0/+2
|
* Fitting help messages to 80 character widthKrystalDelusion2022-08-242-24/+28
| | | | | | | | | 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.
* sim: -hdlname option to preserve flattened hierarchy in sim outputJannis Harder2022-08-161-9/+41
|
* clk2fflogic: Generate less unused logic when using verificJannis Harder2022-08-161-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.
* formalff: New -setundef optionJannis Harder2022-08-161-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 clksJannis Harder2022-08-161-0/+22
| | | | | | 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 passJannis Harder2022-08-163-1/+194
| | | | | | | 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.
* support file locations containing spacesMiodrag Milanovic2022-08-081-1/+1
|
* sim: Fix $anyseq in nested modulesJannis Harder2022-07-221-11/+21
|
* async2sync: turn FFs with const clks into gclk FFs with feedbackJannis Harder2022-06-301-0/+3
| | | | | | | | The formal backends do not support multiple clocks. This includes constant clocks. Constant clocks do appear in what isn't a proper multiclock design, for example when mapping not fully initialized ROMs. As converting FFs with constant clocks to FFs using the global is doable even in a single clock flow, make async2sync do this.
* fmcombine: Add _gold/_gate suffix to memidsJannis Harder2022-06-031-0/+3
|
* Observe $TMPDIR variable when creating tmp filesMohamed A. Bamakhrama2022-05-271-1/+1
| | | | | | | | | POSIX defines $TMPDIR as containing the pathname of the directory where programs can create temporary files. On most systems, this variable points to "/tmp". However, on some systems it can point to a different location. Without respecting this variable, yosys fails to run on such systems. Signed-off-by: Mohamed A. Bamakhrama <mohamed@alumni.tum.de>
* fix crash when no fst inputMiodrag Milanovic2022-05-041-1/+2
|
* Start restoring memory state from VCD/FSTMiodrag Milanovic2022-05-041-2/+17
|
* AIM file could have gaps in or between inputs and initsMiodrag Milanovic2022-05-021-3/+6
|
* Match $anyseq input if connected to public wireMiodrag Milanovic2022-04-221-6/+12
|
* Treat $anyseq as input from FSTMiodrag Milanovic2022-04-221-0/+21
|
* Last sample from input does not represent changeMiodrag Milanovic2022-04-221-1/+2
|
* latches are always set to zeroMiodrag Milanovic2022-04-221-6/+1
|
* If not multiclock, output only on clock edgesMiodrag Milanovic2022-04-221-0/+18
|
* Set init state for all wires from FST and set pastMiodrag Milanovic2022-04-221-13/+12
|
* Fix multiclock for btor2 witnessMiodrag Milanovic2022-04-221-5/+9
|
* Fix reading aiw from other solversMiodrag Milanovic2022-04-151-2/+2
|
* Use wrap_async_control_gate if ff is fineMiodrag Milanovic2022-04-081-9/+11
|
generated by cgit v1.2.3 (git 2.25.1) at 2025-03-23 05:14:06 +0000