OpenCores
URL https://opencores.org/ocsvn/zipcpu/zipcpu/trunk

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [peripherals/] [zipcounter.v] - Diff between revs 201 and 209

Show entire file | Details | Blame | View Log

Rev 201 Rev 209
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

powered by: WebSVN 2.1.0

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