Krystine Sherwin
5a4e72f57a
Fix sim writeback check for yw_cosim
...
Writeback of simulation state into initial state was only working for `run()` and `run_cosim_fst()`.
This change moves the writeback into the `write_output_files()` function so that all simulation modes work with the writeback option.
2023-05-08 13:13:09 +12:00
Jannis Harder
1698202ccc
sim: For yw cosim, drive parent module's signals for input ports
2023-02-13 12:26:06 +01:00
Jannis Harder
d6c7aa0e3d
sim/formalff: Clock handling for yw cosim
2023-01-11 18:07:16 +01:00
Jannis Harder
7ddec5093f
sim: Improvements and fixes for yw cosim
...
* Fixed $cover handling
* Improved sparse memory handling when writing traces
* JSON summary output
2023-01-11 18:07:16 +01:00
Jannis Harder
dda972a148
sim: New -append option for Yosys witness cosim
...
This is needed to support SBY's append option.
2023-01-11 18:07:16 +01:00
Jannis Harder
2dd5652215
sim: Add Yosys witness (.yw) cosimulation
2023-01-11 18:07:16 +01:00
Jannis Harder
f6458bab70
sim: Only check formal cells during gclk simulation updates
...
This is required for compatibility with non-multiclock formal semantics.
2023-01-11 18:07:16 +01:00
Jannis Harder
9c6198a827
sim: Internal API to set $initstate
...
This is not yet added to any of the simulation drivers.
2023-01-11 18:07:16 +01:00
Jannis Harder
44b26d5c6d
sim: Emit used memory addresses as signals to output traces
...
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.
2023-01-11 18:07:16 +01:00
Claire Xenia Wolf
1bc832a8e1
Allow non-unique modules without state in sim writeback-mode
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-12-21 10:43:02 +01:00
Jannis Harder
5ff69a0fe2
sim: Improved global clock handling
2022-11-30 18:50:53 +01:00
KrystalDelusion
a14dec79eb
Rst docs conversion ( #3496 )
...
Rst docs conversion
2022-11-15 12:55:22 +01:00
Jannis Harder
9b4fba3870
sim: Run a comb-only update step to set past values during FST cosim
...
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.
2022-11-07 14:09:33 +01:00
KrystalDelusion
9465b2af95
Fitting help messages to 80 character width
...
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.
2022-08-24 10:40:57 +12:00
Jannis Harder
f7023d06a2
sim: -hdlname option to preserve flattened hierarchy in sim output
2022-08-16 13:37:30 +02:00
Jannis Harder
c0063288d6
Add the $anyinit cell and the formalff pass
...
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.
2022-08-16 13:37:30 +02:00
Jannis Harder
14ba50908b
sim: Fix $anyseq in nested modules
2022-07-22 14:48:30 +02:00
Miodrag Milanovic
8e02b3ca30
fix crash when no fst input
2022-05-04 11:21:39 +02:00
Miodrag Milanovic
ad48639cdd
Start restoring memory state from VCD/FST
2022-05-04 10:41:04 +02:00
Miodrag Milanovic
3730db4b98
AIM file could have gaps in or between inputs and inits
2022-05-02 11:18:30 +02:00
Miodrag Milanovic
bbfdea2f8a
Match $anyseq input if connected to public wire
2022-04-22 17:20:17 +02:00
Miodrag Milanovic
4d80bc24c7
Treat $anyseq as input from FST
2022-04-22 16:23:39 +02:00
Miodrag Milanovic
33f4009bb5
Last sample from input does not represent change
2022-04-22 13:46:11 +02:00
Miodrag Milanovic
83cad82b29
latches are always set to zero
2022-04-22 12:04:05 +02:00
Miodrag Milanovic
c989adcc2d
If not multiclock, output only on clock edges
2022-04-22 12:03:39 +02:00
Miodrag Milanovic
75032a565d
Set init state for all wires from FST and set past
2022-04-22 11:57:39 +02:00
Miodrag Milanovic
8fa2f3b260
Fix multiclock for btor2 witness
2022-04-22 11:53:41 +02:00
Miodrag Milanovic
9508bb2330
Fix reading aiw from other solvers
2022-04-15 11:45:16 +02:00
Miodrag Milanovic
6020ba67ac
past_ad initial value setting
2022-04-02 19:13:15 +02:00
Miodrag Milanovic
2c96ecc5f7
setInitState can be only one altering values
2022-04-02 19:13:15 +02:00
Miodrag Milanovic
b54aecd80a
Set past_d value for init state
2022-04-02 19:13:15 +02:00
Miodrag Milanovic
c95b9b4ba5
Support memories in aiw and multiclock
2022-03-31 13:10:13 +02:00
Miodrag Milanovic
322ab1cd54
Proper SigBit forming in sim
2022-03-22 14:43:18 +01:00
Miodrag Milanovic
ff3b0c2c46
Proper SigBit forming in sim
2022-03-22 14:22:32 +01:00
Miodrag Milanovic
55eed8df57
More verbose warnings
2022-03-18 14:47:35 +01:00
Miodrag Milanovic
1f3423cd7d
Recognize registers and set initial state for them in tb
2022-03-16 14:35:39 +01:00
Miodrag Milanovic
e217e3017a
Update sim help message.
2022-03-16 07:55:57 +01:00
Miodrag Milanovic
f5c20b8286
Added fst2tb pass for generating testbench
2022-03-14 19:06:29 +01:00
Miodrag Milanović
cbece4af0c
Merge pull request #3229 from YosysHQ/micko/sim_date
...
Add date parameter to enable full date/time and version info
2022-03-11 19:02:57 +01:00
Claire Xenia Wolf
e21badd4b3
Add "sim -q" option
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-03-11 16:26:11 +01:00
Miodrag Milanovic
37de369ba7
Add date parameter to enable full date/time and version info
2022-03-11 16:01:59 +01:00
Claire Xenia Wolf
be32de1caa
Small fix in "sim" help message
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-03-11 15:36:23 +01:00
Miodrag Milanovic
5204694123
FstData already do conversion to VCD
2022-03-11 15:21:36 +01:00
Miodrag Milanovic
b72c779204
Support cell name in btor witness file
2022-03-11 15:11:14 +01:00
Miodrag Milanovic
357336339a
Proper write of memory data
2022-03-11 11:19:53 +01:00
Miodrag Milanovic
295b0d1899
Start work on memory init
2022-03-09 18:34:02 +01:00
Miodrag Milanovic
f37ac5d934
Fixes and error check
2022-03-09 09:48:29 +01:00
Miodrag Milanovic
ede348cdc2
cleanup
2022-03-07 16:32:32 +01:00
Miodrag Milanovic
1b1ecd4ab0
Error checks for aiger witness
2022-03-07 15:00:14 +01:00
Miodrag Milanovic
b6aca1d743
btor2 witness co-simulation
2022-03-07 13:59:36 +01:00