URL
https://opencores.org/ocsvn/zipcpu/zipcpu/trunk
Subversion Repositories zipcpu
[/] [zipcpu/] [trunk/] [bench/] [formal/] [abs_prefetch.v] - Rev 209
Compare with Previous | Blame | View Log
//////////////////////////////////////////////////////////////////////////////// // // Filename: abs_prefetch.v // // Project: Zip CPU -- a small, lightweight, RISC CPU soft core // // Purpose: Rather than feed our CPU with actual valid instructions returned // from memory, this is an abstract prefetch. It's not even a // perfect or complete abstract prefetch at that--it doesn't actually // access memory. However, it will maintain the abstract interface with // the CPU.s // // In other words, this abs_prefetch may produce the exact same results a // true prefetch would have produced--whether it be prefetch.v, dblfetch.v, // or even pfcache.v. On the other hand, it might not. If the CPU can // pass either way, then it can most certainly pass with a true prefetch. // // Creator: Dan Gisselquist, Ph.D. // Gisselquist Technology, LLC // //////////////////////////////////////////////////////////////////////////////// // // Copyright (C) 2015-2019, 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 abs_prefetch(i_clk, i_reset, i_new_pc, i_clear_cache, // i_early_branch, i_from_addr, 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, i_wb_ack, i_wb_stall, i_wb_err, i_wb_data, o_illegal); parameter ADDRESS_WIDTH = 30; localparam BUSW = 32; // Number of data lines on the bus localparam AW=ADDRESS_WIDTH; // Shorthand for ADDRESS_WIDTH // input wire i_clk, i_reset; // // The interface with the rest of the CPU input wire i_new_pc; input wire i_clear_cache; input wire i_stall_n; input wire [(AW+1):0] i_pc; output wire [(BUSW-1):0] o_insn; output wire [(AW+1):0] o_pc; output wire o_valid; // // The wishbone bus interface output wire o_wb_cyc, o_wb_stb; output wire o_wb_we; output wire [(AW-1):0] o_wb_addr; output wire [(BUSW-1):0] o_wb_data; // input wire i_wb_ack, i_wb_stall, i_wb_err; input wire [(BUSW-1):0] i_wb_data; // // o_illegal will be true if this instruction was the result of // a bus error (This is also part of the CPU interface) output reg o_illegal; // // Fixed bus outputs: we read from the bus only, never write. // Thus the output data is ... irrelevant and don't care. We set it // to zero just to set it to something. assign o_wb_cyc = 0; assign o_wb_stb = 0; assign o_wb_we = 0; assign o_wb_addr = 0; assign o_wb_data = 0; reg [(AW-1):0] r_pc; reg waiting_on_pc; reg [5:0] wait_for_valid; always @(posedge i_clk) if (i_new_pc) r_pc = i_pc[AW+1:2]; else if ((o_valid)&&(i_stall_n)) r_pc <= r_pc + 1'b1; (* anyconst *) reg [(AW-1):0] any_pc; assign o_pc = { (o_valid) ? r_pc : any_pc, 2'b00 }; (* anyseq *) reg any_illegal; always @(posedge i_clk) if ((i_reset)||(i_clear_cache)||(i_new_pc)||(waiting_on_pc)) o_illegal <= 1'b0; else if ((!o_illegal)&&(wait_for_valid == 1'b1)) o_illegal <= any_illegal; (* anyseq *) reg [5:0] wait_time; always @(*) assume(wait_time > 0); initial waiting_on_pc <= 1'b1; always @(posedge i_clk) if ((i_reset)||(i_clear_cache)) waiting_on_pc <= 1'b1; else if (i_new_pc) waiting_on_pc <= 1'b0; always @(posedge i_clk) if ((i_reset)||(i_clear_cache)) wait_for_valid <= 6'h3f; else if ((i_new_pc)||(waiting_on_pc)) wait_for_valid <= wait_time; else if (wait_for_valid > 0) wait_for_valid <= wait_for_valid - 1'b1; (* anyseq *) reg [(BUSW-1):0] any_insn; assign o_valid = (!waiting_on_pc)&&(wait_for_valid == 0); assign o_insn = any_insn; `ifdef FORMAL `define ASSUME assume `define ASSERT assert // 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; always @(*) if (!f_past_valid) `ASSERT(i_reset); ///////////////////////////////////////////////// // // // Assumptions about our inputs // // ///////////////////////////////////////////////// // // Assume we start from a reset condition initial `ASSERT(i_reset); ///////////////////////////////////////////////// // // // Assertions about our outputs // // ///////////////////////////////////////////////// ///////////////////////////////////////////////////// // // // Assertions about our return responses to the CPU // // ///////////////////////////////////////////////////// // Consider it invalid to present the CPU with the same instruction // twice in a row. always @(posedge i_clk) if ((f_past_valid)&&($past(o_valid))&&($past(i_stall_n))&&(o_valid)) assume(o_pc != $past(o_pc)); always @(*) begin `ASSERT(i_pc[1:0] == 2'b00); assume(o_pc[1:0] == 2'b00); end // // Assume we start from a reset condition initial `ASSUME(i_reset); // 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)&&($past(i_reset))) `ASSERT(i_new_pc); // // // 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 @(*) `ASSERT(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)&&($past(i_reset))) `ASSERT(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))) `ASSERT(i_new_pc); always @(*) `ASSUME(i_pc[1:0] == 2'b00); ///////////////////////////////////////////////// // // // Assertions about our outputs // // ///////////////////////////////////////////////// // // 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 assume($stable(o_pc)); assume($stable(o_insn)); assume($stable(o_valid)); assume($stable(o_illegal)); end // // As with i_pc[1:0], the bottom two bits of the address are unused. // Let's assert here that they remain zero. always @(*) assume(o_pc[1:0] == 2'b00); always @(posedge i_clk) if ((f_past_valid)&&(!$past(o_illegal))&&(o_illegal)) assume(o_valid); always @(posedge i_clk) if ((f_past_valid)&&($past(i_new_pc))) assume(!o_valid); `endif // FORMAL endmodule