| Line 25... |
Line 25... |
// 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-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 49... |
Line 49... |
//
|
//
|
//
|
//
|
////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////
|
//
|
//
|
//
|
//
|
module zipcounter(i_clk, i_ce,
|
`default_nettype none
|
|
//
|
|
module zipcounter(i_clk, i_reset, i_event,
|
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;
|
parameter BW = 32;
|
input i_clk, i_ce;
|
//
|
|
localparam F_LGDEPTH = 2;
|
|
//
|
|
input wire i_clk, i_reset, i_event;
|
// 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 reg [(BW-1):0] o_wb_data;
|
output reg [(BW-1):0] o_wb_data;
|
// Interrupt line
|
// Interrupt line
|
output reg o_int;
|
output reg o_int;
|
|
|
initial o_int = 0;
|
initial o_int = 0;
|
initial o_wb_data = 32'h00;
|
initial o_wb_data = 32'h00;
|
always @(posedge i_clk)
|
always @(posedge i_clk)
|
if ((i_wb_stb)&&(i_wb_we))
|
if (i_reset)
|
|
{ o_int, o_wb_data } <= 0;
|
|
else if ((i_wb_stb)&&(i_wb_we))
|
{ o_int, o_wb_data } <= { 1'b0, i_wb_data };
|
{ o_int, o_wb_data } <= { 1'b0, i_wb_data };
|
else if (i_ce)
|
else if (i_event)
|
{ o_int, o_wb_data } <= o_wb_data+{{(BW-1){1'b0}},1'b1};
|
{ o_int, o_wb_data } <= o_wb_data+{{(BW-1){1'b0}},1'b1};
|
else
|
else
|
o_int <= 1'b0;
|
o_int <= 1'b0;
|
|
|
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_stb);
|
if (i_reset)
|
|
o_wb_ack <= 1'b0;
|
|
else
|
|
o_wb_ack <= i_wb_stb;
|
assign o_wb_stall = 1'b0;
|
assign o_wb_stall = 1'b0;
|
|
|
|
|
|
// Make verilator happy
|
|
// verilator lint_off UNUSED
|
|
wire unused;
|
|
assign unused = i_wb_cyc;
|
|
// 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;
|
|
|
|
always @(*)
|
|
if (!f_past_valid)
|
|
assume(i_reset);
|
|
|
|
////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assumptions about our inputs
|
|
//
|
|
//
|
|
////////////////////////////////////////////////
|
|
//
|
|
|
|
////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Bus interface properties
|
|
//
|
|
//
|
|
////////////////////////////////////////////////
|
|
//
|
|
|
|
// We never stall the bus
|
|
always @(*)
|
|
assert(!o_wb_stall);
|
|
|
|
// We always ack every transaction on the following clock
|
|
always @(posedge i_clk)
|
|
assert(o_wb_ack == ((f_past_valid)&&(!$past(i_reset))
|
|
&&($past(i_wb_stb))));
|
|
|
|
wire [(F_LGDEPTH-1):0] f_nreqs, f_nacks, f_outstanding;
|
|
|
|
fwb_slave #( .AW(1), .F_MAX_STALL(0),
|
|
.F_MAX_ACK_DELAY(1), .F_LGDEPTH(F_LGDEPTH)
|
|
) fwbi(i_clk, i_reset,
|
|
i_wb_cyc, i_wb_stb, i_wb_we, 1'b0, i_wb_data, 4'hf,
|
|
o_wb_ack, o_wb_stall, o_wb_data, 1'b0,
|
|
f_nreqs, f_nacks, f_outstanding);
|
|
|
|
always @(*)
|
|
if ((o_wb_ack)&&(i_wb_cyc))
|
|
assert(f_outstanding==1);
|
|
else
|
|
assert(f_outstanding == 0);
|
|
|
|
////////////////////////////////////////////////
|
|
//
|
|
//
|
|
// Assumptions about our outputs
|
|
//
|
|
//
|
|
////////////////////////////////////////////////
|
|
//
|
|
|
|
// Drop the interrupt line and reset the counter on any reset
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(i_reset)))
|
|
assert((!o_int)&&(o_wb_data == 0));
|
|
|
|
// Clear the interrupt and set the counter on any write (other than
|
|
// during a reset)
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))
|
|
&&($past(i_wb_stb))&&($past(i_wb_we)))
|
|
assert((!o_int)&&(o_wb_data == $past(i_wb_data)));
|
|
|
|
// Normal logic of the routine itself
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&(!$past(i_reset))&&(!$past(i_wb_stb)))
|
|
begin
|
|
if (!$past(i_event))
|
|
begin
|
|
// If the CE line wasn't set on the last clock, then the
|
|
// counter must not change, and the interrupt line must
|
|
// be low.
|
|
assert(o_wb_data == $past(o_wb_data));
|
|
assert(!o_int);
|
|
end else // if ($past(i_event))
|
|
begin
|
|
// Otherwise, if the CE line was high on the last clock,
|
|
// then our counter should have incremented.
|
|
assert(o_wb_data == $past(o_wb_data) + 1'b1);
|
|
|
|
// Likewise, if the counter rolled over, then the
|
|
// output interrupt, o_int, should be true.
|
|
if ($past(o_wb_data)=={(BW){1'b1}})
|
|
assert(o_int);
|
|
else
|
|
// In all other circumstances it should be clear
|
|
assert(!o_int);
|
|
end
|
|
end
|
|
|
|
//
|
|
// The output interrupt should never be true two clocks in a row
|
|
always @(posedge i_clk)
|
|
if ((f_past_valid)&&($past(o_int)))
|
|
assert(!o_int);
|
|
|
|
`endif
|
endmodule
|
endmodule
|
|
|
No newline at end of file
|
No newline at end of file
|
