OpenCores
URL https://opencores.org/ocsvn/wbuart32/wbuart32/trunk

Subversion Repositories wbuart32

[/] [wbuart32/] [trunk/] [rtl/] [rxuartlite.v] - Blame information for rev 23

Go to most recent revision | Details | Compare with Previous | View Log

Line No. Rev Author Line
1 15 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    rxuartlite.v
4
//
5
// Project:     wbuart32, a full featured UART with simulator
6
//
7
// Purpose:     Receive and decode inputs from a single UART line.
8
//
9
//
10
//      To interface with this module, connect it to your system clock,
11
//      and a UART input.  Set the parameter to the number of clocks per
12
//      baud.  When data becomes available, the o_wr line will be asserted
13
//      for one clock cycle.
14
//
15
//      This interface only handles 8N1 serial port communications.  It does
16
//      not handle the break, parity, or frame error conditions.
17
//
18
//
19
// Creator:     Dan Gisselquist, Ph.D.
20
//              Gisselquist Technology, LLC
21
//
22
////////////////////////////////////////////////////////////////////////////////
23
//
24 21 dgisselq
// Copyright (C) 2015-2018, Gisselquist Technology, LLC
25 15 dgisselq
//
26
// This program is free software (firmware): you can redistribute it and/or
27
// modify it under the terms of  the GNU General Public License as published
28
// by the Free Software Foundation, either version 3 of the License, or (at
29
// your option) any later version.
30
//
31
// This program is distributed in the hope that it will be useful, but WITHOUT
32
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
33
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
34
// for more details.
35
//
36
// You should have received a copy of the GNU General Public License along
37
// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
38
// target there if the PDF file isn't present.)  If not, see
39
// <http://www.gnu.org/licenses/> for a copy.
40
//
41
// License:     GPL, v3, as defined and found on www.gnu.org,
42
//              http://www.gnu.org/licenses/gpl.html
43
//
44
//
45
////////////////////////////////////////////////////////////////////////////////
46
//
47
//
48 17 dgisselq
`default_nettype        none
49
//
50
`define RXUL_BIT_ZERO           4'h0
51
`define RXUL_BIT_ONE            4'h1
52
`define RXUL_BIT_TWO            4'h2
53
`define RXUL_BIT_THREE          4'h3
54
`define RXUL_BIT_FOUR           4'h4
55
`define RXUL_BIT_FIVE           4'h5
56
`define RXUL_BIT_SIX            4'h6
57
`define RXUL_BIT_SEVEN          4'h7
58
`define RXUL_STOP               4'h8
59 21 dgisselq
`define RXUL_WAIT               4'h9
60 17 dgisselq
`define RXUL_IDLE               4'hf
61 15 dgisselq
 
62
module rxuartlite(i_clk, i_uart_rx, o_wr, o_data);
63 21 dgisselq
        parameter                       TIMER_BITS = 10;
64
        parameter  [(TIMER_BITS-1):0]    CLOCKS_PER_BAUD = 868;  // 115200 MBaud at 100MHz
65
        localparam                      TB = TIMER_BITS;
66 17 dgisselq
        input   wire            i_clk;
67
        input   wire            i_uart_rx;
68 15 dgisselq
        output  reg             o_wr;
69
        output  reg     [7:0]    o_data;
70
 
71
 
72 21 dgisselq
        wire    [(TB-1):0]       half_baud;
73
        reg     [3:0]            state;
74 15 dgisselq
 
75 21 dgisselq
        assign  half_baud = { 1'b0, CLOCKS_PER_BAUD[(TB-1):1] };
76
        reg     [(TB-1):0]       baud_counter;
77
        reg                     zero_baud_counter;
78 15 dgisselq
 
79
 
80
        // Since this is an asynchronous receiver, we need to register our
81
        // input a couple of clocks over to avoid any problems with 
82
        // metastability.  We do that here, and then ignore all but the
83
        // ck_uart wire.
84
        reg     q_uart, qq_uart, ck_uart;
85 21 dgisselq
        initial q_uart  = 1'b1;
86
        initial qq_uart = 1'b1;
87
        initial ck_uart = 1'b1;
88 15 dgisselq
        always @(posedge i_clk)
89 21 dgisselq
                { ck_uart, qq_uart, q_uart } <= { qq_uart, q_uart, i_uart_rx };
90 15 dgisselq
 
91
        // Keep track of the number of clocks since the last change.
92
        //
93
        // This is used to determine if we are in either a break or an idle
94
        // condition, as discussed further below.
95 21 dgisselq
        reg     [(TB-1):0]       chg_counter;
96
        initial chg_counter = {(TB){1'b1}};
97 15 dgisselq
        always @(posedge i_clk)
98
                if (qq_uart != ck_uart)
99 21 dgisselq
                        chg_counter <= 0;
100
                else if (chg_counter != { (TB){1'b1} })
101 15 dgisselq
                        chg_counter <= chg_counter + 1;
102
 
103
        // Are we in the middle of a baud iterval?  Specifically, are we
104
        // in the middle of a start bit?  Set this to high if so.  We'll use
105
        // this within our state machine to transition out of the IDLE
106
        // state.
107
        reg     half_baud_time;
108
        initial half_baud_time = 0;
109
        always @(posedge i_clk)
110 21 dgisselq
                half_baud_time <= (!ck_uart)&&(chg_counter >= half_baud-1'b1-1'b1);
111 15 dgisselq
 
112
 
113 17 dgisselq
        initial state = `RXUL_IDLE;
114 15 dgisselq
        always @(posedge i_clk)
115
        begin
116 17 dgisselq
                if (state == `RXUL_IDLE)
117 15 dgisselq
                begin // Idle state, independent of baud counter
118
                        // By default, just stay in the IDLE state
119 17 dgisselq
                        state <= `RXUL_IDLE;
120 21 dgisselq
                        if ((!ck_uart)&&(half_baud_time))
121 15 dgisselq
                                // UNLESS: We are in the center of a valid
122
                                // start bit
123 17 dgisselq
                                state <= `RXUL_BIT_ZERO;
124 21 dgisselq
                end else if ((state >= `RXUL_WAIT)&&(ck_uart))
125
                        state <= `RXUL_IDLE;
126
                else if (zero_baud_counter)
127 15 dgisselq
                begin
128 21 dgisselq
                        if (state <= `RXUL_STOP)
129 15 dgisselq
                                // Data arrives least significant bit first.
130
                                // By the time this is clocked in, it's what
131
                                // you'll have.
132
                                state <= state + 1;
133
                end
134
        end
135
 
136
        // Data bit capture logic.
137
        //
138
        // This is drastically simplified from the state machine above, based
139
        // upon: 1) it doesn't matter what it is until the end of a captured
140
        // byte, and 2) the data register will flush itself of any invalid
141
        // data in all other cases.  Hence, let's keep it real simple.
142
        reg     [7:0]    data_reg;
143
        always @(posedge i_clk)
144 21 dgisselq
                if ((zero_baud_counter)&&(state != `RXUL_STOP))
145
                        data_reg <= { qq_uart, data_reg[7:1] };
146 15 dgisselq
 
147
        // Our data bit logic doesn't need nearly the complexity of all that
148
        // work above.  Indeed, we only need to know if we are at the end of
149
        // a stop bit, in which case we copy the data_reg into our output
150
        // data register, o_data, and tell others (for one clock) that data is
151
        // available.
152
        //
153 21 dgisselq
        initial o_wr = 1'b0;
154 15 dgisselq
        initial o_data = 8'h00;
155
        always @(posedge i_clk)
156 21 dgisselq
                if ((zero_baud_counter)&&(state == `RXUL_STOP)&&(ck_uart))
157 15 dgisselq
                begin
158
                        o_wr   <= 1'b1;
159
                        o_data <= data_reg;
160
                end else
161
                        o_wr   <= 1'b0;
162
 
163
        // The baud counter
164
        //
165
        // This is used as a "clock divider" if you will, but the clock needs
166
        // to be reset before any byte can be decoded.  In all other respects,
167 18 dgisselq
        // we set ourselves up for CLOCKS_PER_BAUD counts between baud
168 15 dgisselq
        // intervals.
169 21 dgisselq
        initial baud_counter = 0;
170 15 dgisselq
        always @(posedge i_clk)
171 21 dgisselq
                if (((state==`RXUL_IDLE))&&(!ck_uart)&&(half_baud_time))
172 15 dgisselq
                        baud_counter <= CLOCKS_PER_BAUD-1'b1;
173 21 dgisselq
                else if (state == `RXUL_WAIT)
174
                        baud_counter <= 0;
175
                else if ((zero_baud_counter)&&(state < `RXUL_STOP))
176
                        baud_counter <= CLOCKS_PER_BAUD-1'b1;
177
                else if (!zero_baud_counter)
178 15 dgisselq
                        baud_counter <= baud_counter-1'b1;
179
 
180
        // zero_baud_counter
181
        //
182
        // Rather than testing whether or not (baud_counter == 0) within our
183
        // (already too complicated) state transition tables, we use
184
        // zero_baud_counter to pre-charge that test on the clock
185
        // before--cleaning up some otherwise difficult timing dependencies.
186 21 dgisselq
        initial zero_baud_counter = 1'b1;
187 15 dgisselq
        always @(posedge i_clk)
188 21 dgisselq
                if ((state == `RXUL_IDLE)&&(!ck_uart)&&(half_baud_time))
189 15 dgisselq
                        zero_baud_counter <= 1'b0;
190 21 dgisselq
                else if (state == `RXUL_WAIT)
191
                        zero_baud_counter <= 1'b1;
192
                else if ((zero_baud_counter)&&(state < `RXUL_STOP))
193
                        zero_baud_counter <= 1'b0;
194
                else if (baud_counter == 1)
195
                        zero_baud_counter <= 1'b1;
196
 
197
`ifdef  FORMAL
198
`define FORMAL_VERILATOR
199
`else
200
`ifdef  VERILATOR
201
`define FORMAL_VERILATOR
202
`endif
203
`endif
204
 
205
`ifdef  FORMAL
206
 
207 23 dgisselq
`define ASSUME  assume
208
 
209 21 dgisselq
`define PHASE_ONE_ASSERT        assert
210
`define PHASE_TWO_ASSERT        assert
211
 
212
`ifdef  PHASE_TWO
213
`undef  PHASE_ONE_ASSERT
214
`define PHASE_ONE_ASSERT        assume
215
`endif
216
 
217
        localparam      F_CKRES = 10;
218
 
219
        wire                    f_tx_start, f_tx_busy;
220
        wire    [(F_CKRES-1):0]  f_tx_step;
221
        reg                     f_tx_zclk;
222
        reg     [(TB-1):0]       f_tx_timer;
223
        wire    [7:0]            f_rx_newdata;
224
        reg     [(TB-1):0]       f_tx_baud;
225
        wire                    f_tx_zbaud;
226
 
227
        wire    [(TB-1):0]       f_max_baud_difference;
228
        reg     [(TB-1):0]       f_baud_difference;
229
        reg     [(TB+3):0]       f_tx_count, f_rx_count;
230
        wire    [7:0]            f_tx_data;
231
 
232
 
233
 
234
        wire                    f_txclk;
235
        reg     [1:0]            f_rx_clock;
236
        reg     [(F_CKRES-1):0]  f_tx_clock;
237
        reg                     f_past_valid, f_past_valid_tx;
238
 
239
        initial f_past_valid = 1'b0;
240
        always @(posedge i_clk)
241
                f_past_valid <= 1'b1;
242
 
243 23 dgisselq
`ifdef  F_OPT_CLK2FFLOGIC
244 21 dgisselq
        initial f_rx_clock = 3'h0;
245
        always @($global_clock)
246
                f_rx_clock <= f_rx_clock + 1'b1;
247
 
248
        always @(*)
249
                assume(i_clk == f_rx_clock[1]);
250 23 dgisselq
`endif
251 21 dgisselq
 
252
 
253
 
254
        ///////////////////////////////////////////////////////////
255
        //
256
        //
257
        // Generate a transmitted signal
258
        //
259
        //
260
        ///////////////////////////////////////////////////////////
261
 
262
 
263
        // First, calculate the transmit clock
264
        localparam [(F_CKRES-1):0] F_MIDSTEP = { 2'b01, {(F_CKRES-2){1'b0}} };
265
        //
266
        // Need to allow us to slip by half a baud clock over 10 baud intervals
267
        //
268
        // (F_STEP / (2^F_CKRES)) * (CLOCKS_PER_BAUD)*10 < CLOCKS_PER_BAUD/2
269
        // F_STEP * 2 * 10 < 2^F_CKRES
270
        localparam [(F_CKRES-1):0] F_HALFSTEP= F_MIDSTEP/32;
271
        localparam [(F_CKRES-1):0] F_MINSTEP = F_MIDSTEP - F_HALFSTEP + 1;
272
        localparam [(F_CKRES-1):0] F_MAXSTEP = F_MIDSTEP + F_HALFSTEP - 1;
273
 
274
        initial assert(F_MINSTEP <= F_MIDSTEP);
275
        initial assert(F_MIDSTEP <= F_MAXSTEP);
276
 
277 23 dgisselq
`ifdef  F_OPT_CLK2FFLOGIC
278 21 dgisselq
        assign  f_tx_step = $anyconst;
279
        //      assume((f_tx_step >= F_MINSTEP)&&(f_tx_step <= F_MAXSTEP));
280
        //
281
        //
282
        always @(*) assume((f_tx_step == F_MINSTEP)
283
                        ||(f_tx_step == F_MIDSTEP)
284
                        ||(f_tx_step == F_MAXSTEP));
285
 
286
        // initial      rx_clock = $anyseq;
287
        always @($global_clock)
288
                f_tx_clock <= f_tx_clock + f_tx_step;
289
 
290
        assign  f_txclk = f_tx_clock[F_CKRES-1];
291 23 dgisselq
`else
292
        assign  f_tx_clk = i_clk;
293
`endif
294 21 dgisselq
        // 
295
        initial f_past_valid_tx = 1'b0;
296
        always @(posedge f_txclk)
297
                f_past_valid_tx <= 1'b1;
298
 
299
        initial assume(i_uart_rx);
300
 
301
 
302
        //////////////////////////////////////////////
303
        //
304
        //
305
        // Build a simulated transmitter
306
        //
307
        //
308
        //////////////////////////////////////////////
309
        //
310
        // First, the simulated timing generator
311
 
312
        // parameter    TIMER_BITS = 10;
313
        // parameter [(TIMER_BITS-1):0] CLOCKS_PER_BAUD = 868;
314
        // localparam   TB = TIMER_BITS;
315
 
316
        assign  f_tx_start = $anyseq;
317
        always @(*)
318
        if (f_tx_busy)
319
                assume(!f_tx_start);
320
 
321
        initial f_tx_baud = 0;
322
        always @(posedge f_txclk)
323
        if ((f_tx_zbaud)&&((f_tx_busy)||(f_tx_start)))
324
                f_tx_baud <= CLOCKS_PER_BAUD-1'b1;
325
        else if (!f_tx_zbaud)
326
                f_tx_baud <= f_tx_baud - 1'b1;
327
 
328
        always @(*)
329
                `PHASE_ONE_ASSERT(f_tx_baud < CLOCKS_PER_BAUD);
330
 
331
        always @(*)
332
        if (!f_tx_busy)
333
                `PHASE_ONE_ASSERT(f_tx_baud == 0);
334
 
335
        assign  f_tx_zbaud = (f_tx_baud == 0);
336
 
337
        // Pick some data to transmit
338
        assign  f_tx_data = $anyseq;
339
 
340
        // But only if we aren't busy
341
        initial assume(f_tx_data == 0);
342
        always @(posedge f_txclk)
343
        if ((!f_tx_zbaud)||(f_tx_busy)||(!f_tx_start))
344
                assume(f_tx_data == $past(f_tx_data));
345
 
346
        // Force the data to change on a clock only
347
        always @($global_clock)
348
        if ((f_past_valid)&&(!$rose(f_txclk)))
349
                assume($stable(f_tx_data));
350
        else if (f_tx_busy)
351
                assume($stable(f_tx_data));
352
 
353
        //
354
        always @($global_clock)
355
        if ((!f_past_valid)||(!$rose(f_txclk)))
356
        begin
357
                assume($stable(f_tx_start));
358
                assume($stable(f_tx_data));
359
        end
360
 
361
        //
362
        //
363
        //
364
 
365
        reg     [9:0]    f_tx_reg;
366
        reg             f_tx_busy;
367
 
368
        // Here's the transmitter itself (roughly)
369
        initial f_tx_busy   = 1'b0;
370
        initial f_tx_reg    = 0;
371
        always @(posedge f_txclk)
372
        if (!f_tx_zbaud)
373
        begin
374
                `PHASE_ONE_ASSERT(f_tx_busy);
375
        end else begin
376
                f_tx_reg  <= { 1'b0, f_tx_reg[9:1] };
377
                if (f_tx_start)
378
                        f_tx_reg <= { 1'b1, f_tx_data, 1'b0 };
379
        end
380
 
381
        // Create a busy flag that we'll use
382
        always @(*)
383
        if (!f_tx_zbaud)
384
                f_tx_busy <= 1'b1;
385
        else if (|f_tx_reg)
386
                f_tx_busy <= 1'b1;
387
        else
388
                f_tx_busy <= 1'b0;
389
 
390
        //
391
        // Tie the TX register to the TX data
392
        always @(posedge f_txclk)
393
        if (f_tx_reg[9])
394
                `PHASE_ONE_ASSERT(f_tx_reg[8:0] == { f_tx_data, 1'b0 });
395
        else if (f_tx_reg[8])
396
                `PHASE_ONE_ASSERT(f_tx_reg[7:0] == f_tx_data[7:0] );
397
        else if (f_tx_reg[7])
398
                `PHASE_ONE_ASSERT(f_tx_reg[6:0] == f_tx_data[7:1] );
399
        else if (f_tx_reg[6])
400
                `PHASE_ONE_ASSERT(f_tx_reg[5:0] == f_tx_data[7:2] );
401
        else if (f_tx_reg[5])
402
                `PHASE_ONE_ASSERT(f_tx_reg[4:0] == f_tx_data[7:3] );
403
        else if (f_tx_reg[4])
404
                `PHASE_ONE_ASSERT(f_tx_reg[3:0] == f_tx_data[7:4] );
405
        else if (f_tx_reg[3])
406
                `PHASE_ONE_ASSERT(f_tx_reg[2:0] == f_tx_data[7:5] );
407
        else if (f_tx_reg[2])
408
                `PHASE_ONE_ASSERT(f_tx_reg[1:0] == f_tx_data[7:6] );
409
        else if (f_tx_reg[1])
410
                `PHASE_ONE_ASSERT(f_tx_reg[0] == f_tx_data[7]);
411
 
412
        // Our counter since we start
413
        initial f_tx_count = 0;
414
        always @(posedge f_txclk)
415
        if (!f_tx_busy)
416
                f_tx_count <= 0;
417
        else
418
                f_tx_count <= f_tx_count + 1'b1;
419
 
420
        always @(*)
421
        if (f_tx_reg == 10'h0)
422
                assume(i_uart_rx);
423
        else
424
                assume(i_uart_rx == f_tx_reg[0]);
425
 
426
        //
427
        // Make sure the absolute transmit clock timer matches our state
428
        //
429
        always @(posedge f_txclk)
430
        if (!f_tx_busy)
431
        begin
432
                if ((!f_past_valid_tx)||(!$past(f_tx_busy)))
433
                        `PHASE_ONE_ASSERT(f_tx_count == 0);
434
        end else if (f_tx_reg[9])
435
                `PHASE_ONE_ASSERT(f_tx_count ==
436
                                    CLOCKS_PER_BAUD -1 -f_tx_baud);
437
        else if (f_tx_reg[8])
438
                `PHASE_ONE_ASSERT(f_tx_count ==
439
                                2 * CLOCKS_PER_BAUD -1 -f_tx_baud);
440
        else if (f_tx_reg[7])
441
                `PHASE_ONE_ASSERT(f_tx_count ==
442
                                3 * CLOCKS_PER_BAUD -1 -f_tx_baud);
443
        else if (f_tx_reg[6])
444
                `PHASE_ONE_ASSERT(f_tx_count ==
445
                                4 * CLOCKS_PER_BAUD -1 -f_tx_baud);
446
        else if (f_tx_reg[5])
447
                `PHASE_ONE_ASSERT(f_tx_count ==
448
                                5 * CLOCKS_PER_BAUD -1 -f_tx_baud);
449
        else if (f_tx_reg[4])
450
                `PHASE_ONE_ASSERT(f_tx_count ==
451
                                6 * CLOCKS_PER_BAUD -1 -f_tx_baud);
452
        else if (f_tx_reg[3])
453
                `PHASE_ONE_ASSERT(f_tx_count ==
454
                                7 * CLOCKS_PER_BAUD -1 -f_tx_baud);
455
        else if (f_tx_reg[2])
456
                `PHASE_ONE_ASSERT(f_tx_count ==
457
                                8 * CLOCKS_PER_BAUD -1 -f_tx_baud);
458
        else if (f_tx_reg[1])
459
                `PHASE_ONE_ASSERT(f_tx_count ==
460
                                9 * CLOCKS_PER_BAUD -1 -f_tx_baud);
461
        else if (f_tx_reg[0])
462
                `PHASE_ONE_ASSERT(f_tx_count ==
463
                                10 * CLOCKS_PER_BAUD -1 -f_tx_baud);
464
        else
465
                `PHASE_ONE_ASSERT(f_tx_count ==
466
                                11 * CLOCKS_PER_BAUD -1 -f_tx_baud);
467
 
468
 
469
        ///////////////////////////////////////
470
        //
471
        // Receiver
472
        //
473
        ///////////////////////////////////////
474
        //
475
        // Count RX clocks since the start of the first stop bit, measured in
476
        // rx clocks
477
        initial f_rx_count = 0;
478
        always @(posedge i_clk)
479
        if (state == `RXUL_IDLE)
480
                f_rx_count = (!ck_uart) ? (chg_counter+2) : 0;
481
        else
482
                f_rx_count <= f_rx_count + 1'b1;
483
        always @(posedge i_clk)
484
        if (state == 0)
485
                `PHASE_ONE_ASSERT(f_rx_count
486
                                == half_baud + (CLOCKS_PER_BAUD-baud_counter));
487
        else if (state == 1)
488
                `PHASE_ONE_ASSERT(f_rx_count == half_baud + 2 * CLOCKS_PER_BAUD
489
                                        - baud_counter);
490
        else if (state == 2)
491
                `PHASE_ONE_ASSERT(f_rx_count == half_baud + 3 * CLOCKS_PER_BAUD
492
                                        - baud_counter);
493
        else if (state == 3)
494
                `PHASE_ONE_ASSERT(f_rx_count == half_baud + 4 * CLOCKS_PER_BAUD
495
                                        - baud_counter);
496
        else if (state == 4)
497
                `PHASE_ONE_ASSERT(f_rx_count == half_baud + 5 * CLOCKS_PER_BAUD
498
                                        - baud_counter);
499
        else if (state == 5)
500
                `PHASE_ONE_ASSERT(f_rx_count == half_baud + 6 * CLOCKS_PER_BAUD
501
                                        - baud_counter);
502
        else if (state == 6)
503
                `PHASE_ONE_ASSERT(f_rx_count == half_baud + 7 * CLOCKS_PER_BAUD
504
                                        - baud_counter);
505
        else if (state == 7)
506
                `PHASE_ONE_ASSERT(f_rx_count == half_baud + 8 * CLOCKS_PER_BAUD
507
                                        - baud_counter);
508
        else if (state == 8)
509
                `PHASE_ONE_ASSERT((f_rx_count == half_baud + 9 * CLOCKS_PER_BAUD
510
                                        - baud_counter)
511
                        ||(f_rx_count == half_baud + 10 * CLOCKS_PER_BAUD
512
                                        - baud_counter));
513
 
514
        always @(*)
515
                `PHASE_ONE_ASSERT( ((!zero_baud_counter)
516
                                &&(state == `RXUL_IDLE)
517
                                &&(baud_counter == 0))
518
                        ||((zero_baud_counter)&&(baud_counter == 0))
519
                        ||((!zero_baud_counter)&&(baud_counter != 0)));
520
 
521
        always @(posedge i_clk)
522
        if (!f_past_valid)
523
                `PHASE_ONE_ASSERT((state == `RXUL_IDLE)&&(baud_counter == 0)
524
                        &&(zero_baud_counter));
525
 
526
        always @(*)
527
        begin
528
                `PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h2);
529
                `PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h4);
530
                `PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h5);
531
                `PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h6);
532
                `PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h9);
533
                `PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'ha);
534
                `PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'hb);
535
                `PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'hd);
536
        end
537
 
538
        always @(posedge i_clk)
539
        if ((f_past_valid)&&($past(state) >= `RXUL_WAIT)&&($past(ck_uart)))
540
                `PHASE_ONE_ASSERT(state == `RXUL_IDLE);
541
 
542
        always @(posedge i_clk)
543
        if ((f_past_valid)&&($past(state) >= `RXUL_WAIT)
544
                        &&(($past(state) != `RXUL_IDLE)||(state == `RXUL_IDLE)))
545
                `PHASE_ONE_ASSERT(zero_baud_counter);
546
 
547
        // Calculate an absolute value of the difference between the two baud
548
        // clocks
549
`ifdef  PHASE_TWO
550
        always @(posedge i_clk)
551
        if ((f_past_valid)&&($past(state)==`RXUL_IDLE)&&(state == `RXUL_IDLE))
552
        begin
553
                `PHASE_TWO_ASSERT(($past(ck_uart))
554
                        ||(chg_counter <=
555
                                { 1'b0, CLOCKS_PER_BAUD[(TB-1):1] }));
556
        end
557
 
558
        always @(posedge f_txclk)
559
        if (!f_past_valid_tx)
560
                `PHASE_TWO_ASSERT((state == `RXUL_IDLE)&&(baud_counter == 0)
561
                        &&(zero_baud_counter)&&(!f_tx_busy));
562
 
563
        wire    [(TB+3):0]       f_tx_count_two_clocks_ago;
564
        assign  f_tx_count_two_clocks_ago = f_tx_count - 2;
565
        always @(*)
566
        if (f_tx_count >= f_rx_count + 2)
567
                f_baud_difference = f_tx_count_two_clocks_ago - f_rx_count;
568
        else
569
                f_baud_difference = f_rx_count - f_tx_count_two_clocks_ago;
570
 
571
        localparam      F_SYNC_DLY = 8;
572
 
573
        wire    [(TB+4+F_CKRES-1):0]     f_sub_baud_difference;
574
        reg     [F_CKRES-1:0]    ck_tx_clock;
575
        reg     [((F_SYNC_DLY-1)*F_CKRES)-1:0]   q_tx_clock;
576
        reg     [TB+3:0] ck_tx_count;
577
        reg     [(F_SYNC_DLY-1)*(TB+4)-1:0]      q_tx_count;
578
        initial q_tx_count = 0;
579
        initial ck_tx_count = 0;
580
        initial q_tx_clock = 0;
581
        initial ck_tx_clock = 0;
582
        always @($global_clock)
583
                { ck_tx_clock, q_tx_clock } <= { q_tx_clock, f_tx_clock };
584
        always @($global_clock)
585
                { ck_tx_count, q_tx_count } <= { q_tx_count, f_tx_count };
586
 
587
 
588
        wire    [TB+4+F_CKRES-1:0]       f_ck_tx_time, f_rx_time;
589
        always @(*)
590
                f_ck_tx_time = { ck_tx_count, !ck_tx_clock[F_CKRES-1],
591
                                                ck_tx_clock[F_CKRES-2:0] };
592
        always @(*)
593
                f_rx_time = { f_rx_count, !f_rx_clock[1], f_rx_clock[0],
594
                                                {(F_CKRES-2){1'b0}} };
595
 
596
        wire    [TB+4+F_CKRES-1:0]       f_signed_difference;
597
        always @(*)
598
                f_signed_difference = f_ck_tx_time - f_rx_time;
599
 
600
        always @(*)
601
        if (f_signed_difference[TB+4+F_CKRES-1])
602
                f_sub_baud_difference = -f_signed_difference;
603
        else
604
                f_sub_baud_difference =  f_signed_difference;
605
 
606
        always @($global_clock)
607
        if (state == `RXUL_WAIT)
608
                `PHASE_TWO_ASSERT((!f_tx_busy)||(f_tx_reg[9:1] == 0));
609
 
610
        always @($global_clock)
611
        if (state == `RXUL_IDLE)
612
        begin
613
                `PHASE_TWO_ASSERT((!f_tx_busy)||(f_tx_reg[9])||(f_tx_reg[9:1]==0));
614
                if (!ck_uart)
615
                        ;//`PHASE_TWO_ASSERT((f_rx_count < 4)||(f_sub_baud_difference <= ((CLOCKS_PER_BAUD<<F_CKRES)/20)));
616 15 dgisselq
                else
617 21 dgisselq
                        `PHASE_TWO_ASSERT((f_tx_reg[9:1]==0)||(f_tx_count < (3 + CLOCKS_PER_BAUD/2)));
618
        end else if (state == 0)
619
                `PHASE_TWO_ASSERT(f_sub_baud_difference
620
                                <=  2 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
621
        else if (state == 1)
622
                `PHASE_TWO_ASSERT(f_sub_baud_difference
623
                                <=  3 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
624
        else if (state == 2)
625
                `PHASE_TWO_ASSERT(f_sub_baud_difference
626
                                <=  4 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
627
        else if (state == 3)
628
                `PHASE_TWO_ASSERT(f_sub_baud_difference
629
                                <=  5 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
630
        else if (state == 4)
631
                `PHASE_TWO_ASSERT(f_sub_baud_difference
632
                                <=  6 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
633
        else if (state == 5)
634
                `PHASE_TWO_ASSERT(f_sub_baud_difference
635
                                <=  7 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
636
        else if (state == 6)
637
                `PHASE_TWO_ASSERT(f_sub_baud_difference
638
                                <=  8 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
639
        else if (state == 7)
640
                `PHASE_TWO_ASSERT(f_sub_baud_difference
641
                                <=  9 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
642
        else if (state == 8)
643
                `PHASE_TWO_ASSERT(f_sub_baud_difference
644
                                <= 10 * ((CLOCKS_PER_BAUD<<F_CKRES)/20));
645 15 dgisselq
 
646 21 dgisselq
        always @(posedge i_clk)
647
        if (o_wr)
648
                `PHASE_TWO_ASSERT(o_data == $past(f_tx_data,4));
649 15 dgisselq
 
650 21 dgisselq
        // always @(posedge i_clk)
651
        // if ((zero_baud_counter)&&(state != 4'hf)&&(CLOCKS_PER_BAUD > 6))
652
                // assert(i_uart_rx == ck_uart);
653
 
654
        // Make sure the data register matches
655
        always @(posedge i_clk)
656
        // if ((f_past_valid)&&(state != $past(state)))
657
        begin
658
                if (state == 4'h0)
659
                        `PHASE_TWO_ASSERT(!data_reg[7]);
660
 
661
                if (state == 4'h1)
662
                        `PHASE_TWO_ASSERT((data_reg[7]
663
                                == $past(f_tx_data[0]))&&(!data_reg[6]));
664
 
665
                if (state == 4'h2)
666
                        `PHASE_TWO_ASSERT(data_reg[7:6]
667
                                        == $past(f_tx_data[1:0]));
668
 
669
                if (state == 4'h3)
670
                        `PHASE_TWO_ASSERT(data_reg[7:5] == $past(f_tx_data[2:0]));
671
 
672
                if (state == 4'h4)
673
                        `PHASE_TWO_ASSERT(data_reg[7:4] == $past(f_tx_data[3:0]));
674
 
675
                if (state == 4'h5)
676
                        `PHASE_TWO_ASSERT(data_reg[7:3] == $past(f_tx_data[4:0]));
677
 
678
                if (state == 4'h6)
679
                        `PHASE_TWO_ASSERT(data_reg[7:2] == $past(f_tx_data[5:0]));
680
 
681
                if (state == 4'h7)
682
                        `PHASE_TWO_ASSERT(data_reg[7:1] == $past(f_tx_data[6:0]));
683
 
684
                if (state == 4'h8)
685
                        `PHASE_TWO_ASSERT(data_reg[7:0] == $past(f_tx_data[7:0]));
686
        end
687
 
688
        always @(posedge i_clk)
689
                cover(o_wr);
690
`endif
691
`endif
692
`ifdef  FORMAL_VERILATOR
693
        // FORMAL properties which can be tested via Verilator as well as
694
        // Yosys FORMAL
695
        always @(*)
696
                assert((state == 4'hf)||(state <= `RXUL_WAIT));
697
        always @(*)
698
                assert(zero_baud_counter == (baud_counter == 0)? 1'b1:1'b0);
699
        always @(*)
700
                assert(baud_counter <= CLOCKS_PER_BAUD-1'b1);
701
 
702
`endif
703
 
704 15 dgisselq
endmodule
705
 
706
 

powered by: WebSVN 2.1.0

© copyright 1999-2024 OpenCores.org, equivalent to Oliscience, all rights reserved. OpenCores®, registered trademark.