Fixed a Tandem-Verification bug (reporting incorrect MIP/MIE/SIP/SIE post-write values)
MIP/MIE/SIP/SIE fields are WARL (Write-Any/Read-Legal). The CSR register forces the user-privilege bits ([8,4,0]) to 0 since riscy-ooo does not support user-level interrupts. However, function Csrfile.fv_warl_xform() was not mirroring this correctly.
This commit is contained in:
File diff suppressed because it is too large
Load Diff
@@ -474,6 +474,11 @@ module mkCsrFile #(Data hartid)(CsrFile);
|
||||
software_int_pend_vec[prvM], readOnlyReg(1'b0),
|
||||
software_int_pend_vec[prvS], readOnlyReg(1'b0) // only if misa.N: software_int_pend_vec[prvU]
|
||||
);
|
||||
// MIP and MIE fields are WARL (Write Any Read Legal)
|
||||
// We support M-privilege and S-privilege bits only;
|
||||
// this mask allows only those bits through.
|
||||
Data mip_mie_warl_mask = zeroExtend (12'h_aaa);
|
||||
|
||||
// minstret
|
||||
Ehr#(2, Data) minstret_ehr <- mkCsrEhr(0);
|
||||
Reg#(Data) minstret_csr = minstret_ehr[0];
|
||||
@@ -810,8 +815,8 @@ module mkCsrFile #(Data hartid)(CsrFile);
|
||||
CSRmtvec: { x[63:2], 1'b0, x[0]};
|
||||
CSRmedeleg: { 48'b0, x[15], 1'b0, x[13:12], x[11], 1'b0, x[9:0]};
|
||||
CSRmideleg: { 52'b0, x[11], 1'b0, x[9:8], x[7], 1'b0, x[5:4], x[3], 1'b0, x[1:0]};
|
||||
CSRmip: { 52'b0, x[11], 1'b0, x[9:8], x[7], 1'b0, x[5:4], x[3], 1'b0, x[1:0]};
|
||||
CSRmie: { 52'b0, x[11], 1'b0, x[9:8], x[7], 1'b0, x[5:4], x[3], 1'b0, x[1:0]};
|
||||
CSRmip: (x & mip_mie_warl_mask);
|
||||
CSRmie: (x & mip_mie_warl_mask);
|
||||
CSRmcounteren: { 61'b0, x[2:0]};
|
||||
CSRmcause: { x[63], 59'b0, x[3:0] };
|
||||
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@@ -2716,22 +2716,22 @@ module mkCoreW(RST_N_dm_power_on_reset,
|
||||
// rule RL_rl_dm_hart0_reset_wait
|
||||
assign CAN_FIRE_RL_rl_dm_hart0_reset_wait =
|
||||
(rg_hart0_reset_delay != 8'd1 ||
|
||||
debug_module$RDY_hart0_reset_client_response_put &&
|
||||
proc$RDY_start) &&
|
||||
proc$RDY_start &&
|
||||
debug_module$RDY_hart0_reset_client_response_put) &&
|
||||
rg_hart0_reset_delay != 8'd0 ;
|
||||
assign WILL_FIRE_RL_rl_dm_hart0_reset_wait =
|
||||
CAN_FIRE_RL_rl_dm_hart0_reset_wait && !EN_start ;
|
||||
|
||||
// rule RL_ClientServerRequest
|
||||
assign CAN_FIRE_RL_ClientServerRequest =
|
||||
debug_module$RDY_hart0_client_run_halt_request_get &&
|
||||
proc$RDY_hart0_run_halt_server_request_put ;
|
||||
proc$RDY_hart0_run_halt_server_request_put &&
|
||||
debug_module$RDY_hart0_client_run_halt_request_get ;
|
||||
assign WILL_FIRE_RL_ClientServerRequest = CAN_FIRE_RL_ClientServerRequest ;
|
||||
|
||||
// rule RL_ClientServerResponse
|
||||
assign CAN_FIRE_RL_ClientServerResponse =
|
||||
debug_module$RDY_hart0_client_run_halt_response_put &&
|
||||
proc$RDY_hart0_run_halt_server_response_get ;
|
||||
proc$RDY_hart0_run_halt_server_response_get &&
|
||||
debug_module$RDY_hart0_client_run_halt_response_put ;
|
||||
assign WILL_FIRE_RL_ClientServerResponse =
|
||||
CAN_FIRE_RL_ClientServerResponse ;
|
||||
|
||||
@@ -2743,25 +2743,25 @@ module mkCoreW(RST_N_dm_power_on_reset,
|
||||
|
||||
// rule RL_mkConnectionGetPut_1
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_1 =
|
||||
v_td2_to_td_0$RDY_in_put && proc$RDY_v_to_TV_0_get ;
|
||||
proc$RDY_v_to_TV_0_get && v_td2_to_td_0$RDY_in_put ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_1 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_1 ;
|
||||
|
||||
// rule RL_mkConnectionGetPut_2
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_2 =
|
||||
v_td2_to_td_0$RDY_out_get && tv_encode$RDY_v_cpu_in_0_put ;
|
||||
tv_encode$RDY_v_cpu_in_0_put && v_td2_to_td_0$RDY_out_get ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_2 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_2 ;
|
||||
|
||||
// rule RL_mkConnectionGetPut_3
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_3 =
|
||||
v_td2_to_td_1$RDY_in_put && proc$RDY_v_to_TV_1_get ;
|
||||
proc$RDY_v_to_TV_1_get && v_td2_to_td_1$RDY_in_put ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_3 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_3 ;
|
||||
|
||||
// rule RL_mkConnectionGetPut_4
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_4 =
|
||||
v_td2_to_td_1$RDY_out_get && tv_encode$RDY_v_cpu_in_1_put ;
|
||||
tv_encode$RDY_v_cpu_in_1_put && v_td2_to_td_1$RDY_out_get ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_4 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_4 ;
|
||||
|
||||
|
||||
@@ -1434,7 +1434,7 @@ module mkP3_Core(CLK,
|
||||
// rule RL_rl_ndm_reset_wait
|
||||
assign CAN_FIRE_RL_rl_ndm_reset_wait =
|
||||
(rg_ndm_reset_delay != 8'd1 ||
|
||||
corew$RDY_ndm_reset_client_response_put && corew$RDY_start) &&
|
||||
corew$RDY_start && corew$RDY_ndm_reset_client_response_put) &&
|
||||
rg_ndm_reset_delay != 8'd0 ;
|
||||
assign WILL_FIRE_RL_rl_ndm_reset_wait = CAN_FIRE_RL_rl_ndm_reset_wait ;
|
||||
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@@ -2716,22 +2716,22 @@ module mkCoreW(RST_N_dm_power_on_reset,
|
||||
// rule RL_rl_dm_hart0_reset_wait
|
||||
assign CAN_FIRE_RL_rl_dm_hart0_reset_wait =
|
||||
(rg_hart0_reset_delay != 8'd1 ||
|
||||
debug_module$RDY_hart0_reset_client_response_put &&
|
||||
proc$RDY_start) &&
|
||||
proc$RDY_start &&
|
||||
debug_module$RDY_hart0_reset_client_response_put) &&
|
||||
rg_hart0_reset_delay != 8'd0 ;
|
||||
assign WILL_FIRE_RL_rl_dm_hart0_reset_wait =
|
||||
CAN_FIRE_RL_rl_dm_hart0_reset_wait && !EN_start ;
|
||||
|
||||
// rule RL_ClientServerRequest
|
||||
assign CAN_FIRE_RL_ClientServerRequest =
|
||||
debug_module$RDY_hart0_client_run_halt_request_get &&
|
||||
proc$RDY_hart0_run_halt_server_request_put ;
|
||||
proc$RDY_hart0_run_halt_server_request_put &&
|
||||
debug_module$RDY_hart0_client_run_halt_request_get ;
|
||||
assign WILL_FIRE_RL_ClientServerRequest = CAN_FIRE_RL_ClientServerRequest ;
|
||||
|
||||
// rule RL_ClientServerResponse
|
||||
assign CAN_FIRE_RL_ClientServerResponse =
|
||||
debug_module$RDY_hart0_client_run_halt_response_put &&
|
||||
proc$RDY_hart0_run_halt_server_response_get ;
|
||||
proc$RDY_hart0_run_halt_server_response_get &&
|
||||
debug_module$RDY_hart0_client_run_halt_response_put ;
|
||||
assign WILL_FIRE_RL_ClientServerResponse =
|
||||
CAN_FIRE_RL_ClientServerResponse ;
|
||||
|
||||
@@ -2743,25 +2743,25 @@ module mkCoreW(RST_N_dm_power_on_reset,
|
||||
|
||||
// rule RL_mkConnectionGetPut_1
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_1 =
|
||||
v_td2_to_td_0$RDY_in_put && proc$RDY_v_to_TV_0_get ;
|
||||
proc$RDY_v_to_TV_0_get && v_td2_to_td_0$RDY_in_put ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_1 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_1 ;
|
||||
|
||||
// rule RL_mkConnectionGetPut_2
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_2 =
|
||||
v_td2_to_td_0$RDY_out_get && tv_encode$RDY_v_cpu_in_0_put ;
|
||||
tv_encode$RDY_v_cpu_in_0_put && v_td2_to_td_0$RDY_out_get ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_2 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_2 ;
|
||||
|
||||
// rule RL_mkConnectionGetPut_3
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_3 =
|
||||
v_td2_to_td_1$RDY_in_put && proc$RDY_v_to_TV_1_get ;
|
||||
proc$RDY_v_to_TV_1_get && v_td2_to_td_1$RDY_in_put ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_3 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_3 ;
|
||||
|
||||
// rule RL_mkConnectionGetPut_4
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_4 =
|
||||
v_td2_to_td_1$RDY_out_get && tv_encode$RDY_v_cpu_in_1_put ;
|
||||
tv_encode$RDY_v_cpu_in_1_put && v_td2_to_td_1$RDY_out_get ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_4 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_4 ;
|
||||
|
||||
|
||||
@@ -1434,7 +1434,7 @@ module mkP3_Core(CLK,
|
||||
// rule RL_rl_ndm_reset_wait
|
||||
assign CAN_FIRE_RL_rl_ndm_reset_wait =
|
||||
(rg_ndm_reset_delay != 8'd1 ||
|
||||
corew$RDY_ndm_reset_client_response_put && corew$RDY_start) &&
|
||||
corew$RDY_start && corew$RDY_ndm_reset_client_response_put) &&
|
||||
rg_ndm_reset_delay != 8'd0 ;
|
||||
assign WILL_FIRE_RL_rl_ndm_reset_wait = CAN_FIRE_RL_rl_ndm_reset_wait ;
|
||||
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@@ -2716,22 +2716,22 @@ module mkCoreW(RST_N_dm_power_on_reset,
|
||||
// rule RL_rl_dm_hart0_reset_wait
|
||||
assign CAN_FIRE_RL_rl_dm_hart0_reset_wait =
|
||||
(rg_hart0_reset_delay != 8'd1 ||
|
||||
debug_module$RDY_hart0_reset_client_response_put &&
|
||||
proc$RDY_start) &&
|
||||
proc$RDY_start &&
|
||||
debug_module$RDY_hart0_reset_client_response_put) &&
|
||||
rg_hart0_reset_delay != 8'd0 ;
|
||||
assign WILL_FIRE_RL_rl_dm_hart0_reset_wait =
|
||||
CAN_FIRE_RL_rl_dm_hart0_reset_wait && !EN_start ;
|
||||
|
||||
// rule RL_ClientServerRequest
|
||||
assign CAN_FIRE_RL_ClientServerRequest =
|
||||
debug_module$RDY_hart0_client_run_halt_request_get &&
|
||||
proc$RDY_hart0_run_halt_server_request_put ;
|
||||
proc$RDY_hart0_run_halt_server_request_put &&
|
||||
debug_module$RDY_hart0_client_run_halt_request_get ;
|
||||
assign WILL_FIRE_RL_ClientServerRequest = CAN_FIRE_RL_ClientServerRequest ;
|
||||
|
||||
// rule RL_ClientServerResponse
|
||||
assign CAN_FIRE_RL_ClientServerResponse =
|
||||
debug_module$RDY_hart0_client_run_halt_response_put &&
|
||||
proc$RDY_hart0_run_halt_server_response_get ;
|
||||
proc$RDY_hart0_run_halt_server_response_get &&
|
||||
debug_module$RDY_hart0_client_run_halt_response_put ;
|
||||
assign WILL_FIRE_RL_ClientServerResponse =
|
||||
CAN_FIRE_RL_ClientServerResponse ;
|
||||
|
||||
@@ -2743,25 +2743,25 @@ module mkCoreW(RST_N_dm_power_on_reset,
|
||||
|
||||
// rule RL_mkConnectionGetPut_1
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_1 =
|
||||
v_td2_to_td_0$RDY_in_put && proc$RDY_v_to_TV_0_get ;
|
||||
proc$RDY_v_to_TV_0_get && v_td2_to_td_0$RDY_in_put ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_1 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_1 ;
|
||||
|
||||
// rule RL_mkConnectionGetPut_2
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_2 =
|
||||
v_td2_to_td_0$RDY_out_get && tv_encode$RDY_v_cpu_in_0_put ;
|
||||
tv_encode$RDY_v_cpu_in_0_put && v_td2_to_td_0$RDY_out_get ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_2 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_2 ;
|
||||
|
||||
// rule RL_mkConnectionGetPut_3
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_3 =
|
||||
v_td2_to_td_1$RDY_in_put && proc$RDY_v_to_TV_1_get ;
|
||||
proc$RDY_v_to_TV_1_get && v_td2_to_td_1$RDY_in_put ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_3 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_3 ;
|
||||
|
||||
// rule RL_mkConnectionGetPut_4
|
||||
assign CAN_FIRE_RL_mkConnectionGetPut_4 =
|
||||
v_td2_to_td_1$RDY_out_get && tv_encode$RDY_v_cpu_in_1_put ;
|
||||
tv_encode$RDY_v_cpu_in_1_put && v_td2_to_td_1$RDY_out_get ;
|
||||
assign WILL_FIRE_RL_mkConnectionGetPut_4 =
|
||||
CAN_FIRE_RL_mkConnectionGetPut_4 ;
|
||||
|
||||
|
||||
@@ -1434,7 +1434,7 @@ module mkP3_Core(CLK,
|
||||
// rule RL_rl_ndm_reset_wait
|
||||
assign CAN_FIRE_RL_rl_ndm_reset_wait =
|
||||
(rg_ndm_reset_delay != 8'd1 ||
|
||||
corew$RDY_ndm_reset_client_response_put && corew$RDY_start) &&
|
||||
corew$RDY_start && corew$RDY_ndm_reset_client_response_put) &&
|
||||
rg_ndm_reset_delay != 8'd0 ;
|
||||
assign WILL_FIRE_RL_rl_ndm_reset_wait = CAN_FIRE_RL_rl_ndm_reset_wait ;
|
||||
|
||||
|
||||
Reference in New Issue
Block a user