PSL Property Specification Language Jasper Design Automation Jasper

PSL Property Specification Language Jasper Design Automation Jasper

PSL Property Specification Language Jasper Design Automation Jasper Design Automation 2005 1 Introduction to PSL Jasper Design Automation 2005 2 Introduction What is PSL? o A language for the formal specification of concurrent systems Particularly applicable for the description of hardware designs Describe properties (or assertions) that are required to hold on a DUV

Key characteristics of PSL include: o Mathematically precise well-defined formal semantics o Very expressive coving large class of real world design behaviors o Known efficient underlying verification algorithms o Intuitive and easy to learn, read, and write o PSL is a layered language, ideal for reuse, and supports multiple HDL flavors Verilog, VHDL, SystemC, and SystemVerilog Jasper Design Automation 2005 3

Background Sugar created at IBM Haifa Research Labs 1994 Syntactic sugaring of CTL FVTC formed in Accellera (OVI) 1998 Branching-time semantics plus regular expressions Jasper Design Automation 2005 FVTC considers: Temporal e

PSL CBV based on ForSpec Sugar 2.0 Sugar 2001 Linear-time semantics Added to Sugar 2002 PSL 1.01 Approved 2003 PSL and SVA alignment 4 PSL 1.1 Approved

IEEE 1850 PSL 2004 2005 PSL enhancements and clarifications Elements of an assertion language Logic, whose origins date back to the Greek philosophers, allows us to answer the question: Does a given model satisfy a given property? model logic property Jasper Design Automation 2005 5

true/false Elements of assertion languages Classical logic deals with timeless statements. o The moon is a satellite of the earth. o The moon is rising (now). universe logic true/false The moon is rising However, in classical logic, we cannot express: o The moon will rise again and again

Jasper Design Automation 2005 6 Temporal Logic Our interest properties of reactive systems. In reactive systems, processes maintain on-going interaction with their environment. Interesting statements about reactive systems depend on time. o For example, A and B are mutually exclusive for all values of time Temporal logic can describe the ordering of events in time without introducing time explicitly.

o Without temporal logic, we would be forced to explicitly write equations involving time: For example, Jasper Design Automation 2005 t.!(A(t) & B(t)) 7 Temporal Logic Pnueli 1977 use of temporal logic for reasoning about reactive systems (LTL). Clarke & Emerson 1981 model checking (CTL). Various temporal logics (LTL, CTL, CTL*,). The logics differ in o o o o o Syntax

Semantics meaning of the formulas. Expressiveness which properties can be expressed. Complexity efficiency of evaluating a property. Underlying model of time. Jasper Design Automation 2005 8 Temporal Logic Model of time: o Finite computation (simulation) or infinite computation (model checking). o Linear or branching Linear each moment in time has a unique possible future. Branching each moment in time can split into various possible futures. p 1 3

1 q 2 2 3 2 1 2 2 3 2 2 1 2 2 2 2 Jasper Design Automation 2005

9 PSL Linear-Time Temporal Logic Intuitive to engineers o Reason about expected behavior over linear sequences of states (computational paths) o Thinking is similar to reviewing a simulation trace Properties evaluated over paths p 0 2 Jasper Design Automation 2005 Infinite path

q 1 0 2 1 10 What We can Express in LTL All Boolean logic properties. Process 2 is in the critical section next p p holds in the next state. Process 2 will be in the critical section in the next state eventually! p eventually p holds. eventually process 2 will enter the critical section Jasper Design Automation 2005 11

What We Cannot Express in LTL? Counting example: p is asserted in every even cycle All the following traces satisfy this property !p,p,!p,p, p,p,p,p,. p,p,!p,p,p,p No linear-time temporal formula can express this property. Jasper Design Automation 2005 12 Extended Regular Expressions Extended regular expressions overcome some of the limitations in linear-time temporal logics lack of expressiveness. They are a convenient way to define a temporal pattern that can match (or more aptly put, specify) sequences of states. Regular expressions let us describe design behavior that involves counting. o

Such as modulo n type behavior, with the * operator. For example, the PSL extended regular expression: {a ; b ; [*3] ; c ; [*2:3] ; d} Jasper Design Automation 2005 13 What Cannot be Express with Regular Expressions The property: eventually p holds forever The following property cannot be expressed with regular expressions: o Eventually, p holds forever p! p! p!

p p p Can be expressed in LTL. For example, in PSL: o eventually always p Jasper Design Automation 2005 14 What We Can Express in LTL and CTL Always if req is received, then ack must be received sometime in the future o LTL: G (req -> F ack)

o CTL: AG(req -> AF ack) Most useful properties are in the common fragment of LTL and CTL (Maidl, 2000). Jasper Design Automation 2005 15 PSL Layers Jasper Design Automation 2005 16 PSL is a Layered Language Modeling Verification Temporal Boolean

Jasper Design Automation 2005 17 Boolean Layer The Boolean layer is used to: o Specify logic expressions without specific timing information using a standard HDL syntax such as Verilog-HDL and VHDL Example (Verilog): // A and B are mutually exclusive ( !(A & B) ) Example (VHDL): -- A and B are mutually exclusive ( not (A and B) ) Jasper Design Automation 2005 18 Temporal Layer The temporal layer is used to:

o Specify when the Boolean expression must be valid o Remove time ambiguities Example: // A and B are always mutually exclusive always ( !(A & B) ) There are many temporal operators: o always property o until property o never property o

o next property Jasper Design Automation 2005 19 Verification Layer The verification layer is used to: o Specify how to use the property: Assertion to be verified against the implementation Assumption to be used as constraint during the verification Or functional coverage metric to improve the overall verification coverage Example: // A and B must always be mutually exclusive assert always ( !(A & B) ) ; Jasper Design Automation 2005

20 Modeling Layer The modeling layer is used to: o Write auxiliary HDL code required to specify complex properties You can define HDL functions that are used in your properties, model complex FSMs or expressions Example: // If req is asserted, ack must be asserted the next cycle wire req; assign req = readA_req || readB_req; assert always (req -> next (ack && gnt)) ; Jasper Design Automation 2005 21 PSL Layers wire req; assign req = readA_req || readB_req;

assert always (req -> next (ack && gnt)) ; Boolean layer Temporal layer Verification layer Modeling layer Jasper Design Automation 2005 22 PSL Sequences Jasper Design Automation 2005 23 PSL Sequences PSL sequences enable us to: o Describe a sequence of Boolean expression (that is, states) PSL sequences are marked by curly braces { and } Advancement of time occurs with each concatenation operator ; Example:

{ req; busy; gnt } Jasper Design Automation 2005 24 PSL Sequences Matching A PSL sequence can have multiple matching diagrams Example: { req; busy; gnt } req req busy busy gnt gnt This diagram represents one possible match

This diagram represents another possible match To explicitly match the waveform, we would need to specify the following Example: { req && !busy && !gnt ; !req && busy && !gnt ; !req && !busy && gnt } req busy gnt Jasper Design Automation 2005 25 Temporal Operators for Sequences PSL supports the following temporal operators for sequences: o Overlapping implication |->

o Non-overlapping implication |=> Example(s): sequence S1 = { req; ack } ; sequence S2 = { start; busy; end } ; // Event start occurs on the same clock cycle as ack property P1 = always S1 |-> S2 ; // Event start occurs on the next clock cycle after ack property P2 = always S1 |=> S2 ; Jasper Design Automation 2005 26 Operators for SERE PSL supports the following operators for SERE: o Repetition in n consecutive clock cycles [*n]

o Repetition in n non-consecutive clock cycles [=n] o Repetition in n non-consecutive clock cycles [->n] o Repetition for 0 or any number of clock cycles [*] o Repetition for 1 or any number of clock cycles [+] o

Repetition for n to m clock clock cycles [*n:m] The number of repetitions must be a positive integer Keyword inf stands for an infinite number of clock cycles Example(s): sequence S1 = { rd[*5] } ; sequence S2 = { rd[->3] } |=> { wr } ; // {!rd[*]; rd; !rd[*]; rd; !rd[*]; rd} sequence S3 = { req} |=> { ack[=1]; done} ; // {!ack[*]; ack; !ack[*]} sequence S4 = { rd[*]; rd; wr }; sequence S5 = { rd[+]; wr } ; sequence S6 = { rd[*2:5] } |=> { wr } ; Jasper Design Automation 2005 27 Example property P1 = { req[+]; ack; wr[*4] } |=> { (wait && !req)[*]; done } ; assert always P1; clock

req 1 or more 0 or more ack write wait 0 or more done Jasper Design Automation 2005 28 Example Properties are Derived from Specification Receiving Data: When the reception of data is complete, then an interrupt should occur: property done_rcving_implies_int = always rose(done_rcving) -> rose(int) ;

assert done_rcving_implies_int ; Jasper Design Automation 2005 29 Example Properties are Derived from Specification Receiving Data: If the signal that indicates a reception in progress is active, then it should remain active until the reception is complete: property rcving_until_done_rcving = always rose(rcving) -> (rcving until done_rcving) ; assert rcving_until_done_rcving ; Jasper Design Automation 2005 30 Example RTL Implementation Queue Design intent oIf Queue is full, then an attempt to insert data is ignored. (Overflow)

oIf Queue is empty, then an attempt to remove data is ignored. (Underflow) qDataIn RTL implementation fragment: function [3:0] qNext; input [3:0] p; qNext = ((p + 1) mod `qSize); endfunction; assign qFull = (qNext(qLast) == qFirst); qLast 7 6 5 4 3 2 1 0 cntrl assign qEmpty = (qLast == qFirst);

PSL implementation assertions: qFirst qDataOut assert always (qFull && qInsert -> next !qEmpty) abort ~rstN ; assert always (qEmpty && qRemove -> next !qFull) abort ~rstN; Jasper Design Automation 2005 31 qInsert qRemove qError qEmpty qFull Verification Units for Grouping Properties and Directives Verification with PSL is based on using verification units vunit [()] {

}; Usually a separate file from RTL Example: vunit inputs vunit my_unit (my_module) { default clock = posedge clk; outputs RTL module A vunit binds to a module or an instance assume never read & write; property P1 = never (full & write); assert P1; assert always (read -> ! empty); }; Jasper Design Automation 2005 32

Types of Assertions and PSL Expressiveness Data Integrity High-level requirements End-to-end Black box Based on design intent Generally require modeling+assertions Packet Ordering Design Intent RTL Implementation RTL implementation assertions Localized Implementation-specific Generally can be expressed using only assertions One Hot

Increment By 1 FIFO Overflow FIFO Overflow Design Behavior Jasper Design Automation 2005 33 To learn more Accellera v1.1 LRM available at My email: Jasper Design Automation 2005 [email protected] 34

Recently Viewed Presentations

  • poetry -

    poetry -

    Rupi Kaur. Born October 5, 1992. From Canada. Published two poetry books. Milk and Honey. The Sun and Her Flowers. Utilized visual poetry. Social media had a huge impact on Kaur's career. Spoken poetry. Poetry Slams. Spoken Word Nights. Open...


    Fire and EMS are now deploying into "Warm Zones" established by Law Enforcement in order to provide interventions for life threatening injuries: Post event reviews find that many fatalities had survivable injuries if there had been earlier intervention by EMS.
  • Schema Refinement and Normalization

    Schema Refinement and Normalization

    Boyce-Codd Normal Form (BCNF) Reln R with FDs F is in BCNF if, for all X A in F+ A X (called a trivial FD), or X is a superkey for R. In other words: "R is in BCNF if...
  • Microbial Source Tracking Techniques: Lake Michigan Beaches Case

    Microbial Source Tracking Techniques: Lake Michigan Beaches Case

    Microbial Source Tracking Techniques: Lake Michigan Beaches Case Studies Erika Jensen, M.S. Great Lakes WATER Institute April 14, 2005 Spatial surveys provide the most useful data Identify hot spots or areas of concern Implement targeted sampling surveys to observe site...
  • All My Sons - Miss Ross

    All My Sons - Miss Ross

    All My Sons. Setting and Symbolism. Setting: Place. The entire play takes place the Keller's back yard. This is important as it is a semi-public private space: it is essentially private property, but in the USA it is culturally thought...
  • 5 -

    5 -

    A boil is a localized infection in the skin that generally starts as a reddened, tender area. Over time, the area becomes firm, hard, and tender. Eventually, the center of the boil softens and becomes filled with infection-fighting white blood...
  • What is new in BizTalk?

    What is new in BizTalk?

    BizTalk releases in 2013. BizTalk Server 2013 has RTM'd. BizTalk Server on Windows Azure Virtual Machines has reached GA. Upcoming BizTalk PaaS offering (think EAI/EDI Labs) Enabling hybrid applications with BizTalk . Develop, Deploy, Scale, Manage, Monitor. Continue to bet...
  • Marine Sedimentation - Suffolk City Public Schools

    Marine Sedimentation - Suffolk City Public Schools

    Deep-sea Sedimentation has 4 main sources for sediment: terrigenous material from the land (found mostly on the shelf), biogenous and hydrogenous from the sea, and volcanic from mid-ocean ridges and other active sites. Major pelagic (open ocean) sediments in the...