yosys

Commit Graph

Author	SHA1	Message	Date
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

Author

SHA1

Message

Date

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

2 Commits