Cheri-research/Toooba
1
0
Fork 0
Code Issues 1 Pull Requests Actions Packages Projects Releases Wiki Activity

Fixed a Tandem-Verification bug (reporting incorrect MIP/MIE/SIP/SIE post-write values)

Browse Source 
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:
rsnikhil
2020-03-04 09:50:39 -05:00
parent 40b55d2c32
commit 75df204e31
11 changed files with 27099 additions and 27049 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14136
builds/RV64ACDFIMSU_Toooba_verilator/Verilog_RTL/mkCore.v
View File

File diff suppressed because it is too large Load Diff

9
src_Core/CPU/CsrFile.bsv
View File

@@ -474,6 +474,11 @@ module mkCsrFile #(Data hartid)(CsrFile);
software_int_pend_vec[prvM], readOnlyReg(1'b0), 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] 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 // minstret
Ehr#(2, Data) minstret_ehr <- mkCsrEhr(0); Ehr#(2, Data) minstret_ehr <- mkCsrEhr(0);
Reg#(Data) minstret_csr = minstret_ehr[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]}; 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]}; 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]}; 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]}; CSRmip: (x & mip_mie_warl_mask);
CSRmie: { 52'b0, x[11], 1'b0, x[9:8], x[7], 1'b0, x[5:4], x[3], 1'b0, x[1:0]}; CSRmie: (x & mip_mie_warl_mask);
CSRmcounteren: { 61'b0, x[2:0]}; CSRmcounteren: { 61'b0, x[2:0]};
CSRmcause: { x[63], 59'b0, x[3:0] }; CSRmcause: { x[63], 59'b0, x[3:0] };

13303
src_SSITH_P3/Verilog_RTL/mkCore.v
View File

File diff suppressed because it is too large Load Diff

20
src_SSITH_P3/Verilog_RTL/mkCoreW.v
View File

@@ -2716,22 +2716,22 @@ module mkCoreW(RST_N_dm_power_on_reset,
// rule RL_rl_dm_hart0_reset_wait // rule RL_rl_dm_hart0_reset_wait
assign CAN_FIRE_RL_rl_dm_hart0_reset_wait = assign CAN_FIRE_RL_rl_dm_hart0_reset_wait =
(rg_hart0_reset_delay != 8'd1 || (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 ; rg_hart0_reset_delay != 8'd0 ;
assign WILL_FIRE_RL_rl_dm_hart0_reset_wait = assign WILL_FIRE_RL_rl_dm_hart0_reset_wait =
CAN_FIRE_RL_rl_dm_hart0_reset_wait && !EN_start ; CAN_FIRE_RL_rl_dm_hart0_reset_wait && !EN_start ;
// rule RL_ClientServerRequest // rule RL_ClientServerRequest
assign CAN_FIRE_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 ; assign WILL_FIRE_RL_ClientServerRequest = CAN_FIRE_RL_ClientServerRequest ;
// rule RL_ClientServerResponse // rule RL_ClientServerResponse
assign CAN_FIRE_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 = assign WILL_FIRE_RL_ClientServerResponse =
CAN_FIRE_RL_ClientServerResponse ; CAN_FIRE_RL_ClientServerResponse ;
@@ -2743,25 +2743,25 @@ module mkCoreW(RST_N_dm_power_on_reset,
// rule RL_mkConnectionGetPut_1 // rule RL_mkConnectionGetPut_1
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_1 =
CAN_FIRE_RL_mkConnectionGetPut_1 ; CAN_FIRE_RL_mkConnectionGetPut_1 ;
// rule RL_mkConnectionGetPut_2 // rule RL_mkConnectionGetPut_2
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_2 =
CAN_FIRE_RL_mkConnectionGetPut_2 ; CAN_FIRE_RL_mkConnectionGetPut_2 ;
// rule RL_mkConnectionGetPut_3 // rule RL_mkConnectionGetPut_3
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_3 =
CAN_FIRE_RL_mkConnectionGetPut_3 ; CAN_FIRE_RL_mkConnectionGetPut_3 ;
// rule RL_mkConnectionGetPut_4 // rule RL_mkConnectionGetPut_4
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_4 =
CAN_FIRE_RL_mkConnectionGetPut_4 ; CAN_FIRE_RL_mkConnectionGetPut_4 ;

2
src_SSITH_P3/Verilog_RTL/mkP3_Core.v
View File

@@ -1434,7 +1434,7 @@ module mkP3_Core(CLK,
// rule RL_rl_ndm_reset_wait // rule RL_rl_ndm_reset_wait
assign CAN_FIRE_RL_rl_ndm_reset_wait = assign CAN_FIRE_RL_rl_ndm_reset_wait =
(rg_ndm_reset_delay != 8'd1 || (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 ; rg_ndm_reset_delay != 8'd0 ;
assign WILL_FIRE_RL_rl_ndm_reset_wait = CAN_FIRE_RL_rl_ndm_reset_wait ; assign WILL_FIRE_RL_rl_ndm_reset_wait = CAN_FIRE_RL_rl_ndm_reset_wait ;

13331
src_SSITH_P3/Verilog_RTL_sim/mkCore.v
View File

File diff suppressed because it is too large Load Diff

20
src_SSITH_P3/Verilog_RTL_sim/mkCoreW.v
View File

@@ -2716,22 +2716,22 @@ module mkCoreW(RST_N_dm_power_on_reset,
// rule RL_rl_dm_hart0_reset_wait // rule RL_rl_dm_hart0_reset_wait
assign CAN_FIRE_RL_rl_dm_hart0_reset_wait = assign CAN_FIRE_RL_rl_dm_hart0_reset_wait =
(rg_hart0_reset_delay != 8'd1 || (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 ; rg_hart0_reset_delay != 8'd0 ;
assign WILL_FIRE_RL_rl_dm_hart0_reset_wait = assign WILL_FIRE_RL_rl_dm_hart0_reset_wait =
CAN_FIRE_RL_rl_dm_hart0_reset_wait && !EN_start ; CAN_FIRE_RL_rl_dm_hart0_reset_wait && !EN_start ;
// rule RL_ClientServerRequest // rule RL_ClientServerRequest
assign CAN_FIRE_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 ; assign WILL_FIRE_RL_ClientServerRequest = CAN_FIRE_RL_ClientServerRequest ;
// rule RL_ClientServerResponse // rule RL_ClientServerResponse
assign CAN_FIRE_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 = assign WILL_FIRE_RL_ClientServerResponse =
CAN_FIRE_RL_ClientServerResponse ; CAN_FIRE_RL_ClientServerResponse ;
@@ -2743,25 +2743,25 @@ module mkCoreW(RST_N_dm_power_on_reset,
// rule RL_mkConnectionGetPut_1 // rule RL_mkConnectionGetPut_1
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_1 =
CAN_FIRE_RL_mkConnectionGetPut_1 ; CAN_FIRE_RL_mkConnectionGetPut_1 ;
// rule RL_mkConnectionGetPut_2 // rule RL_mkConnectionGetPut_2
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_2 =
CAN_FIRE_RL_mkConnectionGetPut_2 ; CAN_FIRE_RL_mkConnectionGetPut_2 ;
// rule RL_mkConnectionGetPut_3 // rule RL_mkConnectionGetPut_3
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_3 =
CAN_FIRE_RL_mkConnectionGetPut_3 ; CAN_FIRE_RL_mkConnectionGetPut_3 ;
// rule RL_mkConnectionGetPut_4 // rule RL_mkConnectionGetPut_4
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_4 =
CAN_FIRE_RL_mkConnectionGetPut_4 ; CAN_FIRE_RL_mkConnectionGetPut_4 ;

2
src_SSITH_P3/Verilog_RTL_sim/mkP3_Core.v
View File

@@ -1434,7 +1434,7 @@ module mkP3_Core(CLK,
// rule RL_rl_ndm_reset_wait // rule RL_rl_ndm_reset_wait
assign CAN_FIRE_RL_rl_ndm_reset_wait = assign CAN_FIRE_RL_rl_ndm_reset_wait =
(rg_ndm_reset_delay != 8'd1 || (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 ; rg_ndm_reset_delay != 8'd0 ;
assign WILL_FIRE_RL_rl_ndm_reset_wait = CAN_FIRE_RL_rl_ndm_reset_wait ; assign WILL_FIRE_RL_rl_ndm_reset_wait = CAN_FIRE_RL_rl_ndm_reset_wait ;

13303
src_SSITH_P3/xilinx_ip/hdl/mkCore.v
View File

File diff suppressed because it is too large Load Diff

20
src_SSITH_P3/xilinx_ip/hdl/mkCoreW.v
View File

@@ -2716,22 +2716,22 @@ module mkCoreW(RST_N_dm_power_on_reset,
// rule RL_rl_dm_hart0_reset_wait // rule RL_rl_dm_hart0_reset_wait
assign CAN_FIRE_RL_rl_dm_hart0_reset_wait = assign CAN_FIRE_RL_rl_dm_hart0_reset_wait =
(rg_hart0_reset_delay != 8'd1 || (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 ; rg_hart0_reset_delay != 8'd0 ;
assign WILL_FIRE_RL_rl_dm_hart0_reset_wait = assign WILL_FIRE_RL_rl_dm_hart0_reset_wait =
CAN_FIRE_RL_rl_dm_hart0_reset_wait && !EN_start ; CAN_FIRE_RL_rl_dm_hart0_reset_wait && !EN_start ;
// rule RL_ClientServerRequest // rule RL_ClientServerRequest
assign CAN_FIRE_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 ; assign WILL_FIRE_RL_ClientServerRequest = CAN_FIRE_RL_ClientServerRequest ;
// rule RL_ClientServerResponse // rule RL_ClientServerResponse
assign CAN_FIRE_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 = assign WILL_FIRE_RL_ClientServerResponse =
CAN_FIRE_RL_ClientServerResponse ; CAN_FIRE_RL_ClientServerResponse ;
@@ -2743,25 +2743,25 @@ module mkCoreW(RST_N_dm_power_on_reset,
// rule RL_mkConnectionGetPut_1 // rule RL_mkConnectionGetPut_1
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_1 =
CAN_FIRE_RL_mkConnectionGetPut_1 ; CAN_FIRE_RL_mkConnectionGetPut_1 ;
// rule RL_mkConnectionGetPut_2 // rule RL_mkConnectionGetPut_2
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_2 =
CAN_FIRE_RL_mkConnectionGetPut_2 ; CAN_FIRE_RL_mkConnectionGetPut_2 ;
// rule RL_mkConnectionGetPut_3 // rule RL_mkConnectionGetPut_3
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_3 =
CAN_FIRE_RL_mkConnectionGetPut_3 ; CAN_FIRE_RL_mkConnectionGetPut_3 ;
// rule RL_mkConnectionGetPut_4 // rule RL_mkConnectionGetPut_4
assign CAN_FIRE_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 = assign WILL_FIRE_RL_mkConnectionGetPut_4 =
CAN_FIRE_RL_mkConnectionGetPut_4 ; CAN_FIRE_RL_mkConnectionGetPut_4 ;

2
src_SSITH_P3/xilinx_ip/hdl/mkP3_Core.v
View File

@@ -1434,7 +1434,7 @@ module mkP3_Core(CLK,
// rule RL_rl_ndm_reset_wait // rule RL_rl_ndm_reset_wait
assign CAN_FIRE_RL_rl_ndm_reset_wait = assign CAN_FIRE_RL_rl_ndm_reset_wait =
(rg_ndm_reset_delay != 8'd1 || (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 ; rg_ndm_reset_delay != 8'd0 ;
assign WILL_FIRE_RL_rl_ndm_reset_wait = CAN_FIRE_RL_rl_ndm_reset_wait ; assign WILL_FIRE_RL_rl_ndm_reset_wait = CAN_FIRE_RL_rl_ndm_reset_wait ;