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

Subversion Repositories zipcpu

[/] [zipcpu/] [trunk/] [bench/] [formal/] [abs_prefetch.v] - Blame information for rev 209

Details | Compare with Previous | View Log

Line No. Rev Author Line
1 209 dgisselq
////////////////////////////////////////////////////////////////////////////////
2
//
3
// Filename:    abs_prefetch.v
4
//
5
// Project:     Zip CPU -- a small, lightweight, RISC CPU soft core
6
//
7
// Purpose:     Rather than feed our CPU with actual valid instructions returned
8
//              from memory, this is an abstract prefetch.  It's not even a
9
//      perfect or complete abstract prefetch at that--it doesn't actually
10
//      access memory.  However, it will maintain the abstract interface with
11
//      the CPU.s
12
//
13
//      In other words, this abs_prefetch may produce the exact same results a
14
//      true prefetch would have produced--whether it be prefetch.v, dblfetch.v,
15
//      or even pfcache.v.  On the other hand, it might not.  If the CPU can
16
//      pass either way, then it can most certainly pass with a true prefetch.
17
//
18
// Creator:     Dan Gisselquist, Ph.D.
19
//              Gisselquist Technology, LLC
20
//
21
////////////////////////////////////////////////////////////////////////////////
22
//
23
// Copyright (C) 2015-2019, Gisselquist Technology, LLC
24
//
25
// This program is free software (firmware): you can redistribute it and/or
26
// modify it under the terms of  the GNU General Public License as published
27
// by the Free Software Foundation, either version 3 of the License, or (at
28
// your option) any later version.
29
//
30
// This program is distributed in the hope that it will be useful, but WITHOUT
31
// ANY WARRANTY; without even the implied warranty of MERCHANTIBILITY or
32
// FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
33
// for more details.
34
//
35
// You should have received a copy of the GNU General Public License along
36
// with this program.  (It's in the $(ROOT)/doc directory.  Run make with no
37
// target there if the PDF file isn't present.)  If not, see
38
// <http://www.gnu.org/licenses/> for a copy.
39
//
40
// License:     GPL, v3, as defined and found on www.gnu.org,
41
//              http://www.gnu.org/licenses/gpl.html
42
//
43
//
44
////////////////////////////////////////////////////////////////////////////////
45
//
46
//
47
`default_nettype        none
48
//
49
module  abs_prefetch(i_clk, i_reset, i_new_pc, i_clear_cache,
50
                        // i_early_branch, i_from_addr,
51
                        i_stall_n, i_pc, o_insn, o_pc, o_valid,
52
                o_wb_cyc, o_wb_stb, o_wb_we, o_wb_addr, o_wb_data,
53
                        i_wb_ack, i_wb_stall, i_wb_err, i_wb_data,
54
                        o_illegal);
55
        parameter       ADDRESS_WIDTH = 30;
56
        localparam      BUSW = 32;      // Number of data lines on the bus
57
        localparam      AW=ADDRESS_WIDTH; // Shorthand for ADDRESS_WIDTH
58
        //
59
        input   wire                    i_clk, i_reset;
60
        //
61
        // The interface with the rest of the CPU
62
        input   wire                    i_new_pc;
63
        input   wire                    i_clear_cache;
64
        input   wire                    i_stall_n;
65
        input   wire    [(AW+1):0]       i_pc;
66
        output  wire    [(BUSW-1):0]     o_insn;
67
        output  wire    [(AW+1):0]       o_pc;
68
        output  wire                    o_valid;
69
        //
70
        // The wishbone bus interface
71
        output  wire                    o_wb_cyc, o_wb_stb;
72
        output  wire                    o_wb_we;
73
        output  wire    [(AW-1):0]       o_wb_addr;
74
        output  wire    [(BUSW-1):0]     o_wb_data;
75
        //
76
        input   wire                    i_wb_ack, i_wb_stall, i_wb_err;
77
        input   wire    [(BUSW-1):0]     i_wb_data;
78
        //
79
        // o_illegal will be true if this instruction was the result of
80
        // a bus error (This is also part of the CPU interface)
81
        output  reg                     o_illegal;
82
        //
83
 
84
        // Fixed bus outputs: we read from the bus only, never write.
85
        // Thus the output data is ... irrelevant and don't care.  We set it
86
        // to zero just to set it to something.
87
        assign  o_wb_cyc  = 0;
88
        assign  o_wb_stb  = 0;
89
        assign  o_wb_we   = 0;
90
        assign  o_wb_addr = 0;
91
        assign  o_wb_data = 0;
92
 
93
 
94
        reg     [(AW-1):0]       r_pc;
95
        reg                     waiting_on_pc;
96
        reg     [5:0]            wait_for_valid;
97
 
98
 
99
 
100
        always @(posedge i_clk)
101
        if (i_new_pc)
102
                r_pc = i_pc[AW+1:2];
103
        else if ((o_valid)&&(i_stall_n))
104
                r_pc <= r_pc + 1'b1;
105
 
106
        (* anyconst *)  reg     [(AW-1):0]       any_pc;
107
        assign  o_pc = { (o_valid) ? r_pc : any_pc, 2'b00 };
108
 
109
 
110
        (* anyseq *)    reg     any_illegal;
111
        always @(posedge i_clk)
112
        if ((i_reset)||(i_clear_cache)||(i_new_pc)||(waiting_on_pc))
113
                o_illegal <= 1'b0;
114
        else if ((!o_illegal)&&(wait_for_valid == 1'b1))
115
                o_illegal <= any_illegal;
116
 
117
        (* anyseq *)    reg     [5:0]    wait_time;
118
        always @(*)
119
                assume(wait_time > 0);
120
 
121
        initial waiting_on_pc <= 1'b1;
122
        always @(posedge i_clk)
123
        if ((i_reset)||(i_clear_cache))
124
                waiting_on_pc <= 1'b1;
125
        else if (i_new_pc)
126
                waiting_on_pc <= 1'b0;
127
 
128
        always @(posedge i_clk)
129
        if ((i_reset)||(i_clear_cache))
130
                wait_for_valid <= 6'h3f;
131
        else if ((i_new_pc)||(waiting_on_pc))
132
                wait_for_valid <= wait_time;
133
        else if (wait_for_valid > 0)
134
                wait_for_valid <= wait_for_valid - 1'b1;
135
 
136
        (* anyseq *)    reg     [(BUSW-1):0]     any_insn;
137
 
138
        assign  o_valid   = (!waiting_on_pc)&&(wait_for_valid == 0);
139
        assign  o_insn    = any_insn;
140
 
141
`ifdef  FORMAL
142
`define ASSUME  assume
143
`define ASSERT  assert
144
 
145
        // Keep track of a flag telling us whether or not $past()
146
        // will return valid results
147
        reg     f_past_valid;
148
        initial f_past_valid = 1'b0;
149
        always @(posedge i_clk)
150
                f_past_valid = 1'b1;
151
        always @(*)
152
        if (!f_past_valid)
153
                `ASSERT(i_reset);
154
 
155
        /////////////////////////////////////////////////
156
        //
157
        //
158
        // Assumptions about our inputs
159
        //
160
        //
161
        /////////////////////////////////////////////////
162
 
163
        //
164
        // Assume we start from a reset condition
165
        initial `ASSERT(i_reset);
166
 
167
        /////////////////////////////////////////////////
168
        //
169
        //
170
        // Assertions about our outputs
171
        //
172
        //
173
        /////////////////////////////////////////////////
174
 
175
        /////////////////////////////////////////////////////
176
        //
177
        //
178
        // Assertions about our return responses to the CPU
179
        //
180
        //
181
        /////////////////////////////////////////////////////
182
 
183
        // Consider it invalid to present the CPU with the same instruction
184
        // twice in a row.
185
        always @(posedge i_clk)
186
        if ((f_past_valid)&&($past(o_valid))&&($past(i_stall_n))&&(o_valid))
187
                assume(o_pc != $past(o_pc));
188
 
189
        always @(*)
190
        begin
191
                `ASSERT(i_pc[1:0] == 2'b00);
192
                assume(o_pc[1:0] == 2'b00);
193
        end
194
 
195
 
196
        //
197
        // Assume we start from a reset condition
198
        initial `ASSUME(i_reset);
199
 
200
        // Assume that any reset is either accompanied by a new address,
201
        // or a new address immediately follows it.
202
        always @(posedge i_clk)
203
        if ((f_past_valid)&&($past(i_reset)))
204
                `ASSERT(i_new_pc);
205
 
206
        //
207
        //
208
        // The bottom two bits of the PC address register are always zero.
209
        // They are there to make examining traces easier, but I expect
210
        // the synthesis tool to remove them.
211
        //
212
        always @(*)
213
                `ASSERT(i_pc[1:0] == 2'b00);
214
 
215
        // Some things to know from the CPU ... there will always be a
216
        // i_new_pc request following any reset
217
        always @(posedge i_clk)
218
        if ((f_past_valid)&&($past(i_reset)))
219
                `ASSERT(i_new_pc);
220
 
221
        // There will also be a i_new_pc request following any request to clear
222
        // the cache.
223
        always @(posedge i_clk)
224
        if ((f_past_valid)&&($past(i_clear_cache)))
225
                `ASSERT(i_new_pc);
226
 
227
        always @(*)
228
                `ASSUME(i_pc[1:0] == 2'b00);
229
 
230
        /////////////////////////////////////////////////
231
        //
232
        //
233
        // Assertions about our outputs
234
        //
235
        //
236
        /////////////////////////////////////////////////
237
 
238
        //
239
        // Assertions about our return responses to the CPU
240
        //
241
        always @(posedge i_clk)
242
        if ((f_past_valid)&&(!$past(i_reset))
243
                        &&(!$past(i_new_pc))&&(!$past(i_clear_cache))
244
                        &&($past(o_valid))&&(!$past(i_stall_n)))
245
        begin
246
                assume($stable(o_pc));
247
                assume($stable(o_insn));
248
                assume($stable(o_valid));
249
                assume($stable(o_illegal));
250
        end
251
 
252
        //
253
        // As with i_pc[1:0], the bottom two bits of the address are unused.
254
        // Let's assert here that they remain zero.
255
        always @(*)
256
                assume(o_pc[1:0] == 2'b00);
257
 
258
        always @(posedge i_clk)
259
        if ((f_past_valid)&&(!$past(o_illegal))&&(o_illegal))
260
                assume(o_valid);
261
 
262
        always @(posedge i_clk)
263
        if ((f_past_valid)&&($past(i_new_pc)))
264
                assume(!o_valid);
265
 
266
`endif  // FORMAL
267
 
268
endmodule

powered by: WebSVN 2.1.0

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