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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [rtl/] [peripherals/] [wbwatchdog.v] - Blame information for rev 209

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
2 69 dgisselq
//
3
// Filename:    wbwatchdog.v
4
//
5
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
//
7
// Purpose:     A Zip timer, redesigned to be a bus watchdog
8
//
9 209 dgisselq
//      This is basically a timer, but there are some unique features to it.
10 69 dgisselq
//
11 209 dgisselq
//      1. There is no way to "write" the timeout to this watchdog.  It is
12
//              fixed with an input (that is assumed to be constant)
13
//      2. The counter returns to i_timer and the interrupt is cleared on any
14
//              reset.
15
//      3. Between resets, the counter counts down to zero.  Once (and if) it
16
//              hits zero, it will remain at zero until reset.
17
//      4. Any time the counter is at zero, and until the reset that resets
18
//              the counter, the output interrupt will be set.
19 69 dgisselq
//
20
//
21
// Creator:     Dan Gisselquist, Ph.D.
22
//              Gisselquist Technology, LLC
23
//
24 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
25 69 dgisselq
//
26 209 dgisselq
// Copyright (C) 2015,2017-2019, Gisselquist Technology, LLC
27 69 dgisselq
//
28
// This program is free software (firmware): you can redistribute it and/or
29
// modify it under the terms of  the GNU General Public License as published
30
// by the Free Software Foundation, either version 3 of the License, or (at
31
// your option) any later version.
32
//
33
// This program is distributed in the hope that it will be useful, but WITHOUT
34
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
35
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
36
// for more details.
37
//
38 201 dgisselq
// You should have received a copy of the GNU General Public License along
39
// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
40
// target there if the PDF file isn't present.)  If not, see
41
// <http://www.gnu.org/licenses/> for a copy.
42
//
43 69 dgisselq
// License:     GPL, v3, as defined and found on www.gnu.org,
44
//              http://www.gnu.org/licenses/gpl.html
45
//
46
//
47 201 dgisselq
////////////////////////////////////////////////////////////////////////////////
48 69 dgisselq
//
49 201 dgisselq
//
50 209 dgisselq
`default_nettype        none
51
//
52
module  wbwatchdog(i_clk, i_reset, i_timeout, o_int);
53 69 dgisselq
        parameter       BW = 32;
54 209 dgisselq
        input   wire            i_clk, i_reset;
55 69 dgisselq
        // Inputs (these were at one time wishbone controlled ...)
56 209 dgisselq
        input   wire [(BW-1):0]  i_timeout;
57 69 dgisselq
        // Interrupt line
58
        output  reg             o_int;
59
 
60
        reg     [(BW-1):0]       r_value;
61 209 dgisselq
        initial r_value = {(BW){1'b1}};
62 69 dgisselq
        always @(posedge i_clk)
63 209 dgisselq
                if (i_reset)
64 69 dgisselq
                        r_value <= i_timeout[(BW-1):0];
65 209 dgisselq
                else if (!o_int)
66 69 dgisselq
                        r_value <= r_value + {(BW){1'b1}}; // r_value - 1;
67
 
68
        // Set the interrupt on our last tick.
69
        initial o_int   = 1'b0;
70
        always @(posedge i_clk)
71 209 dgisselq
                if (i_reset)
72 69 dgisselq
                        o_int <= 1'b0;
73 209 dgisselq
                else if (!o_int)
74 69 dgisselq
                        o_int <= (r_value == { {(BW-1){1'b0}}, 1'b1 });
75
 
76 209 dgisselq
`ifdef  FORMAL
77
        reg     f_past_valid;
78
 
79
        initial f_past_valid = 1'b0;
80
        always @(posedge f_past_valid)
81
                f_past_valid <= 1'b1;
82
 
83
        ///////////////////////////////////////////////
84
        //
85
        //
86
        // Assumptions about our inputs
87
        //
88
        //
89
        ///////////////////////////////////////////////
90
        always @(*)
91
                assume(i_timeout > 1);
92
        always @(posedge i_clk)
93
        if (f_past_valid)
94
                assume(i_timeout == $past(i_timeout));
95
 
96
        //
97
        //
98
        ///////////////////////////////////////////////
99
        //
100
        //
101
        // Assertions about our internal state and our outputs
102
        //
103
        //
104
        ///////////////////////////////////////////////
105
        //
106
        //
107
        always @(posedge i_clk)
108
        if ((f_past_valid)&&($past(o_int))&&(!$past(i_reset)))
109
                assert(o_int);
110
 
111
        always @(*)
112
                assert(o_int == (r_value == 0));
113
 
114
        always @(posedge i_clk)
115
        if ((f_past_valid)&&(!$past(i_reset))&&(!$past(o_int)))
116
        begin
117
                assert(r_value == $past(r_value)-1'b1);
118
        end
119
 
120
        always @(posedge i_clk)
121
        if ((!f_past_valid)||($past(i_reset)))
122
        begin
123
                if (!f_past_valid)
124
                        assert(r_value == {(BW){1'b1}});
125
                else // if ($past(i_reset))
126
                        assert(r_value == $past(i_timeout));
127
                assert(!o_int);
128
        end
129
`endif
130 69 dgisselq
endmodule

powered by: WebSVN 2.1.0

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