OpenCores
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
 

Compare with Previous | Blame | View Log

powered by: WebSVN 2.1.0

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