| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Filename: fwbc_master.v |
| // |
| // Project: WB2AXIPSP: bus bridges and other odds and ends |
| // |
| // Purpose: This file describes the rules of a wishbone *classic* |
| // interaction from the perspective of a wishbone classic master. |
| // These formal rules may be used with SymbiYosys to *prove* that the |
| // master properly generates outgoing responses to drive an (assumed |
| // correct) slave. |
| // |
| // |
| // Creator: Dan Gisselquist, Ph.D. |
| // Gisselquist Technology, LLC |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // Copyright (C) 2019-2020, Gisselquist Technology, LLC |
| // |
| // This file is part of the WB2AXIP project. |
| // |
| // The WB2AXIP project contains free software and gateware, licensed under the |
| // Apache License, Version 2.0 (the "License"). You may not use this project, |
| // or this file, except in compliance with the License. You may obtain a copy |
| // of the License at |
| // |
| // http://www.apache.org/licenses/LICENSE-2.0 |
| // |
| // Unless required by applicable law or agreed to in writing, software |
| // distributed under the License is distributed on an "AS IS" BASIS, WITHOUT |
| // WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the |
| // License for the specific language governing permissions and limitations |
| // under the License. |
| // |
| //////////////////////////////////////////////////////////////////////////////// |
| // |
| // |
| `default_nettype none |
| // |
| module fwbc_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_cti, i_wb_bte, |
| i_wb_ack, i_wb_idata, i_wb_err, i_wb_rty); |
| parameter AW=32, DW=32; |
| parameter F_MAX_DELAY = 4; |
| parameter [0:0] OPT_BUS_ABORT = 0; |
| localparam DLYBITS= $clog2(F_MAX_DELAY+1); |
| // |
| 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 [2:0] i_wb_cti; |
| input wire [1:0] i_wb_bte; |
| // |
| input wire i_wb_ack; |
| input wire [(DW-1):0] i_wb_idata; |
| input wire i_wb_err; |
| input wire i_wb_rty; |
| // |
| |
| `define SLAVE_ASSUME assert |
| `define SLAVE_ASSERT assume |
| |
| // next_addr, for use in calculating the next address within a |
| // burst |
| reg [AW-1:0] next_addr; |
| |
| |
| // |
| // 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+3+2-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, |
| i_wb_cti, i_wb_bte }; |
| |
| // |
| // 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) |
| `SLAVE_ASSUME(i_reset); |
| // |
| // |
| // Assertions regarding the initial (and reset) state |
| // |
| // |
| |
| // |
| // Assume we start from a reset condition |
| initial assert(i_reset); |
| initial `SLAVE_ASSUME(!i_wb_cyc); |
| initial `SLAVE_ASSUME(!i_wb_stb); |
| // |
| initial `SLAVE_ASSERT(!i_wb_ack); |
| initial `SLAVE_ASSERT(!i_wb_err); |
| initial `SLAVE_ASSERT(!i_wb_rty); |
| |
| always @(posedge i_clk) |
| if ((!f_past_valid)||($past(i_reset))) |
| begin |
| `SLAVE_ASSUME(!i_wb_cyc); |
| `SLAVE_ASSUME(!i_wb_stb); |
| // |
| `SLAVE_ASSERT(!i_wb_ack); |
| `SLAVE_ASSERT(!i_wb_err); |
| `SLAVE_ASSERT(!i_wb_rty); |
| end |
| |
| // |
| // |
| // Bus requests |
| // |
| // |
| |
| // This core only supports classic CTIs. Burst types are therefore |
| // irrelevant and ignored. |
| always @(*) |
| if (i_wb_stb) |
| `SLAVE_ASSUME(i_wb_cti == 3'b0); |
| |
| // STB can only be true if CYC is also true |
| always @(*) |
| if (i_wb_stb) |
| `SLAVE_ASSUME(i_wb_cyc); |
| |
| // If a request was both outstanding and stalled on the last clock, |
| // then nothing should change on this clock regarding it. |
| always @(posedge i_clk) |
| if ((f_past_valid)&&(!$past(i_reset)) |
| &&($past(i_wb_stb))&&(i_wb_cyc) |
| &&(!$past(i_wb_ack | i_wb_err | i_wb_rty))) |
| `SLAVE_ASSUME(i_wb_stb); |
| |
| always @(posedge i_clk) |
| if ((f_past_valid)&&(!$past(i_reset)) |
| &&($past(i_wb_stb))&&!$past(i_wb_ack|i_wb_err|i_wb_rty)) |
| begin |
| `SLAVE_ASSUME(i_wb_stb); |
| `SLAVE_ASSUME($stable(i_wb_we)); |
| `SLAVE_ASSUME($stable(i_wb_addr)); |
| `SLAVE_ASSUME($stable(i_wb_sel)); |
| `SLAVE_ASSUME($stable(i_wb_cti)); |
| `SLAVE_ASSUME($stable(i_wb_bte)); |
| if (i_wb_we) |
| `SLAVE_ASSUME($stable(i_wb_data)); |
| end |
| |
| // |
| // |
| // Bus responses |
| // |
| // |
| |
| // If STB (or CYC) was low on the last two clock cycles, then both |
| // ACK and ERR should be low on this clock cycle. |
| always @(posedge i_clk) |
| if ((f_past_valid)&&(!$past(i_wb_stb))&&(!i_wb_stb)) |
| begin |
| `SLAVE_ASSERT(!i_wb_ack); |
| `SLAVE_ASSERT(!i_wb_err); |
| `SLAVE_ASSERT(!i_wb_rty); |
| end else if (f_past_valid && $past(i_wb_ack|i_wb_err|i_wb_rty) |
| && !i_wb_stb) |
| begin |
| `SLAVE_ASSERT(!i_wb_ack); |
| `SLAVE_ASSERT(!i_wb_err); |
| `SLAVE_ASSERT(!i_wb_rty); |
| end |
| |
| // |
| // OPT_BUS_ABORT |
| // |
| // If CYC is dropped, this will abort the transaction in |
| // progress. Not all busses support this option, and it's |
| // not specifically called out in the spec. Therefore, we'll |
| // check if this is set (it will be clear by default) and |
| // prohibit a transaction from being aborted otherwise |
| always @(posedge i_clk) |
| if (f_past_valid && !$past(i_reset) && !OPT_BUS_ABORT |
| && $past(i_wb_stb && !(i_wb_ack|i_wb_err|i_wb_rty))) |
| `SLAVE_ASSUME(i_wb_stb); |
| |
| // |
| // No more than one of ACK, ERR or RTY may ever be true at a given time |
| always @(*) |
| begin |
| if (i_wb_ack) |
| `SLAVE_ASSERT(!i_wb_err && !i_wb_rty); |
| else if (i_wb_err) |
| `SLAVE_ASSERT(!i_wb_rty); |
| end |
| |
| localparam [2:0] C_CLASSIC = 3'b000; |
| localparam [2:0] C_FIXED = 3'b001; |
| localparam [2:0] C_INCR = 3'b010; |
| localparam [2:0] C_EOB = 3'b111; |
| localparam [1:0] B_LINEAR = 2'b00; |
| localparam [1:0] B_WRAP4 = 2'b01; |
| localparam [1:0] B_WRAP8 = 2'b10; |
| localparam [1:0] B_WRAP16 = 2'b11; |
| |
| // Burst address checking |
| always @(*) |
| if (i_wb_stb) |
| begin |
| // Several designations are reserved. Using those |
| // designations is "illegal". |
| assert(i_wb_cti != 3'b011); |
| assert(i_wb_cti != 3'b100); |
| assert(i_wb_cti != 3'b101); |
| assert(i_wb_cti != 3'b110); |
| end |
| |
| always @(posedge i_clk) |
| next_addr <= i_wb_addr + 1; |
| |
| always @(posedge i_clk) |
| if (f_past_valid && !$past(i_reset) && !i_reset |
| && $past(i_wb_stb)&&($past(i_wb_err|i_wb_rty|i_wb_ack)) |
| &&($past(i_wb_cti != C_CLASSIC))&&($past(i_wb_cti != C_EOB))) |
| begin |
| assert(i_wb_stb); |
| if ($past(i_wb_cti) == C_FIXED) |
| begin |
| assert($stable(i_wb_addr)); |
| assert((i_wb_cti == C_FIXED || i_wb_cti == C_EOB)); |
| end else if ($past(i_wb_cti == C_INCR)) |
| begin |
| assert($stable(i_wb_bte)); |
| case(i_wb_bte) |
| B_LINEAR: assert(i_wb_addr == next_addr); |
| B_WRAP4: begin |
| // 4-beat wrap burst |
| assert(i_wb_addr[1:0] == next_addr[1:0]); |
| assert($stable(i_wb_addr[AW-1:2])); |
| end |
| B_WRAP8: begin |
| // 8-beat wrap burst |
| assert(i_wb_addr[2:0] == next_addr[2:0]); |
| assert($stable(i_wb_addr[AW-1:3])); |
| end |
| B_WRAP16: begin |
| // 16-beat wrap burst |
| assert(i_wb_addr[3:0] == next_addr[3:0]); |
| assert($stable(i_wb_addr[AW-1:4])); |
| end |
| endcase |
| end |
| end |
| |
| generate if (F_MAX_DELAY > 0) |
| begin : DELAYCOUNT |
| // |
| // 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_ack && !i_wb_err && !i_wb_rty)) |
| f_stall_count <= f_stall_count + 1'b1; |
| else |
| f_stall_count <= 0; |
| |
| always @(*) |
| if (i_wb_cyc) |
| `SLAVE_ASSERT(f_stall_count < F_MAX_DELAY); |
| end endgenerate |
| |
| //////////////////////////////////////////////////////////////////////// |
| // |
| // Some basic cover properties |
| // |
| //////////////////////////////////////////////////////////////////////// |
| // |
| reg [3:0] ack_count; |
| |
| initial ack_count = 0; |
| always @(posedge i_clk) |
| if (i_reset || !i_wb_cyc) |
| ack_count <= 0; |
| else if (f_past_valid && i_wb_ack) |
| ack_count <= ack_count + 1; |
| |
| always @(*) |
| cover(!i_wb_cyc && ack_count > 4); |
| always @(*) |
| cover(!i_wb_cyc && ack_count > 3); |
| |
| endmodule |
| // |
| // Lest some other module want to use these macros, we undefine them here |
| `undef SLAVE_ASSUME |
| `undef SLAVE_ASSERT |