| 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 one step beyond the simplest instruction fetch,
|
// Purpose: This is one step beyond the simplest instruction fetch,
|
// prefetch.v. dblfetch.v uses memory pipelining to fetch two
|
// prefetch.v. dblfetch.v uses memory pipelining to fetch two
|
// instruction words in one cycle, figuring that the unpipelined CPU can't
|
// (or more) instruction words in one bus cycle. If the CPU consumes
|
// go through both at once, but yet recycles itself fast enough for the
|
// either of these before the bus cycle completes, a new request will be
|
// next instruction that would follow. It is designed to be a touch
|
// made of the bus. In this way, we can keep the CPU filled in spite
|
// faster than the single instruction prefetch, although not as fast as
|
// of a (potentially) slow memory operation. The bus request will end
|
// the prefetch and cache found elsewhere.
|
// when both requests have been sent and both result locations are empty.
|
//
|
//
|
// There are some gotcha's in this logic, however. For example, it's
|
// This routine is designed to be a touch faster than the single
|
// illegal to switch devices mid-transaction, since the second device
|
// instruction prefetch (prefetch.v), although not as fast as the
|
// might have different timing. I.e. the first device might take 8
|
// prefetch and cache approach found elsewhere (pfcache.v).
|
// clocks to create an ACK, and the second device might take 2 clocks, the
|
|
// acks might therefore come on top of each other, or even out of order.
|
|
// But ... in order to keep logic down, we keep track of the PC in the
|
|
// o_wb_addr register. Hence, this register gets changed on any i_new_pc.
|
|
// The i_pc value associated with i_new_pc will only be valid for one
|
|
// clock, hence we can't wait to change. To keep from violating the WB
|
|
// rule, therefore, we *must* immediately stop requesting any transaction,
|
|
// and then terminate the bus request as soon as possible.
|
|
//
|
|
// This has consequences in terms of logic used, leaving this routine
|
|
// anything but simple--even though the number of wires affected by
|
|
// this is small (o_wb_cyc, o_wb_stb, and last_ack).
|
|
//
|
//
|
|
// 20180222: Completely rebuilt.
|
//
|
//
|
// Creator: Dan Gisselquist, Ph.D.
|
// Creator: Dan Gisselquist, Ph.D.
|
// Gisselquist Technology, LLC
|
// Gisselquist Technology, LLC
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
// Copyright (C) 2017, Gisselquist Technology, LLC
|
// Copyright (C) 2017-2019, Gisselquist Technology, LLC
|
//
|
//
|
// This program is free software (firmware): you can redistribute it and/or
|
// 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 56... |
Line 45... |
//
|
//
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
module dblfetch(i_clk, i_rst, i_new_pc, i_clear_cache,
|
`default_nettype none
|
i_stall_n, i_pc, o_i, o_pc, o_v,
|
//
|
|
module dblfetch(i_clk, i_reset, i_new_pc, i_clear_cache,
|
|
i_stall_n, i_pc, o_insn, o_pc, o_valid,
|
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,
|
o_illegal);
|
o_illegal);
|
parameter ADDRESS_WIDTH=32, AUX_WIDTH = 1;
|
parameter ADDRESS_WIDTH=30, AUX_WIDTH = 1;
|
localparam AW=ADDRESS_WIDTH;
|
localparam AW=ADDRESS_WIDTH, DW = 32;
|
input i_clk, i_rst, i_new_pc, i_clear_cache,
|
input wire i_clk, i_reset, i_new_pc, i_clear_cache,
|
i_stall_n;
|
i_stall_n;
|
input [(AW-1):0] i_pc;
|
input wire [(AW+1):0] i_pc;
|
output reg [31:0] o_i;
|
output reg [(DW-1):0] o_insn;
|
output reg [(AW-1):0] o_pc;
|
output reg [(AW+1):0] o_pc;
|
output wire o_v;
|
output reg o_valid;
|
// 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;
|
// And ... the result if we got an error
|
// And ... the result if we got an error
|
output reg o_illegal;
|
output reg o_illegal;
|
|
|
assign o_wb_we = 1'b0;
|
assign o_wb_we = 1'b0;
|
assign o_wb_data = 32'h0000;
|
assign o_wb_data = 32'h0000;
|
|
|
reg last_ack, last_stb, invalid_bus_cycle;
|
reg last_stb, invalid_bus_cycle;
|
|
|
reg [31:0] cache [0:1];
|
reg [(DW-1):0] cache_word;
|
reg cache_read_addr, cache_write_addr;
|
reg cache_valid;
|
reg [1:0] cache_valid;
|
reg [1:0] inflight;
|
|
reg cache_illegal;
|
|
|
initial o_wb_cyc = 1'b0;
|
initial o_wb_cyc = 1'b0;
|
initial o_wb_stb = 1'b0;
|
initial o_wb_stb = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((i_rst)||(i_wb_err))
|
if ((i_reset)||((o_wb_cyc)&&(i_wb_err)))
|
begin
|
begin
|
o_wb_cyc <= 1'b0;
|
o_wb_cyc <= 1'b0;
|
o_wb_stb <= 1'b0;
|
o_wb_stb <= 1'b0;
|
// last_stb <= 1'b0;
|
|
// last_ack <= 1'b0;
|
|
end else if (o_wb_cyc)
|
end else if (o_wb_cyc)
|
begin
|
begin
|
if ((o_wb_stb)&&(!i_wb_stall))
|
if ((!o_wb_stb)||(!i_wb_stall))
|
begin
|
o_wb_stb <= (!last_stb);
|
// last_stb <= 1'b1;
|
|
o_wb_stb <= !last_stb;
|
|
end
|
|
// if (i_wb_ack)
|
|
// last_ack <= 1'b1;
|
|
if ((i_new_pc)||(invalid_bus_cycle))
|
|
o_wb_stb <= 1'b0;
|
|
|
|
if ((i_wb_ack)&&(
|
|
// Relase the bus on the second ack
|
// Relase the bus on the second ack
|
(last_ack)
|
if (((i_wb_ack)&&(!o_wb_stb)&&(inflight<=1))
|
// Or on the first ACK, if we've been told
|
||((!o_wb_stb)&&(inflight == 0))
|
// we have an invalid bus cycle
|
// Or any new transaction request
|
||((o_wb_stb)&&(i_wb_stall)&&(last_stb)&&(
|
||((i_new_pc)||(i_clear_cache)))
|
(i_new_pc)||(invalid_bus_cycle)))
|
|
))
|
|
begin
|
begin
|
o_wb_cyc <= 1'b0;
|
o_wb_cyc <= 1'b0;
|
o_wb_stb <= 1'b0;
|
o_wb_stb <= 1'b0;
|
end
|
end
|
|
|
if ((!last_stb)&&(i_wb_stall)&&((i_new_pc)||(invalid_bus_cycle)))
|
end else if ((i_new_pc)||(invalid_bus_cycle)
|
// Also release the bus with no acks, if we
|
||((o_valid)&&(i_stall_n)&&(!o_illegal)))
|
// haven't made any requests
|
|
begin
|
|
o_wb_cyc <= 1'b0;
|
|
o_wb_stb <= 1'b0;
|
|
end
|
|
end else if ((invalid_bus_cycle)
|
|
||((o_v)&&(i_stall_n)&&(cache_read_addr))) // Initiate a bus cycle
|
|
begin
|
begin
|
|
// Initiate a bus cycle if ... the last bus cycle was
|
|
// aborted (bus error or new_pc), we've been given a
|
|
// new PC to go get, or we just exhausted our one
|
|
// instruction cache
|
o_wb_cyc <= 1'b1;
|
o_wb_cyc <= 1'b1;
|
o_wb_stb <= 1'b1;
|
o_wb_stb <= 1'b1;
|
// last_stb <= 1'b0;
|
|
// last_ack <= 1'b0;
|
|
end
|
end
|
|
|
initial last_stb = 1'b0;
|
initial inflight = 2'b00;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((o_wb_cyc)&&(o_wb_stb)&&(!i_wb_stall))
|
if (!o_wb_cyc)
|
last_stb <= 1'b1;
|
inflight <= 2'b00;
|
else if (!o_wb_cyc)
|
else begin
|
last_stb <= 1'b0;
|
case({ ((o_wb_stb)&&(!i_wb_stall)), i_wb_ack })
|
|
2'b01: inflight <= inflight - 1'b1;
|
|
2'b10: inflight <= inflight + 1'b1;
|
|
// If neither ack nor request, then no change. Likewise
|
|
// if we have both an ack and a request, there's no change
|
|
// in the number of requests in flight.
|
|
default: begin end
|
|
endcase
|
|
end
|
|
|
initial last_ack = 1'b0;
|
always @(*)
|
always @(posedge i_clk)
|
last_stb = (inflight != 2'b00)||((o_valid)&&(!i_stall_n));
|
if ((o_wb_cyc)&&(i_wb_ack))
|
|
last_ack <= 1'b1;
|
|
else if ((o_wb_cyc)&&(o_wb_stb)&&(i_wb_stall)&&(
|
|
(i_new_pc)||(invalid_bus_cycle)))
|
|
last_ack <= 1'b1;
|
|
else if ((o_wb_cyc)&&(o_wb_stb)&&(!i_wb_stall)&&(!last_stb)&&(
|
|
(i_new_pc)||(invalid_bus_cycle)))
|
|
last_ack <= 1'b1;
|
|
else if (!o_wb_cyc)
|
|
last_ack <= 1'b0;
|
|
|
|
initial invalid_bus_cycle = 1'b0;
|
initial invalid_bus_cycle = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_rst)
|
if ((o_wb_cyc)&&(i_new_pc))
|
invalid_bus_cycle <= 1'b0;
|
|
else if ((i_new_pc)||(i_clear_cache))
|
|
invalid_bus_cycle <= 1'b1;
|
invalid_bus_cycle <= 1'b1;
|
else if (!o_wb_cyc)
|
else if (!o_wb_cyc)
|
invalid_bus_cycle <= 1'b0;
|
invalid_bus_cycle <= 1'b0;
|
|
|
initial o_wb_addr = {(AW){1'b1}};
|
initial o_wb_addr = {(AW){1'b1}};
|
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_stb)&&(!i_wb_stall)&&(!invalid_bus_cycle))
|
else if ((o_wb_stb)&&(!i_wb_stall))
|
o_wb_addr <= o_wb_addr + 1'b1;
|
o_wb_addr <= o_wb_addr + 1'b1;
|
|
|
initial cache_write_addr = 1'b0;
|
//////////////////
|
|
//
|
|
// Now for the immediate output word to the CPU
|
|
//
|
|
//////////////////
|
|
|
|
initial o_valid = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (!o_wb_cyc)
|
if ((i_reset)||(i_new_pc)||(i_clear_cache))
|
cache_write_addr <= 1'b0;
|
o_valid <= 1'b0;
|
else if ((o_wb_cyc)&&(i_wb_ack))
|
else if ((o_wb_cyc)&&((i_wb_ack)||(i_wb_err)))
|
cache_write_addr <= cache_write_addr + 1'b1;
|
o_valid <= 1'b1;
|
|
else if (i_stall_n)
|
|
o_valid <= cache_valid;
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((o_wb_cyc)&&(i_wb_ack))
|
if ((!o_valid)||(i_stall_n))
|
cache[cache_write_addr] <= i_wb_data;
|
begin
|
|
if (cache_valid)
|
|
o_insn <= cache_word;
|
|
else
|
|
o_insn <= i_wb_data;
|
|
end
|
|
|
initial cache_read_addr = 1'b0;
|
initial o_pc[1:0] = 2'b00;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((i_new_pc)||(invalid_bus_cycle)
|
if (i_new_pc)
|
||((o_v)&&(cache_read_addr)&&(i_stall_n)))
|
o_pc <= i_pc;
|
cache_read_addr <= 1'b0;
|
else if ((o_valid)&&(i_stall_n))
|
else if ((o_v)&&(i_stall_n))
|
o_pc[AW+1:2] <= o_pc[AW+1:2] + 1'b1;
|
cache_read_addr <= 1'b1;
|
|
|
|
|
initial o_illegal = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((i_new_pc)||(invalid_bus_cycle))
|
if ((i_reset)||(i_new_pc)||(i_clear_cache))
|
cache_valid <= 2'b00;
|
o_illegal <= 1'b0;
|
|
else if ((!o_valid)||(i_stall_n))
|
|
begin
|
|
if (cache_valid)
|
|
o_illegal <= (o_illegal)||(cache_illegal);
|
|
else if ((o_wb_cyc)&&(i_wb_err))
|
|
o_illegal <= 1'b1;
|
|
end
|
|
|
|
|
|
//////////////////
|
|
//
|
|
// Now for the output/cached word
|
|
//
|
|
//////////////////
|
|
|
|
initial cache_valid = 1'b0;
|
|
always @(posedge i_clk)
|
|
if ((i_reset)||(i_new_pc)||(i_clear_cache))
|
|
cache_valid <= 1'b0;
|
else begin
|
else begin
|
if ((o_v)&&(i_stall_n))
|
if ((o_valid)&&(o_wb_cyc)&&((i_wb_ack)||(i_wb_err)))
|
cache_valid[cache_read_addr] <= 1'b0;
|
cache_valid <= (!i_stall_n)||(cache_valid);
|
|
else if (i_stall_n)
|
|
cache_valid <= 1'b0;
|
|
end
|
|
|
|
always @(posedge i_clk)
|
if ((o_wb_cyc)&&(i_wb_ack))
|
if ((o_wb_cyc)&&(i_wb_ack))
|
cache_valid[cache_write_addr] <= 1'b1;
|
cache_word <= i_wb_data;
|
|
|
|
initial cache_illegal = 1'b0;
|
|
always @(posedge i_clk)
|
|
if ((i_reset)||(i_clear_cache)||(i_new_pc))
|
|
cache_illegal <= 1'b0;
|
|
else if ((o_wb_cyc)&&(i_wb_err)&&(o_valid)&&(!i_stall_n))
|
|
cache_illegal <= 1'b1;
|
|
//
|
|
// Some of these properties can be done in yosys-smtbmc, *or* Verilator
|
|
//
|
|
// Ver1lator is different from yosys, however, in that Verilator doesn't support
|
|
// the $past() directive. Further, any `assume`'s turn into `assert()`s
|
|
// within Verilator. We can use this to help prove that the properties
|
|
// of interest truly hold, and that any contracts we create or assumptions we
|
|
// make truly hold in practice (i.e. in simulation).
|
|
//
|
|
`ifdef FORMAL
|
|
`define VERILATOR_FORMAL
|
|
`else
|
|
`ifdef VERILATOR
|
|
//
|
|
// Define VERILATOR_FORMAL here to have Verilator check your formal properties
|
|
// during simulation. assert() and assume() statements will both have the
|
|
// same effect within VERILATOR of causing your simulation to suddenly end.
|
|
//
|
|
// I have this property commented because it only works on the newest versions
|
|
// of Verilator (3.9 something and later), and I tend to still use Verilator
|
|
// 3.874.
|
|
//
|
|
// `define VERILATOR_FORMAL
|
|
`endif
|
|
`endif
|
|
|
|
`ifdef VERILATOR_FORMAL
|
|
// Keep track of a flag telling us whether or not $past()
|
|
// will return valid results
|
|
reg f_past_valid;
|
|
initial f_past_valid = 1'b0;
|
|
always @(posedge i_clk)
|
|
f_past_valid = 1'b1;
|
|
|
|
// Keep track of some alternatives to $past that can still be used
|
|
// in a VERILATOR environment
|
|
reg f_past_reset, f_past_clear_cache, f_past_o_valid,
|
|
f_past_stall_n;
|
|
|
|
initial f_past_reset = 1'b1;
|
|
initial f_past_clear_cache = 1'b0;
|
|
initial f_past_o_valid = 1'b0;
|
|
initial f_past_stall_n = 1'b1;
|
|
always @(posedge i_clk)
|
|
begin
|
|
f_past_reset <= i_reset;
|
|
f_past_clear_cache <= i_clear_cache;
|
|
f_past_o_valid <= o_valid;
|
|
f_past_stall_n <= i_stall_n;
|
end
|
end
|
|
`endif
|
|
|
initial o_i = {(32){1'b1}};
|
`ifdef FORMAL
|
|
//
|
|
//
|
|
// Generic setup
|
|
//
|
|
//
|
|
`ifdef DBLFETCH
|
|
`define ASSUME assume
|
|
`else
|
|
`define ASSUME assert
|
|
`endif
|
|
|
|
/////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assumptions about our inputs
|
|
//
|
|
//
|
|
/////////////////////////////////////////////////
|
|
|
|
always @(*)
|
|
if (!f_past_valid)
|
|
`ASSUME(i_reset);
|
|
|
|
//
|
|
// Assume that resets, new-pc commands, and clear-cache commands
|
|
// are never more than pulses--one clock wide at most.
|
|
//
|
|
// It may be that the CPU treats us differently. We'll only restrict
|
|
// our solver to this here.
|
|
/*
|
|
always @(posedge i_clk)
|
|
if (f_past_valid)
|
|
begin
|
|
if (f_past_reset)
|
|
restrict(!i_reset);
|
|
if ($past(i_new_pc))
|
|
restrict(!i_new_pc);
|
|
end
|
|
*/
|
|
|
|
//
|
|
// Assume we start from a reset condition
|
|
initial assume(i_reset);
|
|
|
|
/////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Wishbone bus properties
|
|
//
|
|
//
|
|
/////////////////////////////////////////////////
|
|
|
|
localparam F_LGDEPTH=2;
|
|
wire [(F_LGDEPTH-1):0] f_nreqs, f_nacks, f_outstanding;
|
|
|
|
//
|
|
// Add a bunch of wishbone-based asserts
|
|
fwb_master #(.AW(AW), .DW(DW), .F_LGDEPTH(F_LGDEPTH),
|
|
.F_MAX_STALL(2),
|
|
.F_MAX_REQUESTS(0), .F_OPT_SOURCE(1),
|
|
.F_OPT_RMW_BUS_OPTION(1),
|
|
.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);
|
|
|
|
`endif
|
|
|
|
//
|
|
// Now, apply the following to Verilator *or* yosys-smtbmc
|
|
//
|
|
`ifdef VERILATOR_FORMAL
|
|
/////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assumptions about our interaction with the CPU
|
|
//
|
|
//
|
|
/////////////////////////////////////////////////
|
|
|
|
// Assume that any reset is either accompanied by a new address,
|
|
// or a new address immediately follows it.
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(f_past_reset))
|
|
assume(i_new_pc);
|
|
|
|
always @(posedge i_clk)
|
|
if (f_past_clear_cache)
|
|
assume(!i_clear_cache);
|
|
|
|
//
|
|
//
|
|
// The bottom two bits of the PC address register are always zero.
|
|
// They are there to make examining traces easier, but I expect
|
|
// the synthesis tool to remove them.
|
|
//
|
|
always @(*)
|
|
assume(i_pc[1:0] == 2'b00);
|
|
|
|
// 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)&&(f_past_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)&&(f_past_clear_cache))
|
|
assume(i_new_pc);
|
|
|
|
always @(posedge i_clk)
|
|
if (f_past_clear_cache)
|
|
assume(!i_clear_cache);
|
|
|
|
always @(*)
|
|
assume(i_pc[1:0] == 2'b00);
|
|
`endif
|
|
|
|
`ifdef FORMAL
|
|
//
|
|
// Let's make some assumptions about how long it takes our phantom
|
|
// (i.e. assumed) CPU to respond.
|
|
//
|
|
// This delay needs to be long enough to flush out any potential
|
|
// errors, yet still short enough that the formal method doesn't
|
|
// take forever to solve.
|
|
//
|
|
`ifdef DBLFETCH
|
|
localparam F_CPU_DELAY = 4;
|
|
reg [4:0] f_cpu_delay;
|
|
|
|
// Now, let's look at the delay the CPU takes to accept an instruction.
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((i_stall_n)&&(o_wb_cyc)&&(i_wb_ack))
|
// If no instruction is ready, then keep our counter at zero
|
o_i <= i_wb_data;
|
if ((!o_valid)||(i_stall_n))
|
|
f_cpu_delay <= 0;
|
else
|
else
|
o_i <= cache[cache_read_addr];
|
// Otherwise, count the clocks the CPU takes to respond
|
|
f_cpu_delay <= f_cpu_delay + 1'b1;
|
|
|
initial o_pc = 0;
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_new_pc)
|
assume(f_cpu_delay < F_CPU_DELAY);
|
o_pc <= i_pc;
|
`endif
|
else if ((o_v)&&(i_stall_n))
|
|
o_pc <= o_pc + 1'b1;
|
|
|
|
assign o_v = cache_valid[cache_read_addr];
|
|
|
|
initial o_illegal = 1'b0;
|
|
|
/////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assertions about our outputs
|
|
//
|
|
//
|
|
/////////////////////////////////////////////////
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((o_wb_cyc)&&(i_wb_err))
|
if ((f_past_valid)&&($past(o_wb_stb))&&(!$past(i_wb_stall))
|
o_illegal <= 1'b1;
|
&&(!$past(i_new_pc)))
|
else if ((!o_wb_cyc)&&((i_new_pc)||(invalid_bus_cycle)))
|
assert(o_wb_addr <= $past(o_wb_addr)+1'b1);
|
o_illegal <= 1'b0;
|
|
|
|
|
//
|
|
// Assertions about our return responses to the CPU
|
|
//
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))
|
|
&&(!$past(i_new_pc))&&(!$past(i_clear_cache))
|
|
&&($past(o_valid))&&(!$past(i_stall_n)))
|
|
begin
|
|
assert($stable(o_pc));
|
|
assert($stable(o_insn));
|
|
assert($stable(o_valid));
|
|
assert($stable(o_illegal));
|
|
end
|
|
|
|
// The same is true of the cache as well.
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))
|
|
&&(!$past(i_new_pc))&&(!$past(i_clear_cache))
|
|
&&($past(o_valid))&&(!$past(i_stall_n))
|
|
&&($past(cache_valid)))
|
|
begin
|
|
assert($stable(cache_valid));
|
|
assert($stable(cache_word));
|
|
assert($stable(cache_illegal));
|
|
end
|
|
|
|
// Consider it invalid to present the CPU with the same instruction
|
|
// twice in a row. Any effort to present the CPU with the same
|
|
// instruction twice in a row must go through i_new_pc, and thus a
|
|
// new bus cycle--hence the assertion below makes sense.
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_new_pc))
|
|
&&($past(o_valid))&&($past(i_stall_n)))
|
|
assert(o_pc[AW+1:2] == $past(o_pc[AW+1:2])+1'b1);
|
|
|
|
|
|
//
|
|
// As with i_pc[1:0], the bottom two bits of the address are unused.
|
|
// Let's assert here that they remain zero.
|
|
always @(*)
|
|
assert(o_pc[1:0] == 2'b00);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))
|
|
&&(!$past(i_new_pc))
|
|
&&(!$past(i_clear_cache))
|
|
&&($past(o_wb_cyc))&&($past(i_wb_err)))
|
|
assert( ((o_valid)&&(o_illegal))
|
|
||((cache_valid)&&(cache_illegal)) );
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(o_illegal))&&(o_illegal))
|
|
assert(o_valid);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(cache_illegal))&&(!cache_valid))
|
|
assert(!cache_illegal);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_new_pc)))
|
|
assert(!o_valid);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(i_clear_cache))
|
|
&&($past(o_valid))&&(!o_valid)&&(!o_illegal))
|
|
assert((o_wb_cyc)||(invalid_bus_cycle));
|
|
|
|
/////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Our "contract" with the CPU
|
|
//
|
|
//
|
|
/////////////////////////////////////////////////
|
|
//
|
|
// For any particular address, that address is associated with an
|
|
// instruction and a flag regarding whether or not it is illegal.
|
|
//
|
|
// Any attempt to return to the CPU a value from this address,
|
|
// must return the value and the illegal flag.
|
|
//
|
|
(* anyconst *) reg [AW-1:0] f_const_addr;
|
|
(* anyconst *) reg [DW-1:0] f_const_insn;
|
|
(* anyconst *) reg f_const_illegal;
|
|
|
|
//
|
|
// While these wires may seem like overkill, and while they make the
|
|
// following logic perhaps a bit more obscure, these predicates make
|
|
// it easier to follow the complex logic on a scope. They don't
|
|
// affect anything synthesized.
|
|
//
|
|
wire f_this_addr, f_this_pc, f_this_req, f_this_data,
|
|
f_this_insn;
|
|
|
|
assign f_this_addr = (o_wb_addr == f_const_addr);
|
|
assign f_this_pc = (o_pc == { f_const_addr, 2'b00 });
|
|
assign f_this_req = (i_pc == { f_const_addr, 2'b00 });
|
|
assign f_this_data = (i_wb_data == f_const_insn);
|
|
assign f_this_insn = (o_insn == f_const_insn);
|
|
|
|
|
|
//
|
|
//
|
|
// Here's our contract:
|
|
//
|
|
// Any time we return a value for the address above, it *must* be
|
|
// the "right" value.
|
|
//
|
|
always @(*)
|
|
if ((o_valid)&&(f_this_pc))
|
|
begin
|
|
if (f_const_illegal)
|
|
assert(o_illegal);
|
|
if (!o_illegal)
|
|
assert(f_this_insn);
|
|
end
|
|
|
|
//
|
|
// The contract will only work if we assume the return from the
|
|
// bus at this address will be the right return.
|
|
wire f_this_return;
|
|
assign f_this_return = (o_wb_addr - f_outstanding == f_const_addr);
|
|
always @(*)
|
|
if ((o_wb_cyc)&&(f_this_return))
|
|
begin
|
|
if (i_wb_ack)
|
|
assume(i_wb_data == f_const_insn);
|
|
|
|
if (f_const_illegal)
|
|
assume(!i_wb_ack);
|
|
else
|
|
assume(!i_wb_err);
|
|
end
|
|
|
|
//
|
|
// Here is a corrollary to our contract. Anything in the one-word
|
|
// cache must also match the contract as well.
|
|
//
|
|
always @(*)
|
|
if ((o_pc[AW+1:2] + 1'b1 == f_const_addr)&&(cache_valid))
|
|
begin
|
|
if (!cache_illegal)
|
|
assert(cache_word == f_const_insn);
|
|
|
|
if (f_const_illegal)
|
|
assert(cache_illegal);
|
|
end
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(cache_illegal))&&(!cache_valid))
|
|
assert(!cache_illegal);
|
|
|
|
////////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Additional assertions necessary to pass induction
|
|
//
|
|
//
|
|
////////////////////////////////////////////////////////
|
|
//
|
|
// We have only a one word cache. Hence, we shouldn't be asking
|
|
// for more data any time we have nowhere to put it.
|
|
always @(*)
|
|
if (o_wb_stb)
|
|
assert((!cache_valid)||(i_stall_n));
|
|
|
|
always @(*)
|
|
if ((o_valid)&&(cache_valid))
|
|
assert((f_outstanding == 0)&&(!o_wb_stb));
|
|
|
|
always @(*)
|
|
if ((o_valid)&&(!i_stall_n))
|
|
assert(f_outstanding < 2);
|
|
|
|
always @(*)
|
|
if ((!o_valid)||(i_stall_n))
|
|
assert(f_outstanding <= 2);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_wb_cyc))&&(!$past(o_wb_stb))
|
|
&&(o_wb_cyc))
|
|
assert(inflight != 0);
|
|
|
|
always @(*)
|
|
if ((o_wb_cyc)&&(i_wb_ack))
|
|
assert(!cache_valid);
|
|
|
|
always @(posedge i_clk)
|
|
if (o_wb_cyc)
|
|
assert(inflight == f_outstanding);
|
|
|
|
wire [AW-1:0] this_return_address,
|
|
next_pc_address;
|
|
assign this_return_address = o_wb_addr - f_outstanding;
|
|
assign next_pc_address = o_pc[AW+1:2] + 1'b1;
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_wb_cyc))
|
|
&&(!$past(i_reset))
|
|
&&(!$past(i_new_pc))
|
|
&&(!$past(i_clear_cache))
|
|
&&(!$past(invalid_bus_cycle))
|
|
&&(($past(i_wb_ack))||($past(i_wb_err)))
|
|
&&((!$past(o_valid))||($past(i_stall_n)))
|
|
&&(!$past(cache_valid)))
|
|
assert(o_pc[AW+1:2] == $past(this_return_address));
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_wb_cyc))&&(!o_valid)&&(!$past(i_new_pc))
|
|
&&(o_wb_cyc))
|
|
assert(o_pc[AW+1:2] == this_return_address);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_wb_cyc))
|
|
&&(!$past(cache_valid))&&(cache_valid))
|
|
assert(next_pc_address == $past(this_return_address));
|
|
|
|
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_wb_cyc))&&(o_wb_cyc))
|
|
begin
|
|
if ((o_valid)&&(!cache_valid))
|
|
assert(this_return_address == next_pc_address);
|
|
else if (!o_valid)
|
|
assert(this_return_address == o_pc[AW+1:2]);
|
|
end else if ((f_past_valid)&&(!invalid_bus_cycle)
|
|
&&(!o_wb_cyc)&&(o_valid)&&(!o_illegal)
|
|
&&(!cache_valid))
|
|
assert(o_wb_addr == next_pc_address);
|
|
|
|
|
|
always @(*)
|
|
if (invalid_bus_cycle)
|
|
assert(!o_wb_cyc);
|
|
always @(*)
|
|
if (cache_valid)
|
|
assert(o_valid);
|
|
|
|
/////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Cover statements
|
|
//
|
|
//
|
|
/////////////////////////////////////////////////////
|
|
|
|
always @(posedge i_clk)
|
|
cover((f_past_valid)&&($past(f_nacks)==3)
|
|
&&($past(i_wb_ack))&&($past(o_wb_cyc)));
|
|
|
|
|
|
/////////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Temporary simplifications
|
|
//
|
|
//
|
|
/////////////////////////////////////////////////////
|
|
|
|
// always @(*)
|
|
// assume((!i_wb_err)&&(!f_const_illegal));
|
|
|
|
|
|
`endif // FORMAL
|
endmodule
|
endmodule
|
|
//
|
|
// Usage: (this) (prior) (old) (S6)
|
|
// Cells 374 387 585 459
|
|
// FDRE 135 108 203 171
|
|
// LUT1 2 3 2
|
|
// LUT2 9 3 4 5
|
|
// LUT3 98 76 104 71
|
|
// LUT4 2 0 2 2
|
|
// LUT5 3 35 35 3
|
|
// LUT6 6 5 10 43
|
|
// MUXCY 58 62 93 62
|
|
// MUXF7 1 0 2 3
|
|
// MUXF8 0 1 1
|
|
// RAM64X1D 0 32 32 32
|
|
// XORCY 60 64 96 64
|
|
//
|
|
|
No newline at end of file
|
No newline at end of file
|
