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

Subversion Repositories wbuart32

Compare Revisions

  • This comparison shows the changes necessary to convert path 
    /wbuart32/trunk
    from Rev 25 to Rev 26
    ↔ Reverse comparison
  •

Rev 25 → Rev 26

/Makefile
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
/bench/cpp/Makefile
46,7 → 46,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
176,4 → 176,6
rm -f ./mkspeech ./speech.hex
rm -rf $(OBJDIR)/
 
ifneq ($(MAKECMDGOALS),clean)
-include $(OBJDIR)/depends.txt
endif
/bench/cpp/helloworld.cpp
12,7 → 12,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
/bench/cpp/linetest.cpp
20,7 → 20,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
/bench/cpp/mkspeech.cpp
12,7 → 12,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
/bench/cpp/speechtest.cpp
17,7 → 17,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
/bench/cpp/uartsim.cpp
11,7 → 11,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
/bench/cpp/uartsim.h
14,7 → 14,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
/bench/formal/Makefile
15,7 → 15,7
##
################################################################################
##
## Copyright (C) 2017, Gisselquist Technology, LLC
## Copyright (C) 2017-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
38,52 → 38,38
################################################################################
##
##
TESTS := ufifo txuartlite rxuartlite
TESTS := ufifo txuartlite rxuartlite txuart
.PHONY: $(TESTS)
all: $(TESTS)
RTL := ../../rtl
SMTBMC := yosys-smtbmc
# SOLVER := -s z3
SOLVER := -s yices
# BMCARGS := --presat $(SOLVER)
BMCARGS := $(SOLVER)
INDARGS := $(SOLVER) -i
 
FIFO := ufifo
TX := txuartlite
TX := txuart
TXLITE:= txuartlite
RX := rxuartlite
 
$(FIFO).smt2: $(RTL)/$(FIFO).v $(FIFO).ys
yosys -ql $(FIFO).yslog -s $(FIFO).ys
.PHONY: $(FIFO) $(TX) $(RX) $(TXLITE)
$(FIFO): $(FIFO)/PASS
$(TX): $(TX)/PASS
$(RX): $(RX)_prf/PASS $(RX)_cvr/PASS
$(TXLITE): $(TXLITE)_cvr/PASS $(TXLITE)_prf/PASS
 
$(TX).smt2: $(RTL)/$(TX).v $(TX).ys
yosys -ql $(TX).yslog -s $(TX).ys
$(TX)/PASS: $(TX).sby $(RTL)/$(TX).v
sby -f $(TX).sby
 
$(RX).smt2: $(RTL)/$(RX).v $(RX).ys
yosys -ql $(RX).yslog -s $(RX).ys
$(RX)_prf/PASS: $(RX).sby $(RTL)/$(RX).v
sby -f $(RX).sby prf
$(RX)_cvr/PASS: $(RX).sby $(RTL)/$(RX).v
sby -f $(RX).sby cvr
 
$(FIFO) : $(FIFO).check
$(FIFO).check: $(FIFO).smt2
$(SMTBMC) --presat $(BMCARGS) -t 10 --dump-vcd $(FIFO).vcd $(FIFO).smt2
$(SMTBMC) $(INDARGS) -t 10 --dump-vcd $(FIFO).vcd $(FIFO).smt2
touch $@
$(TXLITE)_cvr/PASS: $(TXLITE).sby $(RTL)/$(TXLITE).v
sby -f $(TXLITE).sby cvr
$(TXLITE)_prf/PASS: $(TXLITE).sby $(RTL)/$(TXLITE).v
sby -f $(TXLITE).sby prf
 
$(TX) : $(TX).check
$(TX).check: $(TX).smt2
$(SMTBMC) --presat $(BMCARGS) -t 90 --dump-vcd $(TX).vcd $(TX).smt2
$(SMTBMC) $(INDARGS) -t 90 --dump-vcd $(TX).vcd $(TX).smt2
$(SMTBMC) -c $(SOLVER) -t 90 --dump-vcd $(TX).vcd $(TX).smt2
touch $@
$(FIFO)/PASS: $(FIFO).sby $(RTL)/$(FIFO).v
sby -f $(FIFO).sby
 
$(RX) : $(RX).check
$(RX).check: $(RX).sby $(RTL)/$(RX).v
sby -f $(RX).sby
touch $@
 
 
.PHONY: clean
clean:
rm -f $(FIFO).smt2 $(FIFO)*.vcd
rm -f $(TX).smt2 $(TX)*.vcd
rm -rf $(RX)_one/ $(RX)_two/
rm -f *.check
rm -rf $(FIFO)/ $(RX)_*/ $(TX)/ $(TXLITE)_cvr/ $(TXLITE)_prf/
/bench/formal/rxuartlite.sby
1,21 → 1,20
[tasks]
one
two
prf
cvr
 
[options]
mode prove
prf: mode prove
cvr: mode cover
multiclock on
one: depth 20
two: depth 120
prf: depth 110
cvr: depth 720
 
[engines]
smtbmc
smtbmc boolector
 
[script]
read -define F_OPT_CLK2FFLOGIC
read -define RXUARTLITE
one: read -sv -formal rxuartlite.v
two: read -sv -D PHASE_TWO -formal rxuartlite.v
prf: read -formal -DRXUARTLITE -D PHASE_TWO rxuartlite.v
cvr: read -formal -DRXUARTLITE -D PHASE_TWO rxuartlite.v
chparam -set CLOCKS_PER_BAUD 16 rxuartlite
prep -top rxuartlite
# opt_merge -share_all
/bench/formal/txuart.sby
0,0 → 1,13
[options]
mode prove
depth 10
 
[engines]
smtbmc boolector
 
[script]
read -formal -DTXUART txuart.v
prep -top txuart
 
[files]
../../rtl/txuart.v
/bench/formal/txuartlite.sby
1,27 → 1,18
[tasks]
verific
yosys
cvr
prf
 
[options]
mode prove
prf: mode prove
cvr: mode cover
depth 90
expect pass
 
[engines]
smtbmc yices
smtbmc boolector
 
[script]
verific:
verific -vlog-define VERIFIC_SVA
verific -sv txuartlite.v
verific -import -extnets -all txuartlite
read -formal -DTXUARTLITE txuartlite.v
prep -top txuartlite
--
 
yosys:
read_verilog -DTXUARTLITE -formal txuartlite.v
prep -top txuartlite
--
 
[files]
../../rtl/txuartlite.v
/bench/formal/ufifo.sby
5,7 → 5,7
smtbmc
 
[script]
read -sv -DUFIFO -formal ufifo.v
read -formal -DUFIFO ufifo.v
prep -top ufifo
 
[files]
/bench/formal
bench/formal Property changes : Modified: svn:ignore ## -8,3 +8,8 ## txuartlite_verific txuartlite_yosys ufifo +rxuartlite_cvr +rxuartlite_prf +txuartlite_cvr +txuartlite_prf +txuart Index: bench/verilog/Makefile =================================================================== --- bench/verilog/Makefile (revision 25) +++ bench/verilog/Makefile (revision 26) @@ -68,7 +68,8 @@ ################################################################################ ## ## -all: test +.PHONY: all +all: test tags YYMMDD=`date +%Y%m%d` CXX := g++ FBDIR := . @@ -75,45 +76,37 @@ VDIRFB:= $(FBDIR)/obj_dir RTLDR := ../../rtl VERILATOR := verilator -VFLAGS := -Wall --MMD --trace -y ../../rtl -cc +VFLAGS := -Wall --MMD --trace -y $(RTLDR) -cc .PHONY: test testline testhello speechfifo test: testline testhello speechfifo -testline: $(VDIRFB)/Vlinetest__ALL.a -testhello: $(VDIRFB)/Vhelloworld__ALL.a +testline: $(VDIRFB)/Vlinetest__ALL.a +testhello: $(VDIRFB)/Vhelloworld__ALL.a speechfifo: $(VDIRFB)/Vspeechfifo__ALL.a -$(VDIRFB)/Vlinetest__ALL.a: $(VDIRFB)/Vlinetest.h $(VDIRFB)/Vlinetest.cpp -$(VDIRFB)/Vlinetest__ALL.a: $(VDIRFB)/Vlinetest.mk -$(VDIRFB)/Vlinetest.h $(VDIRFB)/Vlinetest.cpp $(VDIRFB)/Vlinetest.mk: linetest.v -$(VDIRFB)/Vlinetest.h $(VDIRFB)/Vlinetest.cpp $(VDIRFB)/Vlinetest.mk: $(RTLDR)/rxuart.v $(RTLDR)/txuart.v -$(VDIRFB)/Vlinetest.h $(VDIRFB)/Vlinetest.cpp $(VDIRFB)/Vlinetest.mk: $(RTLDR)/rxuartlite.v $(RTLDR)/txuartlite.v +$(VDIRFB)/Vlinetest__ALL.a: $(VDIRFB)/Vlinetest.cpp +$(VDIRFB)/Vhelloworld__ALL.a: $(VDIRFB)/Vhelloworld.cpp +$(VDIRFB)/Vspeechfifo__ALL.a: $(VDIRFB)/Vspeechfifo.cpp -$(VDIRFB)/Vhelloworld__ALL.a: $(VDIRFB)/Vhelloworld.h $(VDIRFB)/Vhelloworld.cpp -$(VDIRFB)/Vhelloworld__ALL.a: $(VDIRFB)/Vhelloworld.mk -$(VDIRFB)/Vhelloworld.h $(VDIRFB)/Vhelloworld.cpp $(VDIRFB)/Vhelloworld.mk: helloworld.v -$(VDIRFB)/Vhelloworld.h $(VDIRFB)/Vhelloworld.cpp $(VDIRFB)/Vhelloworld.mk: $(RTLDR)/txuartlite.v $(RTLDR)/txuart.v - -SPEECHSRCS := $(addprefix $(RTLDR)/,rxuart.v txuart.v rxuartlite.v txuartlite.v ufifo.v wbuart.v) -SPEECHVFILES:= $(addprefix $(VDIRFB)/,Vspeechfifo.h Vspeechfifo.cpp Vspeechfifo.mk) -$(VDIRFB)/Vspeechfifo__ALL.a: $(VDIRFB)/Vspeechfifo.h $(VDIRFB)/Vspeechfifo.cpp -$(VDIRFB)/Vspeechfifo__ALL.a: $(VDIRFB)/Vspeechfifo.mk -$(SPEECHVFILES): speechfifo.v $(SPEECHSRCS) - -$(VDIRFB)/V%.cpp $(VDIRFB)/V%.h $(VDIRFB)/V%.mk: $(FBDIR)/%.v +$(VDIRFB)/V%.mk: $(VDIRFB)/%.h +$(VDIRFB)/V%.h: $(VDIRFB)/%.cpp +$(VDIRFB)/V%.cpp: $(FBDIR)/%.v $(VERILATOR) $(VFLAGS) $*.v -$(VDIRFB)/V%__ALL.a: $(VDIRFB)/V%.mk +$(VDIRFB)/V%__ALL.a: $(VDIRFB)/V%.cpp cd $(VDIRFB); make -f V$*.mk +tags: $(wildcard *.v) $(wildcard $(RTLDR)/*.v) + ctags *.v $(RTLDR)/*.v + .PHONY: clean clean: - rm -rf $(VDIRFB)/*.mk - rm -rf $(VDIRFB)/*.cpp - rm -rf $(VDIRFB)/*.h - rm -rf $(VDIRFB)/ + rm -rf tags $(VDIRFB)/ -DIRS := $(wildcard $(VDIRFB)/*.d) -ifneq ($(DIRS),) --include $(DIRS) +DEPS := $(wildcard $(VDIRFB)/*.d) + +ifneq ($(MAKECMDGOALS),clean) +ifneq ($(DEPS),) +include $(DEPS) endif +endif
/bench/verilog
bench/verilog Property changes : Modified: svn:ignore ## -1,3 +1,4 ## obj_dir speech.hex speech.inc +tags Index: doc/gpl-3.0.pdf =================================================================== Cannot display: file marked as a binary type. svn:mime-type = application/octet-stream Index: doc/spec.pdf =================================================================== Cannot display: file marked as a binary type. svn:mime-type = application/octet-stream Index: rtl/Makefile =================================================================== --- rtl/Makefile (revision 25) +++ rtl/Makefile (revision 26) @@ -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
/rtl/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
/rtl/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
/rtl/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
 
/rtl/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;
/rtl/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
/rtl/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;
/rtl
rtl Property changes : Modified: svn:ignore ## -1 +1,2 ## obj_dir +tags

powered by: WebSVN 2.1.0

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