aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
Commit message (Collapse)AuthorAgeFilesLines
* 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
|
* Makefile: properly conditionalize features requiring compression.Iris Johnson2022-04-071-0/+2
|
* past_ad initial value settingMiodrag Milanovic2022-04-021-0/+3
|
* setInitState can be only one altering valuesMiodrag Milanovic2022-04-021-4/+6
|
* Set past_d value for init stateMiodrag Milanovic2022-04-021-0/+2
|
* Set init values for wrapped async control signalsMiodrag Milanovic2022-04-011-0/+2
|
* Support memories in aiw and multiclockMiodrag Milanovic2022-03-311-16/+86
|
* Proper SigBit forming in simMiodrag Milanovic2022-03-221-4/+4
|
* Proper SigBit forming in simMiodrag Milanovic2022-03-221-4/+4
|
* More verbose warningsMiodrag Milanovic2022-03-181-5/+7
|
* Recognize registers and set initial state for them in tbMiodrag Milanovic2022-03-161-6/+32
|
* Update sim help message.Miodrag Milanovic2022-03-161-1/+2
|
* Added fst2tb pass for generating testbenchMiodrag Milanovic2022-03-141-0/+319
|
* Merge pull request #3229 from YosysHQ/micko/sim_dateMiodrag Milanović2022-03-111-7/+20
|\ | | | | Add date parameter to enable full date/time and version info
| * Add date parameter to enable full date/time and version infoMiodrag Milanovic2022-03-111-7/+20
| |
* | Add "sim -q" optionClaire Xenia Wolf2022-03-111-8/+19
|/ | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* Small fix in "sim" help messageClaire Xenia Wolf2022-03-111-1/+1
| | | | Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
* FstData already do conversion to VCDMiodrag Milanovic2022-03-111-1/+2
|
* Support cell name in btor witness fileMiodrag Milanovic2022-03-111-5/+14
|
* Proper write of memory dataMiodrag Milanovic2022-03-111-14/+13
|
* Start work on memory initMiodrag Milanovic2022-03-091-9/+34
|
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-01 10:49:10 +0000