mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-14 17:28:44 +00:00
30 lines
1.2 KiB
Markdown
30 lines
1.2 KiB
Markdown
A simple example for using abstractions
|
|
=======================================
|
|
|
|
Consider the design in `demo.v` and the properties in `props.sv`. Obviously the
|
|
properties are true, but that is hard to prove because it would take thousands of
|
|
cycles to get from the activation of one output signal to the next.
|
|
|
|
This can be solved by replacing counter with the abstraction in `abstr.sv`.
|
|
|
|
In order to do this we must first prove that the abstraction is correct. This is
|
|
done with `sby -f abstr.sby`.
|
|
|
|
Then we apply the abstraction by assuming what we have just proven and otherwise
|
|
turn `counter` into a cutpoint. See `props.sby` for details.
|
|
|
|
Running `sby -f props.sby prv` proves the properties and `sby -f props.sby cvr`
|
|
produces a cover trace that shows the abstraction in action.
|
|
|
|
Suggested exercises:
|
|
|
|
- Make modifications to `abstr.sv` and/or `demo.v`. Make a prediction if the
|
|
change will make `sby -f abstr.sby` or `sby -f props.sby prv` fail and test your
|
|
prediction.
|
|
|
|
- What happens if we remove `abstr.sv` from `props.sby`, but leave the `cutpoint`
|
|
command in place?
|
|
|
|
- What happens if we remove the `cutpoint` command from `props.sby`, but leave
|
|
`abstr.sv` in place?
|