Assumption review with the designer of the neighbouring block: is each assumption guaranteed by their RTL?
Property review against the spec, requirement by requirement: is anything missing? Does each property say what the spec says?
Trace review: walk through a few cover traces together. It is the fastest way for a designer to spot a misunderstanding.
Regressions
Practice
Why
Run formal in CI on every RTL change (or nightly for heavy runs)
Catches regressions while the change is fresh
Time budgets per property
A property that suddenly takes 10× longer often signals a real change in the design
Fail on new vacuity or unreachable covers
Prevents silent false positives after RTL changes
Store CEX traces as artefacts
Speeds up debug and makes failures reproducible
Track proven/bounded/failed counts over time
Makes progress and risk visible to the project
formal-ci.yml
# .github/workflows/formal.yml — example CI job for the open-source flow
name: formal
on: [push, pull_request]
jobs:
sby:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Install OSS CAD Suite
uses: YosysHQ/setup-oss-cad-suite@v3
- name: Run all formal jobs
run: |
for f in $(find examples -name '*.sby'); do
(cd $(dirname $f) && sby -f $(basename $f)) || exit 1
done
Was this page helpful?Thanks — noted!
Tip: select any text on the page before clicking Report and it will be quoted in your report.
