Page 1

Page 2

# PSL recap

## Four layers

• Boolean layer
• Temporal layer
• Verification layer
• Modelling layer
Page 3

## Boolean layer

### Boolean operators from the HDL language

• From VHDL:
• a and b
• a or b
• not a
• a=b
• More logical operators:
• a->b
• a<->b
Page 4

## Temporal layer

• always p
• never p
• next p
• p until q
• p before q
• eventually! p
Page 5

### Next

• 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
Page 6

• p until q
• p until! q
• p until_ q
• p until!_ q
• p before q
• p before_ q
• p before! q
• p before!_ q
Page 7

Page 8

# The meaning of PSL

## Examples from last week

• assert always req -> next (ack before req)
• assert always req -> (ack before req)
Page 9

## What is the meaning of all the temporal operators in PSL?

• 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
• 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
Page 10

# Propositions involving time?

• Propositional Logic
• We can states properties about the current values of boolean variables
• not (a and b)
• a -> b
• Think of a signal as a sequence of values that vary over time
• a = a0, a1, a2, a3, ...
• We can then write e.g. a0 -> b1  and a at -> bt+1
Page 11

# Temporal Operators

## Can be explained as syntactic sugar for predicate logic

• `always not (a and b)` ⇔ (∀t) not (at and at)
• `always a -> next b` ⇔ (∀t) at -> bt+1
• `eventually! a` ⇔ (∃t) at
Page 12

# Predicate Logic

• Good
• Powerful
• Well established
• Undecidable (= no automatic verification tools)
Page 13

# Temporal Logic

• Good
• Decidable (automatic formal verification is possible)
• Not as powerful as predicate logic
Page 14

# Linear Temporal Logic (LTL)

## What is it?

• It is a logic for stating properties of linear sequences of states.
• A (potentially infinite) sequence is also called a path.
• π = s0, s1, s2, s3, ...
• 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
Page 15

# Temporal Operators in LTL

• Basic Operators (there is only two!)
• X p
• p U q
• Compared to PSL
• X p = next! p
• p U q = p until! q
Page 16

## Meaning

•  π ⊨ X p  if tail π ⊨ p Assuming π = s0, s1, ... tail π = s1, s2, ... drop k π = sk, sk+1, ... π ⊨ p U q  if for some k: drop k π ⊨ q drop j π ⊨ p, for all j
• Note:
• p U q requires a cycle where q is true
• Possible traces: q..., pq..., ppq..., pppq..., ppppq..., ...
• SERE: {p[*];q}
Page 17

# Derived Operators in LTL

• 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
Page 18

Page 19

# The meaning of PSL

• 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.
Page 20

# Next? Next!

• 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
Page 21

# The meaning of PSL

## always, never and eventually!

• 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)
Page 22

## Weak, strong and overlapping until

•  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)
Page 23

## before_ and until

• 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
Page 24

## before and until

• 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
Page 25

# Back to the example from last week

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

• `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
Page 26
##### Back to the example from last week
• We can conlude that
• always req -> (ack before req)
• requires
• always not req
Page 27

# Summary

• 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.
• 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.
Page 28