• Joined on 2020-05-28
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-29 13:35:30 +08:00
e0bc557d49 Add rvfi_pc_bwd_check
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-29 13:18:36 +08:00
226b225324 Add rvfi_liveness_check
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-29 12:55:48 +08:00
0aaf7e8d03 Resolve import issue in rvfi_insn_check.py for now
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-28 17:55:41 +08:00
0c971e96ce Update rvfi_insn_check.py
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-28 14:25:26 +08:00
032e4c254d Create template for RVFI instruction check
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-28 14:22:01 +08:00
bae6fb38bd Add rvfi_imem_check
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-28 14:04:20 +08:00
9908c603fe Add rvfi_ill_check
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-28 13:42:48 +08:00
26a0af8517 Add rvfi_hang_check
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-27 15:31:55 +08:00
0ae0e9c356 Add rvfi_dmem_check
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-27 14:37:18 +08:00
4ba5262165 Add rvfi_channel check
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-27 14:16:53 +08:00
8cb5110199 Add check for causality
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-24 13:51:15 +08:00
2421f1f6b6 Add RV32IM ISA
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-24 13:32:52 +08:00
5bce84836c Add REMU instruction for RV32M
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-24 13:30:13 +08:00
4600eaeb74 Add REM instruction for RV32M
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-24 13:27:57 +08:00
7f3f88cb69 Add DIVU instruction for RV32M
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-24 13:25:29 +08:00
2b198303c6 Add DIV instruction for RV32M
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-24 13:22:53 +08:00
f13208455d Add MULHU instruction for RV32M
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-24 13:20:15 +08:00
7a61919a88 Add MULHSU instruction for RV32M
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-24 13:16:55 +08:00
9b4f6ac359 Add MULH instruction for RV32M
dsleung pushed to master at M-Labs/riscv-formal-nmigen 2020-07-24 13:13:15 +08:00
c72205d433 Modify MUL instruction to use alternative operations