- Boolean layer
- Temporal layer
- Verification layer
- Modelling layer

- From VHDL:
- a and b
- a or b
- not a
- a=b

- More logical operators:
- a->b
- a<->b

- always p
- never p
- next p
- p until q
- p before q
- eventually! p

- next[i] p
- next_a[i to j] p
- next_e[i to j] p
- next_event(b) p
- next_event_a(b)[i to j] p
- next_event_e(b)[i to j] p

- p until q
- p until! q
- p until_ q
- p until!_ q
- p before q
- p before_ q
- p before! q
- p before!_ q

- assert p
- assume p
- See also the short intro to Jasper Gold and the PSL Reference Guide.

- assert always req -> next (ack before req)
- assert always req -> (ack before req)

- Foundation Language (FL)
- Based on
**Linear Temporal Logic (LTL)** - Useful for expressing properties of a trace (a linear sequence of states)
- Can be used both with simulation and formal verification

- Based on
- Optional Branching Extension (OBE)
- Based on
**Computation Tree Logic (CTL)** - Can express properties about the different ways in which a system can behave
- Useful for Formal Verification

- Based on

- Propositional Logic
- We can states properties about the current values of boolean variables
- not (a and b)
- a -> b

- We can states properties about the current values of boolean variables
- What about Time?
- Think of a signal as a sequence of values that vary over time
- a = a
_{0}, a_{1}, a_{2}, a_{3}, ...

- a = a
- We can then write e.g.
a
_{0}-> b_{1}and a a_{t}-> b_{t+1}

- Think of a signal as a sequence of values that vary over time

`always not (a and b)`

⇔ (∀t) not (a_{t}and a_{t})`always a -> next b`

⇔ (∀t) a_{t}-> b_{t+1}`eventually! a`

⇔ (∃t) a_{t}

- Good
- Powerful
- Well established

- Bad
- Undecidable (= no automatic verification tools)

- Good
- Decidable (automatic formal verification is possible)

- Bad
- Not as powerful as predicate logic

- It is a logic for stating properties of
*linear sequences of states*. - A (potentially infinite) sequence is also called a
*path*.- π = s
_{0}, s_{1}, s_{2}, s_{3}, ...

- π = s
- A path starts in a particular state and extends to the end of time.
- A path is identified by the state it starts in.
- When we say that a formula is true in a particular state, we mean
that it is true for the path that starts in that state.
- π ⊨ p
- s ⊨ p

- Basic Operators (there is only two!)
- X p
- p U q

- Compared to PSL
- X p = next! p
- p U q = p until! q

π ⊨ X p **if**tail π ⊨ p- Assuming
- π = s
_{0}, s_{1}, ... - tail π = s
_{1}, s_{2}, ... - drop k π = s
_{k}, s_{k+1}, ...

- π ⊨ p U q
**if**for some k: - drop k π ⊨ q
- drop j π ⊨ p,
**for all**j<k

- Note:
- p U q requires a cycle where q is true
- Possible traces: q..., pq..., ppq..., pppq..., ppppq..., ...
- SERE: {p[*];q}

- Two derived operators
- F p = true U p (finally, future)
- G p = ¬ F (¬p) (globally)

- Compared to PSL
- F p = eventually! p
- G p = always p

- The formal semantics in PSL reference manual makes use of a translation to LTL.
- For example, we have seen that
- p until! q = p U q
- always p = G p
- next! p = X p
- eventually! p = F p

- The translation gives a meaning to the operators and shows how they are related.

- The PSL reference manual uses both X and X! and defines
- X p = ¬ X! (¬p)
- next p = X p
- next! p = X! p

- LTL has only X
- next! p = X p

- never p = always (not p) = G (¬p) = ¬(F¬¬p)

= ¬(Fp) = not (eventually! p) - not (always p) = ¬(G p) = ¬¬(F ¬p)

= F ¬p = eventually! (not p)

p until q = (p U q) ∨ G p = (p until! q) or always p - p until_ q = p until (p and q)
- p until!_ q = p until! (p and q)

- p before!_ q = (not q) until! p
p before_ q = (not q) until p = ((not q) until! p) or always (not q) = (p before!_ q) or never q

- p before! q = (not q) until! (p and not q)
p before q = (not q) until (p and not q) = ((not q) until! (p and not q)) or always (not q) = (p before! q) or never q

`ack before req`

=`(ack before! req) or never req`

- Consider a cycle where req is true...
`never req`

is false, so`ack before! req`

has to be true`ack before! req`

=`(not req) until! (ack and not req)`

`not req`

is false, so`ack and not req`

has to be true- but
`ack and not req`

=`ack and false`

=`false`

! - so
`ack before req`

is false - so
`req -> ack before req`

is false

- We can conlude that
- always req -> (ack before req)

- requires
- always not req

- LTL is a logic for stating properies of paths (linear sequences of states)
- Every state has
*one*unique next state. - A path is identified by the state it starts in.

- Every state has
**But**we want to state properties of circuits!- In each state, the next state depends on the input (typically).
- Instead of a linear sequence, there is a branching structure.
- Each state becomes a node in a tree. Many different paths start in each state.
- We can still talk about properties of paths, but we need to make it clear which paths we are talking about.