Numerous fixes, so now generating correct Tandem-Verification traces for all 229 ISA tests.

This commit is contained in:
rsnikhil
2020-02-14 15:37:20 -05:00
parent 8434df2dac
commit 0264984136
31 changed files with 66046 additions and 63814 deletions

View File

@@ -84,13 +84,20 @@ interface CsrFile;
// normal write by FPU inst to FPU CSR
method Bool fpuInstNeedWr(Bit#(5) fflags, Bool fpu_dirty);
method Action fpuInstWr(Bit#(5) fflags); // FPU must become dirty
`ifdef INCLUDE_TANDEM_VERIF
// Returns new fcsr and mstatus (pure function)
method Tuple2 #(Bit #(5), Data) fpuInst_csr_updates (Bit #(5) fflags,
Bool init_for_way0,
Bit #(5) old_fflags,
Data old_mstatus);
`endif
// 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);
method ActionValue#(Trap_Updates) trap(Trap t, Addr pc, Addr faultAddr, Bit #(32) orig_inst);
method ActionValue#(RET_Updates) sret;
method ActionValue#(RET_Updates) mret;
@@ -602,6 +609,18 @@ module mkCsrFile #(Data hartid)(CsrFile);
StatsCsr stats_module <- mkStatsCsr;
Reg#(Data) stats_csr = stats_module.reg_ifc;
Reg #(Data) rg_tselect <- mkConfigReg (0);
// Note: ISA test rv64mi-p-breakpoint assumes tdata1's reset value == 0
// Until we implement trigger functionality,
// force 'tdata1.type' field ([xlen-1:xlen-4]) to zero
// meaning: 'There is no trigger at this tselect'
Reg #(Bit #(4)) rg_tdata1_type <- mkReadOnlyReg (0);
Reg #(Bit #(1)) rg_tdata1_dmode <- mkCsrReg (0);
Reg #(Bit #(59)) rg_tdata1_data <- mkCsrReg (0);
Reg #(Data) rg_tdata1 = concatReg3 (rg_tdata1_type, rg_tdata1_dmode, rg_tdata1_data);
Reg #(Data) rg_tdata2 <- mkConfigRegU;
Reg #(Data) rg_tdata3 <- mkConfigRegU;
`ifdef INCLUDE_GDB_CONTROL
// DCSR is 32b even in RV64
Bit #(32) dcsr_reset_value = {4'h4, // [31:28] xdebugver
@@ -734,6 +753,11 @@ module mkCsrFile #(Data hartid)(CsrFile);
CSRtrng: trng_csr;
`endif
CSRtselect: rg_tselect;
CSRtdata1: rg_tdata1;
CSRtdata2: rg_tdata2;
CSRtdata3: rg_tdata3;
`ifdef INCLUDE_GDB_CONTROL
CSRdcsr: rg_dcsr; // TODO: take NMI into account (cf. Piccolo/Flute)
CSRdpc: rg_dpc;
@@ -790,6 +814,8 @@ module mkCsrFile #(Data hartid)(CsrFile);
CSRmcounteren: { 61'b0, x[2:0]};
CSRmcause: { x[63], 59'b0, x[3:0] };
CSRtdata1: { 4'b0, x [59:0] }; // Force tdata.type == 0 ("no trigger at this tselect")
// Supervisor level CSRs
CSRsstatus: fn_sstatus_val (getXLBits, // uxl
x [19], // mxr
@@ -853,6 +879,27 @@ module mkCsrFile #(Data hartid)(CsrFile);
fflags_reg <= fflags_reg | fflags;
endmethod
`ifdef INCLUDE_TANDEM_VERIF
method Tuple2 #(Bit #(5), Data) fpuInst_csr_updates (Bit #(5) fflags,
Bool init_for_way0,
Bit #(5) old_fflags,
Data old_mstatus);
// Note: old_fflags and old_mstatus are accumulated in
// sequential program order, and so may differ from fflags_reg
// 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) new_fflags = (old_fflags | fflags);
Data new_mstatus = { old_mstatus [63:15], 2'b11, old_mstatus [12:0] };
return tuple2 (new_fflags, new_mstatus);
endmethod
`endif
method Data warl_xform (CSR csr, Data x);
return fv_warl_xform (csr, x);
endmethod
@@ -886,7 +933,7 @@ module mkCsrFile #(Data hartid)(CsrFile);
end
endmethod
method ActionValue#(Trap_Updates) trap(Trap t, Addr pc, Addr addr);
method ActionValue#(Trap_Updates) trap(Trap t, Addr pc, Addr addr, Bit #(32) orig_inst);
// figure out trap cause & trap val
Bit#(1) cause_interrupt = 0;
Bit#(4) cause_code = 0;
@@ -895,6 +942,7 @@ module mkCsrFile #(Data hartid)(CsrFile);
tagged Exception .e: begin
cause_code = pack(e);
trap_val = (case(e)
IllegalInst: zeroExtend (orig_inst);
InstAddrMisaligned, Breakpoint: return pc;
InstAccessFault, InstPageFault,

View File

@@ -126,6 +126,17 @@ module mkTrace_Data2_to_Trace_Data (Trace_Data2_to_Trace_Data_IFC);
td2.fflags,
td2.mstatus); // [FX] updated
else if (td2.ppc_vaddr_csrData matches tagged VAddr .eaddr
&&& td2.dst matches tagged Valid (tagged Fpu .fpr_rd)
&&& (td2.iType == Ld))
td = mkTrace_F_LOAD (fall_thru_PC,
isize,
td2.orig_inst,
fpr_rd,
td2.dst_data, // rd_val
eaddr,
td2.mstatus);
else if (td2.ppc_vaddr_csrData matches tagged VAddr .eaddr
&&& (td2.iType == Ld))
td = mkTrace_I_LOAD (fall_thru_PC,

View File

@@ -141,6 +141,7 @@ typedef struct {
Addr pc;
Addr addr;
Trap trap;
Bit #(32) orig_inst;
} CommitTrap deriving(Bits, Eq, FShow);
`ifdef INCLUDE_GDB_CONTROL
@@ -174,17 +175,20 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
`ifdef INCLUDE_TANDEM_VERIF
Integer way0 = 0;
ToReorderBuffer no_deq_data = ?;
Bit #(5) no_fflags = ?;
Data no_mstatus = ?;
Maybe #(Trap_Updates) no_trap_updates = tagged Invalid;
Maybe #(RET_Updates) no_ret_updates = tagged Invalid;
function Action fa_to_TV (Integer way,
Bit #(64) serial_num,
ToReorderBuffer deq_data,
Bit #(5) fflags,
Data mstatus,
Maybe #(Trap_Updates) m_trap_updates,
Maybe #(RET_Updates) m_ret_updates);
action
CsrFile csrf = inIfc.csrfIfc;
let mstatus = csrf.rd (CSRmstatus);
let tval = (m_trap_updates matches tagged Valid .tu ? tu.tval : deq_data.tval);
let upd_pc = (m_ret_updates matches tagged Valid .ru ? ru.new_pc : deq_data.pc);
let x = Trace_Data2 {serial_num: serial_num,
@@ -199,7 +203,7 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
trap: deq_data.trap,
tval: tval,
ppc_vaddr_csrData: deq_data.ppc_vaddr_csrData,
fflags: deq_data.fflags,
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
@@ -226,7 +230,7 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
rule rl_send_tv_reset (rg_just_after_reset);
Bit #(64) serial_num = 0;
fa_to_TV (way0, serial_num, ?, no_trap_updates, no_ret_updates);
fa_to_TV (way0, serial_num, no_deq_data, no_fflags, no_mstatus, no_trap_updates, no_ret_updates);
rg_just_after_reset <= False;
rg_serial_num <= 1;
endrule
@@ -510,7 +514,8 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
let commitTrap_val = Valid (CommitTrap {
trap: trap,
pc: x.pc,
addr: vaddr
addr: vaddr,
orig_inst: x.orig_inst
});
commitTrap <= commitTrap_val;
`ifdef INCLUDE_TANDEM_VERIF
@@ -615,11 +620,11 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
if (! debugger_halt) begin
// trap handling & redirect
let trap_updates <- csrf.trap(trap.trap, trap.pc, trap.addr);
let trap_updates <- csrf.trap(trap.trap, trap.pc, trap.addr, trap.orig_inst);
inIfc.redirectPc(trap_updates.new_pc);
`ifdef INCLUDE_TANDEM_VERIF
fa_to_TV (way0, rg_serial_num, x, tagged Valid trap_updates, no_ret_updates);
fa_to_TV (way0, rg_serial_num, x, no_fflags, no_mstatus, tagged Valid trap_updates, no_ret_updates);
`endif
rg_serial_num <= rg_serial_num + 1;
@@ -743,7 +748,7 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
inIfc.redirectPc(next_pc);
`ifdef INCLUDE_TANDEM_VERIF
fa_to_TV (way0, rg_serial_num, x, no_trap_updates, m_ret_updates);
fa_to_TV (way0, rg_serial_num, x, no_fflags, no_mstatus, no_trap_updates, m_ret_updates);
`endif
rg_serial_num <= rg_serial_num + 1;
@@ -856,6 +861,12 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
Bit #(64) instret = 0;
`ifdef INCLUDE_TANDEM_VERIF
// These variables accumulate fflags and mstatus in sequential Program Order ('po')
// (whereas the 'fflags' variable does just one update after superscalar retirement).
Bit #(5) po_fflags = ?;
Data po_mstatus = ?;
`endif
// compute what actions to take
for(Integer i = 0; i < valueof(SupSize); i = i+1) begin
if(!stop && rob.deqPort[i].canDeq) begin
@@ -874,8 +885,22 @@ module mkCommitStage#(CommitInput inIfc)(CommitStage);
$display("instret:%0d PC:0x%0h instr:0x%08h", rg_serial_num + instret, x.pc, x.orig_inst,
" iType:", fshow (x.iType), " [doCommitNormalInst [%0d]]", i);
end
`ifdef INCLUDE_TANDEM_VERIF
fa_to_TV (i, rg_serial_num + instret, x, no_trap_updates, no_ret_updates);
Bool init_for_way0 = (i == 0);
match {. new_fflags, .new_mstatus} = csrf.fpuInst_csr_updates (x.fflags,
init_for_way0,
po_fflags,
po_mstatus);
po_fflags = new_fflags;
po_mstatus = new_mstatus;
Bool is_fmv_x_dw = ((x.orig_inst & 32'b_1111110_11111_00000_111_00000_1111111)
== 32'b_1110000_00000_00000_000_00000_1010011);
fa_to_TV (i, rg_serial_num + instret, x,
(is_fmv_x_dw ? 5'b0 : po_fflags),
po_mstatus,
no_trap_updates, no_ret_updates);
`endif
instret = instret + 1;

View File

@@ -553,13 +553,21 @@ module mkFetchStage(FetchStage);
default: begin
// Access fault
cause = Valid (InstAccessFault);
// Without 'C' extension:
// Addr align32b_mask = 'h3;
// tval = (in.pc & (~ align32b_mask));
Addr align16b_mask = 'h1;
tval = (in.pc & (~ align16b_mask));
end
endcase
end
else begin
// TLB exception: record the request address
Addr align32b_mask = 'h3;
tval = (in.pc & (~ align32b_mask));
// Without 'C' extension:
// Addr align32b_mask = 'h3;
// tval = (in.pc & (~ align32b_mask));
Addr align16b_mask = 'h1;
tval = (in.pc & (~ align16b_mask));
end
let out = Fetch2ToFetch3 {

View File

@@ -350,6 +350,10 @@ module mkRenameStage#(RenameInput inIfc)(RenameStage);
iType: dInst.iType,
dst: arch_regs.dst,
dst_data: ?, // Available only after execution
`ifdef INCLUDE_TANDEM_VERIF
store_data: ?,
store_data_BE: ?,
`endif
csr: dInst.csr,
claimed_phy_reg: False, // no renaming is done
trap: firstTrap,
@@ -526,6 +530,10 @@ module mkRenameStage#(RenameInput inIfc)(RenameStage);
iType: dInst.iType,
dst: arch_regs.dst,
dst_data: ?, // Available only after execution
`ifdef INCLUDE_TANDEM_VERIF
store_data: ?,
store_data_BE: ?,
`endif
csr: dInst.csr,
claimed_phy_reg: True, // XXX we always claim a free reg in rename
trap: Invalid, // no trap
@@ -693,6 +701,10 @@ module mkRenameStage#(RenameInput inIfc)(RenameStage);
iType: dInst.iType,
dst: arch_regs.dst,
dst_data: ?, // Available only after execution
`ifdef INCLUDE_TANDEM_VERIF
store_data: ?,
store_data_BE: ?,
`endif
csr: dInst.csr,
claimed_phy_reg: True, // XXX we always claim a free reg in rename
trap: Invalid, // no trap
@@ -1047,6 +1059,10 @@ module mkRenameStage#(RenameInput inIfc)(RenameStage);
iType: dInst.iType,
dst: arch_regs.dst,
dst_data: ?, // Available only after execution
`ifdef INCLUDE_TANDEM_VERIF
store_data: ?,
store_data_BE: ?,
`endif
csr: dInst.csr,
claimed_phy_reg: True, // XXX we always claim a free reg in rename
trap: Invalid, // no trap

View File

@@ -270,6 +270,11 @@ typedef enum {
CSRtrng = 12'hcc0, // random number for secure boot
`endif
CSRtselect = 12'h7A0, // Debug/trace tselect
CSRtdata1 = 12'h7A1, // Debug/trace tdata1
CSRtdata2 = 12'h7A2, // Debug/trace tdata2
CSRtdata3 = 12'h7A3, // Debug/trace tdata3
`ifdef INCLUDE_GDB_CONTROL
CSRdcsr = 12'h7B0, // Debug control and status
CSRdpc = 12'h7B1, // Debug PC
@@ -334,6 +339,19 @@ function CSR unpackCSR(Bit#(12) x);
pack(CSR'(CSRmspec )): (CSRmspec );
pack(CSR'(CSRtrng )): (CSRtrng );
`endif
pack(CSR'(CSRtselect )): (CSRtselect );
pack(CSR'(CSRtdata1 )): (CSRtdata1 );
pack(CSR'(CSRtdata2 )): (CSRtdata2 );
pack(CSR'(CSRtdata3 )): (CSRtdata3 );
`ifdef INCLUDE_GDB_CONTROL
pack(CSR'(CSRdcsr )): (CSRdcsr );
pack(CSR'(CSRdpc )): (CSRdpc );
pack(CSR'(CSRdscratch0 )): (CSRdscratch0 );
pack(CSR'(CSRdscratch1 )): (CSRdscratch1 );
`endif
default : (CSRnone );
endcase);
endfunction