PSLCourse

Property Specification Language: 

Property Specification Language Roderick Bloem (TU Graz) Based on material by: Cindy Eisner (IBM Haifa Research Labs) Dana Fisman (Weizmann Institute of Science) Avigail Orni (IBM Haifa Research Labs) Sitvanit Ruah (IBM Haifa Research Labs)

Contents: 

Contents Some History Boolean Layer Formulas SEREs Plenty of examples, one exercise

Formal Specification: 

Formal Specification Property Specification Language (PSL) is Easy to read and write Mathematically precise What does this mean: every request must remain asserted until a grant is received? Which signals are meant? What does “until” mean? … In English, properties are imprecise, or long and hard to understand, or both

Property Specification Language: 

Property Specification Language PSL: Property Specification Language. Intended to specify temporal properties of hardware Based on Sugar Initially a nice way to write Computation Tree Logic Extended to regular expressions Changed to Linear Time Logic Incorporates 10 years of IBM experience in property-based verification A rich language with many ways to express any property 2005: IEEE Standard P1850

Uses of PSL: 

Uses of PSL For documentation As input to a formal verification tool Model checker Theorem prover As input for a testing tool Assertion-based verification (ABV)

The structure of PSL: 

The structure of PSL Modeling layer Temporal layer Verification layer Boolean layer Sugar comes in multiple flavors/dialects: Verilog, VHDL, … vunit example { wire req; assign req = read_req | write_req ; assert always (req -> next (ack | abort)) ; }

The structure of PSL –the Temporal Layer: 

LTL G F X The structure of PSL – the Temporal Layer CTL

Boolean Layer: 

Boolean Layer We’ll assume Verilog flavor Boolean Expression states something about one cycle (ack | abort) !(ack1 & ack2) req  ack But what is your system is not combinational?

Sequential Systems: 

Sequential Systems We will assume a synchronous, one-clock system PSL can handle multiple clocks & asynchronous systems Behavior of a system is described as waveform assert, I can states that something is true for all waveforms

Basic Temporal Operators: 

Basic Temporal Operators always never next eventually! until before

always & never: 

always & never always !(gnt1 & gnt2) Compare with !(gnt1 & gnt2) This means that we do not have both grants in the first cycle never (gnt1 & gnt2)

next: 

next always(req  next gnt) OK X X OK OK OK

next: 

next next[2] = next next always(req  next[4] gnt) next_e[i..j] ack ack occurs between i and j cycles in the future (inclusive i, j) next_a[i..j] ack ack occurs from now + i cycles until now + j cycles (inclusive)

eventually!: 

eventually! always(req  eventually! gnt) Every request must eventually be followed by a gnt. The bang (!) means that the operator is strong: you may not wait forever!

until: 

until always( req  next (busy until gnt) ) gnt may or may not come (weak operator) busy must hold upto cycle before gnt always( req  next (busy until! gnt) ) gnt must come (strong operator) always( req  next (busy until_ gnt) ) busy must hold in the cycle that gnt occurs, if gnt occurs always( req  next (busy until_! gnt) ) busy must hold in the cycle that gnt occurs, and gnt must occur

weak and strong,inclusive and exclusive: 

weak and strong, inclusive and exclusive req  next (busy ??? gnt) until OK until! OK until_ X until_! X until OK until! X until_ OK until_! X until OK until! OK until_ X until_! X until OK until! OK until_ OK until_! OK

Rationale for Weak & Strong: 

Rationale for Weak & Strong Different semantics may be needed Is grant mandatory? Without formal verification, there is no way to falsify a strong operator! If grant does not come, have we not waited long enough, or is there a bug? Consider “bounded liveness”: next_e[1..4] grant Cf. “I will give you your money eventually!”

until!: 

until! What is the simplest system that satisfies always( req  next (busy until! gnt) )?

Tricky Things: 

Tricky Things always((next ack)  req) At any cycle, if there is an ack in the next tick, there is a req in the present tick Every ack must be preceded by a request Stating that a signal is 1 at some cycle does not require that it is 0 at other cycles An implication does not require that the left side is ever true the right hand side is ever false

before: 

before always(req  next (ack before req)) No two reqs without intervening ack req may not come simultaneously with ack (must be before) ack may never come What is the difference with always(req  (ack before req))? We also have before_ (ack and req may be simultaneous), before! (ack must appear), and before_! (both)

Exercise: Putting it All Together: 

Exercise: Putting it All Together Specify an arbiter Possible properties No simultaneous acks Every req is acknowledged

Sequential Extended Regular Expressions: 

Sequential Extended Regular Expressions The following is cumbersome: always (reqin  next(ackout  next(!abortin  (ackin & next ackin)))) Sequences appear frequently. Sequential Extended Regular Expressions (SEREs) make writing sequences easy.

SEREs: 

SEREs String signals together with a semicolon: {reqin; ackout; !abortin} Note: You can use the Boolean layer inside SEREs You can use SEREs in formulas You cannot use formulas in SEREs SEREs are built using braces {} instead of brackets ().

Weak Suffix Implication: 

Weak Suffix Implication always({reqin; ackout; !abortin} |-> {ackin; ackin}) Whenever we see reqin followed by ackout followed by !abortin, we get two ackins. Note: Overlap: ackin and !abortin are simultaneous. Compare to always(reqin & next(ackout & next !abortin))  (ackin & (next ackin))) In the latter case, the first ackin coincides with reqin With |->, the second sequence starts when the first has completed.

SEREs: repetition [*i..j]: 

SEREs: repetition [*i..j] always ({req;ack} |=> {start_trans;data[*1..8];end_trans}) |=> is like |-> without overlap data[*1..8] means that data is asserted between 1 and 8 consecutive cycles. Not consecutive: always ({req;ack} |=> {start_trans;data[=1..8];end_trans})

Repetition: 

Repetition {req;ack} |=>{start_trans;data[*1..8];end_trans} {req;ack} |=> {start_trans;data[=1..8]; end_trans}

Strong & Weak Suffix Implication: 

Strong & Weak Suffix Implication always {req;ack} |=> {start;data[*];end} does not require end to occur! always {req;ack} |=> {start;data[*];end} ! requires end to occur.

forall: 

forall Suppose we have an arbiter with 7 clients forall i in 1..7: always(req == i  eventually! ack == i) req = 0 means no requests.

next_event: 

next_event forall i in 1..7: always(req == i  nextevent_(ack)(dest == i)) Whenever there is a request from client i, the next ack is for client i. Does not require ack to occur (guess how to change that!) forall i in 1..7: always(req == i  nextevent_[2](ack)(dest == i)) The next 2 acks must be to i.

abort: 

abort always(start  ( (always (req  eventually! ack)) abort interrupt ) ) Any request must be acknowledged, unless interrupted.

The structure of PSL: 

The structure of PSL Modeling layer Temporal layer Verification layer Boolean layer Sugar comes in multiple flavors/dialects: Verilog, VHDL, … vunit example { wire req; assign req = read_req | write_req ; assert always (req -> next (ack | abort)) ; }

Verification Layer: 

Verification Layer The verification layer tells your tool what to do with the properties assume formula assume that the property holds assert formula assert that the property holds cover SERE Make sure that the simulator has seen a trace satisfying SERE vunit arb{ assume always (req1  next(ack1 before req1)); assume always (req2  next(ack2 before req2)); assert always (req1  eventually! ack1 ) assert always (req2  eventually! ack2 ) assert never(req1 & req2) }

Modeling Layer: 

Modeling Layer The modeling layer allows you to use Verilog in your properties vunit arb{ wire illegal_ack; assign illegal_ack = ack1 & ack2; … assert never(illegal_ack) }

Named Properties: 

Named Properties Suppose you have an initialization sequence At least 5 ticks, maybe longer If longer than five ticks, you can tell because done is 0. You want three properties to hold after initialization, for instance always(r1 -> a1) always(r2 -> a2) never(a1 & a2) Here is how you do it without retyping the initialization sequence three times property AfterInitial(property condition) = {true[5];{done=0}*;{done=1}}(condition); assert AfterInitial(always(r1 -> a1)); assert AfterInitial(always(r2 -> a2)); assert AfterInitial(never(a1 & a2));

Another Exercise: 

Another Exercise Take the specification of the arbiter by another group Try to construct an arbiter that is “wrong,” but still adheres to the spec Correct possible mistakes Write the spec using the verification layer Alternative: Specifying a 3-bit counter. The counter has up and down inputs, output ready. The counter has an initialization phase. It will be done after 3 ticks or when the output ready goes high, whichever occurs first. The counter will be in the reset state after the end of the initialization phase, and will only start responding to the inputs afterwards.

More Info: 

More Info The PSL Home Page: http://www.haifa.ibm.com/projects/verification/sugar Language Reference Manual List of Tools Tutorial EETimes www.eedesign.com/features/exclusive/OEG20020509S0075 Sugar tutorial Property Based System Design (PROSYD): http://www.prosyd.org/twiki/view/Public/DeliverablePageWP1: Property by Example Guide

Tools: 

Tools @HDL: @Verifier/@Designer, Formal Property Checker Aldec Inc.: Riviera-2005.04, Assertion Checking Integrated in Mixed HDL Simulation Kernel Assertive Design: DesignPSL, PSL-based verification tool suite Atrenta, Inc.: PeriScope, Predictive Analysis, Assertion-Based Analysis and Functional Verification for RTL designs Averant: Solidify, Formal Property Checker Avery Design: TestWizard, Assertion Checking Integrated in Testbench Automation Tool Axis System: Assertion Processor, Assertion Checking Integrated in Emulation Engine Cadence: Incisive Unified Simulator, Simulator with Integrated Static and Dynamic Assertion Checking Capabilities Denali Software: MMAV, PureSpec Interface Verification IP Dolphin Integration: SMASH, Assertion Checking Packaged with Mixed-Signal Simulator Doulos Ltd.: PSL Training Courses Esperan: PSL Training Courses Esterel Technologies: Esterel Studio, Assertion Checking Integrated in System Modeling Platform Fintronics: FinSim, Assertion Checking Integrated in Simulation Engine FTL Systems: Auriga, Assertion Checking Integrated in Parallel, Mixed-Signal Simulator FTL Systems: Merlin, Asynchronous Behavioral Synthesis (Sugar extended for capturing properties of asynchronous design) IBM: RuleBase PE, Formal Property Checker IBM: FoCs, Assertion Checker for Simulation/Emulation (vendor independent) IBM: Sugar1to2, Translate Sugar 1.0 Assertions to PSL/Sugar Interra Systems: Beacon-PSL, PSL Test Suite Interra Systems: Cheetah/Jaguar, PSL Analysis/Parsing Jasper Design Automation: JasperGold, Verification System Formal Property Checker Jeda Technologies, Inc.: JEDAX, Assertion Checking Integrated in HVL Mentor Graphics: CheckerWare, Library of Protocol Checkers Mentor Graphics: ModelSim 5.8, Assertion Checking Integrated in Simulation Engine Nobug Consulting: Specification Compiler Sugar-to-’e’ Translator Novas: Debussi/Verdi , Assertion-Based Debug Systems Real Intent: Verix, Formal Assertion-Based Verification System Structured Design Verification: TransactorWizard, Protocol Verification Tool Summit Design: Visual Elite, Synapticad: TestBencher Pro, Generation of Protocol Checkers Synapticad: Transaction Tracker, Specify Transaction Patterns Syntest Technologies: TurboCheck-RTL, Design-for-Test Rule Checking Temento Systems: Dialite, Dynamic assertion checking Tharas Systems: Hammer, Assertion Checking Integrated in Emulation Engine TNI/Valiosys: imPROVE-HDL, Formal Property Checker Verific Design Automation: PSL Parser/Analyzer Verisity (Cadence): Specman Elite, Assertion Checking Integrated in Testbench Automation Tool Veritable: Verity-Check, Formal Property Checker Veritools: Undertow Suite, Integrated Debugging Environment

Colophon: 

Colophon These slides were made by Roderick Bloem, Graz University of Technology. The material is based on the PSL tutorial by Cindy Eisner and Dana Fisman, which can be found at www.eedesign.com/features/exclusive/OEG20020509S0075. Parts are also based on the language reference manual, and on numerous discussions with members of the PROSYD team. Funded in part by the EU under grant 507219 (PROSYD). All mistakes are my responsibility. You are free to reuse any of this material, a reference to its source is appreciated.