// 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
This page: |
Created: | Wed Apr 6 17:30:52 2022 |
|
From: |
../verilog/cmsdk_apb_uart_streamio.v |