Skip to content

/ riscv-formal

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add support for optionally ignoring rmask #37

Closed
wants to merge 1 commit into from
+127 −2
Closed

Add support for optionally ignoring rmask #37

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter...
Filter file types
Jump to…
Jump to file
Failed to load files.

Always

Just for now

6 docs/config.md
View file
Open in desktop
@@ -72,6 +72,12 @@ to retire memory load/store operations for smaller units (half-words, bytes)
word aligned with the appropiate `rmask/wmask` values to select the correct
bytes. In this case the `RISCV_FORMAL_ALIGNED_MEM` macro must be defined.

RISCV_FORMAL_IGNORE_RMASK
-------------------------

This can be defined for cores that do not have read mask support for memory
accesses.

RISCV_FORMAL_BLACKBOX_REGS
--------------------------

2 docs/rvfi.md
View file
Open in desktop
@@ -83,7 +83,7 @@ When the define `RISCV_FORMAL_ALIGNED_MEM` is set, the address must have a 4-byt

`rvfi_mem_wdata` is the post-state data written to `rvfi_mem_addr`. `rvfi_mem_wmask` specifies which bytes are valid.

When `RISCV_FORMAL_ALIGNED_MEM` is set then `riscv-formal` assumes that unaligned memory access causes a trap.
When `RISCV_FORMAL_ALIGNED_MEM` is set then `riscv-formal` assumes that unaligned memory access causes a trap. Finally, when `RISCV_FORMAL_IGNORE_RMASK` is set, `rvfi_mem_rmask` has to be set to zero.

### Alternative Arithmetic Operations

24 insns/generate.py
View file
Open in desktop
@@ -488,7 +488,11 @@ def insn_l(insn, funct3, numbytes, signext, misa=0):
assign(f, "spec_rs1_addr", "insn_rs1")
assign(f, "spec_rd_addr", "insn_rd")
assign(f, "spec_mem_addr", "addr & ~(`RISCV_FORMAL_XLEN/8-1)")
print("`ifdef RISCV_FORMAL_IGNORE_RMASK", file=f)
assign(f, "spec_mem_rmask", "0")
print("`else", file=f)
assign(f, "spec_mem_rmask", "((1 << %d)-1) << (addr-spec_mem_addr)" % numbytes)
print("`endif", file=f)
if signext:
assign(f, "spec_rd_wdata", "spec_rd_addr ? $signed(result) : 0")
else:
@@ -504,7 +508,11 @@ def insn_l(insn, funct3, numbytes, signext, misa=0):
assign(f, "spec_rs1_addr", "insn_rs1")
assign(f, "spec_rd_addr", "insn_rd")
assign(f, "spec_mem_addr", "addr")
print("`ifdef RISCV_FORMAL_IGNORE_RMASK", file=f)
assign(f, "spec_mem_rmask", "0")
print("`else", file=f)
assign(f, "spec_mem_rmask", "((1 << %d)-1)" % numbytes)
print("`endif", file=f)
if signext:
assign(f, "spec_rd_wdata", "spec_rd_addr ? $signed(result) : 0")
else:
@@ -735,7 +743,11 @@ def insn_c_l(insn, funct3, numbytes, signext, misa=MISA_C):
assign(f, "spec_rs1_addr", "insn_rs1")
assign(f, "spec_rd_addr", "insn_rd")
assign(f, "spec_mem_addr", "addr & ~(`RISCV_FORMAL_XLEN/8-1)")
print("`ifdef RISCV_FORMAL_IGNORE_RMASK", file=f)
assign(f, "spec_mem_rmask", "0")
print("`else", file=f)
assign(f, "spec_mem_rmask", "((1 << %d)-1) << (addr-spec_mem_addr)" % numbytes)
print("`endif", file=f)
if signext:
assign(f, "spec_rd_wdata", "spec_rd_addr ? $signed(result) : 0")
else:
@@ -751,7 +763,11 @@ def insn_c_l(insn, funct3, numbytes, signext, misa=MISA_C):
assign(f, "spec_rs1_addr", "insn_rs1")
assign(f, "spec_rd_addr", "insn_rd")
assign(f, "spec_mem_addr", "addr")
print("`ifdef RISCV_FORMAL_IGNORE_RMASK", file=f)
assign(f, "spec_mem_rmask", "0")
print("`else", file=f)
assign(f, "spec_mem_rmask", "((1 << %d)-1)" % numbytes)
print("`endif", file=f)
if signext:
assign(f, "spec_rd_wdata", "spec_rd_addr ? $signed(result) : 0")
else:
@@ -996,7 +1012,11 @@ def insn_c_lsp(insn, funct3, numbytes, signext, misa=MISA_C):
assign(f, "spec_rs1_addr", "2")
assign(f, "spec_rd_addr", "insn_rd")
assign(f, "spec_mem_addr", "addr & ~(`RISCV_FORMAL_XLEN/8-1)")
print("`ifdef RISCV_FORMAL_IGNORE_RMASK", file=f)
assign(f, "spec_mem_rmask", "0")
print("`else", file=f)
assign(f, "spec_mem_rmask", "((1 << %d)-1) << (addr-spec_mem_addr)" % numbytes)
print("`endif", file=f)
if signext:
assign(f, "spec_rd_wdata", "spec_rd_addr ? $signed(result) : 0")
else:
@@ -1012,7 +1032,11 @@ def insn_c_lsp(insn, funct3, numbytes, signext, misa=MISA_C):
assign(f, "spec_rs1_addr", "2")
assign(f, "spec_rd_addr", "insn_rd")
assign(f, "spec_mem_addr", "addr")
print("`ifdef RISCV_FORMAL_IGNORE_RMASK", file=f)
assign(f, "spec_mem_rmask", "0")
print("`else", file=f)
assign(f, "spec_mem_rmask", "((1 << %d)-1)" % numbytes)
print("`endif", file=f)
if signext:
assign(f, "spec_rd_wdata", "spec_rd_addr ? $signed(result) : 0")
else:
8 insns/insn_c_ld.v
View file
Open in desktop
@@ -48,7 +48,11 @@ module rvfi_insn_c_ld (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 8)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 2;
assign spec_trap = ((addr & (8-1)) != 0) || !misa_ok;
@@ -59,7 +63,11 @@ module rvfi_insn_c_ld (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 8)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 2;
assign spec_trap = !misa_ok;
8 insns/insn_c_ldsp.v
View file
Open in desktop
@@ -47,7 +47,11 @@ module rvfi_insn_c_ldsp (
assign spec_rs1_addr = 2;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 8)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 2;
assign spec_trap = ((addr & (8-1)) != 0) || !misa_ok;
@@ -58,7 +62,11 @@ module rvfi_insn_c_ldsp (
assign spec_rs1_addr = 2;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 8)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 2;
assign spec_trap = !misa_ok;
8 insns/insn_c_lw.v
View file
Open in desktop
@@ -48,7 +48,11 @@ module rvfi_insn_c_lw (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 4)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 2;
assign spec_trap = ((addr & (4-1)) != 0) || !misa_ok;
@@ -59,7 +63,11 @@ module rvfi_insn_c_lw (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 4)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 2;
assign spec_trap = !misa_ok;
8 insns/insn_c_lwsp.v
View file
Open in desktop
@@ -47,7 +47,11 @@ module rvfi_insn_c_lwsp (
assign spec_rs1_addr = 2;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 4)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 2;
assign spec_trap = ((addr & (4-1)) != 0) || !misa_ok;
@@ -58,7 +62,11 @@ module rvfi_insn_c_lwsp (
assign spec_rs1_addr = 2;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 4)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 2;
assign spec_trap = !misa_ok;
8 insns/insn_lb.v
View file
Open in desktop
@@ -48,7 +48,11 @@ module rvfi_insn_lb (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 1)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = ((addr & (1-1)) != 0) || !misa_ok;
@@ -59,7 +63,11 @@ module rvfi_insn_lb (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 1)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = !misa_ok;
8 insns/insn_lbu.v
View file
Open in desktop
@@ -48,7 +48,11 @@ module rvfi_insn_lbu (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 1)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? result : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = ((addr & (1-1)) != 0) || !misa_ok;
@@ -59,7 +63,11 @@ module rvfi_insn_lbu (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 1)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? result : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = !misa_ok;
8 insns/insn_ld.v
View file
Open in desktop
@@ -48,7 +48,11 @@ module rvfi_insn_ld (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 8)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = ((addr & (8-1)) != 0) || !misa_ok;
@@ -59,7 +63,11 @@ module rvfi_insn_ld (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 8)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = !misa_ok;
8 insns/insn_lh.v
View file
Open in desktop
@@ -48,7 +48,11 @@ module rvfi_insn_lh (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 2)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = ((addr & (2-1)) != 0) || !misa_ok;
@@ -59,7 +63,11 @@ module rvfi_insn_lh (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 2)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = !misa_ok;
8 insns/insn_lhu.v
View file
Open in desktop
@@ -48,7 +48,11 @@ module rvfi_insn_lhu (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 2)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? result : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = ((addr & (2-1)) != 0) || !misa_ok;
@@ -59,7 +63,11 @@ module rvfi_insn_lhu (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 2)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? result : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = !misa_ok;
8 insns/insn_lw.v
View file
Open in desktop
@@ -48,7 +48,11 @@ module rvfi_insn_lw (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 4)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = ((addr & (4-1)) != 0) || !misa_ok;
@@ -59,7 +63,11 @@ module rvfi_insn_lw (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 4)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? $signed(result) : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = !misa_ok;
8 insns/insn_lwu.v
View file
Open in desktop
@@ -48,7 +48,11 @@ module rvfi_insn_lwu (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr & ~(`RISCV_FORMAL_XLEN/8-1);
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 4)-1) << (addr-spec_mem_addr);
`endif
assign spec_rd_wdata = spec_rd_addr ? result : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = ((addr & (4-1)) != 0) || !misa_ok;
@@ -59,7 +63,11 @@ module rvfi_insn_lwu (
assign spec_rs1_addr = insn_rs1;
assign spec_rd_addr = insn_rd;
assign spec_mem_addr = addr;
`ifdef RISCV_FORMAL_IGNORE_RMASK
assign spec_mem_rmask = 0;
`else
assign spec_mem_rmask = ((1 << 4)-1);
`endif
assign spec_rd_wdata = spec_rd_addr ? result : 0;
assign spec_pc_wdata = rvfi_pc_rdata + 4;
assign spec_trap = !misa_ok;
ProTip! Use n and p to navigate between commits in a pull request.