PMU_quota.sv 8.38 KB
Newer Older
Guillem's avatar
Guillem committed
1
//-----------------------------------------------------
GuillemCabo's avatar
GuillemCabo committed
2
3
//  DEPRECATED. DO NOT USE
//-----------------------------------------------------
Guillem's avatar
Guillem committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
// ProjectName: LEON3_kc705_pmu
// Function   : Submodule of the PMU to handle quota consumption of a single
//              core.
// Description: This module checks the content of the counters selected by the
//              mask register. The value of the selected counters is added and
//              compared against the quota limit register.  If the total quota 
//              is exceeded then an interrupt is risen.
//
//              To account for a given event a 1 must be set to the Quota mask 
//              register. When the mask is 0 the value is not accounted for the
//              quota.
//
//              The adition of counters is sequential, therefore you could
//              notice up to N cycles (where N is the number of counters
//              ) from the point that the quota is exceeded until the point
//              where the interrupt is risen. 
//
// Coder      : G.Cabo
// References : 

`default_nettype none
`timescale 1 ns / 1 ps

`ifndef SYNT
    `ifdef FORMAL 
        `define ASSERTIONS
    `endif
`endif
module PMU_quota #
	(
		// Width of counters registers
		parameter integer REG_WIDTH	= 32,
		// Amount of counters
		parameter integer N_COUNTERS	= 9,
        //Localparameters
Guillem's avatar
Guillem committed
39
        //TODO: extend if needed more control
40
        localparam max_width = $clog2(N_COUNTERS)+REG_WIDTH
Guillem's avatar
Guillem committed
41
42
43
44
45
46
47
48
49
50
51
52
53
54
	)
	(
		// Global Clock Signal
		input wire  clk_i,
		// Global Reset Signal. This Signal is Active LOW
		input wire  rstn_i,
        // Input wire from wrapper containing the values of the counters
        input wire [REG_WIDTH-1:0] counter_value_i [0:N_COUNTERS-1],
        // Soft Reset Signal from configuration registeres. This Signal is 
            // Active HIGH
		input wire  softrst_i,
        // Input wire from wrapper with the maximum allowed quota consumption
            //Quota is calculated with the
            //sum_all_counters (counter_value_i[n] * counter_quota_mask_i[n]) 
55
        input wire [REG_WIDTH-1:0] quota_limit_i,
Guillem's avatar
Guillem committed
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
        // Input quota interrupt mask. Only counters with their corresponding
            // mask interrupt set to high can be added to compute towards the
            // total quota that triggers the interrupt
        input wire [N_COUNTERS-1:0] quota_mask_i, 
        // Interrupt quota
        output wire intr_quota_o 
	);

//-------------Quota
    //A quota consumption interruption is generated when the total of 
    //measured events exceeds the value set in quota_limit_i.
    
    //To account for a given event a 1 must be set to the correspondent bit in
    //quota_mask_i.
    //When the mask is 0 the value is not accounted for the quota.
    
    // Maximum width of counter to prevent overflow given the addition of N 
        //values of fix width
    // Mask counter values that are disabled
    wire [REG_WIDTH-1:0] masked_counter_value_int [0:N_COUNTERS-1];
    genvar x;
    generate
        //mask counter values
        for (x=0; x<N_COUNTERS; x=x+1) begin : mask_counters
            //when reset is eneabled the values are 0. If not reset
            // check the mask and pass the value of the counter if enabled
            assign masked_counter_value_int[x]=
                    (softrst_i || (rstn_i == 1'b0))
                    ? {REG_WIDTH{1'b0}} : {REG_WIDTH{quota_mask_i[x]}} & counter_value_i[x];
        end
    endgenerate
    
    //Add values of all the masked signals sequentially
    // state_int shall  jump to reset state if the mask changes
    wire new_mask;
    reg [N_COUNTERS-1:0] old_mask;
GuillemCabo's avatar
GuillemCabo committed
92
    always_ff @(posedge clk_i) begin
Guillem's avatar
Guillem committed
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
        if(rstn_i == 1'b0 ) begin
            old_mask <= {N_COUNTERS{1'b0}};
        end else if(softrst_i) begin 
            old_mask <= {N_COUNTERS{1'b0}};
        end else begin
            old_mask <= quota_mask_i;
        end
    end
    assign new_mask = old_mask != quota_mask_i ? 1'b1: 1'b0;
        //generate  a freespining counter to add values masked registers
        //State 0 = Reset suma_int
        //State 1 = Add counter 0 + Suman_int
        // ...
        //State n = Add counter n + Suman_int
        //State 0 = Reset suma_int
        // ...
109
110
    localparam N_BITS_STATES =$clog2(N_COUNTERS+1);
    reg [N_BITS_STATES-1:0] state_int;
GuillemCabo's avatar
GuillemCabo committed
111
    always_ff @(posedge clk_i) begin
Guillem's avatar
Guillem committed
112
113
        integer i;
        if(rstn_i == 1'b0 ) begin
114
                state_int <={N_BITS_STATES{1'b0}};
Guillem's avatar
Guillem committed
115
        end else if(softrst_i || new_mask) begin 
116
                state_int <={N_BITS_STATES{1'b0}};
Guillem's avatar
Guillem committed
117
        end else begin
118
119
120
121
            if(state_int >= N_BITS_STATES'(N_COUNTERS)) begin
                //prevent overflow of statemachine
                state_int <= 0;
            end else begin            
GuillemCabo's avatar
GuillemCabo committed
122
                state_int <= N_BITS_STATES'(state_int + 1'b1);
123
            end
Guillem's avatar
Guillem committed
124
125
126
127
128
129
        end
    end
    // One state per counter +  reset state -> $clog2(N_COUNTERS+1)

    localparam padding0 = max_width - REG_WIDTH;
    reg [max_width-1:0] suma_int;
GuillemCabo's avatar
GuillemCabo committed
130
    always_ff @(posedge clk_i) begin
Guillem's avatar
Guillem committed
131
132
133
134
135
136
137
        integer i;
        if(rstn_i == 1'b0 ) begin
                suma_int <={max_width{1'b0}};
        end else begin
            if(softrst_i) begin
                suma_int <={max_width{1'b0}};
            end else begin          
138
                if(new_mask || (state_int==0)) begin
Guillem's avatar
Guillem committed
139
140
                    suma_int <={max_width{1'b0}};
                end else begin
141
                    suma_int <= suma_int + {{padding0{1'b0}},masked_counter_value_int[state_int-1]}; 
Guillem's avatar
Guillem committed
142
143
144
145
146
                end
            end
        end
    end

Guillem's avatar
Guillem committed
147
148
    //Hold the state of the interruption
    reg hold_intr_quota;
GuillemCabo's avatar
GuillemCabo committed
149
    always_ff @(posedge clk_i) begin
Guillem's avatar
Guillem committed
150
151
152
153
154
155
        if(rstn_i == 1'b0 ) begin
                hold_intr_quota <= 1'b0; 
        end else begin
            if(softrst_i) begin
                hold_intr_quota <= 1'b0; 
            end else begin
156
                hold_intr_quota <= hold_intr_quota | intr_quota_o;
Guillem's avatar
Guillem committed
157
158
159
160
161
162
            end
        end
    end
    
    //Check if quota is exceeded and generate interrupt or interrupt has been
    //previously triggered and never reseted
GuillemCabo's avatar
GuillemCabo committed
163
    assign intr_quota_o = (suma_int > max_width'(quota_limit_i) )
Guillem's avatar
Guillem committed
164
                        ? 1'b1 : hold_intr_quota;
Guillem's avatar
Guillem committed
165
166
167
168
169
170
171

////////////////////////////////////////////////////////////////////////////////
//
// Formal Verification section begins here.
//
////////////////////////////////////////////////////////////////////////////////
`ifdef	FORMAL
GuillemCabo's avatar
GuillemCabo committed
172
    /*
Guillem's avatar
Guillem committed
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
    //auxiliar registers
    reg f_past_valid ;
    initial f_past_valid = 1'b0;
    //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
    always @(*) begin
		if(0 == f_past_valid) begin
            assume(0 == rstn_i);
         end
    end
         
   default clocking @(posedge clk_i); endclocking   
   // Set quotalimit stable and trigger the interrupt
   cover property (((quota_limit_i==5)[*5] |-> (intr_quota_o==1))); 
   // Set all the the events in the mask to one and keep it stable
   cover property ((quota_mask_i== {N_COUNTERS{1'b1}})[*5] |-> (intr_quota_o==1));
GuillemCabo's avatar
GuillemCabo committed
192
   */
Guillem's avatar
Guillem committed
193
   // Roll over the max value of suma_int
194
   /*
Guillem's avatar
Guillem committed
195
196
   cover property (($past(suma_int)=={max_width{1'b1}})
                    &&(rstn_i == 1) &&(softrst_i == 0)
197
                    && (new_mask==0)[*(2**N_BITS_STATES)+2] |-> (intr_quota_o==1)
Guillem's avatar
Guillem committed
198
                    );
199
    */
Guillem's avatar
Guillem committed
200
    // Count up, count 0 and count up again. Interrupt shall be stable 
201
202
/*Disabled after change the maximum quota to REG_WIDTH from max_width
 * cover property (
Guillem's avatar
Guillem committed
203
204
205
206
207
                    ($past(suma_int,1)=={max_width{1'b1}})
                    &&($past(suma_int,2)=={max_width{1'b0}})
                    &&($past(suma_int,3)=={max_width{1'b1}})
                    &&(rstn_i == 1) &&(softrst_i == 0)
                    );
208
*/
Guillem's avatar
Guillem committed
209
210
    // The interruption can't fall once it is risen unless the unit is
    // softreset 
GuillemCabo's avatar
GuillemCabo committed
211
    /*
Guillem's avatar
Guillem committed
212
213
214
215
    assert property ($rose(intr_quota_o) |-> ($past(softrst_i)||$past(rstn_i)));
    // The interruption shall be high eventually
    assert property (##[0:$] intr_quota_o );

216
217
218
    //Since state_int is fully encoded and needs one state for each counter
    //+ a reset state. state_int can't be larger than the number of counters
    assert property (state_int <= N_COUNTERS);
Guillem's avatar
Guillem committed
219
220
221
    // use all inputs. Roll over all the states of the addition once before
    // trigger an interrupt
    //TODO
GuillemCabo's avatar
GuillemCabo committed
222
*/
Guillem's avatar
Guillem committed
223
224
225
226
227
`endif

endmodule

`default_nettype wire //allow compatibility with legacy code and xilinx ip