| Line 43... |
Line 43... |
// 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 67... |
Line 67... |
//
|
//
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
module ziptimer(i_clk, i_rst, i_ce,
|
`default_nettype none
|
|
//
|
|
module ziptimer(i_clk, i_reset, i_ce,
|
i_wb_cyc, i_wb_stb, i_wb_we, i_wb_data,
|
i_wb_cyc, i_wb_stb, i_wb_we, i_wb_data,
|
o_wb_ack, o_wb_stall, o_wb_data,
|
o_wb_ack, o_wb_stall, o_wb_data,
|
o_int);
|
o_int);
|
parameter BW = 32, VW = (BW-1), RELOADABLE=1;
|
parameter BW = 32, VW = (BW-1), RELOADABLE=1;
|
input i_clk, i_rst, i_ce;
|
input wire i_clk, i_reset, i_ce;
|
// Wishbone inputs
|
// Wishbone inputs
|
input i_wb_cyc, i_wb_stb, i_wb_we;
|
input wire i_wb_cyc, i_wb_stb, i_wb_we;
|
input [(BW-1):0] i_wb_data;
|
input wire [(BW-1):0] i_wb_data;
|
// Wishbone outputs
|
// Wishbone outputs
|
output reg o_wb_ack;
|
output reg o_wb_ack;
|
output wire o_wb_stall;
|
output wire o_wb_stall;
|
output wire [(BW-1):0] o_wb_data;
|
output wire [(BW-1):0] o_wb_data;
|
// Interrupt line
|
// Interrupt line
|
output reg o_int;
|
output reg o_int;
|
|
|
reg r_running;
|
reg r_running;
|
|
|
wire wb_write;
|
wire wb_write;
|
assign wb_write = ((i_wb_cyc)&&(i_wb_stb)&&(i_wb_we));
|
assign wb_write = ((i_wb_stb)&&(i_wb_we));
|
|
|
wire auto_reload;
|
wire auto_reload;
|
wire [(VW-1):0] reload_value;
|
wire [(VW-1):0] interval_count;
|
|
|
initial r_running = 1'b0;
|
initial r_running = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_rst)
|
if (i_reset)
|
r_running <= 1'b0;
|
r_running <= 1'b0;
|
else if (wb_write)
|
else if (wb_write)
|
r_running <= (|i_wb_data[(VW-1):0]);
|
r_running <= (|i_wb_data[(VW-1):0]);
|
else if ((o_int)&&(~auto_reload))
|
else if ((r_zero)&&(!auto_reload))
|
r_running <= 1'b0;
|
r_running <= 1'b0;
|
|
|
generate
|
generate
|
if (RELOADABLE != 0)
|
if (RELOADABLE != 0)
|
begin
|
begin
|
reg r_auto_reload;
|
reg r_auto_reload;
|
reg [(VW-1):0] r_reload_value;
|
reg [(VW-1):0] r_interval_count;
|
|
|
initial r_auto_reload = 1'b0;
|
initial r_auto_reload = 1'b0;
|
|
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (wb_write)
|
if (i_reset)
|
r_auto_reload <= (i_wb_data[(BW-1)]);
|
r_auto_reload <= 1'b0;
|
|
else if (wb_write)
|
|
r_auto_reload <= (i_wb_data[(BW-1)])
|
|
&&(|i_wb_data[(VW-1):0]);
|
|
|
assign auto_reload = r_auto_reload;
|
assign auto_reload = r_auto_reload;
|
|
|
// If setting auto-reload mode, and the value to other
|
// If setting auto-reload mode, and the value to other
|
// than zero, set the auto-reload value
|
// than zero, set the auto-reload value
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((wb_write)&&(i_wb_data[(BW-1)])&&(|i_wb_data[(VW-1):0]))
|
if (wb_write)
|
r_reload_value <= i_wb_data[(VW-1):0];
|
r_interval_count <= i_wb_data[(VW-1):0];
|
assign reload_value = r_reload_value;
|
assign interval_count = r_interval_count;
|
end else begin
|
end else begin
|
assign auto_reload = 1'b0;
|
assign auto_reload = 1'b0;
|
assign reload_value = 0;
|
assign interval_count = 0;
|
end endgenerate
|
end endgenerate
|
|
|
|
|
reg [(VW-1):0] r_value;
|
reg [(VW-1):0] r_value;
|
initial r_value = 0;
|
initial r_value = 0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (wb_write)
|
if (i_reset)
|
|
r_value <= 0;
|
|
else if (wb_write)
|
r_value <= i_wb_data[(VW-1):0];
|
r_value <= i_wb_data[(VW-1):0];
|
else if ((r_running)&&(i_ce)&&(~o_int))
|
else if ((i_ce)&&(r_running))
|
r_value <= r_value + {(VW){1'b1}}; // r_value - 1;
|
begin
|
else if ((r_running)&&(auto_reload)&&(o_int))
|
if (!r_zero)
|
r_value <= reload_value;
|
r_value <= r_value - 1'b1;
|
|
else if (auto_reload)
|
|
r_value <= interval_count;
|
|
end
|
|
|
|
reg r_zero = 1'b1;
|
|
always @(posedge i_clk)
|
|
if (i_reset)
|
|
r_zero <= 1'b1;
|
|
else if (wb_write)
|
|
r_zero <= (i_wb_data[(VW-1):0] == 0);
|
|
else if ((r_running)&&(i_ce))
|
|
begin
|
|
if (r_value == { {(VW-1){1'b0}}, 1'b1 })
|
|
r_zero <= 1'b1;
|
|
else if ((r_zero)&&(auto_reload))
|
|
r_zero <= 1'b0;
|
|
end
|
|
|
// Set the interrupt on our last tick, as we transition from one to
|
// Set the interrupt on our last tick, as we transition from one to
|
// zero.
|
// zero.
|
initial o_int = 1'b0;
|
initial o_int = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if (i_rst)
|
if ((i_reset)||(wb_write)||(!i_ce))
|
o_int <= 1'b0;
|
|
else if (i_ce)
|
|
o_int <= (r_running)&&(r_value == { {(VW-1){1'b0}}, 1'b1 });
|
|
else
|
|
o_int <= 1'b0;
|
o_int <= 1'b0;
|
|
else // if (i_ce)
|
|
o_int <= (r_value == { {(VW-1){1'b0}}, 1'b1 });
|
|
|
initial o_wb_ack = 1'b0;
|
initial o_wb_ack = 1'b0;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
o_wb_ack <= (i_wb_cyc)&&(i_wb_stb);
|
o_wb_ack <= (!i_reset)&&(i_wb_stb);
|
assign o_wb_stall = 1'b0;
|
assign o_wb_stall = 1'b0;
|
|
|
generate
|
generate
|
if (VW < BW-1)
|
if (VW < BW-1)
|
assign o_wb_data = { auto_reload, {(BW-1-VW){1'b0}}, r_value };
|
assign o_wb_data = { auto_reload, {(BW-1-VW){1'b0}}, r_value };
|
else
|
else
|
assign o_wb_data = { auto_reload, r_value };
|
assign o_wb_data = { auto_reload, r_value };
|
endgenerate
|
endgenerate
|
|
|
|
// Make verilator happy
|
|
// verilator lint_off UNUSED
|
|
wire [32:0] unused;
|
|
assign unused = { i_wb_cyc, i_wb_data };
|
|
// verilator lint_on UNUSED
|
|
|
|
`ifdef FORMAL
|
|
reg f_past_valid;
|
|
initial f_past_valid = 1'b0;
|
|
always @(posedge i_clk)
|
|
f_past_valid <= 1'b1;
|
|
initial assume(i_reset);
|
|
always @(*)
|
|
if (!f_past_valid)
|
|
assume(i_reset);
|
|
|
|
always @(posedge i_clk)
|
|
if ((!f_past_valid)||($past(i_reset)))
|
|
begin
|
|
assert(r_value == 0);
|
|
assert(r_running == 0);
|
|
assert(auto_reload == 0);
|
|
assert(r_zero == 1'b1);
|
|
end
|
|
|
|
|
|
always @(*)
|
|
assert(r_zero == (r_value == 0));
|
|
|
|
always @(*)
|
|
if (r_value != 0)
|
|
assert(r_running);
|
|
|
|
always @(*)
|
|
if (auto_reload)
|
|
assert(r_running);
|
|
|
|
always @(*)
|
|
if (!RELOADABLE)
|
|
assert(auto_reload == 0);
|
|
|
|
always @(*)
|
|
if (auto_reload)
|
|
assert(interval_count != 0);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(r_value)==0)
|
|
&&(!$past(wb_write))&&(!$past(auto_reload)))
|
|
assert(r_value == 0);
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(wb_write))
|
|
&&($past(r_value)==0)&&($past(auto_reload)))
|
|
begin
|
|
if ($past(i_ce))
|
|
assert(r_value == interval_count);
|
|
else
|
|
assert(r_value == $past(r_value));
|
|
end
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))
|
|
&&(!$past(wb_write))&&($past(r_value)!=0))
|
|
begin
|
|
if ($past(i_ce))
|
|
assert(r_value == $past(r_value)-1'b1);
|
|
else
|
|
assert(r_value == $past(r_value));
|
|
end
|
|
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))&&($past(wb_write)))
|
|
assert(r_value == $past(i_wb_data[(VW-1):0]));
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))&&($past(wb_write))
|
|
&&(RELOADABLE)&&(|$past(i_wb_data[(VW-1):0])))
|
|
assert(auto_reload == $past(i_wb_data[(BW-1)]));
|
|
|
|
always @(posedge i_clk)
|
|
if (!(f_past_valid)||($past(i_reset)))
|
|
assert(!o_int);
|
|
else if (($past(wb_write))||(!$past(i_ce)))
|
|
assert(!o_int);
|
|
else
|
|
assert(o_int == ((r_running)&&(r_value == 0)));
|
|
|
|
always @(posedge i_clk)
|
|
if ((!f_past_valid)||($past(i_reset)))
|
|
assert(!o_wb_ack);
|
|
else if ($past(i_wb_stb))
|
|
assert(o_wb_ack);
|
|
|
|
always @(*)
|
|
assert(!o_wb_stall);
|
|
always @(*)
|
|
assert(o_wb_data[BW-1] == auto_reload);
|
|
always @(*)
|
|
assert(o_wb_data[VW-1:0] == r_value);
|
|
`endif
|
endmodule
|
endmodule
|
|
|
No newline at end of file
|
No newline at end of file
|
