A Practical Introduction to PSL

PSL comments are flavor dependent. For each flavor, the comment capability is consistent with that provided by the corresponding HDL environment. For the SystemC, SystemVerilog, and Verilog flavors, both the block comment style ( /* ....*/) and the trailing comment style ( // ....< eol>) are supported. For the VHDL flavor, the trailing comment style ( -- ....< eol>) is supported. For the GDL flavor, both the block comment style ( /* ....*/) and the trailing comment style ( -- ....< eol>) are supported.
PSL provides a way to gives names to properties and to SEREs which can then be instantiated. For example, Figure 8.1 declares a property named getgrant and instantiates it twice. Property getgrant takes four parameters: a Boolean expression req, a numeric expression n, and two additional Boolean expressions gnt and clk. The two instantiations of getgrant shown in Figure 8.1 are equivalent to the two assertions shown in Figure 8.2.
Figure 8.3 shows the declaration and instantiation of two named SEREs. A named SERE is introduced by the keyword sequence. The instantiations of named SEREs reqseq and dataseq in Figure 8.3 result in an assertion equivalent to that of Figure 8.4.