URL
https://opencores.org/ocsvn/wbuart32/wbuart32/trunk
Subversion Repositories wbuart32
Compare Revisions
- This comparison shows the changes necessary to convert path
/wbuart32/trunk/rtl
- from Rev 24 to Rev 26
- ↔ Reverse comparison
Rev 24 → Rev 26
/Makefile
16,7 → 16,7
## |
################################################################################ |
## |
## Copyright (C) 2015-2016, Gisselquist Technology, LLC |
## Copyright (C) 2015-2019, Gisselquist Technology, LLC |
## |
## This program is free software (firmware): you can redistribute it and/or |
## modify it under the terms of the GNU General Public License as published |
39,7 → 39,7
################################################################################ |
## |
## |
all: test |
all: test tags |
YYMMDD=`date +%Y%m%d` |
CXX := g++ |
FBDIR := . |
53,36 → 53,31
test: $(VDIRFB)/Vtxuartlite__ALL.a |
test: $(VDIRFB)/Vrxuartlite__ALL.a |
|
$(VDIRFB)/Vrxuart__ALL.a: $(VDIRFB)/Vrxuart.h $(VDIRFB)/Vrxuart.cpp |
$(VDIRFB)/Vrxuart__ALL.a: $(VDIRFB)/Vrxuart.mk |
$(VDIRFB)/Vrxuart.h $(VDIRFB)/Vrxuart.cpp $(VDIRFB)/Vrxuart.mk: rxuart.v |
$(VDIRFB)/Vrxuart__ALL.a: $(VDIRFB)/Vrxuart.cpp |
$(VDIRFB)/Vtxuart__ALL.a: $(VDIRFB)/Vtxuart.cpp |
$(VDIRFB)/Vrxuartlite__ALL.a: $(VDIRFB)/Vrxuartlite.cpp |
$(VDIRFB)/Vtxuartlite__ALL.a: $(VDIRFB)/Vtxuartlite.cpp |
$(VDIRFB)/Vwbuart__ALL.a: $(VDIRFB)/Vwbuart.cpp |
|
$(VDIRFB)/Vrxuartlite__ALL.a: $(VDIRFB)/Vrxuartlite.h $(VDIRFB)/Vrxuartlite.cpp |
$(VDIRFB)/Vrxuartlite__ALL.a: $(VDIRFB)/Vrxuartlite.mk |
$(VDIRFB)/Vrxuartlite.h $(VDIRFB)/Vrxuartlite.cpp $(VDIRFB)/Vrxuartlite.mk: rxuartlite.v |
$(VDIRFB)/V%.mk: $(VDIRFB)/%.h |
$(VDIRFB)/V%.h: $(VDIRFB)/%.cpp |
$(VDIRFB)/V%.cpp: $(FBDIR)/%.v |
$(VERILATOR) --trace -MMD -Wall -cc $*.v |
|
$(VDIRFB)/Vtxuart__ALL.a: $(VDIRFB)/Vtxuart.h $(VDIRFB)/Vtxuart.cpp |
$(VDIRFB)/Vtxuart__ALL.a: $(VDIRFB)/Vtxuart.mk |
$(VDIRFB)/Vtxuart.h $(VDIRFB)/Vtxuart.cpp $(VDIRFB)/Vtxuart.mk: txuart.v |
|
$(VDIRFB)/Vtxuartlite__ALL.a: $(VDIRFB)/Vtxuartlite.h $(VDIRFB)/Vtxuartlite.cpp |
$(VDIRFB)/Vtxuartlite__ALL.a: $(VDIRFB)/Vtxuartlite.mk |
$(VDIRFB)/Vtxuartlite.h $(VDIRFB)/Vtxuartlite.cpp $(VDIRFB)/Vtxuartlite.mk: txuartlite.v |
|
$(VDIRFB)/Vwbuart__ALL.a: $(VDIRFB)/Vwbuart.h $(VDIRFB)/Vwbuart.cpp |
$(VDIRFB)/Vwbuart__ALL.a: $(VDIRFB)/Vwbuart.mk |
$(VDIRFB)/Vwbuart.h $(VDIRFB)/Vwbuart.cpp $(VDIRFB)/Vwbuart.mk: wbuart.v ufifo.v txuart.v rxuart.v |
|
$(VDIRFB)/V%.cpp $(VDIRFB)/V%.h $(VDIRFB)/V%.mk: $(FBDIR)/%.v |
$(VERILATOR) -Wall -cc $*.v |
|
$(VDIRFB)/V%__ALL.a: $(VDIRFB)/V%.mk |
cd $(VDIRFB); make -f V$*.mk |
|
tags: $(wildcard *.v) |
ctags *.v |
|
.PHONY: clean |
clean: |
rm -rf $(VDIRFB)/*.mk |
rm -rf $(VDIRFB)/*.cpp |
rm -rf $(VDIRFB)/*.h |
rm -rf $(VDIRFB)/ |
rm -rf tags $(VDIRFB)/ |
|
DEPS := $(wildcard $(VDIRFB)/*.d) |
|
ifneq ($(MAKECMDGOALS),clean) |
ifneq ($(DEPS),) |
include $(DEPS) |
endif |
endif |
/rxuart.v
65,7 → 65,7
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// Copyright (C) 2015-2016, Gisselquist Technology, LLC |
// Copyright (C) 2015-2019, Gisselquist Technology, LLC |
// |
// This program is free software (firmware): you can redistribute it and/or |
// modify it under the terms of the GNU General Public License as published |
/rxuartlite.v
21,7 → 21,7
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// Copyright (C) 2015-2018, Gisselquist Technology, LLC |
// Copyright (C) 2015-2019, Gisselquist Technology, LLC |
// |
// This program is free software (firmware): you can redistribute it and/or |
// modify it under the terms of the GNU General Public License as published |
61,7 → 61,11
|
module rxuartlite(i_clk, i_uart_rx, o_wr, o_data); |
parameter TIMER_BITS = 10; |
`ifdef FORMAL |
parameter [(TIMER_BITS-1):0] CLOCKS_PER_BAUD = 16; // Necessary for formal proof |
`else |
parameter [(TIMER_BITS-1):0] CLOCKS_PER_BAUD = 868; // 115200 MBaud at 100MHz |
`endif |
localparam TB = TIMER_BITS; |
input wire i_clk; |
input wire i_uart_rx; |
95,10 → 99,10
reg [(TB-1):0] chg_counter; |
initial chg_counter = {(TB){1'b1}}; |
always @(posedge i_clk) |
if (qq_uart != ck_uart) |
chg_counter <= 0; |
else if (chg_counter != { (TB){1'b1} }) |
chg_counter <= chg_counter + 1; |
if (qq_uart != ck_uart) |
chg_counter <= 0; |
else if (chg_counter != { (TB){1'b1} }) |
chg_counter <= chg_counter + 1; |
|
// Are we in the middle of a baud iterval? Specifically, are we |
// in the middle of a start bit? Set this to high if so. We'll use |
112,25 → 116,23
|
initial state = `RXUL_IDLE; |
always @(posedge i_clk) |
if (state == `RXUL_IDLE) |
begin // Idle state, independent of baud counter |
// By default, just stay in the IDLE state |
state <= `RXUL_IDLE; |
if ((!ck_uart)&&(half_baud_time)) |
// UNLESS: We are in the center of a valid |
// start bit |
state <= `RXUL_BIT_ZERO; |
end else if ((state >= `RXUL_WAIT)&&(ck_uart)) |
state <= `RXUL_IDLE; |
else if (zero_baud_counter) |
begin |
if (state == `RXUL_IDLE) |
begin // Idle state, independent of baud counter |
// By default, just stay in the IDLE state |
state <= `RXUL_IDLE; |
if ((!ck_uart)&&(half_baud_time)) |
// UNLESS: We are in the center of a valid |
// start bit |
state <= `RXUL_BIT_ZERO; |
end else if ((state >= `RXUL_WAIT)&&(ck_uart)) |
state <= `RXUL_IDLE; |
else if (zero_baud_counter) |
begin |
if (state <= `RXUL_STOP) |
// Data arrives least significant bit first. |
// By the time this is clocked in, it's what |
// you'll have. |
state <= state + 1; |
end |
if (state <= `RXUL_STOP) |
// Data arrives least significant bit first. |
// By the time this is clocked in, it's what |
// you'll have. |
state <= state + 1; |
end |
|
// Data bit capture logic. |
141,8 → 143,8
// data in all other cases. Hence, let's keep it real simple. |
reg [7:0] data_reg; |
always @(posedge i_clk) |
if ((zero_baud_counter)&&(state != `RXUL_STOP)) |
data_reg <= { qq_uart, data_reg[7:1] }; |
if ((zero_baud_counter)&&(state != `RXUL_STOP)) |
data_reg <= { qq_uart, data_reg[7:1] }; |
|
// Our data bit logic doesn't need nearly the complexity of all that |
// work above. Indeed, we only need to know if we are at the end of |
153,12 → 155,12
initial o_wr = 1'b0; |
initial o_data = 8'h00; |
always @(posedge i_clk) |
if ((zero_baud_counter)&&(state == `RXUL_STOP)&&(ck_uart)) |
begin |
o_wr <= 1'b1; |
o_data <= data_reg; |
end else |
o_wr <= 1'b0; |
if ((zero_baud_counter)&&(state == `RXUL_STOP)&&(ck_uart)) |
begin |
o_wr <= 1'b1; |
o_data <= data_reg; |
end else |
o_wr <= 1'b0; |
|
// The baud counter |
// |
168,14 → 170,14
// intervals. |
initial baud_counter = 0; |
always @(posedge i_clk) |
if (((state==`RXUL_IDLE))&&(!ck_uart)&&(half_baud_time)) |
baud_counter <= CLOCKS_PER_BAUD-1'b1; |
else if (state == `RXUL_WAIT) |
baud_counter <= 0; |
else if ((zero_baud_counter)&&(state < `RXUL_STOP)) |
baud_counter <= CLOCKS_PER_BAUD-1'b1; |
else if (!zero_baud_counter) |
baud_counter <= baud_counter-1'b1; |
if (((state==`RXUL_IDLE))&&(!ck_uart)&&(half_baud_time)) |
baud_counter <= CLOCKS_PER_BAUD-1'b1; |
else if (state == `RXUL_WAIT) |
baud_counter <= 0; |
else if ((zero_baud_counter)&&(state < `RXUL_STOP)) |
baud_counter <= CLOCKS_PER_BAUD-1'b1; |
else if (!zero_baud_counter) |
baud_counter <= baud_counter-1'b1; |
|
// zero_baud_counter |
// |
185,14 → 187,14
// before--cleaning up some otherwise difficult timing dependencies. |
initial zero_baud_counter = 1'b1; |
always @(posedge i_clk) |
if ((state == `RXUL_IDLE)&&(!ck_uart)&&(half_baud_time)) |
zero_baud_counter <= 1'b0; |
else if (state == `RXUL_WAIT) |
zero_baud_counter <= 1'b1; |
else if ((zero_baud_counter)&&(state < `RXUL_STOP)) |
zero_baud_counter <= 1'b0; |
else if (baud_counter == 1) |
zero_baud_counter <= 1'b1; |
if ((state == `RXUL_IDLE)&&(!ck_uart)&&(half_baud_time)) |
zero_baud_counter <= 1'b0; |
else if (state == `RXUL_WAIT) |
zero_baud_counter <= 1'b1; |
else if ((zero_baud_counter)&&(state < `RXUL_STOP)) |
zero_baud_counter <= 1'b0; |
else if (baud_counter == 1) |
zero_baud_counter <= 1'b1; |
|
`ifdef FORMAL |
`define FORMAL_VERILATOR |
203,21 → 205,18
`endif |
|
`ifdef FORMAL |
|
`define ASSUME assume |
`define ASSERT assert |
`ifdef VERIFIC |
(* gclk *) wire gbl_clk; |
global clocking @(posedge gbl_clk); endclocking |
`endif |
|
`define PHASE_ONE_ASSERT assert |
`define PHASE_TWO_ASSERT assert |
|
`ifdef PHASE_TWO |
`undef PHASE_ONE_ASSERT |
`define PHASE_ONE_ASSERT assume |
`endif |
|
localparam F_CKRES = 10; |
|
wire f_tx_start, f_tx_busy; |
wire [(F_CKRES-1):0] f_tx_step; |
(* anyseq *) wire f_tx_start; |
(* anyconst *) wire [(F_CKRES-1):0] f_tx_step; |
reg f_tx_zclk; |
reg [(TB-1):0] f_tx_timer; |
wire [7:0] f_rx_newdata; |
227,7 → 226,7
wire [(TB-1):0] f_max_baud_difference; |
reg [(TB-1):0] f_baud_difference; |
reg [(TB+3):0] f_tx_count, f_rx_count; |
wire [7:0] f_tx_data; |
(* anyseq *) wire [7:0] f_tx_data; |
|
|
|
240,7 → 239,6
always @(posedge i_clk) |
f_past_valid <= 1'b1; |
|
`ifdef F_OPT_CLK2FFLOGIC |
initial f_rx_clock = 3'h0; |
always @($global_clock) |
f_rx_clock <= f_rx_clock + 1'b1; |
247,7 → 245,6
|
always @(*) |
assume(i_clk == f_rx_clock[1]); |
`endif |
|
|
|
274,8 → 271,6
initial assert(F_MINSTEP <= F_MIDSTEP); |
initial assert(F_MIDSTEP <= F_MAXSTEP); |
|
`ifdef F_OPT_CLK2FFLOGIC |
assign f_tx_step = $anyconst; |
// assume((f_tx_step >= F_MINSTEP)&&(f_tx_step <= F_MAXSTEP)); |
// |
// |
283,14 → 278,10
||(f_tx_step == F_MIDSTEP) |
||(f_tx_step == F_MAXSTEP)); |
|
// initial rx_clock = $anyseq; |
always @($global_clock) |
f_tx_clock <= f_tx_clock + f_tx_step; |
|
assign f_txclk = f_tx_clock[F_CKRES-1]; |
`else |
assign f_tx_clk = i_clk; |
`endif |
// |
initial f_past_valid_tx = 1'b0; |
always @(posedge f_txclk) |
313,7 → 304,6
// parameter [(TIMER_BITS-1):0] CLOCKS_PER_BAUD = 868; |
// localparam TB = TIMER_BITS; |
|
assign f_tx_start = $anyseq; |
always @(*) |
if (f_tx_busy) |
assume(!f_tx_start); |
326,17 → 316,14
f_tx_baud <= f_tx_baud - 1'b1; |
|
always @(*) |
`PHASE_ONE_ASSERT(f_tx_baud < CLOCKS_PER_BAUD); |
`ASSERT(f_tx_baud < CLOCKS_PER_BAUD); |
|
always @(*) |
if (!f_tx_busy) |
`PHASE_ONE_ASSERT(f_tx_baud == 0); |
`ASSERT(f_tx_baud == 0); |
|
assign f_tx_zbaud = (f_tx_baud == 0); |
|
// Pick some data to transmit |
assign f_tx_data = $anyseq; |
|
// But only if we aren't busy |
initial assume(f_tx_data == 0); |
always @(posedge f_txclk) |
371,7 → 358,7
always @(posedge f_txclk) |
if (!f_tx_zbaud) |
begin |
`PHASE_ONE_ASSERT(f_tx_busy); |
`ASSERT(f_tx_busy); |
end else begin |
f_tx_reg <= { 1'b0, f_tx_reg[9:1] }; |
if (f_tx_start) |
391,23 → 378,23
// Tie the TX register to the TX data |
always @(posedge f_txclk) |
if (f_tx_reg[9]) |
`PHASE_ONE_ASSERT(f_tx_reg[8:0] == { f_tx_data, 1'b0 }); |
`ASSERT(f_tx_reg[8:0] == { f_tx_data, 1'b0 }); |
else if (f_tx_reg[8]) |
`PHASE_ONE_ASSERT(f_tx_reg[7:0] == f_tx_data[7:0] ); |
`ASSERT(f_tx_reg[7:0] == f_tx_data[7:0] ); |
else if (f_tx_reg[7]) |
`PHASE_ONE_ASSERT(f_tx_reg[6:0] == f_tx_data[7:1] ); |
`ASSERT(f_tx_reg[6:0] == f_tx_data[7:1] ); |
else if (f_tx_reg[6]) |
`PHASE_ONE_ASSERT(f_tx_reg[5:0] == f_tx_data[7:2] ); |
`ASSERT(f_tx_reg[5:0] == f_tx_data[7:2] ); |
else if (f_tx_reg[5]) |
`PHASE_ONE_ASSERT(f_tx_reg[4:0] == f_tx_data[7:3] ); |
`ASSERT(f_tx_reg[4:0] == f_tx_data[7:3] ); |
else if (f_tx_reg[4]) |
`PHASE_ONE_ASSERT(f_tx_reg[3:0] == f_tx_data[7:4] ); |
`ASSERT(f_tx_reg[3:0] == f_tx_data[7:4] ); |
else if (f_tx_reg[3]) |
`PHASE_ONE_ASSERT(f_tx_reg[2:0] == f_tx_data[7:5] ); |
`ASSERT(f_tx_reg[2:0] == f_tx_data[7:5] ); |
else if (f_tx_reg[2]) |
`PHASE_ONE_ASSERT(f_tx_reg[1:0] == f_tx_data[7:6] ); |
`ASSERT(f_tx_reg[1:0] == f_tx_data[7:6] ); |
else if (f_tx_reg[1]) |
`PHASE_ONE_ASSERT(f_tx_reg[0] == f_tx_data[7]); |
`ASSERT(f_tx_reg[0] == f_tx_data[7]); |
|
// Our counter since we start |
initial f_tx_count = 0; |
430,39 → 417,39
if (!f_tx_busy) |
begin |
if ((!f_past_valid_tx)||(!$past(f_tx_busy))) |
`PHASE_ONE_ASSERT(f_tx_count == 0); |
`ASSERT(f_tx_count == 0); |
end else if (f_tx_reg[9]) |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
CLOCKS_PER_BAUD -1 -f_tx_baud); |
else if (f_tx_reg[8]) |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
2 * CLOCKS_PER_BAUD -1 -f_tx_baud); |
else if (f_tx_reg[7]) |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
3 * CLOCKS_PER_BAUD -1 -f_tx_baud); |
else if (f_tx_reg[6]) |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
4 * CLOCKS_PER_BAUD -1 -f_tx_baud); |
else if (f_tx_reg[5]) |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
5 * CLOCKS_PER_BAUD -1 -f_tx_baud); |
else if (f_tx_reg[4]) |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
6 * CLOCKS_PER_BAUD -1 -f_tx_baud); |
else if (f_tx_reg[3]) |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
7 * CLOCKS_PER_BAUD -1 -f_tx_baud); |
else if (f_tx_reg[2]) |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
8 * CLOCKS_PER_BAUD -1 -f_tx_baud); |
else if (f_tx_reg[1]) |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
9 * CLOCKS_PER_BAUD -1 -f_tx_baud); |
else if (f_tx_reg[0]) |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
10 * CLOCKS_PER_BAUD -1 -f_tx_baud); |
else |
`PHASE_ONE_ASSERT(f_tx_count == |
`ASSERT(f_tx_count == |
11 * CLOCKS_PER_BAUD -1 -f_tx_baud); |
|
|
482,37 → 469,37
f_rx_count <= f_rx_count + 1'b1; |
always @(posedge i_clk) |
if (state == 0) |
`PHASE_ONE_ASSERT(f_rx_count |
`ASSERT(f_rx_count |
== half_baud + (CLOCKS_PER_BAUD-baud_counter)); |
else if (state == 1) |
`PHASE_ONE_ASSERT(f_rx_count == half_baud + 2 * CLOCKS_PER_BAUD |
`ASSERT(f_rx_count == half_baud + 2 * CLOCKS_PER_BAUD |
- baud_counter); |
else if (state == 2) |
`PHASE_ONE_ASSERT(f_rx_count == half_baud + 3 * CLOCKS_PER_BAUD |
`ASSERT(f_rx_count == half_baud + 3 * CLOCKS_PER_BAUD |
- baud_counter); |
else if (state == 3) |
`PHASE_ONE_ASSERT(f_rx_count == half_baud + 4 * CLOCKS_PER_BAUD |
`ASSERT(f_rx_count == half_baud + 4 * CLOCKS_PER_BAUD |
- baud_counter); |
else if (state == 4) |
`PHASE_ONE_ASSERT(f_rx_count == half_baud + 5 * CLOCKS_PER_BAUD |
`ASSERT(f_rx_count == half_baud + 5 * CLOCKS_PER_BAUD |
- baud_counter); |
else if (state == 5) |
`PHASE_ONE_ASSERT(f_rx_count == half_baud + 6 * CLOCKS_PER_BAUD |
`ASSERT(f_rx_count == half_baud + 6 * CLOCKS_PER_BAUD |
- baud_counter); |
else if (state == 6) |
`PHASE_ONE_ASSERT(f_rx_count == half_baud + 7 * CLOCKS_PER_BAUD |
`ASSERT(f_rx_count == half_baud + 7 * CLOCKS_PER_BAUD |
- baud_counter); |
else if (state == 7) |
`PHASE_ONE_ASSERT(f_rx_count == half_baud + 8 * CLOCKS_PER_BAUD |
`ASSERT(f_rx_count == half_baud + 8 * CLOCKS_PER_BAUD |
- baud_counter); |
else if (state == 8) |
`PHASE_ONE_ASSERT((f_rx_count == half_baud + 9 * CLOCKS_PER_BAUD |
`ASSERT((f_rx_count == half_baud + 9 * CLOCKS_PER_BAUD |
- baud_counter) |
||(f_rx_count == half_baud + 10 * CLOCKS_PER_BAUD |
- baud_counter)); |
|
always @(*) |
`PHASE_ONE_ASSERT( ((!zero_baud_counter) |
`ASSERT( ((!zero_baud_counter) |
&&(state == `RXUL_IDLE) |
&&(baud_counter == 0)) |
||((zero_baud_counter)&&(baud_counter == 0)) |
520,37 → 507,36
|
always @(posedge i_clk) |
if (!f_past_valid) |
`PHASE_ONE_ASSERT((state == `RXUL_IDLE)&&(baud_counter == 0) |
`ASSERT((state == `RXUL_IDLE)&&(baud_counter == 0) |
&&(zero_baud_counter)); |
|
always @(*) |
begin |
`PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h2); |
`PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h4); |
`PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h5); |
`PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h6); |
`PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h9); |
`PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'ha); |
`PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'hb); |
`PHASE_ONE_ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'hd); |
`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h2); |
`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h4); |
`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h5); |
`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h6); |
`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'h9); |
`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'ha); |
`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'hb); |
`ASSERT({ ck_uart,qq_uart,q_uart,i_uart_rx } != 4'hd); |
end |
|
always @(posedge i_clk) |
if ((f_past_valid)&&($past(state) >= `RXUL_WAIT)&&($past(ck_uart))) |
`PHASE_ONE_ASSERT(state == `RXUL_IDLE); |
`ASSERT(state == `RXUL_IDLE); |
|
always @(posedge i_clk) |
if ((f_past_valid)&&($past(state) >= `RXUL_WAIT) |
&&(($past(state) != `RXUL_IDLE)||(state == `RXUL_IDLE))) |
`PHASE_ONE_ASSERT(zero_baud_counter); |
`ASSERT(zero_baud_counter); |
|
// Calculate an absolute value of the difference between the two baud |
// clocks |
`ifdef PHASE_TWO |
always @(posedge i_clk) |
if ((f_past_valid)&&($past(state)==`RXUL_IDLE)&&(state == `RXUL_IDLE)) |
begin |
`PHASE_TWO_ASSERT(($past(ck_uart)) |
`ASSERT(($past(ck_uart)) |
||(chg_counter <= |
{ 1'b0, CLOCKS_PER_BAUD[(TB-1):1] })); |
end |
557,7 → 543,7
|
always @(posedge f_txclk) |
if (!f_past_valid_tx) |
`PHASE_TWO_ASSERT((state == `RXUL_IDLE)&&(baud_counter == 0) |
`ASSERT((state == `RXUL_IDLE)&&(baud_counter == 0) |
&&(zero_baud_counter)&&(!f_tx_busy)); |
|
wire [(TB+3):0] f_tx_count_two_clocks_ago; |
570,7 → 556,7
|
localparam F_SYNC_DLY = 8; |
|
wire [(TB+4+F_CKRES-1):0] f_sub_baud_difference; |
reg [(TB+4+F_CKRES-1):0] f_sub_baud_difference; |
reg [F_CKRES-1:0] ck_tx_clock; |
reg [((F_SYNC_DLY-1)*F_CKRES)-1:0] q_tx_clock; |
reg [TB+3:0] ck_tx_count; |
585,7 → 571,7
{ ck_tx_count, q_tx_count } <= { q_tx_count, f_tx_count }; |
|
|
wire [TB+4+F_CKRES-1:0] f_ck_tx_time, f_rx_time; |
reg [TB+4+F_CKRES-1:0] f_ck_tx_time, f_rx_time; |
always @(*) |
f_ck_tx_time = { ck_tx_count, !ck_tx_clock[F_CKRES-1], |
ck_tx_clock[F_CKRES-2:0] }; |
593,7 → 579,7
f_rx_time = { f_rx_count, !f_rx_clock[1], f_rx_clock[0], |
{(F_CKRES-2){1'b0}} }; |
|
wire [TB+4+F_CKRES-1:0] f_signed_difference; |
reg [TB+4+F_CKRES-1:0] f_signed_difference; |
always @(*) |
f_signed_difference = f_ck_tx_time - f_rx_time; |
|
605,47 → 591,47
|
always @($global_clock) |
if (state == `RXUL_WAIT) |
`PHASE_TWO_ASSERT((!f_tx_busy)||(f_tx_reg[9:1] == 0)); |
`ASSERT((!f_tx_busy)||(f_tx_reg[9:1] == 0)); |
|
always @($global_clock) |
if (state == `RXUL_IDLE) |
begin |
`PHASE_TWO_ASSERT((!f_tx_busy)||(f_tx_reg[9])||(f_tx_reg[9:1]==0)); |
`ASSERT((!f_tx_busy)||(f_tx_reg[9])||(f_tx_reg[9:1]==0)); |
if (!ck_uart) |
;//`PHASE_TWO_ASSERT((f_rx_count < 4)||(f_sub_baud_difference <= ((CLOCKS_PER_BAUD<<F_CKRES)/20))); |
else |
`PHASE_TWO_ASSERT((f_tx_reg[9:1]==0)||(f_tx_count < (3 + CLOCKS_PER_BAUD/2))); |
`ASSERT((f_tx_reg[9:1]==0)||(f_tx_count < (3 + CLOCKS_PER_BAUD/2))); |
end else if (state == 0) |
`PHASE_TWO_ASSERT(f_sub_baud_difference |
`ASSERT(f_sub_baud_difference |
<= 2 * ((CLOCKS_PER_BAUD<<F_CKRES)/20)); |
else if (state == 1) |
`PHASE_TWO_ASSERT(f_sub_baud_difference |
`ASSERT(f_sub_baud_difference |
<= 3 * ((CLOCKS_PER_BAUD<<F_CKRES)/20)); |
else if (state == 2) |
`PHASE_TWO_ASSERT(f_sub_baud_difference |
`ASSERT(f_sub_baud_difference |
<= 4 * ((CLOCKS_PER_BAUD<<F_CKRES)/20)); |
else if (state == 3) |
`PHASE_TWO_ASSERT(f_sub_baud_difference |
`ASSERT(f_sub_baud_difference |
<= 5 * ((CLOCKS_PER_BAUD<<F_CKRES)/20)); |
else if (state == 4) |
`PHASE_TWO_ASSERT(f_sub_baud_difference |
`ASSERT(f_sub_baud_difference |
<= 6 * ((CLOCKS_PER_BAUD<<F_CKRES)/20)); |
else if (state == 5) |
`PHASE_TWO_ASSERT(f_sub_baud_difference |
`ASSERT(f_sub_baud_difference |
<= 7 * ((CLOCKS_PER_BAUD<<F_CKRES)/20)); |
else if (state == 6) |
`PHASE_TWO_ASSERT(f_sub_baud_difference |
`ASSERT(f_sub_baud_difference |
<= 8 * ((CLOCKS_PER_BAUD<<F_CKRES)/20)); |
else if (state == 7) |
`PHASE_TWO_ASSERT(f_sub_baud_difference |
`ASSERT(f_sub_baud_difference |
<= 9 * ((CLOCKS_PER_BAUD<<F_CKRES)/20)); |
else if (state == 8) |
`PHASE_TWO_ASSERT(f_sub_baud_difference |
`ASSERT(f_sub_baud_difference |
<= 10 * ((CLOCKS_PER_BAUD<<F_CKRES)/20)); |
|
always @(posedge i_clk) |
if (o_wr) |
`PHASE_TWO_ASSERT(o_data == $past(f_tx_data,4)); |
`ASSERT(o_data == $past(f_tx_data,4)); |
|
// always @(posedge i_clk) |
// if ((zero_baud_counter)&&(state != 4'hf)&&(CLOCKS_PER_BAUD > 6)) |
656,39 → 642,60
// if ((f_past_valid)&&(state != $past(state))) |
begin |
if (state == 4'h0) |
`PHASE_TWO_ASSERT(!data_reg[7]); |
`ASSERT(!data_reg[7]); |
|
if (state == 4'h1) |
`PHASE_TWO_ASSERT((data_reg[7] |
`ASSERT((data_reg[7] |
== $past(f_tx_data[0]))&&(!data_reg[6])); |
|
if (state == 4'h2) |
`PHASE_TWO_ASSERT(data_reg[7:6] |
`ASSERT(data_reg[7:6] |
== $past(f_tx_data[1:0])); |
|
if (state == 4'h3) |
`PHASE_TWO_ASSERT(data_reg[7:5] == $past(f_tx_data[2:0])); |
`ASSERT(data_reg[7:5] == $past(f_tx_data[2:0])); |
|
if (state == 4'h4) |
`PHASE_TWO_ASSERT(data_reg[7:4] == $past(f_tx_data[3:0])); |
`ASSERT(data_reg[7:4] == $past(f_tx_data[3:0])); |
|
if (state == 4'h5) |
`PHASE_TWO_ASSERT(data_reg[7:3] == $past(f_tx_data[4:0])); |
`ASSERT(data_reg[7:3] == $past(f_tx_data[4:0])); |
|
if (state == 4'h6) |
`PHASE_TWO_ASSERT(data_reg[7:2] == $past(f_tx_data[5:0])); |
`ASSERT(data_reg[7:2] == $past(f_tx_data[5:0])); |
|
if (state == 4'h7) |
`PHASE_TWO_ASSERT(data_reg[7:1] == $past(f_tx_data[6:0])); |
`ASSERT(data_reg[7:1] == $past(f_tx_data[6:0])); |
|
if (state == 4'h8) |
`PHASE_TWO_ASSERT(data_reg[7:0] == $past(f_tx_data[7:0])); |
`ASSERT(data_reg[7:0] == $past(f_tx_data[7:0])); |
end |
//////////////////////////////////////////////////////////////////////// |
// |
// Cover properties |
// |
//////////////////////////////////////////////////////////////////////// |
// |
always @(posedge i_clk) |
cover(o_wr); // Step 626, takes about 20mins |
|
always @(posedge i_clk) |
cover(o_wr); |
begin |
cover(!ck_uart); |
cover((f_past_valid)&&($rose(ck_uart))); // 82 |
cover((zero_baud_counter)&&(state == `RXUL_BIT_ZERO)); // 110 |
cover((zero_baud_counter)&&(state == `RXUL_BIT_ONE)); // 174 |
cover((zero_baud_counter)&&(state == `RXUL_BIT_TWO)); // 238 |
cover((zero_baud_counter)&&(state == `RXUL_BIT_THREE));// 302 |
cover((zero_baud_counter)&&(state == `RXUL_BIT_FOUR)); // 366 |
cover((zero_baud_counter)&&(state == `RXUL_BIT_FIVE)); // 430 |
cover((zero_baud_counter)&&(state == `RXUL_BIT_SIX)); // 494 |
cover((zero_baud_counter)&&(state == `RXUL_BIT_SEVEN));// 558 |
cover((zero_baud_counter)&&(state == `RXUL_STOP)); // 622 |
cover((zero_baud_counter)&&(state == `RXUL_WAIT)); // 626 |
end |
|
`endif |
`endif |
`ifdef FORMAL_VERILATOR |
// FORMAL properties which can be tested via Verilator as well as |
// Yosys FORMAL |
/txuart.v
69,7 → 69,7
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// Copyright (C) 2015-2017, Gisselquist Technology, LLC |
// Copyright (C) 2015-2019, Gisselquist Technology, LLC |
// |
// This program is free software (firmware): you can redistribute it and/or |
// modify it under the terms of the GNU General Public License as published |
95,27 → 95,27
// |
`default_nettype none |
// |
`define TXU_BIT_ZERO 4'h0 |
`define TXU_BIT_ONE 4'h1 |
`define TXU_BIT_TWO 4'h2 |
`define TXU_BIT_THREE 4'h3 |
`define TXU_BIT_FOUR 4'h4 |
`define TXU_BIT_FIVE 4'h5 |
`define TXU_BIT_SIX 4'h6 |
`define TXU_BIT_SEVEN 4'h7 |
`define TXU_PARITY 4'h8 // Constant 1 |
`define TXU_STOP 4'h9 // Constant 1 |
`define TXU_SECOND_STOP 4'ha |
// 4'hb // Unused |
// 4'hc // Unused |
// `define TXU_START 4'hd // An unused state |
`define TXU_BREAK 4'he |
`define TXU_IDLE 4'hf |
// |
// |
module txuart(i_clk, i_reset, i_setup, i_break, i_wr, i_data, |
i_cts_n, o_uart_tx, o_busy); |
parameter [30:0] INITIAL_SETUP = 31'd868; |
// |
localparam [3:0] TXU_BIT_ZERO = 4'h0; |
localparam [3:0] TXU_BIT_ONE = 4'h1; |
localparam [3:0] TXU_BIT_TWO = 4'h2; |
localparam [3:0] TXU_BIT_THREE = 4'h3; |
localparam [3:0] TXU_BIT_FOUR = 4'h4; |
localparam [3:0] TXU_BIT_FIVE = 4'h5; |
localparam [3:0] TXU_BIT_SIX = 4'h6; |
localparam [3:0] TXU_BIT_SEVEN = 4'h7; |
localparam [3:0] TXU_PARITY = 4'h8; |
localparam [3:0] TXU_STOP = 4'h9; |
localparam [3:0] TXU_SECOND_STOP = 4'ha; |
// |
localparam [3:0] TXU_BREAK = 4'he; |
localparam [3:0] TXU_IDLE = 4'hf; |
// |
// |
input wire i_clk, i_reset; |
input wire [30:0] i_setup; |
input wire i_break; |
133,24 → 133,26
output wire o_busy; |
|
wire [27:0] clocks_per_baud, break_condition; |
wire [1:0] data_bits; |
wire use_parity, parity_even, dblstop, fixd_parity, |
fixdp_value, hw_flow_control; |
wire [1:0] i_data_bits, data_bits; |
wire use_parity, parity_odd, dblstop, fixd_parity, |
fixdp_value, hw_flow_control, i_parity_odd; |
reg [30:0] r_setup; |
assign clocks_per_baud = { 4'h0, r_setup[23:0] }; |
assign break_condition = { r_setup[23:0], 4'h0 }; |
assign hw_flow_control = !r_setup[30]; |
assign i_data_bits = i_setup[29:28]; |
assign data_bits = r_setup[29:28]; |
assign dblstop = r_setup[27]; |
assign use_parity = r_setup[26]; |
assign fixd_parity = r_setup[25]; |
assign parity_even = r_setup[24]; |
assign i_parity_odd = i_setup[24]; |
assign parity_odd = r_setup[24]; |
assign fixdp_value = r_setup[24]; |
|
reg [27:0] baud_counter; |
reg [3:0] state; |
reg [7:0] lcl_data; |
reg calc_parity, r_busy, zero_baud_counter; |
reg calc_parity, r_busy, zero_baud_counter, last_state; |
|
|
// First step ... handle any hardware flow control, if so enabled. |
169,77 → 171,70
// initial qq_cts_n = 1'b1; |
// initial ck_cts = 1'b0; |
always @(posedge i_clk) |
q_cts_n <= i_cts_n; |
{ qq_cts_n, q_cts_n } <= { q_cts_n, i_cts_n }; |
always @(posedge i_clk) |
qq_cts_n <= q_cts_n; |
always @(posedge i_clk) |
ck_cts <= (!qq_cts_n)||(!hw_flow_control); |
|
initial o_uart_tx = 1'b1; |
initial r_busy = 1'b1; |
initial state = `TXU_IDLE; |
initial lcl_data= 8'h0; |
initial calc_parity = 1'b0; |
// initial baud_counter = clocks_per_baud;//ILLEGAL--not constant |
initial state = TXU_IDLE; |
always @(posedge i_clk) |
if (i_reset) |
begin |
if (i_reset) |
begin |
r_busy <= 1'b1; |
state <= TXU_IDLE; |
end else if (i_break) |
begin |
state <= TXU_BREAK; |
r_busy <= 1'b1; |
end else if (!zero_baud_counter) |
begin // r_busy needs to be set coming into here |
r_busy <= 1'b1; |
end else if (state == TXU_BREAK) |
begin |
state <= TXU_IDLE; |
r_busy <= !ck_cts; |
end else if (state == TXU_IDLE) // STATE_IDLE |
begin |
if ((i_wr)&&(!r_busy)) |
begin // Immediately start us off with a start bit |
r_busy <= 1'b1; |
state <= `TXU_IDLE; |
end else if (i_break) |
case(i_data_bits) |
2'b00: state <= TXU_BIT_ZERO; |
2'b01: state <= TXU_BIT_ONE; |
2'b10: state <= TXU_BIT_TWO; |
2'b11: state <= TXU_BIT_THREE; |
endcase |
end else begin // Stay in idle |
r_busy <= !ck_cts; |
end |
end else begin |
// One clock tick in each of these states ... |
// baud_counter <= clocks_per_baud - 28'h01; |
r_busy <= 1'b1; |
if (state[3] == 0) // First 8 bits |
begin |
state <= `TXU_BREAK; |
r_busy <= 1'b1; |
end else if (!zero_baud_counter) |
begin // r_busy needs to be set coming into here |
r_busy <= 1'b1; |
end else if (state == `TXU_BREAK) |
if (state == TXU_BIT_SEVEN) |
state <= (use_parity)? TXU_PARITY:TXU_STOP; |
else |
state <= state + 1; |
end else if (state == TXU_PARITY) |
begin |
state <= `TXU_IDLE; |
r_busy <= 1'b1; |
end else if (state == `TXU_IDLE) // STATE_IDLE |
state <= TXU_STOP; |
end else if (state == TXU_STOP) |
begin // two stop bit(s) |
if (dblstop) |
state <= TXU_SECOND_STOP; |
else |
state <= TXU_IDLE; |
end else // `TXU_SECOND_STOP and default: |
begin |
if ((i_wr)&&(!r_busy)) |
begin // Immediately start us off with a start bit |
r_busy <= 1'b1; |
case(data_bits) |
2'b00: state <= `TXU_BIT_ZERO; |
2'b01: state <= `TXU_BIT_ONE; |
2'b10: state <= `TXU_BIT_TWO; |
2'b11: state <= `TXU_BIT_THREE; |
endcase |
end else begin // Stay in idle |
r_busy <= !ck_cts; |
end |
end else begin |
// One clock tick in each of these states ... |
// baud_counter <= clocks_per_baud - 28'h01; |
r_busy <= 1'b1; |
if (state[3] == 0) // First 8 bits |
begin |
if (state == `TXU_BIT_SEVEN) |
state <= (use_parity)?`TXU_PARITY:`TXU_STOP; |
else |
state <= state + 1'b1; |
end else if (state == `TXU_PARITY) |
begin |
state <= `TXU_STOP; |
end else if (state == `TXU_STOP) |
begin // two stop bit(s) |
if (dblstop) |
state <= `TXU_SECOND_STOP; |
else |
state <= `TXU_IDLE; |
end else // `TXU_SECOND_STOP and default: |
begin |
state <= `TXU_IDLE; // Go back to idle |
// Still r_busy, since we need to wait |
// for the baud clock to finish counting |
// out this last bit. |
end |
end |
end |
state <= TXU_IDLE; // Go back to idle |
// Still r_busy, since we need to wait |
// for the baud clock to finish counting |
// out this last bit. |
end |
end |
|
// o_busy |
// |
259,8 → 254,8
// the size of our data word. |
initial r_setup = INITIAL_SETUP; |
always @(posedge i_clk) |
if (state == `TXU_IDLE) |
r_setup <= i_setup; |
if (!o_busy) |
r_setup <= i_setup; |
|
// lcl_data |
// |
271,11 → 266,12
// true and i_wr is, we set it and r_busy is true thereafter. |
// Then, on any zero_baud_counter (i.e. change between baud intervals) |
// we simple logically shift the register right to grab the next bit. |
initial lcl_data = 8'hff; |
always @(posedge i_clk) |
if (!r_busy) |
lcl_data <= i_data; |
else if (zero_baud_counter) |
lcl_data <= { 1'b0, lcl_data[7:1] }; |
if (!r_busy) |
lcl_data <= i_data; |
else if (zero_baud_counter) |
lcl_data <= { 1'b0, lcl_data[7:1] }; |
|
// o_uart_tx |
// |
293,16 → 289,16
// or changing, and hence what it's calculated value is. |
// 1'b1 at all other times (stop bits, idle, etc) |
always @(posedge i_clk) |
if (i_reset) |
o_uart_tx <= 1'b1; |
else if ((i_break)||((i_wr)&&(!r_busy))) |
o_uart_tx <= 1'b0; |
else if (zero_baud_counter) |
casez(state) |
4'b0???: o_uart_tx <= lcl_data[0]; |
`TXU_PARITY: o_uart_tx <= calc_parity; |
default: o_uart_tx <= 1'b1; |
endcase |
if (i_reset) |
o_uart_tx <= 1'b1; |
else if ((i_break)||((i_wr)&&(!r_busy))) |
o_uart_tx <= 1'b0; |
else if (zero_baud_counter) |
casez(state) |
4'b0???: o_uart_tx <= lcl_data[0]; |
TXU_PARITY: o_uart_tx <= calc_parity; |
default: o_uart_tx <= 1'b1; |
endcase |
|
|
// calc_parity |
311,17 → 307,20
// parity is fixed, then the parity bit is given by the fixed parity |
// value (r_setup[24]). Otherwise the parity is given by the GF2 |
// sum of all the data bits (plus one for even parity). |
initial calc_parity = 1'b0; |
always @(posedge i_clk) |
if (fixd_parity) |
calc_parity <= fixdp_value; |
else if (zero_baud_counter) |
begin |
if (state[3] == 0) // First 8 bits of msg |
calc_parity <= calc_parity ^ lcl_data[0]; |
else |
calc_parity <= parity_even; |
end else if (!r_busy) |
calc_parity <= parity_even; |
if (!o_busy) |
calc_parity <= i_setup[24]; |
else if (fixd_parity) |
calc_parity <= fixdp_value; |
else if (zero_baud_counter) |
begin |
if (state[3] == 0) // First 8 bits of msg |
calc_parity <= calc_parity ^ lcl_data[0]; |
else if (state == TXU_IDLE) |
calc_parity <= parity_odd; |
end else if (!r_busy) |
calc_parity <= parity_odd; |
|
|
// All of the above logic is driven by the baud counter. Bits must last |
356,7 → 355,7
// than waiting for the end of the next (fictitious and arbitrary) baud |
// interval. |
// |
// When (i_wr)&&(!r_busy)&&(state == `TXU_IDLE) then we're not only in |
// When (i_wr)&&(!r_busy)&&(state == TXU_IDLE) then we're not only in |
// the idle state, but we also just accepted a command to start writing |
// the next word. At this point, the baud counter needs to be reset |
// to the number of clocks per baud, and zero_baud_counter set to zero. |
376,207 → 375,759
zero_baud_counter <= 1'b0; |
end else if (!zero_baud_counter) |
baud_counter <= baud_counter - 28'h01; |
else if (state == `TXU_BREAK) |
// Give us four idle baud intervals before becoming |
// available |
baud_counter <= clocks_per_baud<<2; |
else if (state == `TXU_IDLE) |
else if (state == TXU_BREAK) |
begin |
baud_counter <= 0; |
zero_baud_counter <= 1'b1; |
end else if (state == TXU_IDLE) |
begin |
baud_counter <= 28'h0; |
zero_baud_counter <= 1'b1; |
if ((i_wr)&&(!r_busy)) |
begin |
baud_counter <= clocks_per_baud - 28'h01; |
baud_counter <= { 4'h0, i_setup[23:0]} - 28'h01; |
zero_baud_counter <= 1'b0; |
end |
end else |
end else if (last_state) |
baud_counter <= clocks_per_baud - 28'h02; |
else |
baud_counter <= clocks_per_baud - 28'h01; |
end |
|
initial last_state = 1'b0; |
always @(posedge i_clk) |
if (dblstop) |
last_state <= (state == TXU_SECOND_STOP); |
else |
last_state <= (state == TXU_STOP); |
|
`ifdef FORMAL |
reg fsv_parity; |
reg [30:0] fsv_setup; |
reg [7:0] fsv_data; |
reg f_past_valid; |
|
initial f_past_valid = 1'b0; |
always @(posedge i_clk) |
f_past_valid <= 1'b1; |
|
always @(posedge i_clk) |
if ((i_wr)&&(!o_busy)) |
fsv_data <= i_data; |
if ((i_wr)&&(!o_busy)) |
fsv_data <= i_data; |
|
initial fsv_setup = INITIAL_SETUP; |
always @(posedge i_clk) |
if ((i_wr)&&(!o_busy)) |
fsv_setup <= i_setup; |
if (!o_busy) |
fsv_setup <= i_setup; |
|
always @(*) |
assert(r_setup == fsv_setup); |
|
|
always @(posedge i_clk) |
assert(zero_baud_counter == (baud_counter == 0)); |
|
always @(*) |
assume(i_setup[21:0] >= 2); |
always @(*) |
assume(i_setup[21:0] <= 16); |
if (!o_busy) |
assert(zero_baud_counter); |
|
/* |
* |
* Will only pass if !i_break && !i_reset, otherwise the setup can |
* change in the middle of this operation |
* |
always @(posedge i_clk) |
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(i_break)) |
&&(($past(o_busy))||($past(i_wr)))) |
assert(baud_counter <= { fsv_setup[23:0], 4'h0 }); |
*/ |
|
// A single baud interval |
sequence BAUD_INTERVAL(DAT, SR, ST); |
((o_uart_tx == DAT)&&(state == ST) |
&&(lcl_data == SR) |
&&(baud_counter == fsv_setup[21:0]-1) |
&&(!zero_baud_counter)) |
##1 ((o_uart_tx == DAT)&&(state == ST) |
&&(lcl_data == SR) |
&&(baud_counter == $past(baud_counter)-1) |
&&(baud_counter > 0) |
&&(baud_counter < fsv_setup[21:0]) |
&&(!zero_baud_counter))[*0:$] |
##1 (o_uart_tx == DAT)&&(state == ST) |
&&(lcl_data == SR) |
&&(zero_baud_counter); |
endsequence |
always @(posedge i_clk) |
if ((f_past_valid)&&(!$past(zero_baud_counter)) |
&&(!$past(i_reset))&&(!$past(i_break))) |
begin |
assert($stable(o_uart_tx)); |
assert($stable(state)); |
assert($stable(lcl_data)); |
if ((state != TXU_IDLE)&&(state != TXU_BREAK)) |
assert($stable(calc_parity)); |
assert(baud_counter == $past(baud_counter)-1'b1); |
end |
|
// |
// Our various sequence data declarations |
reg [5:0] f_five_seq; |
reg [6:0] f_six_seq; |
reg [7:0] f_seven_seq; |
reg [8:0] f_eight_seq; |
reg [2:0] f_stop_seq; // parity bit, stop bit, double stop bit |
|
|
// |
// One byte transmitted |
// |
// DATA = the byte that is sent |
// CKS = the number of clocks per bit |
// |
sequence SEND5(DATA); |
BAUD_INTERVAL(1'b0, DATA, 4'h3) |
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h4) |
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h5) |
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h6) |
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h7) |
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h8); |
endsequence |
//////////////////////////////////////////////////////////////////////// |
// |
// Five bit data |
// |
//////////////////////////////////////////////////////////////////////// |
|
sequence SEND6(DATA); |
BAUD_INTERVAL(1'b0, DATA, 4'h2) |
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h3) |
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h4) |
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h5) |
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h6) |
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h7) |
##1 BAUD_INTERVAL(DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h8); |
endsequence |
initial f_five_seq = 0; |
always @(posedge i_clk) |
if ((i_reset)||(i_break)) |
f_five_seq = 0; |
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy) |
&&(i_data_bits == 2'b11)) // five data bits |
f_five_seq <= 1; |
else if (zero_baud_counter) |
f_five_seq <= f_five_seq << 1; |
|
sequence SEND7(DATA); |
BAUD_INTERVAL(1'b0, DATA, 4'h1) |
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h2) |
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h3) |
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h4) |
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h5) |
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h6) |
##1 BAUD_INTERVAL(DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h7) |
##1 BAUD_INTERVAL(DATA[6], {{(7){1'b1}},DATA[7:7]}, 4'h8); |
endsequence |
always @(*) |
if (|f_five_seq) |
begin |
assert(fsv_setup[29:28] == data_bits); |
assert(data_bits == 2'b11); |
assert(baud_counter < fsv_setup[23:0]); |
|
sequence SEND8(DATA); |
BAUD_INTERVAL(1'b0, DATA, 4'h0) |
##1 BAUD_INTERVAL(DATA[0], {{(1){1'b1}},DATA[7:1]}, 4'h1) |
##1 BAUD_INTERVAL(DATA[1], {{(2){1'b1}},DATA[7:2]}, 4'h2) |
##1 BAUD_INTERVAL(DATA[2], {{(3){1'b1}},DATA[7:3]}, 4'h3) |
##1 BAUD_INTERVAL(DATA[3], {{(4){1'b1}},DATA[7:4]}, 4'h4) |
##1 BAUD_INTERVAL(DATA[4], {{(5){1'b1}},DATA[7:5]}, 4'h5) |
##1 BAUD_INTERVAL(DATA[5], {{(6){1'b1}},DATA[7:6]}, 4'h6) |
##1 BAUD_INTERVAL(DATA[6], {{(7){1'b1}},DATA[7:7]}, 4'h7) |
##1 BAUD_INTERVAL(DATA[7], 8'hff, 4'h8); |
endsequence |
assert(1'b0 == |f_six_seq); |
assert(1'b0 == |f_seven_seq); |
assert(1'b0 == |f_eight_seq); |
assert(r_busy); |
assert(state > 4'h2); |
end |
|
always @(*) |
case(f_five_seq) |
6'h00: begin assert(1); end |
6'h01: begin |
assert(state == 4'h3); |
assert(o_uart_tx == 1'b0); |
assert(lcl_data[4:0] == fsv_data[4:0]); |
if (!fixd_parity) |
assert(calc_parity == parity_odd); |
end |
6'h02: begin |
assert(state == 4'h4); |
assert(o_uart_tx == fsv_data[0]); |
assert(lcl_data[3:0] == fsv_data[4:1]); |
if (!fixd_parity) |
assert(calc_parity == fsv_data[0] ^ parity_odd); |
end |
6'h04: begin |
assert(state == 4'h5); |
assert(o_uart_tx == fsv_data[1]); |
assert(lcl_data[2:0] == fsv_data[4:2]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd); |
end |
6'h08: begin |
assert(state == 4'h6); |
assert(o_uart_tx == fsv_data[2]); |
assert(lcl_data[1:0] == fsv_data[4:3]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd); |
end |
6'h10: begin |
assert(state == 4'h7); |
assert(o_uart_tx == fsv_data[3]); |
assert(lcl_data[0] == fsv_data[4]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd); |
end |
6'h20: begin |
if (use_parity) |
assert(state == 4'h8); |
else |
assert(state == 4'h9); |
assert(o_uart_tx == fsv_data[4]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[4:0]) ^ parity_odd); |
end |
default: begin assert(0); end |
endcase |
|
//////////////////////////////////////////////////////////////////////// |
// |
// Six bit data |
// |
//////////////////////////////////////////////////////////////////////// |
|
initial f_six_seq = 0; |
always @(posedge i_clk) |
if (fsv_setup[25]) |
fsv_parity <= fsv_setup[24]; |
else |
case(fsv_setup[29:28]) |
2'b00: fsv_parity <= (^fsv_data[4:0]) ^ fsv_setup[24]; |
2'b01: fsv_parity <= (^fsv_data[5:0]) ^ fsv_setup[24]; |
2'b10: fsv_parity <= (^fsv_data[6:0]) ^ fsv_setup[24]; |
2'b11: fsv_parity <= (^fsv_data[7:0]) ^ fsv_setup[24]; |
endcase |
if ((i_reset)||(i_break)) |
f_six_seq = 0; |
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy) |
&&(i_data_bits == 2'b10)) // six data bits |
f_six_seq <= 1; |
else if (zero_baud_counter) |
f_six_seq <= f_six_seq << 1; |
|
assert property( @(posedge i_clk) |
(o_busy)[*2] |=> $stable(fsv_parity)); |
always @(*) |
if (|f_six_seq) |
begin |
assert(fsv_setup[29:28] == 2'b10); |
assert(fsv_setup[29:28] == data_bits); |
assert(baud_counter < fsv_setup[23:0]); |
|
assert property( @(posedge i_clk) |
(o_busy) |=> $stable(fsv_data)); |
assert(1'b0 == |f_five_seq); |
assert(1'b0 == |f_seven_seq); |
assert(1'b0 == |f_eight_seq); |
assert(r_busy); |
assert(state > 4'h1); |
end |
|
assert property( @(posedge i_clk) |
(o_busy) |=> $stable(fsv_setup)); |
always @(*) |
case(f_six_seq) |
7'h00: begin assert(1); end |
7'h01: begin |
assert(state == 4'h2); |
assert(o_uart_tx == 1'b0); |
assert(lcl_data[5:0] == fsv_data[5:0]); |
if (!fixd_parity) |
assert(calc_parity == parity_odd); |
end |
7'h02: begin |
assert(state == 4'h3); |
assert(o_uart_tx == fsv_data[0]); |
assert(lcl_data[4:0] == fsv_data[5:1]); |
if (!fixd_parity) |
assert(calc_parity == fsv_data[0] ^ parity_odd); |
end |
7'h04: begin |
assert(state == 4'h4); |
assert(o_uart_tx == fsv_data[1]); |
assert(lcl_data[3:0] == fsv_data[5:2]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd); |
end |
7'h08: begin |
assert(state == 4'h5); |
assert(o_uart_tx == fsv_data[2]); |
assert(lcl_data[2:0] == fsv_data[5:3]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd); |
end |
7'h10: begin |
assert(state == 4'h6); |
assert(o_uart_tx == fsv_data[3]); |
assert(lcl_data[1:0] == fsv_data[5:4]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd); |
end |
7'h20: begin |
assert(state == 4'h7); |
assert(lcl_data[0] == fsv_data[5]); |
assert(o_uart_tx == fsv_data[4]); |
if (!fixd_parity) |
assert(calc_parity == ((^fsv_data[4:0]) ^ parity_odd)); |
end |
7'h40: begin |
if (use_parity) |
assert(state == 4'h8); |
else |
assert(state == 4'h9); |
assert(o_uart_tx == fsv_data[5]); |
if (!fixd_parity) |
assert(calc_parity == ((^fsv_data[5:0]) ^ parity_odd)); |
end |
default: begin if (f_past_valid) assert(0); end |
endcase |
|
sequence SENDPARITY(SETUP); |
((o_uart_tx == fsv_parity)&&(state == `TXU_PARITY) |
&&(SETUP[26]) |
&&(baud_counter == SETUP[21:0]-1) |
&&(!zero_baud_counter)) |
##1 ((o_uart_tx == fsv_parity)&&(state == `TXU_PARITY) |
&&(SETUP[26]) |
&&(baud_counter < SETUP[21:0]) |
&&(baud_counter > 0) |
&&(baud_counter == $past(baud_counter)-1) |
&&(!zero_baud_counter))[*0:$] |
##1 (o_uart_tx == fsv_parity)&&(state == `TXU_PARITY) |
&&(SETUP[26]) |
&&(zero_baud_counter); |
endsequence |
//////////////////////////////////////////////////////////////////////// |
// |
// Seven bit data |
// |
//////////////////////////////////////////////////////////////////////// |
initial f_seven_seq = 0; |
always @(posedge i_clk) |
if ((i_reset)||(i_break)) |
f_seven_seq = 0; |
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy) |
&&(i_data_bits == 2'b01)) // seven data bits |
f_seven_seq <= 1; |
else if (zero_baud_counter) |
f_seven_seq <= f_seven_seq << 1; |
|
sequence SENDSINGLESTOP(CKS,ST); |
((o_uart_tx == 1'b1)&&(state == ST) |
&&(baud_counter == CKS-1) |
&&(!zero_baud_counter)) |
##1 ((o_uart_tx == 1'b1)&&(state == ST) |
&&(baud_counter > 0) |
&&(baud_counter == $past(baud_counter)-1) |
&&(!zero_baud_counter))[*0:$] |
##1 (o_uart_tx == 1'b1)&&(state == ST) |
&&(zero_baud_counter); |
endsequence |
always @(*) |
if (|f_seven_seq) |
begin |
assert(fsv_setup[29:28] == 2'b01); |
assert(fsv_setup[29:28] == data_bits); |
assert(baud_counter < fsv_setup[23:0]); |
|
sequence SENDFULLSTOP(SETUP); |
((!SETUP[27]) throughout SENDSINGLESTOP(SETUP[21:0],`TXU_STOP)) |
or (SETUP[27]) throughout |
SENDSINGLESTOP(SETUP[21:0],`TXU_STOP) |
##1 SENDSINGLESTOP(SETUP[21:0],`TXU_SECOND_STOP); |
endsequence |
assert(1'b0 == |f_five_seq); |
assert(1'b0 == |f_six_seq); |
assert(1'b0 == |f_eight_seq); |
assert(r_busy); |
assert(state != 4'h0); |
end |
|
sequence UART_IDLE; |
(!o_busy)&&(o_uart_tx)&&(zero_baud_counter); |
endsequence |
always @(*) |
case(f_seven_seq) |
8'h00: begin assert(1); end |
8'h01: begin |
assert(state == 4'h1); |
assert(o_uart_tx == 1'b0); |
assert(lcl_data[6:0] == fsv_data[6:0]); |
if (!fixd_parity) |
assert(calc_parity == parity_odd); |
end |
8'h02: begin |
assert(state == 4'h2); |
assert(o_uart_tx == fsv_data[0]); |
assert(lcl_data[5:0] == fsv_data[6:1]); |
if (!fixd_parity) |
assert(calc_parity == fsv_data[0] ^ parity_odd); |
end |
8'h04: begin |
assert(state == 4'h3); |
assert(o_uart_tx == fsv_data[1]); |
assert(lcl_data[4:0] == fsv_data[6:2]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd); |
end |
8'h08: begin |
assert(state == 4'h4); |
assert(o_uart_tx == fsv_data[2]); |
assert(lcl_data[3:0] == fsv_data[6:3]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd); |
end |
8'h10: begin |
assert(state == 4'h5); |
assert(o_uart_tx == fsv_data[3]); |
assert(lcl_data[2:0] == fsv_data[6:4]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd); |
end |
8'h20: begin |
assert(state == 4'h6); |
assert(o_uart_tx == fsv_data[4]); |
assert(lcl_data[1:0] == fsv_data[6:5]); |
if (!fixd_parity) |
assert(calc_parity == ((^fsv_data[4:0]) ^ parity_odd)); |
end |
8'h40: begin |
assert(state == 4'h7); |
assert(lcl_data[0] == fsv_data[6]); |
assert(o_uart_tx == fsv_data[5]); |
if (!fixd_parity) |
assert(calc_parity == ((^fsv_data[5:0]) ^ parity_odd)); |
end |
8'h80: begin |
if (use_parity) |
assert(state == 4'h8); |
else |
assert(state == 4'h9); |
assert(o_uart_tx == fsv_data[6]); |
if (!fixd_parity) |
assert(calc_parity == ((^fsv_data[6:0]) ^ parity_odd)); |
end |
default: begin if (f_past_valid) assert(0); end |
endcase |
|
assert property ( @(posedge i_clk) (!o_busy) |-> UART_IDLE); |
|
//////////////////////////////////////////////////////////////////////// |
// |
// Eight bit data |
// |
//////////////////////////////////////////////////////////////////////// |
initial f_eight_seq = 0; |
always @(posedge i_clk) |
if ((i_reset)||(i_break)) |
f_eight_seq = 0; |
else if ((state == TXU_IDLE)&&(i_wr)&&(!o_busy) |
&&(i_data_bits == 2'b00)) // Eight data bits |
f_eight_seq <= 1; |
else if (zero_baud_counter) |
f_eight_seq <= f_eight_seq << 1; |
|
assert property ( @(posedge i_clk) |
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b00) |=> |
((o_busy) throughout |
SEND5(fsv_data) |
##1 SENDPARITY(fsv_setup) |
##1 SENDFULLSTOP(fsv_setup) |
) |
##1 UART_IDLE); |
always @(*) |
if (|f_eight_seq) |
begin |
assert(fsv_setup[29:28] == 2'b00); |
assert(fsv_setup[29:28] == data_bits); |
assert(baud_counter < { 6'h0, fsv_setup[23:0]}); |
|
assert property ( @(posedge i_clk) |
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b01) |=> |
((o_busy) throughout |
SEND6(fsv_data) |
##1 SENDPARITY(fsv_setup) |
##1 SENDFULLSTOP(fsv_setup) |
) |
##1 UART_IDLE); |
assert(1'b0 == |f_five_seq); |
assert(1'b0 == |f_six_seq); |
assert(1'b0 == |f_seven_seq); |
assert(r_busy); |
end |
|
assert property ( @(posedge i_clk) |
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b10) |=> |
((o_busy) throughout |
SEND7(fsv_data) |
##1 SENDPARITY(fsv_setup) |
##1 SENDFULLSTOP(fsv_setup) |
) |
##1 UART_IDLE); |
always @(*) |
case(f_eight_seq) |
9'h000: begin assert(1); end |
9'h001: begin |
assert(state == 4'h0); |
assert(o_uart_tx == 1'b0); |
assert(lcl_data[7:0] == fsv_data[7:0]); |
if (!fixd_parity) |
assert(calc_parity == parity_odd); |
end |
9'h002: begin |
assert(state == 4'h1); |
assert(o_uart_tx == fsv_data[0]); |
assert(lcl_data[6:0] == fsv_data[7:1]); |
if (!fixd_parity) |
assert(calc_parity == fsv_data[0] ^ parity_odd); |
end |
9'h004: begin |
assert(state == 4'h2); |
assert(o_uart_tx == fsv_data[1]); |
assert(lcl_data[5:0] == fsv_data[7:2]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[1:0]) ^ parity_odd); |
end |
9'h008: begin |
assert(state == 4'h3); |
assert(o_uart_tx == fsv_data[2]); |
assert(lcl_data[4:0] == fsv_data[7:3]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[2:0]) ^ parity_odd); |
end |
9'h010: begin |
assert(state == 4'h4); |
assert(o_uart_tx == fsv_data[3]); |
assert(lcl_data[3:0] == fsv_data[7:4]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[3:0]) ^ parity_odd); |
end |
9'h020: begin |
assert(state == 4'h5); |
assert(o_uart_tx == fsv_data[4]); |
assert(lcl_data[2:0] == fsv_data[7:5]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[4:0]) ^ parity_odd); |
end |
9'h040: begin |
assert(state == 4'h6); |
assert(o_uart_tx == fsv_data[5]); |
assert(lcl_data[1:0] == fsv_data[7:6]); |
if (!fixd_parity) |
assert(calc_parity == (^fsv_data[5:0]) ^ parity_odd); |
end |
9'h080: begin |
assert(state == 4'h7); |
assert(o_uart_tx == fsv_data[6]); |
assert(lcl_data[0] == fsv_data[7]); |
if (!fixd_parity) |
assert(calc_parity == ((^fsv_data[6:0]) ^ parity_odd)); |
end |
9'h100: begin |
if (use_parity) |
assert(state == 4'h8); |
else |
assert(state == 4'h9); |
assert(o_uart_tx == fsv_data[7]); |
if (!fixd_parity) |
assert(calc_parity == ((^fsv_data[7:0]) ^ parity_odd)); |
end |
default: begin if (f_past_valid) assert(0); end |
endcase |
|
assert property ( @(posedge i_clk) |
(i_wr)&&(!o_busy)&&(i_setup[29:28]==2'b11) |=> |
((o_busy) throughout |
SEND8(fsv_data) |
##1 SENDPARITY(fsv_setup) |
##1 SENDFULLSTOP(fsv_setup) |
) |
##1 UART_IDLE); |
//////////////////////////////////////////////////////////////////////// |
// |
// Combined properties for all of the data sequences |
// |
//////////////////////////////////////////////////////////////////////// |
always @(posedge i_clk) |
if (((|f_five_seq[5:0]) || (|f_six_seq[6:0]) || (|f_seven_seq[7:0]) |
|| (|f_eight_seq[8:0])) |
&& ($past(zero_baud_counter))) |
assert(baud_counter == { 4'h0, fsv_setup[23:0] }-1); |
|
|
//////////////////////////////////////////////////////////////////////// |
// |
// The stop sequence |
// |
// This consists of any parity bit, as well as one or two stop bits |
//////////////////////////////////////////////////////////////////////// |
initial f_stop_seq = 1'b0; |
always @(posedge i_clk) |
if ((i_reset)||(i_break)) |
f_stop_seq <= 0; |
else if (zero_baud_counter) |
begin |
f_stop_seq <= 0; |
if (f_stop_seq[0]) // Coming from a parity bit |
begin |
if (dblstop) |
f_stop_seq[1] <= 1'b1; |
else |
f_stop_seq[2] <= 1'b1; |
end |
|
if (f_stop_seq[1]) |
f_stop_seq[2] <= 1'b1; |
|
if (f_eight_seq[8] | f_seven_seq[7] | f_six_seq[6] |
| f_five_seq[5]) |
begin |
if (use_parity) |
f_stop_seq[0] <= 1'b1; |
else if (dblstop) |
f_stop_seq[1] <= 1'b1; |
else |
f_stop_seq[2] <= 1'b1; |
end |
end |
|
always @(*) |
if (|f_stop_seq) |
begin |
assert(1'b0 == |f_five_seq[4:0]); |
assert(1'b0 == |f_six_seq[5:0]); |
assert(1'b0 == |f_seven_seq[6:0]); |
assert(1'b0 == |f_eight_seq[7:0]); |
|
assert(r_busy); |
end |
|
always @(*) |
if (f_stop_seq[0]) |
begin |
// 9 if dblstop and use_parity |
if (dblstop) |
assert(state == TXU_STOP); |
else |
assert(state == TXU_STOP); |
assert(use_parity); |
assert(o_uart_tx == fsv_parity); |
end |
|
always @(*) |
if (f_stop_seq[1]) |
begin |
// if (!use_parity) |
assert(state == TXU_SECOND_STOP); |
assert(dblstop); |
assert(o_uart_tx); |
end |
|
always @(*) |
if (f_stop_seq[2]) |
begin |
assert(state == 4'hf); |
assert(o_uart_tx); |
assert(baud_counter < fsv_setup[23:0]-1'b1); |
end |
|
|
always @(*) |
if (fsv_setup[25]) |
fsv_parity <= fsv_setup[24]; |
else |
case(fsv_setup[29:28]) |
2'b00: fsv_parity = (^fsv_data[7:0]) ^ fsv_setup[24]; |
2'b01: fsv_parity = (^fsv_data[6:0]) ^ fsv_setup[24]; |
2'b10: fsv_parity = (^fsv_data[5:0]) ^ fsv_setup[24]; |
2'b11: fsv_parity = (^fsv_data[4:0]) ^ fsv_setup[24]; |
endcase |
|
////////////////////////////////////////////////////////////////////// |
// |
// The break sequence |
// |
////////////////////////////////////////////////////////////////////// |
reg [1:0] f_break_seq; |
initial f_break_seq = 2'b00; |
always @(posedge i_clk) |
if (i_reset) |
f_break_seq <= 2'b00; |
else if (i_break) |
f_break_seq <= 2'b01; |
else if (!zero_baud_counter) |
f_break_seq <= { |f_break_seq, 1'b0 }; |
else |
f_break_seq <= 0; |
|
always @(posedge i_clk) |
if (f_break_seq[0]) |
assert(baud_counter == { $past(fsv_setup[23:0]), 4'h0 }); |
always @(posedge i_clk) |
if ((f_past_valid)&&($past(f_break_seq[1]))&&(state != TXU_BREAK)) |
begin |
assert(state == TXU_IDLE); |
assert(o_uart_tx == 1'b1); |
end |
|
always @(*) |
if (|f_break_seq) |
begin |
assert(state == TXU_BREAK); |
assert(r_busy); |
assert(o_uart_tx == 1'b0); |
end |
|
////////////////////////////////////////////////////////////////////// |
// |
// Properties for use during induction if we are made a submodule of |
// the rxuart |
// |
////////////////////////////////////////////////////////////////////// |
|
// Need enough bits for reset (24+4) plus enough bits for all of the |
// various characters, 24+4, so 24+5 is a minimum of this counter |
// |
`ifndef TXUART |
reg [28:0] f_counter; |
initial f_counter = 0; |
always @(posedge i_clk) |
if (!o_busy) |
f_counter <= 1'b0; |
else |
f_counter <= f_counter + 1'b1; |
|
always @(*) |
if (f_five_seq[0]|f_six_seq[0]|f_seven_seq[0]|f_eight_seq[0]) |
assert(f_counter == (fsv_setup[23:0] - baud_counter - 1)); |
else if (f_five_seq[1]|f_six_seq[1]|f_seven_seq[1]|f_eight_seq[1]) |
assert(f_counter == ({4'h0, fsv_setup[23:0], 1'b0} - baud_counter - 1)); |
else if (f_five_seq[2]|f_six_seq[2]|f_seven_seq[2]|f_eight_seq[2]) |
assert(f_counter == ({4'h0, fsv_setup[23:0], 1'b0} |
+{5'h0, fsv_setup[23:0]} |
- baud_counter - 1)); |
else if (f_five_seq[3]|f_six_seq[3]|f_seven_seq[3]|f_eight_seq[3]) |
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0} |
- baud_counter - 1)); |
else if (f_five_seq[4]|f_six_seq[4]|f_seven_seq[4]|f_eight_seq[4]) |
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0} |
+{5'h0, fsv_setup[23:0]} |
- baud_counter - 1)); |
else if (f_five_seq[5]|f_six_seq[5]|f_seven_seq[5]|f_eight_seq[5]) |
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0} |
+{4'h0, fsv_setup[23:0], 1'b0} |
- baud_counter - 1)); |
else if (f_six_seq[6]|f_seven_seq[6]|f_eight_seq[6]) |
assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0} |
+{5'h0, fsv_setup[23:0]} |
+{4'h0, fsv_setup[23:0], 1'b0} |
- baud_counter - 1)); |
else if (f_seven_seq[7]|f_eight_seq[7]) |
assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} // 8 |
- baud_counter - 1)); |
else if (f_eight_seq[8]) |
assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} // 9 |
+{5'h0, fsv_setup[23:0]} |
- baud_counter - 1)); |
else if (f_stop_seq[0] || (!use_parity && f_stop_seq[1])) |
begin |
// Parity bit, or first of two stop bits |
case(data_bits) |
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{4'h0, fsv_setup[23:0], 1'b0} // 10 |
- baud_counter - 1)); |
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{5'h0, fsv_setup[23:0]} // 9 |
- baud_counter - 1)); |
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
- baud_counter - 1)); // 8 |
2'b11: assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0} |
+{5'h0, fsv_setup[23:0]} // 7 |
+{4'h0, fsv_setup[23:0], 1'b0} |
- baud_counter - 1)); |
endcase |
end else if (!use_parity && !dblstop && f_stop_seq[2]) |
begin |
// No parity, single stop bit |
// Different from the one above, since the last counter is has |
// one fewer items within it |
case(data_bits) |
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{4'h0, fsv_setup[23:0], 1'b0} // 10 |
- baud_counter - 2)); |
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{5'h0, fsv_setup[23:0]} // 9 |
- baud_counter - 2)); |
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
- baud_counter - 2)); // 8 |
2'b11: assert(f_counter == ({3'h0, fsv_setup[23:0], 2'b0} |
+{5'h0, fsv_setup[23:0]} // 7 |
+{4'h0, fsv_setup[23:0], 1'b0} |
- baud_counter - 2)); |
endcase |
end else if (f_stop_seq[1]) |
begin |
// Parity and the first of two stop bits |
assert(dblstop && use_parity); |
case(data_bits) |
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{5'h0, fsv_setup[23:0]} // 11 |
+{4'h0, fsv_setup[23:0], 1'b0} |
- baud_counter - 1)); |
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{4'h0, fsv_setup[23:0], 1'b0} // 10 |
- baud_counter - 1)); |
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{5'h0, fsv_setup[23:0]} // 9 |
- baud_counter - 1)); |
2'b11: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
- baud_counter - 1)); // 8 |
endcase |
end else if ((dblstop ^ use_parity) && f_stop_seq[2]) |
begin |
// Parity and one stop bit |
// assert(!dblstop && use_parity); |
case(data_bits) |
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{5'h0, fsv_setup[23:0]} // 11 |
+{4'h0, fsv_setup[23:0], 1'b0} |
- baud_counter - 2)); |
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{4'h0, fsv_setup[23:0], 1'b0} // 10 |
- baud_counter - 2)); |
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{5'h0, fsv_setup[23:0]} // 9 |
- baud_counter - 2)); |
2'b11: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
- baud_counter - 2)); // 8 |
endcase |
end else if (f_stop_seq[2]) |
begin |
assert(dblstop); |
assert(use_parity); |
// Parity and two stop bits |
case(data_bits) |
2'b00: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{3'h0, fsv_setup[23:0], 2'b00} // 12 |
- baud_counter - 2)); |
2'b01: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{5'h0, fsv_setup[23:0]} // 11 |
+{4'h0, fsv_setup[23:0], 1'b0} |
- baud_counter - 2)); |
2'b10: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{4'h0, fsv_setup[23:0], 1'b0} // 10 |
- baud_counter - 2)); |
2'b11: assert(f_counter == ({2'h0, fsv_setup[23:0], 3'b0} |
+{5'h0, fsv_setup[23:0]} // 9 |
- baud_counter - 2)); |
endcase |
end |
`endif |
|
////////////////////////////////////////////////////////////////////// |
// |
// Other properties, not necessarily associated with any sequences |
// |
////////////////////////////////////////////////////////////////////// |
always @(*) |
assert((state < 4'hb)||(state >= 4'he)); |
////////////////////////////////////////////////////////////////////// |
// |
// Careless/limiting assumption section |
// |
////////////////////////////////////////////////////////////////////// |
always @(*) |
assume(i_setup[23:0] > 2); |
always @(*) |
assert(fsv_setup[23:0] > 2); |
|
`endif // FORMAL |
endmodule |
|
/txuartlite.v
25,7 → 25,7
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// Copyright (C) 2015-2017, Gisselquist Technology, LLC |
// Copyright (C) 2015-2019, Gisselquist Technology, LLC |
// |
// This program is free software (firmware): you can redistribute it and/or |
// modify it under the terms of the GNU General Public License as published |
67,7 → 67,6
parameter [4:0] TIMING_BITS = 5'd24; |
localparam TB = TIMING_BITS; |
parameter [(TB-1):0] CLOCKS_PER_BAUD = 8; // 24'd868; |
parameter [0:0] F_OPT_CLK2FFLOGIC = 1'b0; |
input wire i_clk; |
input wire i_wr; |
input wire [7:0] i_data; |
192,14 → 191,14
initial baud_counter = 0; |
always @(posedge i_clk) |
begin |
zero_baud_counter <= (baud_counter == 24'h01); |
zero_baud_counter <= (baud_counter == 1); |
if (state == `TXUL_IDLE) |
begin |
baud_counter <= 24'h0; |
baud_counter <= 0; |
zero_baud_counter <= 1'b1; |
if ((i_wr)&&(!r_busy)) |
begin |
baud_counter <= CLOCKS_PER_BAUD - 24'h01; |
baud_counter <= CLOCKS_PER_BAUD - 1'b1; |
zero_baud_counter <= 1'b0; |
end |
end else if ((zero_baud_counter)&&(state == 4'h9)) |
207,9 → 206,9
baud_counter <= 0; |
zero_baud_counter <= 1'b1; |
end else if (!zero_baud_counter) |
baud_counter <= baud_counter - 24'h01; |
baud_counter <= baud_counter - 1'b1; |
else |
baud_counter <= CLOCKS_PER_BAUD - 24'h01; |
baud_counter <= CLOCKS_PER_BAUD - 1'b1; |
end |
|
// |
230,22 → 229,6
|
reg f_past_valid, f_last_clk; |
|
generate if (F_OPT_CLK2FFLOGIC) |
begin |
|
always @($global_clock) |
begin |
restrict(i_clk == !f_last_clk); |
f_last_clk <= i_clk; |
if (!$rose(i_clk)) |
begin |
`ASSUME($stable(i_wr)); |
`ASSUME($stable(i_data)); |
end |
end |
|
end endgenerate |
|
initial f_past_valid = 1'b0; |
always @(posedge i_clk) |
f_past_valid <= 1'b1; |
/ufifo.v
18,7 → 18,7
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// Copyright (C) 2015-2018, Gisselquist Technology, LLC |
// Copyright (C) 2015-2019, Gisselquist Technology, LLC |
// |
// This program is free software (firmware): you can redistribute it and/or |
// modify it under the terms of the GNU General Public License as published |
48,7 → 48,6
parameter BW=8; // Byte/data width |
parameter [3:0] LGFLEN=4; |
parameter RXFIFO=1'b0; |
parameter [0:0] F_OPT_CLK2FFLOGIC = 1'b0; |
input wire i_clk, i_rst; |
input wire i_wr; |
input wire [(BW-1):0] i_data; |
295,24 → 294,6
// |
reg f_past_valid, f_last_clk; |
|
initial restrict(i_rst); |
|
generate if (F_OPT_CLK2FFLOGIC) |
begin |
always @($global_clock) |
begin |
restrict(i_clk == !f_last_clk); |
f_last_clk <= i_clk; |
if (!$rose(i_clk)) |
begin |
`ASSUME($stable(i_rst)); |
`ASSUME($stable(i_wr)); |
`ASSUME($stable(i_data)); |
`ASSUME($stable(i_rd)); |
end |
end |
end endgenerate |
|
// |
// Underflows are a very real possibility, should the user wish to |
// read from this FIFO while it is empty. Our parent module will need |
/wbuart.v
14,7 → 14,7
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// Copyright (C) 2015-2016, Gisselquist Technology, LLC |
// Copyright (C) 2015-2019, Gisselquist Technology, LLC |
// |
// This program is free software (firmware): you can redistribute it and/or |
// modify it under the terms of the GNU General Public License as published |
44,6 → 44,8
`define UART_FIFO 2'b01 |
`define UART_RXREG 2'b10 |
`define UART_TXREG 2'b11 |
// |
// `define USE_LITE_UART |
module wbuart(i_clk, i_rst, |
// |
i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, |
127,7 → 129,7
// valid when stb is high. |
`ifdef USE_LITE_UART |
rxuartlite #(INITIAL_SETUP[23:0]) |
rx(i_clk, (i_rst), i_uart_rx, rx_stb, rx_uart_data); |
rx(i_clk, i_uart_rx, rx_stb, rx_uart_data); |
assign rx_break = 1'b0; |
assign rx_perr = 1'b0; |
assign rx_ferr = 1'b0; |
.
Property changes :
Modified: svn:ignore
## -1 +1,2 ##
obj_dir
+tags