Subversion Repositories zipcpu

////////////////////////////////////////////////////////////////////////////////

//

// Filename:    zipcounter.v

//

// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core

//

// Purpose:

//              A very, _very_ simple counter.  It's purpose doesn't really

//      include rollover, but it will interrupt on rollover.  It can be set,

//      although my design concept is that it can be reset.  It cannot be

//      halted.  It will always produce interrupts--whether or not they are 

//      handled interrupts is another question--that's up to the interrupt

//      controller.

//

//      My intention is to use this counter for process accounting: I should

//      be able to use this to count clock ticks of processor time assigned to

//      each task by resetting the counter at the beginning of every task

//      interval, and reading the result at the end of the interval.  As long

//      as the interval is less than 2^32 clocks, there should be no problem.

//      Similarly, this can be used to measure CPU wishbone bus stalls, 

//      prefetch stalls, or other CPU stalls (i.e. stalling as part of a JMP

//      instruction, or a read from the condition codes following a write).

//

//

// 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  zipcounter(i_clk, i_reset, i_event,

                i_wb_cyc, i_wb_stb, i_wb_we, i_wb_data,

                        o_wb_ack, o_wb_stall, o_wb_data,

                o_int);

        parameter       BW = 32;

        //

        localparam      F_LGDEPTH = 2;

        //

        input   wire                    i_clk, i_reset, i_event;

        // Wishbone inputs

        input   wire                    i_wb_cyc, i_wb_stb, i_wb_we;

        input   wire    [(BW-1):0]       i_wb_data;

        // Wishbone outputs

        output  reg                     o_wb_ack;

        output  wire                    o_wb_stall;

        output  reg     [(BW-1):0]       o_wb_data;

        // Interrupt line

        output  reg                     o_int;

        initial o_int = 0;

        initial o_wb_data = 32'h00;

        always @(posedge i_clk)

                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 };

                else if (i_event)

                        { o_int, o_wb_data } <= o_wb_data+{{(BW-1){1'b0}},1'b1};

                else

                        o_int <= 1'b0;

        initial o_wb_ack = 1'b0;

        always @(posedge i_clk)

        if (i_reset)

                o_wb_ack <= 1'b0;

        else

                o_wb_ack <= i_wb_stb;

        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