Principles of Verifiable RTL Design

Examples

The follow examples are from the 2nd edition of Principles of Verifiable RTL Design.

Chapter 3

Example 3-1.

    
`ifdef EVENTS_ON
// Detects when queue is full
// and queue write request occur simultaneousl
always @(posedge ck) begin
  if(reset_n == 1'b1 && c_q_full && c_q_write) begin
    $display("EVENT%0d:%t:%m", EV_Q_FULL_WR, $time);  
  end
end
`endif

Example 3-2.

    
// Detects when both queue full
// and queue write request simultaneously occur
event_monitor #(`EV_Q1_Q2_FULL) dv_q_full_write (ck, reset_n, 
                                   c_q_full && c_q_write);

Example 3-3.

    
module event_monitor (ck, reset_n, test);
input ck, reset_n, 
test;
parameter event_id=0;
// rtl_synthesis off
  `ifdef EVENTS_ON
    always @(posedge ck) begin
      if(reset_n == 1'b1 && test==1'b1) begin 
        $display("EVENT LOG %d:%t:%m", event_id, $time);
      end
    end
  `endif
//rtl_synthesis on
endmodule // event_monitor

Example 3-4.

    
assert condition
  report message
    severity level

Example 3-5.

    
assert_eventually err_num (ck, reset_n, ev1_expr, p_expr, 
                       ev2_expr,`ASSERT_ERR_NUM);

Example 3-6.

    
module assert_always (ck, reset_n, test_expr);
  input ck, reset_n, test_expr;
  parameter severity_level = 0;
  parameter msg="ASSERT ALWAYS VIOLATION";
`ifdef ASSERT_ON
  integer error_count;
  initial error_count = 0;
  always @(posedge ck) begin
    `ifdef ASSERT_GLOBAL_RESET
      if (`ASSERT_GLOBAL_RESET != 1'b0) begin
    `else
      if (reset_n != 1'b0) begin
    `endif
        if (test_expr  != 1'b1) begin
          error_count = error_count + 1;
          `ifdef ASSERT_MAX_REPORT_ERROR
            if (error_count <=
                  `ASSERT_MAX_REPORT_ERROR)
          `endif
              $display("%s : severity %0d : time %0t : %m", 
                        msg, severity_level, $time);
          if (severity_level == 0) $finish;
        end
     end
   end
 end // always
`endif
endmodule // assert_always

Example 3-7.

    
assertion_instantiation ::= assert_identifier
   [parameter_value_assignment] module_instance ;
parameter_value_assignment ::= #(severity_number {,other
   parameter expressions}, message)
module_instance ::= name_of_instance
   ([list_of_module_connections])
name_of_instance ::= module_instance_identifier
list_of_module_connections ::=
   ordered_port_connection {,ordered_port_connection} |
   named_port_connection {,named_port_connection}
ordered_port_connection ::= [expression]
named_port_connection ::= .port_identifier ([expression])
assert_identifer ::= assert_[type_identifier]
type_identifier ::= identifier

Example 3-8.

    
if (`TOP.dv_initialization_complete) // Check for reset done
  if(event_expr) // Check for event
    $display("EVENT%0d:%d:%m", `EVENT_NUM, $time);

Example 3-9.

    
ASSERT_EVENTUALLY (err_num, ck, reset_n, ev1_exp, p_expr,
        ev2_expr, `ASSERT_ERR_NUM);

Example 3-8.

    
// rtl_synthesis off
`ifdef ASSERT_ON
  assert_eventually err_num (ck, reset_n, ev1_expr, p_expr,
         ev2_expr, `ASSERT_ERR_NUM);
`endif
// rtl_synthesis on

Chapter 4

Example 4-1.

    
`ifdef  RTL
<RTL behavior specification>
`else
<macro cell instance implementation>
`endif
    For example: 
    
`ifdef  RTL
assign perr = ^in; // calculate parity on `in'
`else
wire t1, t2, t3;
     XOR3 u1 (t1, in[0], in[1], in[2]);
     XOR3 u2 (t2, in[3], in[4], in[5]);
     XOR3 u3 (t3, in[6], in[7], in[8]);
     XOR3 u4 (perr, t1, t2, t3);
`endif

Example 4-2.

    
module dff (ck,q,d,ck,rst_,scan_sel,scan_in);
  // parameterized module
  always @(posedge ck) 
if (rst_ == 0) 
    q <= 0; 
else if (scan_sel ) 
    q <= scan_in ; 
else 
q <= d;
endmodule // dff

Example 4-3.

    
dff #(16) dff_a (ck, r_a, c_a, reset_, scan_sel);
dff #(16) dff_b (ck, r_b, c_b, reset_, scan_sel); 
dff #(16) dff_c (ck, r_c, c_c, reset_, scan_sel);

Example 4-4.

    
if (rst_ == 1'b0) 
    r_a <= 16'h0; 
else if (scan_sel) 
    r_a <= \dff_a.scan_in ; 
else 
    r_a <= c_a;
if (rst_ == 1'b0) 
    r_b <= 16'h0; 
else if (scan_sel) 
    r_b <= \dff_b.scan_in ; 
else 
    r_b <= c_b; 
if (rst_ == 1'b0) 
    r_c <= 16'h0; 
else if (scan_sel) 
    r_c <= \dff_c.scan_in ; 
else 
r_a <= c_c;

Example 4-5.

    
if (rst_ == 1'b0) begin
    r_a <= 16'b0; 
    r_b <= 16'b0; 
    r_c <= 16'b0; 
end 
else if (scan_sel) begin 
r_a <= \dff_a.scan_in ;
    r_b <= \dff_b.scan_in ;
    r_c <= \dff_c.scan_in ;
end 
else begin
    r_a <= c_a; 
    r_b <= c_b; 
    r_c <= c_c; 
end

Example 4-6.

    
MUX2_20 muxes (
    .S (<1 bit port connection>),
    .D0 (<20 bit port connection>),
    .D1 (<20 bit port connection>),
    .X_ (<20 bit port connection>)
  );

Example 4-7.

    
module mux2_20(x_, d0, d1, s);
  output [19:0] x_;
  input s;
  input [19:0] d0;
  input [19:0] d1;
  assign x_ = ~(s ? d1 : d0);
endmodule // mux2_20

Example 4-8.

    
module mux2_20(x_, d0, d1, s);
  output [19:0] x_;
  input s;
  input [19:0] d0;
  input [19:0] d1;
mux2_4 m0(
  .s(s), .d1(d1[19:16]), .d0(d0[19:16]),
  .x_(x_[19:16]));
mux2_4 m1(
  .s(s), .d1(d1[15:12]), .d0(d0[15:12]),
  .x_(x_[15:12]));
mux2_4 m2(
  .s(s), .d1(d1[11:8]), .d0(d0[11:8]),
  .x_(x_[11:8]));
mux2_4 m3(
  .s(s), .d1(d1[7:4]), .d0(d0[7:4]),
  .x_(x_[7:4]));
mux2_4 m4(
  .s(s), .d1(d1[3:0]), .d0(d0[3:0]),
  .x_(x_[3:0]));
endmodule // mux2_20

module mux2_4(s, d0, d1, x_);
  input s;
  input [3:0] d0, d1;
  output [3:0] x_;
// Vendor Macro Cell
SLI42M sli42_0( .A1(d1[0]),A2(d1[1]),.A3(d1[2]),.A4(d1[3]),
    .B1(d0[0]),.B2(d0[1]),.B3(d0[2]),.B4(d0[3]),.S(s),
    .X1(x_[0]),.X2(x_[1]),.X3(x_[2]),.X4(x_[3]));
endmodule // mux2_4
module SLI42M (A1,A2,A3,A4,B1,B2,B3, B4,S,X1,X2,X3,X4);
  input S;
  input A1,A2,A3,A4,B1,B2,B3,B4;
  output X1,X2,X3,X4;
  assign X1 = ~(S ? A1 : B1 ) ;
  assign X2 = ~(S ? A2 : B2 ) ;
  assign X3 = ~(S ? A3 : B3 ) ;
  assign X4 = ~(S ? A4 : B4 ) ;
endmodule // SLI42M

Example 4-9.

    
module dff (q,d,ck,rst,scan_sel,scan_in);
  :  // parameterized module
  always @(posedge ck) 
    q <= (rst  == 1'b1) ? 0 : (scan_sel ? scan_in : d);
  :
endmodule // dff

Example 4-10.

    
// scan stitch include file
//  -- to be included in the top module of the design
assign core.in_p3.in_reg.rb0_s.scan_in[3:0] = {
                core.out_m3.out_reg.rb0.q [29], 
                core.in_m2.err.r12.q [4], 
                core.in_p3.pkt_info.r11.q [7], 
                core.out_p3.out_reg.rb0.q [32]};
assign core.in_p3.in_reg.rb1.scan_in =
                core.in_p3.in_reg.rb0_s.q [3];

Example 4-11.

    
simulation dff_<$1>(q, ck, d);
  output [<$1-1:0>] q; 
  input ck;  input [<$1-1:0>] d; 
  always @(posedge ck) begin 
      q <= d; 
  end 
  initial $InitialState(q);
synthesis dff_<$1>(q, ck, d); 
  output [<$1-1:0>] q; 
  input ck;  input [<$1-1:0>] d; 
  cffd r<$1-1:0>( .d(d<$1-1:0>),.ck(ck), .q(q<$1-1:0>));

Example 4-12.

    
DFF (2, reg_idle, r_idle, ck, c_idle); 
DFF (4, reg_head, r_head, ck, c_head);

Example 4-13.

    
dff_2 reg_idle ( .d(c_idle), .ck(ck_a), .q(r_idle)); 
dff_4 reg_head ( .d(c_head), .ck(ck_a), .q(r_head));

Example 4-14.

    
module dff_2(q, ck, d); 
  output [1:0] q; 
  input ck;  input [1:0] d; 
  always @(posedge ck) begin 
    q <= d; 
  end
  initial $InitialState(q);
endmodule // dff_2
module dff_4(q, ck, d); 
  output [3:0] q; 
  input ck;  input [3:0] d; 
  always @(posedge ck) begin 
    q <= d; 
  end
  initial $InitialState(q);
endmodule // dff_4

Example 4-15.

    
module dff_2(q, ck, d); 
output [1:0] q; 
  input ck; 
  input [1:0] d; 
  cffd r0(  .d(d[1]), .ck(ck), .q(q[1])  ); 
  cffd r1(  .d(d[0]), .ck(ck), .q(q[0])  ); 
endmodule // dff_2
module dff_4(q, ck, d); 
  output [3:0] q; 
input ck; 
  input [3:0] d; 
  cffd r0(  .d(d[3]), .ck(ck), .q(q[3])  ); 
  cffd r1(  .d(d[2]), .ck(ck), .q(q[2])  ); 
  cffd r2(  .d(d[1]), .ck(ck), .q(q[1])  ); 
  cffd r3(  .d(d[0]), .ck(ck), .q(q[0])  ); 
endmodule // dff_2

Chapter 5

Example 5-1.

    
module x;
  reg a,b,c;
  reg d,e;
  always @(b or c)
    d = b ^ c;
// Extra evaluation in event-driven simulation
  always @(a or d)
    begin
      e = a ^ d;
      if ($time > 0) $display(" e = %b",e);
    end
  initial
    begin
      {a,b,c} = 3'b000;
      #1;
      a = 1'b1;
      b = 1'b1;
      #1;
      $finish;
    end
endmodule // x

Example 5-2.

    
  always @(a or b or c) begin
    d = b ^ c;
    e = a ^ d;
// Only one evaluation in rank-ordered simulation
    if ($time > 0) $display(" e = %b",e);
  end

Example 5-3.

    a) Original Verilog 
    
assign c = a;
assign g = f;
always @( c or d) begin
        case (c)
                2'h0 : f = d;
                2'h1 : f = 1'b0;
                default : f = 1'b1;
        endcase
end
assign d = b;
    b) Rank-ordered Verilog 
    
always @(a or b) begin
  c = a;
  d = b;
  case (c)
    2'h0 : f = d;
    2'h1 : f = 1'b0;
    default : f = 1'b1;
  endcase
  g = f;
end

Example 5-4.

    a) Original RTL logic. 
    
always @(a) begin
  case ( a )
    3'h0 : z = 3'h3 ;
    3'h3 : z = 3'h6 ;
    3'h6 : z = 3'h0 ;
    default : z = 3'h7 ;
  endcase
end
assign w = ( c  != 1'b0 ) ? z : a  ;
always @(a or b or w) begin
  case ( b )
    4'h0 : d = w ;
    default : d = a  ;
  endcase
end
    b) After branch partitioning. 
    
always @(a or b or c)   
  case ( b)
    4'h0 :begin
        if ( c  != 1'b0 ) begin
          case ( a)
            3'h0 : z = 3'h3 ;
            3'h3 : z = 3'h6 ;
            3'h6 : z = 3'h0 ;
            default : z = 3'h7 ;
          endcase         
          w = z ;
        end
        else
          w = a ;
        d = w ;
      end
    default : d = a ;
  endcase

Chapter 6

Example 6-1.

    
`ifdef  RTL
  assign perr = ^in; // calculate parity on `in'
`else
  wire t1, t2, t3;
     XOR3 u1 (t1, in[0], in[1], in[2]);
     XOR3 u2 (t2, in[3], in[4], in[5]);
     XOR3 u3 (t3, in[6], in[7], in[8]);
     XOR3 u4 (perr, t1, t2, t3);
`endif

Example 6-2.

    
  assign  c_a = f1;
  assign  c_b = f2;
  assign  c_c = f3;
  assign  c_y =(c_a & c_b) | c_c;

Example 6-3.

    
Map (c_a,  A)
Map (c_b,  B)
Map (c_c,  C)
Map (c_y,  X)

Example 6-4.

    
  assign c_indx = (((coord_x * coord_y) & dx_mask) + indx_offset);

Example 6-5.

    
  mult_16x16 mult1 (coord_x, coor_y, mult1_prod);
  assign c_indx = ((mult1_prod & indx_mask) + indx_offset);

Example 6-6.

    
  case ((a & b | c ^ d) || mem[idx])
    4'b0100: c_nxt_st = r_nxt_st << 1;
    4'b1000: c_nxt_st = r_nxt_st >> 1;
    default: c_nxt_st = r_nxt_st;
  endcase;

Example 6-7.

    
  c_nxt_st_test = (a & b | c ^ d) || mem[idx];
  case (c_nxt_st_test)
    4'b0100: c_nxt_st = r_nxt_st << 1;
    4'b1000: c_nxt_st = r_nxt_st >> 1;
    default: c_nxt_st = r_nxt_st;
  endcase;

Example 6-8.

    
  wire a, b, q;
  reg [1:0] s;
  reg [1:0] en_n;
  :
  always @(s) begin 
    case (s) //rtl_synthesis full_case
      2'b00: en_n = 2'b11;
      2'b01: en_n = 2'b10;
      2'b10: en_n = 2'b01;
    endcase
  end
  assign q = (~en_n[0]) ? a : 1'bz;
  assign q = (~en_n[1]) ? b : 1'bz;

Example 6-9.

    
module dff_xc_4 ( q, d, scan_in, ck, scan_sel, reset_, phase_en); 
  output  [3:0] q;
  input  [3:0] d, scan_in; 
  input ck, scan_sel, reset_, phase_en; 
  reg [3:0] q;
  always @(posedge ck) begin // model checking model
    if (phase_en) // to support common clock abstraction
          q <= (reset_n==0)?4'b0000:((scan_sel)?scan_in:d);
  end
endmodule // dff_xc_4

Chapter 7

Example 7-1.

    
`timescale 1 ns / 10 ps
// Define time to offset random initialization of registers.
`define TIMEINIT #0.05;
`define TIMEINITLATCH #0.06;
`define TIMEINITRESET #0.07;
`define TIMEINITTEST #0.1
...
initial
  Initialize the waveform viewer.
...
initial begin
`TIMEINIT
  Randomly initialize flip-flops.
end
initial begin
`TIMEINITLATCH
  Randomly initialize latches.
end
initial begin
`TIMEINITRESET
  Randomly initialize reset flip-flops.
end
initial begin
`TIMEINITTEST
  Start the clocks and the test.
end

Example 7-2.

    
always @(BCK)
  BCK_NBA <= BCK;
assign `TIMEASSIGN DATA = BCK ? QH : QL;

Example 7-3.

    
assign `TIMEASSIGN DATA = BCK ? QH : QL;

Example 7-4.

    
`define TIMENBA #0.01
...
always @posedge (ck)
  q <= `TIMENBA d;

Figure 7-1.

False-path feedback 
    
module m (s, a, b, y, z);
  input s;
  input a, b;
  output y, z;
  wire s, a, b;
  wire y, z;
  assign y = s ? a : z;
  assign z = s ? y : b;
endmodule // m

Example 7-5.

    a) Module with apparent feedback 
    
module m (a, d);
  input a;
  output d;
  reg b, d;
  wire c;
  always @(a or c)
    begin
      b = a;
      d = c;
    end
  assign c = b;
endmodule // m
    b) Inlining assign to clear up feedback 
    
module m (a, d);
  input a;
  output d;
  reg b, c, d;
  always @(a)
    begin
      b = a;
      c = b;
      d = c;
    end
endmodule // m
    c) Moving procedural assignments to assign 
    
module m (a, d);
  input a;
  output d;
  wire b, c, d;
  assign b = a;
  assign d = c;
  assign c = b;
endmodule // m

Example 7-6.

    a) Functionally-specified case 
    
module c (r_o, c_n);
  input [1:0] r_o;
  output [1:0] c_n;
  reg [1:0] c_n;
  always @(r_o)
    case (r_o) // rtl_synthesis full_case 
      2'b00 : c_n = 2'b01;
      2'b01 : c_n = 2'b10;
      2'b10 : c_n = 2'b00;
    endcase
endmodule // c
    b) Fully-specified case 
    
module c (r_o, c_n);
  input [1:0] r_o;
  output [1:0] c_n;
  reg [1:0] c_n;
  always @(r_o)
    case (r_o) 
      2'b00 : c_n = 2'b01;
      2'b01 : c_n = 2'b10;
      2'b10 : c_n = 2'b00;
      2'b11 : c_n = 2'b00;
    endcase
endmodule // c

Example 7-7.

    
module one_hot(c_hot,c_code);
  input [7:0] c_hot;
  output [2:0] c_code;
  reg [2:0] c_code;
  always @ (c_hot) begin
    case (c_hot) // RTL synthesis full_case
      8'b10000000: c_code = 3'b000;
      8'b01000000: c_code = 3'b001;
      8'b00100000: c_code = 3'b010;
      8'b00010000: c_code = 3'b011;
      8'b00001000: c_code = 3'b100;
      8'b00000100: c_code = 3'b101;
      8'b00000010: c_code = 3'b110;
      8'b00000001: c_code = 3'b111;
      default: c_code = 3'b000; // causes 3X gates
    endcase
  end // always (c_hot)
endmodule // one_hot

Example 7-8.

    

module one_hot(c_hot,c_code);
  input [7:0] c_hot;
  output [2:0] c_code;
  reg [2:0] c_code;
  reg [2:0] c_code0,c_code1,c_code2,c_code3;
  reg [2:0] c_code4,c_code5,c_code6;
  always @ (c_hot) begin
    c_code6 = (c_hot [6]) ? 3'b001 : 3'b000;
    c_code5 = (c_hot [5]) ? 3'b010 : 3'b000;
    c_code4 = (c_hot [4]) ? 3'b011 : 3'b000;
    c_code3 = (c_hot [3]) ? 3'b100 : 3'b000;
    c_code2 = (c_hot [2]) ? 3'b101 : 3'b000;
    c_code1 = (c_hot [1]) ? 3'b110 : 3'b000;
    c_code0 = (c_hot [0]) ? 3'b111 : 3'b000;
    c_code = c_code0 | c_code1 | c_code2 | c_code3 |
             c_code4 | c_code5 | c_code6;
  end // always (c_hot)
endmodule // one_hot

Example 7-9.

    
    case (c_hot)
      8'b00000001,
      8'b00000010,
      8'b00000100,
      8'b00001000,
      8'b00010000,
      8'b00100000,
      8'b01000000,
      8'b10000000: c_hot_error = 1'b0;
      default: c_hot_error = 1'b1;
    endcase
  end // always (c_hot) 
  assert_one_hot c_hot_check #(0, 8) 
                   (ck, reset_n, c_hot);
endmodule // one_hot

Example 7-10.

    
module dff_tri(pin,qin,ck,dis);
  parameter w = 3;
  output [w-1:0] pin;
  input [w-1:0] qin;
  input ck;
  input dis;
  reg [w-1:0] qout;
  always @(posedge ck)
    qout <= qin;
  tri [w-1:0] pin = !dis ? qout : {w{1'bZ}};
endmodule // dff_tri

Example 7-11.

    

module rec_tri_4(pin);
  inout [3:0] pin;
  reg [3:0] ipin,qpin;
  always @(pin or qpin) begin
    ipin = pin;
    $Trapxz(ipin,pin,qpin);
  end
  initial
    $InitialState(qpin);
endmodule // rec_tri_4

Example 7-12.

    a) Verilog Source 
    
...
`ifdef RTL
  RTL version of logic
`else
  gate-level version of logic
`endif
...
    b) Boolean equivalence command line options 
    
  -model1 a.v -model2 +define+RTL a.v

Example 7-13.

    
module chip0(
  chip timing inputs,
  chip function i-o's);
  tapper1 tapper(
    chip timing inputs
    core timing outputs);
  chip_core1 core(
    chip function i-o's);
endmodule // chip0

module chip_tapper1(
  chip timin inputs,
  core timing inputs);
  timing control procedures
endmodule // chip_tapper1

module chip_core1(
  core timing inputs,
  chip function i-o's);
  chip major module instances
endmodule // chip_core1

Example 7-14.

    

    
`include "<file name>"
module <prefix><name><level number> (input-output);
  <input declarations>
  <clocks>
  <reset>
  <data>
  <output declarations>
  <inout declarations>
  <wire declarations>
  <major submodule instances - explicit port connections>
endmodule // <prefix><name><level number>

Example 7-15.

    

    
`include ""
module <prefix><name><level number> (input-output);
  <input declarations>
    <clocks>
    <reset>
    <data>
  <output declarations>
  <inout declarations>
  <wire declarations>
  <reg declarations>
  <always procedural blocks>
  <assign statements>
  <major submodule instances - explicit port connections>
  <library module instances -
          may have implicit port connections>
endmodule // <prefix><name><level number>

Example 7-16.

    a) Implicit port-order based signal connections input 
    
  dff #(4) reg_head (r_head, ck, c_head);
    b) Explicit port-signal connections output 
    
  dff #(4) reg_head (.d(c_head),
                     .ck(ck),
                     .q(r_head));

Example 7-17.

    a) Submodules with consistent names 
    
module dr5(a, s, t);
  input a;
  output [1:0] s, t;
  ...
endmodule // dr5
module rc5(s, t, z);
  input [1:0] s, t;
  output z;
  ...
endmodule // rc5
    b) Module instantiating dr5 and rc5 
    
module nu4();
  dr5 dr();
  rc5 rc();
endmodule // nu4
    c) Consistent names imply connections 
    
module nu4 (a,z);
    input       a;
    output      z;
    wire [1:0]  s;
    wire [1:0]  t;
    dr5 dr (
      .a ( a ),
      .s ( s ),
      .t ( t ));
    rc5 rc (
      .s ( s ),
      .t ( t ),
      .z ( z ));
endmodule // nu4

Example 7-18.

    
dfft_xc reg_eri_last (
       .q(r_eri_last),
       .xq(r_eri_last_n),
      .ck(ck),
      .d(c_eri_last),
      .reset_n(reset_n),
       .i_scan(i_scan)
       );

Example 7-19.

    
// Flip-flop with scan and inverted output
module dff_sn_32(q, q_, ck, d, sc_sel, scan_in);
  output [31:0] q;
  output [31:0] q_;
  input ck;
  input [31:0] d;
  input sc_sel;
  input [31:0] scan_in;
  tri0 [31:0] scan_in;
  reg [31:0] q;
  assign q_ = ~q;
  always @(posedge ck) begin
    q <= sc_sel ? scan_in : d;
  end
endmodule // dff_sn_32

Example 7-20.

    
module respsend (
  ...
  function [6:0] start_pointer;
  ...
  endfunction // start_pointer
  ...
  always @(r_pop_cnt ...
    begin
      ...
    end // always @(r_pop_cnt
  ...
endmodule // respsend

Example 7-21.

    
// Determine if we can bypass. Unfortunately, 
// we need to wait for the A cycle in the table
// since the MC needs A cycle bits coincident
// with the win. Only local requests will be bypassed.
  assign c_bp_hdr_val = (r_hdr_valids_1 == 11'b0) &&
                        (r_hdr_valids == 11'h400);
  ...

Chapter 8

Example 8-1.

    a) Bad: Flip-flops in-lined in module 
    
  always @(posedge ck250)
    begin
      r_rcs <= rst_ ? c_rcs : 0;
      r_del <= c_del;
      r_avail <= c_avail;
      r_n1 <= rst_ ? c_n1 : 0;
      r_n2 <= rst_ ? c_n2 : 0;
      r_n3 <= rst_ ? c_n3 : 0;
      r_n4 <= rst_ ? c_n4 : 0;
      r_n5 <= rst_ ? c_n5 : 0;
      r_n6 <= rst_ ? c_n6 : 0;
    end
    b) Good: Flip-flops instantiated in module 
    
  dff_r reg_rcs (r_rcs, ck250, rst_, c_rcs);
  dff_r5 reg_del (r_del, ck250, c_del);
  dff reg_avail ( r_avail, ck250, c_avail);
  dff_r5 reg_n1 (r_n1, ck250, rst_ , c_n1);
  dff_r5 reg_n2 (r_n2, ck250, rst_ , c_n2);
  dff_r5 reg_n3 (r_n3, ck250, rst_ , c_n3);
  dff_r5 reg_n4 (r_n4, ck250, rst_ , c_n4);
  dff_r5 reg_n5 (r_n5, ck250, rst_ , c_n5);
  dff_r5 reg_n6 (r_n6, ck250, rst_ , c_n6);

Example 8-2.

    
  reg [15:0] a,b,c;
  ...
  begin
    b = 16'b0000000000000000;
    c = 16'b000000000000X000;
    a = b + c;
    $display(" a = %b",a);
  end

Example 8-3.

    
  reg [1:0] d,e;
  ...
  begin
    d = 2'b0X;
    case (d)
      2'b00 : e = 2'b01;
      2'b01 : e = 2'b11;
      2'b10 : e = 2'b10;
      2'b11 : e = 2'b00;
      default : e = 2'bXX;
    endcase
    $display(" e = %b",e);
end

Example 8-4.

    
  reg [1:0] d,e;
  ...
  begin
    case (d)
      2'b00 : e = 2'b01;
      2'b01 : e = 2'b11;
      2'b10 : e = 2'b10;
      default : e = 2'b00;
      endcase
      $display(" e = %b",e);
    end

Example 8-5.

    a) X intercept in if-else 
    
  if (f === 1'b0) 
    g = 2'b00;
  else
  if (f === 1'bX) 
    g = 2'b0X; 
  else
    g = 2'b01;
    b) X intercept in case 
    
  reg [1:0] d,e;
  ...
  begin
    case (d) 
      2'b00 : e = 2'b01; 
      2'b0X : e = 2'bX1;
      2'b01 : e = 2'b11; 
      2'bX0 : e = 2'bXX; 
      2'bXX : e = 2'bXX; 
      2'bX1 : e = 2'bXX;
      2'b10 : e = 2'b10; 
      2'b1X : e = 2'bX0; 
      2'b11 : e = 2'b00;
    endcase
  end

Example 8-6.

    
  reg [1:0] d,e;
  ...
  begin
    e = { ( ^ d), ~d[1]};
  end

Example 8-7.

    
  case (select) 
    2'b00 : mux = a;
    2'b01 : mux = b; 
    2'b10 : mux = c; 
    2'b11 : mux = d; 
    default : mux = 'bX; 
  endcase

Example 8-8.

    a) Bit references 
    
    c_ecc_out_1 =c_in [10] ^ c_in[11]
               ^ c_in[12] ^ c_in[13]
               ^ c_in[14] ^ c_in[15]
               ^ c_in[16] ^ c_in[17]
               ^ c_in[18] ^ c_in[19]
               ^ c_in[20] ^ c_in[21]
               ^ c_in[22] ^ c_in[23]
               ^ c_in[24] ^ c_in[25]
               ^ c_in[26] ^ c_in[27]
               ^ c_in[28] ^ c_in[32]
               ^ c_in[35] ^ c_in[38]
               ^ c_in[39];
    b) Parallel value operations 
    
    c_ecc_out_1 = ^ (c_in & 40'h003ffff893);

Example 8-9.

    
module fifo(
  ...
  parameter WIDTH = 13;
  parameter DEPTH = 32;
  parameter ENCODE = 0;
  ...
  function [31:0] encoder;
    input   [WIDTH-1:0]    indata;
    begin
      if (ENCODE != 0) begin
        < calculate encode value based on indata >
      end
      else
        encoder = indata; 
    end

Example 8-10.

    a) Bad: Slow / Less Obvious 
    
  input [`N-1:0] a;
  output [`N-1:0] b;
  integer i;
  reg [`N-1:0] b;
  always @ (a) begin
    for (i=0; i<=`N-1; i=i+1)
      b[i] = ~a[i];
  end
    b) Good: Fast / Simple and Clear 
    
  input [`N-1:0] a;
  output [`N-1:0] b;
  assign b = ~a;

Example 8-11.

    a) Bad: Simulates slower 
    
  input [15:0] a;
  output [0:15] b;
  integer i;
  reg [0:15] b;
  always @ (a) begin
    for (i=0; i<=15; i=i+1) 
      b[15 - i] = a[i];
  end
    b) Good: Simulates faster 
    
  input [15:0] a;
  output [0:15] b;
  assign b = {a[0], a[1], a[2], a[3],
              a[4], a[5], a[6], a[7],
              a[8], a[9], a[10], a[11],
              a[12], a[13], a[14], a[15] };

Example 8-12.

    a) Memory model with poor simulation performance 
    
  for(i = 0; i < fifo_depth; i = i+1)
    begin
      case({reset_L_ff, w_addr_ff == i})
        2'b00,
        2'b01: entry_ff[i] <= 0;
        2'b11: entry_ff[i] <= write_data;
        2'b10: entry_ff[i] <= entry_ff[i];
      endcase
    end
    b) Memory model with improved simulation performance 
    
  if (reset_L_ff)
    for(i = 0; i < fifo_depth; i = i+1) entry_ff[i] <= 0;
  else
    entry_ff[w_addr_ff] <= write_data;

Example 8-13.

    
module c (r_o, c_n);
  input [1:0] r_o;
  output [1:0] c_n;
  reg [1:0] c_n;
  always @(r_o)
    case (r_o) // rtl_synthesis full_case 
      2'b00 : c_n = 2'b01;
      2'b01 : c_n = 2'b10;
      2'b10 : c_n = 2'b00;
    endcase
endmodule // c

Example 8-14.

    
  casex (c_hot) // RTL synthesis parallel_case
    8'b1???????: c_code = 3'b000;
    8'b?1??????: c_code = 3'b001;
    8'b??1?????: c_code = 3'b010;
    8'b???1????: c_code = 3'b011;
    8'b????1???: c_code = 3'b100;
    8'b?????1??: c_code = 3'b101;
    8'b??????1?: c_code = 3'b110;
    8'b???????1: c_code = 3'b111;
  endcase

Example 8-15.

    
  casex (1'b1) // RTL synthesis parallel_case
    c_hot[7] : c_code = 3'b000;
    c_hot[6] : c_code = 3'b001;
    c_hot[5] : c_code = 3'b010;
    c_hot[4] : c_code = 3'b011;
    c_hot[3] : c_code = 3'b100;
    c_hot[2] : c_code = 3'b101;
    c_hot[1] : c_code = 3'b110;
    c_hot[0] : c_code = 3'b111;
  endcase

Example 8-16.

    
  always
    begin
      @(posedge ck);
        e1 <= 2'b00;
      @(posedge ck);
        e1 <= 2'b01;
      @(posedge ck);
        e1 <= 2'b11;
      @(posedge ck);
       e1 <= 2'b10;
    end

Example 8-17.

    
module dff (q, d, ck);
  output [7:0] q;
  input [7:0] d;
  input ck;
  always @(posedge ck)
    q <= d;
// rtl_synthesis off
  initial
    q = 8'h00;
// rtl_synthesis on
endmodule // dff

Example 8-18.

    
module b (p, w, x, y, z);
  input [7:0] w, x, y, z;
  output [7:0] p;
  wire [7:0] w, x, y, z;
  reg [7:0] p, r, s;
  always @(w or x or y) // or z omitted
    begin
      r = w | x;
      s = y | z;
      p = r & s;
    end
endmodule // b

Example 8-19.

    
module b (p, w, x, y, z);
  input [7:0] w, x, y, z;
  output [7:0] p;
  wire [7:0] w, x, y, z;
  reg [7:0] p, r, s;
  always @(w or x or y or z)
    begin
      r = w | x; // rank 1 
      p = r & s; // rank 2 
      s = y | z; // rank 1 
    end
endmodule // b

Example 8-20.

    
module dff_2 (q, ck ,rst , d);
  input clk ,rst;
  input [1:0] d;
  output [1:0] q;
  reg [1:0] q;
  always @(posedge ck)
    q <= #1 (rst == 1'b0) ? d : 2'b00;
endmodule // dff_2

Example 8-21.

    a) Custom-timed inserted states 
    
  always @(posedge ck)
    begin
      o_ad_valid <= #0.01 2'bz;
      o_ad_validb <= #0.01 2'bz;
      o_trans_id <= #0.01 6'bz;
      o_master_id <= #0.01 3'bz;
    end
    b) Common-timed inserted states 
    
  always @(posedge ck)
    begin
      o_ad_valid <= `DELAYNBA 2'bz;
      o_ad_validb <= `DELAYNBA 2'bz;
      o_trans_id <= `DELAYNBA 6'bz;
      o_master_id <= `DELAYNBA 3'bz;
    end
    c) Clock-timed inserted states 
    
  always @(posedge `top.ck_i)
    begin
      o_ad_valid <= 2'bz;
      o_ad_validb <= 2'bz;
      o_trans_id <= 6'bz;
      o_master_id <= 3'bz;
    end

Example 8-22.

    a) Blocking assignments with a race 
    
  always @(posedge ck)
    begin
      b = a;
    end
  always @(posedge ck)
    begin
      c = b;
    end
    b) Non-blocking assignments eliminate the race 
    
  always @(posedge ck)
    begin
      b <= a;
    end
  always @(posedge ck)
    begin
      c <= b;
    end
    c) Sequential/combinational blocks eliminate the race 
    
  always @(posedge ck)
    begin
      b <= a;
    end
  always @(b)
    begin
      c = b;
    end
    d) Combined combinational block eliminates the race 
    
  always @(a)
    begin
      b = a;
      c = b;
    end

Example 8-23.

    a) done is always zero, whatever the value of count_ff 
    
  assign done = & (count_ff [4:0] + 1);
    b) done is one, when count_ff is 5'b11110 
    
  assign done = & (count_ff [4:0] + 5'd1);

Example 8-24.

    
  always @(a_r or b_c) begin
    if (a_r == 1'b1)
      d_c = d_c + b_c;
    else
      d_c = d_c - b_c;
  end

Example 8-25.

    
  always @(posedge clk or reset_)
    pad_ff <= reset_ ? pad_o : 32'h0;

Example 8-26.

    
  always @(posedge s1)
    d1_ready  <= (reset_L) ? 1'b1 : 1'b0;
  always @(negedge clk) 
    d1_ready <=  ~d0_ready & d1_ready;

Chapter 9

Example 9-1.

    
module b ;
endmodule

Example 9-2.

    
module module;
endmodule

Example 9-3.

    
// to end-of-line 
/* to */

Example 9-4.

    
/* The following module is a simulation
   diagnostic aid, not real hardware */
// rtl_synthesis off
module a ;
// The internals of this module will be supplied by
// the formal DV project
endmodule // a
// rtl_synthesis on

Example 9-5.

    a) Module b_c 
    
module b_c(o, i, j);
  input i, j;
  output o;
  wire o;
  assign o = i | j;
endmodule // b_c
    b) Module b_d 
    
module b_d(o, i, j);
  input i, j;
  output o;
  wire o;
  assign o = i & j;
endmodule // b_d

Example 9-6.

    a) Submodules b_c, b_d 
    
module b_c(o, i, j);
  input [7:0] i, j;
  output [7:0] o;
  wire [7:0] o;
  assign o = i | j;
endmodule // b_c
module b_d(o, i, j);
  input [7:0] i, j;
  output [7:0] o; 
  wire [7:0] o;
  assign o = i & j;
endmodule // b_d
    b) Module b 
    

module b (p, w, x, y, z);
  input [7:0] w, x, y, z;
  output [7:0] p;
  wire [7:0] p, r, s,
             w, x, y, z;
  b_c c1(r, w, x);
  b_c c2(s, y, z);
  b_d d0(p, r, s);
endmodule // b

Example 9-7.

    
a) Expressed as a bit range
assign o [7:0] = i [7:0] | j [7:0];
b) Expressed as individual bit-wise or operations:
assign o [7] = i [7] | j [7];
assign o [6] = i [6] | j [6];
assign o [5] = i [5] | j [5];
assign o [4] = i [4] | j [4];
assign o [3] = i [3] | j [3];
assign o [2] = i [2] | j [2];
assign o [1] = i [1] | j [1];
assign o [0] = i [0] | j [0];

Example 9-8.

    
module b_c(o, i, j);
parameter w = 1; // 1 is the default value
input [w-1:0] i, j;
output [w-1:0] o;
wire [w-1:0] o;
assign o = i | j;
endmodule // b_c
...
b_c #(8) c1(r, w, x); // 8-bit instantiation of b_c

Example 9-9.

    
module b (p, w, x, y, z);
  input [7:0] w, x, y, z;
  output [7:0] p;
  wire [7:0] p, w, x, y, z;
  assign p = (w | x) & (y | z);
endmodule // b

Example 9-10.

    
  wire c, a; 
  wire [7:0] b; 
  assign c = a | | b; // is not treated consistently
  assign c = a | ( | b ); // is treated consistently

Example 9-11.

    

module b (p, w, x, y, z);
  input [7:0] w, x, y, z;
  output [7:0] p;
  wire [7:0] w, x, y, z;
  reg [7:0] p, r, s;
  always @(w or x or y or z)
    begin
      r = w | x;
      s = y | z;
      p = r & s; 
    end
endmodule // b

Example 9-12.

    
  always @(w or x or y or z)
    p = (w | x) & (y | z);

Example 9-13.

    
  assign p = (w | x) & (y | z);

Example 9-14.

    
module b_dp(ap_in0,ap_in1, ap_out0,ap_out1);
  input [39:0] ap_in0, ap_in1;
  output [47:0] ap_out0, ap_out1;
  reg [47:0] ap_out0, ap_out1;
  function [47:0] c_ecc_out;
    input [39:0] c_data_in;
    begin
      c_ecc_out = { (^ (c_data_in & 40'h00000007f8)),
                    (^ (c_data_in & 40'h003ffff893)),
                    (^ (c_data_in & 40'h0fc03f5c06)),
                    (^ (c_data_in & 40'h71c3cfa84d)),
                    (^ (c_data_in & 40'hb6445533ff)),
                    (^ (c_data_in & 40'hd298e2fa38)),
                    (^ (c_data_in & 40'h0f294bc17f)),
                    (^ (c_data_in & 40'hea360cfc67)) ,
                    c_data_in};
    end
  endfunction
  always @(ap_in0 or ap_in1)
    begin
      ap_out0 = c_ecc_out (ap_in0);
      ap_out1 = c_ecc_out (ap_in1);
    end
endmodule // b_dp

Example 9-15.

    
assign ap_out0 = c_ecc_out (ap_in0);
assign ap_out1 = c_ecc_out (ap_in1);

Example 9-16.

    
module b_mux (p, s, w, x, y, z);
  input [1:0] s;
  input [7:0] w, x, y, z;
  output [7:0] p;
  wire [1:0] s;
  wire [7:0] w, x, y, z;
  reg [7:0] p;
  always @(s or w or x or y or z)
    case (s)
      2'b00 : p = w;
      2'b01 : p = x;
      2'b10 : p = y;
      2'b11 : p = z;
    endcase
endmodule // b_mux

Example 9-17.

    
module b_gc (ck ,rst , r_gc);
  input ck ,rst;
  output [1:0] r_gc;
  wire [1:0] r_gc;
  reg [1:0] n;
  always @(r_gc)
    case (r_gc)
      2'b00 : n = 2'b01;
      2'b01 : n = 2'b11;
      2'b11 : n = 2'b10;
      2'b10 : n = 2'b00;
    endcase
  dff #(2) reg_r ( .q(r_gc), .ck(ck), .d(n), .rst (rst) );
endmodule // b_gc

Example 9-18.

    
module enum_encode (c_error_vector, c_code);
  input [4:0] c_error_vector;
  output [2:0] c_code;
  reg [2:0] c_code;
  always @ (c_error_vector)
    begin
      casex (c_error_vector)
        5'b1????: c_code = 3'h1;
        5'b01???: c_code = 3'h2;
        5'b001??: c_code = 3'h3;
        5'b0001?: c_code = 3'h4;
        5'b00001: c_code = 3'h5;
        5'b00000: c_code = 3'h0;
      endcase
    end
endmodule // enum_encode

Example 9-19.

    
module dff (q, ck ,rst , d);
  parameter w = 1;
  input ck ,rst;
  input [w-1:0] d;
  output [w-1:0] q;
  reg [w-1:0] q;
  always @(posedge ck)
    q <= (rst == 1'b0) ? d : {w{1'b0}};
endmodule // dff

Example 9-20.

    
module mwxd(clk,we,wr_ad,rd_ad,di,r_do);
  parameter w = 16; // word width
  parameter d = 512; // memory depth
  parameter a = 9; // address width
  input clk, we;
  input [a-1:0] wr_ad;
  input [a-1:0] rd_ad;
  input [w-1:0] di;
  output [w-1:0] r_do;
  reg [a-1:0] r_wr_ad;
  reg [a-1:0] r_rd_ad;
  reg r_we;
  reg [w-1:0] r_di;
  reg [w-1:0] r_do;
  reg [w-1:0] core [0:d-1];
  wire [w-1:0] c_do;
  always @(posedge clk) begin
    r_wr_ad <= wr_ad;
    r_rd_ad <= rd_ad;
    r_we <= we;
    r_di <= di;
    r_do <= c_do;
  end always
  assign c_do = core[r_rd_ad];
  always @(negedge clk)
    if (r_we)
      core[r_wr_ad] = r_di;
endmodule // mwxd.

Example 9-21.

    
  ...
  if (severity_level == 0) $finish;
  ...

Example 9-22.

    
module ck_gen (ck);
  output ck;
  reg ck;
  always `CK_MSTR ck = ~ck;
  initial ck = 1'b0;
endmodule // ck_gen

Example 9-23.

    
module stimulus(ck,c_stimulus,c_reset);
  input ck;
  output [4:0] c_stimulus;
  output c_reset;
  reg reset;
  reg [4:0] c_stimulus;
  reg [5:0] c_counter;
  reg c_reset;
  wire [5:0] r_counter;
  always @(r_counter) begin
    c_counter = r_counter + 6'd1;
    if (r_counter == 6'h20)
      $finish;
    c_stimulus = c_counter[4:0];
  end
  dff #(6) reg_counter (r_counter,ck,c_reset,c_counter);
initial begin
  c_counter = 6'd0;
  c_reset = 1'b1;
  `TIME_RESET ;
  c_reset = 1'b0;
end
endmodule // stimulus

Example 9-24.

    
module log_xz_test(ck_l,c_stimulus,c_codex,c_codez);
  input ck_l;
  input [4:0] c_stimulus;
  input [2:0] c_codex,c_codez;
  always @(posedge ck_l) begin
    $display (" %t %b %h %h", $time,
               c_stimulus,c_codex,c_codez);
  end
endmodule // log_xz_test

Example 9-25.

    
// clock half-period:
`define CK_MSTR #5
// reset hold time:
`define TIME_RESET #6
// run with assertion active:
`define ASSERT_ON
module testbench();
  wire ck;
  wire [4:0] c_stimulus;
  wire [2:0] c_codex;
  wire [2:0] c_codez;
  wire c_reset;
  ck_gen ck_gen (ck);
  stimulus s (.ck (ck), .c_stimulus (c_stimulus),
              .c_reset(c_reset));
  enum_encode x (.c_error_vector (c_stimulus),
                 .c_code (c_codex));
  enum_encodez z (.c_error_vector (c_stimulus),
                  .c_code (c_codez));
// result checking:
  log_xz_test xz_test(ck,c_stimulus,c_codex,c_codez);
assert_always #(1,"c_codex != c_codez") safety
                  (ck, ~c_reset, c_codex == c_codez);
endmodule // testbench

Example 9-26.

    a) Here we have state machine state names defined in terms of numeric equivalents.
    
`define R_NORMAL 2'h0
`define R_WAIT 2'h1
`define R_DONE 2'h2
`define R_IDLE 2'h3
    b) The following lines define names for bit fields. 
    
`define IO_T_FLD 15:10
`define IO_Q_FLD 9:4
`define IO_S_FLD 3:0
    c) This line defines a memory array size. 
    
`define QT_DEPTH 64

Example 9-27.

    
module b_gc (ck ,rst , r_gc);
`include "Example9-25"
  input ck ,rst;
  output [1:0] r_gc;
  wire [1:0] r_gc;
  reg [1:0] n;
  always @(r_gc)
    case (r_gc)
      `R_NORMAL : n = `R_WAIT;
      `R_WAIT : n = `R_IDLE;
      `R_IDLE : n = `R_DONE;
      `R_DONE : n = `R_NORMAL;
    endcase
  dff #(2) reg_r ( .q(r_gc), .ck(ck), .d(n), .rst (rst) );
endmodule // b_gc

Example 9-28.

    
  reg [(8 * `SWDTH) - 1 ) : 0] r_chip_id;
  reg [`IO_T_FLD] qt_array [0: `QT_DEPTH-1];

Appendix A

Example A-1.

    
`ifdef SHORT
`define LIMIT 10
`else // !SHORT
`define LIMIT 10_000_000
`endif // SHORT
module reverse;
  integer i,j;
  reg [0:7] e0,e1,b;
  initial
    begin
      e0 = 8'h99;
      e1 = 8'h99;
      b = 8'd0;
      for (i = 0; i < `LIMIT; i = i + 1) begin
`ifdef METHOD1
        for (j = 0; j < 8; j = j + 1)
          e0[j] = e0[j] ^ b[7-j];
`endif // METHOD1
`ifdef METHOD2
      e1 = e1 ^ {b[7],b[6],b[5],b[4],b[3],b[2],b[1],b[0]};
`endif // METHOD2
`ifdef CHECK
      if (e0 != e1) begin
        $display(" e0 != e1 - %h !- %h",e0,e1);
        $finish;
      end
`endif // CHECK
      b = b + 8'd1;
    end
`ifdef METHOD1
    $display(" e0 = %h",e0);
`endif // METHOD1
`ifdef METHOD2
    $display(" e1 = %h",e1);
`endif // METHOD2
    $finish;
  end
endmodule // reverse

Appendix C

In this section we provide examples for typical assertion monitors. These assertion monitors are consistent with the print version of Principles of Verifiable RTL Design Second Edition, as well as the examples from Chapter 3 and 5 shown above.

You can find a complete and updated assertion monitor library at the Open Verification Library (OVL) Initiative web-site (www.verificationlib.org). The OVL assertions are similar in concept to those presented here and in the book. The OVL assertion library includes Verilog source code and full documentation that you can freely download.

Example C-1. assert_always

Syntax 

    
assert_always [#(severity_level,msg)]
                [inst_name] (clk, reset_n, test_expr);

Definition 

    
module assert_always (ck, reset_n, test_expr);
  input ck, reset_n, test_expr;
  parameter severity_level = 0;
  parameter msg="ASSERT ALWAYS VIOLATION";
`ifdef ASSERT_ON
  integer error_count;
  initial error_count = 0;
  always @(posedge ck) begin
`ifdef ASSERT_GLOBAL_RESET
    if (`ASSERT_GLOBAL_RESET != 1'b0) begin
`else 
    if (reset_n != 1'b0) begin
`endif
      if (test_expr != 1'b1) begin
        error_count = error_count + 1;
        `ifdef ASSERT_MAX_REPORT_ERROR
          if (error_count <=`ASSERT_MAX_REPORT_ERROR)
        `endif
          $display("%s : severity %0d : time %0t : %m", 
                   msg, severity_level, $time);
        if (severity_level == 0) $finish;
      end
    end
  end // always
`endif
endmodule // assert_always

Example C-2. assert_change

Syntax 

    
 assert_change [#(severity_level, width, num_cks, flag, msg)]
          [inst_name] ( clk, reset_n, start_event, test_expr);

Definition 

    
module assert_change (clk, reset_n, start_event, test_expr);
  parameter severity_level=0;
  parameter width=1;
  parameter num_cks=1;
  parameter flag=0;
  parameter msg="ASSERT CHANGE VIOLATION";

  input clk;
  input reset_n;
  input start_event;
  input [width-1:0] test_expr;

//synopsys translate_off
`ifdef ASSERT_ON
  parameter CHANGE_START = 1'b0;
  parameter CHANGE_CHECK = 1'b1;
  parameter FLAG_IGNORE_NEW_START = 2'b00;
  parameter FLAG_RESET_ON_START = 2'b01;
  parameter FLAG_ERR_ON_START = 2'b10;

  reg r_change;
  reg [width-1:0] r_check_value;
  reg r_state;
  integer i;
  integer error_count;
  initial error_count = 0;

initial begin
  r_state=CHANGE_START;
  r_change=1'b0;
end

always @(posedge clk) begin
`ifdef ASSERT_GLOBAL_RESET
  if (`ASSERT_GLOBAL_RESET != 1'b0) begin
`else
  if (reset_n != 0) begin // active low reset_n
`endif
    case (r_state)
      CHANGE_START:
        if (start_event == 1'b1) begin
          r_change <= 1'b0;
          r_state <= CHANGE_CHECK;
          r_check_value <= test_expr;
          i <= num_cks;
        end
      CHANGE_CHECK:
        begin
// Count clock ticks
          if (start_event == 1'b1) begin
            if (flag == FLAG_IGNORE_NEW_START && i > 0)
              i <= i-1;
            else if (flag == FLAG_RESET_ON_START)
              i <= num_cks;
            else if (flag == FLAG_ERR_ON_START) begin
              error_count = error_count + 1;
`ifdef ASSERT_MAX_REPORT_ERROR
              if (error_count <=`ASSERT_MAX_REPORT_ERROR)
`endif
              $display("%s : illegal start event : time %0t : %m",
                               msg, $time);
              if (severity_level == 0) $finish;
            end
            else begin
// illegal 'flag' parameter value specified
// during instantiation!
              error_count = error_count + 1;
`ifdef ASSERT_MAX_REPORT_ERROR
              if (error_count <= `ASSERT_MAX_REPORT_ERROR)
`endif
              $display(
                  "%s : illegal flag parameter %0d : time %0t : %m",
                            msg, flag, $time);
              if (severity_level == 0) $finish;
            end
          end
        else if (i > 0)
          i <= i-1;
        if (r_check_value != test_expr) begin
          r_change <= 1'b1;
        end
// go to start state on last check
        if (i == 1) begin
          r_state <= CHANGE_START;
// Check that the property is true
          if ((r_change != 1'b1) &&
              (r_check_value == test_expr)) begin
            error_count = error_count + 1;
`ifdef ASSERT_MAX_REPORT_ERROR
           if (error_count <=`ASSERT_MAX_REPORT_ERROR)
`endif
           $display("%s : severity %0d : time %0t : %m",
                     msg, severity_level, $time);
           if (severity_level == 0) $finish;
          end
        end
        r_check_value <= test_expr;
      end
    endcase
  end
  else begin
    r_state <= CHANGE_START;
    r_change <= 1'b0;
  end
end // always
`endif
//synopsys translate_on
endmodule // assert_change

Example C-3. assert_window

Syntax 

    
assert_window [#(severity_level, msg)] [inst_name] (clk, reset_n,
                        start_event, test_expr, end_event);

Definition 

    
module assert_window (clk, reset_n, start_event, test_expr, end_event);
  input clk, reset_n, start_event, test_expr, end_event;
  parameter severity_level = 0;
  parameter msg="ASSERT WINDOW VIOLATION";

// synopsys translate_off
`ifdef ASSERT_ON
// local paramaters used as defines
  parameter WINDOW_START = 1'b0;
  parameter WINDOW_CHECK = 1'b1;

  reg r_state;
  initial r_state=WINDOW_START;
  integer error_count;
  initial error_count = 0;

  always @(posedge clk) begin
`ifdef ASSERT_GLOBAL_RESET
    if (`ASSERT_GLOBAL_RESET != 1'b0) begin
`else
    if (reset_n != 0) begin // active low reset_n
`endif
      case (r_state)
        WINDOW_START:
          if (start_event == 1'b1) begin
            r_state <= WINDOW_CHECK;
          end
        WINDOW_CHECK:
          begin
            if (end_event == 1'b1) begin
              r_state <= WINDOW_START;
            end
            else if (test_expr != 1'b1) begin
              error_count = error_count + 1;
`ifdef ASSERT_MAX_REPORT_ERROR
              if (error_count <= `ASSERT_MAX_REPORT_ERROR)
`endif
                $display("%s : severity %0d : time %0t : %m",
                          msg, severity_level, $time);
              if (severity_level == 0) $finish;
            end
          end
      endcase
    end
    else begin
      r_state <= WINDOW_START;
  end
end // always
`endif
// synopsys translate_on
endmodule // assert_window