IEC 62531: Property Specification Language (PSL) for Formal Verification of Digital Circuits

IEC 62531, adopted from IEEE Std 1850, defines the Property Specification Language (PSL), a formal language for specifying properties of digital hardware designs. PSL enables engineers to express complex temporal behaviours and constraints in a precise, unambiguous manner that can be verified through both dynamic simulation and formal verification tools. As integrated circuit designs grow exponentially in complexity, with modern System-on-Chip devices containing billions of transistors and hundreds of clock domains, traditional simulation-only verification approaches have become insufficient to ensure functional correctness. PSL, alongside SystemVerilog Assertions (SVA), provides the foundation for assertion-based verification (ABV) methodologies that have become essential in the semiconductor industry.

PSL Language Architecture and Temporal Logic Foundations

The PSL language is built on a four-layer architecture. The Boolean layer consists of standard Boolean expressions over the design signals, identical to those used in HDL expressions. The Temporal layer provides operators for specifying behaviour over time, built upon Linear Temporal Logic (LTL) extended with Sequential Extended Regular Expressions (SEREs). The Verification layer provides directives such as assert, assume, and cover that tell verification tools what to do with the properties. The Modelling layer allows auxiliary code to support property specification, including functions for computing expected values or configuring verification environments.

The temporal operators are the heart of PSL. The fundamental LTL operators include always (G operator in LTL — globally), never (G with negation), eventually! (F — future), until! (U — strong until), before, and next. These operators are supplemented by clocked variants using the @ operator, which allows properties to be specified relative to specific clock edges. The SERE layer enables regular-expression-like specification of sequential behaviours, with operators including concatenation (;), fusion (:), kleene star ([+] and [*N]), and Boolean intersection (&).

Assertion-Based Verification Methodology and Engineering Practice

PSL supports three verification directives that serve distinct purposes in a verification methodology. The assert directive specifies a property that must always hold; if the property fails during simulation or is found to be false in formal analysis, the tool reports an error. The assume directive specifies a constraint on the design environment — these are assumptions about the inputs that the verification tool must respect, and they enable the verification of internal blocks with constrained input stimuli. The cover directive specifies coverage points that track whether certain behaviours have been exercised during simulation, providing quantitative measurement of verification completeness.

From an engineering methodology perspective, effective PSL usage follows several established patterns. The first is the specification of interface protocol properties: every bus protocol — AXI, AHB, APB, PCI Express, USB — has timing relationships that can be captured as PSL assertions. For example, an AXI valid-ready handshake property in PSL ensures that when valid is asserted, ready must eventually be asserted. These interface properties are reusable across projects and form the basis of a verification IP library. The second pattern is the use of PSL assume directives to constrain formal verification tools, defining the legal input sequences that the design can receive. Without such assumptions, formal tools explore unreachable states, generating false counter-examples that waste engineering time.

Third, PSL cover directives are used to define functional coverage points, complementing code coverage metrics by capturing whether specific behaviours specified by the design intent have been exercised. A typical coverage specification might track all possible arbitration scenarios in a bus arbiter, ensuring that each master has been granted access under varying priority conditions. Industry experience shows that designs with comprehensive PSL assertions achieve 30-50% higher bug-finding rates during verification and 40-60% fewer post-silicon escapes compared to designs relying solely on directed test and code coverage.

Engineering Design Insights for PSL-Based Formal Verification

Deploying PSL effectively in a real-world verification flow requires careful attention to several engineering considerations. First, the property set must be developed as an integral part of the design specification, not as an afterthought added during verification. Writing properties after the RTL is complete tends to reflect the design as implemented rather than the design as intended, reducing the likelihood of finding specification-to-implementation mismatches. Best practice is to capture PSL assertions during the architecture phase, before RTL coding begins, turning the properties into executable specifications that guide implementation.

Second, the complexity of PSL properties significantly affects formal verification tool performance. Highly complex properties with deeply nested temporal operators or long SERE sequences can cause state-space explosion in model checking. Engineers should decompose complex properties into smaller, simpler assertions that are easier to prove. A property such as always (req -> eventually! (ack before [!30])) (request must be acknowledged within 30 cycles) is both intuitive and efficiently verifiable, while a property spanning hundreds of cycles with multiple intervening conditions may require property decomposition or abstraction techniques to be tractable.

Third, the interaction between PSL assume directives and the reset sequence requires careful design. During reset, many design signals are in undefined or transitional states that would violate normal operating assertions. PSL provides the default clock and reset handling constructs to manage these scenarios, typically specifying that assertions are disabled during reset and only become active after a defined reset completion condition. Failure to properly handle reset can result in hundreds of false assertion failures during the reset sequence, overwhelming engineers and obscuring genuine design bugs.