aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat/sim.cc
Commit message (Collapse)AuthorAgeFilesLines
* sim: For yw cosim, drive parent module's signals for input portsJannis Harder2023-02-131-1/+25
|
* sim/formalff: Clock handling for yw cosimJannis Harder2023-01-111-19/+32
|
* 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.
* 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>
* sim: Improved global clock handlingJannis Harder2022-11-301-13/+14
|
* 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.
* Fitting help messages to 80 character widthKrystalDelusion2022-08-241-3/+4
| | | | | | | | | 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
|
* Add the $anyinit cell and the formalff passJannis Harder2022-08-161-1/+1
| | | | | | | 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.
* sim: Fix $anyseq in nested modulesJannis Harder2022-07-221-11/+21
|
* 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
|
* 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
|
* 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
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-23 12:03:34 +0000