Page 1

PSL and Temporal Logic

Hardware Description and Verification

Thomas Hallgren

2010-03-23

Page 2

PSL recap

Four layers

Page 3
PSL recap

Boolean layer

Boolean operators from the HDL language

Page 4
PSL recap

Temporal layer

Page 5
PSL recap → Temporal layer

Lots of variants

Next

Page 6
PSL recap → Temporal layer → Lots of variants

Until and Before

Page 7
PSL recap

Verification layer

Page 8

The meaning of PSL

Examples from last week

Page 9
The meaning of PSL

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

Page 10

Propositions involving time?

Page 11

Temporal Operators

Can be explained as syntactic sugar for predicate logic

Page 12

Predicate Logic

Page 13

Temporal Logic

Page 14

Linear Temporal Logic (LTL)

What is it?

Page 15

Temporal Operators in LTL

Page 16
Temporal Operators in LTL

Meaning

Page 17

Derived Operators in LTL

Page 18

Temporal Operators in LTL illustrated

Page 19

The meaning of PSL

Page 20

Next? Next!

Page 21

The meaning of PSL

always, never and eventually!

Page 22
The meaning of PSL

Weak, strong and overlapping until

Page 23
The meaning of PSL

before_ and until

Page 24
The meaning of PSL

before and until

Page 25

Back to the example from last week

assert always req -> (ack before req)

Page 26
Back to the example from last week
Page 27

Summary

Page 28

Next step: Computation Tree Logic (CTL)

See Mary Sheeran's slides from 2008