3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-12 16:28:17 +00:00
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
This commit is contained in:
Claire Wolf 2020-04-03 15:18:52 +02:00
parent 1c92dff6ed
commit d18656084c

View file

@ -10,7 +10,7 @@ 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 In order to do this we must first prove that the abstraction is correct. This is
done with `sby -f abstr.sby`. done with `sby -f abstr.sby`.
Then we apply the abstriction by assuming what we have just proven and otherwise Then we apply the abstraction by assuming what we have just proven and otherwise
turn `counter` into a cutpoint. See `props.sby` for details. 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` Running `sby -f props.sby prv` proves the properties and `sby -f props.sby cvr`