| Line 4... |
Line 4... |
//
|
//
|
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core
|
// Project: Zip CPU -- a small, lightweight, RISC CPU soft core
|
//
|
//
|
// Purpose: This is a very simple instruction fetch approach. It gets
|
// Purpose: This is a very simple instruction fetch approach. It gets
|
// one instruction at a time. Future versions should pipeline
|
// one instruction at a time. Future versions should pipeline
|
// fetches and perhaps even cache results--this doesn't do that.
|
// fetches and perhaps even cache results--this doesn't do that. It
|
// It should, however, be simple enough to get things running.
|
// should, however, be simple enough to get things running.
|
//
|
//
|
// The interface is fascinating. The 'i_pc' input wire is just
|
// The interface is fascinating. The 'i_pc' input wire is just a
|
// a suggestion of what to load. Other wires may be loaded
|
// suggestion of what to load. Other wires may be loaded instead. i_pc
|
// instead. i_pc is what must be output, not necessarily input.
|
// is what must be output, not necessarily input.
|
//
|
//
|
// 20150919 -- Added support for the WB error signal. When reading an
|
// 20150919 -- Added support for the WB error signal. When reading an
|
// instruction results in this signal being raised, the pipefetch
|
// instruction results in this signal being raised, the pipefetch module
|
// module will set an illegal instruction flag to be returned to
|
// will set an illegal instruction flag to be returned to the CPU together
|
// the CPU together with the instruction. Hence, the ZipCPU
|
// with the instruction. Hence, the ZipCPU can trap on it if necessary.
|
// can trap on it if necessary.
|
//
|
|
// 20171020 -- Added a formal proof to prove that the module works. This
|
|
// also involved adding a req_addr register, and the logic associated
|
|
// with it.
|
|
//
|
|
// 20171113 -- Removed the req_addr register, replacing it with a bus abort
|
|
// capability.
|
//
|
//
|
// Creator: Dan Gisselquist, Ph.D.
|
// Creator: Dan Gisselquist, Ph.D.
|
// Gisselquist Technology, LLC
|
// Gisselquist Technology, LLC
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
// Copyright (C) 2015,2017, Gisselquist Technology, LLC
|
// Copyright (C) 2015,2017-2019, Gisselquist Technology, LLC
|
//
|
//
|
// This program is free software (firmware): you can redistribute it and/or
|
// 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
|
// 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
|
// by the Free Software Foundation, either version 3 of the License, or (at
|
// your option) any later version.
|
// your option) any later version.
|
| Line 46... |
Line 52... |
//
|
//
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
// Flash requires a minimum of 4 clocks per byte to read, so that would be
|
`default_nettype none
|
// 4*(4bytes/32bit word) = 16 clocks per word read---and that's in pipeline
|
//
|
// mode which this prefetch does not support. In non--pipelined mode, the
|
//
|
// flash will require (16+6+6)*2 = 56 clocks plus 16 clocks per word read,
|
module prefetch(i_clk, i_reset, i_new_pc, i_clear_cache, i_stalled_n, i_pc,
|
// or 72 clocks to fetch one instruction.
|
o_insn, o_pc, o_valid, o_illegal,
|
module prefetch(i_clk, i_rst, i_new_pc, i_clear_cache, i_stalled_n, i_pc,
|
|
o_i, o_pc, o_valid, o_illegal,
|
|
o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
|
o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
|
i_wb_ack, i_wb_stall, i_wb_err, i_wb_data);
|
i_wb_ack, i_wb_stall, i_wb_err, i_wb_data);
|
parameter ADDRESS_WIDTH=32;
|
parameter ADDRESS_WIDTH=30, DATA_WIDTH=32;
|
localparam AW=ADDRESS_WIDTH;
|
localparam AW=ADDRESS_WIDTH,
|
input i_clk, i_rst, i_new_pc, i_clear_cache,
|
DW=DATA_WIDTH;
|
i_stalled_n;
|
input wire i_clk, i_reset;
|
input [(AW-1):0] i_pc;
|
// CPU interaction wires
|
output reg [31:0] o_i;
|
input wire i_new_pc, i_clear_cache, i_stalled_n;
|
output wire [(AW-1):0] o_pc;
|
// We ignore i_pc unless i_new_pc is true as well
|
output reg o_valid;
|
input wire [(AW+1):0] i_pc;
|
|
output reg [(DW-1):0] o_insn; // Instruction read from WB
|
|
output wire [(AW+1):0] o_pc; // Address of that instruction
|
|
output reg o_valid; // If the output is valid
|
|
output reg o_illegal; // Result is from a bus err
|
// Wishbone outputs
|
// Wishbone outputs
|
output reg o_wb_cyc, o_wb_stb;
|
output reg o_wb_cyc, o_wb_stb;
|
output wire o_wb_we;
|
output wire o_wb_we;
|
output reg [(AW-1):0] o_wb_addr;
|
output reg [(AW-1):0] o_wb_addr;
|
output wire [31:0] o_wb_data;
|
output wire [(DW-1):0] o_wb_data;
|
// And return inputs
|
// And return inputs
|
input i_wb_ack, i_wb_stall, i_wb_err;
|
input wire i_wb_ack, i_wb_stall, i_wb_err;
|
input [31:0] i_wb_data;
|
input wire [(DW-1):0] i_wb_data;
|
output reg o_illegal;
|
|
|
// Declare local variables
|
|
reg invalid;
|
|
|
|
// These are kind of obligatory outputs when dealing with a bus, that
|
|
// we'll set them here. Nothing's going to pay attention to these,
|
|
// though, this is primarily for form.
|
assign o_wb_we = 1'b0;
|
assign o_wb_we = 1'b0;
|
assign o_wb_data = 32'h0000;
|
assign o_wb_data = 32'h0000;
|
|
|
// Let's build it simple and upgrade later: For each instruction
|
// Let's build it simple and upgrade later: For each instruction
|
// we do one bus cycle to get the instruction. Later we should
|
// we do one bus cycle to get the instruction. Later we should
|
// pipeline this, but for now let's just do one at a time.
|
// pipeline this, but for now let's just do one at a time.
|
initial o_wb_cyc = 1'b0;
|
initial o_wb_cyc = 1'b0;
|
initial o_wb_stb = 1'b0;
|
initial o_wb_stb = 1'b0;
|
initial o_wb_addr= 0;
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((i_rst)||(i_wb_ack)||(i_wb_err))
|
if ((i_reset)||((o_wb_cyc)&&((i_wb_ack)||(i_wb_err))))
|
begin
|
begin
|
|
// End any bus cycle on a reset, or a return ACK
|
|
// or error.
|
o_wb_cyc <= 1'b0;
|
o_wb_cyc <= 1'b0;
|
o_wb_stb <= 1'b0;
|
o_wb_stb <= 1'b0;
|
end else if ((!o_wb_cyc)&&((i_stalled_n)||(!o_valid)))
|
end else if ((!o_wb_cyc)&&(
|
begin // Initiate a bus cycle
|
// Start if the last instruction output was
|
|
// accepted, *and* it wasn't a bus error
|
|
// response
|
|
((i_stalled_n)&&(!o_illegal))
|
|
// Start if the last bus result ended up
|
|
// invalid
|
|
||(invalid)
|
|
// Start on any request for a new address
|
|
||(i_new_pc)))
|
|
begin
|
|
// Initiate a bus transaction
|
o_wb_cyc <= 1'b1;
|
o_wb_cyc <= 1'b1;
|
o_wb_stb <= 1'b1;
|
o_wb_stb <= 1'b1;
|
end else if (o_wb_cyc) // Independent of ce
|
end else if (o_wb_cyc)
|
begin
|
begin
|
if (~i_wb_stall)
|
// If our request has been accepted, then drop the
|
|
// strobe line
|
|
if (!i_wb_stall)
|
o_wb_stb <= 1'b0;
|
o_wb_stb <= 1'b0;
|
|
|
|
// Abort on new-pc
|
|
// ... clear_cache is identical, save that it will
|
|
// immediately be followed by a new PC, so we don't
|
|
// need to worry about that other than to drop
|
|
// CYC and STB here.
|
|
if (i_new_pc)
|
|
begin
|
|
o_wb_cyc <= 1'b0;
|
|
o_wb_stb <= 1'b0;
|
|
end
|
end
|
end
|
|
|
reg invalid;
|
//
|
|
// If during the current bus request, a command came in from the CPU
|
|
// that will invalidate the results of that request, then we need to
|
|
// keep track of an "invalid" flag to remember that and so squash
|
|
// the result.
|
|
//
|
initial invalid = 1'b0;
|
initial invalid = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!o_wb_cyc)
|
if ((i_reset)||(!o_wb_cyc))
|
invalid <= 1'b0;
|
invalid <= 1'b0;
|
else if ((i_new_pc)||(i_clear_cache))
|
else if (i_new_pc)
|
invalid <= (!o_wb_stb);
|
invalid <= 1'b1;
|
|
|
|
// The wishbone request address, o_wb_addr
|
|
//
|
|
// The rule regarding this address is that it can *only* be changed
|
|
// when no bus request is active. Further, since the CPU is depending
|
|
// upon this value to know what "PC" is associated with the instruction
|
|
// it is processing, we can't change until either the CPU has accepted
|
|
// our result, or it is requesting a new PC (and hence not using the
|
|
// output).
|
|
//
|
|
initial o_wb_addr= 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_new_pc)
|
if (i_new_pc)
|
o_wb_addr <= i_pc;
|
o_wb_addr <= i_pc[AW+1:2];
|
else if ((!o_wb_cyc)&&(i_stalled_n)&&(!invalid))
|
else if ((o_valid)&&(i_stalled_n)&&(!o_illegal))
|
o_wb_addr <= o_wb_addr + 1'b1;
|
o_wb_addr <= o_wb_addr + 1'b1;
|
|
|
|
// The instruction returned is given by the data returned from the bus.
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((o_wb_cyc)&&(i_wb_ack))
|
if ((o_wb_cyc)&&(i_wb_ack))
|
o_i <= i_wb_data;
|
o_insn <= i_wb_data;
|
|
|
|
//
|
|
// Finally, the flags associated with the prefetch. The rule is that
|
|
// if the output represents a return from the bus, then o_valid needs
|
|
// to be true. o_illegal will be true any time the last bus request
|
|
// resulted in an error. o_illegal is only relevant to the CPU when
|
|
// o_valid is also true, hence o_valid will be true even in the case
|
|
// of a bus error in our request.
|
|
//
|
initial o_valid = 1'b0;
|
initial o_valid = 1'b0;
|
initial o_illegal = 1'b0;
|
initial o_illegal = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_rst)
|
if ((i_reset)||(i_new_pc)||(i_clear_cache))
|
begin
|
begin
|
|
// On any reset, request for a new PC (i.e. a branch),
|
|
// or a request to clear our cache (i.e. the data
|
|
// in memory may have changed), we invalidate any
|
|
// output.
|
o_valid <= 1'b0;
|
o_valid <= 1'b0;
|
o_illegal <= 1'b0;
|
o_illegal <= 1'b0;
|
end else if ((o_wb_cyc)&&(i_wb_ack))
|
end else if ((o_wb_cyc)&&((i_wb_ack)||(i_wb_err)))
|
begin
|
begin
|
o_valid <= (!i_wb_err)&&(!invalid);
|
// Otherwise, at the end of our bus cycle, the
|
o_illegal <= ( i_wb_err)&&(!invalid);
|
// answer will be valid. Well, not quite. If the
|
end else if ((i_stalled_n)||(i_clear_cache))
|
// user requested something mid-cycle (i_new_pc)
|
|
// or (i_clear_cache), then we'll have to redo the
|
|
// bus request, so we aren't valid.
|
|
//
|
|
o_valid <= 1'b1;
|
|
o_illegal <= ( i_wb_err);
|
|
end else if (i_stalled_n)
|
begin
|
begin
|
|
// Once the CPU accepts any result we produce, clear
|
|
// the valid flag, lest we send two identical
|
|
// instructions to the CPU.
|
|
//
|
o_valid <= 1'b0;
|
o_valid <= 1'b0;
|
o_illegal <= 1'b0;
|
//
|
|
// o_illegal doesn't change ... that way we don't
|
|
// access the bus again until a new address request
|
|
// is given to us, via i_new_pc, or we are asked
|
|
// to check again via i_clear_cache
|
|
//
|
|
// o_illegal <= (!i_stalled_n);
|
end
|
end
|
|
|
assign o_pc = o_wb_addr;
|
// The o_pc output shares its value with the (last) wishbone address
|
|
assign o_pc = { o_wb_addr, 2'b00 };
|
|
|
|
// Make verilator happy
|
|
// verilator lint_off UNUSED
|
|
wire [1:0] unused;
|
|
assign unused = i_pc[1:0];
|
|
// verilator lint_on UNUSED
|
|
`ifdef FORMAL
|
|
localparam F_LGDEPTH=2;
|
|
reg f_past_valid;
|
|
wire [(F_LGDEPTH-1):0] f_nreqs, f_nacks,
|
|
f_outstanding;
|
|
reg [(AW-1):0] f_last_pc;
|
|
reg f_last_pc_valid;
|
|
reg [(AW-1):0] f_req_addr;
|
|
|
|
//
|
|
//
|
|
// Generic setup
|
|
//
|
|
//
|
|
`ifdef PREFETCH
|
|
`define ASSUME assume
|
|
`else
|
|
`define ASSUME assert
|
|
`endif
|
|
|
|
// Assume a clock
|
|
|
|
// Keep track of a flag telling us whether or not $past()
|
|
// will return valid results
|
|
initial f_past_valid = 1'b0;
|
|
always @(posedge i_clk)
|
|
f_past_valid = 1'b1;
|
|
|
|
/////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assumptions about our inputs
|
|
//
|
|
//
|
|
/////////////////////////////////////////////////
|
|
|
|
// Assume we start from a reset condition
|
|
initial `ASSUME(i_reset);
|
|
always @(*)
|
|
if (!f_past_valid)
|
|
`ASSUME(i_reset);
|
|
// Some things to know from the CPU ... there will always be a
|
|
// i_new_pc request following any reset
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_reset)))
|
|
`ASSUME(i_new_pc);
|
|
|
|
// There will also be a i_new_pc request following any request to clear
|
|
// the cache.
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_clear_cache)))
|
|
`ASSUME(i_new_pc);
|
|
|
|
//
|
|
//
|
|
// Let's make some assumptions about how long it takes our
|
|
// phantom bus and phantom CPU to respond.
|
|
//
|
|
// These delays need to be long enough to flush out any potential
|
|
// errors, yet still short enough that the formal method doesn't
|
|
// take forever to solve.
|
|
//
|
|
localparam F_CPU_DELAY = 4;
|
|
reg [4:0] f_cpu_delay;
|
|
// First, let's assume that any response from the bus comes back
|
|
// within F_WB_DELAY clocks
|
|
|
|
// Here's our delay assumption: We'll assume that the
|
|
// wishbone will always respond within F_WB_DELAY clock ticks
|
|
// of the beginning of any cycle.
|
|
//
|
|
// This includes both dropping the stall line, as well as
|
|
// acknowledging any request. While this may not be
|
|
// a reasonable assumption for a piped master, it should
|
|
// work here for us.
|
|
|
|
// Count the number of clocks it takes the CPU to respond to our
|
|
// instruction.
|
|
always @(posedge i_clk)
|
|
// If no instruction is ready, then keep our counter at zero
|
|
if ((i_reset)||(!o_valid)||(i_stalled_n))
|
|
f_cpu_delay <= 0;
|
|
else
|
|
// Otherwise, count the clocks the CPU takes to respond
|
|
f_cpu_delay <= f_cpu_delay + 1'b1;
|
|
|
|
`ifdef PREFETCH
|
|
// Only *assume* that we are less than F_CPU_DELAY if we are not
|
|
// integrated into the CPU
|
|
always @(posedge i_clk)
|
|
assume(f_cpu_delay < F_CPU_DELAY);
|
|
`endif
|
|
|
|
fwb_master #(.AW(AW), .DW(DW),.F_LGDEPTH(F_LGDEPTH),
|
|
.F_MAX_REQUESTS(1), .F_OPT_SOURCE(1),
|
|
.F_OPT_RMW_BUS_OPTION(0),
|
|
.F_OPT_DISCONTINUOUS(0))
|
|
f_wbm(i_clk, i_reset,
|
|
o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data, 4'h0,
|
|
i_wb_ack, i_wb_stall, i_wb_data, i_wb_err,
|
|
f_nreqs, f_nacks, f_outstanding);
|
|
|
|
/////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assertions about our outputs
|
|
//
|
|
//
|
|
/////////////////////////////////////////////////
|
|
//
|
|
// Assertions about our wishbone control outputs first
|
|
// Prefetches don't write
|
|
always @(posedge i_clk)
|
|
if (o_wb_stb)
|
|
assert(!o_wb_we);
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(f_past_valid))
|
|
&&($past(i_clear_cache,2))
|
|
&&($past(o_wb_cyc,2)))
|
|
// Make sure any clear-cache transaction is aborted,
|
|
// *and* that no valid instructions get sent to the
|
|
// CPU
|
|
assert((!$past(o_wb_cyc))||(!o_wb_cyc));
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_valid))&&(o_valid))
|
|
assert(o_wb_addr == $past(o_wb_addr));
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(!i_reset))&&($past(invalid)))
|
|
assert(o_wb_cyc);
|
|
|
|
// Any time the CPU accepts an instruction, assert that on the
|
|
// valid line will be low on the next clock
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_valid))&&($past(i_stalled_n)))
|
|
assert(!o_valid);
|
|
|
|
// Since we only change our output on a response from the bus, we
|
|
// need to insist that the item has been read by the CPU before
|
|
// we go looking/asking for a next value.
|
|
//
|
|
// This routine should never be requesting a new instruction when
|
|
// one is valid--lest the CPU never accept the old instruction and we
|
|
// have nothing to do with the data when the bus request returns.
|
|
always @(*)
|
|
if (o_wb_cyc)
|
|
assert(!o_valid);
|
|
|
|
// If we just got a valid instruction from the wishbone, assert that
|
|
// the instruction is listed as valid on the next instruction cycle
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))
|
|
&&($past(o_wb_cyc))
|
|
&&($past(!i_clear_cache))
|
|
&&($past(i_wb_ack))&&(!$past(i_wb_err)))
|
|
begin
|
|
if (!invalid)
|
|
assert(o_valid);
|
|
end
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_clear_cache)))
|
|
assert(!o_valid);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(f_past_valid))
|
|
&&($past(i_clear_cache,2))
|
|
&&($past(o_wb_cyc,2)))
|
|
// Make sure any clear-cache transaction is aborted,
|
|
// *and* that no valid instructions get sent to the
|
|
// CPU
|
|
assert(!o_valid);
|
|
|
|
//
|
|
// Assertions about our return responses
|
|
//
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))
|
|
&&(!$past(i_new_pc))&&(!$past(i_clear_cache))
|
|
&&($past(o_valid))&&(!$past(i_stalled_n)))
|
|
assert(o_valid == $past(o_valid));
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_valid))&&(o_valid))
|
|
begin
|
|
assert($stable(o_pc));
|
|
assert($stable(o_insn));
|
|
assert($stable(o_illegal));
|
|
end
|
|
|
|
//
|
|
// The o_illegal line is the one we use to remind us not to go
|
|
// back and retry the last value if it returned a bus error. Hence,
|
|
// let's assert that this line stays constant any time o_wb_cyc
|
|
// is low, and we haven't received any new requests.
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))
|
|
&&(!$past(i_new_pc))&&(!$past(i_clear_cache))
|
|
&&($past(!o_wb_cyc)))
|
|
assert(o_illegal == $past(o_illegal));
|
|
|
|
|
|
//
|
|
//
|
|
// Let's examine whether or not we "walk" though PC addresses one
|
|
// at a time like we expect.
|
|
//
|
|
initial f_last_pc_valid = 1'b0;
|
|
always @(posedge i_clk)
|
|
if ((i_reset)||(i_clear_cache)||(i_new_pc)||(invalid))
|
|
f_last_pc_valid <= 1'b0;
|
|
else if (o_valid)
|
|
f_last_pc_valid <= (!o_illegal);
|
|
|
|
// initial f_last_pc = 0;
|
|
always @(posedge i_clk)
|
|
if (o_valid)
|
|
f_last_pc <= o_pc[AW+1:2];
|
|
else if (f_last_pc_valid)
|
|
assert(o_pc[AW+1:2] == f_last_pc + 1'b1);
|
|
|
|
always @(*)
|
|
assert(o_pc[1:0] == 2'b00);
|
|
|
|
// If we are producing a new result, and no new-pc or clear cache
|
|
// has come through (i.e. f_last_pc_valid is true), then the resulting
|
|
// PC should be one more than the last time.
|
|
//
|
|
// The o_valid && !$past(o_valid) is necessary because f_last_pc_valid
|
|
// will be different by the second o_valid.
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(o_valid)
|
|
&&(!$past(o_valid))&&(f_last_pc_valid))
|
|
assert(o_pc[AW+1:2] == (f_last_pc + 1'b1));
|
|
|
|
// Let's also keep track of the address the CPU wants us to return.
|
|
// Any time the CPU branches to a new_pc, we'll record that request.
|
|
// Likewise, any time an instruction is returned from the bus,
|
|
// we'll increment this address so as to automatically walk through
|
|
// memory.
|
|
//
|
|
always @(*)
|
|
assume(i_pc[1:0] == 2'b00);
|
|
initial f_req_addr = 0;
|
|
always @(posedge i_clk)
|
|
if (i_new_pc)
|
|
f_req_addr <= i_pc[AW+1:2];
|
|
else if ((!invalid)&&(o_wb_cyc)&&(i_wb_ack)&&(!i_wb_err))
|
|
f_req_addr <= f_req_addr + 1'b1;
|
|
|
|
// Let's also keep the formal methods on track. Any time we are
|
|
// requesting a value, it should either be from the req_addr, or if
|
|
// not a new value should've come in rendering this one invalid.
|
|
always @(posedge i_clk)
|
|
if (o_wb_cyc)
|
|
assert((invalid)||(f_req_addr == o_wb_addr));
|
|
// This isn't good enough for induction, so we'll need to
|
|
// constrain this further
|
|
else if ((!o_valid)&&(!i_new_pc)&&(!i_reset))
|
|
assert(f_req_addr == o_wb_addr);
|
|
|
|
// In this version, invalid should only ever be high for one cycle.
|
|
// CYC should be high on the cycle following--if ever.
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(invalid)))
|
|
assert(!invalid);
|
|
|
|
(* anyconst *) reg [AW:0] const_addr;
|
|
(* anyconst *) reg [DW-1:0] const_insn;
|
|
|
|
wire f_this_addr, f_this_pc, f_this_req, f_this_data;
|
|
assign f_this_addr = (o_wb_addr == const_addr[AW-1:0]);
|
|
assign f_this_pc = (o_pc == { const_addr[AW-1:0], 2'b00 });
|
|
assign f_this_req = (i_pc == { const_addr[AW-1:0], 2'b00 });
|
|
assign f_this_data = (i_wb_data == const_insn);
|
|
|
|
reg f_addr_pending;
|
|
initial f_addr_pending = 1'b0;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
f_addr_pending <= 1'b0;
|
|
else if (!o_wb_cyc)
|
|
f_addr_pending <= 1'b0;
|
|
else if ((o_wb_stb)&&(f_this_addr))
|
|
begin
|
|
if ((!i_wb_ack)&&(!i_wb_err))
|
|
f_addr_pending <= 1'b1;
|
|
end
|
|
|
|
always @(*)
|
|
if ((o_wb_stb)&&(f_this_addr)&&(!i_wb_stall))
|
|
begin
|
|
if (!const_addr[AW])
|
|
assume(!i_wb_err);
|
|
else
|
|
assume(!i_wb_ack);
|
|
if (i_wb_ack)
|
|
assume(f_this_data);
|
|
end else if ((o_wb_cyc)&&(f_addr_pending))
|
|
begin
|
|
if (!const_addr[AW])
|
|
assume(!i_wb_err);
|
|
else
|
|
assume(!i_wb_ack);
|
|
if (i_wb_ack)
|
|
assume(f_this_data);
|
|
end
|
|
|
|
always @(*)
|
|
if ((o_valid)&&(f_this_pc)&&(!o_illegal))
|
|
assert(o_insn == const_insn);
|
|
always @(*)
|
|
if ((o_valid)&&(f_this_pc))
|
|
assert(o_illegal == const_addr[AW]);
|
|
|
|
reg f_insn_pending;
|
|
|
|
initial f_insn_pending = 1'b0;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
f_insn_pending <= 1'b0;
|
|
else if (i_clear_cache)
|
|
f_insn_pending <= 1'b0;
|
|
else if ((i_new_pc)&&(f_this_req))
|
|
f_insn_pending <= 1'b1;
|
|
else if ((o_valid)||(i_new_pc))
|
|
f_insn_pending <= 1'b0;
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_wb_cyc))&&(o_wb_cyc)&&(f_insn_pending))
|
|
assert(f_this_pc);
|
|
|
|
always @(posedge i_clk)
|
|
if (((f_past_valid)&&($past(o_wb_cyc))&&($past(f_insn_pending)))
|
|
&&(!$past(i_reset))&&(!$past(i_clear_cache))
|
|
&&(!$past(i_new_pc)))
|
|
begin
|
|
if(!o_wb_cyc)
|
|
assert((o_valid)&&(f_this_pc));
|
|
end
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(o_wb_cyc))&&(!o_wb_cyc))
|
|
assert(!f_insn_pending);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_wb_cyc))&&(o_wb_cyc)&&(f_this_addr))
|
|
assert(f_addr_pending);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_wb_cyc))&&(f_insn_pending))
|
|
assert(f_this_addr);
|
|
`endif
|
endmodule
|
endmodule
|
|
//
|
|
// Usage: (this) (mid) (past)
|
|
// Cells 167 230 175
|
|
// FDRE 67 97 69
|
|
// LUT1 1 1 1
|
|
// LUT2 1 3 3
|
|
// LUT3 31 63 33
|
|
// LUT4 5 3 3
|
|
// LUT5 1 3 3
|
|
// LUT6 2 1 3
|
|
// MUXCY 29 29 31
|
|
// XORCY 30 30 32
|
|
|
No newline at end of file
|
No newline at end of file
|
