hw/vendor/lowrisc_ibex/rtl/ibex_id_stage.sv Cov: 100%
1: // Copyright lowRISC contributors.
2: // Copyright 2018 ETH Zurich and University of Bologna, see also CREDITS.md.
3: // Licensed under the Apache License, Version 2.0, see LICENSE for details.
4: // SPDX-License-Identifier: Apache-2.0
5:
6: `ifdef RISCV_FORMAL
7: `define RVFI
8: `endif
9:
10: /**
11: * Instruction Decode Stage
12: *
13: * Decode stage of the core. It decodes the instructions and hosts the register
14: * file.
15: */
16: module ibex_id_stage #(
17: parameter bit RV32E = 0,
18: parameter bit RV32M = 1
19: ) (
20: input logic clk_i,
21: input logic rst_ni,
22:
23: input logic test_en_i,
24:
25: input logic fetch_enable_i,
26: output logic ctrl_busy_o,
27: output logic illegal_insn_o,
28:
29: // Interface to IF stage
30: input logic instr_valid_i,
31: input logic instr_new_i,
32: input logic [31:0] instr_rdata_i, // from IF-ID pipeline registers
33: input logic [15:0] instr_rdata_c_i, // from IF-ID pipeline registers
34: input logic instr_is_compressed_i,
35: output logic instr_req_o,
36: output logic instr_valid_clear_o, // kill instr in IF-ID reg
37: output logic id_in_ready_o, // ID stage is ready for next instr
38:
39: // Jumps and branches
40: input logic branch_decision_i,
41:
42: // IF and ID stage signals
43: output logic pc_set_o,
44: output ibex_pkg::pc_sel_e pc_mux_o,
45: output ibex_pkg::exc_pc_sel_e exc_pc_mux_o,
46: output ibex_pkg::exc_cause_e exc_cause_o,
47:
48: input logic illegal_c_insn_i,
49: input logic instr_fetch_err_i,
50:
51: input logic [31:0] pc_id_i,
52:
53: // Stalls
54: input logic ex_valid_i, // EX stage has valid output
55: input logic lsu_valid_i, // LSU has valid output, or is done
56: // ALU
57: output ibex_pkg::alu_op_e alu_operator_ex_o,
58: output logic [31:0] alu_operand_a_ex_o,
59: output logic [31:0] alu_operand_b_ex_o,
60:
61: // MUL, DIV
62: output logic mult_en_ex_o,
63: output logic div_en_ex_o,
64: output ibex_pkg::md_op_e multdiv_operator_ex_o,
65: output logic [1:0] multdiv_signed_mode_ex_o,
66: output logic [31:0] multdiv_operand_a_ex_o,
67: output logic [31:0] multdiv_operand_b_ex_o,
68:
69: // CSR
70: output logic csr_access_o,
71: output ibex_pkg::csr_op_e csr_op_o,
72: output logic csr_save_if_o,
73: output logic csr_save_id_o,
74: output logic csr_restore_mret_id_o,
75: output logic csr_restore_dret_id_o,
76: output logic csr_save_cause_o,
77: output logic [31:0] csr_mtval_o,
78: input ibex_pkg::priv_lvl_e priv_mode_i,
79: input logic csr_mstatus_tw_i,
80: input logic illegal_csr_insn_i,
81:
82: // Interface to load store unit
83: output logic data_req_ex_o,
84: output logic data_we_ex_o,
85: output logic [1:0] data_type_ex_o,
86: output logic data_sign_ext_ex_o,
87: output logic [31:0] data_wdata_ex_o,
88:
89: input logic lsu_addr_incr_req_i,
90: input logic [31:0] lsu_addr_last_i,
91:
92: // Interrupt signals
93: input logic csr_mstatus_mie_i,
94: input logic csr_msip_i,
95: input logic csr_mtip_i,
96: input logic csr_meip_i,
97: input logic [14:0] csr_mfip_i,
98: input logic irq_pending_i,
99: input logic irq_nm_i,
100: output logic nmi_mode_o,
101:
102: input logic lsu_load_err_i,
103: input logic lsu_store_err_i,
104:
105: // Debug Signal
106: output logic debug_mode_o,
107: output ibex_pkg::dbg_cause_e debug_cause_o,
108: output logic debug_csr_save_o,
109: input logic debug_req_i,
110: input logic debug_single_step_i,
111: input logic debug_ebreakm_i,
112: input logic debug_ebreaku_i,
113: input logic trigger_match_i,
114:
115: // Write back signal
116: input logic [31:0] regfile_wdata_lsu_i,
117: input logic [31:0] regfile_wdata_ex_i,
118: input logic [31:0] csr_rdata_i,
119:
120: `ifdef RVFI
121: output logic [4:0] rfvi_reg_raddr_ra_o,
122: output logic [31:0] rfvi_reg_rdata_ra_o,
123: output logic [4:0] rfvi_reg_raddr_rb_o,
124: output logic [31:0] rfvi_reg_rdata_rb_o,
125: output logic [4:0] rfvi_reg_waddr_rd_o,
126: output logic [31:0] rfvi_reg_wdata_rd_o,
127: output logic rfvi_reg_we_o,
128: `endif
129:
130: // Performance Counters
131: output logic perf_jump_o, // executing a jump instr
132: output logic perf_branch_o, // executing a branch instr
133: output logic perf_tbranch_o, // executing a taken branch instr
134: output logic instr_ret_o,
135: output logic instr_ret_compressed_o
136: );
137:
138: import ibex_pkg::*;
139:
140: // Decoder/Controller, ID stage internal signals
141: logic illegal_insn_dec;
142: logic ebrk_insn;
143: logic mret_insn_dec;
144: logic dret_insn_dec;
145: logic ecall_insn_dec;
146: logic wfi_insn_dec;
147:
148: logic branch_in_dec;
149: logic branch_set_n, branch_set_q;
150: logic jump_in_dec;
151: logic jump_set;
152:
153: logic instr_executing;
154: logic instr_multicycle;
155: logic instr_multicycle_done_n, instr_multicycle_done_q;
156: logic stall_lsu;
157: logic stall_multdiv;
158: logic stall_branch;
159: logic stall_jump;
160:
161: // Immediate decoding and sign extension
162: logic [31:0] imm_i_type;
163: logic [31:0] imm_s_type;
164: logic [31:0] imm_b_type;
165: logic [31:0] imm_u_type;
166: logic [31:0] imm_j_type;
167: logic [31:0] zimm_rs1_type;
168:
169: logic [31:0] imm_a; // contains the immediate for operand b
170: logic [31:0] imm_b; // contains the immediate for operand b
171:
172: // Register file interface
173: logic [4:0] regfile_raddr_a;
174: logic [4:0] regfile_raddr_b;
175:
176: logic [4:0] regfile_waddr;
177:
178: logic [31:0] regfile_rdata_a;
179: logic [31:0] regfile_rdata_b;
180: logic [31:0] regfile_wdata;
181:
182: rf_wd_sel_e regfile_wdata_sel;
183: logic regfile_we;
184: logic regfile_we_wb, regfile_we_dec;
185:
186: // ALU Control
187: alu_op_e alu_operator;
188: op_a_sel_e alu_op_a_mux_sel, alu_op_a_mux_sel_dec;
189: op_b_sel_e alu_op_b_mux_sel, alu_op_b_mux_sel_dec;
190:
191: imm_a_sel_e imm_a_mux_sel;
192: imm_b_sel_e imm_b_mux_sel, imm_b_mux_sel_dec;
193:
194: // Multiplier Control
195: logic mult_en_id, mult_en_dec; // use integer multiplier
196: logic div_en_id, div_en_dec; // use integer division or reminder
197: logic multdiv_en_dec;
198: md_op_e multdiv_operator;
199: logic [1:0] multdiv_signed_mode;
200:
201: // Data Memory Control
202: logic data_we_id;
203: logic [1:0] data_type_id;
204: logic data_sign_ext_id;
205: logic data_req_id, data_req_dec;
206:
207: // CSR control
208: logic csr_pipe_flush;
209:
210: logic [31:0] alu_operand_a;
211: logic [31:0] alu_operand_b;
212:
213: /////////////
214: // LSU Mux //
215: /////////////
216:
217: // Misaligned loads/stores result in two aligned loads/stores, compute second address
218: assign alu_op_a_mux_sel = lsu_addr_incr_req_i ? OP_A_FWD : alu_op_a_mux_sel_dec;
219: assign alu_op_b_mux_sel = lsu_addr_incr_req_i ? OP_B_IMM : alu_op_b_mux_sel_dec;
220: assign imm_b_mux_sel = lsu_addr_incr_req_i ? IMM_B_INCR_ADDR : imm_b_mux_sel_dec;
221:
222: ///////////////////
223: // Operand A MUX //
224: ///////////////////
225:
226: // Immediate MUX for Operand A
227: assign imm_a = (imm_a_mux_sel == IMM_A_Z) ? zimm_rs1_type : '0;
228:
229: // ALU MUX for Operand A
230: always_comb begin : alu_operand_a_mux
231: unique case (alu_op_a_mux_sel)
232: OP_A_REG_A: alu_operand_a = regfile_rdata_a;
233: OP_A_FWD: alu_operand_a = lsu_addr_last_i;
234: OP_A_CURRPC: alu_operand_a = pc_id_i;
235: OP_A_IMM: alu_operand_a = imm_a;
236: default: alu_operand_a = pc_id_i;
237: endcase
238: end
239:
240: ///////////////////
241: // Operand B MUX //
242: ///////////////////
243:
244: // Immediate MUX for Operand B
245: always_comb begin : immediate_b_mux
246: unique case (imm_b_mux_sel)
247: IMM_B_I: imm_b = imm_i_type;
248: IMM_B_S: imm_b = imm_s_type;
249: IMM_B_B: imm_b = imm_b_type;
250: IMM_B_U: imm_b = imm_u_type;
251: IMM_B_J: imm_b = imm_j_type;
252: IMM_B_INCR_PC: imm_b = instr_is_compressed_i ? 32'h2 : 32'h4;
253: IMM_B_INCR_ADDR: imm_b = 32'h4;
254: default: imm_b = 32'h4;
255: endcase
256: end
257:
258: // ALU MUX for Operand B
259: assign alu_operand_b = (alu_op_b_mux_sel == OP_B_IMM) ? imm_b : regfile_rdata_b;
260:
261: ///////////////////////
262: // Register File MUX //
263: ///////////////////////
264:
265: // Register file write enable mux - do not propagate illegal CSR ops, do not write when idle,
266: // for loads/stores and multdiv operations write when the data is ready only
267: assign regfile_we = (illegal_csr_insn_i || !instr_executing) ? 1'b0 :
268: (data_req_dec || multdiv_en_dec) ? regfile_we_wb : regfile_we_dec;
269:
270: // Register file write data mux
271: always_comb begin : regfile_wdata_mux
272: unique case (regfile_wdata_sel)
273: RF_WD_EX: regfile_wdata = regfile_wdata_ex_i;
274: RF_WD_LSU: regfile_wdata = regfile_wdata_lsu_i;
275: RF_WD_CSR: regfile_wdata = csr_rdata_i;
276: default: regfile_wdata = regfile_wdata_ex_i;
277: endcase
278: end
279:
280: ///////////////////
281: // Register File //
282: ///////////////////
283:
284: ibex_register_file #( .RV32E ( RV32E ) ) registers_i (
285: .clk_i ( clk_i ),
286: .rst_ni ( rst_ni ),
287:
288: .test_en_i ( test_en_i ),
289:
290: // Read port a
291: .raddr_a_i ( regfile_raddr_a ),
292: .rdata_a_o ( regfile_rdata_a ),
293: // Read port b
294: .raddr_b_i ( regfile_raddr_b ),
295: .rdata_b_o ( regfile_rdata_b ),
296: // write port
297: .waddr_a_i ( regfile_waddr ),
298: .wdata_a_i ( regfile_wdata ),
299: .we_a_i ( regfile_we )
300: );
301:
302: `ifdef RVFI
303: assign rfvi_reg_raddr_ra_o = regfile_raddr_a;
304: assign rfvi_reg_rdata_ra_o = regfile_rdata_a;
305: assign rfvi_reg_raddr_rb_o = regfile_raddr_b;
306: assign rfvi_reg_rdata_rb_o = regfile_rdata_b;
307: assign rfvi_reg_waddr_rd_o = regfile_waddr;
308: assign rfvi_reg_wdata_rd_o = regfile_wdata;
309: assign rfvi_reg_we_o = regfile_we;
310: `endif
311:
312: /////////////
313: // Decoder //
314: /////////////
315:
316: ibex_decoder #(
317: .RV32E ( RV32E ),
318: .RV32M ( RV32M )
319: ) decoder_i (
320: .clk_i ( clk_i ),
321: .rst_ni ( rst_ni ),
322:
323: // controller
324: .illegal_insn_o ( illegal_insn_dec ),
325: .ebrk_insn_o ( ebrk_insn ),
326: .mret_insn_o ( mret_insn_dec ),
327: .dret_insn_o ( dret_insn_dec ),
328: .ecall_insn_o ( ecall_insn_dec ),
329: .wfi_insn_o ( wfi_insn_dec ),
330: .jump_set_o ( jump_set ),
331:
332: // from IF-ID pipeline register
333: .instr_new_i ( instr_new_i ),
334: .instr_rdata_i ( instr_rdata_i ),
335: .illegal_c_insn_i ( illegal_c_insn_i ),
336:
337: // immediates
338: .imm_a_mux_sel_o ( imm_a_mux_sel ),
339: .imm_b_mux_sel_o ( imm_b_mux_sel_dec ),
340:
341: .imm_i_type_o ( imm_i_type ),
342: .imm_s_type_o ( imm_s_type ),
343: .imm_b_type_o ( imm_b_type ),
344: .imm_u_type_o ( imm_u_type ),
345: .imm_j_type_o ( imm_j_type ),
346: .zimm_rs1_type_o ( zimm_rs1_type ),
347:
348: // register file
349: .regfile_wdata_sel_o ( regfile_wdata_sel ),
350: .regfile_we_o ( regfile_we_dec ),
351:
352: .regfile_raddr_a_o ( regfile_raddr_a ),
353: .regfile_raddr_b_o ( regfile_raddr_b ),
354: .regfile_waddr_o ( regfile_waddr ),
355:
356: // ALU
357: .alu_operator_o ( alu_operator ),
358: .alu_op_a_mux_sel_o ( alu_op_a_mux_sel_dec ),
359: .alu_op_b_mux_sel_o ( alu_op_b_mux_sel_dec ),
360:
361: // MULT & DIV
362: .mult_en_o ( mult_en_dec ),
363: .div_en_o ( div_en_dec ),
364: .multdiv_operator_o ( multdiv_operator ),
365: .multdiv_signed_mode_o ( multdiv_signed_mode ),
366:
367: // CSRs
368: .csr_access_o ( csr_access_o ),
369: .csr_op_o ( csr_op_o ),
370: .csr_pipe_flush_o ( csr_pipe_flush ),
371:
372: // LSU
373: .data_req_o ( data_req_dec ),
374: .data_we_o ( data_we_id ),
375: .data_type_o ( data_type_id ),
376: .data_sign_extension_o ( data_sign_ext_id ),
377:
378: // jump/branches
379: .jump_in_dec_o ( jump_in_dec ),
380: .branch_in_dec_o ( branch_in_dec )
381: );
382:
383: ////////////////
384: // Controller //
385: ////////////////
386:
387: assign illegal_insn_o = instr_valid_i & (illegal_insn_dec | illegal_csr_insn_i);
388:
389: ibex_controller controller_i (
390: .clk_i ( clk_i ),
391: .rst_ni ( rst_ni ),
392:
393: .fetch_enable_i ( fetch_enable_i ),
394: .ctrl_busy_o ( ctrl_busy_o ),
395:
396: // decoder related signals
397: .illegal_insn_i ( illegal_insn_o ),
398: .ecall_insn_i ( ecall_insn_dec ),
399: .mret_insn_i ( mret_insn_dec ),
400: .dret_insn_i ( dret_insn_dec ),
401: .wfi_insn_i ( wfi_insn_dec ),
402: .ebrk_insn_i ( ebrk_insn ),
403: .csr_pipe_flush_i ( csr_pipe_flush ),
404:
405: // from IF-ID pipeline
406: .instr_valid_i ( instr_valid_i ),
407: .instr_i ( instr_rdata_i ),
408: .instr_compressed_i ( instr_rdata_c_i ),
409: .instr_is_compressed_i ( instr_is_compressed_i ),
410: .instr_fetch_err_i ( instr_fetch_err_i ),
411: .pc_id_i ( pc_id_i ),
412:
413: // to IF-ID pipeline
414: .instr_valid_clear_o ( instr_valid_clear_o ),
415: .id_in_ready_o ( id_in_ready_o ),
416:
417: // to prefetcher
418: .instr_req_o ( instr_req_o ),
419: .pc_set_o ( pc_set_o ),
420: .pc_mux_o ( pc_mux_o ),
421: .exc_pc_mux_o ( exc_pc_mux_o ),
422: .exc_cause_o ( exc_cause_o ),
423:
424: // LSU
425: .lsu_addr_last_i ( lsu_addr_last_i ),
426: .load_err_i ( lsu_load_err_i ),
427: .store_err_i ( lsu_store_err_i ),
428:
429: // jump/branch control
430: .branch_set_i ( branch_set_q ),
431: .jump_set_i ( jump_set ),
432:
433: // interrupt signals
434: .csr_mstatus_mie_i ( csr_mstatus_mie_i ),
435: .csr_msip_i ( csr_msip_i ),
436: .csr_mtip_i ( csr_mtip_i ),
437: .csr_meip_i ( csr_meip_i ),
438: .csr_mfip_i ( csr_mfip_i ),
439: .irq_pending_i ( irq_pending_i ),
440: .irq_nm_i ( irq_nm_i ),
441: .nmi_mode_o ( nmi_mode_o ),
442:
443: // CSR Controller Signals
444: .csr_save_if_o ( csr_save_if_o ),
445: .csr_save_id_o ( csr_save_id_o ),
446: .csr_restore_mret_id_o ( csr_restore_mret_id_o ),
447: .csr_restore_dret_id_o ( csr_restore_dret_id_o ),
448: .csr_save_cause_o ( csr_save_cause_o ),
449: .csr_mtval_o ( csr_mtval_o ),
450: .priv_mode_i ( priv_mode_i ),
451: .csr_mstatus_tw_i ( csr_mstatus_tw_i ),
452:
453: // Debug Signal
454: .debug_mode_o ( debug_mode_o ),
455: .debug_cause_o ( debug_cause_o ),
456: .debug_csr_save_o ( debug_csr_save_o ),
457: .debug_req_i ( debug_req_i ),
458: .debug_single_step_i ( debug_single_step_i ),
459: .debug_ebreakm_i ( debug_ebreakm_i ),
460: .debug_ebreaku_i ( debug_ebreaku_i ),
461: .trigger_match_i ( trigger_match_i ),
462:
463: // stall signals
464: .stall_lsu_i ( stall_lsu ),
465: .stall_multdiv_i ( stall_multdiv ),
466: .stall_jump_i ( stall_jump ),
467: .stall_branch_i ( stall_branch ),
468:
469: // Performance Counters
470: .perf_jump_o ( perf_jump_o ),
471: .perf_tbranch_o ( perf_tbranch_o )
472: );
473:
474: //////////////
475: // ID-EX/WB //
476: //////////////
477:
478: assign multdiv_en_dec = mult_en_dec | div_en_dec;
479: assign instr_multicycle = data_req_dec | multdiv_en_dec | branch_in_dec | jump_in_dec;
480:
481: // Forward decoder output to EX, WB and controller only if current instr is still
482: // being executed. This is the case if the current instr is either:
483: // - a new instr (not yet done)
484: // - a multicycle instr that is not yet done
485: // An instruction error will suppress any requests or register writes
486: assign instr_executing = (instr_new_i | (instr_multicycle & ~instr_multicycle_done_q)) &
487: ~instr_fetch_err_i;
488: assign data_req_id = instr_executing ? data_req_dec : 1'b0;
489: assign mult_en_id = instr_executing ? mult_en_dec : 1'b0;
490: assign div_en_id = instr_executing ? div_en_dec : 1'b0;
491:
492: ///////////
493: // ID-EX //
494: ///////////
495:
496: assign data_req_ex_o = data_req_id;
497: assign data_we_ex_o = data_we_id;
498: assign data_type_ex_o = data_type_id;
499: assign data_sign_ext_ex_o = data_sign_ext_id;
500: assign data_wdata_ex_o = regfile_rdata_b;
501:
502: assign alu_operator_ex_o = alu_operator;
503: assign alu_operand_a_ex_o = alu_operand_a;
504: assign alu_operand_b_ex_o = alu_operand_b;
505:
506: assign mult_en_ex_o = mult_en_id;
507: assign div_en_ex_o = div_en_id;
508:
509: assign multdiv_operator_ex_o = multdiv_operator;
510: assign multdiv_signed_mode_ex_o = multdiv_signed_mode;
511: assign multdiv_operand_a_ex_o = regfile_rdata_a;
512: assign multdiv_operand_b_ex_o = regfile_rdata_b;
513:
514: typedef enum logic { IDLE, WAIT_MULTICYCLE } id_fsm_e;
515: id_fsm_e id_wb_fsm_cs, id_wb_fsm_ns;
516:
517: ////////////////////////////////
518: // ID-EX/WB Pipeline Register //
519: ////////////////////////////////
520:
521: always_ff @(posedge clk_i or negedge rst_ni) begin : id_wb_pipeline_reg
522: if (!rst_ni) begin
523: id_wb_fsm_cs <= IDLE;
524: branch_set_q <= 1'b0;
525: instr_multicycle_done_q <= 1'b0;
526: end else begin
527: id_wb_fsm_cs <= id_wb_fsm_ns;
528: branch_set_q <= branch_set_n;
529: instr_multicycle_done_q <= instr_multicycle_done_n;
530: end
531: end
532:
533: //////////////////
534: // ID-EX/WB FSM //
535: //////////////////
536:
537: always_comb begin : id_wb_fsm
538: id_wb_fsm_ns = id_wb_fsm_cs;
539: instr_multicycle_done_n = instr_multicycle_done_q;
540: regfile_we_wb = 1'b0;
541: stall_lsu = 1'b0;
542: stall_multdiv = 1'b0;
543: stall_jump = 1'b0;
544: stall_branch = 1'b0;
545: branch_set_n = 1'b0;
546: perf_branch_o = 1'b0;
547: instr_ret_o = 1'b0;
548:
549: unique case (id_wb_fsm_cs)
550:
551: IDLE: begin
552: // only detect multicycle when instruction is new, do not re-detect after
553: // execution (when waiting for next instruction from IF stage)
554: if (instr_new_i & ~instr_fetch_err_i) begin
555: unique case (1'b1)
556: data_req_dec: begin
557: // LSU operation
558: id_wb_fsm_ns = WAIT_MULTICYCLE;
559: stall_lsu = 1'b1;
560: instr_multicycle_done_n = 1'b0;
561: end
562: multdiv_en_dec: begin
563: // MUL or DIV operation
564: id_wb_fsm_ns = WAIT_MULTICYCLE;
565: stall_multdiv = 1'b1;
566: instr_multicycle_done_n = 1'b0;
567: end
568: branch_in_dec: begin
569: // cond branch operation
570: id_wb_fsm_ns = branch_decision_i ? WAIT_MULTICYCLE : IDLE;
571: stall_branch = branch_decision_i;
572: instr_multicycle_done_n = ~branch_decision_i;
573: branch_set_n = branch_decision_i;
574: perf_branch_o = 1'b1;
575: instr_ret_o = ~branch_decision_i;
576: end
577: jump_in_dec: begin
578: // uncond branch operation
579: id_wb_fsm_ns = WAIT_MULTICYCLE;
580: stall_jump = 1'b1;
581: instr_multicycle_done_n = 1'b0;
582: end
583: default: begin
584: instr_multicycle_done_n = 1'b0;
585: instr_ret_o = 1'b1;
586: end
587: endcase
588: end
589: end
590:
591: WAIT_MULTICYCLE: begin
592: if ((data_req_dec & lsu_valid_i) | (~data_req_dec & ex_valid_i)) begin
593: id_wb_fsm_ns = IDLE;
594: instr_multicycle_done_n = 1'b1;
595: regfile_we_wb = regfile_we_dec & ~lsu_load_err_i;
596: instr_ret_o = 1'b1;
597: end else begin
598: stall_lsu = data_req_dec;
599: stall_multdiv = multdiv_en_dec;
600: stall_branch = branch_in_dec;
601: stall_jump = jump_in_dec;
602: end
603: end
604:
605: default: begin
606: id_wb_fsm_ns = IDLE;
607: end
608: endcase
609: end
610:
611: assign instr_ret_compressed_o = instr_ret_o & instr_is_compressed_i;
612:
613: ////////////////
614: // Assertions //
615: ////////////////
616:
617: // Selectors must be known/valid.
618: `ASSERT_KNOWN(IbexAluOpMuxSelKnown, alu_op_a_mux_sel, clk_i, !rst_ni)
619: `ASSERT(IbexImmBMuxSelValid, imm_b_mux_sel inside {
620: IMM_B_I,
621: IMM_B_S,
622: IMM_B_B,
623: IMM_B_U,
624: IMM_B_J,
625: IMM_B_INCR_PC,
626: IMM_B_INCR_ADDR
627: }, clk_i, !rst_ni)
628: `ASSERT(IbexRegfileWdataSelValid, regfile_wdata_sel inside {
629: RF_WD_LSU,
630: RF_WD_EX,
631: RF_WD_CSR
632: }, clk_i, !rst_ni)
633: `ASSERT_KNOWN(IbexWbStateKnown, id_wb_fsm_cs, clk_i, !rst_ni)
634:
635: // Branch decision must be valid when jumping.
636: `ASSERT(IbexBranchDecisionValid, branch_in_dec |-> !$isunknown(branch_decision_i), clk_i, !rst_ni)
637:
638: // Instruction delivered to ID stage can not contain X.
639: `ASSERT(IbexIdInstrKnown,
640: (instr_valid_i && !(illegal_c_insn_i || instr_fetch_err_i)) |-> !$isunknown(instr_rdata_i),
641: clk_i, !rst_ni)
642:
643: // Multicycle enable signals must be unique.
644: `ASSERT(IbexMulticycleEnableUnique,
645: $onehot0({data_req_dec, multdiv_en_dec, branch_in_dec, jump_in_dec}), clk_i, !rst_ni)
646:
647: `ifdef CHECK_MISALIGNED
648: `ASSERT(IbexMisalignedMemoryAccess, !lsu_addr_incr_req_i, clk_i, !rst_ni)
649: `endif
650:
651: endmodule
652: