URL
https://opencores.org/ocsvn/wb2axip/wb2axip/trunk
Subversion Repositories wb2axip
Compare Revisions
- This comparison shows the changes necessary to convert path
/wb2axip/trunk
- from Rev 9 to Rev 10
- ↔ Reverse comparison
Rev 9 → Rev 10
/bench/formal/Makefile
0,0 → 1,94
################################################################################ |
## |
## Filename: Makefile |
## |
## Project: Pipelined Wishbone to AXI converter |
## |
## Purpose: To direct the formal verification of the bus bridge |
## sources. |
## |
## Targets: The default target, all, tests all of the components defined |
## within this module. |
## |
## Creator: Dan Gisselquist, Ph.D. |
## Gisselquist Technology, LLC |
## |
################################################################################ |
## |
## 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 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. |
## |
## 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 |
## <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 |
## |
################################################################################ |
## |
## |
TESTS := wbm2axisp wbarbiter # axim2wbsp |
.PHONY: $(TESTS) |
all: $(TESTS) |
RTL := ../../rtl |
SMTBMC := yosys-smtbmc |
# SOLVER := -s z3 |
SOLVER := -s yices |
# SOLVER := -s boolector |
BMCARGS := --presat $(SOLVER) |
# BMCARGS := $(SOLVER) |
INDARGS := $(SOLVER) -i |
|
WBARB := wbarbiter |
WB2AXI := wbm2axisp |
AXI2WB := axim2wbsp |
|
$(WBARB).smt2: $(RTL)/$(WBARB).v fwb_master.v fwb_slave.v $(WBARB).ys |
yosys -ql $(WBARB).yslog -s $(WBARB).ys |
|
$(WB2AXI).smt2: $(RTL)/$(WB2AXI).v $(WB2AXI).ys fwb_slave.v faxi_master.v |
yosys -ql $(WB2AXI).yslog -s $(WB2AXI).ys |
|
$(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 |
|
$(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 $@ |
|
$(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 $@ |
|
$(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 $@ |
|
.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 |
/bench/formal/axim2wbsp.ys
0,0 → 1,11
read_verilog -D AXIM2WBSP -formal ../../rtl/axim2wbsp.v |
read_verilog -D AXIM2WBSP -formal ../../rtl/aximwr2wbsp.v |
read_verilog -D AXIM2WBSP -formal ../../rtl/aximrd2wbsp.v |
read_verilog -D AXIM2WBSP -formal ../../rtl/wbarbiter.v |
read_verilog -D AXIM2WBSP -formal fwb_master.v |
read_verilog -D AXIM2WBSP -formal fwb_slave.v |
read_verilog -D AXIM2WBSP -formal faxi_slave.v |
prep -top axim2wbsp -nordff |
clk2fflogic |
opt -share_all |
write_smt2 -wires axim2wbsp.smt2 |
/bench/formal/fav_slave.v
0,0 → 1,197
//////////////////////////////////////////////////////////////////////////////// |
// |
// Filename: fav_slave.v |
// |
// Project: Pipelined Wishbone to AXI converter |
// |
// Purpose: Formal properties of an Avalon slave. These are the properties |
// the module owning the slave should use: they assume inputs from |
// the bus master, and assert that the outputs from the slave are valid. |
// |
// Creator: Dan Gisselquist, Ph.D. |
// Gisselquist Technology, LLC |
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// 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 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. |
// |
// 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 |
// <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 |
// |
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// |
`default_nettype none |
// |
module fav_slave(i_clk, i_reset, |
i_av_read, |
i_av_write, |
i_av_address, |
i_av_writedata, |
i_av_byteenable, |
i_av_lock, |
i_av_waitrequest, // = wb_stall |
// |
i_av_writeresponsevalid, |
// |
i_av_readdatavalid, |
i_av_readdata, |
i_av_response, // Error response = 2'b11 |
f_rd_nreqs, f_rd_nacks, f_rd_outstanding, |
f_wr_nreqs, f_wr_nacks, f_wr_outstanding); |
parameter DW=32, AW=14; |
parameter F_LGDEPTH=6; |
parameter [(F_LGDEPTH-1):0] F_MAX_REQUESTS = 62; |
input wire i_clk, i_reset; |
input wire i_av_read; |
input wire i_av_write; |
input wire [(AW-1):0] i_av_address; |
input wire [(DW-1):0] i_av_writedata; |
input wire [(DW/8-1):0] i_av_byteenable; |
input wire i_av_lock; |
// |
input wire i_av_waitrequest; |
input wire i_av_writeresponsevalid; |
input wire i_av_readdatavalid; |
input wire [(DW-1):0] i_av_readdata; |
input wire [1:0] i_av_response; |
// |
output reg [(F_LGDEPTH-1):0] f_rd_nreqs, f_rd_nacks; |
output wire [(F_LGDEPTH-1):0] f_rd_outstanding; |
output reg [(F_LGDEPTH-1):0] f_wr_nreqs, f_wr_nacks; |
output wire [(F_LGDEPTH-1):0] f_wr_outstanding; |
|
assert property(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}}); |
|
|
|
reg f_past_valid; |
initial f_past_valid = 1'b0; |
always @(posedge i_clk) |
f_past_valid <= 1'b1; |
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+(DW/8)):0] f_wr_request; |
assign f_wr_request = { i_av_write, i_av_address, i_av_writedata, |
i_av_byteenable }; |
|
|
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 |
|
always @(posedge i_clk) |
if ((f_past_valid)&&(!$past(i_av_lock))) |
assume((!i_av_lock)||(i_av_read)||(i_av_write)); |
|
initial f_rd_nreqs = 0; |
always @(posedge i_clk) |
if (i_reset) |
f_rd_nreqs <= 0; |
else if ((i_av_read)&&(!i_av_waitrequest)) |
f_rd_nreqs <= f_rd_nreqs + 1'b1; |
|
initial f_rd_nacks = 0; |
always @(posedge i_clk) |
if (i_reset) |
f_rd_nacks <= 0; |
else if (i_av_readdatavalid) |
f_rd_nacks <= f_rd_nacks + 1'b1; |
|
assign f_rd_outstanding = f_rd_nreqs - f_rd_nacks; |
|
initial f_wr_nreqs = 0; |
always @(posedge i_clk) |
if (i_reset) |
f_wr_nreqs <= 0; |
else if ((i_av_write)&&(!i_av_waitrequest)) |
f_wr_nreqs <= f_wr_nreqs + 1'b1; |
|
initial f_wr_nacks = 0; |
always @(posedge i_clk) |
if (i_reset) |
f_wr_nacks <= 0; |
else if (i_av_writeresponsevalid) |
f_wr_nacks <= f_wr_nacks + 1'b1; |
|
assign f_wr_outstanding = f_wr_nreqs - f_wr_nacks; |
|
|
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); |
end |
|
always @(posedge i_clk) |
if ((f_past_valid)&&($past(i_reset))) |
begin |
assert(!i_av_readdatavalid); |
assert(!i_av_writeresponsevalid); |
assert(f_rd_nreqs == 0); |
assert(f_rd_nacks == 0); |
assert(f_wr_nreqs == 0); |
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)); |
|
always @(*) |
assume((!i_av_read)||(!i_av_write)); |
|
always @(*) |
assert((!i_av_writeresponsevalid)||(!i_av_readdatavalid)); |
|
always @(posedge i_clk) |
if (f_rd_outstanding == 0) |
assert(!i_av_readdatavalid); |
|
always @(posedge i_clk) |
if (f_wr_outstanding == 0) |
assert(!i_av_writeresponsevalid); |
|
endmodule |
/bench/formal/faxi_master.v
0,0 → 1,756
//////////////////////////////////////////////////////////////////////////////// |
// |
// Filename: faxi_master.v (Formal properties of an AXI master) |
// |
// Project: Pipelined Wishbone to AXI converter |
// |
// Purpose: |
// |
// Creator: Dan Gisselquist, Ph.D. |
// Gisselquist Technology, LLC |
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// 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 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. |
// |
// 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 |
// <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 |
// |
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// |
`default_nettype none |
// |
module faxi_master #( |
parameter C_AXI_ID_WIDTH = 3, // The AXI id width used for R&W |
// This is an int between 1-16 |
parameter C_AXI_DATA_WIDTH = 128,// 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 [(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 |
) ( |
input i_clk, // System clock |
input 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 [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 |
input wire [1:0] i_axi_awburst, // Write Burst type |
input wire [0:0] i_axi_awlock, // Write lock type |
input wire [3:0] i_axi_awcache, // Write Cache type |
input wire [2:0] i_axi_awprot, // Write Protection type |
input wire [3:0] i_axi_awqos, // Write Quality of Svc |
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_wlast, // Last write transaction |
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 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 [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 |
input wire [1:0] i_axi_arburst, // Read Burst type |
input wire [0:0] i_axi_arlock, // Read lock type |
input wire [3:0] i_axi_arcache, // Read Cache type |
input wire [2:0] i_axi_arprot, // Read Protection type |
input wire [3:0] i_axi_arqos, // Read Protection type |
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 i_axi_rvalid, // Read reponse valid |
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 |
|
); |
reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_wr_id_complete; |
|
//***************************************************************************** |
// Parameter declarations |
//***************************************************************************** |
|
localparam LG_AXI_DW = ( C_AXI_DATA_WIDTH == 8) ? 3 |
: ((C_AXI_DATA_WIDTH == 16) ? 4 |
: ((C_AXI_DATA_WIDTH == 32) ? 5 |
: ((C_AXI_DATA_WIDTH == 64) ? 6 |
: ((C_AXI_DATA_WIDTH == 128) ? 7 |
: 8)))); |
|
localparam LG_WB_DW = ( DW == 8) ? 3 |
: ((DW == 16) ? 4 |
: ((DW == 32) ? 5 |
: ((DW == 64) ? 6 |
: ((DW == 128) ? 7 |
: 8)))); |
localparam LGFIFOLN = C_AXI_ID_WIDTH; |
localparam FIFOLN = (1<<LGFIFOLN); |
|
|
//***************************************************************************** |
// 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, |
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]); |
|
// |
// Setup |
// |
reg f_past_valid; |
integer k; |
|
initial f_past_valid = 1'b0; |
always @(posedge i_clk) |
f_past_valid <= 1'b1; |
always @(*) |
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)); |
end |
end |
|
//////////////////////////////////////////////////// |
// |
// |
// Reset properties |
// |
// |
//////////////////////////////////////////////////// |
|
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); |
end |
|
//////////////////////////////////////////////////// |
// |
// |
// Stability assumptions, AXI inputs/responses |
// |
// |
//////////////////////////////////////////////////// |
|
// Assume any response from the bus will not change prior to that |
// response being accepted |
always @(posedge i_clk) |
if (f_past_valid) |
begin |
if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready))) |
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)); |
end |
|
if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready))) |
begin |
assume(i_axi_bid == $past(i_axi_bid)); |
assume(i_axi_bresp == $past(i_axi_bresp)); |
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); |
|
////////////////////////////////////////////// |
// |
// |
// Stability assumptions, AXI outputs/requests |
// |
// |
////////////////////////////////////////////// |
|
// 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)); |
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 |
|
// |
// |
|
/////////////////////////////////////////////////////////////////// |
// |
// |
// 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) |
if ((!i_axi_reset_n)||(!i_axi_awvalid)||(i_axi_awready)) |
f_axi_awstall <= 0; |
else |
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); |
|
reg [(C_AXI_ID_WIDTH):0] f_axi_wstall; |
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 |
f_axi_wstall <= f_axi_wstall + 1'b1; |
always @(*) |
assume((F_AXI_MAXSTALL==0)||(f_axi_wstall < F_AXI_MAXSTALL)); |
|
|
// |
// AXI read address channel |
// |
// |
reg [(C_AXI_ID_WIDTH):0] f_axi_arstall; |
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 |
f_axi_arstall <= f_axi_arstall + 1'b1; |
always @(*) |
assume((F_AXI_MAXSTALL==0)||(f_axi_arstall < F_AXI_MAXSTALL)); |
|
|
//////////////////////////////////////////////////////////////////////// |
// |
// |
// Count outstanding transactions |
// |
// |
//////////////////////////////////////////////////////////////////////// |
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)&&(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 |
|
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 |
|
// Do not let the number of outstanding requests overflow |
always @(posedge i_clk) |
assert(f_axi_wr_outstanding < {(C_AXI_ID_WIDTH){1'b1}}); |
always @(posedge i_clk) |
assert(f_axi_awr_outstanding < {(C_AXI_ID_WIDTH){1'b1}}); |
always @(posedge i_clk) |
assert(f_axi_rd_outstanding < {(C_AXI_ID_WIDTH){1'b1}}); |
|
//////////////////////////////////////////////////////////////////////// |
// |
// |
// 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. |
// |
// |
//////////////////////////////////////////////////////////////////////// |
|
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)||(axi_rd_ack)) |
f_axi_rd_ack_delay <= 0; |
else if (f_axi_rd_outstanding > 0) |
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)) |
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)) |
f_axi_awr_ack_delay <= 0; |
else if (f_axi_awr_outstanding > 0) |
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 @(posedge i_clk) |
assume((F_AXI_MAXDELAY==0)||(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)); |
|
//////////////////////////////////////////////////////////////////////// |
// |
// |
// Assume all 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 |
// individual acknowledgements coming back if there's no outstanding |
// burst. |
// |
// |
//////////////////////////////////////////////////////////////////////// |
|
// |
// AXI write response channel |
// |
always @(posedge i_clk) |
if ((!axi_awr_req)&&(axi_wr_ack)) |
assume(f_axi_awr_outstanding > 0); |
always @(posedge i_clk) |
if ((!axi_wr_req)&&(axi_wr_ack)) |
assume(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); |
|
/////////////////////////////////////////////////////////////////// |
// |
// |
// 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)) |
assert(f_axi_awr_id_outstanding[i_axi_awid+1'b1] == 1'b0); |
assert((!F_CHECK_IDS) |
||(f_axi_awr_id_outstanding[i_axi_awid] == 1'b0)); |
assert((!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 |
|
if (axi_wr_req) |
begin |
if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS)) |
assert(f_axi_wr_id_outstanding[i_axi_awid+1'b1] == 1'b0); |
assert((!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 |
assume(f_axi_wr_id_complete[i_axi_awid] == 1'b0); |
f_axi_wr_id_complete[i_axi_awid] <= 1'b1; |
end |
end |
|
// When issuing a read |
if (axi_ard_req) |
begin |
if ((F_CONSECUTIVE_IDS)&&(F_CHECK_IDS)) |
assert(f_axi_rd_id_outstanding[i_axi_arid+1'b1] == 1'b0); |
assert((!F_CHECK_IDS) |
||(f_axi_rd_id_outstanding[i_axi_arid] == 1'b0)); |
f_axi_rd_id_outstanding[i_axi_arid] <= 1'b1; |
end |
|
// When a write is acknowledged |
if (axi_wr_ack) |
begin |
if (F_CHECK_IDS) |
begin |
assume(f_axi_awr_id_outstanding[i_axi_bid]); |
assume(f_axi_wr_id_outstanding[i_axi_bid]); |
assume((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS) |
||(!f_axi_wr_id_outstanding[i_axi_bid-1'b1])); |
assume((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS) |
||(!f_axi_awr_id_outstanding[i_axi_bid-1'b1])); |
assume(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 |
|
// When a read is acknowledged |
if (axi_rd_ack) |
begin |
if (F_CHECK_IDS) |
begin |
assume(f_axi_rd_id_outstanding[i_axi_rid]); |
assume((!F_STRICT_ORDER)||(!F_CONSECUTIVE_IDS) |
||(!f_axi_rd_id_outstanding[i_axi_rid-1'b1])); |
end |
|
if (i_axi_rlast) |
f_axi_rd_id_outstanding[i_axi_rid] <= 1'b0; |
end |
end |
|
|
reg [LGFIFOLN:0] f_axi_rd_id_outstanding_count, |
f_axi_awr_id_outstanding_count, |
f_axi_wr_id_outstanding_count; |
|
initial f_axi_rd_id_outstanding_count = 0; |
initial f_axi_awr_id_outstanding_count = 0; |
initial f_axi_wr_id_outstanding_count = 0; |
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 |
|
always @(*) |
assert((!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)); |
|
always @(*) |
assert((!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); |
|
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; |
|
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 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; |
assert(f_wr_pending == 0); |
r_last_wr_id_valid <= 1'b1; |
end |
|
if (axi_ard_req) |
f_rd_pending[i_axi_arid] <= i_axi_arlen+9'h1; |
|
|
if ((axi_wr_req)&&(i_axi_wlast)) |
begin |
f_wr_count <= 0; |
r_last_wr_id_valid <= 1'b0; |
assert( |
// 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; |
|
if (axi_rd_ack) |
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)) |
assume(i_axi_rid == r_last_rd_id); |
end |
|
if ((axi_rd_ack)&&(i_axi_rlast)) |
assert(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; |
end |
end else begin |
always @(*) begin |
// 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)); |
|
assert((!i_axi_arvalid)||(i_axi_arlen==0)); |
assert((!i_axi_awvalid)||(i_axi_awlen==0)); |
end |
|
always @(posedge i_clk) |
if (i_axi_awvalid) |
assert(i_axi_awlen == 0); |
always @(posedge i_clk) |
if (i_axi_arvalid) |
assert(i_axi_arlen == 0); |
always @(posedge i_clk) |
if (i_axi_wvalid) |
assert(i_axi_wlast); |
always @(posedge i_clk) |
if (i_axi_rvalid) |
assume(i_axi_rlast); |
end endgenerate |
|
`endif |
endmodule |
/bench/formal/faxi_slave.v
0,0 → 1,757
//////////////////////////////////////////////////////////////////////////////// |
// |
// Filename: faxi_slave.v (Formal properties of an AXI slave) |
// |
// Project: Pipelined Wishbone to AXI converter |
// |
// Purpose: |
// |
// Creator: Dan Gisselquist, Ph.D. |
// Gisselquist Technology, LLC |
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// 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 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. |
// |
// 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 |
// <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 |
// |
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// |
`default_nettype none |
// |
module faxi_slave #( |
parameter C_AXI_ID_WIDTH = 3, // The AXI id width used for R&W |
// This is an int between 1-16 |
parameter C_AXI_DATA_WIDTH = 128,// 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 [(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 |
) ( |
input i_clk, // System clock |
input 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 [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 |
input wire [1:0] i_axi_awburst, // Write Burst type |
input wire [0:0] i_axi_awlock, // Write lock type |
input wire [3:0] i_axi_awcache, // Write Cache type |
input wire [2:0] i_axi_awprot, // Write Protection type |
input wire [3:0] i_axi_awqos, // Write Quality of Svc |
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_wlast, // Last write transaction |
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 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 [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 |
input wire [1:0] i_axi_arburst, // Read Burst type |
input wire [0:0] i_axi_arlock, // Read lock type |
input wire [3:0] i_axi_arcache, // Read Cache type |
input wire [2:0] i_axi_arprot, // Read Protection type |
input wire [3:0] i_axi_arqos, // Read Protection type |
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 i_axi_rvalid, // Read reponse valid |
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 |
|
); |
reg [((1<<C_AXI_ID_WIDTH)-1):0] f_axi_wr_id_complete; |
|
//***************************************************************************** |
// Parameter declarations |
//***************************************************************************** |
|
localparam LG_AXI_DW = ( C_AXI_DATA_WIDTH == 8) ? 3 |
: ((C_AXI_DATA_WIDTH == 16) ? 4 |
: ((C_AXI_DATA_WIDTH == 32) ? 5 |
: ((C_AXI_DATA_WIDTH == 64) ? 6 |
: ((C_AXI_DATA_WIDTH == 128) ? 7 |
: 8)))); |
|
localparam LG_WB_DW = ( DW == 8) ? 3 |
: ((DW == 16) ? 4 |
: ((DW == 32) ? 5 |
: ((DW == 64) ? 6 |
: ((DW == 128) ? 7 |
: 8)))); |
localparam LGFIFOLN = C_AXI_ID_WIDTH; |
localparam FIFOLN = (1<<LGFIFOLN); |
|
|
//***************************************************************************** |
// 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, |
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]); |
|
// |
// Setup |
// |
reg f_past_valid; |
integer k; |
|
initial f_past_valid = 1'b0; |
always @(posedge i_clk) |
f_past_valid <= 1'b1; |
always @(*) |
if (!f_past_valid) |
assume(!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 |
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 |
// |
// |
//////////////////////////////////////////////////// |
|
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); |
end |
|
//////////////////////////////////////////////////// |
// |
// |
// Stability assumptions, AXI inputs/responses |
// |
// |
//////////////////////////////////////////////////// |
|
// Assume any response from the bus will not change prior to that |
// response being accepted |
always @(posedge i_clk) |
if (f_past_valid) |
begin |
if ((f_past_valid)&&($past(i_axi_rvalid))&&(!$past(i_axi_rready))) |
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)); |
end |
|
if ((f_past_valid)&&($past(i_axi_bvalid))&&(!$past(i_axi_bready))) |
begin |
assert(i_axi_bid == $past(i_axi_bid)); |
assert(i_axi_bresp == $past(i_axi_bresp)); |
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); |
|
////////////////////////////////////////////// |
// |
// |
// Stability assumptions, AXI outputs/requests |
// |
// |
////////////////////////////////////////////// |
|
// 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)); |
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 |
|
// |
// |
|
/////////////////////////////////////////////////////////////////// |
// |
// |
// 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) |
if ((!i_axi_reset_n)||(!i_axi_awvalid)||(i_axi_awready)) |
f_axi_awstall <= 0; |
else |
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); |
|
reg [(C_AXI_ID_WIDTH):0] f_axi_wstall; |
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 |
f_axi_wstall <= f_axi_wstall + 1'b1; |
always @(*) |
assert((F_AXI_MAXSTALL==0)||(f_axi_wstall < F_AXI_MAXSTALL)); |
|
|
// |
// AXI read address channel |
// |
// |
reg [(C_AXI_ID_WIDTH):0] f_axi_arstall; |
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 |
f_axi_arstall <= f_axi_arstall + 1'b1; |
always @(*) |
assert((F_AXI_MAXSTALL==0)||(f_axi_arstall < F_AXI_MAXSTALL)); |
|
|
//////////////////////////////////////////////////////////////////////// |
// |
// |
// 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)&&(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 |
|
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 |
|
// Do not let the number of outstanding requests overflow |
always @(posedge i_clk) |
assume(f_axi_wr_outstanding < {(C_AXI_ID_WIDTH){1'b1}}); |
always @(posedge i_clk) |
assume(f_axi_awr_outstanding < {(C_AXI_ID_WIDTH){1'b1}}); |
always @(posedge i_clk) |
assume(f_axi_rd_outstanding < {(C_AXI_ID_WIDTH){1'b1}}); |
|
//////////////////////////////////////////////////////////////////////// |
// |
// |
// 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. |
// |
// |
//////////////////////////////////////////////////////////////////////// |
|
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)||(axi_rd_ack)) |
f_axi_rd_ack_delay <= 0; |
else if (f_axi_rd_outstanding > 0) |
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)) |
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)) |
f_axi_awr_ack_delay <= 0; |
else if (f_axi_awr_outstanding > 0) |
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 @(posedge i_clk) |
assert((F_AXI_MAXDELAY==0)||(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)); |
|
//////////////////////////////////////////////////////////////////////// |
// |
// |
// Assume all 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 |
// individual acknowledgements coming back if there's no outstanding |
// burst. |
// |
// |
//////////////////////////////////////////////////////////////////////// |
|
// |
// 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); |
|
// |
// 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); |
|
/////////////////////////////////////////////////////////////////// |
// |
// |
// 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 |
|
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 |
|
// 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 |
|
// 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 |
|
// 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])); |
end |
|
if (i_axi_rlast) |
f_axi_rd_id_outstanding[i_axi_rid] <= 1'b0; |
end |
end |
|
|
reg [LGFIFOLN:0] f_axi_rd_id_outstanding_count, |
f_axi_awr_id_outstanding_count, |
f_axi_wr_id_outstanding_count; |
|
initial f_axi_rd_id_outstanding_count = 0; |
initial f_axi_awr_id_outstanding_count = 0; |
initial f_axi_wr_id_outstanding_count = 0; |
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 |
|
always @(*) |
assume((!F_CHECK_IDS)||(f_axi_awr_outstanding== f_axi_awr_id_outstanding_count)); |
|
always @(*) |
assume((!F_CHECK_IDS)||(f_axi_wr_outstanding == f_axi_wr_id_outstanding_count)); |
|
always @(*) |
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); |
|
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; |
|
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 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 |
|
if (axi_ard_req) |
f_rd_pending[i_axi_arid] <= i_axi_arlen+9'h1; |
|
|
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; |
|
if (axi_rd_ack) |
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); |
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; |
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)); |
|
assume((!i_axi_arvalid)||(i_axi_arlen==0)); |
assume((!i_axi_awvalid)||(i_axi_awlen==0)); |
end |
|
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 |
endmodule |
/bench/formal/fwb_master.v
0,0 → 1,417
//////////////////////////////////////////////////////////////////////////////// |
// |
// Filename: fwb_master.v |
// |
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core |
// |
// Purpose: This file describes the rules of a wishbone interaction from the |
// perspective of a wishbone master. These formal rules may be used |
// with yosys-smtbmc to *prove* that the master properly handles outgoing |
// transactions and incoming responses. |
// |
// This module contains no functional logic. It is intended for formal |
// verification only. The outputs returned, the number of requests that |
// have been made, the number of acknowledgements received, and the number |
// of outstanding requests, are designed for further formal verification |
// purposes *only*. |
// |
// This file is different from a companion formal_slave.v file in that the |
// assertions are made on the outputs of the wishbone master: o_wb_cyc, |
// o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, and o_wb_sel, while only |
// assumptions are made about the inputs: i_wb_stall, i_wb_ack, i_wb_data, |
// i_wb_err. In the formal_slave.v, assumptions are made about the |
// slave inputs (the master outputs), and assertions are made about the |
// slave outputs (the master inputs). |
// |
// |
// |
// |
// Creator: Dan Gisselquist, Ph.D. |
// Gisselquist Technology, LLC |
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// 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 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. |
// |
// 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 |
// <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 |
// |
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// |
`default_nettype none |
// |
module fwb_master(i_clk, i_reset, |
// The Wishbone bus |
i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel, |
i_wb_ack, i_wb_stall, i_wb_idata, i_wb_err, |
// Some convenience output parameters |
f_nreqs, f_nacks, f_outstanding); |
parameter AW=32, DW=32; |
parameter F_MAX_STALL = 0, |
F_MAX_ACK_DELAY = 0; |
parameter F_LGDEPTH = 4; |
parameter [(F_LGDEPTH-1):0] F_MAX_REQUESTS = 0; |
// |
// If true, allow the bus to be kept open when there are no outstanding |
// requests. This is useful for any master that might execute a |
// read modify write cycle, such as an atomic add. |
parameter [0:0] F_OPT_RMW_BUS_OPTION = 1; |
// |
// |
parameter [0:0] F_OPT_SHORT_CIRCUIT_PROOF = 0; |
// |
// If this is the source of a request, then we can assume STB and CYC |
// will initially start out high. Master interfaces following the |
// source on the way to the slave may not have this property |
parameter [0:0] F_OPT_SOURCE = 0; |
// |
// If true, allow the bus to issue multiple discontinuous requests. |
// Unlike F_OPT_RMW_BUS_OPTION, these requests may be issued while other |
// requests are outstanding |
parameter [0:0] F_OPT_DISCONTINUOUS = 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; |
localparam DLYBITS= (MAX_DELAY < 4) ? 2 |
: ((MAX_DELAY < 16) ? 4 |
: ((MAX_DELAY < 64) ? 6 |
: ((MAX_DELAY < 256) ? 8 |
: ((MAX_DELAY < 1024) ? 10 |
: ((MAX_DELAY < 4096) ? 12 |
: ((MAX_DELAY < 16384) ? 14 |
: ((MAX_DELAY < 65536) ? 16 |
: 32))))))); |
// |
input wire i_clk, i_reset; |
// Input/master bus |
input wire i_wb_cyc, i_wb_stb, i_wb_we; |
input wire [(AW-1):0] i_wb_addr; |
input wire [(DW-1):0] i_wb_data; |
input wire [(DW/8-1):0] i_wb_sel; |
// |
input wire i_wb_ack; |
input wire i_wb_stall; |
input wire [(DW-1):0] i_wb_idata; |
input wire i_wb_err; |
// |
output reg [(F_LGDEPTH-1):0] f_nreqs, f_nacks; |
output wire [(F_LGDEPTH-1):0] f_outstanding; |
|
// |
// Let's just make sure our parameters are set up right |
// |
assert property(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}}); |
|
// |
// Wrap the request line in a bundle. The top bit, named STB_BIT, |
// is the bit indicating whether the request described by this vector |
// is a valid request or not. |
// |
localparam STB_BIT = 2+AW+DW+DW/8-1; |
wire [STB_BIT:0] f_request; |
assign f_request = { i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel }; |
|
// |
// A quick register to be used later to know if the $past() operator |
// will yield valid result |
reg f_past_valid; |
initial f_past_valid = 1'b0; |
always @(posedge i_clk) |
f_past_valid <= 1'b1; |
always @(*) |
if (!f_past_valid) |
assume(i_reset); |
// |
// |
// Assertions regarding the initial (and reset) state |
// |
// |
|
// |
// Assume we start from a reset condition |
initial assert(i_reset); |
initial assert(!i_wb_cyc); |
initial assert(!i_wb_stb); |
// |
initial assume(!i_wb_ack); |
initial assume(!i_wb_err); |
|
always @(posedge i_clk) |
if ((f_past_valid)&&($past(i_reset))) |
begin |
assert(!i_wb_cyc); |
assert(!i_wb_stb); |
// |
assume(!i_wb_ack); |
assume(!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 |
|
// |
// |
// Bus requests |
// |
// |
|
// Following any bus error, the CYC line should be dropped to abort |
// the transaction |
always @(posedge i_clk) |
if ((f_past_valid)&&($past(i_wb_err))&&($past(i_wb_cyc))) |
assert(!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); |
|
// If a request was both outstanding and stalled on the last clock, |
// then nothing should change on this clock regarding it. |
always @(posedge i_clk) |
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)); |
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)); |
|
|
// 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)); |
|
// 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); |
|
|
// |
// |
// Bus responses |
// |
// |
|
// 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))) |
begin |
assume(!i_wb_ack); |
assume(!i_wb_err); |
// Stall may still be true--such as when we are not |
// selected at some arbiter between us and the slave |
end |
|
// ACK and ERR may never both be true at the same time |
always @(*) |
assume((!i_wb_ack)||(!i_wb_err)); |
|
generate if (F_MAX_STALL > 0) |
begin : MXSTALL |
// |
// Assume the slave cannnot stall for more than F_MAX_STALL |
// counts. We'll count this forward any time STB and STALL |
// are both true. |
// |
reg [(DLYBITS-1):0] f_stall_count; |
|
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); |
end endgenerate |
|
generate if (F_MAX_ACK_DELAY > 0) |
begin : MXWAIT |
// |
// Assume the slave will respond within F_MAX_ACK_DELAY cycles, |
// counted either from the end of the last request, or from the |
// last ACK received |
// |
reg [(DLYBITS-1):0] f_ackwait_count; |
|
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; |
end endgenerate |
|
// |
// Count the number of requests that have been made |
// |
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; |
|
|
// |
// Count the number of acknowledgements that have been received |
// |
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; |
|
// |
// The number of outstanding requests is the difference between |
// the number of requests and the number of acknowledgements |
// |
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 @(posedge i_clk) |
if ((i_wb_cyc)&&(f_outstanding == 0)) |
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); |
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 |
// This is true for the master only, and more specifically |
// only for those masters that are the initial source of any |
// transaction. By the time an interaction gets to the slave, |
// 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); |
end endgenerate |
|
|
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) |
assert((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 |
// transactions, even though nothing is outstanding. For |
// these busses, turn F_OPT_RMW_BUS_OPTION on. |
end endgenerate |
|
generate if (F_OPT_SHORT_CIRCUIT_PROOF) |
begin |
// In many ways, we don't care what happens on the bus return |
// lines if the cycle line is low, so restricting them to a |
// known value makes a lot of sense. |
// |
// On the other hand, if something above *does* depend upon |
// these values (when it shouldn't), then we might want to know |
// about it. |
// |
// |
always @(posedge i_clk) |
begin |
if (!i_wb_cyc) |
begin |
restrict(!i_wb_stall); |
restrict($stable(i_wb_idata)); |
end else if ((!$past(i_wb_ack))&&(!i_wb_ack)) |
restrict($stable(i_wb_idata)); |
end |
end endgenerate |
|
generate if ((!F_OPT_DISCONTINUOUS)&&(!F_OPT_RMW_BUS_OPTION)) |
begin : INSIST_ON_NO_DISCONTINUOUS_STBS |
// Within my own code, once a request begins it goes to |
// completion and the CYC line is dropped. The master |
// is not allowed to raise STB again after dropping it. |
// Doing so would be a *discontinuous* request. |
// |
// However, in any RMW scheme, discontinuous requests are |
// 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); |
end endgenerate |
|
endmodule |
/bench/formal/fwb_slave.v
0,0 → 1,374
//////////////////////////////////////////////////////////////////////////////// |
// |
// Filename: fwb_slave.v |
// |
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core |
// |
// Purpose: This file describes the rules of a wishbone interaction from the |
// perspective of a wishbone slave. These formal rules may be used |
// with yosys-smtbmc to *prove* that the slave properly handles outgoing |
// responses to (assumed correct) incoming requests. |
// |
// This module contains no functional logic. It is intended for formal |
// verification only. The outputs returned, the number of requests that |
// have been made, the number of acknowledgements received, and the number |
// of outstanding requests, are designed for further formal verification |
// purposes *only*. |
// |
// This file is different from a companion formal_master.v file in that |
// assumptions are made about the inputs to the slave: i_wb_cyc, |
// i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, and i_wb_sel, while full |
// assertions are made about the outputs: o_wb_stall, o_wb_ack, o_wb_data, |
// o_wb_err. In the formal_master.v, assertions are made about the |
// master outputs (slave inputs)), and assumptions are made about the |
// master inputs (the slave outputs). |
// |
// |
// |
// |
// Creator: Dan Gisselquist, Ph.D. |
// Gisselquist Technology, LLC |
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// 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 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. |
// |
// 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 |
// <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 |
// |
// |
//////////////////////////////////////////////////////////////////////////////// |
// |
// |
`default_nettype none |
// |
module fwb_slave(i_clk, i_reset, |
// The Wishbone bus |
i_wb_cyc, i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel, |
i_wb_ack, i_wb_stall, i_wb_idata, i_wb_err, |
// Some convenience output parameters |
f_nreqs, f_nacks, f_outstanding); |
parameter AW=32, DW=32; |
parameter F_MAX_STALL = 0, |
F_MAX_ACK_DELAY = 0; |
parameter F_LGDEPTH = 4; |
parameter [(F_LGDEPTH-1):0] F_MAX_REQUESTS = 0; |
// |
// If true, allow the bus to be kept open when there are no outstanding |
// requests. This is useful for any master that might execute a |
// read modify write cycle, such as an atomic add. |
parameter [0:0] F_OPT_RMW_BUS_OPTION = 1; |
// |
// |
// If true, allow the bus to issue multiple discontinuous requests. |
// Unlike F_OPT_RMW_BUS_OPTION, these requests may be issued while other |
// requests are outstanding |
parameter [0:0] F_OPT_DISCONTINUOUS = 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; |
localparam DLYBITS= (MAX_DELAY < 4) ? 2 |
: ((MAX_DELAY < 16) ? 4 |
: ((MAX_DELAY < 64) ? 6 |
: ((MAX_DELAY < 256) ? 8 |
: ((MAX_DELAY < 1024) ? 10 |
: ((MAX_DELAY < 4096) ? 12 |
: ((MAX_DELAY < 16384) ? 14 |
: ((MAX_DELAY < 65536) ? 16 |
: 32))))))); |
// |
input wire i_clk, i_reset; |
// Input/master bus |
input wire i_wb_cyc, i_wb_stb, i_wb_we; |
input wire [(AW-1):0] i_wb_addr; |
input wire [(DW-1):0] i_wb_data; |
input wire [(DW/8-1):0] i_wb_sel; |
// |
input wire i_wb_ack; |
input wire i_wb_stall; |
input wire [(DW-1):0] i_wb_idata; |
input wire i_wb_err; |
// |
output reg [(F_LGDEPTH-1):0] f_nreqs, f_nacks; |
output wire [(F_LGDEPTH-1):0] f_outstanding; |
|
// |
// Let's just make sure our parameters are set up right |
// |
assert property(F_MAX_REQUESTS < {(F_LGDEPTH){1'b1}}); |
|
// |
// Wrap the request line in a bundle. The top bit, named STB_BIT, |
// is the bit indicating whether the request described by this vector |
// is a valid request or not. |
// |
localparam STB_BIT = 2+AW+DW+DW/8-1; |
wire [STB_BIT:0] f_request; |
assign f_request = { i_wb_stb, i_wb_we, i_wb_addr, i_wb_data, i_wb_sel }; |
|
// |
// A quick register to be used later to know if the $past() operator |
// will yield valid result |
reg f_past_valid; |
initial f_past_valid = 1'b0; |
always @(posedge i_clk) |
f_past_valid <= 1'b1; |
always @(*) |
if (!f_past_valid) |
assume(i_reset); |
// |
// |
// Assertions regarding the initial (and reset) state |
// |
// |
|
// |
// Assume we start from a reset condition |
initial assume(i_reset); |
initial assume(!i_wb_cyc); |
initial assume(!i_wb_stb); |
// |
initial assert(!i_wb_ack); |
initial assert(!i_wb_err); |
|
always @(posedge i_clk) |
if ((f_past_valid)&&($past(i_reset))) |
begin |
assume(!i_wb_cyc); |
assume(!i_wb_stb); |
// |
assert(!i_wb_ack); |
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 |
|
// |
// |
// Bus requests |
// |
// |
|
// Following any bus error, the CYC line should be dropped to abort |
// the transaction |
always @(posedge i_clk) |
if ((f_past_valid)&&($past(i_wb_err))&&($past(i_wb_cyc))) |
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); |
|
// If a request was both outstanding and stalled on the last clock, |
// then nothing should change on this clock regarding it. |
always @(posedge i_clk) |
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)); |
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)); |
|
|
// 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)); |
|
// 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); |
|
|
// |
// |
// Bus responses |
// |
// |
|
// 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))) |
begin |
assert(!i_wb_ack); |
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 |
|
// ACK and ERR may never both be true at the same time |
always @(*) |
assume((!i_wb_ack)||(!i_wb_err)); |
|
generate if (F_MAX_STALL > 0) |
begin : MXSTALL |
// |
// Assume the slave cannnot stall for more than F_MAX_STALL |
// counts. We'll count this forward any time STB and STALL |
// are both true. |
// |
reg [(DLYBITS-1):0] f_stall_count; |
|
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); |
end endgenerate |
|
generate if (F_MAX_ACK_DELAY > 0) |
begin : MXWAIT |
// |
// Assume the slave will respond within F_MAX_ACK_DELAY cycles, |
// counted either from the end of the last request, or from the |
// last ACK received |
// |
reg [(DLYBITS-1):0] f_ackwait_count; |
|
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; |
end endgenerate |
|
// |
// Count the number of requests that have been received |
// |
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; |
|
|
// |
// Count the number of acknowledgements that have been returned |
// |
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; |
|
// |
// The number of outstanding requests is the difference between |
// the number of requests and the number of acknowledgements |
// |
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 @(posedge i_clk) |
if ((i_wb_cyc)&&(f_outstanding == 0)) |
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); |
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)); |
// 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 |
// transactions, even though nothing is outstanding. For |
// these busses, turn F_OPT_RMW_BUS_OPTION on. |
end endgenerate |
|
generate if ((!F_OPT_DISCONTINUOUS)&&(!F_OPT_RMW_BUS_OPTION)) |
begin : INSIST_ON_NO_DISCONTINUOUS_STBS |
// Within my own code, once a request begins it goes to |
// completion and the CYC line is dropped. The master |
// is not allowed to raise STB again after dropping it. |
// Doing so would be a *discontinuous* request. |
// |
// However, in any RMW scheme, discontinuous requests are |
// 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); |
end endgenerate |
|
endmodule |
/bench/formal/wbarbiter.ys
0,0 → 1,7
read_verilog -D WBARBITER -formal ../../rtl/wbarbiter.v |
read_verilog -formal /home/dan/work/rnd/zipcpu/trunk/rtl/aux/fwb_master.v |
read_verilog -formal /home/dan/work/rnd/zipcpu/trunk/rtl/aux/fwb_slave.v |
prep -top wbarbiter -nordff |
clk2fflogic |
opt -share_all |
write_smt2 -wires wbarbiter.smt2 |
/bench/formal/wbm2axisp.ys
0,0 → 1,7
read_verilog -D WBM2AXISP -formal ../../rtl/wbm2axisp.v |
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 |