HierarchyFilesModulesSignalsTasksFunctionsHelp
Prev12
     );

   // There should be no rising edge of RXINT if receive interrupt is disabled
    assert_next
    #(`OVL_ERROR, 1,1,0, `OVL_ASSERT,
    "RXINT should not be triggered when disabled")
    u_ovl_rxint_disable
      (.clk(PCLK ), .reset_n (PRESETn),
     .start_event ((reg_ctrl[3]==1'b0) & (RXINT == 1'b0)),
     .test_expr   (RXINT == 1'b0)
     );

   // if RXINT falling edge, there must has been a write to INTCLEAR register with bit[1]=1
   assert_implication
     #(`OVL_ERROR,`OVL_ASSERT,
     "When there is a falling edge of RXINT, there must has been a write to INTCLEAR")
   u_ovl_rxint_clear
     (.clk(PCLK), .reset_n(PRESETn),
      .antecedent_expr(ovl_last_rxint & (~RXINT)), // Falling edge of TXINT
      .consequent_expr(ovl_last_psel & ovl_last_pwrite &
      (ovl_last_paddr==10'h003) & (ovl_last_pwdata[1]) ) // There must has been a write to INTCLEAR
     );

   // rx_buf_full should rise if rx_state change from 9 to 10
    assert_next
    #(`OVL_ERROR, 1,1,0, `OVL_ASSERT,
    "rx_buf_full should be asserted when a new character is received")
    u_ovl_rx_buf_full
      (.clk(PCLK ), .reset_n (PRESETn),
     .start_event ((rx_state==9) & (nxt_rx_state==10)),
     .test_expr   (rx_buf_full == 1'b1)
     );

   // if rx_buf_full falling edge, there must has been a read to the receive buffer
   assert_implication
     #(`OVL_ERROR,`OVL_ASSERT,
     "When there is a falling edge of RXINT, there must has been a read to receive buffer")
   u_ovl_rx_buf_full_clear
     (.clk(PCLK), .reset_n(PRESETn),
      .antecedent_expr((~rx_buf_full) & ovl_last_rx_buf_full), // Falling edge of rx_buf_full
      .consequent_expr(ovl_last_psel & (~ovl_last_pwrite) &
      (ovl_last_paddr==10'h000)  ) // There must has been a read to rx data
     );

   // TXOVRINT must be 0 if reg_ctrl[4]=0
   assert_implication
     #(`OVL_ERROR,`OVL_ASSERT,
     "When there is a falling edge of RXINT, there must has been a write to INTCLEAR")
   u_ovl_txovrint_disable
     (.clk(PCLK), .reset_n(PRESETn),
      .antecedent_expr(~reg_ctrl[4]),
      .consequent_expr(~TXOVRINT)
     );

   // RXOVRINT must be 0 if reg_ctrl[5]=0
   assert_implication
     #(`OVL_ERROR,`OVL_ASSERT,
     "When there is a falling edge of RXINT, there must has been a write to INTCLEAR")
   u_ovl_rxovrint_disable
     (.clk(PCLK), .reset_n(PRESETn),
      .antecedent_expr(~reg_ctrl[5]),
      .consequent_expr(~RXOVRINT)
     );

   // if a write take place to TX data buffer and tx_buf_full was 1, reg_tx_overrun will be set
    assert_next
    #(`OVL_ERROR, 1,1,0, `OVL_ASSERT,
    "tx buffer overrun should be asserted when a new character is write to buffer and buffer is already full")
    u_ovl_tx_buffer_overrun
      (.clk(PCLK ), .reset_n (PRESETn),
     .start_event (write_enable00 & tx_buf_full & (~tx_buf_clear)),
     .test_expr   (reg_tx_overrun == 1'b1)
     );

   // if rx_buf_full is high and rx_state change from 9 to 10, reg_rx_overrun will be set
    assert_next
    #(`OVL_ERROR, 1,1,0, `OVL_ASSERT,
    "rx buffer overrun should be asserted when a new character is received and rx buffer is already full")
    u_ovl_rx_buffer_overrun
      (.clk(PCLK ), .reset_n (PRESETn),
     .start_event (rx_buf_full & (~rx_data_read) & (rx_state==9) & (nxt_rx_state==10)),
     .test_expr   (reg_rx_overrun == 1'b1)
     );

   // if write to INTCLEAR  with bit[2]=1, reg_tx_overrun will be cleared,
    // Cannot have new overrun at the same time because the APB can only do onething at a time
    assert_next
    #(`OVL_ERROR, 1,1,0, `OVL_ASSERT,
    "tx buffer overrun should be clear when write to INTCLEAR")
    u_ovl_tx_buffer_overrun_clear_a
      (.clk(PCLK ), .reset_n (PRESETn),
     .start_event (write_enable0c & (PWDATA[2])),
     .test_expr   (reg_tx_overrun==1'b0)
     );

   // if write to STATUS  with bit[2]=1, reg_tx_overrun will be cleared,
    // Cannot have new overrun at the same time because the APB can only do onething at a time
    assert_next
    #(`OVL_ERROR, 1,1,0, `OVL_ASSERT,
    "tx buffer overrun should be clear when write to INTCLEAR")
    u_ovl_tx_buffer_overrun_clear_b
      (.clk(PCLK ), .reset_n (PRESETn),
     .start_event (write_enable04 & (PWDATA[2])),
     .test_expr   (reg_tx_overrun==1'b0)
     );

   // if write to INTCLEAR  with bit[3]=1, reg_rx_overrun will be cleared, unless a new overrun take place
    assert_next
    #(`OVL_ERROR, 1,1,0, `OVL_ASSERT,
    "rx buffer overrun should be clear when write to INTCLEAR, unless new overrun")
    u_ovl_rx_buffer_overrun_clear_a
      (.clk(PCLK ), .reset_n (PRESETn),
     .start_event (write_enable0c & (PWDATA[3]) & (~(rx_buf_full & (rx_state==9) & (nxt_rx_state==10)))),
     .test_expr   (reg_rx_overrun==1'b0)
     );

   // If rx buffer is not full, it cannot have new overrun
    assert_next
    #(`OVL_ERROR, 1,1,0, `OVL_ASSERT,
    "rx buffer overrun should be clear when write to INTCLEAR, unless new overrun")
    u_ovl_rx_buffer_overrun_when_empty
      (.clk(PCLK ), .reset_n (PRESETn),
     .start_event ((~rx_buf_full) & (reg_rx_overrun==1'b0)),
     .test_expr   (reg_rx_overrun==1'b0)
     );


   // Reading of reg_baud_div (worth checking due to two stage read mux)
    assert_next
    #(`OVL_ERROR, 1, 1, 0, `OVL_ASSERT,
    "Reading of baud rate divider value")
    u_ovl_read_baud_rate_divide_cfg
      (.clk(PCLK ), .reset_n (PRESETn),
     .start_event   (PSEL & (~PENABLE) & (~PWRITE) & (PADDR[11:2]==10'h004)),
     .test_expr     (PRDATA=={{12{1'b0}}, reg_baud_div})
     );

   // Recommended Baud Rate divider value is at least 16
   assert_never
     #(`OVL_ERROR,`OVL_ASSERT,
       "UART enabled with baud rate less than 16")
   u_ovl_baud_rate_divider_illegal
     (.clk(PCLK), .reset_n(PRESETn),
      .test_expr(((reg_ctrl[0]) & (reg_ctrl[6]==1'b0) & (reg_baud_div[19:4]=={16{1'b0}}) ) |
                 ((reg_ctrl[1]) &                       (reg_baud_div[19:4]=={16{1'b0}}) ) )
      );

   // Test mode never changes from hi-speed to normal speed unless TX is idle
   assert_never
     #(`OVL_ERROR,`OVL_ASSERT,
       "High speed test mode has been changed when TX was not idle")
   u_ovl_change_speed_tx_illegal
     (.clk(PCLK), .reset_n(PRESETn),
      .test_expr((tx_state != 4'd00) & (reg_ctrl[6] != ovl_last_reg_ctrl[6]))
      );

`endif

endmodule

12
HierarchyFilesModulesSignalsTasksFunctionsHelp

This page: Created:Wed Nov 16 11:46:42 2022
From: ../verilog/cmsdk_apb_usrt.v

Verilog converted to html by v2html 7.30.1.3 (written by Costas Calamvokis).Help