| 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: A Zip timer, redesigned to be a bus watchdog
|
// Purpose: A Zip timer, redesigned to be a bus watchdog
|
//
|
//
|
// This is a **really** stripped down Zip Timer. All options for external
|
// This is basically a timer, but there are some unique features to it.
|
// control have been removed. This timer may be reset, and ... that's
|
//
|
// about it. The goal is that this stripped down timer be used as a bus
|
// 1. There is no way to "write" the timeout to this watchdog. It is
|
// watchdog element. Even at that, it's not really fully featured. The
|
// fixed with an input (that is assumed to be constant)
|
// rest of the important features can be found in the zipsystem module.
|
// 2. The counter returns to i_timer and the interrupt is cleared on any
|
//
|
// reset.
|
// As a historical note, the wishbone watchdog timer began as a normal
|
// 3. Between resets, the counter counts down to zero. Once (and if) it
|
// timer, with some fixed inputs. This makes sense, if you think about it:
|
// hits zero, it will remain at zero until reset.
|
// if the goal is to interrupt a stalled wishbone transaction by inserting
|
// 4. Any time the counter is at zero, and until the reset that resets
|
// a bus error, then you can't use the bus to set it up or configure it
|
// the counter, the output interrupt will be set.
|
// simply because the bus in question is ... well, unreliable. You're
|
|
// trying to make it reliable.
|
|
//
|
|
// The problem with using the ziptimer in a stripped down implementation
|
|
// was that the fixed inputs caused the synthesis tool to complain about
|
|
// the use of registers values would never change. This solves that
|
|
// problem by explicitly removing the cruft that would otherwise
|
|
// just create synthesis warnings and errors.
|
|
//
|
//
|
//
|
//
|
// 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 53... |
Line 45... |
//
|
//
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
module wbwatchdog(i_clk, i_rst, i_ce, i_timeout, o_int);
|
`default_nettype none
|
|
//
|
|
module wbwatchdog(i_clk, i_reset, i_timeout, o_int);
|
parameter BW = 32;
|
parameter BW = 32;
|
input i_clk, i_rst, i_ce;
|
input wire i_clk, i_reset;
|
// Inputs (these were at one time wishbone controlled ...)
|
// Inputs (these were at one time wishbone controlled ...)
|
input [(BW-1):0] i_timeout;
|
input wire [(BW-1):0] i_timeout;
|
// Interrupt line
|
// Interrupt line
|
output reg o_int;
|
output reg o_int;
|
|
|
reg [(BW-1):0] r_value;
|
reg [(BW-1):0] r_value;
|
initial r_value = 0;
|
initial r_value = {(BW){1'b1}};
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_rst)
|
if (i_reset)
|
r_value <= i_timeout[(BW-1):0];
|
r_value <= i_timeout[(BW-1):0];
|
else if ((i_ce)&&(~o_int))
|
else if (!o_int)
|
r_value <= r_value + {(BW){1'b1}}; // r_value - 1;
|
r_value <= r_value + {(BW){1'b1}}; // r_value - 1;
|
|
|
// Set the interrupt on our last tick.
|
// Set the interrupt on our last tick.
|
initial o_int = 1'b0;
|
initial o_int = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((i_rst)||(~i_ce))
|
if (i_reset)
|
o_int <= 1'b0;
|
o_int <= 1'b0;
|
else
|
else if (!o_int)
|
o_int <= (r_value == { {(BW-1){1'b0}}, 1'b1 });
|
o_int <= (r_value == { {(BW-1){1'b0}}, 1'b1 });
|
|
|
|
`ifdef FORMAL
|
|
reg f_past_valid;
|
|
|
|
initial f_past_valid = 1'b0;
|
|
always @(posedge f_past_valid)
|
|
f_past_valid <= 1'b1;
|
|
|
|
///////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assumptions about our inputs
|
|
//
|
|
//
|
|
///////////////////////////////////////////////
|
|
always @(*)
|
|
assume(i_timeout > 1);
|
|
always @(posedge i_clk)
|
|
if (f_past_valid)
|
|
assume(i_timeout == $past(i_timeout));
|
|
|
|
//
|
|
//
|
|
///////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assertions about our internal state and our outputs
|
|
//
|
|
//
|
|
///////////////////////////////////////////////
|
|
//
|
|
//
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_int))&&(!$past(i_reset)))
|
|
assert(o_int);
|
|
|
|
always @(*)
|
|
assert(o_int == (r_value == 0));
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(o_int)))
|
|
begin
|
|
assert(r_value == $past(r_value)-1'b1);
|
|
end
|
|
|
|
always @(posedge i_clk)
|
|
if ((!f_past_valid)||($past(i_reset)))
|
|
begin
|
|
if (!f_past_valid)
|
|
assert(r_value == {(BW){1'b1}});
|
|
else // if ($past(i_reset))
|
|
assert(r_value == $past(i_timeout));
|
|
assert(!o_int);
|
|
end
|
|
`endif
|
endmodule
|
endmodule
|
|
|
No newline at end of file
|
No newline at end of file
|
