# Semantics

The semantics of PSL are declarative rather than imperative, meaning that PSL
allows you to describe and reason about an abstract succession of states in
such a way as to be equally applicable for generating simulation checkers, for
formal proof and for documentation. Unlike some other current property
languages, the definition of PSL is not tied to the idea of a checker implemented
as a finite state machine executing in monotonically increasing simulation time.
Indeed, it is possible to write PSL properties that cannot be implemented
efficiently as simulation checkers. Those properties that *can* be implemented as
efficient finite state machine automata are said to belong to the *simple subset* of
PSL. Most practical properties fall in the simple subset.

The semantics of the temporal layer are defined by considering all possible paths through all possible states of a design. A PSL property is said to hold in a particular cycle if it matches (depending on the meaning of the temporal operator in question) a path starting with the current cycle and extending a finite or infinite number of cycles into the future. In other words, to see if a particular property holds, you should choose a particular cycle to start from and then peer forward into the future, comparing the actual state of the design with the obligations imposed by the temporal operators. For a typical PSL property (i.e. one that uses the always operator), this rule applies equally and independently for every cycle.

The semantics of SEREs is defined somewhat differently by considering the set
of all possible sequences that can be generated from a particular SERE. For
example, the SERE {a[+]} generates the sequences {a}, {a;a}, {a;a;a},...
A SERE is said to *hold tightly* on a finite path if the sequence of states that
constitute that path belongs to the set of sequences generated by the SERE. In
other words, a SERE that matches a particular finite sequence of states is said
to *hold tightly* over that path, whereas a property is said to *hold* in a particular
cycle if it matches a finite or infinite sequence of states, looking forward in time
starting from that cycle.

### More PSL?

Learn more about PSL and using PSL to improve your verification process. Consider attending Assertion-Based Verification with PSL. Or, if you are ready to learn some advanced VHDL or Verilog then consider the new improved Expert VHDL or Expert Verilog classes now including PSL.