From 29fb2c5f66cba4d56ef0477606b457fe7426eafd Mon Sep 17 00:00:00 2001
From: Christos Gentsos <christos.gentsos@cern.ch>
Date: Tue, 14 Apr 2020 12:34:59 +0200
Subject: [PATCH] Add support for optionally ignoring rmask

---
 docs/config.md      |  6 ++++++
 docs/rvfi.md        |  2 +-
 insns/generate.py   | 24 ++++++++++++++++++++++++
 insns/insn_c_ld.v   |  8 ++++++++
 insns/insn_c_ldsp.v |  8 ++++++++
 insns/insn_c_lw.v   |  8 ++++++++
 insns/insn_c_lwsp.v |  8 ++++++++
 insns/insn_lb.v     |  8 ++++++++
 insns/insn_lbu.v    |  8 ++++++++
 insns/insn_ld.v     |  8 ++++++++
 insns/insn_lh.v     |  8 ++++++++
 insns/insn_lhu.v    |  8 ++++++++
 insns/insn_lw.v     |  8 ++++++++
 insns/insn_lwu.v    |  8 ++++++++
 monitor/generate.py |  9 ++++++++-
 15 files changed, 127 insertions(+), 2 deletions(-)

diff --git a/docs/config.md b/docs/config.md
index 1ac6fe0..7470563 100644
--- a/docs/config.md
+++ b/docs/config.md
@@ -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
 --------------------------
 
diff --git a/docs/rvfi.md b/docs/rvfi.md
index 812615a..80ac725 100644
--- a/docs/rvfi.md
+++ b/docs/rvfi.md
@@ -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
 
diff --git a/insns/generate.py b/insns/generate.py
index 6bbb26d..099167d 100644
--- a/insns/generate.py
+++ b/insns/generate.py
@@ -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:
diff --git a/insns/insn_c_ld.v b/insns/insn_c_ld.v
index 141b681..2b43432 100644
--- a/insns/insn_c_ld.v
+++ b/insns/insn_c_ld.v
@@ -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;
diff --git a/insns/insn_c_ldsp.v b/insns/insn_c_ldsp.v
index 58aed8f..ff1548f 100644
--- a/insns/insn_c_ldsp.v
+++ b/insns/insn_c_ldsp.v
@@ -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;
diff --git a/insns/insn_c_lw.v b/insns/insn_c_lw.v
index 355d421..67de4e5 100644
--- a/insns/insn_c_lw.v
+++ b/insns/insn_c_lw.v
@@ -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;
diff --git a/insns/insn_c_lwsp.v b/insns/insn_c_lwsp.v
index 3602e69..7843e4c 100644
--- a/insns/insn_c_lwsp.v
+++ b/insns/insn_c_lwsp.v
@@ -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;
diff --git a/insns/insn_lb.v b/insns/insn_lb.v
index 702ae14..bd6f069 100644
--- a/insns/insn_lb.v
+++ b/insns/insn_lb.v
@@ -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;
diff --git a/insns/insn_lbu.v b/insns/insn_lbu.v
index 6212380..1610547 100644
--- a/insns/insn_lbu.v
+++ b/insns/insn_lbu.v
@@ -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;
diff --git a/insns/insn_ld.v b/insns/insn_ld.v
index 11f3845..6f239e2 100644
--- a/insns/insn_ld.v
+++ b/insns/insn_ld.v
@@ -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;
diff --git a/insns/insn_lh.v b/insns/insn_lh.v
index 93754cd..096eba3 100644
--- a/insns/insn_lh.v
+++ b/insns/insn_lh.v
@@ -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;
diff --git a/insns/insn_lhu.v b/insns/insn_lhu.v
index cb9f926..528ca18 100644
--- a/insns/insn_lhu.v
+++ b/insns/insn_lhu.v
@@ -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;
diff --git a/insns/insn_lw.v b/insns/insn_lw.v
index 212624e..28dfe32 100644
--- a/insns/insn_lw.v
+++ b/insns/insn_lw.v
@@ -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;
diff --git a/insns/insn_lwu.v b/insns/insn_lwu.v
index 96c14d3..eeaa141 100644
--- a/insns/insn_lwu.v
+++ b/insns/insn_lwu.v
@@ -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;
diff --git a/monitor/generate.py b/monitor/generate.py
index 2273689..cc53735 100755
--- a/monitor/generate.py
+++ b/monitor/generate.py
@@ -17,6 +17,7 @@
 verbose_mode = False
 noregscheck = False
 nopccheck = False
+normaskcheck = False
 
 def usage():
     print("""
@@ -49,6 +50,9 @@ def usage():
   -P
       do not check consistency of pc reads and writes
 
+  -K
+      do not check the memory read mask
+
   -A
       add assert(0) statements to the error handlers
 
@@ -61,7 +65,7 @@ def usage():
     sys.exit(1)
 
 try:
-    opts, args = getopt.getopt(sys.argv[1:], "i:p:c:r:aMRPAQV")
+    opts, args = getopt.getopt(sys.argv[1:], "i:p:c:r:aMRPAQVK")
 except:
     usage()
 
@@ -82,6 +86,8 @@ def usage():
         noregscheck = True
     elif o == "-P":
         nopccheck = True
+    elif o == "-K":
+        normaskcheck = True
     elif o == "-U":
         nocausality = True
     elif o == "-O":
@@ -596,6 +602,7 @@ def usage():
 expected_flags = {
     "RISCV_FORMAL_COMPRESSED": compressed,
     "RISCV_FORMAL_ALIGNED_MEM": aligned,
+    "RISCV_FORMAL_IGNORE_RMASK": normaskcheck,
 }
 
 def print_rewrite_file(filename):