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

Subversion Repositories zipcpu

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

Details | Compare with Previous | View Log


////////////////////////////////////////////////////////////////////////////////
//
// Filename:    zipjiffies.v
//
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
//
// Purpose:     This peripheral is motivated by the Linux use of 'jiffies'.
//      A process, in Linux, can request to be put to sleep until a certain
//      number of 'jiffies' have elapsed.  Using this interface, the CPU can
//      read the number of 'jiffies' from this peripheral (it only has the
//      one location in address space), add the sleep length to it, and
//      write the result back to the peripheral.  The zipjiffies peripheral
//      will record the value written to it only if it is nearer the current
//      counter value than the last current waiting interrupt time.  If no
//      other interrupts are waiting, and this time is in the future, it will
//      be enabled.  (There is currrently no way to disable a jiffie interrupt
//      once set.)  The processor may then place this sleep request into a
//      list among other sleep requests.  Once the timer expires, it would
//      write the next jiffy request to the peripheral and wake up the process
//      whose timer had expired.
//
//      Quite elementary, really.
//
// Interface:
//      This peripheral contains one register: a counter.  Reads from the
//      register return the current value of the counter.  Writes within
//      the (N-1) bit space following the current time set an interrupt.
//      Writes of values that occurred in the last 2^(N-1) ticks will be
//      ignored.  The timer then interrupts when it's value equals that time. 
//      Multiple writes cause the jiffies timer to select the nearest possible
//      interrupt.  Upon an interrupt, the next interrupt time/value is cleared
//      and will need to be reset if the CPU wants to get notified again.  With
//      only the single interface, there is no way of knowing when the next
//      interrupt is scheduled for, neither is there any way to slow down the
//      interrupt timer in case you don't want it overflowing as often and you
//      wish to wait more jiffies than it supports.  Thus, currently, if you
//      have a timer you wish to wait upon that is more than 2^31 into the
//      future, you would need to set timers along the way, wake up on those
//      timers, and set further timer's until you finally get to your
//      destination.
//
//
// 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  zipjiffies(i_clk, i_reset, i_ce,
                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;
        input   wire                    i_clk, i_reset, i_ce;
        // 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  wire    [(BW-1):0]       o_wb_data;
        // Interrupt line
        output  reg                     o_int;
 
        //
        // Our counter logic: The counter is always counting up--it cannot
        // be stopped or altered.  It's really quite simple.  Okay, not quite.
        // We still support the clock enable line.  We do this in order to
        // support debugging, so that if we get everything running inside a
        // debugger, the timer's all slow down so that everything can be stepped
        // together, one clock at a time.
        //
        reg     [(BW-1):0]       r_counter;
        initial r_counter = 0;
        always @(posedge i_clk)
                if (i_reset)
                        r_counter <= 0;
                else if (i_ce)
                        r_counter <= r_counter+1;
 
        //
        // 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.
        //
        reg                             int_set,  new_set;
        reg             [(BW-1):0]       int_when, new_when;
        wire    signed  [(BW-1):0]       till_when, till_wb;
        assign  till_when = int_when-r_counter;
        assign  till_wb   = new_when-r_counter;
 
        initial new_set = 1'b0;
        always @(posedge i_clk)
        if (i_reset)
        begin
                new_set  <= 1'b0;
                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
                // about setting it at all times.
                new_when<= i_wb_data;
        end
 
        initial o_int   = 1'b0;
        initial int_set = 1'b0;
        always @(posedge i_clk)
        if (i_reset)
        begin
                o_int <= 0;
                int_set <= 0;
        end else begin
                o_int <= 1'b0;
                if ((i_ce)&&(int_set)&&(r_counter == int_when))
                        // Interrupts are self-clearing
                        o_int <= 1'b1;  // Set the interrupt flag for one clock
                else if ((new_set)&&(till_wb <= 0))
                        o_int <= 1'b1;
 
                if ((new_set)&&(till_wb > 0))
                        int_set <= 1'b1;
                else if ((i_ce)&&(r_counter == int_when))
                        int_set <= 1'b0;
        end
 
        always @(posedge i_clk)
        if ((new_set)&&(till_wb > 0)&&((till_wb<till_when)||(!int_set)))
                int_when <= new_when;
 
        //
        // Acknowledge any wishbone accesses -- everything we did took only
        // one clock anyway.
        //
        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_data = r_counter;
        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

Line No.	Rev	Author	Line
1	2	dgisselq	`////////////////////////////////////////////////////////////////////////////////`
2			`//`
3			`// Filename: zipjiffies.v`
4			`//`
5			`// Project: Zip CPU -- a small, lightweight, RISC CPU soft core`
6			`//`
7			`// Purpose: This peripheral is motivated by the Linux use of 'jiffies'.`
8			`// A process, in Linux, can request to be put to sleep until a certain`
9			`// number of 'jiffies' have elapsed. Using this interface, the CPU can`
10			`// read the number of 'jiffies' from this peripheral (it only has the`
11			`// one location in address space), add the sleep length to it, and`
12			`// write the result back to the peripheral. The zipjiffies peripheral`
13			`// will record the value written to it only if it is nearer the current`
14			`// counter value than the last current waiting interrupt time. If no`
15			`// other interrupts are waiting, and this time is in the future, it will`
16			`// be enabled. (There is currrently no way to disable a jiffie interrupt`
17			`// once set.) The processor may then place this sleep request into a`
18			`// list among other sleep requests. Once the timer expires, it would`
19			`// write the next jiffy request to the peripheral and wake up the process`
20			`// whose timer had expired.`
21			`//`
22			`// Quite elementary, really.`
23			`//`
24			`// Interface:`
25			`// This peripheral contains one register: a counter. Reads from the`
26			`// register return the current value of the counter. Writes within`
27			`// the (N-1) bit space following the current time set an interrupt.`
28			`// Writes of values that occurred in the last 2^(N-1) ticks will be`
29			`// ignored. The timer then interrupts when it's value equals that time.`
30			`// Multiple writes cause the jiffies timer to select the nearest possible`
31			`// interrupt. Upon an interrupt, the next interrupt time/value is cleared`
32			`// and will need to be reset if the CPU wants to get notified again. With`
33			`// only the single interface, there is no way of knowing when the next`
34			`// interrupt is scheduled for, neither is there any way to slow down the`
35			`// interrupt timer in case you don't want it overflowing as often and you`
36			`// wish to wait more jiffies than it supports. Thus, currently, if you`
37			`// have a timer you wish to wait upon that is more than 2^31 into the`
38			`// future, you would need to set timers along the way, wake up on those`
39			`// timers, and set further timer's until you finally get to your`
40			`// destination.`
41			`//`
42			`//`
43			`// Creator: Dan Gisselquist, Ph.D.`
44	69	dgisselq	`// Gisselquist Technology, LLC`
45	2	dgisselq	`//`
46			`////////////////////////////////////////////////////////////////////////////////`
47			`//`
48	209	dgisselq	`// Copyright (C) 2015-2019, Gisselquist Technology, LLC`
49	2	dgisselq	`//`
50			`// This program is free software (firmware): you can redistribute it and/or`
51			`// modify it under the terms of the GNU General Public License as published`
52			`// by the Free Software Foundation, either version 3 of the License, or (at`
53			`// your option) any later version.`
54			`//`
55			`// This program is distributed in the hope that it will be useful, but WITHOUT`
56			`// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or`
57			`// FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License`
58			`// for more details.`
59			`//`
60	201	dgisselq	`// You should have received a copy of the GNU General Public License along`
61			`// with this program. (It's in the $(ROOT)/doc directory. Run make with no`
62			`// target there if the PDF file isn't present.) If not, see`
63			`// <http://www.gnu.org/licenses/> for a copy.`
64			`//`
65	2	dgisselq	`// License: GPL, v3, as defined and found on www.gnu.org,`
66			`// http://www.gnu.org/licenses/gpl.html`
67			`//`
68			`//`
69			`////////////////////////////////////////////////////////////////////////////////`
70			`//`
71	201	dgisselq	`//`
72	209	dgisselq	`default_nettype none
73			`//`
74			`module zipjiffies(i_clk, i_reset, i_ce,`
75	2	dgisselq	`i_wb_cyc, i_wb_stb, i_wb_we, i_wb_data,`
76			`o_wb_ack, o_wb_stall, o_wb_data,`
77			`o_int);`
78	160	dgisselq	`parameter BW = 32;`
79	209	dgisselq	`input wire i_clk, i_reset, i_ce;`
80	2	dgisselq	`// Wishbone inputs`
81	209	dgisselq	`input wire i_wb_cyc, i_wb_stb, i_wb_we;`
82			`input wire [(BW-1):0] i_wb_data;`
83	2	dgisselq	`// Wishbone outputs`
84			`output reg o_wb_ack;`
85			`output wire o_wb_stall;`
86			`output wire [(BW-1):0] o_wb_data;`
87			`// Interrupt line`
88			`output reg o_int;`
89
90			`//`
91			`// Our counter logic: The counter is always counting up--it cannot`
92			`// be stopped or altered. It's really quite simple. Okay, not quite.`
93			`// We still support the clock enable line. We do this in order to`
94			`// support debugging, so that if we get everything running inside a`
95			`// debugger, the timer's all slow down so that everything can be stepped`
96			`// together, one clock at a time.`
97			`//`
98			`reg [(BW-1):0] r_counter;`
99	209	dgisselq	`initial r_counter = 0;`
100	2	dgisselq	`always @(posedge i_clk)`
101	209	dgisselq	`if (i_reset)`
102			`r_counter <= 0;`
103			`else if (i_ce)`
104	2	dgisselq	`r_counter <= r_counter+1;`
105
106			`//`
107			`// Writes to the counter set an interrupt--but only if they are in the`
108			`// future as determined by the signed result of an unsigned subtract.`
109			`//`
110			`reg int_set, new_set;`
111			`reg [(BW-1):0] int_when, new_when;`
112			`wire signed [(BW-1):0] till_when, till_wb;`
113			`assign till_when = int_when-r_counter;`
114			`assign till_wb = new_when-r_counter;`
115	9	dgisselq
116			`initial new_set = 1'b0;`
117			`always @(posedge i_clk)`
118	209	dgisselq	`if (i_reset)`
119	160	dgisselq	`begin`
120	209	dgisselq	`new_set <= 1'b0;`
121			`new_when <= 0;`
122			`end else begin`
123			`// Delay WB commands (writes) by a clock to simplify our logic`
124			`new_set <= ((i_wb_stb)&&(i_wb_we));`
125	160	dgisselq	`// new_when is a don't care when new_set = 0, so don't worry`
126			`// about setting it at all times.`
127			`new_when<= i_wb_data;`
128			`end`
129	9	dgisselq
130	2	dgisselq	`initial o_int = 1'b0;`
131			`initial int_set = 1'b0;`
132			`always @(posedge i_clk)`
133	209	dgisselq	`if (i_reset)`
134	2	dgisselq	`begin`
135	209	dgisselq	`o_int <= 0;`
136			`int_set <= 0;`
137			`end else begin`
138	2	dgisselq	`o_int <= 1'b0;`
139			`if ((i_ce)&&(int_set)&&(r_counter == int_when))`
140	160	dgisselq	`// Interrupts are self-clearing`
141			`o_int <= 1'b1; // Set the interrupt flag for one clock`
142			`else if ((new_set)&&(till_wb <= 0))`
143			`o_int <= 1'b1;`
144	2	dgisselq
145	160	dgisselq	`if ((new_set)&&(till_wb > 0))`
146			`int_set <= 1'b1;`
147			`else if ((i_ce)&&(r_counter == int_when))`
148			`int_set <= 1'b0;`
149	2	dgisselq	`end`
150
151	209	dgisselq	`always @(posedge i_clk)`
152			`if ((new_set)&&(till_wb > 0)&&((till_wb<till_when)\|\|(!int_set)))`
153			`int_when <= new_when;`
154
155	2	dgisselq	`//`
156			`// Acknowledge any wishbone accesses -- everything we did took only`
157			`// one clock anyway.`
158			`//`
159	209	dgisselq	`initial o_wb_ack = 1'b0;`
160	2	dgisselq	`always @(posedge i_clk)`
161	209	dgisselq	`if (i_reset)`
162			`o_wb_ack <= 1'b0;`
163			`else`
164			`o_wb_ack <= i_wb_stb;`
165	9	dgisselq
166	2	dgisselq	`assign o_wb_data = r_counter;`
167			`assign o_wb_stall = 1'b0;`
168	209	dgisselq
169			`// Make verilator happy`
170			`// verilator lint_off UNUSED`
171			`wire unused;`
172			`assign unused = i_wb_cyc;`
173			`// verilator lint_on UNUSED`
174			`ifdef FORMAL
175			`reg f_past_valid;`
176			`initial f_past_valid = 1'b0;`
177			`always @(posedge i_clk)`
178			`f_past_valid <= 1'b1;`
179
180			`////////////////////////////////////////////////`
181			`//`
182			`//`
183			`// Assumptions about our inputs`
184			`//`
185			`//`
186			`////////////////////////////////////////////////`
187			`//`
188			`// Some basic WB assumtions`
189
190			`// We will not start out in a wishbone cycle`
191			`initial assume(!i_wb_cyc);`
192
193			`// Following any reset the cycle line will be low`
194			`always @(posedge i_clk)`
195			`if ((f_past_valid)&&($past(i_reset)))`
196			`assume(!i_wb_cyc);`
197
198			`// Anytime the stb is high, the cycle line must also be high`
199			`always @(posedge i_clk)`
200			`assume((!i_wb_stb)\|\|(i_wb_cyc));`
201
202
203			`////////////////////////////////////////////////`
204			`//`
205			`//`
206			`// Assumptions about our bus outputs`
207			`//`
208			`//`
209			`////////////////////////////////////////////////`
210			`//`
211
212			`// We never stall the bus`
213			`always @(*)`
214			`assert(!o_wb_stall);`
215			`// We always ack every transaction on the following clock`
216			`always @(posedge i_clk)`
217			`if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb)))`
218			`assert(o_wb_ack);`
219			`else`
220			`assert(!o_wb_ack);`
221
222
223			`////////////////////////////////////////////////`
224			`//`
225			`//`
226			`// Assumptions about our internal state and our outputs`
227			`//`
228			`//`
229			`////////////////////////////////////////////////`
230			`//`
231			`always @(posedge i_clk)`
232			`if ((f_past_valid)&&($past(i_reset)))`
233			`begin`
234			`assert(!o_wb_ack);`
235			`end`
236
237			`always @(posedge i_clk)`
238			`if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))`
239			`&&($past(i_wb_we)))`
240			`assert(new_when == $past(i_wb_data));`
241
242			`always @(posedge i_clk)`
243			`if ((f_past_valid)&&(!$past(i_reset))&&($past(i_wb_stb))`
244			`&&($past(i_wb_we)))`
245			`assert(new_set);`
246			`else`
247			`assert(!new_set);`
248
249			`//`
250			`//`
251			`//`
252
253			`always @(posedge i_clk)`
254			`if ((f_past_valid)&&($past(i_reset)))`
255			`assert(!o_int);`
256
257			`always @(posedge i_clk)`
258			`if ((f_past_valid)&&($past(i_reset)))`
259			`begin`
260			`assert(!int_set);`
261			`assert(!new_set);`
262			`end`
263
264			`always @(posedge i_clk)`
265			`if ((f_past_valid)&&(!$past(i_reset))&&($past(new_set))`
266			`&&(!$past(till_wb[BW-1]))`
267			`&&($past(till_wb) > 0))`
268			`assert(int_set);`
269
270			`always @(posedge i_clk)`
271			`if ((f_past_valid)&&(!$past(i_reset))&&($past(i_ce))`
272			`&&($past(r_counter)==$past(int_when)))`
273			`begin`
274			`assert((o_int)\|\|(!$past(int_set)));`
275			`assert((!int_set)\|\|($past(new_set)));`
276			`end`
277
278			`always @(posedge i_clk)`
279			`if ((f_past_valid)&&(!$past(i_reset))&&(!$past(new_set))&&(!$past(int_set)))`
280			`assert(!int_set);`
281
282			`always @(posedge i_clk)`
283			`if ((!f_past_valid)\|\|($past(i_reset)))`
284			`assert(!o_int);`
285			`else if (($past(new_set))&&($past(till_wb) < 0))`
286			`assert(o_int);`
287
288			`always @(posedge i_clk)`
289			`if ((f_past_valid)&&`
290			`((!$past(new_set))`
291			`\|\|($past(till_wb[BW-1]))`
292			`\|\|($past(till_wb == 0))))`
293			`assert(int_when == $past(int_when));`
294			`//`
295			`endif
296	2	dgisselq	`endmodule`

Browse

Tools

Subversion Repositories zipcpu

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