sby/docs/examples/abstract

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?