How the PSL assertions are different from SVA assertions?

SystemVerilog
1

How the PSL assertions are different from SVA assertions?

2

It has been a very long time since I used PSL, but I can tell you that I definitely prefer SVA over PSL because I see it as more expressive. To recollect PSL I wrote this simple model shown below, which gave me identical simulation results.
requirements: After rose of req, a rdy within 1 to 4 cycles, and an ack in the next cycle after that.
**SVA CODE:**first_match($rose(req) ##[1:4] rdy) |=> ack
**PSL CODE:**always ({$rose(req); !rdy[*0:3]; rdy} |=> {ack});
Differences:

  1. No delay operator in PSL; must express that with a repeat of the NOT condition.
    I prefer the SVA version on this. In PSL the antecedent reads: "rose req, at next cycle
    NO rdy repeated 0 to 3 cycles, and at next cycle rdy
    The SVA version reads as: first_match of (rose req, and then rdy within 1 to 4 cycles.
  2. PSL requires all these {} brackets for sequences.
  3. SVA has the action block.
    There are other differences, but I don’t have the time to go into them, as I would have to dig into it. SVA is part of 1800, which goes through regular updates. Next 1800 update due to be out by (maybe early)2017. I don’t believe there is any further work on PSL, unless it’s from the VHDL side, if any.
import uvm_pkg::*;
`include "uvm_macros.svh"

module mpsl; 
		bit clk, ack, rdy, req,   bus_available;           

	// Verilog flavor
	// psl default clock = (posedge clk);
	// psl property REQ_ACK =
	//  always ({$rose(req); !rdy[*0:3]; rdy} |=> {ack});
	// psl assert REQ_ACK;
    ap1: assert property(@(posedge clk) 
    		          first_match($rose(req) ##[1:4] rdy) |=> ack ) 
    	    else `uvm_info("mpsl",$sformatf("%m : error in ack %b", $sampled(ack)), UVM_LOW);
	initial forever #5 clk=!clk; 
	
	always @(posedge clk) 
	begin 
		if (!randomize(ack, rdy, req))  `uvm_error("MYERR", "This is a randomize error"); 
		
	end 
endmodule

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
3

In reply to ben@SystemVerilog.us:

The following table summarizes the differences; note, with 1800’2012, there are practically NO differences in operators. http://systemverilog.us/PSLandSVAOperators.pdf

Also, see https://www.demosondemand.com/dod/indorgs/accellera.aspx#tutorials
Pragmatic ABV: Effective Assertion-Based Verification

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
4

In reply to ben@SystemVerilog.us:

Ben,
Thanks for the explaination. Can anyone suggest,among SVA and PLS which language is preferred on AMS verification prospective?

5

In reply to Padmashree B:

More work is done with SVA than PSL in the area of verification, including AMS.
Search on (AMS verification SystemVerilog)

http://www.synopsys.com/tools/verification/amsverification/circuitsimulation/documents/customsim-vcs-wp.pdf
Ben