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

Subversion Repositories wb2axip

Compare Revisions

  • This comparison shows the changes necessary to convert path 
    /
    from Rev 9 to Rev 10
    ↔ Reverse comparison
  •

Rev 9 → Rev 10

/wb2axip/trunk/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
/wb2axip/trunk/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
/wb2axip/trunk/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
/wb2axip/trunk/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
/wb2axip/trunk/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
/wb2axip/trunk/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
/wb2axip/trunk/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
/wb2axip/trunk/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
/wb2axip/trunk/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

powered by: WebSVN 2.1.0

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