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.