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.

Register Log in

Stucked at UART formal verification

Status
Not open for further replies.
P

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
I have already added so many assert() at https://github.com/promach/UART/blob/development/rtl/test_UART.v , but during induction test, formal verification tool leads me straight to https://i.imgur.com/GNUAl7z.png which is the second last state during UART receiving mechanism at line 258 ?

Line 258 is about verifying the parity bit received against the parity value calculated from the received data, however, my coding failed this assert() test.

I am not sure what other assert() I should add before parity assertion. Could anyone advise ?

Screenshot from 2018-01-28 22-01-15.png

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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272

module test_UART(clk, reset, serial_out, enable, i_data, o_busy, received_data, data_is_valid, rx_error);
 
parameter INPUT_DATA_WIDTH = 8;
parameter PARITY_ENABLED = 1;
parameter PARITY_TYPE = 0;  // 0 = even parity, 1 = odd parity
 
input clk;
input reset;
 
// transmitter signals
input enable;
input [(INPUT_DATA_WIDTH-1):0] i_data;
output o_busy;
output serial_out;
 
`ifdef FORMAL
wire baud_clk;
wire [(INPUT_DATA_WIDTH+PARITY_ENABLED+1):0] shift_reg;  // Tx internal PISO
`endif
 
// receiver signals
wire serial_in;
output reg data_is_valid;
output reg rx_error;
output reg [(INPUT_DATA_WIDTH-1):0] received_data;
 
`ifdef FORMAL
localparam NUMBER_OF_BITS = INPUT_DATA_WIDTH + 3;   // 1 start bit, 8 data bits, 1 parity bit, 1 stop bit
wire [($clog2(NUMBER_OF_BITS)-1) : 0] state;  // for Rx
`endif
 
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)
`ifdef FORMAL
    , .state(state), .baud_clk(baud_clk), .shift_reg(shift_reg)
`endif
);
 
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
 
localparam Rx_IDLE       = 4'b0000;
localparam Rx_START_BIT  = 4'b0001;
localparam Rx_DATA_BIT_0 = 4'b0010;
localparam Rx_DATA_BIT_1 = 4'b0011;
localparam Rx_DATA_BIT_2 = 4'b0100;
localparam Rx_DATA_BIT_3 = 4'b0101;
localparam Rx_DATA_BIT_4 = 4'b0110;
localparam Rx_DATA_BIT_5 = 4'b0111;
localparam Rx_DATA_BIT_6 = 4'b1000;
localparam Rx_DATA_BIT_7 = 4'b1001;
localparam Rx_PARITY_BIT = 4'b1010;
localparam Rx_STOP_BIT   = 4'b1011;
 
localparam NUMBER_OF_RX_SYNCHRONIZERS = 3; // three FF synhronizers for clock domain crossing
localparam CLOCKS_PER_BIT = 8;
 
reg had_been_enabled;   // a signal to latch 'enable'
reg[($clog2(NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS)-1) : 0] cnt;  // to track the number of clock cycles incurred between assertion of 'transmission_had_started' signal from Tx and assertion of 'data_is_valid' signal from Rx
 
reg transmission_had_started; 
reg had_just_reset;
reg first_clock_passed;
 
initial begin
    had_been_enabled = 0;  
    cnt = 0;
    transmission_had_started = 0;
    had_just_reset = 0;
    first_clock_passed = 0;
end
 
always @(posedge clk)
begin
    first_clock_passed <= 1;
end
 
 
wire [($clog2(NUMBER_OF_BITS-1)-1) : 0] stop_bit_location;
assign stop_bit_location = (cnt < NUMBER_OF_BITS) ? (NUMBER_OF_BITS - 1 - cnt) : 0;  // if not during UART transmission, set to zero as default for no specific reason
 
wire [($clog2(NUMBER_OF_BITS)-1) : 0] stop_bit_location_plus_one = stop_bit_location + 1;
 
always @(posedge clk)
begin
    assert(cnt < NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS + 1);
    assert(stop_bit_location < NUMBER_OF_BITS);
    
    if(($past(first_clock_passed) == 0) && (first_clock_passed == 1)) begin
        assert($past(stop_bit_location) == (NUMBER_OF_BITS-1));
        assert($past(&shift_reg) == 1);
    end
end
 
always @(posedge clk)
begin
    if(reset) begin
        cnt <= 0;
        had_been_enabled <= 0;
        transmission_had_started <= 0;
    end
 
    else if(baud_clk) begin
        if(transmission_had_started) begin
            cnt <= cnt + 1;
        end
        transmission_had_started <= had_been_enabled;  // Tx only operates at every rising edge of 'baud_clk' (Tx's clock)
    end    
 
    else begin
 
        if(enable && (!had_been_enabled)) begin
            cnt <= 0;
            assert(cnt == 0);            
            had_been_enabled <= 1;
            assert(state == Rx_IDLE);
            assert(data_is_valid == 0);
            
            if(had_just_reset) begin
                assert(&shift_reg == 1);
            end
            
            assert(serial_out == 1);
            assert(o_busy == 0);
        end
 
        else if(transmission_had_started) begin
 
            if(cnt == 0) begin // start of UART transmission
                assert(state < Rx_STOP_BIT);
                assert(data_is_valid == 0);
                assert(shift_reg == {1'b0, 1'b1, (^i_data), i_data});  // ^data is even parity bit
                assert(serial_out == 0);   // start bit
                assert(o_busy == 1);
            end
            
            else if((cnt > 0) && (cnt < (NUMBER_OF_BITS-1))) begin  // during UART transmission
                assert(state < Rx_STOP_BIT);
                assert(data_is_valid == 0);
                assert(shift_reg[stop_bit_location_plus_one] == 1'b0);
                assert(shift_reg[stop_bit_location] == 1'b1);
                assert(o_busy == 1);                
            end
 
            else if(cnt == (NUMBER_OF_BITS - 1)) begin // end of UART transmission
                assert(state < Rx_STOP_BIT);
                assert(data_is_valid == 0);
                assert(shift_reg == 0);
                assert(serial_out == 1);   // stop bit
                assert(o_busy == 1);
            end
            
            else begin // if(cnt > ((NUMBER_OF_BITS + 1)*CLOCKS_PER_BIT)) begin  // UART Rx internal states
                
                if(state == Rx_START_BIT) begin
                    assert(data_is_valid == 0);
                    assert(serial_in == 0);
                    assert(o_busy == 1);
                    assert(cnt == (NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS + 1)*CLOCKS_PER_BIT);                    
                end
 
                else if((state > Rx_START_BIT) && (state < Rx_PARITY_BIT)) begin // data bits
                    assert(data_is_valid == 1);
                    assert(o_busy == 1);
                    assert(cnt == (NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS + (state - Rx_START_BIT) +  1)*CLOCKS_PER_BIT);                  
                end
    
                else if(state == Rx_PARITY_BIT) begin
                    assert(data_is_valid == 0);
                    assert(serial_in == ^i_data);
                    assert(o_busy == 1);
                    assert(cnt == (NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS + state +  1)*CLOCKS_PER_BIT);                   
                end
                        
                else begin // if(state == Rx_STOP_BIT) begin  // end of one UART transaction (both transmitting and receiving)
                    assert(state == Rx_STOP_BIT);
                    assert(data_is_valid == 1);
                    assert(serial_in == 1);
                    assert(o_busy == 0);
                    assert(cnt == (NUMBER_OF_BITS + NUMBER_OF_RX_SYNCHRONIZERS + 1)*CLOCKS_PER_BIT);
                    cnt <= 0;
                    had_been_enabled <= 0;
                end
                /*
                else begin
                    assert(state == Rx_IDLE);
                    assert(data_is_valid == 0);
                    assert(serial_in == 1); 
                end*/
            end
        end
            
        else begin  // UART Tx and Rx are idling, still waiting for baud_clk
            cnt <= 0;
            assert(cnt == 0);
            assert(state == Rx_IDLE);
            assert(data_is_valid == 0);
            assert(serial_out == 1);
            
            if(!had_been_enabled) begin
                assert(&shift_reg == 1);
            end
        end
    end
end
 
always @(posedge clk)
begin
    if(reset) begin
        had_just_reset <= 1;
        //assert();
    end
 
    else begin
        had_just_reset <= 0;
        
        if(!had_just_reset) begin
            if((had_been_enabled) && (!$past(had_been_enabled))) begin
                assert(!$past(o_busy));
                assert(o_busy);
            end
 
            else if((had_been_enabled) && ($past(had_been_enabled))) begin
                assert($past(o_busy));
                assert(o_busy);
            end
 
            else begin
                assert(!$past(o_busy));
                
                if($past(enable)) begin
                    assert(o_busy);
                end
 
                else begin
                    assert(!o_busy);
                end
 
                assert(serial_out == 1);
            end
        end
    end
end
 
always @(posedge clk)
begin
    if(reset | o_busy) begin
        assume(enable == 0);
    end
    
    if(enable | had_been_enabled) begin
        assume($past(i_data) == i_data);
    end
end
 
always @(posedge clk)
begin
    assert(!rx_error);   // no parity error
 
    if(data_is_valid) begin   // state == Rx_STOP_BIT
        assert(received_data == i_data);
        assert(cnt < NUMBER_OF_BITS*CLOCKS_PER_BIT);
    end
 
    if((!had_just_reset) && (state <= Rx_STOP_BIT) && (first_clock_passed) && (transmission_had_started) && ($past(transmission_had_started)) && ($past(baud_clk))) begin
        assert(cnt - $past(cnt) == 1);
    end
end
 
`endif
 
endmodule
 
Last edited:

I am already using assertion. What do you mean ? Could you be more exact by posting specific line of the UART code ?
 

These are inline assertions, they are Not SVA. Having assertions inline to code like this is not standard
Also, I doubt anyone here uses formal for verification. You may need to try somewhere else, like Mentor's verification academy
https://verificationacademy.com/topics

Is there any reason you are using formal? and not dynamic simulation?
 

promach said:
Besides, what comment do you have regarding https://verificationacademy.com/forums/systemverilog/stucked-uart-formal-verification#answer-65848 ?
Click to expand...

The guy mentions, your code has nothing to do with formal verification. Sounds substantiated.

I'm neither interested in formal verification, but in any case you have written some kind of test bench with failing parity check. How can this stimulation generate correct parity?
Code: 
assign serial_in = serial_out; // tx goes to rx, so that we know that our UART works at least in terms of logic-wise

- - - Updated - - -

If the DUT has both Rx and Tx channel, serial_in = serial_out can work. Your test has failed, to know why, you need to look into the DUT.
 


SVA has a very specific format. It is designed so that you can write the specifications for your design externally to the design. You can test signals directly, or create sequences you expect to happen during the test.

Here is an example spec:
1. When enable is high, response should be high 3 clocks later.
2. WHen enable is high, then byte enable should not be 0
3. If reset is asserted, then enable should be low on the next clock


Code Verilog - [expand]
1
2
3

A_RESPONSE_AFTER_3CLK : assert property ( @(posedge clk) enable |-> ##3 response );
A_BYTEEN_NOT_0 : assert property ( @(posedge clk) enable |-> (byte_en != 0 ) );
A_RST : assert property ( @(posedge clk) rst |=> ~enable );


That is SVA. Properties can be defined separately from asserts, and sequences can be defined for properties.
You can also define assumes and covers in a similar fashion.

The post on verification academy is correct - you are not really testing your design, you are testing the testbench. You are approaching this in completly the wrong way. How come you have access to a formal tool? Simulators are much much cheaper (some are free!) and probably more appropriate for a small UART. Formal tools are usually used by ASIC developers, for far more complex designs (and cost 10s of thousands of dollars a seat!)

Basics of SVA can be found here:
https://www.doulos.com/knowhow/sysverilog/tutorial/assertions/

- - - Updated - - -

DOulos are also running a webinar on SVA tomorrow: https://www.doulos.com/content/events/SVA_expert.php?pk_campaign=LastChance
 
you are not really testing your design, you are testing the testbench. You are approaching this in completly the wrong way.
Click to expand...

Would you be able to give a general direction in the context of UART on how my testbench should be written such that I am testing the design instead of the testbench ?
 

Status
Not open for further replies.

Similar threads

Part and Inventory Search

Welcome to EDABoard.com

Sponsor

Back
Top