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

Subversion Repositories zipcpu

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

Show entire file | Details | Blame | View Log

Rev 201 Rev 209
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-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  zipjiffies(i_clk, i_ce,
`default_nettype        none
 
//
 
module  zipjiffies(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;
        parameter       BW = 32;
        input                           i_clk, 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
Line 92... Line 94...
        // support debugging, so that if we get everything running inside a
        // support debugging, so that if we get everything running inside a
        // debugger, the timer's all slow down so that everything can be stepped
        // debugger, the timer's all slow down so that everything can be stepped
        // together, one clock at a time.
        // together, one clock at a time.
        //
        //
        reg     [(BW-1):0]       r_counter;
        reg     [(BW-1):0]       r_counter;
 
        initial r_counter = 0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                if (i_ce)
                if (i_reset)
 
                        r_counter <= 0;
 
                else if (i_ce)
                        r_counter <= r_counter+1;
                        r_counter <= r_counter+1;
 
 
        //
        //
        // Writes to the counter set an interrupt--but only if they are in the
        // Writes to the counter set an interrupt--but only if they are in the
        // future as determined by the signed result of an unsigned subtract.
        // future as determined by the signed result of an unsigned subtract.
Line 108... Line 113...
        assign  till_when = int_when-r_counter;
        assign  till_when = int_when-r_counter;
        assign  till_wb   = new_when-r_counter;
        assign  till_wb   = new_when-r_counter;
 
 
        initial new_set = 1'b0;
        initial new_set = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if (i_reset)
        begin
        begin
                // Delay things by a clock to simplify our logic
                new_set  <= 1'b0;
                new_set <= ((i_wb_cyc)&&(i_wb_stb)&&(i_wb_we));
                new_when <= 0;
 
        end else begin
 
                // Delay WB commands (writes) by a clock to simplify our logic
 
                new_set <= ((i_wb_stb)&&(i_wb_we));
                // new_when is a don't care when new_set = 0, so don't worry
                // new_when is a don't care when new_set = 0, so don't worry
                // about setting it at all times.
                // about setting it at all times.
                new_when<= i_wb_data;
                new_when<= i_wb_data;
        end
        end
 
 
        initial o_int   = 1'b0;
        initial o_int   = 1'b0;
        initial int_set = 1'b0;
        initial int_set = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
 
        if (i_reset)
        begin
        begin
 
                o_int <= 0;
 
                int_set <= 0;
 
        end else begin
                o_int <= 1'b0;
                o_int <= 1'b0;
                if ((i_ce)&&(int_set)&&(r_counter == int_when))
                if ((i_ce)&&(int_set)&&(r_counter == int_when))
                        // Interrupts are self-clearing
                        // Interrupts are self-clearing
                        o_int <= 1'b1;  // Set the interrupt flag for one clock
                        o_int <= 1'b1;  // Set the interrupt flag for one clock
                else if ((new_set)&&(till_wb <= 0))
                else if ((new_set)&&(till_wb <= 0))
Line 131... Line 144...
 
 
                if ((new_set)&&(till_wb > 0))
                if ((new_set)&&(till_wb > 0))
                        int_set <= 1'b1;
                        int_set <= 1'b1;
                else if ((i_ce)&&(r_counter == int_when))
                else if ((i_ce)&&(r_counter == int_when))
                        int_set <= 1'b0;
                        int_set <= 1'b0;
 
        end
 
 
                if ((new_set)&&(till_wb > 0)&&((till_wb<till_when)||(~int_set)))
        always @(posedge i_clk)
 
        if ((new_set)&&(till_wb > 0)&&((till_wb<till_when)||(!int_set)))
                        int_when <= new_when;
                        int_when <= new_when;
        end
 
 
 
        //
        //
        // Acknowledge any wishbone accesses -- everything we did took only
        // Acknowledge any wishbone accesses -- everything we did took only
        // one clock anyway.
        // one clock anyway.
        //
        //
 
        initial o_wb_ack = 1'b0;
        always @(posedge i_clk)
        always @(posedge i_clk)
                o_wb_ack <= (i_wb_cyc)&&(i_wb_stb);
        if (i_reset)
 
                o_wb_ack <= 1'b0;
 
        else
 
                o_wb_ack <= i_wb_stb;
 
 
        assign  o_wb_data = r_counter;
        assign  o_wb_data = r_counter;
        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;
 
 
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
        // Assumptions about our inputs
 
        //
 
        //
 
        ////////////////////////////////////////////////
 
        //
 
        // Some basic WB assumtions
 
 
 
        // We will not start out in a wishbone cycle
 
        initial assume(!i_wb_cyc);
 
 
 
        // Following any reset the cycle line will be low
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_reset)))
 
                assume(!i_wb_cyc);
 
 
 
        // Anytime the stb is high, the cycle line must also be high
 
        always @(posedge i_clk)
 
                assume((!i_wb_stb)||(i_wb_cyc));
 
 
 
 
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
        // Assumptions about our bus outputs
 
        //
 
        //
 
        ////////////////////////////////////////////////
 
        //
 
 
 
        // We never stall the bus
 
        always @(*)
 
                assert(!o_wb_stall);
 
        // We always ack every transaction on the following clock
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb)))
 
                assert(o_wb_ack);
 
        else
 
                assert(!o_wb_ack);
 
 
 
 
 
        ////////////////////////////////////////////////
 
        //
 
        //
 
        // Assumptions about our internal state and our outputs
 
        //
 
        //
 
        ////////////////////////////////////////////////
 
        //
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_reset)))
 
        begin
 
                assert(!o_wb_ack);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
 
                        &&($past(i_wb_we)))
 
                assert(new_when == $past(i_wb_data));
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))
 
                        &&($past(i_wb_we)))
 
                assert(new_set);
 
        else
 
                assert(!new_set);
 
 
 
        //
 
        //
 
        //
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_reset)))
 
                assert(!o_int);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&($past(i_reset)))
 
        begin
 
                assert(!int_set);
 
                assert(!new_set);
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(new_set))
 
                        &&(!$past(till_wb[BW-1]))
 
                        &&($past(till_wb) > 0))
 
                assert(int_set);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&($past(i_ce))
 
                &&($past(r_counter)==$past(int_when)))
 
        begin
 
                assert((o_int)||(!$past(int_set)));
 
                assert((!int_set)||($past(new_set)));
 
        end
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&(!$past(i_reset))&&(!$past(new_set))&&(!$past(int_set)))
 
                assert(!int_set);
 
 
 
        always @(posedge i_clk)
 
        if ((!f_past_valid)||($past(i_reset)))
 
                assert(!o_int);
 
        else if (($past(new_set))&&($past(till_wb) < 0))
 
                assert(o_int);
 
 
 
        always @(posedge i_clk)
 
        if ((f_past_valid)&&
 
                        ((!$past(new_set))
 
                        ||($past(till_wb[BW-1]))
 
                        ||($past(till_wb == 0))))
 
                assert(int_when == $past(int_when));
 
        //
 
`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.