Now that we have seen the example of FIFO assertion using OVL, let's see the example of using PSL to build assertions for the FIFO. PSL assertions can be coded in two ways.

• inline Coding : In this method, psl assertions are coded into verilog code as comments.
• External File : In this method, psl assertions are coded into a separate file with vunit as name.

inline Coding

• All assertions appear within a consecutive series of comments appropriate for the context.
• The first assertion statement line must begin with the psl keyword.
• Both the psl keyword and the keyword that follows it must be on the same line.
• Specify a label followed by a colon.
• Assert the behavior described in the property by using the assert or assume keyword.
• Describe the behavior of the design.
• Assertions cannot be embedded in Verilog tasks, functions, or UDPs.
• Example : // psl label: assert behavior;

External File

• To add assertions to an existing design without modifying the source text, as with legacy IP.
• To experiment with assertions before embedding them in the source file.
• When you are working in teams where the assertions are not created by the HDL author.

vunit verification_unit_name (module_name) {
  default clock = clock_edge;
  property_name: assert behavior;
  property_name: cover {behavior};
}

For more details refer to PSL usage guide that comes with the simulator.

In the code below, we use a psl assertion to check if no write is done when FIFO is full and also check if no read is done when FIFO is empty.

We can code psl assertions inline with code with // or /* */. Before we write any assertion, we need to declare the clock as in the example.

ncverilog +assert verilog_file1.v verilog_file2.v

   1 //=============================================
   2 // Function  : Synchronous (single clock) FIFO
   3 //             With Assertion
   4 // Coder     : Deepak Kumar Tala
   5 // Date      : 31-October-2002
   6 //=============================================
   7 module syn_fifo (
   8 clk      , // Clock input
   9 rst      , // Active high reset
  10 wr_cs    , // Write chip select
  11 rd_cs    , // Read chipe select
  12 data_in  , // Data input
  13 rd_en    , // Read enable
  14 wr_en    , // Write Enable
  15 data_out , // Data Output
  16 empty    , // FIFO empty
  17 full       // FIFO full
  18 );    
  19  
  20 // FIFO constants
  21 parameter DATA_WIDTH = 8;
  22 parameter ADDR_WIDTH = 8;
  23 parameter RAM_DEPTH = (1 << ADDR_WIDTH);
  24 // Port Declarations
  25 input clk ;
  26 input rst ;
  27 input wr_cs ;
  28 input rd_cs ;
  29 input rd_en ;
  30 input wr_en ;
  31 input [DATA_WIDTH-1:0] data_in ;
  32 output full ;
  33 output empty ;
  34 output [DATA_WIDTH-1:0] data_out ;
  35 
  36 //-----------Internal variables-------------------
  37 reg [ADDR_WIDTH-1:0] wr_pointer;
  38 reg [ADDR_WIDTH-1:0] rd_pointer;
  39 reg [ADDR_WIDTH :0] status_cnt;
  40 reg [DATA_WIDTH-1:0] data_out ;
  41 wire [DATA_WIDTH-1:0] data_ram ;
  42 
  43 //-----------Variable assignments---------------
  44 assign full = (status_cnt == (RAM_DEPTH-1));
  45 assign empty = (status_cnt == 0);
  46 
  47 //-----------Code Start---------------------------
  48 always @ (posedge clk or posedge rst)
  49 begin : WRITE_POINTER
  50   if (rst) begin
  51    wr_pointer <= 0;
  52   end else if (wr_cs && wr_en ) begin
  53    wr_pointer <= wr_pointer + 1;
  54   end
  55 end
  56 
  57 always @ (posedge clk or posedge rst)
  58 begin : READ_POINTER
  59   if (rst) begin
  60     rd_pointer <= 0;
  61     data_out <= 0;
  62   end else if (rd_cs && rd_en ) begin
  63     rd_pointer <= rd_pointer + 1;
  64     data_out <= data_ram;
  65   end
  66 end
  67 
  68 always  @ (posedge clk or posedge rst)
  69 begin : READ_DATA
  70   if (rst) begin
  71     data_out <= 0;
  72   end else if (rd_cs && rd_en ) begin
  73     data_out <= data_ram;
  74   end
  75 end
  76 
  77 always @ (posedge clk or posedge rst)
  78 begin : STATUS_COUNTER
  79   if (rst) begin
  80     status_cnt <= 0;
  81   // Read but no write.
  82   end else if ((rd_cs && rd_en) &&  ! (wr_cs && wr_en) 
  83                 && (status_cnt  ! = 0)) begin
  84     status_cnt <= status_cnt - 1;
  85   // Write but no read.
  86   end else if ((wr_cs && wr_en) &&  ! (rd_cs && rd_en) 
  87                && (status_cnt  ! = RAM_DEPTH)) begin
  88     status_cnt <= status_cnt + 1;
  89   end
  90 end 
  91    
  92 ram_dp_ar_aw #(DATA_WIDTH,ADDR_WIDTH) DP_RAM (
  93 .address_0 (wr_pointer) , // address_0 input 
  94 .data_0    (data_in)    , // data_0 bi-directional
  95 .cs_0      (wr_cs)      , // chip select
  96 .we_0      (wr_en)      , // write enable
  97 .oe_0      (1'b0)       , // output enable
  98 .address_1 (rd_pointer) , // address_q input
  99 .data_1    (data_ram)   , // data_1 bi-directional
 100 .cs_1      (rd_cs)      , // chip select
 101 .we_1      (1'b0)       , // Read enable
 102 .oe_1      (rd_en)        // output enable
 103 );  
 104 
 105 // Add assertion here
 106 // psl default clock = (posedge clk);
 107 // psl ERRORwritefull: assert never {full && wr_en && wr_cs};
 108 // psl ERRORreadempty: assert never {empty && rd_en && rd_cs};
 109 
 110 endmodule

Whenever there is a violation, an assertion is printed.

 0 wr:0 wr_data:00 rd:0 rd_data:xx
 5 wr:0 wr_data:00 rd:0 rd_data:00
 10 wr:1 wr_data:00 rd:0 rd_data:00
 12 wr:1 wr_data:01 rd:0 rd_data:00
 14 wr:1 wr_data:02 rd:0 rd_data:00
 16 wr:1 wr_data:03 rd:0 rd_data:00
 18 wr:1 wr_data:04 rd:0 rd_data:00
 20 wr:1 wr_data:05 rd:0 rd_data:00
 22 wr:1 wr_data:06 rd:0 rd_data:00
 24 wr:1 wr_data:07 rd:0 rd_data:00
 ncsim: *E,ASRTST (syn_fifo_psl.v,107): (time 25 NS) 
 Assertion fifo_tb.fifo.ERRORwritefull has failed 
 26 wr:1 wr_data:08 rd:0 rd_data:00
 28 wr:1 wr_data:09 rd:0 rd_data:00
 30 wr:0 wr_data:09 rd:0 rd_data:00
 32 wr:0 wr_data:09 rd:1 rd_data:00
 33 wr:0 wr_data:09 rd:1 rd_data:08
 35 wr:0 wr_data:09 rd:1 rd_data:09
 39 wr:0 wr_data:09 rd:1 rd_data:03
 41 wr:0 wr_data:09 rd:1 rd_data:04
 43 wr:0 wr_data:09 rd:1 rd_data:05
 45 wr:0 wr_data:09 rd:1 rd_data:06
 47 wr:0 wr_data:09 rd:1 rd_data:07
 ncsim: *E,ASRTST (syn_fifo_psl.v,108): (time 49 NS) 
 Assertion fifo_tb.fifo.ERRORreadempty has failed 
 49 wr:0 wr_data:09 rd:1 rd_data:08
 ncsim: *E,ASRTST (syn_fifo_psl.v,108): (time 51 NS) 
 Assertion fifo_tb.fifo.ERRORreadempty has failed 
 51 wr:0 wr_data:09 rd:1 rd_data:09
 52 wr:0 wr_data:09 rd:0 rd_data:09
 Simulation complete via $finish(1) at time 152 NS + 0
 fifo_tb.v:36   #100 $finish;

Like with any other simulation, we need to have post processing scripts to process the messages that are printed by the simulator to declare if the simulation has passed or failed.

Copyright © 1998-2014

Deepak Kumar Tala - All rights reserved

Do you have any Comment? mail me at:deepak@asic-world.com