PSL PWM Duty Cycle

Hi,
Sorry if this is OT.
This must be an issue that comes up a lot - I am trying to verify the width (in clock cycles) of a pulse, where this width is defined in a register. i.e. Is not constant.

asrt_duty_pwm1 : assert always {~pwm1_dig;pwm1_dig} |-> {pwm1_dig[duty1_dff];~pwm1_dig[(1000-duty1_dff)]} ;

Unfortunately, this does not work, and I get the error:

  asrt_duty_pwm1 : assert always {~pwm1_dig;pwm1_dig} |-> {pwm1_dig[*duty1_dff];~pwm1_dig[*(1000-duty1_dff)]} ;
                                                                             |

ncvlog: *E,NOTPAR (/design/proj/sp34/users/steven.dennis_sp34a_175/digital/modules/sp34_dpwm.pslvlog,8|81): Illegal operand for constant expression [4(IEEE)].

Can somebody suggest a workaround? Would I have the same issue using SVA?
Thanks,
Steven

In reply to moogyd:
The following is a much easier solution for you. Not everything needs to be concurrent assertions; you can use supporting logic, as shown here.


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	// verify the width (in clock cycles) of a pulse, where this width is defined in a register.  
	bit clk, pw;  
	int count, pw_limit=5;
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;   
	
	always_ff  @(posedge clk)  begin
	  if($fell(pw)) count <= 1; 
	  if($rose(pw)) assert (count == pw_limit) 
                 $display("PASS, @%t count=%d", $time, count);
	    else $display("pw error, @%t count=%d", $time, count); 
	  else count += 1; 
    end 

 initial begin 
     repeat(200) begin 
       @(posedge clk);   
       if (!randomize(pw)  with 
          {pw dist {0 :=6, 1 := 1};
           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule   
// SIm results 
# pw error, @                3330 count=          4
# PASS, @                3450 count=          5
# pw error, @                3490 count=          1
# pw error, @                3530 count=          1
# pw error, @                3570 count=          1
# pw error, @                3610 count=          1
# pw error, @                3930 count=         15
# ** Note: $finish    : pw.sv(24)
#    Time: 3990 ns  Iteration: 1  Instance: /top

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

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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

In reply to ben@SystemVerilog.us:
If you need a SVA assertion, instead of just supporting code with an immediate assertion (a better approach, BTY), yoiu can do this.


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	// verify the width (in clock cycles) of a pulse, where this width is defined in a register.  
	bit clk, pw;  
	int count, pw_limit=1;
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;   
	
	always_ff  @(posedge clk)  begin
	  if($fell(pw)) count <= 1; 
          if($rose(pw)) ap_1: assert (count == pw_limit) $display("PASS, @%t count=%d", $time, count);
	  else $display("pw error, @%t count=%d", $time, count); 
		else count += 1; 
         end 
    
    // concurrent assertion  <<<<--------------------------------------------
    property p_pw; 
    	int v_count; 
    	($fell(pw), v_count = 0) |=> 
    		first_match((1, v_count+=1)[*1:$] ##0 $rose(pw)) ##0 v_count == pw_limit; 
    endproperty 
    ap_pw: assert property(p_pw)
    		else $display("pw error @%t", $time); 
    // -----------------------*********************************-----------------
 initial begin 
     repeat(200) begin 
       @(posedge clk);   
       #2 if (!randomize(pw)  with 
          // { pw dist {[1:4] :=1, [5:7] := 2};
       	 { pw dist {0 :=1, 1 := 1};
           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule 
// Sim results 
pw error, @                 130 count=          6
# PASS, @                 170 count=          1
# pw error, @                 230 count=          2
# pw error @                 230
# pw error, @                 290 count=          2
# pw error @                 290
# PASS, @                 330 count=          1
# PASS, @                 370 count=          1
# pw error, @                 490 count=          3
# pw error @                 490
 

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

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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

Thanks a lot Ben - that’s perfect.

BTW - the assertion solution means I don’t have top update the RTL.

Steven

p.s. I tried to mark both you posts as a solution, but this isn’t allowed.

In reply to moogyd:

BTW - the assertion solution means I don’t have top update the RTL.

Steven,
The best way to avoid changes to your RTL is to use checkers. From my book,

Checkers have numerous advantages over modules and interfaces: they are race-free, they allow sequences and properties as arguments, their invocation syntax is more intuitive and concise, they may be instantiated both inside and outside procedural code, they may infer their clock and reset contexts, they have free variables, etc.46 Checkers are ignored by synthesis tools; this allows assertions to be embedded in RTL code, but without the concerns associated with improper synthesis of supporting code. It also allows for external modifications of code within the checkers without changing any time-stamp of RTL code.
46 From “ SystemVerilog Checkers: Key Building Blocks for Verification IP”,
Laurence Bisht, Dmitry Korchemny, Erik Seligman Intel Corporation http://events.dvcon.org/2012/proceedings/papers/01P_1.pdf

Below is complete code with the use of a SV checker.


import uvm_pkg::*; `include "uvm_macros.svh" 
checker rtl_chk(input bit clk, pw,
                      int pw_limit); 
// verify the width (in clock cycles) of a pulse, where this width is defined in a register. 
  int count;
  default clocking @(posedge clk); endclocking
  always_ff  @(posedge clk)  begin
    if($fell(pw)) count <= 1; 
    if($rose(pw)) ap_1: assert (count == pw_limit) $display("PASS, @%t count=%d", $time, count);
                        else $display("pw error, @%t count=%d", $time, count); 
    else count += 1; 
  end 
    
  // concurrent assertion 
  property p_pw; 
	int v_count; 
	($fell(pw), v_count = 0) |=> 
		first_match((1, v_count+=1)[*1:$] ##0 $rose(pw)) ##0 v_count == pw_limit; 
  endproperty 
  ap_pw: assert property(p_pw)
		else $display("pw error @%t", $time); 
endchecker 
	
module rtl; 
	bit clk, pw;  
	int pw_limit=1;
	initial forever #10 clk=!clk;   
	rtl_chk rtl_chk1(clk, pw, pw_limit);
	
 initial begin 
     repeat(200) begin 
       @(posedge clk);   
       #2 if (!randomize(pw)  with 
          // { pw dist {[1:4] :=1, [5:7] := 2};
       	 { pw dist {0 :=1, 1 := 1};
           }) `uvm_error("MYERR", "This is a randomize error")
       end 
       $finish; 
    end 
endmodule  
// Sim results 
PASS, @                  30 count=          1
# PASS, @                  90 count=          1
# pw error @                 190
# pw error, @                 190 count=          4
# PASS, @                 290 count=          1
# PASS, @                 330 count=          1
# pw error @                 430

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

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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