aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
Commit message (Collapse)AuthorAgeFilesLines
* 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
|
* Fixes and error checkMiodrag Milanovic2022-03-091-1/+5
|
* cleanupMiodrag Milanovic2022-03-071-1/+2
|
* Error checks for aiger witnessMiodrag Milanovic2022-03-071-0/+7
|
* btor2 witness co-simulationMiodrag Milanovic2022-03-071-8/+123
|
* Merge pull request #3219 from YosysHQ/micko/quick_vcdMiodrag Milanović2022-03-041-0/+1
|\ | | | | VCD reader support by using external tool
| * VCD reader support by using external toolMiodrag Milanovic2022-02-281-0/+1
| |
* | Add option to ignore X only signals in outputMiodrag Milanovic2022-03-021-8/+32
| |
* | Write simulation files after simulation is performedMiodrag Milanovic2022-03-021-145/+151
| |
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-06 15:08:17 +0000