138 lines
4.7 KiB
Plaintext
138 lines
4.7 KiB
Plaintext
/*-
|
|
* Copyright (c) 2018 Jack Deeley
|
|
* Copyright (c) 2018-2019 Peter Rugg
|
|
* All rights reserved.
|
|
*
|
|
* This software was developed by SRI International and the University of
|
|
* Cambridge Computer Laboratory (Department of Computer Science and
|
|
* Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
|
|
* DARPA SSITH research programme.
|
|
*
|
|
* @BERI_LICENSE_HEADER_START@
|
|
*
|
|
* Licensed to BERI Open Systems C.I.C. (BERI) under one or more contributor
|
|
* license agreements. See the NOTICE file distributed with this work for
|
|
* additional information regarding copyright ownership. BERI licenses this
|
|
* file to you under the BERI Hardware-Software License, Version 1.0 (the
|
|
* "License"); you may not use this file except in compliance with the
|
|
* License. You may obtain a copy of the License at:
|
|
*
|
|
* http://www.beri-open-systems.org/legal/license-1-0.txt
|
|
*
|
|
* Unless required by applicable law or agreed to in writing, Work distributed
|
|
* under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR
|
|
* CONDITIONS OF ANY KIND, either express or implied. See the License for the
|
|
* specific language governing permissions and limitations under the License.
|
|
*
|
|
* @BERI_LICENSE_HEADER_END@
|
|
*/
|
|
|
|
package Verifier;
|
|
|
|
import RVFI_DII :: *;
|
|
import ISA_Decls :: *;
|
|
import CPU_Globals :: *;
|
|
`ifdef ISA_CHERI
|
|
import CHERICap :: *;
|
|
import CHERICC_Fat :: *;
|
|
`endif
|
|
|
|
`ifdef RVFI
|
|
// This function relies on info that is only passed in RVFI-mode.
|
|
|
|
Bit#(32) ecall_insn = 32'h73;
|
|
|
|
function RVFI_DII_Execution #(XLEN,MEMWIDTH) getRVFIInfoCondensed(
|
|
// Using the full data gives us access to rd_valid and a few other fields.
|
|
Data_Stage2_to_Stage3 data_s2_s3,
|
|
WordXL trapPC,
|
|
Bit#(64) order,
|
|
Bool isTrap,
|
|
Exc_Code exc,
|
|
Bool handler,
|
|
Bool halted
|
|
);
|
|
|
|
Data_RVFI_Stage2 s2 = data_s2_s3.info_RVFI_s2;
|
|
Data_RVFI_Stage1 s1 = s2.stage1;
|
|
|
|
return RVFI_DII_Execution {
|
|
rvfi_order: order,
|
|
// Not all traps are relevant in the Clifford-RVFI framework, e.g. page faults.
|
|
rvfi_trap: isTrap,
|
|
rvfi_halt: (halted) ? True : (data_s2_s3.instr == ecall_insn),
|
|
rvfi_intr: handler,
|
|
rvfi_insn: data_s2_s3.instr,
|
|
rvfi_rs1_addr: s1.rs1_addr,
|
|
rvfi_rs2_addr: s1.rs2_addr,
|
|
rvfi_rd_addr: data_s2_s3.rd_valid ? data_s2_s3.rd : 0,
|
|
rvfi_rs1_data: s1.rs1_data,
|
|
rvfi_rs2_data: s1.rs2_data,
|
|
`ifdef ISA_CHERI
|
|
rvfi_rd_wdata: data_s2_s3.rd == 0 ? 0 : getAddr(data_s2_s3.rd_val),
|
|
`else
|
|
rvfi_rd_wdata: data_s2_s3.rd == 0 ? 0 : data_s2_s3.rd_val,
|
|
`endif
|
|
rvfi_pc_rdata: data_s2_s3.pc,
|
|
rvfi_pc_wdata: isTrap ? trapPC : s1.pc_wdata,
|
|
rvfi_mem_wdata: s1.mem_wdata,
|
|
rvfi_mem_addr: s1.mem_addr,
|
|
rvfi_mem_rmask: s2.mem_rmask,
|
|
rvfi_mem_wmask: s2.mem_wmask,
|
|
`ifdef ISA_CHERI
|
|
rvfi_mem_rdata: getAddr(data_s2_s3.rd_val)
|
|
`else
|
|
rvfi_mem_rdata: data_s2_s3.rd_val
|
|
`endif
|
|
};
|
|
endfunction : getRVFIInfoCondensed
|
|
|
|
|
|
|
|
function RVFI_DII_Execution #(XLEN,MEMWIDTH) getRVFIInfoS1 (
|
|
Data_Stage1_to_Stage2 data_s1_s2,
|
|
WordXL next_pc,
|
|
Bit#(64) order,
|
|
Bool isTrap,
|
|
Exc_Code exc,
|
|
Bool handler,
|
|
Bool halted
|
|
);
|
|
|
|
Data_RVFI_Stage1 s1 = data_s1_s2.info_RVFI_s1;
|
|
|
|
return RVFI_DII_Execution {
|
|
rvfi_order: order,
|
|
rvfi_trap: isTrap,
|
|
rvfi_halt: (halted) ? True : (data_s1_s2.instr == ecall_insn),
|
|
rvfi_intr: handler,
|
|
rvfi_insn: data_s1_s2.instr,
|
|
rvfi_rs1_addr: s1.rs1_addr,
|
|
rvfi_rs2_addr: s1.rs2_addr,
|
|
rvfi_rs1_data: s1.rs1_data,
|
|
rvfi_rs2_data: s1.rs2_data,
|
|
rvfi_pc_rdata: data_s1_s2.pc,
|
|
rvfi_pc_wdata: isTrap ? next_pc : s1.pc_wdata,
|
|
rvfi_mem_addr: s1.mem_addr,
|
|
// Although we know what rd *would* be, the fact that we're using this function
|
|
// means we can't have actually written to it.
|
|
rvfi_rd_addr: 0,
|
|
rvfi_rd_wdata: 0,
|
|
rvfi_mem_rmask: 0,
|
|
rvfi_mem_wmask: 0,
|
|
rvfi_mem_wdata: 0,
|
|
rvfi_mem_rdata: 0
|
|
};
|
|
endfunction : getRVFIInfoS1
|
|
|
|
function Bit #(TDiv#(MEMWIDTH,8)) getMemMask(Bit #(3) width_code, Bit #(XLEN) addr);
|
|
Bit #(5) width = 5'b1 << width_code;
|
|
Bit #(TDiv#(MEMWIDTH,8)) result = truncate((9'b1 << width) - 9'b1);
|
|
return result;
|
|
endfunction : getMemMask
|
|
|
|
`endif
|
|
|
|
endpackage
|
|
|