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 |