Continue to Site

Welcome to EDAboard.com

Welcome to our site! EDAboard.com is an international Electronics Discussion Forum focused on EDA software, circuits, schematics, books, theory, papers, asic, pld, 8051, DSP, Network, RF, Analog Design, PCB, Service Manuals... and a whole lot more! To participate you need to register. Registration is free. Click here to register now.

Question on debugging bug in UART arised due to cover() failure

Status
Not open for further replies.

promach

Advanced Member level 4
Joined
Feb 22, 2016
Messages
1,199
Helped
2
Reputation
4
Reaction score
5
Trophy points
1,318
Activity points
11,636
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 ?


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

 

This seems to be very odd code. Even for formal.
I dont think the auther really knows what he's doing with SVA. I would avoid it.
Assumes, asserts and covers shouldnt really be in always blocks. You should create properties and then assert/assume/cover the properties.

Unless you're using a formal tool, ensure FORMAL is not `define d
 

this is weird but it looks like enable never rises, thus has_been_enabled never rises either. therefore you can't cover it.
 

@ThisIsNotSam

Do you understand why I have the signal 'has_been_enabled' ?

I suppose the cover statement is only being executed if and only if 'enabled' is ever HIGH.

In this case, how should I modify the cover() code ?
 

Covers are usually used in formal as test cases to ensure that some condition can actually occur. Here, you are covering the case that data_is_valid occurs 1 clock after enable.
Still, this really isnt the best way to write asserts and covers, especially not for formal.

You really should be writing them like this.


Code Verilog - [expand]
1
2
// Should be on it's own line, not inside an always
cover property( @(posedge clk) enable |=> data_is_valid );



Also, Im not sure you have proper understanding of assumes.
Assumes are there to minimise the cone of influence for inputs on outputs. Basically, narrowing down the test space. Your initial assumes are useless and not required.

Your formal should all be formatted like this:


Code Verilog - [expand]
1
2
3
4
5
6
7
assert property( !rx_error );
assert property( @(posedge clk) data_is_valid |-> (received_data == i_data) );
 
assume property( o_busy |-> (enable == 0) );
assume property( @(posedge clk) (!enable || data_is_valid ) |-> i_data == $past(i_data) );
 
cover property ( @(posedge clk) enable |=> data_is_valid );

 

Status
Not open for further replies.

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Back
Top