mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-06 22:34:07 +00:00
Code Activity

Update README.md

Browse source
This commit is contained in:
Claire Xen 2021-12-17 15:48:01 +01:00 committed by GitHub
parent 4a07e026dd
commit 7f2c4189dc
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
docs/examples/indinv/README.md
View file

@ -4,7 +4,8 @@ Proving and Using Inductive Invariants for Interval Property Checking
Inductive invariants are boolean functions over the design state, that
1. return true for every reachable state (=invariants), and
2. if they return true for a state then they will also return true
for every state reachable from the given state (=inductive).
for every state reachable from the given state (=inductive)
Formally, inductive invariants are sets of states that are closed under
the state transition function (=inductive), and contain the entire set
of reachable states (=invariants).
@ -67,14 +68,14 @@ first set of states. Let's call the `state != 0` property `p0`:
let p0 = (state != 0);
```
So `state != 0` is a true invariant for our circuit, but it is not an inductive invariant,
because we can go from a state for which `state != 0` is true to a state for
which it is false. Specifically there are two such states for this circuit: 1 and 17
So `p0` is a true invariant for our circuit, but it is not an inductive invariant,
because we can go from a state for which `p0` is true to a state for which it is
false. Specifically there are two such states for this circuit: 1 and 17
(The property `state != 0` is k-inductive for k=4, but for this example we are
only interested in 1-induction.)
(The property `p0` is k-inductive for k=6, but for this example we are
only interested in proofs via 1-induction.)
However, the following property would be inductive, as can be easily confirmed
The following property however would be inductive, as can be easily confirmed
by looking up the 4 states in the state chart above.
```SystemVerilog