3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-07 22:55:18 +00:00
sby/docs/examples/abstract
Clifford Wolf 5ef5187673 Add docs/examples/abstract/.gitignore
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-18 10:31:55 +02:00
..
.gitignore Add docs/examples/abstract/.gitignore 2019-06-18 10:31:55 +02:00
abstr.sby Add docs/examples/abstract 2019-03-27 14:45:30 +01:00
abstr.sv Minor improvements in docs/examples/abstract/abstr.sv 2019-03-27 14:49:35 +01:00
demo.v Add docs/examples/abstract 2019-03-27 14:45:30 +01:00
props.sby Add docs/examples/abstract 2019-03-27 14:45:30 +01:00
props.sv Add docs/examples/abstract 2019-03-27 14:45:30 +01:00
README.md Add docs/examples/abstract 2019-03-27 14:45:30 +01:00

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 abstriction 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?