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

Subversion Repositories wb2axip

Compare Revisions

  • This comparison shows the changes necessary to convert path 
    /wb2axip/trunk/bench/formal
    from Rev 11 to Rev 16
    ↔ Reverse comparison
  •

Rev 11 → Rev 16

/Makefile
15,30 → 15,34
##
################################################################################
##
## Copyright (C) 2017, Gisselquist Technology, LLC
## Copyright (C) 2017-2018, 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
## by the Free Software Foundation, either version 3 of the License, or (at
## your option) any later version.
## This file is part of the pipelined Wishbone to AXI converter project, a
## project that contains multiple bus bridging designs and formal bus property
## sets.
##
## This program is distributed in the hope that it will be useful, but WITHOUT
## ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
## FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
## for more details.
## The bus bridge designs and property sets are free RTL designs: you can
## redistribute them and/or modify any of them under the terms of the GNU
## Lesser General Public License as published by the Free Software Foundation,
## either version 3 of the License, or (at your option) any later version.
##
## You should have received a copy of the GNU General Public License along
## with this program. (It's in the $(ROOT)/doc directory. Run make with no
## target there if the PDF file isn't present.) If not, see
## The bus bridge designs and property sets are distributed in the hope that
## they will be useful, but WITHOUT ANY WARRANTY; without even the implied
## warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
## GNU Lesser General Public License for more details.
##
## You should have received a copy of the GNU Lesser General Public License
## along with these designs. (It's in the $(ROOT)/doc directory. Run make
## with no target there if the PDF file isn't present.) If not, see
## <http://www.gnu.org/licenses/> for a copy.
##
## License: GPL, v3, as defined and found on www.gnu.org,
## http://www.gnu.org/licenses/gpl.html
## License: LGPL, v3, as defined and found on www.gnu.org,
## http://www.gnu.org/licenses/lgpl.html
##
################################################################################
##
##
TESTS := wbm2axisp wbarbiter # axim2wbsp
TESTS := wbarbiter wbm2axilite axilrd2wbsp axilwr2wbsp demoaxi axlite2wbsp wbxbar # wbm2axisp axim2wbsp
.PHONY: $(TESTS)
all: $(TESTS)
RTL := ../../rtl
50,45 → 54,214
# BMCARGS := $(SOLVER)
INDARGS := $(SOLVER) -i
 
WBARB := wbarbiter
WB2AXI := wbm2axisp
AXI2WB := axim2wbsp
DEMOAXI := demoaxi
WBARB := wbarbiter
WB2AXI := wbm2axisp
AXI2WB := axim2wbsp
WB2LITE := wbm2axilite
RDLITE := axilrd2wbsp
WRLITE := axilwr2wbsp
AXLITE := axlite2wbsp
XILINXDEMO := xlnxdemo
WBXBAR := wbxbar
WBXBAR4x8 := wbxbar4x8
WBXBAR1x8 := wbxbar1x8
WBXBAR4x1 := wbxbar4x1
WB := fwb_master.v fwb_slave.v
 
$(WBARB).smt2: $(RTL)/$(WBARB).v fwb_master.v fwb_slave.v $(WBARB).ys
yosys -ql $(WBARB).yslog -s $(WBARB).ys
.PHONY: $(WBARB) $(WB2AXI) $(RDLITE) $(WRLITE) $(AXLITE) $(WB2LITE) $(DEMOAXI)
 
$(WB2AXI).smt2: $(RTL)/$(WB2AXI).v $(WB2AXI).ys fwb_slave.v faxi_master.v
yosys -ql $(WB2AXI).yslog -s $(WB2AXI).ys
$(WBARB): $(WBARB)_prf/PASS $(WBARB)_cvr/PASS
$(WBARB)_prf/PASS: $(RTL)/$(WBARB).v $(WBARB).sby $(WB)
sby -f $(WBARB).sby
$(WBARB)_cvr/PASS: $(RTL)/$(WBARB).v $(WBARB).sby $(WB)
sby -f $(WBARB).sby
 
$(AXI2WB).smt2: $(RTL)/$(AXI2WB).v $(AXI2WB).ys fwb_master.v faxi_slave.v
$(AXI2WB).smt2: $(RTL)/aximwr2wbsp.v $(RTL)/aximrd2wbsp.v
$(AXI2WB).smt2: $(RTL)/wbarbiter.v
yosys -ql $(AXI2WB).yslog -s $(AXI2WB).ys
.PHONY: $(WB2AXI)
$(WB2AXI): $(WB2AXI)/PASS
$(WB2AXI)/PASS: $(RTL)/$(WB2AXI).v $(WB2AXI).sby $(WB)
sby -f $(WB2AXI).sby
 
$(WBARB) : $(WBARB).check
$(WBARB).check: $(WBARB).smt2
rm -f $@
$(SMTBMC) $(BMCARGS) -t 36 --dump-vcd $(WBARB).vcd $(WBARB).smt2
$(SMTBMC) $(INDARGS) -t 32 --dump-vcd $(WBARB).vcd $(WBARB).smt2
touch $@
$(RDLITE): $(RDLITE)_prf/PASS $(RDLITE)_cvr/PASS
$(RDLITE)_prf/PASS: $(RDLITE).sby $(RTL)/$(RDLITE).v $(WB)
sby -f $(RDLITE).sby prf
$(RDLITE)_cvr/PASS: $(RDLITE).sby $(RTL)/$(RDLITE).v $(WB)
sby -f $(RDLITE).sby cvr
 
$(WB2AXI) : $(WB2AXI).check
$(WB2AXI).check: $(WB2AXI).smt2
rm -f $@
$(SMTBMC) $(BMCARGS) -t 36 --dump-vcd $(WB2AXI).vcd $(WB2AXI).smt2
$(SMTBMC) $(INDARGS) -t 32 --dump-vcd $(WB2AXI).vcd $(WB2AXI).smt2
touch $@
$(WRLITE): $(WRLITE)_prf/PASS $(WRLITE)_cvr/PASS
$(WRLITE)_prf/PASS: $(WRLITE).sby $(RTL)/$(WRLITE).v $(WB)
sby -f $(WRLITE).sby prf
$(WRLITE)_cvr/PASS: $(WRLITE).sby $(RTL)/$(WRLITE).v $(WB)
sby -f $(WRLITE).sby cvr
 
$(AXI2WB) : $(AXI2WB).check
$(AXI2WB).check: $(AXI2WB).smt2
rm -f $@
$(SMTBMC) $(BMCARGS) -t 60 --dump-vcd $(AXI2WB).vcd $(AXI2WB).smt2
$(SMTBMC) $(INDARGS) -t 58 --dump-vcd $(AXI2WB).vcd $(AXI2WB).smt2
touch $@
$(AXLITE): $(AXLITE)_prf/PASS $(AXLITE)_cvr/PASS
AXLITE_DEPS := $(RTL)/$(RDLITE).v $(RTL)/$(WRLITE).v \
$(RTL)/$(WBARB).v fwb_master.v faxil_slave.v \
$(AXLITE).sby $(RTL)/$(AXLITE).v \
$(RDLITE)_prf/PASS $(RDLITE)_cvr/PASS \
$(WRLITE)_prf/PASS $(WRLITE)_cvr/PASS
 
$(AXLITE)_prf/PASS: $(AXLITE_DEPS)
sby -f $(AXLITE).sby prf
 
$(AXLITE)_cvr/PASS: $(AXLITE_DEPS)
sby -f $(AXLITE).sby cvr
 
.PHONY: $(WB2LITE)
$(WB2LITE): $(WB2LITE)_cvr/PASS $(WB2LITE)_prf/PASS
$(WB2LITE)_prf/PASS: $(RTL)/$(WB2LITE).v
$(WB2LITE)_prf/PASS: $(WB2LITE).sby fwb_slave.v faxil_master.v
sby -f $(WB2LITE).sby prf
 
$(WB2LITE)_cvr/PASS: $(RTL)/$(WB2LITE).v
$(WB2LITE)_cvr/PASS: $(WB2LITE).sby fwb_slave.v faxil_master.v
sby -f $(WB2LITE).sby cvr
 
$(DEMOAXI): $(DEMOAXI)_prf/PASS $(DEMOAXI)_cvr/PASS
$(DEMOAXI)_prf/PASS: $(RTL)/$(DEMOAXI).v $(DEMOAXI).sby faxil_slave.v
sby -f $(DEMOAXI).sby prf
$(DEMOAXI)_cvr/PASS: $(RTL)/$(DEMOAXI).v $(DEMOAXI).sby faxil_slave.v
sby -f $(DEMOAXI).sby cvr
 
.PHONY: $(XILINXDEMO)
$(XILINXDEMO): $(XILINXDEMO)_prf/PASS $(XILINXDEMO)_cvr/PASS
$(XILINXDEMO)_prf/PASS: $(XILINXDEMO).v $(XILINXDEMO).sby faxil_slave.v
sby -f $(XILINXDEMO).sby prf
$(XILINXDEMO)_cvr/PASS: $(XILINXDEMO).v $(XILINXDEMO).sby faxil_slave.v
sby -f $(XILINXDEMO).sby cvr
 
 
.PHONY: $(AXI2WB)
$(AXI2WB)/PASS: $(RTL)/$(AXI2WB).v $(AXI2WB).sby
$(AXI2WB)/PASS: $(WB)
$(AXI2WB)/PASS: faxi_slave.v
$(AXI2WB)/PASS: f_order.v
$(AXI2WB)/PASS: $(RTL)/aximwr2wbsp.v $(RTL)/aximrd2wbsp.v
$(AXI2WB)/PASS: $(RTL)/wbarbiter.v
echo "The AXI2WB bridge does not work yet, so I do not expect this one to pass"
echo sby -f $(AXI2WB).sby
 
.PHONY: $(WBXBAR) $(WBXBAR4x8) $(WBXBAR1x8) $(WBXBAR4x1)
$(WBXBAR): $(WBXBAR4x8) $(WBXBAR1x8) $(WBXBAR4x1)
$(WBXBAR4x8): wbxbar_prf4x8_buflp/PASS
wbxbar_prf4x8_buflp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_buflp
$(WBXBAR4x8): wbxbar_prf4x8_buf/PASS
wbxbar_prf4x8_buf/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_buf
$(WBXBAR4x8): wbxbar_prf4x8_lp/PASS
wbxbar_prf4x8_lp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_lp
$(WBXBAR4x8): wbxbar_prf4x8_cheap/PASS
wbxbar_prf4x8_cheap/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_cheap
$(WBXBAR4x8): wbxbar_prf4x8_buflpko/PASS
wbxbar_prf4x8_buflpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_buflpko
$(WBXBAR4x8): wbxbar_prf4x8_bufko/PASS
wbxbar_prf4x8_bufko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_bufko
$(WBXBAR4x8): wbxbar_prf4x8_lpko/PASS
wbxbar_prf4x8_lpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_lpko
$(WBXBAR4x8): wbxbar_prf4x8_cheapko/PASS
wbxbar_prf4x8_cheapko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_cheapko
$(WBXBAR4x8): wbxbar_prf4x8_buflpkos/PASS
wbxbar_prf4x8_buflpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_buflpkos
$(WBXBAR4x8): wbxbar_prf4x8_bufkos/PASS
wbxbar_prf4x8_bufkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_bufkos
$(WBXBAR4x8): wbxbar_prf4x8_lpkos/PASS
wbxbar_prf4x8_lpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_lpkos
$(WBXBAR4x8): wbxbar_prf4x8_cheapkos/PASS
wbxbar_prf4x8_cheapkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x8_cheapkos
$(WBXBAR1x8): wbxbar_prf1x8_buflp/PASS
wbxbar_prf1x8_buflp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_buflp
$(WBXBAR1x8): wbxbar_prf1x8_buf/PASS
wbxbar_prf1x8_buf/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_buf
$(WBXBAR1x8): wbxbar_prf1x8_lp/PASS
wbxbar_prf1x8_lp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_lp
$(WBXBAR1x8): wbxbar_prf1x8_cheap/PASS
wbxbar_prf1x8_cheap/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_cheap
$(WBXBAR1x8): wbxbar_prf1x8_buflpko/PASS
wbxbar_prf1x8_buflpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_buflpko
$(WBXBAR1x8): wbxbar_prf1x8_bufko/PASS
wbxbar_prf1x8_bufko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_bufko
$(WBXBAR1x8): wbxbar_prf1x8_lpko/PASS
wbxbar_prf1x8_lpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_lpko
$(WBXBAR1x8): wbxbar_prf1x8_cheapko/PASS
wbxbar_prf1x8_cheapko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_cheapko
$(WBXBAR1x8): wbxbar_prf1x8_buflpkos/PASS
wbxbar_prf1x8_buflpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_buflpkos
$(WBXBAR1x8): wbxbar_prf1x8_bufkos/PASS
wbxbar_prf1x8_bufkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_bufkos
$(WBXBAR1x8): wbxbar_prf1x8_lpkos/PASS
wbxbar_prf1x8_lpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_lpkos
$(WBXBAR1x8): wbxbar_prf1x8_cheapkos/PASS
wbxbar_prf1x8_cheapkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf1x8_cheapkos
$(WBXBAR4x1): wbxbar_prf4x1_buflp/PASS
wbxbar_prf4x1_buflp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_buflp
$(WBXBAR4x1): wbxbar_prf4x1_buf/PASS
wbxbar_prf4x1_buf/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_buf
$(WBXBAR4x1): wbxbar_prf4x1_lp/PASS
wbxbar_prf4x1_lp/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_lp
$(WBXBAR4x1): wbxbar_prf4x1_cheap/PASS
wbxbar_prf4x1_cheap/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_cheap
$(WBXBAR4x1): wbxbar_prf4x1_buflpko/PASS
wbxbar_prf4x1_buflpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_buflpko
$(WBXBAR4x1): wbxbar_prf4x1_bufko/PASS
wbxbar_prf4x1_bufko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_bufko
$(WBXBAR4x1): wbxbar_prf4x1_lpko/PASS
wbxbar_prf4x1_lpko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_lpko
$(WBXBAR4x1): wbxbar_prf4x1_cheapko/PASS
wbxbar_prf4x1_cheapko/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_cheapko
$(WBXBAR4x1): wbxbar_prf4x1_buflpkos/PASS
wbxbar_prf4x1_buflpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_buflpkos
$(WBXBAR4x1): wbxbar_prf4x1_bufkos/PASS
wbxbar_prf4x1_bufkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_bufkos
$(WBXBAR4x1): wbxbar_prf4x1_lpkos/PASS
wbxbar_prf4x1_lpkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_lpkos
$(WBXBAR4x1): wbxbar_prf4x1_cheapkos/PASS
wbxbar_prf4x1_cheapkos/PASS: $(WBXBAR).sby $(RTL)/$(WBXBAR).v $(WB)
sby -f $(WBXBAR).sby prf4x1_cheapkos
 
.PHONY: clean
clean:
rm -f $(WBARB).smt2 $(WBARB).yslog $(WBARB)*.vcd
rm -f $(WB2AXI).smt2 $(WB2AXI).yslog $(WB2AXI)*.vcd
rm -f $(AXI2WB).smt2 $(AXI2WB).yslog $(AXI2WB)*.vcd
rm -f *.check
rm -rf $(WBARB)_prf/ $(WBARB)_cvr/
rm -rf $(WB2LITE)_cvr/ $(WB2LITE)_prf/
rm -rf $(RDLITE)_cvr/ $(RDLITE)_prf
rm -rf $(WRLITE)_cvr/ $(WRLITE)_prf
rm -rf $(AXLITE)_cvr/ $(AXLITE)_prf
rm -rf $(DEMOAXI)_cvr/ $(DEMOAXI)_prf
@# The three broken cores, to include Xilinx's
rm -rf $(WB2AXI)/
rm -rf $(AXI2WB)/
rm -rf $(XILINXDEMO)_cvr/ $(XILINXDEMO)_prf
# rm -f *.check
/axilrd2wbsp.gtkw
0,0 → 1,70
[*]
[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
[*] Fri Dec 28 05:15:33 2018
[*]
[dumpfile] "(null)"
[savefile] "/home/dan/jericho/work/rnd/opencores/wb2axip/trunk/bench/formal/axilrd2wbsp.gtkw"
[timestart] 0
[size] 1898 600
[pos] -1 -1
*-5.054117 210 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 270
[signals_width] 210
[sst_expanded] 1
[sst_vpaned_height] 143
@28
[color] 3
axilrd2wbsp.i_axi_reset_n
[color] 3
axilrd2wbsp.i_clk
@200
-
@28
axilrd2wbsp.i_axi_arvalid
axilrd2wbsp.o_axi_arready
@22
axilrd2wbsp.i_axi_araddr[27:0]
axilrd2wbsp.i_axi_arcache[3:0]
@28
axilrd2wbsp.i_axi_arprot[2:0]
@200
-
@28
[color] 2
axilrd2wbsp.o_axi_rvalid
[color] 2
axilrd2wbsp.i_axi_rready
@22
[color] 2
axilrd2wbsp.o_axi_rdata[31:0]
@28
[color] 2
axilrd2wbsp.o_axi_rresp[1:0]
@200
-
@28
axilrd2wbsp.o_wb_cyc
axilrd2wbsp.o_wb_stb
@22
axilrd2wbsp.o_wb_addr[25:0]
@28
[color] 2
axilrd2wbsp.i_wb_stall
[color] 2
axilrd2wbsp.i_wb_ack
@23
[color] 2
axilrd2wbsp.i_wb_data[31:0]
@28
[color] 2
axilrd2wbsp.i_wb_err
@200
-
@28
[color] 3
axilrd2wbsp.r_stb
@22
[color] 3
axilrd2wbsp.r_addr[25:0]
[pattern_trace] 1
[pattern_trace] 0
/axilrd2wbsp.sby
0,0 → 1,23
[tasks]
cvr
prf
 
[options]
prf: mode prove
prf: depth 5
cvr: mode cover
cvr: depth 32
 
[engines]
smtbmc
 
[script]
read -formal -D AXILRD2WBSP axilrd2wbsp.v
read -formal -D AXILRD2WBSP faxil_slave.v
read -formal -D AXILRD2WBSP fwb_master.v
prep -top axilrd2wbsp
 
[files]
../../rtl/axilrd2wbsp.v
faxil_slave.v
fwb_master.v
/axilwr2wbsp.sby
0,0 → 1,23
[tasks]
prf
cvr
 
[options]
prf: mode prove
prf: depth 5
cvr: mode cover
cvr: depth 40
 
[engines]
smtbmc
 
[script]
read -formal -D AXILWR2WBSP axilwr2wbsp.v
read -formal -D AXILWR2WBSP faxil_slave.v
read -formal -D AXILWR2WBSP fwb_master.v
prep -top axilwr2wbsp
 
[files]
../../rtl/axilwr2wbsp.v
faxil_slave.v
fwb_master.v
/axim2wbsp.ys
5,7 → 5,6
read_verilog -D AXIM2WBSP -formal fwb_master.v
read_verilog -D AXIM2WBSP -formal fwb_slave.v
read_verilog -D AXIM2WBSP -formal faxi_slave.v
read_verilog -D AXIM2WBSP -formal f_order.v
prep -top axim2wbsp -nordff
clk2fflogic
opt -share_all
write_smt2 -wires axim2wbsp.smt2
/axlite2wbsp.gtkw
0,0 → 1,122
[*]
[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
[*] Fri Dec 28 11:45:02 2018
[*]
[dumpfile] "(null)"
[savefile] "/home/dan/jericho/work/rnd/opencores/wb2axip/trunk/bench/formal/axlite2wbsp.gtkw"
[timestart] 0
[size] 1920 1021
[pos] -1 -1
*-6.124164 160 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[treeopen] axlite2wbsp.
[treeopen] axlite2wbsp.ARB_WB.
[treeopen] axlite2wbsp.AXI_RD.
[treeopen] axlite2wbsp.AXI_RD.axi_read_decoder.
[treeopen] axlite2wbsp.AXI_WR.
[treeopen] axlite2wbsp.AXI_WR.axi_write_decoder.
[sst_width] 270
[signals_width] 210
[sst_expanded] 1
[sst_vpaned_height] 290
@28
[color] 3
axlite2wbsp.i_axi_reset_n
[color] 3
axlite2wbsp.o_reset
[color] 3
axlite2wbsp.i_clk
@200
-
@28
[color] 2
axlite2wbsp.i_axi_awvalid
[color] 2
axlite2wbsp.o_axi_awready
@22
[color] 2
axlite2wbsp.i_axi_awaddr[27:0]
@c00022
[color] 2
axlite2wbsp.i_axi_awcache[3:0]
@28
(0)axlite2wbsp.i_axi_awcache[3:0]
(1)axlite2wbsp.i_axi_awcache[3:0]
(2)axlite2wbsp.i_axi_awcache[3:0]
(3)axlite2wbsp.i_axi_awcache[3:0]
@1401200
-group_end
@28
[color] 2
axlite2wbsp.i_axi_awprot[2:0]
@200
-
@28
[color] 2
axlite2wbsp.i_axi_wvalid
[color] 2
axlite2wbsp.o_axi_wready
@22
[color] 2
axlite2wbsp.i_axi_wdata[31:0]
[color] 2
axlite2wbsp.i_axi_wstrb[3:0]
@28
[color] 2
axlite2wbsp.AXI_WR.axi_write_decoder.err_state
@200
-
@28
[color] 3
axlite2wbsp.o_axi_bvalid
[color] 3
axlite2wbsp.i_axi_bready
[color] 3
axlite2wbsp.o_axi_bresp[1:0]
@200
-
@28
axlite2wbsp.i_axi_arvalid
axlite2wbsp.o_axi_arready
@22
axlite2wbsp.i_axi_araddr[27:0]
axlite2wbsp.i_axi_arcache[3:0]
@28
axlite2wbsp.i_axi_arprot[2:0]
@200
-
@28
[color] 2
axlite2wbsp.o_axi_rvalid
[color] 2
axlite2wbsp.i_axi_rready
@22
[color] 2
axlite2wbsp.o_axi_rdata[31:0]
@28
[color] 2
axlite2wbsp.o_axi_rresp[1:0]
[color] 2
axlite2wbsp.AXI_RD.axi_read_decoder.err_state
@200
-
@28
axlite2wbsp.o_wb_cyc
axlite2wbsp.o_wb_stb
axlite2wbsp.o_wb_we
@22
axlite2wbsp.o_wb_addr[25:0]
axlite2wbsp.o_wb_data[31:0]
axlite2wbsp.o_wb_sel[3:0]
@28
[color] 2
axlite2wbsp.i_wb_stall
[color] 2
axlite2wbsp.i_wb_ack
@22
[color] 2
axlite2wbsp.i_wb_data[31:0]
@28
[color] 2
axlite2wbsp.i_wb_err
[pattern_trace] 1
[pattern_trace] 0
/axlite2wbsp.sby
0,0 → 1,31
[tasks]
cvr
prf
 
[options]
prf: mode prove
prf: depth 5
cvr: mode cover
cvr: depth 40
 
[engines]
smtbmc
 
[script]
read -formal -D AXLITE2WBSP axlite2wbsp.v
read -formal -D AXLITE2WBSP axilrd2wbsp.v
read -formal -D AXLITE2WBSP axilwr2wbsp.v
read -formal -D AXLITE2WBSP wbarbiter.v
read -formal -D AXLITE2WBSP faxil_slave.v
read -formal -D AXLITE2WBSP fwb_master.v
read -formal -D AXLITE2WBSP fwb_slave.v
prep -top axlite2wbsp
 
[files]
../../rtl/axlite2wbsp.v
../../rtl/axilrd2wbsp.v
../../rtl/axilwr2wbsp.v
../../rtl/wbarbiter.v
faxil_slave.v
fwb_master.v
fwb_slave.v
/demoaxi.gtkw
0,0 → 1,71
[*]
[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
[*] Wed Dec 26 15:57:11 2018
[*]
[dumpfile] "/home/dan/jericho/work/rnd/opencores/wb2axip/trunk/bench/formal/demoaxi_cvr/engine_0/trace2.vcd"
[dumpfile_mtime] "Wed Dec 26 15:51:31 2018"
[dumpfile_size] 26484
[savefile] "/home/dan/jericho/work/rnd/opencores/wb2axip/trunk/bench/formal/demoaxi.gtkw"
[timestart] 0
[size] 1600 600
[pos] -1 -1
*-6.254814 180 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 270
[signals_width] 200
[sst_expanded] 1
[sst_vpaned_height] 143
@29
[color] 3
demoaxi.S_AXI_ARESETN
[color] 3
demoaxi.S_AXI_ACLK
@200
-
@28
demoaxi.S_AXI_AWVALID
demoaxi.S_AXI_AWREADY
@22
demoaxi.S_AXI_AWADDR[7:0]
@28
demoaxi.S_AXI_AWPROT[2:0]
@200
-
@28
demoaxi.S_AXI_WVALID
demoaxi.S_AXI_WREADY
@22
demoaxi.S_AXI_WDATA[31:0]
demoaxi.S_AXI_WSTRB[3:0]
@200
-
@28
[color] 2
demoaxi.S_AXI_BVALID
[color] 2
demoaxi.S_AXI_BREADY
[color] 2
demoaxi.S_AXI_BRESP[1:0]
@200
-
@28
demoaxi.S_AXI_ARVALID
demoaxi.S_AXI_ARREADY
@22
demoaxi.S_AXI_ARADDR[7:0]
@28
demoaxi.S_AXI_ARPROT[2:0]
@200
-
@28
[color] 2
demoaxi.S_AXI_RVALID
[color] 2
demoaxi.S_AXI_RREADY
@22
[color] 2
demoaxi.S_AXI_RDATA[31:0]
@28
[color] 2
demoaxi.S_AXI_RRESP[1:0]
[pattern_trace] 1
[pattern_trace] 0
/demoaxi.sby
0,0 → 1,21
[tasks]
prf
cvr
 
[options]
prf: mode prove
prf: depth 26
cvr: mode cover
cvr: depth 40
 
[engines]
smtbmc
 
[script]
read -formal demoaxi.v
read -formal faxil_slave.v
prep -top demoaxi
 
[files]
../../rtl/demoaxi.v
faxil_slave.v
/fav_slave.v
15,25 → 15,28
//
// Copyright (C) 2015-2016, 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
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
// This file is part of the pipelined Wishbone to AXI converter project, a
// project that contains multiple bus bridging designs and formal bus property
// sets.
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
// for more details.
// The bus bridge designs and property sets are free RTL designs: you can
// redistribute them and/or modify any of them under the terms of the GNU
// Lesser General Public License as published by the Free Software Foundation,
// either version 3 of the License, or (at your option) any later version.
//
// You should have received a copy of the GNU General Public License along
// with this program. (It's in the $(ROOT)/doc directory, run make with no
// target there if the PDF file isn't present.) If not, see
// The bus bridge designs and property sets are distributed in the hope that
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with these designs. (It's in the $(ROOT)/doc directory. Run make
// with no target there if the PDF file isn't present.) If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License: GPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/gpl.html
// License: LGPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/lgpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
88,31 → 91,106
always @(*)
assert((f_past_valid) || (i_reset));
 
wire [AW:0] f_rd_request;
assign f_rd_request = { i_av_read, i_av_address };
wire [AW+(DW/8):0] f_rd_request;
assign f_rd_request = { i_av_read, i_av_byteenable, i_av_address };
 
wire [(AW+DW+(DW/8)):0] f_wr_request;
assign f_wr_request = { i_av_write, i_av_address, i_av_writedata,
i_av_byteenable };
 
/////////////////////////////
//
// Require that nothing changes, save on a clock tick.
//
// This is only required if yosys is using the clk2fflogic
// command, a command only required if multiple clocks are
// in use. Since this can greatly slow down formal proofs,
// we limit any code associated with this option to only
// those times the option is in play.
//
/////////////////////////////
 
always @($global_clock)
if ((f_past_valid)&&(!$rose(i_clk)))
generate if (F_OPT_CLK2FFLOGIC)
begin
assume($stable(f_rd_request));
assume($stable(f_wr_request));
assume($stable(i_av_lock));
always @($global_clock)
if ((f_past_valid)&&(!$rose(i_clk)))
begin
assume($stable(f_rd_request));
assume($stable(f_wr_request));
assume($stable(i_av_lock));
 
assert($stable(i_av_readdatavalid));
assert($stable(i_av_writeresponsevalid));
assert($stable(i_av_readdata));
assert($stable(i_av_response));
end
assert($stable(i_av_readdatavalid));
assert($stable(i_av_writeresponsevalid));
assert($stable(i_av_readdata));
assert($stable(i_av_response));
end
end endgenerate
 
/////////////////////////////
//
// Assumptions about a slave's inputs
//
/////////////////////////////
 
 
initial assume(!i_av_read);
initial assume(!i_av_write);
initial assume(!i_av_lock);
//
initial assert(!i_av_readdatavalid);
initial assert(!i_av_writeresponsevalid);
//
 
always @(posedge i_clk)
if (i_reset)
begin
assume(!i_av_read);
assume(!i_av_write);
assume(!i_av_lock);
end
 
always @(*)
if (i_av_write)
assume(|i_av_byteenable);
 
// It is a protocol violation to issue both read and write requests
// on the same clock
always @(*)
assume((!i_av_read)||(!i_av_write));
 
// Once a read request has been placed upon the bus, it will remain
// there until wait request goes low
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_read)))
assume((i_reset)||(f_rd_request == $past(f_rd_request)));
 
// Same thing for a write request
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_write)))
assume((i_reset)||(f_wr_request == $past(f_wr_request)));
 
// A lock request can only be asserted at the same time a read or
// write request is being made.
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_av_lock)))
assume((!i_av_lock)||(i_av_read)||(i_av_write));
 
// A lock request can only be de-asserted following the last read
// or write request made with it asserted
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_av_lock)
&&(!i_av_read)&&(!i_av_write)))
assume((i_reset)||(i_av_lock)
||(i_av_read)||(i_av_write));
 
 
/////////////////////////////
//
// Internal state variables
//
/////////////////////////////
 
// Count the number of read requests
initial f_rd_nreqs = 0;
always @(posedge i_clk)
if (i_reset)
120,6 → 198,7
else if ((i_av_read)&&(!i_av_waitrequest))
f_rd_nreqs <= f_rd_nreqs + 1'b1;
 
// Count the number of read acknowledgements
initial f_rd_nacks = 0;
always @(posedge i_clk)
if (i_reset)
127,8 → 206,11
else if (i_av_readdatavalid)
f_rd_nacks <= f_rd_nacks + 1'b1;
 
assign f_rd_outstanding = f_rd_nreqs - f_rd_nacks;
// The difference between read requests and acknowledgements is
// the number of outstanding read requests
assign f_rd_outstanding = (i_reset) ? 0 : (f_rd_nreqs - f_rd_nacks);
 
// Count the number of write requests
initial f_wr_nreqs = 0;
always @(posedge i_clk)
if (i_reset)
136,6 → 218,7
else if ((i_av_write)&&(!i_av_waitrequest))
f_wr_nreqs <= f_wr_nreqs + 1'b1;
 
// Count the number of write acknowledgements/responses
initial f_wr_nacks = 0;
always @(posedge i_clk)
if (i_reset)
172,26 → 255,85
assert(f_wr_nacks == 0);
end
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_read)))
assume($stable(f_rd_request));
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_av_waitrequest))&&($past(i_av_write)))
assume($stable(f_wr_request));
 
// Just like a read and write request cannot both be made at the same
// time, neither can both responses come back at the same time
always @(*)
assume((!i_av_read)||(!i_av_write));
 
always @(*)
assert((!i_av_writeresponsevalid)||(!i_av_readdatavalid));
 
// If nothing is outstanding, then there should be no responses.
// If i_reset is asserted, a response may have been registered, and
// so may still return on this clock.
always @(posedge i_clk)
if (f_rd_outstanding == 0)
if ((f_rd_outstanding == 0)&&(!i_reset)
&&((!i_av_read)||(i_av_waitrequest)))
assert(!i_av_readdatavalid);
 
always @(posedge i_clk)
if (f_wr_outstanding == 0)
if ((f_wr_outstanding == 0)&&(!i_reset)
&&((!i_av_write)||(i_av_waitrequest)))
assert(!i_av_writeresponsevalid);
 
always @(*)
assert({1'b0, f_wr_outstanding} + { 1'b0, f_rd_outstanding }
< F_MAX_REQUESTS);
 
generate if (F_OPT_MAX_STALL > 0)
begin
reg [(LGWAIT-1):0] stall_count;
 
initial stall_count = 0;
always @(posedge i_clk)
if (i_reset)
stall_count <= 0;
else if (((i_av_read)||(i_av_write))&&(i_av_waitrequest))
stall_count <= stall_count + 1'b1;
else
stall_count <= 0;
 
always @(*)
assert((i_reset)||(stall_count < F_OPT_MAX_STALL));
end endgenerate
 
generate if (F_OPT_MAX_WAIT > 0)
begin
reg [(LGWAIT-1):0] read_wait, write_wait;
 
//
// Insist on a minimum amount of time to wait for a *read*
// response.
//
always @(posedge i_clk)
if (i_reset)
read_wait <= 0;
else if ((i_av_readdatavalid)
||((i_av_read)&&(!i_av_waitrequest)))
read_wait <= 0;
else if (f_rd_outstanding > 0)
read_wait <= read_wait + 1'b1;
 
always @(*)
assert((i_av_readdatavalid)
||(f_rd_outstanding == 0)
||(read_wait < F_OPT_MAX_WAIT));
 
 
//
// Insist on a minimum amount of time to wait for a *write*
// response.
//
always @(posedge i_clk)
if (i_reset)
write_wait <= 0;
else if ((i_av_writeresponsevalid)
||((i_av_write)&&(!i_av_waitrequest)))
write_wait <= 0;
else if (f_wr_outstanding > 0)
write_wait <= write_wait + 1'b1;
 
always @(*)
assert((i_av_writeresponsevalid)
||(f_wr_outstanding == 0)
||(write_wait < F_OPT_MAX_WAIT));
end endgenerate
 
endmodule
/faxi_master.v
13,25 → 13,28
//
// Copyright (C) 2017, 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
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
// This file is part of the pipelined Wishbone to AXI converter project, a
// project that contains multiple bus bridging designs and formal bus property
// sets.
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
// for more details.
// The bus bridge designs and property sets are free RTL designs: you can
// redistribute them and/or modify any of them under the terms of the GNU
// Lesser General Public License as published by the Free Software Foundation,
// either version 3 of the License, or (at your option) any later version.
//
// You should have received a copy of the GNU General Public License along
// with this program. (It's in the $(ROOT)/doc directory, run make with no
// target there if the PDF file isn't present.) If not, see
// The bus bridge designs and property sets are distributed in the hope that
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with these designs. (It's in the $(ROOT)/doc directory. Run make
// with no target there if the PDF file isn't present.) If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License: GPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/gpl.html
// License: LGPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/lgpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
44,18 → 47,20
parameter C_AXI_ADDR_WIDTH = 28, // AXI Address width (log wordsize)
localparam DW = C_AXI_DATA_WIDTH,
localparam AW = C_AXI_ADDR_WIDTH,
parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXSTALL = 3,
parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXDELAY = 3,
parameter [0:0] F_STRICT_ORDER = 0, // Reorder, or not? 0 -> Reorder
parameter [0:0] F_CONSECUTIVE_IDS= 0, // 0=ID's must be consecutive
parameter [0:0] F_OPT_BURSTS = 1'b1, // Check burst lengths
parameter [0:0] F_CHECK_IDS = 1'b1 // Check ID's upon issue&return
parameter [0:0] F_CHECK_IDS = 1'b1, // Check ID's upon issue&return
parameter [7:0] F_AXI_MAXBURST = 8'hff,// Maximum burst length, minus 1
parameter [0:0] F_OPT_CLK2FFLOGIC= 1'b0, // Multiple clock testing?
parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXSTALL = 3,
parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXDELAY = 3
) (
input i_clk, // System clock
input i_axi_reset_n,
input wire i_clk, // System clock
input wire i_axi_reset_n,
 
// AXI write address channel signals
input i_axi_awready, // Slave is ready to accept
input wire i_axi_awready,//Slave is ready to accept
input wire [C_AXI_ID_WIDTH-1:0] i_axi_awid, // Write ID
input wire [AW-1:0] i_axi_awaddr, // Write address
input wire [7:0] i_axi_awlen, // Write Burst Length
76,7 → 81,7
 
// AXI write response channel signals
input wire [C_AXI_ID_WIDTH-1:0] i_axi_bid, // Response ID
input wire [1:0] i_axi_bresp, // Write response
input wire [1:0] i_axi_bresp, // Write response
input wire i_axi_bvalid, // Write reponse valid
input wire i_axi_bready, // Response ready
 
95,9 → 100,9
 
// AXI read data channel signals
input wire [C_AXI_ID_WIDTH-1:0] i_axi_rid, // Response ID
input wire [1:0] i_axi_rresp, // Read response
input wire [1:0] i_axi_rresp, // Read response
input wire i_axi_rvalid, // Read reponse valid
input wire [DW-1:0] i_axi_rdata, // Read data
input wire [DW-1:0] i_axi_rdata, // Read data
input wire i_axi_rlast, // Read last
input wire i_axi_rready, // Read Response ready
//
106,8 → 111,10
output reg [(C_AXI_ID_WIDTH-1):0] f_axi_awr_outstanding,
output reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_rd_id_outstanding,
output reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_awr_id_outstanding,
output reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_wr_id_outstanding
 
output reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_wr_id_outstanding,
// output reg [(9-1):0] f_axi_wr_pending,
// output reg [(9-1):0] f_axi_rd_count,
output reg [(9-1):0] f_axi_wr_count
);
reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_wr_id_complete;
 
130,6 → 137,8
: 8))));
localparam LGFIFOLN = C_AXI_ID_WIDTH;
localparam FIFOLN = (1<<LGFIFOLN);
localparam F_LGDEPTH = C_AXI_ID_WIDTH;
localparam F_AXI_MAXWAIT = F_AXI_MAXSTALL;
 
 
//*****************************************************************************
136,22 → 145,6
// Internal register and wire declarations
//*****************************************************************************
 
// Things we're not changing ...
always @(*)
begin
assert(i_axi_awlen == 8'h0); // Burst length is one
assert(i_axi_awsize == 3'b101); // maximum bytes per burst is 32
assert(i_axi_awburst == 2'b01); // Incrementing address (ignored)
assert(i_axi_arburst == 2'b01); // Incrementing address (ignored)
assert(i_axi_awlock == 1'b0); // Normal signaling
assert(i_axi_arlock == 1'b0); // Normal signaling
assert(i_axi_awcache == 4'h2); // Normal: no cache, no buffer
assert(i_axi_arcache == 4'h2); // Normal: no cache, no buffer
assert(i_axi_awprot == 3'b010);// Unpriviledged, unsecure, data access
assert(i_axi_arprot == 3'b010);// Unpriviledged, unsecure, data access
assert(i_axi_awqos == 4'h0); // Lowest quality of service (unused)
assert(i_axi_arqos == 4'h0); // Lowest quality of service (unused)
end
 
// wire w_fifo_full;
wire axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req,
166,6 → 159,9
assign axi_rd_err = (axi_rd_ack)&&(i_axi_rresp[1]);
assign axi_wr_err = (axi_wr_ack)&&(i_axi_bresp[1]);
 
`define SLAVE_ASSUME assert
`define SLAVE_ASSERT assume
 
//
// Setup
//
176,239 → 172,278
always @(posedge i_clk)
f_past_valid <= 1'b1;
always @(*)
if (!f_past_valid)
assert(!i_axi_reset_n);
if (!f_past_valid)
assert(!i_axi_reset_n);
 
//
// All signals must be synchronous with the clock
//
always @($global_clock)
if (f_past_valid) begin
// Assume our inputs will only change on the positive edge
// of the clock
if (!$rose(i_clk))
begin
// AXI inputs
assume($stable(i_axi_awready));
assume($stable(i_axi_wready));
//
assume($stable(i_axi_bid));
assume($stable(i_axi_bresp));
assume($stable(i_axi_bvalid));
assume($stable(i_axi_arready));
//
assume($stable(i_axi_rid));
assume($stable(i_axi_rresp));
assume($stable(i_axi_rvalid));
assume($stable(i_axi_rdata));
assume($stable(i_axi_rlast));
//
// AXI outputs
//
assert($stable(i_axi_awvalid));
assert($stable(i_axi_awid));
assert($stable(i_axi_awlen));
assert($stable(i_axi_awsize));
assert($stable(i_axi_awlock));
assert($stable(i_axi_awcache));
assert($stable(i_axi_awprot));
assert($stable(i_axi_awqos));
//
assert($stable(i_axi_wvalid));
assert($stable(i_axi_wdata));
assert($stable(i_axi_wstrb));
assert($stable(i_axi_wlast));
//
assert($stable(i_axi_arvalid));
assert($stable(i_axi_arid));
assert($stable(i_axi_arlen));
assert($stable(i_axi_arsize));
assert($stable(i_axi_arburst));
assert($stable(i_axi_arlock));
assert($stable(i_axi_arprot));
assert($stable(i_axi_arqos));
//
assert($stable(i_axi_bready));
//
assert($stable(i_axi_rready));
//
// Formal outputs
//
assert($stable(f_axi_rd_outstanding));
assert($stable(f_axi_wr_outstanding));
assert($stable(f_axi_awr_outstanding));
generate if (F_OPT_CLK2FFLOGIC)
begin
 
always @($global_clock)
if (f_past_valid) begin
// Assume our inputs will only change on the positive
// edge of the clock
if (!$rose(i_clk))
begin
// AXI inputs
assume($stable(i_axi_awready));
assume($stable(i_axi_wready));
//
assume($stable(i_axi_bid));
assume($stable(i_axi_bresp));
assume($stable(i_axi_bvalid));
assume($stable(i_axi_arready));
//
assume($stable(i_axi_rid));
assume($stable(i_axi_rresp));
assume($stable(i_axi_rvalid));
assume($stable(i_axi_rdata));
assume($stable(i_axi_rlast));
//
// AXI outputs
//
assert($stable(i_axi_awvalid));
assert($stable(i_axi_awid));
assert($stable(i_axi_awlen));
assert($stable(i_axi_awsize));
assert($stable(i_axi_awlock));
assert($stable(i_axi_awcache));
assert($stable(i_axi_awprot));
assert($stable(i_axi_awqos));
//
assert($stable(i_axi_wvalid));
assert($stable(i_axi_wdata));
assert($stable(i_axi_wstrb));
assert($stable(i_axi_wlast));
//
assert($stable(i_axi_arvalid));
assert($stable(i_axi_arid));
assert($stable(i_axi_arlen));
assert($stable(i_axi_arsize));
assert($stable(i_axi_arburst));
assert($stable(i_axi_arlock));
assert($stable(i_axi_arprot));
assert($stable(i_axi_arqos));
//
assert($stable(i_axi_bready));
//
assert($stable(i_axi_rready));
//
// Formal outputs
//
assert($stable(f_axi_rd_outstanding));
assert($stable(f_axi_wr_outstanding));
assert($stable(f_axi_awr_outstanding));
end
end
end
end endgenerate
 
////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
//
//
// Reset properties
//
//
////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
 
//
// If asserted, the reset must be asserted for a minimum of 16 clocks
reg [3:0] f_reset_length;
initial f_reset_length = 0;
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_axi_reset_n)))
if (i_axi_reset_n)
f_reset_length <= 0;
else if (!(&f_reset_length))
f_reset_length <= f_reset_length + 1'b1;
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
`SLAVE_ASSUME(!i_axi_reset_n);
 
always @(*)
if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
`SLAVE_ASSUME(!i_axi_reset_n);
 
always @(posedge i_clk)
if ((!f_past_valid)||(!$past(i_axi_reset_n)))
begin
assert(!i_axi_arvalid);
assert(!i_axi_awvalid);
assert(!i_axi_wvalid);
assume(!i_axi_bvalid);
assume(!i_axi_rvalid);
`SLAVE_ASSUME(!i_axi_arvalid);
`SLAVE_ASSUME(!i_axi_awvalid);
`SLAVE_ASSUME(!i_axi_wvalid);
//
`SLAVE_ASSERT(!i_axi_bvalid);
`SLAVE_ASSERT(!i_axi_rvalid);
end
 
////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
//
//
// Stability assumptions, AXI inputs/responses
// Stability properties--what happens if valid and not ready
//
//
////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
 
// Assume any response from the bus will not change prior to that
// response being accepted
always @(posedge i_clk)
if (f_past_valid)
if ((f_past_valid)&&($past(i_axi_reset_n)))
begin
if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready)))
// Write address channel
if ((f_past_valid)&&($past(i_axi_awvalid))&&(!$past(i_axi_awready)))
begin
assume(i_axi_rid == $past(i_axi_rid));
assume(i_axi_rresp == $past(i_axi_rresp));
assume(i_axi_rdata == $past(i_axi_rdata));
assume(i_axi_rlast == $past(i_axi_rlast));
`SLAVE_ASSUME(i_axi_awvalid);
`SLAVE_ASSUME(i_axi_awaddr == $past(i_axi_awaddr));
`SLAVE_ASSUME($stable(i_axi_awid));
`SLAVE_ASSUME($stable(i_axi_awlen));
`SLAVE_ASSUME($stable(i_axi_awsize));
`SLAVE_ASSUME($stable(i_axi_awburst));
`SLAVE_ASSUME($stable(i_axi_awlock));
`SLAVE_ASSUME($stable(i_axi_awcache));
`SLAVE_ASSUME($stable(i_axi_awprot));
`SLAVE_ASSUME($stable(i_axi_awqos));
end
 
if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready)))
// Write data channel
if ((f_past_valid)&&($past(i_axi_wvalid))&&(!$past(i_axi_wready)))
begin
assume(i_axi_bid == $past(i_axi_bid));
assume(i_axi_bresp == $past(i_axi_bresp));
`SLAVE_ASSUME(i_axi_wvalid);
`SLAVE_ASSUME(i_axi_wstrb == $past(i_axi_wstrb));
`SLAVE_ASSUME(i_axi_wdata == $past(i_axi_wdata));
`SLAVE_ASSUME(i_axi_wlast);
end
end
 
// Nothing should be returning a result on the first clock
initial assume(!i_axi_bvalid);
initial assume(!i_axi_rvalid);
//
initial assert(!i_axi_arvalid);
initial assert(!i_axi_awvalid);
initial assert(!i_axi_wvalid);
// Incoming Read address channel
if ((f_past_valid)&&($past(i_axi_arvalid))&&(!$past(i_axi_arready)))
begin
`SLAVE_ASSUME(i_axi_arvalid);
`SLAVE_ASSUME(i_axi_arid == $past(i_axi_arid));
`SLAVE_ASSUME(i_axi_araddr == $past(i_axi_araddr));
`SLAVE_ASSUME(i_axi_arlen == $past(i_axi_arlen));
`SLAVE_ASSUME(i_axi_arsize == $past(i_axi_arsize));
`SLAVE_ASSUME(i_axi_arburst == $past(i_axi_arburst));
`SLAVE_ASSUME(i_axi_arlock == $past(i_axi_arlock));
`SLAVE_ASSUME(i_axi_arcache == $past(i_axi_arcache));
`SLAVE_ASSUME(i_axi_arprot == $past(i_axi_arprot));
`SLAVE_ASSUME(i_axi_arqos == $past(i_axi_arqos));
end
 
//////////////////////////////////////////////
//
//
// Stability assumptions, AXI outputs/requests
//
//
//////////////////////////////////////////////
// Assume any response from the bus will not change prior to that
// response being accepted
if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready)))
begin
`SLAVE_ASSERT(i_axi_rvalid);
`SLAVE_ASSERT(i_axi_rid == $past(i_axi_rid));
`SLAVE_ASSERT(i_axi_rresp == $past(i_axi_rresp));
`SLAVE_ASSERT(i_axi_rdata == $past(i_axi_rdata));
`SLAVE_ASSERT(i_axi_rlast == $past(i_axi_rlast));
end
 
// Read address chanel
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_axi_arvalid))&&(!$past(i_axi_arready)))
begin
assert(i_axi_arvalid);
assert($stable(i_axi_arid));
assert($stable(i_axi_araddr));
assert($stable(i_axi_arlen));
assert($stable(i_axi_arsize));
assert($stable(i_axi_arburst));
assert($stable(i_axi_arlock));
assert($stable(i_axi_arcache));
assert($stable(i_axi_arprot));
assert($stable(i_axi_arqos));
assert($stable(i_axi_arvalid));
if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready)))
begin
`SLAVE_ASSERT(i_axi_bvalid);
`SLAVE_ASSERT(i_axi_bid == $past(i_axi_bid));
`SLAVE_ASSERT(i_axi_bresp == $past(i_axi_bresp));
end
end
 
// If valid, but not ready, on any channel is true, nothing changes
// until valid && ready
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_axi_awvalid))&&(!$past(i_axi_awready)))
begin
assert($stable(i_axi_awid));
assert($stable(i_axi_awaddr));
assert($stable(i_axi_awlen));
assert($stable(i_axi_awsize));
assert($stable(i_axi_awburst));
assert($stable(i_axi_awlock));
assert($stable(i_axi_awcache));
assert($stable(i_axi_awprot));
assert($stable(i_axi_awqos));
assert($stable(i_axi_awvalid));
end
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_axi_wvalid))&&(!$past(i_axi_wready)))
begin
// AXI write data channel signals
assert($stable(i_axi_wdata));
assert($stable(i_axi_wstrb));
assert($stable(i_axi_wlast));
assert($stable(i_axi_wvalid));
end
 
// Nothing should be returned or requested on the first clock
initial `SLAVE_ASSUME(!i_axi_arvalid);
initial `SLAVE_ASSUME(!i_axi_awvalid);
initial `SLAVE_ASSUME(!i_axi_wvalid);
//
//
initial `SLAVE_ASSERT(!i_axi_bvalid);
initial `SLAVE_ASSERT(!i_axi_rvalid);
 
///////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
//
//
// Insist upon a maximum delay before a request is accepted
//
//
///////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
 
//
// AXI write address channel
//
//
reg [(C_AXI_ID_WIDTH):0] f_axi_awstall;
initial f_axi_awstall = 0;
always @(posedge i_clk)
generate if (F_AXI_MAXWAIT > 0)
begin : CHECK_STALL_COUNT
//
// AXI write address channel
//
//
reg [(F_LGDEPTH-1):0] f_axi_awstall,
f_axi_wstall,
f_axi_arstall,
f_axi_bstall,
f_axi_rstall;
 
initial f_axi_awstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_awvalid)||(i_axi_awready))
f_axi_awstall <= 0;
else
else if ((!i_axi_bvalid)||(i_axi_bready))
f_axi_awstall <= f_axi_awstall + 1'b1;
always @(*)
assume((F_AXI_MAXSTALL==0)||(f_axi_awstall < F_AXI_MAXSTALL));
 
//
// AXI write data channel
//
//
// AXI explicitly allows write bursts with zero strobes. This is part
// of how a transaction is aborted (if at all).
//always @(*) if (i_axi_wvalid) assert(|i_axi_wstrb);
always @(*)
`SLAVE_ASSERT(f_axi_awstall < F_AXI_MAXWAIT);
 
reg [(C_AXI_ID_WIDTH):0] f_axi_wstall;
initial f_axi_wstall = 0;
always @(posedge i_clk)
//
// AXI write data channel
//
//
initial f_axi_wstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_wvalid)||(i_axi_wready))
f_axi_wstall <= 0;
else
else if ((!i_axi_bvalid)||(i_axi_bready))
f_axi_wstall <= f_axi_wstall + 1'b1;
always @(*)
assume((F_AXI_MAXSTALL==0)||(f_axi_wstall < F_AXI_MAXSTALL));
 
always @(*)
`SLAVE_ASSERT(f_axi_wstall < F_AXI_MAXWAIT);
 
//
// AXI read address channel
//
//
reg [(C_AXI_ID_WIDTH):0] f_axi_arstall;
initial f_axi_arstall = 0;
always @(posedge i_clk)
//
// AXI read address channel
//
//
initial f_axi_arstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_arvalid)||(i_axi_arready))
f_axi_arstall <= 0;
else
else if ((!i_axi_rvalid)||(i_axi_rready))
f_axi_arstall <= f_axi_arstall + 1'b1;
always @(*)
assume((F_AXI_MAXSTALL==0)||(f_axi_arstall < F_AXI_MAXSTALL));
 
always @(*)
`SLAVE_ASSERT(f_axi_arstall < F_AXI_MAXWAIT);
 
// AXI write response channel
initial f_axi_bstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_bvalid)||(i_axi_bready))
f_axi_bstall <= 0;
else
f_axi_bstall <= f_axi_bstall + 1'b1;
 
always @(*)
`SLAVE_ASSUME(f_axi_bstall < F_AXI_MAXWAIT);
 
// AXI read response channel
initial f_axi_rstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_rvalid)||(i_axi_rready))
f_axi_rstall <= 0;
else
f_axi_rstall <= f_axi_rstall + 1'b1;
 
always @(*)
`SLAVE_ASSUME(f_axi_rstall < F_AXI_MAXWAIT);
 
end endgenerate
 
 
////////////////////////////////////////////////////////////////////////
//
//
// Count outstanding transactions
// Count outstanding transactions. With these measures, we count
// once per any burst.
//
//
////////////////////////////////////////////////////////////////////////
442,11 → 477,11
 
// Do not let the number of outstanding requests overflow
always @(posedge i_clk)
assert(f_axi_wr_outstanding < {(C_AXI_ID_WIDTH){1'b1}});
`SLAVE_ASSERT(f_axi_wr_outstanding < {(F_LGDEPTH){1'b1}});
always @(posedge i_clk)
assert(f_axi_awr_outstanding < {(C_AXI_ID_WIDTH){1'b1}});
`SLAVE_ASSERT(f_axi_awr_outstanding < {(F_LGDEPTH){1'b1}});
always @(posedge i_clk)
assert(f_axi_rd_outstanding < {(C_AXI_ID_WIDTH){1'b1}});
`SLAVE_ASSERT(f_axi_rd_outstanding < {(F_LGDEPTH){1'b1}});
 
////////////////////////////////////////////////////////////////////////
//
458,44 → 493,48
//
////////////////////////////////////////////////////////////////////////
 
reg [(C_AXI_ID_WIDTH):0] f_axi_wr_ack_delay,
f_axi_awr_ack_delay,
f_axi_rd_ack_delay;
generate if (F_AXI_MAXDELAY > 0)
begin : CHECK_MAX_DELAY
 
initial f_axi_rd_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(axi_rd_ack))
reg [(C_AXI_ID_WIDTH):0] f_axi_wr_ack_delay,
f_axi_awr_ack_delay,
f_axi_rd_ack_delay;
 
initial f_axi_rd_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(i_axi_rvalid)||(f_axi_rd_outstanding==0))
f_axi_rd_ack_delay <= 0;
else if (f_axi_rd_outstanding > 0)
else
f_axi_rd_ack_delay <= f_axi_rd_ack_delay + 1'b1;
 
initial f_axi_wr_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(axi_wr_ack))
initial f_axi_wr_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(i_axi_bvalid)||(f_axi_wr_outstanding==0))
f_axi_wr_ack_delay <= 0;
else if (f_axi_wr_outstanding > 0)
f_axi_wr_ack_delay <= f_axi_wr_ack_delay + 1'b1;
 
initial f_axi_awr_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(axi_wr_ack))
initial f_axi_awr_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(i_axi_bvalid)||(f_axi_awr_outstanding == 0))
f_axi_awr_ack_delay <= 0;
else if (f_axi_awr_outstanding > 0)
else
f_axi_awr_ack_delay <= f_axi_awr_ack_delay + 1'b1;
 
always @(posedge i_clk)
assume((F_AXI_MAXDELAY==0)||(f_axi_rd_ack_delay < F_AXI_MAXDELAY));
always @(*)
`SLAVE_ASSERT(f_axi_rd_ack_delay < F_AXI_MAXDELAY);
 
always @(posedge i_clk)
assume((F_AXI_MAXDELAY==0)||(f_axi_wr_ack_delay < F_AXI_MAXDELAY));
always @(*)
`SLAVE_ASSERT(f_axi_wr_ack_delay < F_AXI_MAXDELAY);
 
always @(posedge i_clk)
assume((F_AXI_MAXDELAY==0)||(f_axi_awr_ack_delay < F_AXI_MAXDELAY));
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_awr_ack_delay < F_AXI_MAXDELAY);
end endgenerate
 
////////////////////////////////////////////////////////////////////////
//
//
// Assume all acknowledgements must follow requests
// Assume acknowledgements must follow requests
//
// The outstanding count is a count of bursts, but the acknowledgements
// we are looking for are individual. Hence, there should be no
509,21 → 548,21
// AXI write response channel
//
always @(posedge i_clk)
if ((!axi_awr_req)&&(axi_wr_ack))
assume(f_axi_awr_outstanding > 0);
if ((!axi_awr_req)&&(i_axi_bvalid))
`SLAVE_ASSERT(f_axi_awr_outstanding > 0);
 
always @(posedge i_clk)
if ((!axi_wr_req)&&(axi_wr_ack))
assume(f_axi_wr_outstanding > 0);
if ((!axi_wr_req)&&(i_axi_bvalid))
`SLAVE_ASSERT(f_axi_wr_outstanding > 0);
 
//
// AXI read data channel signals
//
initial f_axi_rd_outstanding = 0;
always @(posedge i_clk)
if ((!axi_ard_req)&&(axi_rd_ack))
assume(f_axi_rd_outstanding > 0);
if ((!axi_ard_req)&&(i_axi_rvalid))
`SLAVE_ASSERT(f_axi_rd_outstanding > 0);
 
///////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
//
//
// Manage the ID buffer. Basic rules apply such as you can't
534,7 → 573,7
// transactions and not necessarily the individual values.
//
//
///////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
// Now, let's look into that FIFO. Without it, we know nothing about
// the ID's
 
648,13 → 687,13
end
 
always @(*)
assert((!F_CHECK_IDS)||(f_axi_awr_outstanding== f_axi_awr_id_outstanding_count));
`SLAVE_ASSUME((!F_CHECK_IDS)||(f_axi_awr_outstanding== f_axi_awr_id_outstanding_count));
 
always @(*)
assert((!F_CHECK_IDS)||(f_axi_wr_outstanding == f_axi_wr_id_outstanding_count));
`SLAVE_ASSUME((!F_CHECK_IDS)||(f_axi_wr_outstanding == f_axi_wr_id_outstanding_count));
 
always @(*)
assert((!F_CHECK_IDS)||(f_axi_rd_outstanding == f_axi_rd_id_outstanding_count));
`SLAVE_ASSUME((!F_CHECK_IDS)||(f_axi_rd_outstanding == f_axi_rd_id_outstanding_count));
 
always @(*)
assume( ((f_axi_wr_id_complete)&(~f_axi_awr_id_outstanding)) == 0);
685,6 → 724,7
f_wr_pending <= i_axi_awlen+9'h1;
assert(f_wr_pending == 0);
r_last_wr_id_valid <= 1'b1;
`SLAVE_ASSUME(i_axi_awlen <= F_AXI_MAXBURST);
end
 
if (axi_ard_req)
716,7 → 756,7
 
r_last_rd_id <= i_axi_rid;
if ((axi_rd_ack)&&(r_last_rd_id_valid))
assume(i_axi_rid == r_last_rd_id);
`SLAVE_ASSERT(i_axi_rid == r_last_rd_id);
end
 
if ((axi_rd_ack)&&(i_axi_rlast))
731,8 → 771,8
// Since we aren't allowing bursts, *every*
// write data and read data must always be the last
// value
assert((i_axi_wlast)||(!i_axi_wvalid));
assume((i_axi_rlast)||(!i_axi_rvalid));
`SLAVE_ASSUME((i_axi_wlast)||(!i_axi_wvalid));
`SLAVE_ASSERT((i_axi_rlast)||(!i_axi_rvalid));
 
assert((!i_axi_arvalid)||(i_axi_arlen==0));
assert((!i_axi_awvalid)||(i_axi_awlen==0));
/faxi_slave.v
4,7 → 4,9
//
// Project: Pipelined Wishbone to AXI converter
//
// Purpose:
// Purpose: This file contains a set of formal properties which can be
// used to formally verify that a core truly follows the full
// AXI4 specification.
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
11,27 → 13,30
//
////////////////////////////////////////////////////////////////////////////////
//
// 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
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
// This file is part of the pipelined Wishbone to AXI converter project, a
// project that contains multiple bus bridging designs and formal bus property
// sets.
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
// for more details.
// The bus bridge designs and property sets are free RTL designs: you can
// redistribute them and/or modify any of them under the terms of the GNU
// Lesser General Public License as published by the Free Software Foundation,
// either version 3 of the License, or (at your option) any later version.
//
// You should have received a copy of the GNU General Public License along
// with this program. (It's in the $(ROOT)/doc directory, run make with no
// target there if the PDF file isn't present.) If not, see
// The bus bridge designs and property sets are distributed in the hope that
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with these designs. (It's in the $(ROOT)/doc directory. Run make
// with no target there if the PDF file isn't present.) If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License: GPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/gpl.html
// License: LGPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/lgpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
44,19 → 49,19
parameter C_AXI_ADDR_WIDTH = 28, // AXI Address width (log wordsize)
localparam DW = C_AXI_DATA_WIDTH,
localparam AW = C_AXI_ADDR_WIDTH,
parameter [0:0] F_OPT_BURSTS = 1'b1, // Check burst lengths
parameter [7:0] F_AXI_MAXBURST = 8'hff,// Maximum burst length, minus 1
parameter F_LGDEPTH = 10,
parameter F_LGFIFO = 3,
parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXSTALL = 3,
parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXDELAY = 3,
parameter [0:0] F_STRICT_ORDER = 0, // Reorder, or not? 0 -> Reorder
parameter [0:0] F_CONSECUTIVE_IDS= 0, // 0=ID's must be consecutive
parameter [0:0] F_OPT_BURSTS = 1'b1, // Check burst lengths
parameter [0:0] F_CHECK_IDS = 1'b1 // Check ID's upon issue&return
parameter [(C_AXI_ID_WIDTH-1):0] F_AXI_MAXDELAY = 3
) (
input i_clk, // System clock
input i_axi_reset_n,
input wire i_clk, // System clock
input wire i_axi_reset_n,
 
// AXI write address channel signals
input i_axi_awready, // Slave is ready to accept
input wire [C_AXI_ID_WIDTH-1:0] i_axi_awid, // Write ID
input wire i_axi_awready,//Slave is ready to accept
// input wire [C_AXI_ID_WIDTH-1:0] i_axi_awid, // Write ID
input wire [AW-1:0] i_axi_awaddr, // Write address
input wire [7:0] i_axi_awlen, // Write Burst Length
input wire [2:0] i_axi_awsize, // Write Burst size
75,14 → 80,14
input wire i_axi_wvalid, // Write valid
 
// AXI write response channel signals
input wire [C_AXI_ID_WIDTH-1:0] i_axi_bid, // Response ID
input wire [1:0] i_axi_bresp, // Write response
// input wire [C_AXI_ID_WIDTH-1:0] i_axi_bid, // Response ID
input wire [1:0] i_axi_bresp, // Write response
input wire i_axi_bvalid, // Write reponse valid
input wire i_axi_bready, // Response ready
 
// AXI read address channel signals
input wire i_axi_arready, // Read address ready
input wire [C_AXI_ID_WIDTH-1:0] i_axi_arid, // Read ID
// input wire [C_AXI_ID_WIDTH-1:0] i_axi_arid, // Read ID
input wire [AW-1:0] i_axi_araddr, // Read address
input wire [7:0] i_axi_arlen, // Read Burst Length
input wire [2:0] i_axi_arsize, // Read Burst size
94,22 → 99,27
input wire i_axi_arvalid, // Read address valid
 
// AXI read data channel signals
input wire [C_AXI_ID_WIDTH-1:0] i_axi_rid, // Response ID
input wire [1:0] i_axi_rresp, // Read response
// input wire [C_AXI_ID_WIDTH-1:0] i_axi_rid, // Response ID
input wire [1:0] i_axi_rresp, // Read response
input wire i_axi_rvalid, // Read reponse valid
input wire [DW-1:0] i_axi_rdata, // Read data
input wire [DW-1:0] i_axi_rdata, // Read data
input wire i_axi_rlast, // Read last
input wire i_axi_rready, // Read Response ready
//
output reg [(C_AXI_ID_WIDTH-1):0] f_axi_rd_outstanding,
output reg [(C_AXI_ID_WIDTH-1):0] f_axi_wr_outstanding,
output reg [(C_AXI_ID_WIDTH-1):0] f_axi_awr_outstanding,
output reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_rd_id_outstanding,
output reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_awr_id_outstanding,
output reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_wr_id_outstanding
 
output reg [F_LGDEPTH-1:0] f_axi_rd_nbursts,
output reg [F_LGDEPTH-1:0] f_axi_rd_outstanding,
output reg [F_LGDEPTH-1:0] f_axi_wr_nbursts,
output reg [F_LGDEPTH-1:0] f_axi_awr_outstanding,
output reg [F_LGDEPTH-1:0] f_axi_awr_nbursts,
// Address writes without write valids
//
// output reg [(9-1):0] f_axi_wr_pending,
//
// RD_COUNT: increment on read w/o last, cleared on read w/ last
output reg [(9-1):0] f_axi_rd_count,
output reg [(72-1):0] f_axi_rdfifo
);
reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_wr_id_complete;
reg [(9-1):0] f_axi_wr_count;
 
//*****************************************************************************
// Parameter declarations
130,6 → 140,7
: 8))));
localparam LGFIFOLN = C_AXI_ID_WIDTH;
localparam FIFOLN = (1<<LGFIFOLN);
localparam F_AXI_MAXWAIT = F_AXI_MAXSTALL;
 
 
//*****************************************************************************
136,22 → 147,6
// Internal register and wire declarations
//*****************************************************************************
 
// Things we're not changing ...
always @(*)
begin
assume(i_axi_awlen == 8'h0); // Burst length is one
assume(i_axi_awsize == 3'b101); // maximum bytes per burst is 32
assume(i_axi_awburst == 2'b01); // Incrementing address (ignored)
assume(i_axi_arburst == 2'b01); // Incrementing address (ignored)
assume(i_axi_awlock == 1'b0); // Normal signaling
assume(i_axi_arlock == 1'b0); // Normal signaling
assume(i_axi_awcache == 4'h2); // Normal: no cache, no buffer
assume(i_axi_arcache == 4'h2); // Normal: no cache, no buffer
assume(i_axi_awprot == 3'b010);// Unpriviledged, unsecure, data access
assume(i_axi_arprot == 3'b010);// Unpriviledged, unsecure, data access
assume(i_axi_awqos == 4'h0); // Lowest quality of service (unused)
assume(i_axi_arqos == 4'h0); // Lowest quality of service (unused)
end
 
// wire w_fifo_full;
wire axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req,
166,6 → 161,9
assign axi_rd_err = (axi_rd_ack)&&(i_axi_rresp[1]);
assign axi_wr_err = (axi_wr_ack)&&(i_axi_bresp[1]);
 
`define SLAVE_ASSUME assume
`define SLAVE_ASSERT assert
 
//
// Setup
//
176,235 → 174,240
always @(posedge i_clk)
f_past_valid <= 1'b1;
always @(*)
if (!f_past_valid)
assume(!i_axi_reset_n);
if (!f_past_valid)
assume(!i_axi_reset_n);
// WAS AN ASSERT
 
////////////////////////////////////////////////////////////////////////
//
// All signals must be synchronous with the clock
//
always @($global_clock)
if (f_past_valid) begin
// Assume our inputs will only change on the positive edge
// of the clock
if (!$rose(i_clk))
begin
// AXI inputs
assert($stable(i_axi_awready));
assert($stable(i_axi_wready));
//
assert($stable(i_axi_bid));
assert($stable(i_axi_bresp));
assert($stable(i_axi_bvalid));
assert($stable(i_axi_arready));
//
assert($stable(i_axi_rid));
assert($stable(i_axi_rresp));
assert($stable(i_axi_rvalid));
assert($stable(i_axi_rdata));
assert($stable(i_axi_rlast));
//
// AXI outputs
//
assume($stable(i_axi_awvalid));
assume($stable(i_axi_awid));
assume($stable(i_axi_awlen));
assume($stable(i_axi_awsize));
assume($stable(i_axi_awlock));
assume($stable(i_axi_awcache));
assume($stable(i_axi_awprot));
assume($stable(i_axi_awqos));
//
assume($stable(i_axi_wvalid));
assume($stable(i_axi_wdata));
assume($stable(i_axi_wstrb));
assume($stable(i_axi_wlast));
//
assume($stable(i_axi_arvalid));
assume($stable(i_axi_arid));
assume($stable(i_axi_arlen));
assume($stable(i_axi_arsize));
assume($stable(i_axi_arburst));
assume($stable(i_axi_arlock));
assume($stable(i_axi_arprot));
assume($stable(i_axi_arqos));
//
assume($stable(i_axi_bready));
//
assume($stable(i_axi_rready));
//
// Formal outputs
//
assume($stable(f_axi_rd_outstanding));
assume($stable(f_axi_wr_outstanding));
assume($stable(f_axi_awr_outstanding));
end
end
 
////////////////////////////////////////////////////
// Reset properties
//
//
// Reset properties
////////////////////////////////////////////////////////////////////////
localparam [0:0] F_OPT_ASSUME_RESET = 1'b1;
generate if (F_OPT_ASSUME_RESET)
begin : ASSUME_INITIAL_RESET
always @(*)
if (!f_past_valid)
assume(!i_axi_reset_n);
end else begin : ASSERT_INITIAL_RESET
always @(*)
if (!f_past_valid)
assert(!i_axi_reset_n);
end endgenerate
//
//
////////////////////////////////////////////////////
// If asserted, the reset must be asserted for a minimum of 16 clocks
reg [3:0] f_reset_length;
initial f_reset_length = 0;
always @(posedge i_clk)
if (i_axi_reset_n)
f_reset_length <= 0;
else if (!(&f_reset_length))
f_reset_length <= f_reset_length + 1'b1;
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_axi_reset_n)))
if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
`SLAVE_ASSUME(!i_axi_reset_n);
 
generate if (F_OPT_ASSUME_RESET)
begin : ASSUME_RESET
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
assume(!i_axi_reset_n);
 
always @(*)
if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
assume(!i_axi_reset_n);
 
end else begin : ASSERT_RESET
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
assert(!i_axi_reset_n);
 
always @(*)
if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
assert(!i_axi_reset_n);
 
end endgenerate
 
always @(posedge i_clk)
if ((!f_past_valid)||(!$past(i_axi_reset_n)))
begin
assume(!i_axi_arvalid);
assume(!i_axi_awvalid);
assume(!i_axi_wvalid);
assert(!i_axi_bvalid);
assert(!i_axi_rvalid);
`SLAVE_ASSUME(!i_axi_arvalid);
`SLAVE_ASSUME(!i_axi_awvalid);
`SLAVE_ASSUME(!i_axi_wvalid);
//
`SLAVE_ASSERT(!i_axi_bvalid);
`SLAVE_ASSERT(!i_axi_rvalid);
end
 
////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
//
//
// Stability assumptions, AXI inputs/responses
// Stability properties--what happens if valid and not ready
//
//
////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
 
// Assume any response from the bus will not change prior to that
// response being accepted
always @(posedge i_clk)
if (f_past_valid)
if ((f_past_valid)&&($past(i_axi_reset_n)))
begin
if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready)))
// Write address channel
if ((f_past_valid)&&($past(i_axi_awvalid))&&(!$past(i_axi_awready)))
begin
assert(i_axi_rid == $past(i_axi_rid));
assert(i_axi_rresp == $past(i_axi_rresp));
assert(i_axi_rdata == $past(i_axi_rdata));
assert(i_axi_rlast == $past(i_axi_rlast));
`SLAVE_ASSUME(i_axi_awvalid);
`SLAVE_ASSUME(i_axi_awaddr == $past(i_axi_awaddr));
// `SLAVE_ASSUME($stable(i_axi_awid));
`SLAVE_ASSUME($stable(i_axi_awlen));
`SLAVE_ASSUME($stable(i_axi_awsize));
`SLAVE_ASSUME($stable(i_axi_awburst));
`SLAVE_ASSUME($stable(i_axi_awlock));
`SLAVE_ASSUME($stable(i_axi_awcache));
`SLAVE_ASSUME($stable(i_axi_awprot));
`SLAVE_ASSUME($stable(i_axi_awqos));
end
 
if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready)))
// Write data channel
if ((f_past_valid)&&($past(i_axi_wvalid))&&(!$past(i_axi_wready)))
begin
assert(i_axi_bid == $past(i_axi_bid));
assert(i_axi_bresp == $past(i_axi_bresp));
`SLAVE_ASSUME(i_axi_wvalid);
`SLAVE_ASSUME($stable(i_axi_wstrb));
`SLAVE_ASSUME($stable(i_axi_wdata));
`SLAVE_ASSUME($stable(i_axi_wlast));
end
end
 
// Nothing should be returning a result on the first clock
initial assert(!i_axi_bvalid);
initial assert(!i_axi_rvalid);
//
initial assume(!i_axi_arvalid);
initial assume(!i_axi_awvalid);
initial assume(!i_axi_wvalid);
// Incoming Read address channel
if ((f_past_valid)&&($past(i_axi_arvalid))&&(!$past(i_axi_arready)))
begin
`SLAVE_ASSUME(i_axi_arvalid);
// `SLAVE_ASSUME($stable(i_axi_arid));
`SLAVE_ASSUME($stable(i_axi_araddr));
`SLAVE_ASSUME($stable(i_axi_arlen));
`SLAVE_ASSUME($stable(i_axi_arsize));
`SLAVE_ASSUME($stable(i_axi_arburst));
`SLAVE_ASSUME($stable(i_axi_arlock));
`SLAVE_ASSUME($stable(i_axi_arcache));
`SLAVE_ASSUME($stable(i_axi_arprot));
`SLAVE_ASSUME($stable(i_axi_arqos));
end
 
//////////////////////////////////////////////
//
//
// Stability assumptions, AXI outputs/requests
//
//
//////////////////////////////////////////////
// Assume any response from the bus will not change prior to that
// response being accepted
if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready)))
begin
`SLAVE_ASSERT(i_axi_rvalid);
// `SLAVE_ASSERT($stable(i_axi_rid));
`SLAVE_ASSERT($stable(i_axi_rresp));
`SLAVE_ASSERT($stable(i_axi_rdata));
`SLAVE_ASSERT($stable(i_axi_rlast));
end
 
// Read address chanel
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_axi_arvalid))&&(!$past(i_axi_arready)))
begin
assume(i_axi_arvalid);
assume($stable(i_axi_arid));
assume($stable(i_axi_araddr));
assume($stable(i_axi_arlen));
assume($stable(i_axi_arsize));
assume($stable(i_axi_arburst));
assume($stable(i_axi_arlock));
assume($stable(i_axi_arcache));
assume($stable(i_axi_arprot));
assume($stable(i_axi_arqos));
assume($stable(i_axi_arvalid));
if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready)))
begin
`SLAVE_ASSERT(i_axi_bvalid);
/// `SLAVE_ASSERT($stable(i_axi_bid));
`SLAVE_ASSERT($stable(i_axi_bresp));
end
end
 
// If valid, but not ready, on any channel is true, nothing changes
// until valid && ready
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_axi_awvalid))&&(!$past(i_axi_awready)))
begin
assume($stable(i_axi_awid));
assume($stable(i_axi_awaddr));
assume($stable(i_axi_awlen));
assume($stable(i_axi_awsize));
assume($stable(i_axi_awburst));
assume($stable(i_axi_awlock));
assume($stable(i_axi_awcache));
assume($stable(i_axi_awprot));
assume($stable(i_axi_awqos));
assume($stable(i_axi_awvalid));
end
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_axi_wvalid))&&(!$past(i_axi_wready)))
begin
// AXI write data channel signals
assume($stable(i_axi_wdata));
assume($stable(i_axi_wstrb));
assume($stable(i_axi_wlast));
assume($stable(i_axi_wvalid));
end
 
// Nothing should be returned or requested on the first clock
initial `SLAVE_ASSUME(!i_axi_arvalid);
initial `SLAVE_ASSUME(!i_axi_awvalid);
initial `SLAVE_ASSUME(!i_axi_wvalid);
//
//
initial `SLAVE_ASSERT(!i_axi_bvalid);
initial `SLAVE_ASSERT(!i_axi_rvalid);
 
///////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
//
//
// Insist upon a maximum delay before a request is accepted
//
//
///////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
 
//
// AXI write address channel
//
//
reg [(C_AXI_ID_WIDTH):0] f_axi_awstall;
initial f_axi_awstall = 0;
always @(posedge i_clk)
generate if (F_AXI_MAXWAIT > 0)
begin : CHECK_STALL_COUNT
//
// AXI write address channel
//
//
reg [(F_LGDEPTH-1):0] f_axi_awstall,
f_axi_wstall,
f_axi_arstall,
f_axi_bstall,
f_axi_rstall;
 
initial f_axi_awstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_awvalid)||(i_axi_awready))
f_axi_awstall <= 0;
else
else if ((!i_axi_bvalid)||(i_axi_bready))
f_axi_awstall <= f_axi_awstall + 1'b1;
always @(*)
assert((F_AXI_MAXSTALL==0)||(f_axi_awstall < F_AXI_MAXSTALL));
 
//
// AXI write data channel
//
//
// AXI explicitly allows write bursts with zero strobes. This is part
// of how a transaction is aborted (if at all).
//always @(*) if (i_axi_wvalid) assume(|i_axi_wstrb);
always @(*)
`SLAVE_ASSERT(f_axi_awstall < F_AXI_MAXWAIT);
 
reg [(C_AXI_ID_WIDTH):0] f_axi_wstall;
initial f_axi_wstall = 0;
always @(posedge i_clk)
//
// AXI write data channel
//
//
// AXI explicitly allows write bursts with zero strobes. This is part
// of how a transaction is aborted (if at all).
 
initial f_axi_wstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_wvalid)||(i_axi_wready))
f_axi_wstall <= 0;
else
else if ((!i_axi_bvalid)||(i_axi_bready))
f_axi_wstall <= f_axi_wstall + 1'b1;
always @(*)
assert((F_AXI_MAXSTALL==0)||(f_axi_wstall < F_AXI_MAXSTALL));
 
always @(*)
`SLAVE_ASSERT(f_axi_wstall < F_AXI_MAXWAIT);
 
//
// AXI read address channel
//
//
reg [(C_AXI_ID_WIDTH):0] f_axi_arstall;
initial f_axi_arstall = 0;
always @(posedge i_clk)
//
// AXI read address channel
//
//
initial f_axi_arstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_arvalid)||(i_axi_arready))
f_axi_arstall <= 0;
else
else if ((!i_axi_rvalid)||(i_axi_rready))
f_axi_arstall <= f_axi_arstall + 1'b1;
always @(*)
assert((F_AXI_MAXSTALL==0)||(f_axi_arstall < F_AXI_MAXSTALL));
 
always @(*)
`SLAVE_ASSERT(f_axi_arstall < F_AXI_MAXWAIT);
 
// AXI write response channel
initial f_axi_bstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_bvalid)||(i_axi_bready))
f_axi_bstall <= 0;
else
f_axi_bstall <= f_axi_bstall + 1'b1;
 
always @(*)
`SLAVE_ASSUME(f_axi_bstall < F_AXI_MAXWAIT);
 
// AXI read response channel
initial f_axi_rstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_rvalid)||(i_axi_rready))
f_axi_rstall <= 0;
else
f_axi_rstall <= f_axi_rstall + 1'b1;
 
always @(*)
`SLAVE_ASSUME(f_axi_rstall < F_AXI_MAXWAIT);
 
end endgenerate
 
 
////////////////////////////////////////////////////////////////////////
//
//
415,40 → 418,82
////////////////////////////////////////////////////////////////////////
initial f_axi_awr_outstanding = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_awr_outstanding <= 0;
else case({ (axi_awr_req), (axi_wr_ack) })
2'b10: f_axi_awr_outstanding <= f_axi_awr_outstanding + 1'b1;
2'b01: f_axi_awr_outstanding <= f_axi_awr_outstanding - 1'b1;
default: begin end
endcase
if (!i_axi_reset_n)
f_axi_awr_outstanding <= 0;
else case({ (axi_awr_req), (axi_wr_req) })
2'b10: f_axi_awr_outstanding <= f_axi_awr_outstanding + i_axi_awlen-1;
2'b01: f_axi_awr_outstanding <= f_axi_awr_outstanding - 1'b1;
2'b11: f_axi_awr_outstanding <= f_axi_awr_outstanding + i_axi_awlen; // +1 -1
default: begin end
endcase
 
initial f_axi_wr_outstanding = 0;
initial f_axi_awr_nbursts = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_wr_outstanding <= 0;
else case({ (axi_wr_req)&&(i_axi_wlast), (axi_wr_ack) })
2'b01: f_axi_wr_outstanding <= f_axi_wr_outstanding - 1'b1;
2'b10: f_axi_wr_outstanding <= f_axi_wr_outstanding + 1'b1;
endcase
if (!i_axi_reset_n)
f_axi_awr_nbursts <= 0;
else case({ (axi_awr_req), (axi_wr_ack) })
2'b10: f_axi_awr_nbursts <= f_axi_awr_nbursts + 1'b1;
2'b01: f_axi_awr_nbursts <= f_axi_awr_nbursts - 1'b1;
default: begin end
endcase
 
initial f_axi_wr_nbursts = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_wr_nbursts <= 0;
else case({ (axi_wr_req)&&(i_axi_wlast), (axi_wr_ack) })
2'b01: f_axi_wr_nbursts <= f_axi_wr_nbursts - 1'b1;
2'b10: f_axi_wr_nbursts <= f_axi_wr_nbursts + 1'b1;
default: begin end
endcase
 
initial f_axi_rd_nbursts = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_rd_nbursts <= 0;
else case({ (axi_ard_req), (axi_rd_ack)&&(i_axi_rlast) })
2'b01: f_axi_rd_nbursts <= f_axi_rd_nbursts - 1'b1;
2'b10: f_axi_rd_nbursts <= f_axi_rd_nbursts + 1'b1;
endcase
 
initial f_axi_rd_outstanding = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_rd_outstanding <= 0;
else case({ (axi_ard_req), (axi_rd_ack)&&(i_axi_rlast) })
2'b01: f_axi_rd_outstanding <= f_axi_rd_outstanding - 1'b1;
2'b10: f_axi_rd_outstanding <= f_axi_rd_outstanding + 1'b1;
endcase
if (!i_axi_reset_n)
f_axi_rd_outstanding <= 0;
else case({ (axi_ard_req), (axi_rd_ack) })
2'b01: f_axi_rd_outstanding <= f_axi_rd_outstanding - 1'b1;
2'b10: f_axi_rd_outstanding <= f_axi_rd_outstanding + i_axi_arlen+1;
2'b11: f_axi_rd_outstanding <= f_axi_rd_outstanding + i_axi_arlen;
endcase
 
// Do not let the number of outstanding requests overflow
always @(posedge i_clk)
assume(f_axi_wr_outstanding < {(C_AXI_ID_WIDTH){1'b1}});
`SLAVE_ASSERT(f_axi_awr_outstanding < {(F_LGDEPTH){1'b1}});
always @(posedge i_clk)
assume(f_axi_awr_outstanding < {(C_AXI_ID_WIDTH){1'b1}});
`SLAVE_ASSERT(f_axi_rd_outstanding < {(F_LGDEPTH){1'b1}});
always @(posedge i_clk)
assume(f_axi_rd_outstanding < {(C_AXI_ID_WIDTH){1'b1}});
`SLAVE_ASSERT(f_axi_awr_nbursts < {(F_LGDEPTH){1'b1}});
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_wr_nbursts < {(F_LGDEPTH){1'b1}});
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_rd_nbursts < {(F_LGDEPTH){1'b1}});
 
// Cannot have outstanding values if there aren't any outstanding
// bursts
always @(posedge i_clk)
if (f_axi_awr_outstanding > 0)
`SLAVE_ASSERT(f_axi_awr_nbursts > 0);
// else if (f_axi_awr_outstanding == 0)
// Doesn't apply. Might have awr_outstanding == 0 and
// awr_nbursts>0
always @(posedge i_clk)
if (f_axi_rd_outstanding > 0)
`SLAVE_ASSERT(f_axi_rd_nbursts > 0);
else
`SLAVE_ASSERT(f_axi_rd_nbursts == 0);
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_rd_nbursts <= f_axi_rd_outstanding);
 
////////////////////////////////////////////////////////////////////////
//
//
459,44 → 504,51
//
////////////////////////////////////////////////////////////////////////
 
reg [(C_AXI_ID_WIDTH):0] f_axi_wr_ack_delay,
f_axi_awr_ack_delay,
f_axi_rd_ack_delay;
generate if (F_AXI_MAXDELAY > 0)
begin : CHECK_MAX_DELAY
 
initial f_axi_rd_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(axi_rd_ack))
reg [(C_AXI_ID_WIDTH):0] f_axi_wr_ack_delay,
f_axi_awr_ack_delay,
f_axi_rd_ack_delay;
 
initial f_axi_rd_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(i_axi_rvalid)||(f_axi_rd_outstanding==0))
f_axi_rd_ack_delay <= 0;
else if (f_axi_rd_outstanding > 0)
else
f_axi_rd_ack_delay <= f_axi_rd_ack_delay + 1'b1;
 
initial f_axi_wr_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(axi_wr_ack))
initial f_axi_wr_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||((i_axi_wvalid)&&(!i_axi_wlast))
||(i_axi_bvalid)||(f_axi_awr_outstanding==0))
f_axi_wr_ack_delay <= 0;
else if (f_axi_wr_outstanding > 0)
else
f_axi_wr_ack_delay <= f_axi_wr_ack_delay + 1'b1;
 
initial f_axi_awr_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(axi_wr_ack))
initial f_axi_awr_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(i_axi_bvalid)||(i_axi_wvalid)
||(f_axi_awr_nbursts == 0)
||(f_axi_wr_nbursts == 0))
f_axi_awr_ack_delay <= 0;
else if (f_axi_awr_outstanding > 0)
else
f_axi_awr_ack_delay <= f_axi_awr_ack_delay + 1'b1;
 
always @(posedge i_clk)
assert((F_AXI_MAXDELAY==0)||(f_axi_rd_ack_delay < F_AXI_MAXDELAY));
always @(*)
`SLAVE_ASSERT(f_axi_rd_ack_delay < F_AXI_MAXDELAY);
 
always @(posedge i_clk)
assert((F_AXI_MAXDELAY==0)||(f_axi_wr_ack_delay < F_AXI_MAXDELAY));
always @(*)
`SLAVE_ASSERT(f_axi_wr_ack_delay < F_AXI_MAXDELAY);
 
always @(posedge i_clk)
assert((F_AXI_MAXDELAY==0)||(f_axi_awr_ack_delay < F_AXI_MAXDELAY));
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_awr_ack_delay < F_AXI_MAXDELAY);
end endgenerate
 
////////////////////////////////////////////////////////////////////////
//
//
// Assume all acknowledgements must follow requests
// Assume acknowledgements must follow requests
//
// The outstanding count is a count of bursts, but the acknowledgements
// we are looking for are individual. Hence, there should be no
510,248 → 562,202
// AXI write response channel
//
always @(posedge i_clk)
if ((!axi_awr_req)&&(axi_wr_ack))
assert(f_axi_awr_outstanding > 0);
always @(posedge i_clk)
if ((!axi_wr_req)&&(axi_wr_ack))
assert(f_axi_wr_outstanding > 0);
if (i_axi_bvalid)
begin
`SLAVE_ASSERT(f_axi_awr_nbursts > 0);
`SLAVE_ASSERT(f_axi_wr_nbursts > 0);
end
 
//
// AXI read data channel signals
//
initial f_axi_rd_outstanding = 0;
always @(posedge i_clk)
if ((!axi_ard_req)&&(axi_rd_ack))
assert(f_axi_rd_outstanding > 0);
if (i_axi_rvalid)
begin
`SLAVE_ASSERT(f_axi_rd_outstanding > 0);
`SLAVE_ASSERT(f_axi_rd_nbursts > 0);
if (!i_axi_rlast)
`SLAVE_ASSERT(f_axi_rd_outstanding > 1);
end
 
///////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
//
//
// Manage the ID buffer. Basic rules apply such as you can't
// make a request of an already requested ID # before that ID
// is returned, etc.
//
// Elements in this buffer reference transactions--possibly burst
// transactions and not necessarily the individual values.
//
//
///////////////////////////////////////////////////////////////////
// Now, let's look into that FIFO. Without it, we know nothing about
// the ID's
////////////////////////////////////////////////////////////////////////
 
initial f_axi_rd_id_outstanding = 0;
initial f_axi_wr_id_outstanding = 0;
initial f_axi_awr_id_outstanding = 0;
initial f_axi_wr_id_complete = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
begin
f_axi_rd_id_outstanding <= 0;
f_axi_wr_id_outstanding <= 0;
f_axi_wr_id_complete <= 0;
f_axi_awr_id_outstanding <= 0;
end else begin
// When issuing a write
if (axi_awr_req)
begin
if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS))
assume(f_axi_awr_id_outstanding[i_axi_awid+1'b1] == 1'b0);
assume((!F_CHECK_IDS)
||(f_axi_awr_id_outstanding[i_axi_awid] == 1'b0));
assume((!F_CHECK_IDS)
||(f_axi_wr_id_complete[i_axi_awid] == 1'b0));
f_axi_awr_id_outstanding[i_axi_awid] <= 1'b1;
f_axi_wr_id_complete[i_axi_awid] <= 1'b0;
end
generate if (!F_OPT_BURSTS)
begin
 
if (axi_wr_req)
begin
if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS))
assume(f_axi_wr_id_outstanding[i_axi_awid+1'b1] == 1'b0);
assume((!F_CHECK_IDS)
||(f_axi_wr_id_outstanding[i_axi_awid] == 1'b0));
f_axi_wr_id_outstanding[i_axi_awid] <= 1'b1;
if (i_axi_wlast)
begin
assert(f_axi_wr_id_complete[i_axi_awid] == 1'b0);
f_axi_wr_id_complete[i_axi_awid] <= 1'b1;
end
end
always @(posedge i_clk)
if (i_axi_awvalid)
`SLAVE_ASSUME(i_axi_awlen == 0);
 
// When issuing a read
if (axi_ard_req)
begin
if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS))
assume(f_axi_rd_id_outstanding[i_axi_arid+1'b1] == 1'b0);
assume((!F_CHECK_IDS)
||(f_axi_rd_id_outstanding[i_axi_arid] == 1'b0));
f_axi_rd_id_outstanding[i_axi_arid] <= 1'b1;
end
always @(posedge i_clk)
if (i_axi_wvalid)
`SLAVE_ASSUME(i_axi_wlast);
 
// When a write is acknowledged
if (axi_wr_ack)
begin
if (F_CHECK_IDS)
begin
assert(f_axi_awr_id_outstanding[i_axi_bid]);
assert(f_axi_wr_id_outstanding[i_axi_bid]);
assert((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS)
||(!f_axi_wr_id_outstanding[i_axi_bid-1'b1]));
assert((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS)
||(!f_axi_awr_id_outstanding[i_axi_bid-1'b1]));
assert(f_axi_wr_id_complete[i_axi_bid]);
end
f_axi_awr_id_outstanding[i_axi_bid] <= 1'b0;
f_axi_wr_id_outstanding[i_axi_bid] <= 1'b0;
f_axi_wr_id_complete[i_axi_bid] <= 1'b0;
end
always @(posedge i_clk)
if (i_axi_arvalid)
`SLAVE_ASSUME(i_axi_arlen == 0);
 
// When a read is acknowledged
if (axi_rd_ack)
begin
if (F_CHECK_IDS)
begin
assert(f_axi_rd_id_outstanding[i_axi_rid]);
assert((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS)
||(!f_axi_rd_id_outstanding[i_axi_rid-1'b1]));
always @(*)
`SLAVE_ASSERT(f_axi_rd_nbursts == f_axi_rd_outstanding);
end endgenerate
 
reg [7:0] wrfifo [0:((1<<F_LGDEPTH)-1)];
reg [7:0] rdfifo [0:((1<<F_LGDEPTH)-1)];
reg [F_LGDEPTH-1:0] rd_rdaddr, wr_rdaddr, rd_wraddr, wr_wraddr;
reg [7:0] rdfifo_data, wrfifo_data;
reg [F_LGDEPTH-1:0] rdfifo_outstanding;
wire [7:0] this_wlen;
wire [F_LGDEPTH-1:0] wrfifo_fill, rdfifo_fill;
 
/*
always @(posedge i_clk)
if (!i_axi_reset_n)
begin
f_axi_wburst_fifo <= 0;
end else case({ axi_awr_req , axi_wr_req, i_axi_wrlast })
3'b010:
f_axi_wburst_fifo[7:0] <= f_axi_wburst_fifo[7:0]-1;
3'b011: begin
`SLAVE_ASSUME(f_axi_wburst_fifo[7:0] == 0);
f_axi_wburst_fifo <= { 8'h0, f_axi_wburst_fifo[63:8] };
end
3'b100:
`SLAVE_ASSUME(f_axi_awr_nbursts < 8);
f_axi_wburst_fifo <= f_axi_wburst_fifo
| ((i_axi_awlen)<<(f_axi_awr_nbursts * 8));
3'b11:
f_axi_wburst_fifo <= { 8'h0, f_axi_wburst_fifo[63:8] }
| ((i_axi_awlen)<<((f_axi_awr_nbursts-1) * 8));
default:
endcase
*/
 
if (i_axi_rlast)
f_axi_rd_id_outstanding[i_axi_rid] <= 1'b0;
end
//
// Count the number of write elements received since the last wlast
initial f_axi_wr_count = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_wr_count <= 0;
else if (axi_wr_req)
begin
if (i_axi_wlast)
f_axi_wr_count <= 1'b0;
else
f_axi_wr_count <= f_axi_wr_count + 1'b1;
end
 
//
// Write information to the write FIFO
initial wr_wraddr = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
wr_wraddr <= 0;
else if (axi_awr_req)
wr_wraddr <= wr_wraddr + 1'b1;
 
reg [LGFIFOLN:0] f_axi_rd_id_outstanding_count,
f_axi_awr_id_outstanding_count,
f_axi_wr_id_outstanding_count;
always @(posedge i_clk)
if (axi_awr_req)
wrfifo[wr_wraddr] <= { i_axi_awlen };
 
initial f_axi_rd_id_outstanding_count = 0;
initial f_axi_awr_id_outstanding_count = 0;
initial f_axi_wr_id_outstanding_count = 0;
//
// Read information from the write queue
always @(*)
begin
//
f_axi_rd_id_outstanding_count = 0;
for(k=0; k< FIFOLN; k=k+1)
if (f_axi_rd_id_outstanding[k])
f_axi_rd_id_outstanding_count
= f_axi_rd_id_outstanding_count +1;
//
f_axi_wr_id_outstanding_count = 0;
for(k=0; k< FIFOLN; k=k+1)
if (f_axi_wr_id_outstanding[k])
f_axi_wr_id_outstanding_count = f_axi_wr_id_outstanding_count +1;
f_axi_awr_id_outstanding_count = 0;
for(k=0; k< FIFOLN; k=k+1)
if (f_axi_awr_id_outstanding[k])
f_axi_awr_id_outstanding_count = f_axi_awr_id_outstanding_count +1;
end
wrfifo_data = wrfifo[wr_rdaddr];
 
always @(*)
assume((!F_CHECK_IDS)||(f_axi_awr_outstanding== f_axi_awr_id_outstanding_count));
assign this_wlen = wrfifo_data;
 
always @(*)
assume((!F_CHECK_IDS)||(f_axi_wr_outstanding == f_axi_wr_id_outstanding_count));
if ((i_axi_wvalid)&&(i_axi_wlast)&&(f_axi_awr_nbursts>0))
`SLAVE_ASSUME(i_axi_wlast == (this_wlen == f_axi_wr_count));
 
always @(*)
assume((!F_CHECK_IDS)||(f_axi_rd_outstanding == f_axi_rd_id_outstanding_count));
// Advance the read pointer for the write FIFO
initial wr_rdaddr = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
wr_rdaddr <= 0;
else if ((axi_wr_req)&&(i_axi_wlast))
wr_rdaddr <= wr_rdaddr + 1'b1;
 
always @(*)
assume( ((f_axi_wr_id_complete)&(~f_axi_awr_id_outstanding)) == 0);
assign wrfifo_fill = wr_wraddr - wr_rdaddr;
 
generate if (F_OPT_BURSTS)
begin
reg [(8-1):0] f_rd_pending [0:(FIFOLN-1)];
reg [(8-1):0] f_wr_pending,
f_rd_count, f_wr_count;
////////////////////////////////////////////////////////////////////////
//
// Read FIFO
//
parameter NRDFIFO = 8;
parameter WRDFIFO = 9;
 
reg r_last_rd_id_valid,
r_last_wr_id_valid;
 
reg [(C_AXI_ID_WIDTH-1):0] r_last_wr_id, r_last_rd_id;
initial f_axi_rd_count = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_rd_count <= 0;
else if (axi_rd_ack)
begin
if (i_axi_rlast)
f_axi_rd_count <= 1'b0;
else
f_axi_rd_count <= f_axi_rd_count + 1'b1;
end
 
initial r_last_wr_id_valid = 1'b0;
initial r_last_rd_id_valid = 1'b0;
always @(posedge i_clk)
if (!i_axi_reset_n)
begin
r_last_wr_id_valid <= 1'b0;
r_last_rd_id_valid <= 1'b0;
f_wr_count <= 0;
f_rd_count <= 0;
end else begin
if (axi_awr_req)
begin
f_wr_pending <= i_axi_awlen+9'h1;
assume(f_wr_pending == 0);
r_last_wr_id_valid <= 1'b1;
end
always @(*)
`SLAVE_ASSUME(f_axi_rd_nbursts <= NRDFIFO);
 
if (axi_ard_req)
f_rd_pending[i_axi_arid] <= i_axi_arlen+9'h1;
/*
always @(*)
if (i_axi_rvalid)
begin
if (i_axi_rlast)
`SLAVE_ASSERT(f_axi_rdfifo[WRDFIFO-1:0] == f_axi_rd_count);
else
`SLAVE_ASSERT(f_axi_rdfifo[WRDFIFO-1:0] < f_axi_rd_count);
end
 
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_rdfifo <= 0;
else casez({ axi_ard_req, axi_rd_ack, i_axi_rlast })
3'b10?: f_axi_rdfifo[ f_axi_rd_nbursts*WRDFIFO +: WRDFIFO]
<= { 1'b0, i_axi_arlen };
// 3'b010: f_axi_rdfifo[ 8:0] <= f_axi_rdfifo[8:0] - 1'b1;
3'b011: f_axi_rdfifo <= { {(WRDFIFO){1'b0}},
f_axi_rdfifo[NRDFIFO*WRDFIFO-1:WRDFIFO] };
3'b111: begin
f_axi_rdfifo <= { {(WRDFIFO){1'b0}},
f_axi_rdfifo[NRDFIFO*WRDFIFO-1:WRDFIFO] };
f_axi_rdfifo[ (f_axi_rd_nbursts-1)*WRDFIFO +: WRDFIFO]
<= { 1'b0, i_axi_arlen };
end
default: begin end
endcase
 
if ((axi_wr_req)&&(i_axi_wlast))
begin
f_wr_count <= 0;
r_last_wr_id_valid <= 1'b0;
assume(
// Either this is the last
// of a series of requests we've
// been waiting for,
(f_wr_pending == f_wr_count - 9'h1)
// *or* the only value
// associated with an as yet
// to be counted request
||((axi_awr_req)&&(i_axi_awlen == 0)));
end else if (axi_wr_req)
f_wr_count <= f_wr_count + 1'b1;
always @(*)
if (f_axi_rd_nbursts < NRDFIFO)
assert(f_axi_rdfifo[NRDFIFO * WRDFIFO-1: f_axi_rd_nbursts*WRDFIFO] == 0);
 
if (axi_rd_ack)
always @(*)
begin
rdfifo_outstanding = 0;
for(k = 0; k < NRDFIFO; k=k+1)
begin
if (k < f_axi_rd_nbursts)
begin
if (i_axi_rlast)
r_last_rd_id_valid <= 1'b0;
else
r_last_rd_id_valid <= 1'b1;
 
r_last_rd_id <= i_axi_rid;
if ((axi_rd_ack)&&(r_last_rd_id_valid))
assert(i_axi_rid == r_last_rd_id);
rdfifo_outstanding = rdfifo_outstanding
+ f_axi_rdfifo[k * WRDFIFO +: WRDFIFO] + 1;
end
 
if ((axi_rd_ack)&&(i_axi_rlast))
assume(f_rd_count == f_rd_pending[i_axi_rid]-9'h1);
if ((axi_rd_ack)&&(i_axi_rlast))
f_rd_count <= 0;
else if (axi_rd_ack)
f_rd_count <= f_rd_count + 1'b1;
assert(f_axi_rdfifo[k*WRDFIFO+(WRDFIFO-1)] == 1'b0);
end
end else begin
always @(*) begin
// Since we aren't allowing bursts, *every*
// write data and read data must always be the last
// value
assume((i_axi_wlast)||(!i_axi_wvalid));
assert((i_axi_rlast)||(!i_axi_rvalid));
end
 
assume((!i_axi_arvalid)||(i_axi_arlen==0));
assume((!i_axi_awvalid)||(i_axi_awlen==0));
end
always @(posedge i_clk)
assert(rdfifo_outstanding - f_axi_rd_count
== f_axi_rd_outstanding);
*/
 
always @(posedge i_clk)
if (i_axi_awvalid)
assume(i_axi_awlen == 0);
always @(posedge i_clk)
if (i_axi_arvalid)
assume(i_axi_arlen == 0);
always @(posedge i_clk)
if (i_axi_wvalid)
assume(i_axi_wlast);
always @(posedge i_clk)
if (i_axi_rvalid)
assert(i_axi_rlast);
end endgenerate
 
`endif
always @(*)
f_axi_rdfifo = 0;
endmodule
/faxil_master.v
0,0 → 1,605
////////////////////////////////////////////////////////////////////////////////
//
// Filename: faxil_master.v (Formal properties of an AXI lite master)
//
// Project: Pipelined Wishbone to AXI converter
//
// Purpose:
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2018-2019, Gisselquist Technology, LLC
//
// This file is part of the pipelined Wishbone to AXI converter project, a
// project that contains multiple bus bridging designs and formal bus property
// sets.
//
// The bus bridge designs and property sets are free RTL designs: you can
// redistribute them and/or modify any of them under the terms of the GNU
// Lesser General Public License as published by the Free Software Foundation,
// either version 3 of the License, or (at your option) any later version.
//
// The bus bridge designs and property sets are distributed in the hope that
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with these designs. (It's in the $(ROOT)/doc directory. Run make
// with no target there if the PDF file isn't present.) If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License: LGPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/lgpl.html
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype none
//
module faxil_master #(
parameter C_AXI_DATA_WIDTH = 32,// Fixed, width of the AXI R&W data
parameter C_AXI_ADDR_WIDTH = 28,// AXI Address width (log wordsize)
localparam DW = C_AXI_DATA_WIDTH,
localparam AW = C_AXI_ADDR_WIDTH,
parameter [0:0] F_OPT_HAS_CACHE = 1'b0,
parameter [0:0] F_OPT_NO_READS = 1'b0,
parameter [0:0] F_OPT_NO_WRITES = 1'b0,
parameter [0:0] F_OPT_BRESP = 1'b1,
parameter [0:0] F_OPT_RRESP = 1'b1,
parameter [0:0] F_OPT_ASSUME_RESET = 1'b0,
parameter F_LGDEPTH = 4,
parameter [(F_LGDEPTH-1):0] F_AXI_MAXWAIT = 12,
parameter [(F_LGDEPTH-1):0] F_AXI_MAXDELAY = 12
) (
input wire i_clk, // System clock
input wire i_axi_reset_n,
 
// AXI write address channel signals
input wire i_axi_awready,//Slave is ready to accept
input wire [AW-1:0] i_axi_awaddr, // Write address
input wire [3:0] i_axi_awcache, // Write Cache type
input wire [2:0] i_axi_awprot, // Write Protection type
input wire i_axi_awvalid, // Write address valid
 
// AXI write data channel signals
input wire i_axi_wready, // Write data ready
input wire [DW-1:0] i_axi_wdata, // Write data
input wire [DW/8-1:0] i_axi_wstrb, // Write strobes
input wire i_axi_wvalid, // Write valid
 
// AXI write response channel signals
input wire [1:0] i_axi_bresp, // Write response
input wire i_axi_bvalid, // Write reponse valid
input wire i_axi_bready, // Response ready
 
// AXI read address channel signals
input wire i_axi_arready, // Read address ready
input wire [AW-1:0] i_axi_araddr, // Read address
input wire [3:0] i_axi_arcache, // Read Cache type
input wire [2:0] i_axi_arprot, // Read Protection type
input wire i_axi_arvalid, // Read address valid
 
// AXI read data channel signals
input wire [1:0] i_axi_rresp, // Read response
input wire i_axi_rvalid, // Read reponse valid
input wire [DW-1:0] i_axi_rdata, // Read data
input wire i_axi_rready, // Read Response ready
//
output reg [(F_LGDEPTH-1):0] f_axi_rd_outstanding,
output reg [(F_LGDEPTH-1):0] f_axi_wr_outstanding,
output reg [(F_LGDEPTH-1):0] f_axi_awr_outstanding
);
 
//*****************************************************************************
// Parameter declarations
//*****************************************************************************
 
//*****************************************************************************
// Internal register and wire declarations
//*****************************************************************************
 
// wire w_fifo_full;
wire axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req,
axi_rd_err, axi_wr_err;
//
assign axi_ard_req = (i_axi_arvalid)&&(i_axi_arready);
assign axi_awr_req = (i_axi_awvalid)&&(i_axi_awready);
assign axi_wr_req = (i_axi_wvalid )&&(i_axi_wready);
//
assign axi_rd_ack = (i_axi_rvalid)&&(i_axi_rready);
assign axi_wr_ack = (i_axi_bvalid)&&(i_axi_bready);
assign axi_rd_err = (axi_rd_ack)&&(i_axi_rresp[1]);
assign axi_wr_err = (axi_wr_ack)&&(i_axi_bresp[1]);
 
`define SLAVE_ASSUME assert
`define SLAVE_ASSERT assume
 
//
// Setup
//
reg f_past_valid;
integer k;
 
initial f_past_valid = 1'b0;
always @(posedge i_clk)
f_past_valid <= 1'b1;
 
generate if (F_OPT_ASSUME_RESET)
begin : ASSUME_INIITAL_RESET
always @(*)
if (!f_past_valid)
assume(!i_axi_reset_n);
end else begin : ASSERT_INIITAL_RESET
always @(*)
if (!f_past_valid)
assert(!i_axi_reset_n);
end endgenerate
 
////////////////////////////////////////////////////////////////////////
//
//
// Reset properties
//
//
////////////////////////////////////////////////////////////////////////
 
//
// If asserted, the reset must be asserted for a minimum of 16 clocks
reg [3:0] f_reset_length;
initial f_reset_length = 0;
always @(posedge i_clk)
if (i_axi_reset_n)
f_reset_length <= 0;
else if (!(&f_reset_length))
f_reset_length <= f_reset_length + 1'b1;
 
 
generate if (F_OPT_ASSUME_RESET)
begin : ASSUME_RESET
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
assume(!i_axi_reset_n);
 
always @(*)
if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
assume(!i_axi_reset_n);
 
end else begin : ASSERT_RESET
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
assert(!i_axi_reset_n);
 
always @(*)
if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
assert(!i_axi_reset_n);
 
end endgenerate
 
always @(posedge i_clk)
if ((!f_past_valid)||(!$past(i_axi_reset_n)))
begin
`SLAVE_ASSUME(!i_axi_arvalid);
`SLAVE_ASSUME(!i_axi_awvalid);
`SLAVE_ASSUME(!i_axi_wvalid);
//
`SLAVE_ASSERT(!i_axi_bvalid);
`SLAVE_ASSERT(!i_axi_rvalid);
end
 
////////////////////////////////////////////////////////////////////////
//
//
// Constant input assumptions (cache and prot)
//
//
////////////////////////////////////////////////////////////////////////
 
always @(*)
if (i_axi_awvalid)
begin
`SLAVE_ASSUME(i_axi_awprot == 3'h0);
if (F_OPT_HAS_CACHE)
// Normal non-cachable, but bufferable
`SLAVE_ASSUME(i_axi_awcache == 4'h3);
else
// No caching capability
`SLAVE_ASSUME(i_axi_awcache == 4'h0);
end
 
always @(*)
if (i_axi_arvalid)
begin
`SLAVE_ASSUME(i_axi_arprot == 3'h0);
if (F_OPT_HAS_CACHE)
// Normal non-cachable, but bufferable
`SLAVE_ASSUME(i_axi_arcache == 4'h3);
else
// No caching capability
`SLAVE_ASSUME(i_axi_arcache == 4'h0);
end
 
always @(*)
if ((i_axi_bvalid)&&(!F_OPT_BRESP))
`SLAVE_ASSERT(i_axi_bresp == 0);
always @(*)
if ((i_axi_rvalid)&&(!F_OPT_RRESP))
`SLAVE_ASSERT(i_axi_rresp == 0);
always @(*)
if (i_axi_bvalid)
`SLAVE_ASSERT(i_axi_bresp != 2'b01); // Exclusive access not allowed
always @(*)
if (i_axi_rvalid)
`SLAVE_ASSERT(i_axi_rresp != 2'b01); // Exclusive access not allowed
 
 
////////////////////////////////////////////////////////////////////////
//
//
// Stability assumptions
//
//
////////////////////////////////////////////////////////////////////////
 
// Assume any response from the bus will not change prior to that
// response being accepted
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_axi_reset_n)))
begin
// Write address channel
if ((f_past_valid)&&($past(i_axi_awvalid))&&(!$past(i_axi_awready)))
begin
`SLAVE_ASSUME(i_axi_awvalid);
`SLAVE_ASSUME($stable(i_axi_awaddr));
end
 
// Write data channel
if ((f_past_valid)&&($past(i_axi_wvalid))&&(!$past(i_axi_wready)))
begin
`SLAVE_ASSUME(i_axi_wvalid);
`SLAVE_ASSUME($stable(i_axi_wstrb));
`SLAVE_ASSUME($stable(i_axi_wdata));
end
 
// Incoming Read address channel
if ((f_past_valid)&&($past(i_axi_arvalid))&&(!$past(i_axi_arready)))
begin
`SLAVE_ASSUME(i_axi_arvalid);
`SLAVE_ASSUME($stable(i_axi_araddr));
end
 
if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready)))
begin
`SLAVE_ASSERT(i_axi_rvalid);
`SLAVE_ASSERT($stable(i_axi_rresp));
`SLAVE_ASSERT($stable(i_axi_rdata));
end
 
if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready)))
begin
`SLAVE_ASSERT(i_axi_bvalid);
`SLAVE_ASSERT($stable(i_axi_bresp));
end
end
 
// Nothing should be returned or requested on the first clock
initial `SLAVE_ASSUME(!i_axi_arvalid);
initial `SLAVE_ASSUME(!i_axi_awvalid);
initial `SLAVE_ASSUME(!i_axi_wvalid);
//
initial `SLAVE_ASSERT(!i_axi_bvalid);
initial `SLAVE_ASSERT(!i_axi_rvalid);
 
////////////////////////////////////////////////////////////////////////
//
//
// Insist upon a maximum delay before a request is accepted
//
//
////////////////////////////////////////////////////////////////////////
 
generate if (F_AXI_MAXWAIT > 0)
begin : CHECK_STALL_COUNT
//
// AXI write address channel
//
//
reg [(F_LGDEPTH-1):0] f_axi_awstall,
f_axi_wstall,
f_axi_arstall,
f_axi_bstall,
f_axi_rstall;
 
initial f_axi_awstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_awvalid)||(i_axi_awready))
f_axi_awstall <= 0;
else if ((f_axi_awr_outstanding >= f_axi_wr_outstanding)
&&(i_axi_awvalid && !i_axi_wvalid))
// If we are waiting for the write channel to be valid
// then don't count stalls
f_axi_awstall <= 0;
else if ((!i_axi_bvalid)||(i_axi_bready))
f_axi_awstall <= f_axi_awstall + 1'b1;
 
always @(*)
`SLAVE_ASSERT(f_axi_awstall < F_AXI_MAXWAIT);
 
//
// AXI write data channel
//
//
initial f_axi_wstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_wvalid)||(i_axi_wready))
f_axi_wstall <= 0;
else if ((f_axi_wr_outstanding >= f_axi_awr_outstanding)
&&(!i_axi_awvalid && i_axi_wvalid))
// If we are waiting for the write address channel
// to be valid, then don't count stalls
f_axi_wstall <= 0;
else if ((!i_axi_bvalid)||(i_axi_bready))
f_axi_wstall <= f_axi_wstall + 1'b1;
 
always @(*)
`SLAVE_ASSERT(f_axi_wstall < F_AXI_MAXWAIT);
 
//
// AXI read address channel
//
//
initial f_axi_arstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_arvalid)||(i_axi_arready))
f_axi_arstall <= 0;
else if ((!i_axi_rvalid)||(i_axi_rready))
f_axi_arstall <= f_axi_arstall + 1'b1;
 
always @(*)
`SLAVE_ASSERT(f_axi_arstall < F_AXI_MAXWAIT);
 
// AXI write response channel
initial f_axi_bstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_bvalid)||(i_axi_bready))
f_axi_bstall <= 0;
else
f_axi_bstall <= f_axi_bstall + 1'b1;
 
always @(*)
`SLAVE_ASSUME(f_axi_bstall < F_AXI_MAXWAIT);
 
// AXI read response channel
initial f_axi_rstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_rvalid)||(i_axi_rready))
f_axi_rstall <= 0;
else
f_axi_rstall <= f_axi_rstall + 1'b1;
 
always @(*)
`SLAVE_ASSUME(f_axi_rstall < F_AXI_MAXWAIT);
 
end endgenerate
 
////////////////////////////////////////////////////////////////////////
//
//
// Xilinx extensions/guarantees to the AXI protocol
//
// 1. The address line will never be more than two clocks ahead of
// the write data channel, and
// 2. The write data channel will never be more than one clock
// ahead of the address channel.
//
//
////////////////////////////////////////////////////////////////////////
//
//
// Rule number one:
always @(posedge i_clk)
if ((i_axi_reset_n)&&($past(i_axi_reset_n))
&&($past(i_axi_awvalid && !i_axi_wvalid,2))
&&($past(f_axi_awr_outstanding>=f_axi_wr_outstanding,2))
&&(!$past(i_axi_wvalid)))
`SLAVE_ASSUME(i_axi_wvalid);
 
// Rule number two:
always @(posedge i_clk)
if ((i_axi_reset_n)&&(!$past(i_axi_awvalid))&&($past(i_axi_wvalid))
&&(f_axi_awr_outstanding < f_axi_wr_outstanding))
`SLAVE_ASSUME(i_axi_awvalid);
 
////////////////////////////////////////////////////////////////////////
//
//
// Count outstanding transactions. With these measures, we count
// once per any burst.
//
//
////////////////////////////////////////////////////////////////////////
initial f_axi_awr_outstanding = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_awr_outstanding <= 0;
else case({ (axi_awr_req), (axi_wr_ack) })
2'b10: f_axi_awr_outstanding <= f_axi_awr_outstanding + 1'b1;
2'b01: f_axi_awr_outstanding <= f_axi_awr_outstanding - 1'b1;
default: begin end
endcase
 
initial f_axi_wr_outstanding = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_wr_outstanding <= 0;
else case({ (axi_wr_req), (axi_wr_ack) })
2'b01: f_axi_wr_outstanding <= f_axi_wr_outstanding - 1'b1;
2'b10: f_axi_wr_outstanding <= f_axi_wr_outstanding + 1'b1;
endcase
 
initial f_axi_rd_outstanding = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_rd_outstanding <= 0;
else case({ (axi_ard_req), (axi_rd_ack) })
2'b01: f_axi_rd_outstanding <= f_axi_rd_outstanding - 1'b1;
2'b10: f_axi_rd_outstanding <= f_axi_rd_outstanding + 1'b1;
endcase
 
//
// Do not let the number of outstanding requests overflow
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_wr_outstanding < {(F_LGDEPTH){1'b1}});
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_awr_outstanding < {(F_LGDEPTH){1'b1}});
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_rd_outstanding < {(F_LGDEPTH){1'b1}});
 
//
// That means that requests need to stop when we're almost full
always @(posedge i_clk)
if (f_axi_awr_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
assert(!i_axi_awvalid);
always @(posedge i_clk)
if (f_axi_wr_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
assert(!i_axi_wvalid);
always @(posedge i_clk)
if (f_axi_rd_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
assert(!i_axi_arvalid);
 
////////////////////////////////////////////////////////////////////////
//
//
// Insist that all responses are returned in less than a maximum delay
// In this case, we count responses within a burst, rather than entire
// bursts.
//
//
////////////////////////////////////////////////////////////////////////
generate if (F_AXI_MAXDELAY > 0)
begin : CHECK_MAX_DELAY
 
reg [(F_LGDEPTH-1):0] f_axi_wr_ack_delay,
f_axi_rd_ack_delay;
 
initial f_axi_rd_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(i_axi_rvalid)||(f_axi_rd_outstanding==0))
f_axi_rd_ack_delay <= 0;
else
f_axi_rd_ack_delay <= f_axi_rd_ack_delay + 1'b1;
 
initial f_axi_wr_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(i_axi_bvalid)||(f_axi_wr_outstanding==0))
f_axi_wr_ack_delay <= 0;
else if (f_axi_wr_outstanding > 0)
f_axi_wr_ack_delay <= f_axi_wr_ack_delay + 1'b1;
 
always @(*)
`SLAVE_ASSERT(f_axi_rd_ack_delay < F_AXI_MAXDELAY);
 
always @(*)
`SLAVE_ASSERT(f_axi_wr_ack_delay < F_AXI_MAXDELAY);
 
end endgenerate
 
////////////////////////////////////////////////////////////////////////
//
//
// Assume acknowledgements must follow requests
//
// The f_axi*outstanding counters count the number of requests. No
// acknowledgment should issue without a pending request
// burst. Further, the spec is clear: you can't acknowledge something
// on the same clock you get the request. There must be at least one
// clock delay.
//
//
////////////////////////////////////////////////////////////////////////
 
//
// AXI write response channel
//
always @(posedge i_clk)
if (i_axi_bvalid)
begin
`SLAVE_ASSERT(f_axi_awr_outstanding > 0);
`SLAVE_ASSERT(f_axi_wr_outstanding > 0);
end
 
//
// AXI read data channel signals
//
always @(posedge i_clk)
if (i_axi_rvalid)
`SLAVE_ASSERT(f_axi_rd_outstanding > 0);
 
////////////////////////////////////////////////////////////////////////
//
//
// Optionally disable either read or write channels (or both??)
//
//
////////////////////////////////////////////////////////////////////////
 
initial assert((!F_OPT_NO_READS)||(!F_OPT_NO_WRITES));
 
generate if (F_OPT_NO_READS)
begin : NO_READS
 
always @(*)
`SLAVE_ASSUME(i_axi_arvalid == 0);
always @(*)
`SLAVE_ASSERT(f_axi_rd_outstanding == 0);
always @(*)
`SLAVE_ASSERT(i_axi_rvalid == 0);
 
end endgenerate
 
generate if (F_OPT_NO_WRITES)
begin : NO_WRITES
 
always @(*)
`SLAVE_ASSUME(i_axi_awvalid == 0);
always @(*)
`SLAVE_ASSUME(i_axi_wvalid == 0);
always @(*)
`SLAVE_ASSERT(f_axi_wr_outstanding == 0);
always @(*)
`SLAVE_ASSERT(f_axi_awr_outstanding == 0);
always @(*)
`SLAVE_ASSERT(i_axi_bvalid == 0);
 
end endgenerate
 
////////////////////////////////////////////////////////////////////////
//
//
// Cover properties
//
// We'll use this to prove that transactions are even possible, and
// hence that we haven't so constrained the bus that nothing can take
// place.
//
//
////////////////////////////////////////////////////////////////////////
 
//
// AXI write response channel
//
always @(posedge i_clk)
if (!F_OPT_NO_WRITES)
cover((i_axi_bvalid)&&(i_axi_bready));
 
//
// AXI read response channel
//
always @(posedge i_clk)
if (!F_OPT_NO_READS)
cover((i_axi_rvalid)&&(i_axi_rready));
endmodule
/faxil_slave.v
0,0 → 1,605
////////////////////////////////////////////////////////////////////////////////
//
// Filename: faxil_slave.v (Formal properties of an AXI lite slave)
//
// Project: Pipelined Wishbone to AXI converter
//
// Purpose:
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2018-2019, Gisselquist Technology, LLC
//
// This file is part of the pipelined Wishbone to AXI converter project, a
// project that contains multiple bus bridging designs and formal bus property
// sets.
//
// The bus bridge designs and property sets are free RTL designs: you can
// redistribute them and/or modify any of them under the terms of the GNU
// Lesser General Public License as published by the Free Software Foundation,
// either version 3 of the License, or (at your option) any later version.
//
// The bus bridge designs and property sets are distributed in the hope that
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with these designs. (It's in the $(ROOT)/doc directory. Run make
// with no target there if the PDF file isn't present.) If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License: LGPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/lgpl.html
//
////////////////////////////////////////////////////////////////////////////////
//
//
`default_nettype none
//
module faxil_slave #(
parameter C_AXI_DATA_WIDTH = 32,// Fixed, width of the AXI R&W data
parameter C_AXI_ADDR_WIDTH = 28,// AXI Address width (log wordsize)
localparam DW = C_AXI_DATA_WIDTH,
localparam AW = C_AXI_ADDR_WIDTH,
parameter [0:0] F_OPT_HAS_CACHE = 1'b0,
parameter [0:0] F_OPT_NO_READS = 1'b0,
parameter [0:0] F_OPT_NO_WRITES = 1'b0,
parameter [0:0] F_OPT_BRESP = 1'b1,
parameter [0:0] F_OPT_RRESP = 1'b1,
parameter [0:0] F_OPT_ASSUME_RESET = 1'b1,
parameter F_LGDEPTH = 4,
parameter [(F_LGDEPTH-1):0] F_AXI_MAXWAIT = 12,
parameter [(F_LGDEPTH-1):0] F_AXI_MAXDELAY = 12
) (
input wire i_clk, // System clock
input wire i_axi_reset_n,
 
// AXI write address channel signals
input wire i_axi_awready,//Slave is ready to accept
input wire [AW-1:0] i_axi_awaddr, // Write address
input wire [3:0] i_axi_awcache, // Write Cache type
input wire [2:0] i_axi_awprot, // Write Protection type
input wire i_axi_awvalid, // Write address valid
 
// AXI write data channel signals
input wire i_axi_wready, // Write data ready
input wire [DW-1:0] i_axi_wdata, // Write data
input wire [DW/8-1:0] i_axi_wstrb, // Write strobes
input wire i_axi_wvalid, // Write valid
 
// AXI write response channel signals
input wire [1:0] i_axi_bresp, // Write response
input wire i_axi_bvalid, // Write reponse valid
input wire i_axi_bready, // Response ready
 
// AXI read address channel signals
input wire i_axi_arready, // Read address ready
input wire [AW-1:0] i_axi_araddr, // Read address
input wire [3:0] i_axi_arcache, // Read Cache type
input wire [2:0] i_axi_arprot, // Read Protection type
input wire i_axi_arvalid, // Read address valid
 
// AXI read data channel signals
input wire [1:0] i_axi_rresp, // Read response
input wire i_axi_rvalid, // Read reponse valid
input wire [DW-1:0] i_axi_rdata, // Read data
input wire i_axi_rready, // Read Response ready
//
output reg [(F_LGDEPTH-1):0] f_axi_rd_outstanding,
output reg [(F_LGDEPTH-1):0] f_axi_wr_outstanding,
output reg [(F_LGDEPTH-1):0] f_axi_awr_outstanding
);
 
//*****************************************************************************
// Parameter declarations
//*****************************************************************************
 
//*****************************************************************************
// Internal register and wire declarations
//*****************************************************************************
 
// wire w_fifo_full;
wire axi_rd_ack, axi_wr_ack, axi_ard_req, axi_awr_req, axi_wr_req,
axi_rd_err, axi_wr_err;
//
assign axi_ard_req = (i_axi_arvalid)&&(i_axi_arready);
assign axi_awr_req = (i_axi_awvalid)&&(i_axi_awready);
assign axi_wr_req = (i_axi_wvalid )&&(i_axi_wready);
//
assign axi_rd_ack = (i_axi_rvalid)&&(i_axi_rready);
assign axi_wr_ack = (i_axi_bvalid)&&(i_axi_bready);
assign axi_rd_err = (axi_rd_ack)&&(i_axi_rresp[1]);
assign axi_wr_err = (axi_wr_ack)&&(i_axi_bresp[1]);
 
`define SLAVE_ASSUME assume
`define SLAVE_ASSERT assert
 
//
// Setup
//
reg f_past_valid;
integer k;
 
initial f_past_valid = 1'b0;
always @(posedge i_clk)
f_past_valid <= 1'b1;
 
generate if (F_OPT_ASSUME_RESET)
begin : ASSUME_INIITAL_RESET
always @(*)
if (!f_past_valid)
assume(!i_axi_reset_n);
end else begin : ASSERT_INIITAL_RESET
always @(*)
if (!f_past_valid)
assert(!i_axi_reset_n);
end endgenerate
 
////////////////////////////////////////////////////////////////////////
//
//
// Reset properties
//
//
////////////////////////////////////////////////////////////////////////
 
//
// If asserted, the reset must be asserted for a minimum of 16 clocks
reg [3:0] f_reset_length;
initial f_reset_length = 0;
always @(posedge i_clk)
if (i_axi_reset_n)
f_reset_length <= 0;
else if (!(&f_reset_length))
f_reset_length <= f_reset_length + 1'b1;
 
 
generate if (F_OPT_ASSUME_RESET)
begin : ASSUME_RESET
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
assume(!i_axi_reset_n);
 
always @(*)
if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
assume(!i_axi_reset_n);
 
end else begin : ASSERT_RESET
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_axi_reset_n))&&(!$past(&f_reset_length)))
assert(!i_axi_reset_n);
 
always @(*)
if ((f_reset_length > 0)&&(f_reset_length < 4'hf))
assert(!i_axi_reset_n);
 
end endgenerate
 
always @(posedge i_clk)
if ((!f_past_valid)||(!$past(i_axi_reset_n)))
begin
`SLAVE_ASSUME(!i_axi_arvalid);
`SLAVE_ASSUME(!i_axi_awvalid);
`SLAVE_ASSUME(!i_axi_wvalid);
//
`SLAVE_ASSERT(!i_axi_bvalid);
`SLAVE_ASSERT(!i_axi_rvalid);
end
 
////////////////////////////////////////////////////////////////////////
//
//
// Constant input assumptions (cache and prot)
//
//
////////////////////////////////////////////////////////////////////////
 
always @(*)
if (i_axi_awvalid)
begin
`SLAVE_ASSUME(i_axi_awprot == 3'h0);
if (F_OPT_HAS_CACHE)
// Normal non-cachable, but bufferable
`SLAVE_ASSUME(i_axi_awcache == 4'h3);
else
// No caching capability
`SLAVE_ASSUME(i_axi_awcache == 4'h0);
end
 
always @(*)
if (i_axi_arvalid)
begin
`SLAVE_ASSUME(i_axi_arprot == 3'h0);
if (F_OPT_HAS_CACHE)
// Normal non-cachable, but bufferable
`SLAVE_ASSUME(i_axi_arcache == 4'h3);
else
// No caching capability
`SLAVE_ASSUME(i_axi_arcache == 4'h0);
end
 
always @(*)
if ((i_axi_bvalid)&&(!F_OPT_BRESP))
`SLAVE_ASSERT(i_axi_bresp == 0);
always @(*)
if ((i_axi_rvalid)&&(!F_OPT_RRESP))
`SLAVE_ASSERT(i_axi_rresp == 0);
always @(*)
if (i_axi_bvalid)
`SLAVE_ASSERT(i_axi_bresp != 2'b01); // Exclusive access not allowed
always @(*)
if (i_axi_rvalid)
`SLAVE_ASSERT(i_axi_rresp != 2'b01); // Exclusive access not allowed
 
 
////////////////////////////////////////////////////////////////////////
//
//
// Stability assumptions
//
//
////////////////////////////////////////////////////////////////////////
 
// Assume any response from the bus will not change prior to that
// response being accepted
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_axi_reset_n)))
begin
// Write address channel
if ((f_past_valid)&&($past(i_axi_awvalid))&&(!$past(i_axi_awready)))
begin
`SLAVE_ASSUME(i_axi_awvalid);
`SLAVE_ASSUME($stable(i_axi_awaddr));
end
 
// Write data channel
if ((f_past_valid)&&($past(i_axi_wvalid))&&(!$past(i_axi_wready)))
begin
`SLAVE_ASSUME(i_axi_wvalid);
`SLAVE_ASSUME($stable(i_axi_wstrb));
`SLAVE_ASSUME($stable(i_axi_wdata));
end
 
// Incoming Read address channel
if ((f_past_valid)&&($past(i_axi_arvalid))&&(!$past(i_axi_arready)))
begin
`SLAVE_ASSUME(i_axi_arvalid);
`SLAVE_ASSUME($stable(i_axi_araddr));
end
 
if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready)))
begin
`SLAVE_ASSERT(i_axi_rvalid);
`SLAVE_ASSERT($stable(i_axi_rresp));
`SLAVE_ASSERT($stable(i_axi_rdata));
end
 
if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready)))
begin
`SLAVE_ASSERT(i_axi_bvalid);
`SLAVE_ASSERT($stable(i_axi_bresp));
end
end
 
// Nothing should be returned or requested on the first clock
initial `SLAVE_ASSUME(!i_axi_arvalid);
initial `SLAVE_ASSUME(!i_axi_awvalid);
initial `SLAVE_ASSUME(!i_axi_wvalid);
//
initial `SLAVE_ASSERT(!i_axi_bvalid);
initial `SLAVE_ASSERT(!i_axi_rvalid);
 
////////////////////////////////////////////////////////////////////////
//
//
// Insist upon a maximum delay before a request is accepted
//
//
////////////////////////////////////////////////////////////////////////
 
generate if (F_AXI_MAXWAIT > 0)
begin : CHECK_STALL_COUNT
//
// AXI write address channel
//
//
reg [(F_LGDEPTH-1):0] f_axi_awstall,
f_axi_wstall,
f_axi_arstall,
f_axi_bstall,
f_axi_rstall;
 
initial f_axi_awstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_awvalid)||(i_axi_awready))
f_axi_awstall <= 0;
else if ((f_axi_awr_outstanding >= f_axi_wr_outstanding)
&&(i_axi_awvalid && !i_axi_wvalid))
// If we are waiting for the write channel to be valid
// then don't count stalls
f_axi_awstall <= 0;
else if ((!i_axi_bvalid)||(i_axi_bready))
f_axi_awstall <= f_axi_awstall + 1'b1;
 
always @(*)
`SLAVE_ASSERT(f_axi_awstall < F_AXI_MAXWAIT);
 
//
// AXI write data channel
//
//
initial f_axi_wstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_wvalid)||(i_axi_wready))
f_axi_wstall <= 0;
else if ((f_axi_wr_outstanding >= f_axi_awr_outstanding)
&&(!i_axi_awvalid && i_axi_wvalid))
// If we are waiting for the write address channel
// to be valid, then don't count stalls
f_axi_wstall <= 0;
else if ((!i_axi_bvalid)||(i_axi_bready))
f_axi_wstall <= f_axi_wstall + 1'b1;
 
always @(*)
`SLAVE_ASSERT(f_axi_wstall < F_AXI_MAXWAIT);
 
//
// AXI read address channel
//
//
initial f_axi_arstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_arvalid)||(i_axi_arready))
f_axi_arstall <= 0;
else if ((!i_axi_rvalid)||(i_axi_rready))
f_axi_arstall <= f_axi_arstall + 1'b1;
 
always @(*)
`SLAVE_ASSERT(f_axi_arstall < F_AXI_MAXWAIT);
 
// AXI write response channel
initial f_axi_bstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_bvalid)||(i_axi_bready))
f_axi_bstall <= 0;
else
f_axi_bstall <= f_axi_bstall + 1'b1;
 
always @(*)
`SLAVE_ASSUME(f_axi_bstall < F_AXI_MAXWAIT);
 
// AXI read response channel
initial f_axi_rstall = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(!i_axi_rvalid)||(i_axi_rready))
f_axi_rstall <= 0;
else
f_axi_rstall <= f_axi_rstall + 1'b1;
 
always @(*)
`SLAVE_ASSUME(f_axi_rstall < F_AXI_MAXWAIT);
 
end endgenerate
 
////////////////////////////////////////////////////////////////////////
//
//
// Xilinx extensions/guarantees to the AXI protocol
//
// 1. The address line will never be more than two clocks ahead of
// the write data channel, and
// 2. The write data channel will never be more than one clock
// ahead of the address channel.
//
//
////////////////////////////////////////////////////////////////////////
//
//
// Rule number one:
always @(posedge i_clk)
if ((i_axi_reset_n)&&($past(i_axi_reset_n))
&&($past(i_axi_awvalid && !i_axi_wvalid,2))
&&($past(f_axi_awr_outstanding>=f_axi_wr_outstanding,2))
&&(!$past(i_axi_wvalid)))
`SLAVE_ASSUME(i_axi_wvalid);
 
// Rule number two:
always @(posedge i_clk)
if ((i_axi_reset_n)&&(!$past(i_axi_awvalid))&&($past(i_axi_wvalid))
&&(f_axi_awr_outstanding < f_axi_wr_outstanding))
`SLAVE_ASSUME(i_axi_awvalid);
 
////////////////////////////////////////////////////////////////////////
//
//
// Count outstanding transactions. With these measures, we count
// once per any burst.
//
//
////////////////////////////////////////////////////////////////////////
initial f_axi_awr_outstanding = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_awr_outstanding <= 0;
else case({ (axi_awr_req), (axi_wr_ack) })
2'b10: f_axi_awr_outstanding <= f_axi_awr_outstanding + 1'b1;
2'b01: f_axi_awr_outstanding <= f_axi_awr_outstanding - 1'b1;
default: begin end
endcase
 
initial f_axi_wr_outstanding = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_wr_outstanding <= 0;
else case({ (axi_wr_req), (axi_wr_ack) })
2'b01: f_axi_wr_outstanding <= f_axi_wr_outstanding - 1'b1;
2'b10: f_axi_wr_outstanding <= f_axi_wr_outstanding + 1'b1;
endcase
 
initial f_axi_rd_outstanding = 0;
always @(posedge i_clk)
if (!i_axi_reset_n)
f_axi_rd_outstanding <= 0;
else case({ (axi_ard_req), (axi_rd_ack) })
2'b01: f_axi_rd_outstanding <= f_axi_rd_outstanding - 1'b1;
2'b10: f_axi_rd_outstanding <= f_axi_rd_outstanding + 1'b1;
endcase
 
//
// Do not let the number of outstanding requests overflow
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_wr_outstanding < {(F_LGDEPTH){1'b1}});
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_awr_outstanding < {(F_LGDEPTH){1'b1}});
always @(posedge i_clk)
`SLAVE_ASSERT(f_axi_rd_outstanding < {(F_LGDEPTH){1'b1}});
 
//
// That means that requests need to stop when we're almost full
always @(posedge i_clk)
if (f_axi_awr_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
assert(!i_axi_awvalid);
always @(posedge i_clk)
if (f_axi_wr_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
assert(!i_axi_wvalid);
always @(posedge i_clk)
if (f_axi_rd_outstanding == { {(F_LGDEPTH-1){1'b1}}, 1'b0} )
assert(!i_axi_arvalid);
 
////////////////////////////////////////////////////////////////////////
//
//
// Insist that all responses are returned in less than a maximum delay
// In this case, we count responses within a burst, rather than entire
// bursts.
//
//
////////////////////////////////////////////////////////////////////////
generate if (F_AXI_MAXDELAY > 0)
begin : CHECK_MAX_DELAY
 
reg [(F_LGDEPTH-1):0] f_axi_wr_ack_delay,
f_axi_rd_ack_delay;
 
initial f_axi_rd_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(i_axi_rvalid)||(f_axi_rd_outstanding==0))
f_axi_rd_ack_delay <= 0;
else
f_axi_rd_ack_delay <= f_axi_rd_ack_delay + 1'b1;
 
initial f_axi_wr_ack_delay = 0;
always @(posedge i_clk)
if ((!i_axi_reset_n)||(i_axi_bvalid)||(f_axi_wr_outstanding==0))
f_axi_wr_ack_delay <= 0;
else if (f_axi_wr_outstanding > 0)
f_axi_wr_ack_delay <= f_axi_wr_ack_delay + 1'b1;
 
always @(*)
`SLAVE_ASSERT(f_axi_rd_ack_delay < F_AXI_MAXDELAY);
 
always @(*)
`SLAVE_ASSERT(f_axi_wr_ack_delay < F_AXI_MAXDELAY);
 
end endgenerate
 
////////////////////////////////////////////////////////////////////////
//
//
// Assume acknowledgements must follow requests
//
// The f_axi*outstanding counters count the number of requests. No
// acknowledgment should issue without a pending request
// burst. Further, the spec is clear: you can't acknowledge something
// on the same clock you get the request. There must be at least one
// clock delay.
//
//
////////////////////////////////////////////////////////////////////////
 
//
// AXI write response channel
//
always @(posedge i_clk)
if (i_axi_bvalid)
begin
`SLAVE_ASSERT(f_axi_awr_outstanding > 0);
`SLAVE_ASSERT(f_axi_wr_outstanding > 0);
end
 
//
// AXI read data channel signals
//
always @(posedge i_clk)
if (i_axi_rvalid)
`SLAVE_ASSERT(f_axi_rd_outstanding > 0);
 
////////////////////////////////////////////////////////////////////////
//
//
// Optionally disable either read or write channels (or both??)
//
//
////////////////////////////////////////////////////////////////////////
 
initial assert((!F_OPT_NO_READS)||(!F_OPT_NO_WRITES));
 
generate if (F_OPT_NO_READS)
begin : NO_READS
 
always @(*)
`SLAVE_ASSUME(i_axi_arvalid == 0);
always @(*)
`SLAVE_ASSERT(f_axi_rd_outstanding == 0);
always @(*)
`SLAVE_ASSERT(i_axi_rvalid == 0);
 
end endgenerate
 
generate if (F_OPT_NO_WRITES)
begin : NO_WRITES
 
always @(*)
`SLAVE_ASSUME(i_axi_awvalid == 0);
always @(*)
`SLAVE_ASSUME(i_axi_wvalid == 0);
always @(*)
`SLAVE_ASSERT(f_axi_wr_outstanding == 0);
always @(*)
`SLAVE_ASSERT(f_axi_awr_outstanding == 0);
always @(*)
`SLAVE_ASSERT(i_axi_bvalid == 0);
 
end endgenerate
 
////////////////////////////////////////////////////////////////////////
//
//
// Cover properties
//
// We'll use this to prove that transactions are even possible, and
// hence that we haven't so constrained the bus that nothing can take
// place.
//
//
////////////////////////////////////////////////////////////////////////
 
//
// AXI write response channel
//
always @(posedge i_clk)
if (!F_OPT_NO_WRITES)
cover((i_axi_bvalid)&&(i_axi_bready));
 
//
// AXI read response channel
//
always @(posedge i_clk)
if (!F_OPT_NO_READS)
cover((i_axi_rvalid)&&(i_axi_rready));
endmodule
/fwb_master.v
23,35 → 23,44
// slave inputs (the master outputs), and assertions are made about the
// slave outputs (the master inputs).
//
// In order to make it easier to compare the slave against the master,
// assumptions with respect to the slave have been marked with the
// `SLAVE_ASSUME macro. Similarly, assertions the slave would make have
// been marked with `SLAVE_ASSERT. This allows the master to redefine
// these two macros to be from his perspective, and therefore the
// diffs between the two files actually show true differences, rather
// than just these differences in perspective.
//
//
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2017, Gisselquist Technology, LLC
// Copyright (C) 2017-2018, 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
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
// This file is part of the pipelined Wishbone to AXI converter project, a
// project that contains multiple bus bridging designs and formal bus property
// sets.
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
// for more details.
// The bus bridge designs and property sets are free RTL designs: you can
// redistribute them and/or modify any of them under the terms of the GNU
// Lesser General Public License as published by the Free Software Foundation,
// either version 3 of the License, or (at your option) any later version.
//
// You should have received a copy of the GNU General Public License along
// with this program. (It's in the $(ROOT)/doc directory. Run make with no
// target there if the PDF file isn't present.) If not, see
// The bus bridge designs and property sets are distributed in the hope that
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with these designs. (It's in the $(ROOT)/doc directory. Run make
// with no target there if the PDF file isn't present.) If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License: GPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/gpl.html
// License: LGPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/lgpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
88,6 → 97,13
parameter [0:0] F_OPT_DISCONTINUOUS = 0;
//
//
// If true, insist that there be a minimum of a single clock delay
// between request and response. This defaults to off since the
// wishbone specification specifically doesn't require this. However,
// some interfaces do, so we allow it as an option here.
parameter [0:0] F_OPT_MINCLOCK_DELAY = 0;
//
//
localparam [(F_LGDEPTH-1):0] MAX_OUTSTANDING = {(F_LGDEPTH){1'b1}};
localparam MAX_DELAY = (F_MAX_STALL > F_MAX_ACK_DELAY)
? F_MAX_STALL : F_MAX_ACK_DELAY;
116,10 → 132,12
output reg [(F_LGDEPTH-1):0] f_nreqs, f_nacks;
output wire [(F_LGDEPTH-1):0] f_outstanding;
 
`define SLAVE_ASSUME assert
`define SLAVE_ASSERT assume
//
// Let's just make sure our parameters are set up right
//
assert property(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});
initial assert(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});
 
//
// Wrap the request line in a bundle. The top bit, named STB_BIT,
138,8 → 156,8
always @(posedge i_clk)
f_past_valid <= 1'b1;
always @(*)
if (!f_past_valid)
assume(i_reset);
if (!f_past_valid)
`SLAVE_ASSUME(i_reset);
//
//
// Assertions regarding the initial (and reset) state
149,38 → 167,25
//
// Assume we start from a reset condition
initial assert(i_reset);
initial assert(!i_wb_cyc);
initial assert(!i_wb_stb);
initial `SLAVE_ASSUME(!i_wb_cyc);
initial `SLAVE_ASSUME(!i_wb_stb);
//
initial assume(!i_wb_ack);
initial assume(!i_wb_err);
initial `SLAVE_ASSERT(!i_wb_ack);
initial `SLAVE_ASSERT(!i_wb_err);
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_reset)))
if ((!f_past_valid)||($past(i_reset)))
begin
assert(!i_wb_cyc);
assert(!i_wb_stb);
`SLAVE_ASSUME(!i_wb_cyc);
`SLAVE_ASSUME(!i_wb_stb);
//
assume(!i_wb_ack);
assume(!i_wb_err);
`SLAVE_ASSERT(!i_wb_ack);
`SLAVE_ASSERT(!i_wb_err);
end
 
// Things can only change on the positive edge of the clock
always @($global_clock)
if ((f_past_valid)&&(!$rose(i_clk)))
begin
assert($stable(i_reset));
assert($stable(i_wb_cyc));
if (i_wb_we)
assert($stable(f_request)); // The entire request should b stabl
else
assert($stable(f_request[(2+AW-1):(DW+DW/8)]));
//
assume($stable(i_wb_ack));
assume($stable(i_wb_stall));
assume($stable(i_wb_idata));
assume($stable(i_wb_err));
end
always @(*)
if (!f_past_valid)
`SLAVE_ASSUME(!i_wb_cyc);
 
//
//
192,12 → 197,12
// the transaction
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_wb_err))&&($past(i_wb_cyc)))
assert(!i_wb_cyc);
`SLAVE_ASSUME(!i_wb_cyc);
 
// STB can only be true if CYC is also true
always @(posedge i_clk)
if (i_wb_stb)
assert(i_wb_cyc);
always @(*)
if (i_wb_stb)
`SLAVE_ASSUME(i_wb_cyc);
 
// If a request was both outstanding and stalled on the last clock,
// then nothing should change on this clock regarding it.
205,27 → 210,31
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
&&($past(i_wb_stall))&&(i_wb_cyc))
begin
assert(i_wb_stb);
assert($stable(f_request));
`SLAVE_ASSUME(i_wb_stb);
`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
`SLAVE_ASSUME(i_wb_addr == $past(i_wb_addr));
`SLAVE_ASSUME(i_wb_sel == $past(i_wb_sel));
if (i_wb_we)
`SLAVE_ASSUME(i_wb_data == $past(i_wb_data));
end
 
// Within any series of STB/requests, the direction of the request
// may not change.
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_wb_stb))&&(i_wb_stb))
assert(i_wb_we == $past(i_wb_we));
if ((f_past_valid)&&($past(i_wb_stb))&&(i_wb_stb))
`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
 
 
// Within any given bus cycle, the direction may *only* change when
// there are no further outstanding requests.
always @(posedge i_clk)
if ((f_past_valid)&&(f_outstanding > 0))
assert(i_wb_we == $past(i_wb_we));
if ((f_past_valid)&&(f_outstanding > 0))
`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
 
// Write requests must also set one (or more) of i_wb_sel
always @(posedge i_clk)
if ((i_wb_stb)&&(i_wb_we))
assert(|i_wb_sel);
// always @(*)
// if ((i_wb_stb)&&(i_wb_we))
// `SLAVE_ASSUME(|i_wb_sel);
 
 
//
237,17 → 246,34
// If CYC was low on the last clock, then both ACK and ERR should be
// low on this clock.
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_wb_cyc)))
if ((f_past_valid)&&(!$past(i_wb_cyc))&&(!i_wb_cyc))
begin
assume(!i_wb_ack);
assume(!i_wb_err);
`SLAVE_ASSERT(!i_wb_ack);
`SLAVE_ASSERT(!i_wb_err);
// Stall may still be true--such as when we are not
// selected at some arbiter between us and the slave
end
 
//
// Any time the CYC line drops, it is possible that there may be a
// remaining (registered) ACK or ERR that hasn't yet been returned.
// Restrict such out of band returns so that they are *only* returned
// if there is an outstanding operation.
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_cyc))&&(!i_wb_cyc))
begin
if (($past(f_outstanding == 0))
&&((!$past(i_wb_stb && !i_wb_stall))
||($past(i_wb_ack|i_wb_err))))
begin
`SLAVE_ASSERT(!i_wb_ack);
`SLAVE_ASSERT(!i_wb_err);
end
end
 
// ACK and ERR may never both be true at the same time
always @(*)
assume((!i_wb_ack)||(!i_wb_err));
`SLAVE_ASSERT((!i_wb_ack)||(!i_wb_err));
 
generate if (F_MAX_STALL > 0)
begin : MXSTALL
260,13 → 286,14
 
initial f_stall_count = 0;
always @(posedge i_clk)
if ((!i_reset)&&(i_wb_stb)&&(i_wb_stall))
f_stall_count <= f_stall_count + 1'b1;
else
f_stall_count <= 0;
always @(posedge i_clk)
if (i_wb_cyc)
assume(f_stall_count < F_MAX_STALL);
if ((!i_reset)&&(i_wb_stb)&&(i_wb_stall))
f_stall_count <= f_stall_count + 1'b1;
else
f_stall_count <= 0;
 
always @(*)
if (i_wb_cyc)
`SLAVE_ASSERT(f_stall_count < F_MAX_STALL);
end endgenerate
 
generate if (F_MAX_ACK_DELAY > 0)
280,13 → 307,18
 
initial f_ackwait_count = 0;
always @(posedge i_clk)
if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
&&(!i_wb_ack)&&(!i_wb_err))
begin
f_ackwait_count <= f_ackwait_count + 1'b1;
assume(f_ackwait_count < F_MAX_ACK_DELAY);
end else
f_ackwait_count <= 0;
if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
&&(!i_wb_ack)&&(!i_wb_err)
&&(f_outstanding > 0))
f_ackwait_count <= f_ackwait_count + 1'b1;
else
f_ackwait_count <= 0;
 
always @(*)
if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
&&(!i_wb_ack)&&(!i_wb_err)
&&(f_outstanding > 0))
`SLAVE_ASSERT(f_ackwait_count < F_MAX_ACK_DELAY);
end endgenerate
 
//
294,10 → 326,10
//
initial f_nreqs = 0;
always @(posedge i_clk)
if ((i_reset)||(!i_wb_cyc))
f_nreqs <= 0;
else if ((i_wb_stb)&&(!i_wb_stall))
f_nreqs <= f_nreqs + 1'b1;
if ((i_reset)||(!i_wb_cyc))
f_nreqs <= 0;
else if ((i_wb_stb)&&(!i_wb_stall))
f_nreqs <= f_nreqs + 1'b1;
 
 
//
305,10 → 337,12
//
initial f_nacks = 0;
always @(posedge i_clk)
if (!i_wb_cyc)
f_nacks <= 0;
else if ((i_wb_ack)||(i_wb_err))
f_nacks <= f_nacks + 1'b1;
if (i_reset)
f_nacks <= 0;
else if (!i_wb_cyc)
f_nacks <= 0;
else if ((i_wb_ack)||(i_wb_err))
f_nacks <= f_nacks + 1'b1;
 
//
// The number of outstanding requests is the difference between
316,38 → 350,37
//
assign f_outstanding = (i_wb_cyc) ? (f_nreqs - f_nacks):0;
 
always @(posedge i_clk)
if ((i_wb_cyc)&&(F_MAX_REQUESTS > 0))
begin
if (i_wb_stb)
assert(f_nreqs < F_MAX_REQUESTS);
else
assert(f_nreqs <= F_MAX_REQUESTS);
assume(f_nacks <= f_nreqs);
assert(f_outstanding < (1<<F_LGDEPTH)-1);
end else
assume(f_outstanding < (1<<F_LGDEPTH)-1);
always @(*)
if ((i_wb_cyc)&&(F_MAX_REQUESTS > 0))
begin
if (i_wb_stb)
`SLAVE_ASSUME(f_nreqs < F_MAX_REQUESTS);
else
`SLAVE_ASSUME(f_nreqs <= F_MAX_REQUESTS);
`SLAVE_ASSERT(f_nacks <= f_nreqs);
assert(f_outstanding < (1<<F_LGDEPTH)-1);
end else
assume(f_outstanding < (1<<F_LGDEPTH)-1);
 
always @(posedge i_clk)
if ((i_wb_cyc)&&(f_outstanding == 0))
always @(*)
if ((i_wb_cyc)&&(f_outstanding == 0))
begin
// If nothing is outstanding, then there should be
// no acknowledgements ... however, an acknowledgement
// *can* come back on the same clock as the stb is
// going out.
if (F_OPT_MINCLOCK_DELAY)
begin
// If nothing is outstanding, then there should be
// no acknowledgements
assume(!i_wb_ack);
// The same is not true of errors. It may be that an
// error is created before the request gets through
// assume(!i_wb_err);
`SLAVE_ASSERT(!i_wb_ack);
`SLAVE_ASSERT(!i_wb_err);
end else begin
`SLAVE_ASSERT((!i_wb_ack)||((i_wb_stb)&&(!i_wb_stall)));
// The same is true of errors. They may not be
// created before the request gets through
`SLAVE_ASSERT((!i_wb_err)||((i_wb_stb)&&(!i_wb_stall)));
end
end
 
// While the error signal may be asserted immediately before
// anything is outstanding, it may only be asserted in
// response to a transaction request--whether completed or
// not.
always @(posedge i_clk)
if ((!i_wb_stb)&&(f_outstanding == 0))
assume(!i_wb_err);
 
 
generate if (F_OPT_SOURCE)
begin : SRC
// Any opening bus request starts with both CYC and STB high
357,8 → 390,8
// the CYC line may go high or low without actually affecting
// the STB line of the slave.
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_wb_cyc))&&(i_wb_cyc))
assert(i_wb_stb);
if ((f_past_valid)&&(!$past(i_wb_cyc))&&(i_wb_cyc))
`SLAVE_ASSUME(i_wb_stb);
end endgenerate
 
 
367,9 → 400,9
// If we aren't waiting for anything, and we aren't issuing
// any requests, then then our transaction is over and we
// should be dropping the CYC line.
always @(posedge i_clk)
if (f_outstanding == 0)
assert((i_wb_stb)||(!i_wb_cyc));
always @(*)
if (f_outstanding == 0)
`SLAVE_ASSUME((i_wb_stb)||(!i_wb_cyc));
// Not all masters will abide by this restriction. Some
// masters may wish to implement read-modify-write bus
// interactions. These masters need to keep CYC high between
392,10 → 425,10
begin
if (!i_wb_cyc)
begin
restrict(!i_wb_stall);
restrict($stable(i_wb_idata));
assume(!i_wb_stall);
assume($stable(i_wb_idata));
end else if ((!$past(i_wb_ack))&&(!i_wb_ack))
restrict($stable(i_wb_idata));
assume($stable(i_wb_idata));
end
end endgenerate
 
410,8 → 443,8
// necessary, and the spec doesn't disallow them. Hence we
// make this check optional.
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(i_wb_stb)))
assert(!i_wb_stb);
if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(i_wb_stb)))
`SLAVE_ASSUME(!i_wb_stb);
end endgenerate
 
endmodule
/fwb_slave.v
23,35 → 23,44
// master outputs (slave inputs)), and assumptions are made about the
// master inputs (the slave outputs).
//
// In order to make it easier to compare the slave against the master,
// assumptions with respect to the slave have been marked with the
// `SLAVE_ASSUME macro. Similarly, assertions the slave would make have
// been marked with `SLAVE_ASSERT. This allows the master to redefine
// these two macros to be from his perspective, and therefore the
// diffs between the two files actually show true differences, rather
// than just these differences in perspective.
//
//
//
// Creator: Dan Gisselquist, Ph.D.
// Gisselquist Technology, LLC
//
////////////////////////////////////////////////////////////////////////////////
//
// Copyright (C) 2017, Gisselquist Technology, LLC
// Copyright (C) 2017-2018, 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
// by the Free Software Foundation, either version 3 of the License, or (at
// your option) any later version.
// This file is part of the pipelined Wishbone to AXI converter project, a
// project that contains multiple bus bridging designs and formal bus property
// sets.
//
// This program is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
// for more details.
// The bus bridge designs and property sets are free RTL designs: you can
// redistribute them and/or modify any of them under the terms of the GNU
// Lesser General Public License as published by the Free Software Foundation,
// either version 3 of the License, or (at your option) any later version.
//
// You should have received a copy of the GNU General Public License along
// with this program. (It's in the $(ROOT)/doc directory. Run make with no
// target there if the PDF file isn't present.) If not, see
// The bus bridge designs and property sets are distributed in the hope that
// they will be useful, but WITHOUT ANY WARRANTY; without even the implied
// warranty of MERCHANTIBILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with these designs. (It's in the $(ROOT)/doc directory. Run make
// with no target there if the PDF file isn't present.) If not, see
// <http://www.gnu.org/licenses/> for a copy.
//
// License: GPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/gpl.html
// License: LGPL, v3, as defined and found on www.gnu.org,
// http://www.gnu.org/licenses/lgpl.html
//
//
////////////////////////////////////////////////////////////////////////////////
//
//
81,6 → 90,14
parameter [0:0] F_OPT_DISCONTINUOUS = 0;
//
//
// If true, insist that there be a minimum of a single clock delay
// between request and response. This defaults to off since the
// wishbone specification specifically doesn't require this. However,
// some interfaces do, so we allow it as an option here.
parameter [0:0] F_OPT_MINCLOCK_DELAY = 0;
//
//
//
localparam [(F_LGDEPTH-1):0] MAX_OUTSTANDING = {(F_LGDEPTH){1'b1}};
localparam MAX_DELAY = (F_MAX_STALL > F_MAX_ACK_DELAY)
? F_MAX_STALL : F_MAX_ACK_DELAY;
109,10 → 126,12
output reg [(F_LGDEPTH-1):0] f_nreqs, f_nacks;
output wire [(F_LGDEPTH-1):0] f_outstanding;
 
`define SLAVE_ASSUME assume
`define SLAVE_ASSERT assert
//
// Let's just make sure our parameters are set up right
//
assert property(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});
initial assert(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}});
 
//
// Wrap the request line in a bundle. The top bit, named STB_BIT,
131,8 → 150,8
always @(posedge i_clk)
f_past_valid <= 1'b1;
always @(*)
if (!f_past_valid)
assume(i_reset);
if (!f_past_valid)
`SLAVE_ASSUME(i_reset);
//
//
// Assertions regarding the initial (and reset) state
141,40 → 160,26
 
//
// Assume we start from a reset condition
initial assume(i_reset);
initial assume(!i_wb_cyc);
initial assume(!i_wb_stb);
initial assert(i_reset);
initial `SLAVE_ASSUME(!i_wb_cyc);
initial `SLAVE_ASSUME(!i_wb_stb);
//
initial assert(!i_wb_ack);
initial assert(!i_wb_err);
initial `SLAVE_ASSERT(!i_wb_ack);
initial `SLAVE_ASSERT(!i_wb_err);
 
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_reset)))
if ((!f_past_valid)||($past(i_reset)))
begin
assume(!i_wb_cyc);
assume(!i_wb_stb);
`SLAVE_ASSUME(!i_wb_cyc);
`SLAVE_ASSUME(!i_wb_stb);
//
assert(!i_wb_ack);
assert(!i_wb_err);
`SLAVE_ASSERT(!i_wb_ack);
`SLAVE_ASSERT(!i_wb_err);
end
 
// Things can only change on the positive edge of the clock
always @($global_clock)
if ((f_past_valid)&&(!$rose(i_clk)))
begin
assume($stable(i_reset));
assume($stable(i_wb_cyc));
assume($stable(f_request));
if (i_wb_we)
assume($stable(f_request)); // The entire request should b stabl
else
assume($stable(f_request[(2+AW-1):(DW+DW/8)]));
//
assert($stable(i_wb_ack));
assert($stable(i_wb_stall));
assert($stable(i_wb_idata));
assert($stable(i_wb_err));
end
always @(*)
if (!f_past_valid)
`SLAVE_ASSUME(!i_wb_cyc);
 
//
//
186,12 → 191,12
// the transaction
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_wb_err))&&($past(i_wb_cyc)))
assume(!i_wb_cyc);
`SLAVE_ASSUME(!i_wb_cyc);
 
// STB can only be true if CYC is also true
always @(posedge i_clk)
if (i_wb_stb)
assume(i_wb_cyc);
always @(*)
if (i_wb_stb)
`SLAVE_ASSUME(i_wb_cyc);
 
// If a request was both outstanding and stalled on the last clock,
// then nothing should change on this clock regarding it.
199,27 → 204,31
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
&&($past(i_wb_stall))&&(i_wb_cyc))
begin
assume(i_wb_stb);
assume($stable(f_request));
`SLAVE_ASSUME(i_wb_stb);
`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
`SLAVE_ASSUME(i_wb_addr == $past(i_wb_addr));
`SLAVE_ASSUME(i_wb_sel == $past(i_wb_sel));
if (i_wb_we)
`SLAVE_ASSUME(i_wb_data == $past(i_wb_data));
end
 
// Within any series of STB/requests, the direction of the request
// may not change.
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_wb_stb))&&(i_wb_stb))
assume(i_wb_we == $past(i_wb_we));
if ((f_past_valid)&&($past(i_wb_stb))&&(i_wb_stb))
`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
 
 
// Within any given bus cycle, the direction may *only* change when
// there are no further outstanding requests.
always @(posedge i_clk)
if ((f_past_valid)&&(f_outstanding > 0))
assume(i_wb_we == $past(i_wb_we));
if ((f_past_valid)&&(f_outstanding > 0))
`SLAVE_ASSUME(i_wb_we == $past(i_wb_we));
 
// Write requests must also set one (or more) of i_wb_sel
always @(posedge i_clk)
if ((i_wb_stb)&&(i_wb_we))
assume(|i_wb_sel);
// always @(*)
// if ((i_wb_stb)&&(i_wb_we))
// `SLAVE_ASSUME(|i_wb_sel);
 
 
//
231,17 → 240,29
// If CYC was low on the last clock, then both ACK and ERR should be
// low on this clock.
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_wb_cyc)))
if ((f_past_valid)&&(!$past(i_wb_cyc))&&(!i_wb_cyc))
begin
assert(!i_wb_ack);
assert(!i_wb_err);
`SLAVE_ASSERT(!i_wb_ack);
`SLAVE_ASSERT(!i_wb_err);
// Stall may still be true--such as when we are not
// selected at some arbiter between us and the slave
end
 
always @(posedge i_clk)
if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_cyc))&&(!i_wb_cyc))
begin
if (($past(f_outstanding == 0))
&&((!$past(i_wb_stb && !i_wb_stall))
||($past(i_wb_ack|i_wb_err))))
begin
`SLAVE_ASSERT(!i_wb_ack);
`SLAVE_ASSERT(!i_wb_err);
end
end
 
// ACK and ERR may never both be true at the same time
always @(*)
assume((!i_wb_ack)||(!i_wb_err));
`SLAVE_ASSERT((!i_wb_ack)||(!i_wb_err));
 
generate if (F_MAX_STALL > 0)
begin : MXSTALL
254,13 → 275,14
 
initial f_stall_count = 0;
always @(posedge i_clk)
if ((!i_reset)&&(i_wb_stb)&&(i_wb_stall))
f_stall_count <= f_stall_count + 1'b1;
else
f_stall_count <= 0;
always @(posedge i_clk)
if (i_wb_cyc)
assert(f_stall_count < F_MAX_STALL);
if ((!i_reset)&&(i_wb_stb)&&(i_wb_stall))
f_stall_count <= f_stall_count + 1'b1;
else
f_stall_count <= 0;
 
always @(*)
if (i_wb_cyc)
`SLAVE_ASSERT(f_stall_count < F_MAX_STALL);
end endgenerate
 
generate if (F_MAX_ACK_DELAY > 0)
274,13 → 296,18
 
initial f_ackwait_count = 0;
always @(posedge i_clk)
if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
&&(!i_wb_ack)&&(!i_wb_err))
begin
f_ackwait_count <= f_ackwait_count + 1'b1;
assert(f_ackwait_count < F_MAX_ACK_DELAY);
end else
f_ackwait_count <= 0;
if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
&&(!i_wb_ack)&&(!i_wb_err)
&&(f_outstanding > 0))
f_ackwait_count <= f_ackwait_count + 1'b1;
else
f_ackwait_count <= 0;
 
always @(*)
if ((!i_reset)&&(i_wb_cyc)&&(!i_wb_stb)
&&(!i_wb_ack)&&(!i_wb_err)
&&(f_outstanding > 0))
`SLAVE_ASSERT(f_ackwait_count < F_MAX_ACK_DELAY);
end endgenerate
 
//
288,10 → 315,10
//
initial f_nreqs = 0;
always @(posedge i_clk)
if ((i_reset)||(!i_wb_cyc))
f_nreqs <= 0;
else if ((i_wb_stb)&&(!i_wb_stall))
f_nreqs <= f_nreqs + 1'b1;
if ((i_reset)||(!i_wb_cyc))
f_nreqs <= 0;
else if ((i_wb_stb)&&(!i_wb_stall))
f_nreqs <= f_nreqs + 1'b1;
 
 
//
299,10 → 326,12
//
initial f_nacks = 0;
always @(posedge i_clk)
if (!i_wb_cyc)
f_nacks <= 0;
else if ((i_wb_ack)||(i_wb_err))
f_nacks <= f_nacks + 1'b1;
if (i_reset)
f_nacks <= 0;
else if (!i_wb_cyc)
f_nacks <= 0;
else if ((i_wb_ack)||(i_wb_err))
f_nacks <= f_nacks + 1'b1;
 
//
// The number of outstanding requests is the difference between
310,45 → 339,45
//
assign f_outstanding = (i_wb_cyc) ? (f_nreqs - f_nacks):0;
 
always @(posedge i_clk)
if ((i_wb_cyc)&&(F_MAX_REQUESTS > 0))
begin
if (i_wb_stb)
assume(f_nreqs < F_MAX_REQUESTS);
else
assume(f_nreqs <= F_MAX_REQUESTS);
assert(f_nacks <= f_nreqs);
assert(f_outstanding < (1<<F_LGDEPTH)-1);
end else
assert(f_outstanding < (1<<F_LGDEPTH)-1);
always @(*)
if ((i_wb_cyc)&&(F_MAX_REQUESTS > 0))
begin
if (i_wb_stb)
`SLAVE_ASSUME(f_nreqs < F_MAX_REQUESTS);
else
`SLAVE_ASSUME(f_nreqs <= F_MAX_REQUESTS);
`SLAVE_ASSERT(f_nacks <= f_nreqs);
assert(f_outstanding < (1<<F_LGDEPTH)-1);
end else
assume(f_outstanding < (1<<F_LGDEPTH)-1);
 
always @(posedge i_clk)
if ((i_wb_cyc)&&(f_outstanding == 0))
always @(*)
if ((i_wb_cyc)&&(f_outstanding == 0))
begin
// If nothing is outstanding, then there should be
// no acknowledgements ... however, an acknowledgement
// *can* come back on the same clock as the stb is
// going out.
if (F_OPT_MINCLOCK_DELAY)
begin
// If nothing is outstanding, then there should be
// no acknowledgements
assert(!i_wb_ack);
// The same is not true of errors. It may be that an
// error is created before the request gets through
// assert(!i_wb_err);
`SLAVE_ASSERT(!i_wb_ack);
`SLAVE_ASSERT(!i_wb_err);
end else begin
`SLAVE_ASSERT((!i_wb_ack)||((i_wb_stb)&&(!i_wb_stall)));
// The same is true of errors. They may not be
// created before the request gets through
`SLAVE_ASSERT((!i_wb_err)||((i_wb_stb)&&(!i_wb_stall)));
end
end
 
// While the error signal may be asserted immediately before
// anything is outstanding, it may only be asserted in
// response to a transaction request--whether completed or
// not.
always @(posedge i_clk)
if ((i_wb_cyc)&&(!i_wb_stb)&&(f_outstanding == 0))
assert(!i_wb_err);
 
generate if (!F_OPT_RMW_BUS_OPTION)
begin
// If we aren't waiting for anything, and we aren't issuing
// any requests, then then our transaction is over and we
// should be dropping the CYC line.
always @(posedge i_clk)
if (f_outstanding == 0)
assume((i_wb_stb)||(!i_wb_cyc));
always @(*)
if (f_outstanding == 0)
`SLAVE_ASSUME((i_wb_stb)||(!i_wb_cyc));
// Not all masters will abide by this restriction. Some
// masters may wish to implement read-modify-write bus
// interactions. These masters need to keep CYC high between
367,8 → 396,8
// necessary, and the spec doesn't disallow them. Hence we
// make this check optional.
always @(posedge i_clk)
if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(i_wb_stb)))
assume(!i_wb_stb);
if ((f_past_valid)&&($past(i_wb_cyc))&&(!$past(i_wb_stb)))
`SLAVE_ASSUME(!i_wb_stb);
end endgenerate
 
endmodule
/wbarbiter.gtkw
0,0 → 1,72
[*]
[*] GTKWave Analyzer v3.3.86 (w)1999-2017 BSI
[*] Fri Dec 28 02:53:33 2018
[*]
[dumpfile] "/home/dan/jericho/work/rnd/opencores/wb2axip/trunk/bench/formal/wbarbiter_cvr/engine_0/trace4.vcd"
[dumpfile_mtime] "Fri Dec 28 02:48:56 2018"
[dumpfile_size] 13681
[savefile] "/home/dan/jericho/work/rnd/opencores/wb2axip/trunk/bench/formal/wbarbiter.gtkw"
[timestart] 0
[size] 1441 600
[pos] -1 -1
*-4.552812 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 270
[signals_width] 160
[sst_expanded] 1
[sst_vpaned_height] 143
@28
wbarbiter.i_clk
wbarbiter.i_reset
@200
-
@28
wbarbiter.i_a_cyc
wbarbiter.i_a_stb
wbarbiter.i_a_we
@22
wbarbiter.i_a_adr[31:0]
wbarbiter.i_a_dat[31:0]
wbarbiter.i_a_sel[3:0]
@29
[color] 2
wbarbiter.o_a_stall
[color] 2
wbarbiter.o_a_ack
[color] 2
wbarbiter.o_a_err
@200
-
@28
wbarbiter.i_b_cyc
wbarbiter.i_b_stb
wbarbiter.i_b_we
@22
wbarbiter.i_b_adr[31:0]
wbarbiter.i_b_dat[31:0]
wbarbiter.i_b_sel[3:0]
@28
[color] 2
wbarbiter.o_b_stall
[color] 2
wbarbiter.o_b_ack
[color] 2
wbarbiter.o_b_err
@200
-
@28
wbarbiter.o_cyc
wbarbiter.o_stb
wbarbiter.o_we
@22
wbarbiter.o_adr[31:0]
wbarbiter.o_dat[31:0]
wbarbiter.o_sel[3:0]
@28
[color] 2
wbarbiter.i_ack
[color] 2
wbarbiter.i_stall
[color] 2
wbarbiter.i_err
[pattern_trace] 1
[pattern_trace] 0
/wbarbiter.sby
0,0 → 1,23
[tasks]
prf
cvr
 
[options]
prf: mode prove
prf: depth 4
cvr: mode cover
cvr: depth 32
 
[engines]
smtbmc
 
[script]
read -formal -D WBARBITER wbarbiter.v
read -formal -D WBARBITER fwb_slave.v
read -formal -D WBARBITER fwb_master.v
prep -top wbarbiter
 
[files]
../../rtl/wbarbiter.v
fwb_slave.v
fwb_master.v
/wbm2axilite.sby
0,0 → 1,23
[tasks]
prf
cvr
 
[options]
prf: mode prove
prf: depth 18
cvr: mode cover
cvr: depth 32
 
[engines]
smtbmc
 
[script]
read -formal -D AXILRD2WBSP wbm2axilite.v
read -formal -D AXILRD2WBSP faxil_master.v
read -formal -D AXILRD2WBSP fwb_slave.v
prep -top wbm2axilite
 
[files]
../../rtl/wbm2axilite.v
faxil_master.v
fwb_slave.v
/wbm2axisp.ys
2,6 → 2,5
read_verilog -D WBM2AXISP -formal faxi_master.v
read_verilog -D WBM2AXISP -formal fwb_slave.v
prep -top wbm2axisp -nordff
clk2fflogic
opt -share_all
write_smt2 -wires wbm2axisp.smt2
/wbxbar.sby
0,0 → 1,69
[tasks]
prf4x8_buflp nxm opt_dblbuffer opt_lowpower
prf4x8_buf nxm opt_dblbuffer
prf4x8_lp nxm opt_lowpower
prf4x8_cheap nxm
prf4x8_buflpko nxm opt_dblbuffer opt_lowpower opt_timeout
prf4x8_bufko nxm opt_dblbuffer opt_timeout
prf4x8_lpko nxm opt_lowpower opt_timeout
prf4x8_cheapko nxm opt_timeout
prf4x8_buflpkos nxm opt_dblbuffer opt_lowpower opt_timeout opt_starvation
prf4x8_bufkos nxm opt_dblbuffer opt_timeout opt_starvation
prf4x8_lpkos nxm opt_lowpower opt_timeout opt_starvation
prf4x8_cheapkos nxm opt_timeout opt_starvation
prf1x8_buflp oxm opt_dblbuffer opt_lowpower
prf1x8_buf oxm opt_dblbuffer
prf1x8_lp oxm opt_lowpower
prf1x8_cheap oxm
prf1x8_buflpko oxm opt_dblbuffer opt_lowpower opt_timeout
prf4x8_bufko oxm opt_dblbuffer opt_timeout
prf1x8_lpko oxm opt_lowpower opt_timeout
prf1x8_cheapko oxm opt_timeout
prf1x8_buflpkos oxm opt_dblbuffer opt_lowpower opt_timeout opt_starvation
prf1x8_bufkos oxm opt_dblbuffer opt_timeout opt_starvation
prf1x8_lpkos oxm opt_lowpower opt_timeout opt_starvation
prf1x8_cheapkos oxm opt_timeout opt_starvation
prf4x1_buflp nxo opt_dblbuffer opt_lowpower
prf4x1_buf nxo opt_dblbuffer
prf4x1_lp nxo opt_lowpower
prf4x1_cheap nxo
prf4x1_buflpko nxo opt_dblbuffer opt_lowpower opt_timeout
prf4x1_bufko nxo opt_dblbuffer opt_timeout
prf4x1_lpko nxo opt_lowpower opt_timeout
prf4x1_cheapko nxo opt_timeout
prf4x1_buflpkos nxo opt_dblbuffer opt_lowpower opt_timeout opt_starvation
prf4x1_bufkos nxo opt_dblbuffer opt_timeout opt_starvation
prf4x1_lpkos nxo opt_lowpower opt_timeout opt_starvation
prf4x1_cheapkos nxo opt_timeout opt_starvation
 
[options]
mode prove
depth 5
 
[engines]
# smtbmc boolector
smtbmc
# smtbmc z3
 
 
[script]
read -formal wbxbar.v
read -formal fwb_slave.v
read -formal fwb_master.v
nxm: chparam -set NM 4 -set NS 8 wbxbar
oxm: chparam -set NM 1 -set NS 8 wbxbar
nxo: chparam -set NM 4 -set NS 1 wbxbar
opt_dblbuffer: chparam -set OPT_DBLBUFFER 1 wbxbar
~opt_dblbuffer: chparam -set OPT_DBLBUFFER 0 wbxbar
opt_lowpower: chparam -set OPT_LOWPOWER 1 wbxbar
~opt_lowpower: chparam -set OPT_LOWPOWER 0 wbxbar
opt_timeout: chparam -set OPT_TIMEOUT 20 wbxbar
~opt_timeout: chparam -set OPT_TIMEOUT 0 wbxbar
opt_starvation: chparam -set OPT_STARVATION_TIMEOUT 1 wbxbar
~opt_starvation: chparam -set OPT_TIMEOUT 0 wbxbar
prep -top wbxbar
 
[files]
../../rtl/wbxbar.v
fwb_slave.v
fwb_master.v
/xlnxdemo.gtkw
0,0 → 1,62
[*]
[*] GTKWave Analyzer v3.3.66 (w)1999-2015 BSI
[*] Thu Dec 27 16:19:38 2018
[*]
[dumpfile] "/home/dan/work/rnd/opencores/wb2axip/trunk/bench/formal/xlnxdemo_cvr/engine_0/trace19.vcd"
[dumpfile_mtime] "Thu Dec 27 03:40:12 2018"
[dumpfile_size] 68959
[savefile] "/home/dan/work/rnd/opencores/wb2axip/trunk/bench/formal/xlnxdemo.gtkw"
[timestart] 0
[size] 1473 600
[pos] -474 -1
*-6.470208 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 196
[signals_width] 166
[sst_expanded] 1
[sst_vpaned_height] 155
@29
[color] 3
xlnxdemo.S_AXI_ARESETN
[color] 3
xlnxdemo.S_AXI_ACLK
@200
-
@28
xlnxdemo.S_AXI_AWVALID
xlnxdemo.S_AXI_AWREADY
@22
xlnxdemo.S_AXI_AWADDR[6:0]
@200
-
@28
xlnxdemo.S_AXI_WVALID
xlnxdemo.S_AXI_WREADY
@22
xlnxdemo.S_AXI_WSTRB[3:0]
xlnxdemo.S_AXI_WDATA[31:0]
@200
-
@28
[color] 2
xlnxdemo.S_AXI_BVALID
[color] 2
xlnxdemo.S_AXI_BREADY
@200
-
@28
xlnxdemo.S_AXI_ARVALID
xlnxdemo.S_AXI_ARREADY
@22
xlnxdemo.S_AXI_ARADDR[6:0]
@200
-
@28
[color] 2
xlnxdemo.S_AXI_RVALID
[color] 2
xlnxdemo.S_AXI_RREADY
@22
[color] 2
xlnxdemo.S_AXI_RDATA[31:0]
[pattern_trace] 1
[pattern_trace] 0
/xlnxdemo.sby
0,0 → 1,21
[tasks]
cvr
prf
 
[options]
cvr: mode cover
cvr: depth 60
prf: mode prove
prf: depth 40
 
[engines]
smtbmc
 
[script]
read -formal xlnxdemo.v
read -formal faxil_slave.v
prep -top xlnxdemo
 
[files]
xlnxdemo.v
faxil_slave.v
/xlnxdemo.v
0,0 → 1,1075
`default_nettype none // Added to the raw demo
`timescale 1 ns / 1 ps
//
module xlnxdemo #
(
// Users to add parameters here
 
// User parameters ends
// Do not modify the parameters beyond this line
 
// Width of S_AXI data bus
parameter integer C_S_AXI_DATA_WIDTH = 32,
// Width of S_AXI address bus
parameter integer C_S_AXI_ADDR_WIDTH = 7
)
(
// Users to add ports here
 
// User ports ends
// Do not modify the ports beyond this line
 
// Global Clock Signal
input wire S_AXI_ACLK,
// Global Reset Signal. This Signal is Active LOW
input wire S_AXI_ARESETN,
// Write address (issued by master, acceped by Slave)
input wire [C_S_AXI_ADDR_WIDTH-1 : 0] S_AXI_AWADDR,
// Write channel Protection type. This signal indicates the
// privilege and security level of the transaction, and whether
// the transaction is a data access or an instruction access.
input wire [2 : 0] S_AXI_AWPROT,
// Write address valid. This signal indicates that the master signaling
// valid write address and control information.
input wire S_AXI_AWVALID,
// Write address ready. This signal indicates that the slave is ready
// to accept an address and associated control signals.
output wire S_AXI_AWREADY,
// Write data (issued by master, acceped by Slave)
input wire [C_S_AXI_DATA_WIDTH-1 : 0] S_AXI_WDATA,
// Write strobes. This signal indicates which byte lanes hold
// valid data. There is one write strobe bit for each eight
// bits of the write data bus.
input wire [(C_S_AXI_DATA_WIDTH/8)-1 : 0] S_AXI_WSTRB,
// Write valid. This signal indicates that valid write
// data and strobes are available.
input wire S_AXI_WVALID,
// Write ready. This signal indicates that the slave
// can accept the write data.
output wire S_AXI_WREADY,
// Write response. This signal indicates the status
// of the write transaction.
output wire [1 : 0] S_AXI_BRESP,
// Write response valid. This signal indicates that the channel
// is signaling a valid write response.
output wire S_AXI_BVALID,
// Response ready. This signal indicates that the master
// can accept a write response.
input wire S_AXI_BREADY,
// Read address (issued by master, acceped by Slave)
input wire [C_S_AXI_ADDR_WIDTH-1 : 0] S_AXI_ARADDR,
// Protection type. This signal indicates the privilege
// and security level of the transaction, and whether the
// transaction is a data access or an instruction access.
input wire [2 : 0] S_AXI_ARPROT,
// Read address valid. This signal indicates that the channel
// is signaling valid read address and control information.
input wire S_AXI_ARVALID,
// Read address ready. This signal indicates that the slave is
// ready to accept an address and associated control signals.
output wire S_AXI_ARREADY,
// Read data (issued by slave)
output wire [C_S_AXI_DATA_WIDTH-1 : 0] S_AXI_RDATA,
// Read response. This signal indicates the status of the
// read transfer.
output wire [1 : 0] S_AXI_RRESP,
// Read valid. This signal indicates that the channel is
// signaling the required read data.
output wire S_AXI_RVALID,
// Read ready. This signal indicates that the master can
// accept the read data and response information.
input wire S_AXI_RREADY
);
 
// AXI4LITE signals
reg [C_S_AXI_ADDR_WIDTH-1 : 0] axi_awaddr;
reg axi_awready;
reg axi_wready;
reg [1 : 0] axi_bresp;
reg axi_bvalid;
reg [C_S_AXI_ADDR_WIDTH-1 : 0] axi_araddr;
reg axi_arready;
reg [C_S_AXI_DATA_WIDTH-1 : 0] axi_rdata;
reg [1 : 0] axi_rresp;
reg axi_rvalid;
 
// Example-specific design signals
// local parameter for addressing 32 bit / 64 bit C_S_AXI_DATA_WIDTH
// ADDR_LSB is used for addressing 32/64 bit registers/memories
// ADDR_LSB = 2 for 32 bits (n downto 2)
// ADDR_LSB = 3 for 64 bits (n downto 3)
localparam integer ADDR_LSB = (C_S_AXI_DATA_WIDTH/32) + 1;
localparam integer OPT_MEM_ADDR_BITS = 4;
//----------------------------------------------
//-- Signals for user logic register space example
//------------------------------------------------
//-- Number of Slave Registers 32
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg0;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg1;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg2;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg3;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg4;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg5;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg6;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg7;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg8;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg9;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg10;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg11;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg12;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg13;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg14;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg15;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg16;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg17;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg18;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg19;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg20;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg21;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg22;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg23;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg24;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg25;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg26;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg27;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg28;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg29;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg30;
reg [C_S_AXI_DATA_WIDTH-1:0] slv_reg31;
wire slv_reg_rden;
wire slv_reg_wren;
reg [C_S_AXI_DATA_WIDTH-1:0] reg_data_out;
integer byte_index;
 
// I/O Connections assignments
 
assign S_AXI_AWREADY = axi_awready;
assign S_AXI_WREADY = axi_wready;
assign S_AXI_BRESP = axi_bresp;
assign S_AXI_BVALID = axi_bvalid;
assign S_AXI_ARREADY = axi_arready;
assign S_AXI_RDATA = axi_rdata;
assign S_AXI_RRESP = axi_rresp;
assign S_AXI_RVALID = axi_rvalid;
// Implement axi_awready generation
// axi_awready is asserted for one S_AXI_ACLK clock cycle when both
// S_AXI_AWVALID and S_AXI_WVALID are asserted. axi_awready is
// de-asserted when reset is low.
 
always @( posedge S_AXI_ACLK )
begin
if ( S_AXI_ARESETN == 1'b0 )
begin
axi_awready <= 1'b0;
end
else
begin
if (~axi_awready && S_AXI_AWVALID && S_AXI_WVALID)
begin
// slave is ready to accept write address when
// there is a valid write address and write data
// on the write address and data bus. This design
// expects no outstanding transactions.
axi_awready <= 1'b1;
end
else
begin
axi_awready <= 1'b0;
end
end
end
 
// Implement axi_awaddr latching
// This process is used to latch the address when both
// S_AXI_AWVALID and S_AXI_WVALID are valid.
 
always @( posedge S_AXI_ACLK )
begin
if ( S_AXI_ARESETN == 1'b0 )
begin
axi_awaddr <= 0;
end
else
begin
if (~axi_awready && S_AXI_AWVALID && S_AXI_WVALID)
begin
// Write Address latching
axi_awaddr <= S_AXI_AWADDR;
end
end
end
 
// Implement axi_wready generation
// axi_wready is asserted for one S_AXI_ACLK clock cycle when both
// S_AXI_AWVALID and S_AXI_WVALID are asserted. axi_wready is
// de-asserted when reset is low.
 
always @( posedge S_AXI_ACLK )
begin
if ( S_AXI_ARESETN == 1'b0 )
begin
axi_wready <= 1'b0;
end
else
begin
if (~axi_wready && S_AXI_WVALID && S_AXI_AWVALID)
begin
// slave is ready to accept write data when
// there is a valid write address and write data
// on the write address and data bus. This design
// expects no outstanding transactions.
axi_wready <= 1'b1;
end
else
begin
axi_wready <= 1'b0;
end
end
end
 
// Implement memory mapped register select and write logic generation
// The write data is accepted and written to memory mapped registers when
// axi_awready, S_AXI_WVALID, axi_wready and S_AXI_WVALID are asserted. Write strobes are used to
// select byte enables of slave registers while writing.
// These registers are cleared when reset (active low) is applied.
// Slave register write enable is asserted when valid address and data are available
// and the slave is ready to accept the write address and write data.
assign slv_reg_wren = axi_wready && S_AXI_WVALID && axi_awready && S_AXI_AWVALID;
 
always @( posedge S_AXI_ACLK )
begin
if ( S_AXI_ARESETN == 1'b0 )
begin
slv_reg0 <= 0;
slv_reg1 <= 0;
slv_reg2 <= 0;
slv_reg3 <= 0;
slv_reg4 <= 0;
slv_reg5 <= 0;
slv_reg6 <= 0;
slv_reg7 <= 0;
slv_reg8 <= 0;
slv_reg9 <= 0;
slv_reg10 <= 0;
slv_reg11 <= 0;
slv_reg12 <= 0;
slv_reg13 <= 0;
slv_reg14 <= 0;
slv_reg15 <= 0;
slv_reg16 <= 0;
slv_reg17 <= 0;
slv_reg18 <= 0;
slv_reg19 <= 0;
slv_reg20 <= 0;
slv_reg21 <= 0;
slv_reg22 <= 0;
slv_reg23 <= 0;
slv_reg24 <= 0;
slv_reg25 <= 0;
slv_reg26 <= 0;
slv_reg27 <= 0;
slv_reg28 <= 0;
slv_reg29 <= 0;
slv_reg30 <= 0;
slv_reg31 <= 0;
end
else begin
if (slv_reg_wren)
begin
case ( axi_awaddr[ADDR_LSB+OPT_MEM_ADDR_BITS:ADDR_LSB] )
5'h00:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 0
slv_reg0[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h01:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 1
slv_reg1[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h02:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 2
slv_reg2[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h03:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 3
slv_reg3[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h04:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 4
slv_reg4[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h05:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 5
slv_reg5[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h06:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 6
slv_reg6[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h07:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 7
slv_reg7[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h08:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 8
slv_reg8[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h09:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 9
slv_reg9[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h0A:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 10
slv_reg10[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h0B:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 11
slv_reg11[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h0C:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 12
slv_reg12[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h0D:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 13
slv_reg13[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h0E:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 14
slv_reg14[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h0F:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 15
slv_reg15[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h10:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 16
slv_reg16[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h11:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 17
slv_reg17[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h12:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 18
slv_reg18[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h13:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 19
slv_reg19[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h14:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 20
slv_reg20[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h15:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 21
slv_reg21[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h16:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 22
slv_reg22[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h17:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 23
slv_reg23[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h18:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 24
slv_reg24[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h19:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 25
slv_reg25[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h1A:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 26
slv_reg26[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h1B:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 27
slv_reg27[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h1C:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 28
slv_reg28[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h1D:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 29
slv_reg29[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h1E:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 30
slv_reg30[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
5'h1F:
for ( byte_index = 0; byte_index <= (C_S_AXI_DATA_WIDTH/8)-1; byte_index = byte_index+1 )
if ( S_AXI_WSTRB[byte_index] == 1 ) begin
// Respective byte enables are asserted as per write strobes
// Slave register 31
slv_reg31[(byte_index*8) +: 8] <= S_AXI_WDATA[(byte_index*8) +: 8];
end
default : begin
slv_reg0 <= slv_reg0;
slv_reg1 <= slv_reg1;
slv_reg2 <= slv_reg2;
slv_reg3 <= slv_reg3;
slv_reg4 <= slv_reg4;
slv_reg5 <= slv_reg5;
slv_reg6 <= slv_reg6;
slv_reg7 <= slv_reg7;
slv_reg8 <= slv_reg8;
slv_reg9 <= slv_reg9;
slv_reg10 <= slv_reg10;
slv_reg11 <= slv_reg11;
slv_reg12 <= slv_reg12;
slv_reg13 <= slv_reg13;
slv_reg14 <= slv_reg14;
slv_reg15 <= slv_reg15;
slv_reg16 <= slv_reg16;
slv_reg17 <= slv_reg17;
slv_reg18 <= slv_reg18;
slv_reg19 <= slv_reg19;
slv_reg20 <= slv_reg20;
slv_reg21 <= slv_reg21;
slv_reg22 <= slv_reg22;
slv_reg23 <= slv_reg23;
slv_reg24 <= slv_reg24;
slv_reg25 <= slv_reg25;
slv_reg26 <= slv_reg26;
slv_reg27 <= slv_reg27;
slv_reg28 <= slv_reg28;
slv_reg29 <= slv_reg29;
slv_reg30 <= slv_reg30;
slv_reg31 <= slv_reg31;
end
endcase
end
end
end
 
// Implement write response logic generation
// The write response and response valid signals are asserted by the slave
// when axi_wready, S_AXI_WVALID, axi_wready and S_AXI_WVALID are asserted.
// This marks the acceptance of address and indicates the status of
// write transaction.
 
always @( posedge S_AXI_ACLK )
begin
if ( S_AXI_ARESETN == 1'b0 )
begin
axi_bvalid <= 0;
axi_bresp <= 2'b0;
end
else
begin
if (axi_awready && S_AXI_AWVALID && ~axi_bvalid && axi_wready && S_AXI_WVALID)
begin
// indicates a valid write response is available
axi_bvalid <= 1'b1;
axi_bresp <= 2'b0; // 'OKAY' response
end // work error responses in future
else
begin
if (S_AXI_BREADY && axi_bvalid)
//check if bready is asserted while bvalid is high)
//(there is a possibility that bready is always asserted high)
begin
axi_bvalid <= 1'b0;
end
end
end
end
 
// Implement axi_arready generation
// axi_arready is asserted for one S_AXI_ACLK clock cycle when
// S_AXI_ARVALID is asserted. axi_awready is
// de-asserted when reset (active low) is asserted.
// The read address is also latched when S_AXI_ARVALID is
// asserted. axi_araddr is reset to zero on reset assertion.
 
always @( posedge S_AXI_ACLK )
begin
if ( S_AXI_ARESETN == 1'b0 )
begin
axi_arready <= 1'b0;
axi_araddr <= 7'b0;
end
else
begin
if (~axi_arready && S_AXI_ARVALID)
begin
// indicates that the slave has acceped the valid read address
axi_arready <= 1'b1;
// Read address latching
axi_araddr <= S_AXI_ARADDR;
end
else
begin
axi_arready <= 1'b0;
end
end
end
 
// Implement axi_arvalid generation
// axi_rvalid is asserted for one S_AXI_ACLK clock cycle when both
// S_AXI_ARVALID and axi_arready are asserted. The slave registers
// data are available on the axi_rdata bus at this instance. The
// assertion of axi_rvalid marks the validity of read data on the
// bus and axi_rresp indicates the status of read transaction.axi_rvalid
// is deasserted on reset (active low). axi_rresp and axi_rdata are
// cleared to zero on reset (active low).
always @( posedge S_AXI_ACLK )
begin
if ( S_AXI_ARESETN == 1'b0 )
begin
axi_rvalid <= 0;
axi_rresp <= 0;
end
else
begin
if (axi_arready && S_AXI_ARVALID && ~axi_rvalid)
begin
// Valid read data is available at the read data bus
axi_rvalid <= 1'b1;
axi_rresp <= 2'b0; // 'OKAY' response
end
else if (axi_rvalid && S_AXI_RREADY)
begin
// Read data is accepted by the master
axi_rvalid <= 1'b0;
end
end
end
 
// Implement memory mapped register select and read logic generation
// Slave register read enable is asserted when valid address is available
// and the slave is ready to accept the read address.
assign slv_reg_rden = axi_arready & S_AXI_ARVALID & ~axi_rvalid;
always @(*)
begin
reg_data_out = 0;
// Address decoding for reading registers
case ( axi_araddr[ADDR_LSB+OPT_MEM_ADDR_BITS:ADDR_LSB] )
5'h00 : reg_data_out = slv_reg0;
5'h01 : reg_data_out = slv_reg1;
5'h02 : reg_data_out = slv_reg2;
5'h03 : reg_data_out = slv_reg3;
5'h04 : reg_data_out = slv_reg4;
5'h05 : reg_data_out = slv_reg5;
5'h06 : reg_data_out = slv_reg6;
5'h07 : reg_data_out = slv_reg7;
5'h08 : reg_data_out = slv_reg8;
5'h09 : reg_data_out = slv_reg9;
5'h0A : reg_data_out = slv_reg10;
5'h0B : reg_data_out = slv_reg11;
5'h0C : reg_data_out = slv_reg12;
5'h0D : reg_data_out = slv_reg13;
5'h0E : reg_data_out = slv_reg14;
5'h0F : reg_data_out = slv_reg15;
5'h10 : reg_data_out = slv_reg16;
5'h11 : reg_data_out = slv_reg17;
5'h12 : reg_data_out = slv_reg18;
5'h13 : reg_data_out = slv_reg19;
5'h14 : reg_data_out = slv_reg20;
5'h15 : reg_data_out = slv_reg21;
5'h16 : reg_data_out = slv_reg22;
5'h17 : reg_data_out = slv_reg23;
5'h18 : reg_data_out = slv_reg24;
5'h19 : reg_data_out = slv_reg25;
5'h1A : reg_data_out = slv_reg26;
5'h1B : reg_data_out = slv_reg27;
5'h1C : reg_data_out = slv_reg28;
5'h1D : reg_data_out = slv_reg29;
5'h1E : reg_data_out = slv_reg30;
5'h1F : reg_data_out = slv_reg31;
default : reg_data_out = 0;
endcase
end
 
// Output register or memory read data
always @( posedge S_AXI_ACLK )
begin
if ( S_AXI_ARESETN == 1'b0 )
begin
axi_rdata <= 0;
end
else
begin
// When there is a valid read address (S_AXI_ARVALID) with
// acceptance of read address by the slave (axi_arready),
// output the read data
if (slv_reg_rden)
begin
axi_rdata <= reg_data_out; // register read data
end
end
end
 
// Add user logic here
 
// User logic ends
//
////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
//
// The following code was not part of the original Xilinx demo.
//
////////////////////////////////////////////////////////////////////////////////
`ifdef FORMAL
localparam F_LGDEPTH = 4;
 
wire [(F_LGDEPTH-1):0] f_axi_awr_outstanding,
f_axi_wr_outstanding,
f_axi_rd_outstanding;
 
//
// Connect our slave to the AXI-lite property set
//
faxil_slave #(// .C_AXI_DATA_WIDTH(C_S_AXI_DATA_WIDTH),
.C_AXI_ADDR_WIDTH(C_S_AXI_ADDR_WIDTH),
.F_LGDEPTH(F_LGDEPTH)) properties(
.i_clk(S_AXI_ACLK),
.i_axi_reset_n(S_AXI_ARESETN),
//
.i_axi_awaddr(S_AXI_AWADDR),
.i_axi_awcache(4'h0),
.i_axi_awprot(S_AXI_AWPROT),
.i_axi_awvalid(S_AXI_AWVALID),
.i_axi_awready(S_AXI_AWREADY),
//
.i_axi_wdata(S_AXI_WDATA),
.i_axi_wstrb(S_AXI_WSTRB),
.i_axi_wvalid(S_AXI_WVALID),
.i_axi_wready(S_AXI_WREADY),
//
.i_axi_bresp(S_AXI_BRESP),
.i_axi_bvalid(S_AXI_BVALID),
.i_axi_bready(S_AXI_BREADY),
//
.i_axi_araddr(S_AXI_ARADDR),
.i_axi_arprot(S_AXI_ARPROT),
.i_axi_arcache(4'h0),
.i_axi_arvalid(S_AXI_ARVALID),
.i_axi_arready(S_AXI_ARREADY),
//
.i_axi_rdata(S_AXI_RDATA),
.i_axi_rresp(S_AXI_RRESP),
.i_axi_rvalid(S_AXI_RVALID),
.i_axi_rready(S_AXI_RREADY),
//
.f_axi_rd_outstanding(f_axi_rd_outstanding),
.f_axi_wr_outstanding(f_axi_wr_outstanding),
.f_axi_awr_outstanding(f_axi_awr_outstanding));
 
reg f_past_valid;
initial f_past_valid = 1'b0;
always @(posedge S_AXI_ACLK)
f_past_valid <= 1'b1;
 
////////////////////////////////////////////////////////////////////////
//
//
// Properties necessary to pass induction
// --- assuming we make it that far (we won't)
//
//
always @(*)
if (S_AXI_ARESETN)
begin
assert(f_axi_rd_outstanding == ((S_AXI_RVALID)? 1:0));
assert(f_axi_wr_outstanding == ((S_AXI_BVALID)? 1:0));
end
 
always @(*)
assert(f_axi_awr_outstanding == f_axi_wr_outstanding);
 
////////////////////////////////////////////////////////////////////////
//
//
// Cover properties
//
//
// Make sure it is possible to change our register
always @(posedge S_AXI_ACLK)
cover($changed(slv_reg0)&&(slv_reg0 == 32'hdeadbeef));
 
always @(posedge S_AXI_ACLK)
cover((axi_rvalid)&&(axi_rdata == 32'hdeadbeef)
&&($past(axi_araddr[ADDR_LSB+OPT_MEM_ADDR_BITS:ADDR_LSB] == 0)));
 
// Make sure it is possible to read from our register
always @(posedge S_AXI_ACLK)
cover($past(reg_data_out == slv_reg0)
&&($past(axi_araddr[ADDR_LSB+OPT_MEM_ADDR_BITS:ADDR_LSB])==0)
&&(axi_rdata == slv_reg0));
 
// Performance test. See if we can retire a request on every other
// instruction
//
// --- This first pair of cover statements will pass as written
//
// First a write check
always @(posedge S_AXI_ACLK)
cover( ((S_AXI_BVALID)&&(S_AXI_BREADY))
&&(!$past((S_AXI_BVALID)&&(S_AXI_BREADY),1))
&&( $past((S_AXI_BVALID)&&(S_AXI_BREADY),2))
&&(!$past((S_AXI_BVALID)&&(S_AXI_BREADY),3)));
 
// Now a read check
always @(posedge S_AXI_ACLK)
cover( ((S_AXI_RVALID)&&(S_AXI_RREADY))
&&(!$past((S_AXI_RVALID)&&(S_AXI_RREADY),1))
&&( $past((S_AXI_RVALID)&&(S_AXI_RREADY),2))
&&(!$past((S_AXI_RVALID)&&(S_AXI_RREADY),3)));
 
// Now let's see if we can retire one value every clock tick
//
// --- These two cover statements will fail, even though the ones
// above will pass. This is why I call the design "crippled".
//
// First a write check
always @(posedge S_AXI_ACLK)
cover( ((S_AXI_BVALID)&&(S_AXI_BREADY))
&&($past((S_AXI_BVALID)&&(S_AXI_BREADY),1))
&&($past((S_AXI_BVALID)&&(S_AXI_BREADY),2))
&&($past((S_AXI_BVALID)&&(S_AXI_BREADY),3)));
 
// Now a read check
always @(posedge S_AXI_ACLK)
cover( ((S_AXI_RVALID)&&(S_AXI_RREADY))
&&($past((S_AXI_RVALID)&&(S_AXI_RREADY),1))
&&($past((S_AXI_RVALID)&&(S_AXI_RREADY),2))
&&($past((S_AXI_RVALID)&&(S_AXI_RREADY),3)));
 
// Now let's spend some time to develop a more complicated read
// trace, showing the capabilities of the core. We'll avoid the
// broken parts of the core, and just present ... something useful.
//
reg [12:0] fr_rdcover, fw_rdcover;
 
initial fr_rdcover = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
fr_rdcover <= 0;
else
fr_rdcover <= fw_rdcover;
 
always @(*)
if ((!S_AXI_ARESETN)||(S_AXI_AWVALID)||(S_AXI_WVALID))
fw_rdcover = 0;
else begin
//
// A basic read request
fw_rdcover[0] = (S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[1] = fr_rdcover[0]
&&(S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[2] = fr_rdcover[1]
&&(!S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[3] = fr_rdcover[2]
&&(!S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[4] = fr_rdcover[3]
&&(!S_AXI_ARVALID)
&&(S_AXI_RREADY);
//
// A high speed/pipelined read request
fw_rdcover[5] = fr_rdcover[4]
&&(S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[6] = fr_rdcover[5]
&&(S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[7] = fr_rdcover[6]
&&(S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[8] = fr_rdcover[7]
&&(S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[9] = fr_rdcover[8]
&&(S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[10] = fr_rdcover[9]
&&(S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[11] = fr_rdcover[10]
&&(!S_AXI_ARVALID)
&&(S_AXI_RREADY);
fw_rdcover[12] = fr_rdcover[11]
&&(!S_AXI_ARVALID)
&&(S_AXI_RREADY);
end
 
always @(*)
begin
cover(fw_rdcover[0]);
cover(fw_rdcover[1]);
cover(fw_rdcover[2]);
cover(fw_rdcover[3]);
cover(fw_rdcover[4]);
cover(fw_rdcover[5]); //
cover(fw_rdcover[6]);
cover(fw_rdcover[7]);
cover(fw_rdcover[8]);
cover(fw_rdcover[9]);
cover(fw_rdcover[10]);
cover(fw_rdcover[11]);
cover(fw_rdcover[12]);
end
 
//
// Now let's repeat our complicated cover approach for the write
// channel.
//
reg [24:0] fr_wrcover, fw_wrcover;
 
initial fr_wrcover = 0;
always @(posedge S_AXI_ACLK)
if (!S_AXI_ARESETN)
fr_wrcover <= 0;
else
fr_wrcover <= fw_wrcover;
 
always @(*)
if ((!S_AXI_ARESETN)||(S_AXI_ARVALID)||(!S_AXI_BREADY))
fw_wrcover = 0;
else begin
//
// A basic (synchronized) write request
fw_wrcover[0] = (S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[1] = fr_wrcover[0]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[2] = fr_wrcover[1]
&&(!S_AXI_AWVALID)
&&(!S_AXI_WVALID);
fw_wrcover[3] = fr_wrcover[2]
&&(!S_AXI_AWVALID)
&&(!S_AXI_WVALID);
fw_wrcover[4] = fr_wrcover[3]
&&(!S_AXI_ARVALID)
&&(S_AXI_RREADY);
//
// Address before data
fw_wrcover[5] = fr_wrcover[4]
&&(S_AXI_AWVALID)
&&(!S_AXI_WVALID);
fw_wrcover[6] = fr_wrcover[5]
&&(S_AXI_AWVALID)
&&(!S_AXI_WVALID);
fw_wrcover[7] = fr_wrcover[6]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[8] = fr_wrcover[7]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[9] = fr_wrcover[8]
&&(!S_AXI_AWVALID)
&&(!S_AXI_WVALID);
fw_wrcover[10] = fr_wrcover[9]
&&(!S_AXI_AWVALID)
&&(!S_AXI_WVALID);
//
// Data before address
fw_wrcover[11] = fr_wrcover[10]
&&(!S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[12] = fr_wrcover[11]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[13] = fr_wrcover[12]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[14] = fr_wrcover[13]
&&(!S_AXI_AWVALID)
&&(!S_AXI_WVALID);
fw_wrcover[15] = fr_wrcover[14]
&&(!S_AXI_AWVALID)
&&(!S_AXI_WVALID);
//
// A high speed/pipelined read request
fw_wrcover[16] = fr_wrcover[15]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[17] = fr_wrcover[16]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[18] = fr_wrcover[17]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[19] = fr_wrcover[18]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[20] = fr_wrcover[19]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[21] = fr_wrcover[20]
&&(S_AXI_AWVALID)
&&(S_AXI_WVALID);
fw_wrcover[22] = fr_wrcover[21]
&&(!S_AXI_AWVALID)
&&(!S_AXI_WVALID);
fw_wrcover[23] = fr_wrcover[22]
&&(!S_AXI_AWVALID)
&&(!S_AXI_WVALID);
fw_wrcover[24] = fr_wrcover[23]
&&(!S_AXI_AWVALID)
&&(!S_AXI_WVALID);
end
 
always @(*)
begin
cover(fw_wrcover[0]);
cover(fw_wrcover[1]);
cover(fw_wrcover[2]);
cover(fw_wrcover[3]);
cover(fw_wrcover[4]);
cover(fw_wrcover[5]); //
cover(fw_wrcover[6]);
cover(fw_wrcover[7]);
cover(fw_wrcover[8]);
cover(fw_wrcover[9]);
cover(fw_wrcover[11]);
cover(fw_wrcover[12]);
cover(fw_wrcover[13]);
cover(fw_wrcover[14]);
cover(fw_wrcover[15]);
cover(fw_wrcover[16]);
cover(fw_wrcover[17]);
cover(fw_wrcover[18]);
cover(fw_wrcover[19]);
cover(fw_wrcover[20]);
cover(fw_wrcover[21]);
cover(fw_wrcover[22]);
cover(fw_wrcover[23]);
cover(fw_wrcover[24]);
end
`endif
//
//
// Bug fixes section
//
// The lines below contain assumptions necessary to get the design
// to work. They represent things Xilinx never thought of when
// building their demo.
//
// The following lines are only questionable a bug
initial axi_arready = 1'b0;
initial axi_awready = 1'b0;
initial axi_wready = 1'b0;
initial axi_bvalid = 1'b0;
initial axi_rvalid = 1'b0;
 
//
// This here is necessary to avoid the biggest bug within the design.
//
// If you uncomment the following two lines, the design will work as
// intended. Only ... the bus now has more requirements to it.
//
// always @(posedge S_AXI_ACLK)
// if ($past(S_AXI_ARESETN))
// assume((S_AXI_RREADY)&&(S_AXI_BREADY));
 
// verilator lint_off UNUSED
wire [9:0] unused;
assign unused = { S_AXI_ARPROT, S_AXI_AWPROT,
axi_awaddr[1:0], axi_araddr[1:0] };
// verilator lint_on UNUSED
endmodule

powered by: WebSVN 2.1.0

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