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

Fixed Tandem-Verification trace generation issue re. MSTATUS on CSRRx instructions that write to FCSR.

Browse Source 
When a CSRRx instruction writes to FCSR/FFLAGS/FRM, the CPU also
changes MSTATUS.FS and, by implication, MSTATUS.SD because the
floating point state has become "dirty".  Tandem Verification
trace-generation was not reporting this update.
This commit is contained in:
rsnikhil
2020-03-08 21:29:30 -04:00
parent fafd99c983
commit 976494a8ff
50 changed files with 260262 additions and 240548 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
src_Core/CPU/CsrFile.bsv
View File

@@ -902,11 +902,11 @@ module mkCsrFile #(Data hartid)(CsrFile);
// and mstatus_csr, which only change after superscalar-wide
// retirement.
old_fflags = (init_for_way0 ? fflags_reg : old_fflags);
old_mstatus = (init_for_way0 ? mstatus_csr : old_mstatus);
Bit #(5) old_fflags1 = (init_for_way0 ? fflags_reg : old_fflags);
Data old_mstatus1 = (init_for_way0 ? mstatus_csr : old_mstatus);
Bit #(5) new_fflags = (old_fflags | fflags);
Data new_mstatus = { old_mstatus [63:15], 2'b11, old_mstatus [12:0] };
Bit #(5) new_fflags = (old_fflags1 | fflags);
Data new_mstatus = { 1'b1, old_mstatus1 [62:15], 2'b11, old_mstatus1 [12:0] };
return tuple2 (new_fflags, new_mstatus);
endmethod

29
src_Core/Core/TV_Encode.bsv
View File

@@ -268,8 +268,8 @@ module mkTV_Encode (TV_Encode_IFC);
match { .n1, .vb1 } = encode_pc (td.pc);
match { .n2, .vb2 } = encode_instr (td.instr_sz, td.instr);
match { .n3, .vb3 } = encode_reg (fv_gpr_regnum (td.rd), td.word1);
match { .n4, .vb4 } = encode_reg (fv_csr_regnum (extend (csr_addr_fflags)), td.word2);
match { .n5, .vb5 } = encode_reg (fv_csr_regnum (extend (csr_addr_mstatus)), td.word4);
match { .n4, .vb4 } = encode_reg (fv_csr_regnum (csr_addr_fflags), td.word2);
match { .n5, .vb5 } = encode_reg (fv_csr_regnum (csr_addr_mstatus), td.word4);
match { .nN, .vbN } = encode_byte (te_op_end_group);
// Concatenate components into a single byte vec
@@ -294,8 +294,8 @@ module mkTV_Encode (TV_Encode_IFC);
match { .n1, .vb1 } = encode_pc (td.pc);
match { .n2, .vb2 } = encode_instr (td.instr_sz, td.instr);
match { .n3, .vb3 } = encode_fpr (fv_fpr_regnum (td.rd), td.word5);
match { .n4, .vb4 } = encode_reg (fv_csr_regnum (extend (csr_addr_fflags)), td.word2);
match { .n5, .vb5 } = encode_reg (fv_csr_regnum (extend (csr_addr_mstatus)), td.word4);
match { .n4, .vb4 } = encode_reg (fv_csr_regnum (csr_addr_fflags), td.word2);
match { .n5, .vb5 } = encode_reg (fv_csr_regnum (csr_addr_mstatus), td.word4);
match { .nN, .vbN } = encode_byte (te_op_end_group);
// Concatenate components into a single byte vec
@@ -343,7 +343,7 @@ module mkTV_Encode (TV_Encode_IFC);
match { .n2, .vb2 } = encode_instr (td.instr_sz, td.instr);
match { .n3, .vb3 } = encode_fpr (fv_fpr_regnum (td.rd), td.word5);
match { .n4, .vb4 } = encode_eaddr (truncate (td.word3));
match { .n5, .vb5 } = encode_reg (fv_csr_regnum (extend (csr_addr_mstatus)), td.word4);
match { .n5, .vb5 } = encode_reg (fv_csr_regnum (csr_addr_mstatus), td.word4);
match { .nN, .vbN } = encode_byte (te_op_end_group);
// Concatenate components into a single byte vec
@@ -446,9 +446,17 @@ module mkTV_Encode (TV_Encode_IFC);
match { .n1, .vb1 } = encode_pc (td.pc);
match { .n2, .vb2 } = encode_instr (td.instr_sz, td.instr);
match { .n3, .vb3 } = encode_reg (fv_gpr_regnum (td.rd), td.word1);
match { .n4, .vb4 } = ((td.word2 == 0)
? tuple2 (0, ?) // CSR was not written
: encode_reg (fv_csr_regnum (truncate (td.word3)), td.word4));
Bool csr_written = (td.word2 [0] == 1'b1);
match { .n4, .vb4 } = (csr_written
? encode_reg (fv_csr_regnum (truncate (td.word3)), td.word4)
: tuple2 (0, ?));
`ifdef ISA_F
// MSTATUS.FS and .SD also updated if CSR instr wrote FFLAGS, FRM or FCSR
Bool mstatus_written = (td.word2 [1] == 1'b1);
match { .n5, .vb5 } = (mstatus_written
? encode_reg (fv_csr_regnum (csr_addr_mstatus), td.word5)
: tuple2 (0, ?));
`endif
match { .nN, .vbN } = encode_byte (te_op_end_group);
// Concatenate components into a single byte vec
@@ -457,7 +465,12 @@ module mkTV_Encode (TV_Encode_IFC);
match { .nn2, .x2 } = vsubst (nn1, x1, n2, vb2);
match { .nn3, .x3 } = vsubst (nn2, x2, n3, vb3);
match { .nn4, .x4 } = vsubst (nn3, x3, n4, vb4);
`ifdef ISA_F
match { .nn5, .x5 } = vsubst (nn4, x4, n5, vb5);
match { .nnN, .xN } = vsubst (nn5, x5, nN, vbN);
`else
match { .nnN, .xN } = vsubst (nn4, x4, nN, vbN);
`endif
f_out.enq (tuple2 (nnN, xN));
endrule

5
src_Core/Core/Trace_Data2_to_Trace_Data.bsv
View File

@@ -179,7 +179,10 @@ module mkTrace_Data2_to_Trace_Data (Trace_Data2_to_Trace_Data_IFC);
td2.dst_data, // rdval
csr_valid,
csr_addr,
csr_data);
csr_data,
// For CSR writes to FFLAGS/FRM/FCSR, also changes MSTATUS
td2.will_dirty_fpu_state,
td2.mstatus);
end
else if ( (td2.iType == Mret)

15
src_Core/ISA/TV_Info.bsv
View File

@@ -301,10 +301,14 @@ function Trace_Data mkTrace_RET (WordXL pc, ISize isize, Bit #(32) instr, Priv_M
endfunction
// CSRRX
// op pc instr_sz instr rd word1 word2 word3 word4
// x x x x x rdval csrvalid csraddr csrval
// op pc instr_sz instr rd word1 word2 word3 word4 word5
// x x x x x rdval mstatus_valid csraddr csrval mstatus
// csrvalid
function Trace_Data mkTrace_CSRRX (WordXL pc, ISize isize, Bit #(32) instr,
RegName rd, WordXL rdval, Bool csrvalid, CSR_Addr csraddr, WordXL csrval);
RegName rd, WordXL rdval,
Bool csrvalid, CSR_Addr csraddr, WordXL csrval,
Bool mstatus_valid,
WordXL mstatus);
Trace_Data td = ?;
td.op = TRACE_CSRRX;
td.pc = pc;
@@ -312,9 +316,12 @@ function Trace_Data mkTrace_CSRRX (WordXL pc, ISize isize, Bit #(32) instr,
td.instr = instr;
td.rd = rd;
td.word1 = rdval;
td.word2 = (csrvalid ? 1 : 0);
td.word2 = ((mstatus_valid ? 2 : 0) | (csrvalid ? 1 : 0));
td.word3 = zeroExtend (csraddr);
td.word4 = csrval;
`ifdef ISA_F
td.word5 = mstatus;
`endif
return td;
endfunction

19
src_Core/RISCY_OOO/procs/RV64G_OOO/CommitStage.bsv
View File

@@ -207,7 +207,7 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
ppc_vaddr_csrData: deq_data.ppc_vaddr_csrData,
fflags: fflags, // deq_data.fflags only has incremental flags
will_dirty_fpu_state: deq_data.will_dirty_fpu_state,
mstatus: mstatus, // For Fpu ops, since [FX] bit changed
mstatus: mstatus, // when SD/XS/FS have changed
// Trap and RET updates
prv: ( m_trap_updates matches tagged Valid .tu
@@ -721,7 +721,11 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
// we claim a phy reg for every inst, so commit its renaming
regRenamingTable.commit[0].commit;
Bool write_satp = False; // flush tlb when satp csr is modified
`ifdef INCLUDE_TANDEM_VERIF
Data new_mstatus = no_mstatus;
`endif
Bool write_satp = False; // flush tlb when satp csr is modified
Bool flush_security = False; // flush for security when the flush csr is written
if(x.iType == Csr) begin
// notify commit of CSR (so MMIO pRq may be handled)
@@ -740,6 +744,11 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
`ifdef INCLUDE_TANDEM_VERIF
Data data_warl_xformed = csrf.warl_xform (csr_idx, csr_data);
x.ppc_vaddr_csrData = tagged CSRData data_warl_xformed;
if (x.will_dirty_fpu_state) begin
Data old_mstatus = csrf.rd (CSRmstatus);
new_mstatus = { 1'b1, old_mstatus [62:15], 2'b11, old_mstatus [12:0] };
end
`endif
// check if satp is modified or not
@@ -774,7 +783,7 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
`ifdef INCLUDE_TANDEM_VERIF
fa_to_TV (way0, rg_serial_num,
tagged Invalid,
x, no_fflags, no_mstatus, no_trap_updates, m_ret_updates);
x, no_fflags, new_mstatus, no_trap_updates, m_ret_updates);
`endif
rg_serial_num <= rg_serial_num + 1;
@@ -814,7 +823,9 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
// checks
doAssert(x.epochIncremented, "must have already incremented epoch");
doAssert((x.iType == Csr) == isValid(x.csr), "only CSR has valid csr idx");
doAssert(x.fflags == 0 && !x.will_dirty_fpu_state, "cannot dirty FPU");
// RSN 2020-03-08: Removed this assertion. Csr instrs that write to
// fflags/frm/fcsr do indeed 'dirty' the fpu state
// doAssert(x.fflags == 0 && !x.will_dirty_fpu_state, "cannot dirty FPU");
doAssert(x.spec_bits == 0, "cannot have spec bits");
doAssert(x.claimed_phy_reg, "must have claimed phy reg");
`ifdef RENAME_DEBUG

9
src_Core/RISCY_OOO/procs/RV64G_OOO/RenameStage.bsv
View File

@@ -525,6 +525,15 @@ module mkRenameStage#(RenameInput inIfc)(RenameStage);
will_dirty_fpu_state = True;
doAssert(False, "system inst never touches FP regs");
end
// CSR instrs that touch certain FP CSRs will dirty FP state.
if (dInst.csr matches tagged Valid .csr
&&& ((dInst.iType == Csr)
&& ((csr == CSRfflags) || (csr == CSRfrm) || (csr == CSRfcsr))))
begin
will_dirty_fpu_state = True;
end
RobInstState rob_inst_state = to_exec ? NotDone : Executed;
let y = ToReorderBuffer{pc: pc,
orig_inst: orig_inst,

1
src_Core/RISCY_OOO/procs/lib/Fpu.bsv
View File

@@ -1,5 +1,6 @@
// Copyright (c) 2016, 2017 Massachusetts Institute of Technology
// Portions Copyright (c) 2019-2020 Bluespec, Inc.
// Permission is hereby granted, free of charge, to any person
// obtaining a copy of this software and associated documentation