promach
Advanced Member level 4
Anyone have any comments about "cover(data_is_valid);" at https://github.com/promach/UART/blob/development/rtl/test_UART.v#L40 ? I have error "Unreached cover statement at ../rtl/test_UART.v:40" . I am not sure what I have missed though
Could anyone advise on what I have missed in my UART design since the code had passed temporal inducton and bounded model check testings ?
Could anyone advise on what I have missed in my UART design since the code had passed temporal inducton and bounded model check testings ?
Code Verilog - [expand] 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 module test_UART(clk, reset, serial_out, enable, i_data, o_busy, received_data, data_is_valid, rx_error); parameter INPUT_DATA_WIDTH = 8; input clk; input reset; // transmitter signals input enable; input [(INPUT_DATA_WIDTH-1):0] i_data; output reg o_busy; output reg serial_out; // receiver signals output reg data_is_valid; output reg rx_error; output reg [(INPUT_DATA_WIDTH-1):0] received_data; wire serial_in; UART uart(.clk(clk), .reset(reset), .serial_out(serial_out), .enable(enable), .i_data(i_data), .o_busy(o_busy), .serial_in(serial_in), .received_data(received_data), .data_is_valid(data_is_valid), .rx_error(rx_error)); assign serial_in = serial_out; // tx goes to rx, so that we know that our UART works at least in terms of logic-wise `ifdef FORMAL initial begin assume(clk == 0); assume(enable == 0); assume(reset == 0); end reg has_been_enabled; always @(posedge clk) begin if(enable) has_been_enabled <= 1; if(has_been_enabled) cover(data_is_valid); end always @(posedge clk) begin if((!enable) || (data_is_valid)) assume($past(i_data) == i_data); if(o_busy) assume(enable == 0); assert(!rx_error); if(data_is_valid) assert(received_data == i_data); end `endif endmodule