3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-05-13 02:34:44 +00:00
Commit graph

3 commits

Author SHA1 Message Date
George Rennie
dfa8453102 tests: remove -seq 1 from sat with -tempinduct where possible
* When used with -tempinduct mode, -seq <N> causes assertions to be
  ignored in the first N steps. While this has uses for reset modelling,
  for these test cases it is unnecessary and could lead to failures
  slipping through uncaught
2024-10-03 16:39:17 +02:00
Jannis Harder
331ac5285f tests: Run async2sync before sat and/or sim to handle $check cells
Right now neither `sat` nor `sim` have support for the `$check` cell.
For formal verification it is a good idea to always run either
async2sync or clk2fflogic which will (in a future commit) lower `$check`
to `$assert`, etc.

While `sim` should eventually support `$check` directly, using
`async2sync` is ok for the current tests that use `sim`, so this commit
also runs `async2sync` before running sim on designs containing
assertions.
2024-02-01 16:14:11 +01:00
Zachary Snow
640b9927fa sv: allow globals in one file to depend on globals in another
This defers the simplification of globals so that globals in one file
may depend on globals in other files. Adds a simplify() call downstream
because globals are appended at the end.
2021-03-12 11:22:41 -05:00