194 lines
10 KiB
Coq
194 lines
10 KiB
Coq
|
module lsu_addrcheck(
|
||
|
|
input clock,
|
||
|
|
input reset,
|
||
|
|
input io_lsu_c2_m_clk,
|
||
|
|
input [31:0] io_start_addr_d,
|
||
|
|
input [31:0] io_end_addr_d,
|
||
|
|
input io_lsu_pkt_d_valid,
|
||
|
|
input io_lsu_pkt_d_bits_fast_int,
|
||
|
|
input io_lsu_pkt_d_bits_by,
|
||
|
|
input io_lsu_pkt_d_bits_half,
|
||
|
|
input io_lsu_pkt_d_bits_word,
|
||
|
|
input io_lsu_pkt_d_bits_dword,
|
||
|
|
input io_lsu_pkt_d_bits_load,
|
||
|
|
input io_lsu_pkt_d_bits_store,
|
||
|
|
input io_lsu_pkt_d_bits_unsign,
|
||
|
|
input io_lsu_pkt_d_bits_dma,
|
||
|
|
input io_lsu_pkt_d_bits_store_data_bypass_d,
|
||
|
|
input io_lsu_pkt_d_bits_load_ldst_bypass_d,
|
||
|
|
input io_lsu_pkt_d_bits_store_data_bypass_m,
|
||
|
|
input [31:0] io_dec_tlu_mrac_ff,
|
||
|
|
input [3:0] io_rs1_region_d,
|
||
|
|
input [31:0] io_rs1_d,
|
||
|
|
output io_is_sideeffects_m,
|
||
|
|
output io_addr_in_dccm_d,
|
||
|
|
output io_addr_in_pic_d,
|
||
|
|
output io_addr_external_d,
|
||
|
|
output io_access_fault_d,
|
||
|
|
output io_misaligned_fault_d,
|
||
|
|
output [3:0] io_exc_mscause_d,
|
||
|
|
output io_fir_dccm_access_error_d,
|
||
|
|
output io_fir_nondccm_access_error_d,
|
||
|
|
input io_scan_mode
|
||
|
|
);
|
||
|
|
`ifdef RANDOMIZE_REG_INIT
|
||
|
|
reg [31:0] _RAND_0;
|
||
|
|
`endif // RANDOMIZE_REG_INIT
|
||
|
|
wire start_addr_in_dccm_region_d = io_start_addr_d[31:28] == 4'hf; // @[lib.scala 356:49]
|
||
|
|
wire start_addr_in_dccm_d = io_start_addr_d[31:16] == 16'hf004; // @[lib.scala 361:39]
|
||
|
|
wire end_addr_in_dccm_region_d = io_end_addr_d[31:28] == 4'hf; // @[lib.scala 356:49]
|
||
|
|
wire end_addr_in_dccm_d = io_end_addr_d[31:16] == 16'hf004; // @[lib.scala 361:39]
|
||
|
|
wire addr_in_iccm = io_start_addr_d[31:28] == 4'he; // @[lsu_addrcheck.scala 42:45]
|
||
|
|
wire start_addr_in_pic_d = io_start_addr_d[31:15] == 17'h1e018; // @[lib.scala 361:39]
|
||
|
|
wire end_addr_in_pic_d = io_end_addr_d[31:15] == 17'h1e018; // @[lib.scala 361:39]
|
||
|
|
wire start_addr_dccm_or_pic = start_addr_in_dccm_region_d | start_addr_in_dccm_region_d; // @[lsu_addrcheck.scala 54:60]
|
||
|
|
wire _T_17 = io_rs1_region_d == 4'hf; // @[lsu_addrcheck.scala 55:55]
|
||
|
|
wire base_reg_dccm_or_pic = _T_17 | _T_17; // @[lsu_addrcheck.scala 55:91]
|
||
|
|
wire [4:0] csr_idx = {io_start_addr_d[31:28],1'h1}; // @[Cat.scala 29:58]
|
||
|
|
wire [31:0] _T_26 = io_dec_tlu_mrac_ff >> csr_idx; // @[lsu_addrcheck.scala 61:50]
|
||
|
|
wire _T_29 = start_addr_dccm_or_pic | addr_in_iccm; // @[lsu_addrcheck.scala 61:121]
|
||
|
|
wire _T_30 = ~_T_29; // @[lsu_addrcheck.scala 61:62]
|
||
|
|
wire _T_31 = _T_26[0] & _T_30; // @[lsu_addrcheck.scala 61:60]
|
||
|
|
wire _T_32 = _T_31 & io_lsu_pkt_d_valid; // @[lsu_addrcheck.scala 61:137]
|
||
|
|
wire _T_33 = io_lsu_pkt_d_bits_store | io_lsu_pkt_d_bits_load; // @[lsu_addrcheck.scala 61:185]
|
||
|
|
wire is_sideeffects_d = _T_32 & _T_33; // @[lsu_addrcheck.scala 61:158]
|
||
|
|
wire _T_35 = io_start_addr_d[1:0] == 2'h0; // @[lsu_addrcheck.scala 62:80]
|
||
|
|
wire _T_36 = io_lsu_pkt_d_bits_word & _T_35; // @[lsu_addrcheck.scala 62:56]
|
||
|
|
wire _T_38 = ~io_start_addr_d[0]; // @[lsu_addrcheck.scala 62:138]
|
||
|
|
wire _T_39 = io_lsu_pkt_d_bits_half & _T_38; // @[lsu_addrcheck.scala 62:116]
|
||
|
|
wire _T_40 = _T_36 | _T_39; // @[lsu_addrcheck.scala 62:90]
|
||
|
|
wire is_aligned_d = _T_40 | io_lsu_pkt_d_bits_by; // @[lsu_addrcheck.scala 62:148]
|
||
|
|
wire [31:0] _T_51 = io_start_addr_d | 32'h7fffffff; // @[lsu_addrcheck.scala 67:56]
|
||
|
|
wire _T_53 = _T_51 == 32'h7fffffff; // @[lsu_addrcheck.scala 67:88]
|
||
|
|
wire [31:0] _T_56 = io_start_addr_d | 32'h3fffffff; // @[lsu_addrcheck.scala 68:56]
|
||
|
|
wire _T_58 = _T_56 == 32'hffffffff; // @[lsu_addrcheck.scala 68:88]
|
||
|
|
wire _T_60 = _T_53 | _T_58; // @[lsu_addrcheck.scala 67:153]
|
||
|
|
wire [31:0] _T_62 = io_start_addr_d | 32'h1fffffff; // @[lsu_addrcheck.scala 69:56]
|
||
|
|
wire _T_64 = _T_62 == 32'hbfffffff; // @[lsu_addrcheck.scala 69:88]
|
||
|
|
wire _T_66 = _T_60 | _T_64; // @[lsu_addrcheck.scala 68:153]
|
||
|
|
wire [31:0] _T_68 = io_start_addr_d | 32'hfffffff; // @[lsu_addrcheck.scala 70:56]
|
||
|
|
wire _T_70 = _T_68 == 32'h8fffffff; // @[lsu_addrcheck.scala 70:88]
|
||
|
|
wire _T_72 = _T_66 | _T_70; // @[lsu_addrcheck.scala 69:153]
|
||
|
|
wire [31:0] _T_98 = io_end_addr_d | 32'h7fffffff; // @[lsu_addrcheck.scala 76:57]
|
||
|
|
wire _T_100 = _T_98 == 32'h7fffffff; // @[lsu_addrcheck.scala 76:89]
|
||
|
|
wire [31:0] _T_103 = io_end_addr_d | 32'h3fffffff; // @[lsu_addrcheck.scala 77:58]
|
||
|
|
wire _T_105 = _T_103 == 32'hffffffff; // @[lsu_addrcheck.scala 77:90]
|
||
|
|
wire _T_107 = _T_100 | _T_105; // @[lsu_addrcheck.scala 76:154]
|
||
|
|
wire [31:0] _T_109 = io_end_addr_d | 32'h1fffffff; // @[lsu_addrcheck.scala 78:58]
|
||
|
|
wire _T_111 = _T_109 == 32'hbfffffff; // @[lsu_addrcheck.scala 78:90]
|
||
|
|
wire _T_113 = _T_107 | _T_111; // @[lsu_addrcheck.scala 77:155]
|
||
|
|
wire [31:0] _T_115 = io_end_addr_d | 32'hfffffff; // @[lsu_addrcheck.scala 79:58]
|
||
|
|
wire _T_117 = _T_115 == 32'h8fffffff; // @[lsu_addrcheck.scala 79:90]
|
||
|
|
wire _T_119 = _T_113 | _T_117; // @[lsu_addrcheck.scala 78:155]
|
||
|
|
wire non_dccm_access_ok = _T_72 & _T_119; // @[lsu_addrcheck.scala 75:7]
|
||
|
|
wire regpred_access_fault_d = start_addr_dccm_or_pic ^ base_reg_dccm_or_pic; // @[lsu_addrcheck.scala 85:57]
|
||
|
|
wire _T_146 = io_start_addr_d[1:0] != 2'h0; // @[lsu_addrcheck.scala 86:76]
|
||
|
|
wire _T_147 = ~io_lsu_pkt_d_bits_word; // @[lsu_addrcheck.scala 86:92]
|
||
|
|
wire _T_148 = _T_146 | _T_147; // @[lsu_addrcheck.scala 86:90]
|
||
|
|
wire picm_access_fault_d = io_addr_in_pic_d & _T_148; // @[lsu_addrcheck.scala 86:51]
|
||
|
|
wire _T_149 = start_addr_in_dccm_d | start_addr_in_pic_d; // @[lsu_addrcheck.scala 91:87]
|
||
|
|
wire _T_150 = ~_T_149; // @[lsu_addrcheck.scala 91:64]
|
||
|
|
wire _T_151 = start_addr_in_dccm_region_d & _T_150; // @[lsu_addrcheck.scala 91:62]
|
||
|
|
wire _T_152 = end_addr_in_dccm_d | end_addr_in_pic_d; // @[lsu_addrcheck.scala 93:57]
|
||
|
|
wire _T_153 = ~_T_152; // @[lsu_addrcheck.scala 93:36]
|
||
|
|
wire _T_154 = end_addr_in_dccm_region_d & _T_153; // @[lsu_addrcheck.scala 93:34]
|
||
|
|
wire _T_155 = _T_151 | _T_154; // @[lsu_addrcheck.scala 91:112]
|
||
|
|
wire _T_156 = start_addr_in_dccm_d & end_addr_in_pic_d; // @[lsu_addrcheck.scala 95:29]
|
||
|
|
wire _T_157 = _T_155 | _T_156; // @[lsu_addrcheck.scala 93:85]
|
||
|
|
wire _T_158 = start_addr_in_pic_d & end_addr_in_dccm_d; // @[lsu_addrcheck.scala 97:29]
|
||
|
|
wire unmapped_access_fault_d = _T_157 | _T_158; // @[lsu_addrcheck.scala 95:85]
|
||
|
|
wire _T_160 = ~start_addr_in_dccm_region_d; // @[lsu_addrcheck.scala 99:33]
|
||
|
|
wire _T_161 = ~non_dccm_access_ok; // @[lsu_addrcheck.scala 99:64]
|
||
|
|
wire mpu_access_fault_d = _T_160 & _T_161; // @[lsu_addrcheck.scala 99:62]
|
||
|
|
wire _T_163 = unmapped_access_fault_d | mpu_access_fault_d; // @[lsu_addrcheck.scala 111:49]
|
||
|
|
wire _T_164 = _T_163 | picm_access_fault_d; // @[lsu_addrcheck.scala 111:70]
|
||
|
|
wire _T_165 = _T_164 | regpred_access_fault_d; // @[lsu_addrcheck.scala 111:92]
|
||
|
|
wire _T_166 = _T_165 & io_lsu_pkt_d_valid; // @[lsu_addrcheck.scala 111:118]
|
||
|
|
wire _T_167 = ~io_lsu_pkt_d_bits_dma; // @[lsu_addrcheck.scala 111:141]
|
||
|
|
wire [3:0] _T_173 = picm_access_fault_d ? 4'h6 : 4'h0; // @[lsu_addrcheck.scala 112:164]
|
||
|
|
wire [3:0] _T_174 = regpred_access_fault_d ? 4'h5 : _T_173; // @[lsu_addrcheck.scala 112:120]
|
||
|
|
wire [3:0] _T_175 = mpu_access_fault_d ? 4'h3 : _T_174; // @[lsu_addrcheck.scala 112:80]
|
||
|
|
wire [3:0] access_fault_mscause_d = unmapped_access_fault_d ? 4'h2 : _T_175; // @[lsu_addrcheck.scala 112:35]
|
||
|
|
wire regcross_misaligned_fault_d = io_start_addr_d[31:28] != io_end_addr_d[31:28]; // @[lsu_addrcheck.scala 113:61]
|
||
|
|
wire _T_178 = ~is_aligned_d; // @[lsu_addrcheck.scala 114:59]
|
||
|
|
wire sideeffect_misaligned_fault_d = is_sideeffects_d & _T_178; // @[lsu_addrcheck.scala 114:57]
|
||
|
|
wire _T_179 = sideeffect_misaligned_fault_d & io_addr_external_d; // @[lsu_addrcheck.scala 115:90]
|
||
|
|
wire _T_180 = regcross_misaligned_fault_d | _T_179; // @[lsu_addrcheck.scala 115:57]
|
||
|
|
wire _T_181 = _T_180 & io_lsu_pkt_d_valid; // @[lsu_addrcheck.scala 115:113]
|
||
|
|
wire [3:0] _T_185 = sideeffect_misaligned_fault_d ? 4'h1 : 4'h0; // @[lsu_addrcheck.scala 116:80]
|
||
|
|
wire [3:0] misaligned_fault_mscause_d = regcross_misaligned_fault_d ? 4'h2 : _T_185; // @[lsu_addrcheck.scala 116:39]
|
||
|
|
wire _T_190 = ~start_addr_in_dccm_d; // @[lsu_addrcheck.scala 118:66]
|
||
|
|
wire _T_191 = start_addr_in_dccm_region_d & _T_190; // @[lsu_addrcheck.scala 118:64]
|
||
|
|
wire _T_192 = ~end_addr_in_dccm_d; // @[lsu_addrcheck.scala 118:120]
|
||
|
|
wire _T_193 = end_addr_in_dccm_region_d & _T_192; // @[lsu_addrcheck.scala 118:118]
|
||
|
|
wire _T_194 = _T_191 | _T_193; // @[lsu_addrcheck.scala 118:88]
|
||
|
|
wire _T_195 = _T_194 & io_lsu_pkt_d_valid; // @[lsu_addrcheck.scala 118:142]
|
||
|
|
wire _T_197 = start_addr_in_dccm_region_d & end_addr_in_dccm_region_d; // @[lsu_addrcheck.scala 119:66]
|
||
|
|
wire _T_198 = ~_T_197; // @[lsu_addrcheck.scala 119:36]
|
||
|
|
wire _T_199 = _T_198 & io_lsu_pkt_d_valid; // @[lsu_addrcheck.scala 119:95]
|
||
|
|
reg _T_201; // @[lsu_addrcheck.scala 121:60]
|
||
|
|
assign io_is_sideeffects_m = _T_201; // @[lsu_addrcheck.scala 121:50]
|
||
|
|
assign io_addr_in_dccm_d = start_addr_in_dccm_d & end_addr_in_dccm_d; // @[lsu_addrcheck.scala 56:32]
|
||
|
|
assign io_addr_in_pic_d = start_addr_in_pic_d & end_addr_in_pic_d; // @[lsu_addrcheck.scala 57:32]
|
||
|
|
assign io_addr_external_d = ~start_addr_dccm_or_pic; // @[lsu_addrcheck.scala 59:30]
|
||
|
|
assign io_access_fault_d = _T_166 & _T_167; // @[lsu_addrcheck.scala 111:21]
|
||
|
|
assign io_misaligned_fault_d = _T_181 & _T_167; // @[lsu_addrcheck.scala 115:25]
|
||
|
|
assign io_exc_mscause_d = io_misaligned_fault_d ? misaligned_fault_mscause_d : access_fault_mscause_d; // @[lsu_addrcheck.scala 117:21]
|
||
|
|
assign io_fir_dccm_access_error_d = _T_195 & io_lsu_pkt_d_bits_fast_int; // @[lsu_addrcheck.scala 118:31]
|
||
|
|
assign io_fir_nondccm_access_error_d = _T_199 & io_lsu_pkt_d_bits_fast_int; // @[lsu_addrcheck.scala 119:33]
|
||
|
|
`ifdef RANDOMIZE_GARBAGE_ASSIGN
|
||
|
|
`define RANDOMIZE
|
||
|
|
`endif
|
||
|
|
`ifdef RANDOMIZE_INVALID_ASSIGN
|
||
|
|
`define RANDOMIZE
|
||
|
|
`endif
|
||
|
|
`ifdef RANDOMIZE_REG_INIT
|
||
|
|
`define RANDOMIZE
|
||
|
|
`endif
|
||
|
|
`ifdef RANDOMIZE_MEM_INIT
|
||
|
|
`define RANDOMIZE
|
||
|
|
`endif
|
||
|
|
`ifndef RANDOM
|
||
|
|
`define RANDOM $random
|
||
|
|
`endif
|
||
|
|
`ifdef RANDOMIZE_MEM_INIT
|
||
|
|
integer initvar;
|
||
|
|
`endif
|
||
|
|
`ifndef SYNTHESIS
|
||
|
|
`ifdef FIRRTL_BEFORE_INITIAL
|
||
|
|
`FIRRTL_BEFORE_INITIAL
|
||
|
|
`endif
|
||
|
|
initial begin
|
||
|
|
`ifdef RANDOMIZE
|
||
|
|
`ifdef INIT_RANDOM
|
||
|
|
`INIT_RANDOM
|
||
|
|
`endif
|
||
|
|
`ifndef VERILATOR
|
||
|
|
`ifdef RANDOMIZE_DELAY
|
||
|
|
#`RANDOMIZE_DELAY begin end
|
||
|
|
`else
|
||
|
|
#0.002 begin end
|
||
|
|
`endif
|
||
|
|
`endif
|
||
|
|
`ifdef RANDOMIZE_REG_INIT
|
||
|
|
_RAND_0 = {1{`RANDOM}};
|
||
|
|
_T_201 = _RAND_0[0:0];
|
||
|
|
`endif // RANDOMIZE_REG_INIT
|
||
|
|
if (reset) begin
|
||
|
|
_T_201 = 1'h0;
|
||
|
|
end
|
||
|
|
`endif // RANDOMIZE
|
||
|
|
end // initial
|
||
|
|
`ifdef FIRRTL_AFTER_INITIAL
|
||
|
|
`FIRRTL_AFTER_INITIAL
|
||
|
|
`endif
|
||
|
|
`endif // SYNTHESIS
|
||
|
|
always @(posedge io_lsu_c2_m_clk or posedge reset) begin
|
||
|
|
if (reset) begin
|
||
|
|
_T_201 <= 1'h0;
|
||
|
|
end else begin
|
||
|
|
_T_201 <= _T_32 & _T_33;
|
||
|
|
end
|
||
|
|
end
|
||
|
|
endmodule
|