Fixed Tandem Verif trace gen for CSRRx on WARL regs: report post-WARL-xformed write-data

This commit is contained in:
rsnikhil
2020-02-11 15:46:24 -05:00
parent db114186af
commit 82e56c2908
11 changed files with 35666 additions and 34293 deletions

File diff suppressed because it is too large Load Diff

View File

@@ -7,7 +7,7 @@
// Ports:
// Name I/O size props
// RDY_write_enq O 1 const
// read_deq O 290
// read_deq O 354
// RDY_read_deq O 1 const
// RDY_setLSQAtCommitNotified O 1 const
// RDY_setExecuted_deqLSQ O 1 const
@@ -26,13 +26,16 @@
// RDY_correctSpeculation O 1 const
// CLK I 1 clock
// RST_N I 1 reset
// write_enq_x I 290
// write_enq_x I 354
// setExecuted_deqLSQ_cause I 5
// setExecuted_deqLSQ_ld_killed I 3
// setExecuted_doFinishAlu_0_set_dst_data I 64
// setExecuted_doFinishAlu_0_set_csrData I 65
// setExecuted_doFinishAlu_0_set_cf I 130
// setExecuted_doFinishAlu_1_set_dst_data I 64
// setExecuted_doFinishAlu_1_set_csrData I 65
// setExecuted_doFinishAlu_1_set_cf I 130
// setExecuted_doFinishFpuMulDiv_0_set_dst_data I 64
// setExecuted_doFinishFpuMulDiv_0_set_fflags I 5
// setExecuted_doFinishMem_vaddr I 64
// setExecuted_doFinishMem_access_at_commit I 1
@@ -84,16 +87,19 @@ module mkRobRowSynth(CLK,
EN_setExecuted_deqLSQ,
RDY_setExecuted_deqLSQ,
setExecuted_doFinishAlu_0_set_dst_data,
setExecuted_doFinishAlu_0_set_csrData,
setExecuted_doFinishAlu_0_set_cf,
EN_setExecuted_doFinishAlu_0_set,
RDY_setExecuted_doFinishAlu_0_set,
setExecuted_doFinishAlu_1_set_dst_data,
setExecuted_doFinishAlu_1_set_csrData,
setExecuted_doFinishAlu_1_set_cf,
EN_setExecuted_doFinishAlu_1_set,
RDY_setExecuted_doFinishAlu_1_set,
setExecuted_doFinishFpuMulDiv_0_set_dst_data,
setExecuted_doFinishFpuMulDiv_0_set_fflags,
EN_setExecuted_doFinishFpuMulDiv_0_set,
RDY_setExecuted_doFinishFpuMulDiv_0_set,
@@ -124,12 +130,12 @@ module mkRobRowSynth(CLK,
input RST_N;
// action method write_enq
input [289 : 0] write_enq_x;
input [353 : 0] write_enq_x;
input EN_write_enq;
output RDY_write_enq;
// value method read_deq
output [289 : 0] read_deq;
output [353 : 0] read_deq;
output RDY_read_deq;
// action method setLSQAtCommitNotified
@@ -143,18 +149,21 @@ module mkRobRowSynth(CLK,
output RDY_setExecuted_deqLSQ;
// action method setExecuted_doFinishAlu_0_set
input [63 : 0] setExecuted_doFinishAlu_0_set_dst_data;
input [64 : 0] setExecuted_doFinishAlu_0_set_csrData;
input [129 : 0] setExecuted_doFinishAlu_0_set_cf;
input EN_setExecuted_doFinishAlu_0_set;
output RDY_setExecuted_doFinishAlu_0_set;
// action method setExecuted_doFinishAlu_1_set
input [63 : 0] setExecuted_doFinishAlu_1_set_dst_data;
input [64 : 0] setExecuted_doFinishAlu_1_set_csrData;
input [129 : 0] setExecuted_doFinishAlu_1_set_cf;
input EN_setExecuted_doFinishAlu_1_set;
output RDY_setExecuted_doFinishAlu_1_set;
// action method setExecuted_doFinishFpuMulDiv_0_set
input [63 : 0] setExecuted_doFinishFpuMulDiv_0_set_dst_data;
input [4 : 0] setExecuted_doFinishFpuMulDiv_0_set_fflags;
input EN_setExecuted_doFinishFpuMulDiv_0_set;
output RDY_setExecuted_doFinishFpuMulDiv_0_set;
@@ -189,7 +198,7 @@ module mkRobRowSynth(CLK,
output RDY_correctSpeculation;
// signals for module outputs
wire [289 : 0] read_deq;
wire [353 : 0] read_deq;
wire [63 : 0] getOrigPC, getOrigPredPC;
wire [31 : 0] getOrig_Inst;
wire RDY_correctSpeculation,
@@ -275,6 +284,11 @@ module mkRobRowSynth(CLK,
wire [65 : 0] m_ppc_vaddr_csrData_rl$D_IN;
wire m_ppc_vaddr_csrData_rl$EN;
// register m_rg_dst_data
reg [63 : 0] m_rg_dst_data;
reg [63 : 0] m_rg_dst_data$D_IN;
wire m_rg_dst_data$EN;
// register m_rg_dst_reg
reg [6 : 0] m_rg_dst_reg;
wire [6 : 0] m_rg_dst_reg$D_IN;
@@ -486,19 +500,19 @@ module mkRobRowSynth(CLK,
CASE_write_enq_x_BITS_165_TO_162_0_write_enq_x_ETC__q5,
CASE_write_enq_x_BITS_165_TO_162_0_write_enq_x_ETC__q6;
reg [1 : 0] CASE_write_enq_x_BITS_97_TO_96_0_write_enq_x_B_ETC__q7;
wire [181 : 0] m_csr_61_BIT_12_62_CONCAT_IF_m_csr_61_BIT_12_6_ETC___d639;
wire [167 : 0] m_trap_dummy2_0_read__38_AND_m_trap_dummy2_1_r_ETC___d638;
wire [65 : 0] IF_NOT_m_ppc_vaddr_csrData_dummy2_0_read__92_9_ETC___d583;
wire [245 : 0] m_rg_dst_data_62_CONCAT_m_csr_63_BIT_12_64_CON_ETC___d643;
wire [168 : 0] m_claimed_phy_reg_40_CONCAT_m_trap_dummy2_0_re_ETC___d642;
wire [65 : 0] IF_NOT_m_ppc_vaddr_csrData_dummy2_0_read__92_9_ETC___d587;
wire [63 : 0] IF_m_ppc_vaddr_csrData_dummy2_0_read__92_AND_m_ETC___d307,
IF_m_ppc_vaddr_csrData_lat_1_whas__74_THEN_m_p_ETC___d206,
IF_m_ppc_vaddr_csrData_lat_3_whas__66_THEN_m_p_ETC___d208,
x__h26921;
x__h26961;
wire [11 : 0] IF_m_spec_bits_lat_1_whas__84_THEN_m_spec_bits_ETC___d290,
bs__h33059,
sb__h33094,
upd__h17960;
bs__h33169,
sb__h33204,
upd__h17993;
wire [4 : 0] IF_m_trap_lat_2_whas_THEN_m_trap_lat_2_wget_BI_ETC___d153,
x_read_deq_fflags__h26018;
x_read_deq_fflags__h26056;
wire [3 : 0] IF_IF_m_trap_lat_2_whas_THEN_NOT_m_trap_lat_2__ETC___d152,
IF_IF_m_trap_lat_2_whas_THEN_m_trap_lat_2_wget_ETC___d131,
IF_IF_m_trap_lat_2_whas_THEN_m_trap_lat_2_wget_ETC___d132,
@@ -527,11 +541,11 @@ module mkRobRowSynth(CLK,
IF_m_trap_lat_2_whas_THEN_m_trap_lat_2_wget_BI_ETC___d74,
IF_m_trap_lat_2_whas_THEN_m_trap_lat_2_wget_BI_ETC___d81,
IF_m_trap_lat_2_whas_THEN_m_trap_lat_2_wget_BI_ETC___d95,
NOT_m_csr_61_BIT_12_62_EQ_setExecuted_doFinish_ETC___d681,
NOT_m_csr_61_BIT_12_62_EQ_setExecuted_doFinish_ETC___d689,
NOT_m_csr_63_BIT_12_64_EQ_setExecuted_doFinish_ETC___d685,
NOT_m_csr_63_BIT_12_64_EQ_setExecuted_doFinish_ETC___d693,
NOT_m_ppc_vaddr_csrData_dummy2_0_read__92_93_O_ETC___d302,
m_rob_inst_state_dummy2_0_read__89_AND_m_rob_i_ETC___d600,
m_trap_dummy2_0_read__38_AND_m_trap_dummy2_1_r_ETC___d543;
m_rob_inst_state_dummy2_0_read__93_AND_m_rob_i_ETC___d604,
m_trap_dummy2_0_read__41_AND_m_trap_dummy2_1_r_ETC___d546;
// action method write_enq
assign RDY_write_enq = 1'd1 ;
@@ -542,9 +556,9 @@ module mkRobRowSynth(CLK,
assign read_deq =
{ m_pc,
m_orig_inst,
m_rg_dst_reg,
m_iType,
m_csr_61_BIT_12_62_CONCAT_IF_m_csr_61_BIT_12_6_ETC___d639 } ;
m_rg_dst_reg,
m_rg_dst_data_62_CONCAT_m_csr_63_BIT_12_64_CON_ETC___d643 } ;
assign RDY_read_deq = 1'd1 ;
// action method setLSQAtCommitNotified
@@ -597,7 +611,7 @@ module mkRobRowSynth(CLK,
assign RDY_getOrig_Inst = 1'd1 ;
// value method dependsOn_wrongSpec
assign dependsOn_wrongSpec = bs__h33059[dependsOn_wrongSpec_tag] ;
assign dependsOn_wrongSpec = bs__h33169[dependsOn_wrongSpec_tag] ;
assign RDY_dependsOn_wrongSpec = 1'd1 ;
// action method correctSpeculation
@@ -890,7 +904,7 @@ module mkRobRowSynth(CLK,
assign m_fflags_rl$EN = 1'd1 ;
// register m_iType
assign m_iType$D_IN = write_enq_x[186:182] ;
assign m_iType$D_IN = write_enq_x[257:253] ;
assign m_iType$EN = EN_write_enq ;
// register m_ldKilled_rl
@@ -923,11 +937,11 @@ module mkRobRowSynth(CLK,
assign m_nonMMIOStDone_rl$EN = 1'd1 ;
// register m_orig_inst
assign m_orig_inst$D_IN = write_enq_x[225:194] ;
assign m_orig_inst$D_IN = write_enq_x[289:258] ;
assign m_orig_inst$EN = EN_write_enq ;
// register m_pc
assign m_pc$D_IN = write_enq_x[289:226] ;
assign m_pc$D_IN = write_enq_x[353:290] ;
assign m_pc$EN = EN_write_enq ;
// register m_ppc_vaddr_csrData_rl
@@ -940,8 +954,30 @@ module mkRobRowSynth(CLK,
IF_m_ppc_vaddr_csrData_lat_3_whas__66_THEN_m_p_ETC___d208 } ;
assign m_ppc_vaddr_csrData_rl$EN = 1'd1 ;
// register m_rg_dst_data
always@(EN_setExecuted_doFinishFpuMulDiv_0_set or
setExecuted_doFinishFpuMulDiv_0_set_dst_data or
EN_setExecuted_doFinishAlu_1_set or
setExecuted_doFinishAlu_1_set_dst_data or
EN_setExecuted_doFinishAlu_0_set or
setExecuted_doFinishAlu_0_set_dst_data)
case (1'b1)
EN_setExecuted_doFinishFpuMulDiv_0_set:
m_rg_dst_data$D_IN = setExecuted_doFinishFpuMulDiv_0_set_dst_data;
EN_setExecuted_doFinishAlu_1_set:
m_rg_dst_data$D_IN = setExecuted_doFinishAlu_1_set_dst_data;
EN_setExecuted_doFinishAlu_0_set:
m_rg_dst_data$D_IN = setExecuted_doFinishAlu_0_set_dst_data;
default: m_rg_dst_data$D_IN =
64'hAAAAAAAAAAAAAAAA /* unspecified value */ ;
endcase
assign m_rg_dst_data$EN =
EN_setExecuted_doFinishAlu_0_set ||
EN_setExecuted_doFinishAlu_1_set ||
EN_setExecuted_doFinishFpuMulDiv_0_set ;
// register m_rg_dst_reg
assign m_rg_dst_reg$D_IN = write_enq_x[193:187] ;
assign m_rg_dst_reg$D_IN = write_enq_x[252:246] ;
assign m_rg_dst_reg$EN = EN_write_enq ;
// register m_rob_inst_state_rl
@@ -955,7 +991,7 @@ module mkRobRowSynth(CLK,
// register m_spec_bits_rl
assign m_spec_bits_rl$D_IN =
EN_correctSpeculation ?
upd__h17960 :
upd__h17993 :
IF_m_spec_bits_lat_1_whas__84_THEN_m_spec_bits_ETC___d290 ;
assign m_spec_bits_rl$EN = 1'd1 ;
@@ -1187,7 +1223,7 @@ module mkRobRowSynth(CLK,
(IF_m_trap_lat_2_whas_THEN_m_trap_lat_2_wget_BI_ETC___d67 ?
4'd3 :
IF_IF_m_trap_lat_2_whas_THEN_m_trap_lat_2_wget_ETC___d148) ;
assign IF_NOT_m_ppc_vaddr_csrData_dummy2_0_read__92_9_ETC___d583 =
assign IF_NOT_m_ppc_vaddr_csrData_dummy2_0_read__92_9_ETC___d587 =
(NOT_m_ppc_vaddr_csrData_dummy2_0_read__92_93_O_ETC___d302 ||
m_ppc_vaddr_csrData_rl[65:64] == 2'd0) ?
{ 2'd0,
@@ -1209,7 +1245,7 @@ module mkRobRowSynth(CLK,
m_ldKilled_rl[1:0]) ;
assign IF_m_memAccessAtCommit_lat_1_whas__60_THEN_m_m_ETC___d266 =
EN_write_enq ?
write_enq_x[186:182] == 5'd14 :
write_enq_x[257:253] == 5'd14 :
(EN_setExecuted_doFinishMem ?
setExecuted_doFinishMem_access_at_commit :
m_memAccessAtCommit_rl) ;
@@ -1317,48 +1353,32 @@ module mkRobRowSynth(CLK,
(m_trap_lat_0$whas ?
m_trap_lat_0$wget[3:0] == 4'd7 :
m_trap_rl[3:0] == 4'd7) ;
assign NOT_m_csr_61_BIT_12_62_EQ_setExecuted_doFinish_ETC___d681 =
assign NOT_m_csr_63_BIT_12_64_EQ_setExecuted_doFinish_ETC___d685 =
m_csr[12] != setExecuted_doFinishAlu_0_set_csrData[64] ;
assign NOT_m_csr_61_BIT_12_62_EQ_setExecuted_doFinish_ETC___d689 =
assign NOT_m_csr_63_BIT_12_64_EQ_setExecuted_doFinish_ETC___d693 =
m_csr[12] != setExecuted_doFinishAlu_1_set_csrData[64] ;
assign NOT_m_ppc_vaddr_csrData_dummy2_0_read__92_93_O_ETC___d302 =
!m_ppc_vaddr_csrData_dummy2_0$Q_OUT ||
!m_ppc_vaddr_csrData_dummy2_1$Q_OUT ||
!m_ppc_vaddr_csrData_dummy2_2$Q_OUT ||
!m_ppc_vaddr_csrData_dummy2_3$Q_OUT ;
assign bs__h33059 =
assign bs__h33169 =
(m_spec_bits_dummy2_0$Q_OUT && m_spec_bits_dummy2_1$Q_OUT &&
m_spec_bits_dummy2_2$Q_OUT) ?
m_spec_bits_rl :
12'd0 ;
assign m_csr_61_BIT_12_62_CONCAT_IF_m_csr_61_BIT_12_6_ETC___d639 =
{ m_csr[12],
CASE_m_csr_BITS_11_TO_0_1_m_csr_BITS_11_TO_0_2_ETC__q3,
m_claimed_phy_reg,
m_trap_dummy2_0_read__38_AND_m_trap_dummy2_1_r_ETC___d638 } ;
assign m_rob_inst_state_dummy2_0_read__89_AND_m_rob_i_ETC___d600 =
m_rob_inst_state_dummy2_0$Q_OUT &&
m_rob_inst_state_dummy2_1$Q_OUT &&
m_rob_inst_state_dummy2_2$Q_OUT &&
m_rob_inst_state_dummy2_3$Q_OUT &&
m_rob_inst_state_dummy2_4$Q_OUT &&
m_rob_inst_state_dummy2_5$Q_OUT &&
m_rob_inst_state_rl ;
assign m_trap_dummy2_0_read__38_AND_m_trap_dummy2_1_r_ETC___d543 =
m_trap_dummy2_0$Q_OUT && m_trap_dummy2_1$Q_OUT &&
m_trap_dummy2_2$Q_OUT &&
m_trap_rl[5] ;
assign m_trap_dummy2_0_read__38_AND_m_trap_dummy2_1_r_ETC___d638 =
{ m_trap_dummy2_0_read__38_AND_m_trap_dummy2_1_r_ETC___d543,
assign m_claimed_phy_reg_40_CONCAT_m_trap_dummy2_0_re_ETC___d642 =
{ m_claimed_phy_reg,
m_trap_dummy2_0_read__41_AND_m_trap_dummy2_1_r_ETC___d546,
m_trap_rl[4],
m_trap_rl[4] ?
CASE_m_trap_rl_BITS_3_TO_0_0_m_trap_rl_BITS_3__ETC__q1 :
CASE_m_trap_rl_BITS_3_TO_0_0_m_trap_rl_BITS_3__ETC__q2,
x__h26921,
IF_NOT_m_ppc_vaddr_csrData_dummy2_0_read__92_9_ETC___d583,
x_read_deq_fflags__h26018,
x__h26961,
IF_NOT_m_ppc_vaddr_csrData_dummy2_0_read__92_9_ETC___d587,
x_read_deq_fflags__h26056,
m_will_dirty_fpu_state,
m_rob_inst_state_dummy2_0_read__89_AND_m_rob_i_ETC___d600,
m_rob_inst_state_dummy2_0_read__93_AND_m_rob_i_ETC___d604,
m_lsqTag,
m_ldKilled_dummy2_0$Q_OUT && m_ldKilled_dummy2_1$Q_OUT &&
m_ldKilled_rl[2],
@@ -1374,18 +1394,35 @@ module mkRobRowSynth(CLK,
m_nonMMIOStDone_dummy2_1$Q_OUT &&
m_nonMMIOStDone_rl,
m_epochIncremented,
bs__h33059 } ;
assign sb__h33094 =
bs__h33169 } ;
assign m_rg_dst_data_62_CONCAT_m_csr_63_BIT_12_64_CON_ETC___d643 =
{ m_rg_dst_data,
m_csr[12],
CASE_m_csr_BITS_11_TO_0_1_m_csr_BITS_11_TO_0_2_ETC__q3,
m_claimed_phy_reg_40_CONCAT_m_trap_dummy2_0_re_ETC___d642 } ;
assign m_rob_inst_state_dummy2_0_read__93_AND_m_rob_i_ETC___d604 =
m_rob_inst_state_dummy2_0$Q_OUT &&
m_rob_inst_state_dummy2_1$Q_OUT &&
m_rob_inst_state_dummy2_2$Q_OUT &&
m_rob_inst_state_dummy2_3$Q_OUT &&
m_rob_inst_state_dummy2_4$Q_OUT &&
m_rob_inst_state_dummy2_5$Q_OUT &&
m_rob_inst_state_rl ;
assign m_trap_dummy2_0_read__41_AND_m_trap_dummy2_1_r_ETC___d546 =
m_trap_dummy2_0$Q_OUT && m_trap_dummy2_1$Q_OUT &&
m_trap_dummy2_2$Q_OUT &&
m_trap_rl[5] ;
assign sb__h33204 =
m_spec_bits_dummy2_2$Q_OUT ?
IF_m_spec_bits_lat_1_whas__84_THEN_m_spec_bits_ETC___d290 :
12'd0 ;
assign upd__h17960 = sb__h33094 & correctSpeculation_mask ;
assign x__h26921 =
assign upd__h17993 = sb__h33204 & correctSpeculation_mask ;
assign x__h26961 =
(m_tval_dummy2_0$Q_OUT && m_tval_dummy2_1$Q_OUT &&
m_tval_dummy2_2$Q_OUT) ?
m_tval_rl :
64'd0 ;
assign x_read_deq_fflags__h26018 =
assign x_read_deq_fflags__h26056 =
(m_fflags_dummy2_0$Q_OUT && m_fflags_dummy2_1$Q_OUT) ?
m_fflags_rl :
5'd0 ;
@@ -1621,6 +1658,8 @@ module mkRobRowSynth(CLK,
if (m_lsqTag$EN) m_lsqTag <= `BSV_ASSIGNMENT_DELAY m_lsqTag$D_IN;
if (m_orig_inst$EN) m_orig_inst <= `BSV_ASSIGNMENT_DELAY m_orig_inst$D_IN;
if (m_pc$EN) m_pc <= `BSV_ASSIGNMENT_DELAY m_pc$D_IN;
if (m_rg_dst_data$EN)
m_rg_dst_data <= `BSV_ASSIGNMENT_DELAY m_rg_dst_data$D_IN;
if (m_rg_dst_reg$EN)
m_rg_dst_reg <= `BSV_ASSIGNMENT_DELAY m_rg_dst_reg$D_IN;
if (m_will_dirty_fpu_state$EN)
@@ -1646,6 +1685,7 @@ module mkRobRowSynth(CLK,
m_orig_inst = 32'hAAAAAAAA;
m_pc = 64'hAAAAAAAAAAAAAAAA;
m_ppc_vaddr_csrData_rl = 66'h2AAAAAAAAAAAAAAAA;
m_rg_dst_data = 64'hAAAAAAAAAAAAAAAA;
m_rg_dst_reg = 7'h2A;
m_rob_inst_state_rl = 1'h0;
m_spec_bits_rl = 12'hAAA;
@@ -1664,39 +1704,39 @@ module mkRobRowSynth(CLK,
#0;
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_doFinishAlu_0_set &&
NOT_m_csr_61_BIT_12_62_EQ_setExecuted_doFinish_ETC___d681)
NOT_m_csr_63_BIT_12_64_EQ_setExecuted_doFinish_ETC___d685)
$fdisplay(32'h80000002, "\n%m: ASSERT FAIL!!");
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_doFinishAlu_0_set &&
NOT_m_csr_61_BIT_12_62_EQ_setExecuted_doFinish_ETC___d681)
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 212, column 60\ncsr valid should match");
NOT_m_csr_63_BIT_12_64_EQ_setExecuted_doFinish_ETC___d685)
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 225, column 60\ncsr valid should match");
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_doFinishAlu_0_set &&
NOT_m_csr_61_BIT_12_62_EQ_setExecuted_doFinish_ETC___d681)
NOT_m_csr_63_BIT_12_64_EQ_setExecuted_doFinish_ETC___d685)
$finish(32'd0);
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_doFinishAlu_1_set &&
NOT_m_csr_61_BIT_12_62_EQ_setExecuted_doFinish_ETC___d689)
NOT_m_csr_63_BIT_12_64_EQ_setExecuted_doFinish_ETC___d693)
$fdisplay(32'h80000002, "\n%m: ASSERT FAIL!!");
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_doFinishAlu_1_set &&
NOT_m_csr_61_BIT_12_62_EQ_setExecuted_doFinish_ETC___d689)
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 212, column 60\ncsr valid should match");
NOT_m_csr_63_BIT_12_64_EQ_setExecuted_doFinish_ETC___d693)
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 225, column 60\ncsr valid should match");
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_doFinishAlu_1_set &&
NOT_m_csr_61_BIT_12_62_EQ_setExecuted_doFinish_ETC___d689)
NOT_m_csr_63_BIT_12_64_EQ_setExecuted_doFinish_ETC___d693)
$finish(32'd0);
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_deqLSQ &&
m_trap_dummy2_0_read__38_AND_m_trap_dummy2_1_r_ETC___d543)
m_trap_dummy2_0_read__41_AND_m_trap_dummy2_1_r_ETC___d546)
$fdisplay(32'h80000002, "\n%m: ASSERT FAIL!!");
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_deqLSQ &&
m_trap_dummy2_0_read__38_AND_m_trap_dummy2_1_r_ETC___d543)
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 326, column 52\ncannot have trap");
m_trap_dummy2_0_read__41_AND_m_trap_dummy2_1_r_ETC___d546)
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 349, column 52\ncannot have trap");
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_deqLSQ &&
m_trap_dummy2_0_read__38_AND_m_trap_dummy2_1_r_ETC___d543)
m_trap_dummy2_0_read__41_AND_m_trap_dummy2_1_r_ETC___d546)
$finish(32'd0);
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_doFinishMem &&
@@ -1707,7 +1747,7 @@ module mkRobRowSynth(CLK,
if (EN_setExecuted_doFinishMem &&
setExecuted_doFinishMem_access_at_commit &&
setExecuted_doFinishMem_non_mmio_st_done)
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 239, column 18\ncannot both be true");
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 253, column 18\ncannot both be true");
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_doFinishMem &&
setExecuted_doFinishMem_access_at_commit &&
@@ -1722,7 +1762,7 @@ module mkRobRowSynth(CLK,
if (EN_setExecuted_doFinishMem &&
setExecuted_doFinishMem_non_mmio_st_done &&
m_iType != 5'd5)
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 243, column 35\nmust be St");
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 257, column 35\nmust be St");
if (RST_N != `BSV_RESET_VALUE)
if (EN_setExecuted_doFinishMem &&
setExecuted_doFinishMem_non_mmio_st_done &&
@@ -1733,7 +1773,7 @@ module mkRobRowSynth(CLK,
$fdisplay(32'h80000002, "\n%m: ASSERT FAIL!!");
if (RST_N != `BSV_RESET_VALUE)
if (EN_write_enq && write_enq_x[18])
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 288, column 40\nld killed must be false");
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 310, column 40\nld killed must be false");
if (RST_N != `BSV_RESET_VALUE)
if (EN_write_enq && write_enq_x[18]) $finish(32'd0);
if (RST_N != `BSV_RESET_VALUE)
@@ -1741,7 +1781,7 @@ module mkRobRowSynth(CLK,
$fdisplay(32'h80000002, "\n%m: ASSERT FAIL!!");
if (RST_N != `BSV_RESET_VALUE)
if (EN_write_enq && write_enq_x[15])
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 289, column 48\nmem access at commit must be false");
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 311, column 48\nmem access at commit must be false");
if (RST_N != `BSV_RESET_VALUE)
if (EN_write_enq && write_enq_x[15]) $finish(32'd0);
if (RST_N != `BSV_RESET_VALUE)
@@ -1749,7 +1789,7 @@ module mkRobRowSynth(CLK,
$fdisplay(32'h80000002, "\n%m: ASSERT FAIL!!");
if (RST_N != `BSV_RESET_VALUE)
if (EN_write_enq && write_enq_x[14])
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 290, column 42\nlsq notified must be false");
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 312, column 42\nlsq notified must be false");
if (RST_N != `BSV_RESET_VALUE)
if (EN_write_enq && write_enq_x[14]) $finish(32'd0);
if (RST_N != `BSV_RESET_VALUE)
@@ -1757,7 +1797,7 @@ module mkRobRowSynth(CLK,
$fdisplay(32'h80000002, "\n%m: ASSERT FAIL!!");
if (RST_N != `BSV_RESET_VALUE)
if (EN_write_enq && write_enq_x[13])
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 291, column 36\nnon mmio st must be false");
$display("Dynamic assertion failed: \"../../src_Core/RISCY_OOO/procs/lib/ReorderBuffer.bsv\", line 313, column 36\nnon mmio st must be false");
if (RST_N != `BSV_RESET_VALUE)
if (EN_write_enq && write_enq_x[13]) $finish(32'd0);
end

File diff suppressed because it is too large Load Diff

View File

@@ -392,6 +392,9 @@ module mkCore#(CoreId coreId)(Core);
method csrf_rd = csrf.rd;
method rob_getPC = rob.getOrigPC[valueof(AluExeNum)].get; // last getPC port
method rob_setExecuted_doFinishMem = rob.setExecuted_doFinishMem;
`ifdef INCLUDE_TANDEM_VERIF
method rob_setExecuted_doFinishMem_RegData = rob.setExecuted_doFinishMem_RegData;
`endif
method rob_setExecuted_deqLSQ = rob.setExecuted_deqLSQ;
method isMMIOAddr = mmio.isMMIOAddr;
method mmioReq = mmio.dataReq;

View File

@@ -84,6 +84,9 @@ interface CsrFile;
method Bool fpuInstNeedWr(Bit#(5) fflags, Bool fpu_dirty);
method Action fpuInstWr(Bit#(5) fflags); // FPU must become dirty
// The WARL transform performed during CSRRx writes to a CSR
method Data warl_xform (CSR csr, Data x);
// Methods for handling traps
method Maybe#(Interrupt) pending_interrupt;
method ActionValue#(Trap_Updates) trap(Trap t, Addr pc, Addr faultAddr);
@@ -443,15 +446,15 @@ module mkCsrFile #(Data hartid)(CsrFile);
Vector#(4, Reg#(Bit#(1))) external_int_pend_vec = replicate(readOnlyReg(0));
external_int_pend_vec[prvU] <- mkCsrReg(0);
external_int_pend_vec[prvS] <- mkCsrReg(0);
external_int_pend_vec[prvM] <- mkCsrReg(0);
external_int_pend_vec[prvM] <- mkCsrReg(0); // TODO: bug (writeable by CSRRx)?
Vector#(4, Reg#(Bit#(1))) timer_int_pend_vec = replicate(readOnlyReg(0));
timer_int_pend_vec[prvU] <- mkCsrReg(0);
timer_int_pend_vec[prvS] <- mkCsrReg(0);
timer_int_pend_vec[prvM] <- mkCsrReg(0);
timer_int_pend_vec[prvM] <- mkCsrReg(0); // TODO: bug (writeable by CSRRx)?
Vector#(4, Reg#(Bit#(1))) software_int_pend_vec = replicate(readOnlyReg(0));
software_int_pend_vec[prvU] <- mkCsrReg(0);
software_int_pend_vec[prvS] <- mkCsrReg(0);
software_int_pend_vec[prvM] <- mkCsrReg(0);
software_int_pend_vec[prvM] <- mkCsrReg(0); // TODO: bug (writeable by CSRRx)?
Reg#(Data) mip_csr = concatReg13(
readOnlyReg(52'b0),
external_int_pend_vec[prvM], readOnlyReg(1'b0),
@@ -609,7 +612,7 @@ module mkCsrFile #(Data hartid)(CsrFile);
1'h0, // [11] stepie
1'h0, // [10] stopcount
1'h0, // [9] stoptime
3'h0, // [8:7] cause // WARNING: 0 is non-standard
3'h0, // [8:6] cause // WARNING: 0 is non-standard
1'h0, // [5] reserved
1'h1, // [4] mprven
1'h0, // [3] nmip // non-maskable interrupt pending
@@ -741,6 +744,83 @@ module mkCsrFile #(Data hartid)(CsrFile);
endcase);
endfunction
// ================================================================
// This function is the WARL (Write Any Read Legal) transform
// performed during CSR writes. Currently it duplicates the logic
// in the _write method of CSRs; ideally this function should be
// separate from the _write method, which should remain as an
// ordinary _write. The WARL'd value is needed for Tandem
// Verification.
function Data fv_warl_xform (CSR csr, Data x);
Asid x_asid = truncate (x [59:44]);
Bit #(16) asid = zeroExtend (x_asid);
return (
case (csr)
// Machine CSRs
CSRmisa: {getXLBits, 36'b0, getExtensionBits(isa)};
CSRmvendorid: 0;
CSRmarchid: 0;
CSRmimpid: 0;
CSRmhartid: hartid;
CSRmstatus: fn_mstatus_val (getXLBits, // sxl
getXLBits, // uxl
x [22], // tsr
x [21], // tw
x [20], // tvm
x [19], // mxr
x [18], // sum
x [17], // mprv
2'b0, // xs
((isa.f || isa.d) ? x [14:13] : 2'b0), // fs
x [12:11], // mpp
x [8], // spp
x [7], // prev_ie_vec[prvM]
x [5], // prev_ie_vec[prvS]
x [4], // prev_ie_vec[prvU]
x [3], // ie_vec[prvM]
x [1], // ie_vec[prvS]
x [0]); // ie_vec[prvU]
CSRmtvec: { x[63:2], 1'b0, x[0]};
CSRmedeleg: { 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]};
CSRmie: { 52'b0, x[11], 1'b0, x[9:8], x[7], 1'b0, x[5:4], x[3], 1'b0, x[1:0]};
CSRmcounteren: { 61'b0, x[2:0]};
CSRmcause: { x[63], 59'b0, x[3:0] };
// Supervisor level CSRs
CSRsstatus: fn_sstatus_val (getXLBits, // uxl
x [19], // mxr
x [18], // sum
2'b0, // xs
((isa.f || isa.d) ? x [14:13] : 2'b0), // fs
x [8], // spp
x [5], // prev_ie_vec[prvS]
x [4], // prev_ie_vec[prvU]
x [1], // ie_vec[prvS]
x [0]); // ie_vec[prvU]
CSRstvec: { x[63:2], 1'b0, x[0]};
CSRsip: { 52'b0, 2'b0, x[9:8], 2'b0, x[5:4], 2'b0, x[1:0]};
CSRsie: { 52'b0, 2'b0, x[9:8], 2'b0, x[5:4], 2'b0, x[1:0]};
CSRscounteren: { 61'b0, x[2:0]};
CSRscause: { x[63], 59'b0, x[3:0] };
CSRsatp: { x[63], 3'b0, asid, x [43:0] };
// User level CSRs
CSRfflags: { 59'b0, x [4:0] };
CSRfrm: { 61'b0, x [2:0] };
CSRfcsr: { 56'b0, x [7:0] };
`ifdef INCLUDE_GDB_CONTROL
// Debug Mode CSRs
CSRdcsr: { 32'b0, x[31:28], 12'b0, x[14], 1'b0, x[13:6], 1'b0, x[4:0] };
`endif
default: x;
endcase);
endfunction
// ================================================================
// INTERFACE
@@ -772,6 +852,10 @@ module mkCsrFile #(Data hartid)(CsrFile);
fflags_reg <= fflags_reg | fflags;
endmethod
method Data warl_xform (CSR csr, Data x);
return fv_warl_xform (csr, x);
endmethod
method Maybe#(Interrupt) pending_interrupt;
// first get all the pending interrupts
Bit#(InterruptNum) pend_ints = truncate(mie_csr & mip_csr);
@@ -865,11 +949,14 @@ module mkCsrFile #(Data hartid)(CsrFile);
/* ie_vec [prvS] */ 0,
ie_vec [prvU]);
Data scause_val = fn_scause_val (cause_interrupt, cause_code);
return Trap_Updates {new_pc: getNextPc(stvec_mode_low_reg, stvec_base_hi_reg),
prv: prvS,
return Trap_Updates {new_pc: getNextPc(stvec_mode_low_reg, stvec_base_hi_reg)
`ifdef INCLUDE_TANDEM_VERIF
, prv: prvS,
status: sstatus_val,
cause: scause_val,
epc: pc};
epc: pc
`endif
};
end
else begin
// ie/prv stack
@@ -896,11 +983,14 @@ module mkCsrFile #(Data hartid)(CsrFile);
ie_vec [prvS],
ie_vec [prvU]);
Data mcause_val = fn_mcause_val (cause_interrupt, cause_code);
return Trap_Updates {new_pc: getNextPc(mtvec_mode_low_reg, mtvec_base_hi_reg),
prv: prvM,
return Trap_Updates {new_pc: getNextPc(mtvec_mode_low_reg, mtvec_base_hi_reg)
`ifdef INCLUDE_TANDEM_VERIF
, prv: prvM,
status: mstatus_val,
cause: mcause_val,
epc: pc};
epc: pc
`endif
};
end
// XXX yield load reservation should be done outside this method
endmethod
@@ -923,9 +1013,12 @@ module mkCsrFile #(Data hartid)(CsrFile);
/* ie_vec [prvM] */ prev_ie_vec[prvM],
ie_vec [prvS],
ie_vec [prvU]);
return RET_Updates {new_pc: mepc_csr,
prv: prev_prv_vec[prvM],
status: mstatus_val};
return RET_Updates {new_pc: mepc_csr
`ifdef INCLUDE_TANDEM_VERIF
, prv: prev_prv_vec[prvM],
status: mstatus_val
`endif
};
endmethod
method ActionValue#(RET_Updates) sret;
@@ -942,9 +1035,12 @@ module mkCsrFile #(Data hartid)(CsrFile);
prev_ie_vec [prvU],
/* ie_vec [prvS] */ prev_ie_vec[prvS],
ie_vec [prvU]);
return RET_Updates {new_pc: sepc_csr,
prv: prev_prv_vec[prvS],
status: sstatus_val};
return RET_Updates {new_pc: sepc_csr
`ifdef INCLUDE_TANDEM_VERIF
, prv: prev_prv_vec[prvS],
status: sstatus_val
`endif
};
endmethod
method VMInfo vmI;

View File

@@ -127,7 +127,7 @@ module mkTrace_Data2_to_Trace_Data (Trace_Data2_to_Trace_Data_IFC);
isize,
td2.orig_inst,
gpr_rd,
td2.dst_data, // rd_val // TODO: setup in Mem pipeline
td2.dst_data, // rd_val
eaddr);
else if (td2.ppc_vaddr_csrData matches tagged VAddr .eaddr

View File

@@ -705,6 +705,12 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
doAssert(False, "must have csr data");
end
csrf.csrInstWr(csr_idx, csr_data);
`ifdef INCLUDE_TANDEM_VERIF
Data data_warl_xformed = csrf.warl_xform (csr_idx, csr_data);
x.ppc_vaddr_csrData = tagged CSRData data_warl_xformed;
`endif
// check if satp is modified or not
write_satp = csr_idx == CSRsatp;
`ifdef SECURITY

View File

@@ -50,6 +50,8 @@ import L1CoCache::*;
import Bypass::*;
import LatencyTimer::*;
import Cur_Cycle :: *;
typedef struct {
// inst info
MemFunc mem_func;
@@ -145,6 +147,9 @@ interface MemExeInput;
// ROB
method Addr rob_getPC(InstTag t);
method Action rob_setExecuted_doFinishMem(InstTag t, Addr vaddr, Bool access_at_commit, Bool non_mmio_st_done);
`ifdef INCLUDE_TANDEM_VERIF
method Action rob_setExecuted_doFinishMem_RegData (InstTag t, Data dst_data);
`endif
method Action rob_setExecuted_deqLSQ(InstTag t, Maybe#(Exception) cause, Maybe#(LdKilledBy) ld_killed);
// MMIO
method Bool isMMIOAddr(Addr a);
@@ -629,6 +634,11 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline);
if(verbose) $display(rule_name, " ", fshow(tag), "; ", fshow(data), "; ", fshow(res));
if(res.dst matches tagged Valid .dst) begin
inIfc.writeRegFile(dst.indx, res.data);
`ifdef INCLUDE_TANDEM_VERIF
inIfc.rob_setExecuted_doFinishMem_RegData (res.instTag, res.data);
`endif
`ifdef PERF_COUNT
// perf: load to use latency
let lat <- ldToUseLatTimer.done(tag);
@@ -766,6 +776,9 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline);
if(lsqDeqLd.dst matches tagged Valid .dst) begin
inIfc.writeRegFile(dst.indx, resp);
inIfc.setRegReadyAggr_mem(dst.indx);
`ifdef INCLUDE_TANDEM_VERIF
inIfc.rob_setExecuted_doFinishMem_RegData (lsqDeqLd.instTag, resp);
`endif
end
inIfc.rob_setExecuted_deqLSQ(lsqDeqLd.instTag, Invalid, Invalid);
if(verbose) $display("[doDeqLdQ_Lr_deq] ", fshow(lsqDeqLd), "; ", fshow(d), "; ", fshow(resp));
@@ -841,6 +854,9 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline);
if(lsqDeqLd.dst matches tagged Valid .dst) begin
inIfc.writeRegFile(dst.indx, resp);
inIfc.setRegReadyAggr_mem(dst.indx);
`ifdef INCLUDE_TANDEM_VERIF
inIfc.rob_setExecuted_doFinishMem_RegData (lsqDeqLd.instTag, resp);
`endif
end
inIfc.rob_setExecuted_deqLSQ(lsqDeqLd.instTag, Invalid, Invalid);
if(verbose) $display("[doDeqLdQ_MMIO_deq] ", fshow(lsqDeqLd), "; ", fshow(d), "; ", fshow(resp));
@@ -1061,6 +1077,9 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline);
if(lsqDeqSt.dst matches tagged Valid .dst) begin
inIfc.writeRegFile(dst.indx, resp);
inIfc.setRegReadyAggr_mem(dst.indx);
`ifdef INCLUDE_TANDEM_VERIF
inIfc.rob_setExecuted_doFinishMem_RegData (lsqDeqSt.instTag, resp);
`endif
end
inIfc.rob_setExecuted_deqLSQ(lsqDeqSt.instTag, Invalid, Invalid);
if(verbose) $display("[doDeqStQ_ScAmo_deq] ", fshow(lsqDeqSt), "; ", fshow(resp));
@@ -1157,6 +1176,9 @@ module mkMemExePipeline#(MemExeInput inIfc)(MemExePipeline);
if(lsqDeqSt.dst matches tagged Valid .dst) begin
inIfc.writeRegFile(dst.indx, resp);
inIfc.setRegReadyAggr_mem(dst.indx);
`ifdef INCLUDE_TANDEM_VERIF
inIfc.rob_setExecuted_doFinishMem_RegData (lsqDeqSt.instTag, resp);
`endif
end
inIfc.rob_setExecuted_deqLSQ(lsqDeqSt.instTag, Invalid, Invalid);
if(verbose) $display("[doDeqStQ_MMIO_deq] ", fshow(lsqDeqSt), "; ", fshow(resp));

View File

@@ -109,6 +109,12 @@ interface ReorderBufferRowEhr#(numeric type aluExeNum, numeric type fpuMulDivExe
// perform), and non-MMIO St can become Executed (NOTE faulting
// instructions are not Executed, they are set at deqLSQ time)
method Action setExecuted_doFinishMem(Addr vaddr, Bool access_at_commit, Bool non_mmio_st_done);
`ifdef INCLUDE_TANDEM_VERIF
// Used after a Ld, Lr, Sc, Amo to record reg data
method Action setExecuted_doFinishMem_RegData (Data dst_data);
`endif
`ifdef INORDER_CORE
// in-order core sets LSQ tag after getting out of issue queue
method Action setLSQTag(LdStQTag t, Bool isFence);
@@ -258,6 +264,13 @@ module mkReorderBufferRowEhr(ReorderBufferRowEhr#(aluExeNum, fpuMulDivExeNum)) p
nonMMIOStDone[nonMMIOSt_finishMem_port] <= non_mmio_st_done;
endmethod
`ifdef INCLUDE_TANDEM_VERIF
// Used after a Ld, Lr, Sc, Amo to record reg data
method Action setExecuted_doFinishMem_RegData (Data dst_data);
rg_dst_data <= dst_data;
endmethod
`endif
`ifdef INORDER_CORE
method Action setLSQTag(LdStQTag t, Bool isFence);
lsqTag <= t;
@@ -427,6 +440,12 @@ interface SupReorderBuffer#(numeric type aluExeNum, numeric type fpuMulDivExeNum
interface Vector#(fpuMulDivExeNum, ROB_setExecuted_doFinishFpuMulDiv) setExecuted_doFinishFpuMulDiv;
// doFinishMem, after addr translation
method Action setExecuted_doFinishMem(InstTag x, Addr vaddr, Bool access_at_commit, Bool non_mmio_st_done);
`ifdef INCLUDE_TANDEM_VERIF
// Used after a Ld, Lr, Sc, Amo to record reg data
method Action setExecuted_doFinishMem_RegData (InstTag x, Data dst_data);
`endif
`ifdef INORDER_CORE
// in-order core sets LSQ tag after getting out of issue queue
method Action setLSQTag(InstTag x, LdStQTag t, Bool isFence);
@@ -997,6 +1016,13 @@ module mkSupReorderBuffer#(
row[x.way][x.ptr].setExecuted_doFinishMem(vaddr, access_at_commit, non_mmio_st_done);
endmethod
`ifdef INCLUDE_TANDEM_VERIF
// Used after a Ld, Lr, Sc, Amo to record reg data
method Action setExecuted_doFinishMem_RegData (InstTag x, Data dst_data);
row[x.way][x.ptr].setExecuted_doFinishMem_RegData (dst_data);
endmethod
`endif
`ifdef INORDER_CORE
method Action setLSQTag(InstTag x, LdStQTag t, Bool isFence);
row[x.way][x.ptr].setLSQTag(t, isFence);

View File

@@ -280,6 +280,9 @@ typedef struct {
typedef struct {
Bool wrongPath;
Maybe#(PhyDst) dst;
`ifdef INCLUDE_TANDEM_VERIF
InstTag instTag; // For recording Ld data in ROB
`endif
Data data;
} LSQRespLdResult deriving(Bits, Eq, FShow);
@@ -1974,6 +1977,9 @@ module mkSplitLSQ(SplitLSQ);
let res = LSQRespLdResult {
wrongPath: False,
dst: Invalid,
`ifdef INCLUDE_TANDEM_VERIF
instTag: ld_instTag [t], // For recording Ld data in ROB
`endif
data: ?
};
if(ld_waitWPResp_resp[t]) begin