MCCU.sv 17.7 KB
Newer Older
Guillem's avatar
Guillem committed
1
2
3
4
//-----------------------------------------------------
// ProjectName: PMU research 
// Function   : Implementation of Maximum-Contention Control Unit (MCCU): 
//              ResourceAccess Count and Contention Time Enforcement.
GuillemCabo's avatar
GuillemCabo committed
5
6
7
// Description: Mechanism that estimates the contention caused for each event,
//              the contention caused is substracted from the asigned quota.
//              When the quota is 0 an interrupt is risen.
Guillem's avatar
Guillem committed
8
9
10
11
12
// Coder      : G.Cabo
// References : https://upcommons.upc.edu/handle/2117/133656

`default_nettype none
//`define DEBUG
Guillem's avatar
Guillem committed
13
14
15
16
17
18
19

`ifndef SYNT
    `ifdef FORMAL 
        `define ASSERTIONS
    `endif
`endif

Guillem's avatar
Guillem committed
20
21
22
23
24
25
`timescale 1 ns / 1 ps
	module MCCU #
	(
		// Width of data registers
		parameter integer DATA_WIDTH	= 32,
		// Width of weights registers
Guillem's avatar
Guillem committed
26
		parameter integer WEIGHTS_WIDTH	= 8,
27
        //Cores. Change this may break Verilator TB
28
        parameter integer N_CORES       =2,
29
        //Signals per core. Change this may break Verilator TB
Guillem's avatar
Guillem committed
30
        parameter integer CORE_EVENTS   =4
Guillem's avatar
Guillem committed
31
32
33
	)
	(
		input wire clk_i,
GuillemCabo's avatar
GuillemCabo committed
34
        //Active low syncronous reset. It can have hardware or software source
Guillem's avatar
Guillem committed
35
		input wire rstn_i,
36
37
		//Active high enable. If enabled quota can decrease and interruptions
        //can be generated
Guillem's avatar
Guillem committed
38
39
40
41
42
        input wire enable_i,
        //Monitored events that can generate contention in the system
        input wire [CORE_EVENTS-1:0] events_i [0:N_CORES-1],
        //Quota for each of the cores, internally registered, set by software
        input wire [DATA_WIDTH-1:0] quota_i [0:N_CORES-1],
43
44
        //Update quota. Set quota_int to the value of quota_i
        input wire update_quota_i [0:N_CORES-1],
45
        //Internal quota available
Guillem's avatar
Guillem committed
46
47
48
49
50
51
52
        output wire [DATA_WIDTH-1:0] quota_o [0:N_CORES-1],
        //Worst contention that  each of the previous events can generate,
        //internally registered, set by software, if 0 event is dissabled
        input wire [WEIGHTS_WIDTH-1:0] events_weights_i [0:N_CORES-1]
                                                       [0:CORE_EVENTS-1],
        //Quota interruption
        output wire interruption_quota_o[N_CORES-1:0]
Guillem's avatar
Guillem committed
53
    );
Guillem's avatar
Guillem committed
54
55
56
57
58
59
60
61
62
63
64
    //Parameters required for additions and substractions of quotas.
    //OVERFLOW_PROT can be reduced. It needs to be a bit larger than 
    //DATA_WIDTH. 
    localparam integer OVERFLOW_PROT = DATA_WIDTH*2;
    //avoid width mismatch when add: OVERFLOW_PROT + DATA_WIDTH
    localparam O_D_0PAD = OVERFLOW_PROT-DATA_WIDTH;
    //avoid width mismatch when add: DATA_WIDTH + WEIGHTS_WIDTH
    localparam D_W_0PAD = DATA_WIDTH-WEIGHTS_WIDTH;
    //avoid width mismatch when add: OVERFLOW_PROT + WEIGHTS_WIDTH
    localparam O_W_0PAD = OVERFLOW_PROT-WEIGHTS_WIDTH;
    
GuillemCabo's avatar
GuillemCabo committed
65
    //internal signals
Guillem's avatar
Guillem committed
66
67
68
    reg [DATA_WIDTH-1:0] quota_int [0:N_CORES-1];//Quota set by external registers
    wire [WEIGHTS_WIDTH-1:0] events_weights_int [0:N_CORES-1] [0:CORE_EVENTS-1];
    reg [OVERFLOW_PROT-1:0] ccc_suma_int [0:N_CORES-1];//Addition of current cycle
Guillem's avatar
Guillem committed
69
70
                                               //consumed quota
    `ifdef DEBUG
Guillem's avatar
Guillem committed
71
72
73
    reg [OVERFLOW_PROT-1:0] debug_ccc_suma_int;//Just one core
    reg [OVERFLOW_PROT-1:0] debug_ccc_suma_loop_int;//Just one core
    reg [WEIGHTS_WIDTH-1:0] debug_events_weights_int [0:CORE_EVENTS-1];//Just one core
Guillem's avatar
Guillem committed
74
75
76
77
    integer k;  
    integer debug_tmp = 0;
    `endif
    /*----------
GuillemCabo's avatar
GuillemCabo committed
78
    Generate one mechanism to monitor the quota for each of the cores in the
Guillem's avatar
Guillem committed
79
80
81
82
    SOC,
    ----------*/
    integer i;
    integer j;
Guillem's avatar
Guillem committed
83
//    generate begin : GeneratedQuotaMonitor
GuillemCabo's avatar
GuillemCabo committed
84
    always @(posedge clk_i) begin: syncReset
Guillem's avatar
Guillem committed
85
86
87
88
89
90
91
        /*----------
        Auxiliar variables
        ----------*/
        longint tmp_ccc_suma_int;//temporal addition of ccc_suma_int
        /*----------
        Reset 
        ----------*/
Guillem's avatar
Guillem committed
92
        if(rstn_i == 1'b0 ) begin
Guillem's avatar
Guillem committed
93
            /*----------
GuillemCabo's avatar
GuillemCabo committed
94
            sync reset Quota
Guillem's avatar
Guillem committed
95
96
97
98
99
            ----------*/
            for (i=0; i<N_CORES; i=i+1) begin : ResetQuota
                quota_int[i] <={DATA_WIDTH{1'b0}}; 
            end
            /*----------
GuillemCabo's avatar
GuillemCabo committed
100
            sync reset current cycle consumed quota
Guillem's avatar
Guillem committed
101
102
103
104
105
            ----------*/
            for (i=0; i<N_CORES; i=i+1) begin : ResetCCCQuota
                ccc_suma_int[i] <={OVERFLOW_PROT{1'b0}}; 
            end
            /*----------
GuillemCabo's avatar
GuillemCabo committed
106
            sync reset debug registers
Guillem's avatar
Guillem committed
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
            ----------*/
            `ifdef DEBUG
            debug_ccc_suma_int <= {OVERFLOW_PROT{1'b0}};
            debug_ccc_suma_loop_int <= {OVERFLOW_PROT{1'b0}};
            for (i=0; i<N_CORES; i=i+1) begin : ResetDebugEvents
            debug_events_weights_int [i]<= {WEIGHTS_WIDTH{1'b0}};
            end
            `endif
        end else begin
        /*----------
        Normal operation
        ----------*/
            /*----------
            Substract to the core quota the weight of each active
            event during this cycle. If the event is active the value
            of the weight is substracted, if not 0 is substracted. Only
            substract quota if enable is active. If the quota has been updated
            this cycle  quota_i is bypass
            ----------*/
            
            //Cases to change the values of quota
            `ifdef ASSERTIONS
            //If unit was not in reset and has not been reseted this cycle
            if($past(rstn_i)&& rstn_i) begin
                for (i=0; i<N_CORES; i=i+1) begin : AssertionsQuotaNonReset
                    //!Enable && !update: hold values quota_int
133
                    if(!$past(enable_i) && !$past(update_quota_i[i])) begin
Guillem's avatar
Guillem committed
134
                        assert(quota_int[i] == $past(quota_int[i]));
Guillem's avatar
Guillem committed
135
136
                    end
                    
Guillem's avatar
Guillem committed
137
138
                    //!Enable && update: Update values quota_int with quota_i,
                    //                      do NOT substract 
139
                    if(!$past(enable_i) && $past(update_quota_i[i])) begin
Guillem's avatar
Guillem committed
140
                        assert(quota_int[i] == $past(quota_i[i]));
Guillem's avatar
Guillem committed
141
                    end
Guillem's avatar
Guillem committed
142
143
144
145
146
                    
                    //Enable && !update:Replace quota_int with quota_int minus
                    //                      consumed quota (ccc_quota). If
                    //                      underflow the content of 
                    //                      quota_int[i] can be 0.
147
                    if($past(enable_i) && !$past(update_quota_i[i])) begin
Guillem's avatar
Guillem committed
148
149
150
                        assert(quota_int[i] == ($past(quota_int[i])-$past(ccc_suma_int[i])) 
                                                || (quota_int[i]==
                                                   {DATA_WIDTH{1'b0}}));
Guillem's avatar
Guillem committed
151
                    end
Guillem's avatar
Guillem committed
152
153
154
155
156
                    
                    //Enable && update: Update values quota_int with quota_i and 
                    //                      substract ccc_quota if  
                    //                      underflow the content of 
                    //                      quota_int[i] can be 0.
157
                    if($past(enable_i) && $past(update_quota_i[i])) begin
Guillem's avatar
Guillem committed
158
159
160
                        assert(quota_int[i] == ($past(quota_i[i])-$past(ccc_suma_int[i]))
                                                || (quota_int[i]==
                                                   {DATA_WIDTH{1'b0}}));
Guillem's avatar
Guillem committed
161
                    end
Guillem's avatar
Guillem committed
162
163
164
165
                end
            end else begin
            //if the  unit has been reseted in current or  previous cycle
                for (i=0; i<N_CORES; i=i+1) begin : AssertionsQuotaReset
Guillem's avatar
Guillem committed
166
                    assert(quota_int[i] == {DATA_WIDTH{1'b0}});
Guillem's avatar
Guillem committed
167
168
169
                end
            end
            `endif
Guillem's avatar
Guillem committed
170

Guillem's avatar
Guillem committed
171
172
            for (i=0; i<N_CORES; i=i+1) begin : SetQuota
                //!Enable && !update: hold values quota_int
173
                if(!enable_i && !update_quota_i[i]) begin
Guillem's avatar
Guillem committed
174
175
176
                    quota_int[i] <= quota_int[i];
                //!Enable && update: Update values quota_int with quota_i,
                //                      do NOT substract 
177
                end else if (!enable_i && update_quota_i[i]) begin
Guillem's avatar
Guillem committed
178
179
180
                    quota_int[i] <= quota_i[i]; 
                //Enable && !update:Replace quota_int with quota_int minus
                //                      consumed quota (ccc_quota)
181
                end else if (enable_i && !update_quota_i[i]) begin
Guillem's avatar
Guillem committed
182
183
184
185
186
187
188
189
                    for (j=0; j<CORE_EVENTS; j=j+1) begin
                            //underflow detection. Padding needed for
                            // prevent width mismatch
                            if( ccc_suma_int[i] > {{O_D_0PAD{1'b0}},quota_int[i]} )
                            begin
                                quota_int[i] <={DATA_WIDTH{1'b0}};  
                            end else begin
                                quota_int[i] <= quota_int[i] - ccc_suma_int[i][DATA_WIDTH-1:0];  
Guillem's avatar
Guillem committed
190
                            end
Guillem's avatar
Guillem committed
191
192
193
                    end
                //Enable && update: Update values quota_int with quota_i and 
                //                      substract ccc_quota 
194
                end else if(enable_i && update_quota_i[i])begin
Guillem's avatar
Guillem committed
195
196
197
198
199
200
201
202
                    for (j=0; j<CORE_EVENTS; j=j+1) begin
                            //underflow detection. Padding needed for
                            // prevent width mismatch
                            if( ccc_suma_int[i] > {{O_D_0PAD{1'b0}},quota_i[i]} )
                            begin
                                quota_int[i] <={DATA_WIDTH{1'b0}};  
                            end else begin
                                quota_int[i] <= quota_i[i] - ccc_suma_int[i][DATA_WIDTH-1:0];  
Guillem's avatar
Guillem committed
203
204
205
206
207
                            end
                    end
                end
            end
            /*----------
Guillem's avatar
Guillem committed
208
209
210
            Add quotas of all active signals. The ones that are not
            enabled are 0. The quotas in  ccc_suma_int[i] are added at every
            cycle independently of the enable signal, but ccc_suma_int will
Guillem's avatar
Guillem committed
211
            only be substracted to the quota if MCCU is enabled
Guillem's avatar
Guillem committed
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
            ----------*/ 
            for (i=0; i<N_CORES; i=i+1) begin : AddEventsWeights
                tmp_ccc_suma_int=0;
                for (j=0; j<CORE_EVENTS; j=j+1) begin
                        //Reguired to avoid warning. Blocking
                        //Assigment is legal when usign temporal
                        //variables.
                        /* verilator lint_off BLKSEQ */
                        tmp_ccc_suma_int ={{O_W_0PAD{1'b0}},events_weights_int[i][j]} + tmp_ccc_suma_int;  
                        /* verilator lint_on BLKSEQ */
                end
                ccc_suma_int[i]<=tmp_ccc_suma_int;
                `ifdef DEBUG
                /* verilator lint_off WIDTH */
                /* verilator lint_off BLKSEQ */
                //This only applies when 4 events are available
                    if(i==0 && CORE_EVENTS==4) begin
                        debug_events_weights_int <= events_weights_int [0];//assign to core 0
                        debug_ccc_suma_int <= debug_events_weights_int[0]+debug_events_weights_int[1]+debug_events_weights_int[2]+debug_events_weights_int[3];
                        debug_tmp=0;
                        for(k=0; k<CORE_EVENTS; k=k+1) begin
                                debug_tmp  =debug_events_weights_int[k] + debug_tmp;  
                        end
                        debug_ccc_suma_loop_int <= debug_tmp;
                    end
                    
                    `ifdef ASSERTIONS
                    assert(debug_ccc_suma_int == debug_ccc_suma_loop_int);
                    `endif
                //disable BLKSeK for the temporal assigment of debug_tmp
                /* verilator lint_on BLKSEQ */
                /* verilator lint_on WIDTH */
                `endif
Guillem's avatar
Guillem committed
245
            end
Guillem's avatar
Guillem committed
246
247
248
        end 
    end
    /*----------
GuillemCabo's avatar
GuillemCabo committed
249
250
    Set weights of events, as this module is used whith a 
    wrapper the values are already registered 
Guillem's avatar
Guillem committed
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
    outside and only need to be forwarded without register them internally.
    Apply the event as a mask. If the event is inactive in the current cycle
    0 is forwarded in events_weights_int for that event.
    ----------*/
    genvar x;
    genvar y;
    for (x=0; x<N_CORES; x=x+1) begin : SetEventsWeights
        for (y=0; y<CORE_EVENTS; y=y+1) begin
            assign     events_weights_int [x][y] = events_i[x][y] ? events_weights_i[x][y]:{WEIGHTS_WIDTH{1'b0}};
        end
    end
    /*----------
    Generate interruptions for quota for each core. Interrupt triggers
    one cycle before the result is registered. There is no record of
    by how much the quota was exceeded. Interruption is only generated if the 
    MCCU is enabled
    ----------*/
GuillemCabo's avatar
GuillemCabo committed
268
269
270
    wire interruption_quota_d[N_CORES-1:0];
    reg interruption_quota_q[N_CORES-1:0];

Guillem's avatar
Guillem committed
271
    for(x=0; x<N_CORES; x=x+1)  begin: InterruptionQuota
GuillemCabo's avatar
GuillemCabo committed
272
        assign interruption_quota_d[x] =
Guillem's avatar
Guillem committed
273
274
275
                 !enable_i ? 1'b0:
                 (ccc_suma_int[x]>{{O_D_0PAD{1'b0}},quota_int[x]})? 1'b1:1'b0;
    end
GuillemCabo's avatar
GuillemCabo committed
276
277
278
279

    for(x=0; x<N_CORES; x=x+1)  begin: InterruptionQuotaHold
        always @(posedge clk_i) begin
            if(rstn_i == 1'b0 ) begin
GuillemCabo's avatar
GuillemCabo committed
280
                interruption_quota_q[x] <= 1'b0;
GuillemCabo's avatar
GuillemCabo committed
281
            end else begin
282
283
284
285
286
                if(enable_i) begin
                    interruption_quota_q[x] <= interruption_quota_d[x] | interruption_quota_q[x];
                end else begin
                    interruption_quota_q[x] <= 1'b0;
                end
GuillemCabo's avatar
GuillemCabo committed
287
288
            end
        end
GuillemCabo's avatar
GuillemCabo committed
289
        assign interruption_quota_o[x] = (enable_i && rstn_i) ? interruption_quota_q[x] : 1'b0;
GuillemCabo's avatar
GuillemCabo committed
290
291
    end

Guillem's avatar
Guillem committed
292
293
294
295
    `ifdef ASSERTIONS
    always @(posedge clk_i) begin
        for(integer x=0; x<N_CORES; x=x+1)  begin: InterruptionQuota
            if(quota_int[x]>ccc_suma_int[x])
GuillemCabo's avatar
GuillemCabo committed
296
                assert (interruption_quota_d[x]==1'b0);
Guillem's avatar
Guillem committed
297
298
299
        end
    end
    `endif
Guillem's avatar
Guillem committed
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
    /*----------
    forward results of internal registers 
    ----------*/
    assign quota_o = quota_int;

/*----------
Section of Formal propperties, valid for SBY 
----------*/
`ifdef	FORMAL
    //auxiliar registers
    reg f_past_valid ;
    initial f_past_valid = 1'b0;
    longint f_sum_weights;
    //Set f_past_valid after first clock cycle
    always@( posedge clk_i )
        f_past_valid <= 1'b1;
   
    //assume that if f_past is not valid you have to reset
    //TODO: Will this lead to problems with k-insuction?
    always @(*) begin
		if(0 == f_past_valid) begin
            assume(0 == rstn_i);
         end
    end
    /*--------------
      When reset (rstn_i)is active all internal registers shall be set to 0 in 
326
      the next cycle.
Guillem's avatar
Guillem committed
327
    --------------*/
328
329
    always @(posedge clk_i) begin
		if(0 == $past(rstn_i) && f_past_valid) begin
Guillem's avatar
Guillem committed
330
331
332
333
334
335
336
337
338
339
340
341
            assert(0 == quota_int.sum()); 
            assert(0 == ccc_suma_int.sum()); 
        end
    end
    /*--------------
      Unless a reset occures, the addition of all current cycle consumed
      quota by all the cores (ccc_suma_int[i]) shall be the same that the 
      addition of all the internal weights (events_weights_int[i][j]) of the 
      previous cycle. Internal weights are non registerd and they set to 0 if 
      the signal for a given weight is not active the current cycle.
    --------------*/  
    //Auxiliar logic to compute sum of all signals and consumed quota
GuillemCabo's avatar
GuillemCabo committed
342
    always@( posedge clk_i) begin
Guillem's avatar
Guillem committed
343
344
345
346
347
348
349
350
351
        f_sum_weights =0; //initialize to 0 and add events_weights_int
        if(rstn_i) begin // reset disabled
                for (i=0; i<N_CORES; i=i+1) begin
                    for (j=0; j<CORE_EVENTS; j=j+1) begin
                        f_sum_weights=f_sum_weights + events_weights_int[i][j];
                    end
                end
        end
    end
352
353
    //assert that the addition of quotas consumed in the current cycle
    //equal to the internal weights.
Guillem's avatar
Guillem committed
354
355
356
    always @(posedge clk_i) begin
        if(rstn_i) begin
            assert(f_sum_weights == ccc_suma_int.sum());
357
        end 
Guillem's avatar
Guillem committed
358
359
360
361
362
363
    end
    /*---------
     * checks when the interruption can be triggered
     * --------*/
    //Interruption can be only high if consumed quota is larger than
    //available quota and the MCCU is enabled
GuillemCabo's avatar
GuillemCabo committed
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386

    default clocking @(posedge clk_i); endclocking;
    
    genvar k;
    for(k=0;k<N_CORES;k++) begin
    // If the unit is in reset or disabled the interrupts shall be 0 immediately.
    assert property (
                    (f_past_valid && (rstn_i==0 || enable_i==0))
                    |->
                    (!interruption_quota_o[k])
                    );
    // If an interrup is actrive it shall remain high unless there is a reset
    assert property (
                    (f_past_valid && (interruption_quota_o[k]==1'b1))
                    |=>
                    ($stable(interruption_quota_o[k]) || (!rstn_i || !enable_i))
                    );

    /// If unit is not in reset or disabled. When quota_int[k]<ccc_suma_int[k] the interrupt 
        //shall rise in the next cycle

    end 
/*
387
    always @(posedge clk_i) begin
Guillem's avatar
Guillem committed
388
        for(k=0;k<N_CORES;k++) begin
GuillemCabo's avatar
GuillemCabo committed
389
390
            if (f_past_valid && rstn_i) begin
                if (($past(quota_int[k]<ccc_suma_int[k]) && enable_i)) begin
391
                    //The interruption shall be high
GuillemCabo's avatar
GuillemCabo committed
392
                    assert(interruption_quota_[k]==1'b1);
393
394
395
                    //The interruption can only be high if the MCCU is enabled
                    assert(interruption_quota_o[k]==enable_i);
                end else begin
GuillemCabo's avatar
GuillemCabo committed
396
397
                    //interruption shall be disabled if not enabled or unit in reset
                    if (enable_i== 0 || rstn_i==0) begin
398
                        assert(interruption_quota_o[k]==1'b0);
GuillemCabo's avatar
GuillemCabo committed
399
400
401
402
403
404
405
                    end else begin
                        //if the interrup was high, hold it high
                        if ($past(interruption_quota_o[k])==1'b1) begin
                            assert(interruption_quota_o[k]==1'b1);
                        end else begin
                            assert(interruption_quota_o[k]==1'b0);
                        end
406
407
                    end
                end
Guillem's avatar
Guillem committed
408
409
410
            end
        end
    end
GuillemCabo's avatar
GuillemCabo committed
411
*/ 
Guillem's avatar
Guillem committed
412
`endif
Guillem's avatar
Guillem committed
413
414
415
endmodule
`default_nettype wire //allow compatibility with legacy code and xilinx ip