Define a reverse carry-less multiply function for cmulr instructions

Also define a SMT property to prove equivalence with the previous implementation.

Update the Makefile.old to use the check_properties target to test the property with Z3, pending CMake integration.

Fixes #824.

Author: pmundkur

Makefile.old

@@ -67,6 +67,10 @@ SAIL_DEFAULT_INST += riscv_insts_vext_red.sail
 SAIL_DEFAULT_INST += riscv_insts_vext_fp_red.sail
 SAIL_DEFAULT_INST += riscv_insts_zicbom.sail
 SAIL_DEFAULT_INST += riscv_insts_zicboz.sail
+SAIL_DEFAULT_INST += riscv_insts_zvbb.sail
+SAIL_DEFAULT_INST += riscv_insts_zvbc.sail
+SAIL_DEFAULT_INST += riscv_insts_zimop.sail
+SAIL_DEFAULT_INST += riscv_insts_zcmop.sail
 
 SAIL_SEQ_INST  = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
 SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail
@@ -94,7 +98,7 @@ SAIL_VM_SRCS += riscv_vmem_tlb.sail
 SAIL_VM_SRCS += riscv_vmem.sail
 
 # Non-instruction sources
-PRELUDE = prelude.sail riscv_errors.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_addrtype.sail prelude_mem_metadata.sail prelude_mem.sail
+PRELUDE = prelude.sail riscv_errors.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_addrtype.sail prelude_mem_metadata.sail prelude_mem.sail arithmetic.sail
 
 SAIL_REGS_SRCS =  riscv_csr_begin.sail       # Start of CSR scattered definitions.
 SAIL_REGS_SRCS += riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail
@@ -125,6 +129,7 @@ SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS)
 SAIL_COQ_SRCS  = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_SRCS) $(SAIL_OTHER_COQ_SRCS))
 
 SAIL_FLAGS += --require-version 0.19
+SAIL_FLAGS += --config config/default.json
 SAIL_FLAGS += --strict-var
 SAIL_FLAGS += -dno_cast
 SAIL_DOC_FLAGS ?= -doc_embed plain
@@ -142,8 +147,8 @@ export LEM_DIR
 
 C_WARNINGS ?=
 #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
-C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h riscv_softfloat.h)
-C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_softfloat.c riscv_sim.c)
+C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_sail.h riscv_config.h riscv_platform_impl.h riscv_platform.h riscv_softfloat.h rvfi_dii.h)
+C_SRCS = $(addprefix c_emulator/,riscv_prelude.cpp riscv_platform_impl.cpp riscv_platform.cpp riscv_softfloat.c rvfi_dii.cpp riscv_sim.cpp)
 
 SOFTFLOAT_DIR    = dependencies/softfloat/berkeley-softfloat-3
 SOFTFLOAT_INCDIR = $(SOFTFLOAT_DIR)/source/include
@@ -205,6 +210,9 @@ all: c_emulator/riscv_sim_$(ARCH)
 check: $(SAIL_SRCS) model/main.sail Makefile.old
 	$(SAIL) $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail
 
+check_properties: $(SAIL_SRCS) Makefile.old
+	$(SAIL) --smt --smt-auto --smt-auto-solver z3 $(SAIL_FLAGS) $(SAIL_SRCS)
+
 interpret: $(SAIL_SRCS) model/main.sail
 	$(SAIL) -i $(SAIL_FLAGS) $(SAIL_SRCS) model/main.sail
 

model/arithmetic.sail

@@ -16,3 +16,26 @@ function carryless_mul(a, b) = {
   };
   result
 }
+
+/* Reverse carry-less multiply. */
+val carryless_mulr : forall 'n, 'n > 0. (bits('n), bits('n)) -> bits('n)
+function carryless_mulr(a, b) = {
+  var result : bits('n) = zeros();
+  foreach (i from 0 to ('n - 1)) {
+    if   a[i] == bitone
+    then result = result ^ (b >> ('n - i - 1));
+  };
+  result
+}
+
+/* Equivalent reverse carry-less multiply. */
+val carryless_mul_reversed : forall 'n, 'n > 0. (bits('n), bits('n)) -> bits('n)
+function carryless_mul_reversed(a, b) = {
+  let prod = carryless_mul(reverse(a), reverse(b));
+  reverse(prod['n - 1 .. 0])
+}
+
+$[property]
+function cmulr_equivalence(a : bits(16), b : bits(16)) -> bool = {
+  carryless_mul_reversed(a, b) == carryless_mulr(a, b)
+}

model/riscv_insts_zbc.sail

@@ -52,7 +52,6 @@ mapping clause assembly = RISCV_CLMULR(rs2, rs1, rd)
   <-> "clmulr" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ reg_name(rs2)
 
 function clause execute (RISCV_CLMULR(rs2, rs1, rd)) = {
-  let prod = carryless_mul(reverse(X(rs1)), reverse(X(rs2)));
-  X(rd) = reverse(prod[xlen - 1 .. 0]);
+  X(rd) = carryless_mulr(X(rs1), X(rs2));
   RETIRE_SUCCESS
 }