Spec PSL

References:

PSL: Property specification language (EDA standard)

  • evovled from Sugar language;
  • adopted as an IEEE standard (1850-2010);
  • grafted onto both SystemVerilog and VHDL;
    • act as an add-on to SystemVerilog/VHDL;
  • Based on CTL/LTL;
  • PSL is divided into four layers:
    • Boolean layer (lowest layer), consists of instantaneous boolean expressions on signals in the design under test;
    • The syntax of this layer follows that of the HDL to which PSL is being applied;
      • Can be verilog, SystemVerilog, VHDL, or others;
      • e.g. a[0:3] & b[0:3] and a(0 to 3) and b(0 to 3) represent the bitwise and of the four most significant bits of vectors a and b in the Verilog and VHDL flavors, respectively.
    • Temporal layer (second layer), allows a designer to state properties that hold across multiple clock cycles.
    • e.g. always !(ena & enb) states that the signals ena and enb will never be true simultaneously in any clock cycle.
      • The always operator, which states that a Boolean expression holds in every clock cycle, is one of the most basic.
    • e.g. always(req -> next ack) states that in every cycle that the req signal is true, the ack signal is true in the next cycle.
      • The next operator, one of the operators that specify delays.
    • e.g. req -> next[2] ack means that ack must be true two cycles after each cycle in which req is true.
      • The -> symbol denotes implication, that is, if the expression to the left is true, that on the right must also be true.
    • e.g. always {req; ack; !cancel} is a syntactic sugar for always (req -> next (ack -> next !cancel)), means that ack must be true after any cycle in which req is true, and cancel must be false in the cycle after that.
    • weak and strong property:
      • weak property can be checked in simulation; i.e., for safety properties;
      • strong property: can only be checked formally; express liveness properties;
      • strong property is marked with a trailing exclamation point !.
      • some operators come in both strong and weak varieties.
      • e.g. always (req -> eventually! ack) states that after req is asserted, ack will always be asserted eventually.
      • eventually! operator illustrates the meaning of strong operators.
      • This is not something that can be checked in simulation: if a particular simulation saw req but did not see ack, it would be incorrect to report that this property failed because running that particular simulation longer might have produced ack.
      • This is the fundamental differences between safety and liveness properties: safety states something bad never happens; liveness states something good eventually happens;
    • Specify a property in which times moves backward.
      • always ((a && next[3] (b)) -> c), states that when a is true and b is true three clock cycles later, c is true in the first cycle when a is true.
    • Verification layer (third layer), instructs a verification tool what tests to perform on a particular design;
    • It amounts to a binding between properties defined with expressions from the Boolean and temporal layer, and modules in the design under test.

    • The following example declares a “verification unit” called ex1a, binds it to the instance named top_block_i1_i2 in the design under test, and declares (the assertion named A1) that the signals ena and enb in that instance are never true simultaneously.

      vunit ex1a(top_block.i1.i2){
    A1: assert never (ena && enb);
}

    • use directives

      • assert,
      • assume, assume a given property;
      • assume_guarantee, both assumes and tests a particular property;
      • restrict, constraints the tool to only consider inputs that have a given property;
      • cover, asks the tool to check whether a certain property was ever observed;
      • fairness, which instructs the tool to only consider paths in which the given property occurs infinitely often, for example, only when the system does not wait indefinitely.

    • Modeling layer (fourth layer): allows Verilog, SystemVerilog, VHDL, or other code to be included inline in a PSL specification.

    • The intention here is to allow addition details about the system under test to be included in the PSL source file.

More

Created Dec 5, 2022 // Last Updated Dec 6, 2022

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?