From dad01ec918e9db662f7c3afee85b359724c85226 Mon Sep 17 00:00:00 2001
From: Tom Verbeure <hombre+github@gmail.com>
Date: Thu, 9 Aug 2018 23:13:32 -0700
Subject: [PATCH] Change mul formal to new method

---
 insns/insn_mul.v    | 5 +++--
 insns/insn_mulh.v   | 5 +++--
 insns/insn_mulhsu.v | 5 +++--
 insns/insn_mulhu.v  | 5 +++--
 4 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/insns/insn_mul.v b/insns/insn_mul.v
index 8763cdd..b610146 100644
--- a/insns/insn_mul.v
+++ b/insns/insn_mul.v
@@ -32,8 +32,9 @@ module rvfi_insn_mul (
 
   // MUL instruction
 `ifdef RISCV_FORMAL_ALTOPS
-  wire [`RISCV_FORMAL_XLEN-1:0] altops_bitmask = 64'h2cdf52a55876063e;
-  wire [`RISCV_FORMAL_XLEN-1:0] result = (rvfi_rs1_rdata + rvfi_rs2_rdata) ^ altops_bitmask;
+  wire [`RISCV_FORMAL_XLEN:0] rs1 = {{`RISCV_FORMAL_XLEN{1'b0}}, rvfi_rs1_rdata};
+  wire [`RISCV_FORMAL_XLEN:0] rs2 = {{`RISCV_FORMAL_XLEN{1'b0}}, rvfi_rs2_rdata};
+  wire [`RISCV_FORMAL_XLEN-1:0] result = ($signed({rs1, rs1}) + $signed({rs2, rs2}));
 `else
   wire [`RISCV_FORMAL_XLEN-1:0] result = rvfi_rs1_rdata * rvfi_rs2_rdata;
 `endif
diff --git a/insns/insn_mulh.v b/insns/insn_mulh.v
index baf9ac0..df6eca3 100644
--- a/insns/insn_mulh.v
+++ b/insns/insn_mulh.v
@@ -32,8 +32,9 @@ module rvfi_insn_mulh (
 
   // MULH instruction
 `ifdef RISCV_FORMAL_ALTOPS
-  wire [`RISCV_FORMAL_XLEN-1:0] altops_bitmask = 64'h15d01651f6583fb7;
-  wire [`RISCV_FORMAL_XLEN-1:0] result = (rvfi_rs1_rdata + rvfi_rs2_rdata) ^ altops_bitmask;
+  wire [`RISCV_FORMAL_XLEN:0] rs1 = {{`RISCV_FORMAL_XLEN{rvfi_rs1_rdata[`RISCV_FORMAL_XLEN-1]}}, rvfi_rs1_rdata};
+  wire [`RISCV_FORMAL_XLEN:0] rs2 = {{`RISCV_FORMAL_XLEN{rvfi_rs2_rdata[`RISCV_FORMAL_XLEN-1]}}, rvfi_rs2_rdata};
+  wire [`RISCV_FORMAL_XLEN-1:0] result = ($signed({rs1, rs1}) + $signed({rs2, rs2})) >> `RISCV_FORMAL_XLEN;
 `else
   wire [`RISCV_FORMAL_XLEN-1:0] result = ({{`RISCV_FORMAL_XLEN{rvfi_rs1_rdata[`RISCV_FORMAL_XLEN-1]}}, rvfi_rs1_rdata} *
 		{{`RISCV_FORMAL_XLEN{rvfi_rs2_rdata[`RISCV_FORMAL_XLEN-1]}}, rvfi_rs2_rdata}) >> `RISCV_FORMAL_XLEN;
diff --git a/insns/insn_mulhsu.v b/insns/insn_mulhsu.v
index c9fc018..16b1931 100644
--- a/insns/insn_mulhsu.v
+++ b/insns/insn_mulhsu.v
@@ -32,8 +32,9 @@ module rvfi_insn_mulhsu (
 
   // MULHSU instruction
 `ifdef RISCV_FORMAL_ALTOPS
-  wire [`RISCV_FORMAL_XLEN-1:0] altops_bitmask = 64'hea3969edecfbe137;
-  wire [`RISCV_FORMAL_XLEN-1:0] result = (rvfi_rs1_rdata - rvfi_rs2_rdata) ^ altops_bitmask;
+  wire [`RISCV_FORMAL_XLEN:0] rs1 = {{`RISCV_FORMAL_XLEN{rvfi_rs1_rdata[`RISCV_FORMAL_XLEN-1]}}, rvfi_rs1_rdata};
+  wire [`RISCV_FORMAL_XLEN:0] rs2 = {{`RISCV_FORMAL_XLEN{1'b0}}, rvfi_rs2_rdata};
+  wire [`RISCV_FORMAL_XLEN-1:0] result = ($signed({rs1, rs1}) + $signed({rs2, rs2})) >> `RISCV_FORMAL_XLEN;
 `else
   wire [`RISCV_FORMAL_XLEN-1:0] result = ({{`RISCV_FORMAL_XLEN{rvfi_rs1_rdata[`RISCV_FORMAL_XLEN-1]}}, rvfi_rs1_rdata} *
 		{`RISCV_FORMAL_XLEN'b0, rvfi_rs2_rdata}) >> `RISCV_FORMAL_XLEN;
diff --git a/insns/insn_mulhu.v b/insns/insn_mulhu.v
index ad1c237..85f13aa 100644
--- a/insns/insn_mulhu.v
+++ b/insns/insn_mulhu.v
@@ -32,8 +32,9 @@ module rvfi_insn_mulhu (
 
   // MULHU instruction
 `ifdef RISCV_FORMAL_ALTOPS
-  wire [`RISCV_FORMAL_XLEN-1:0] altops_bitmask = 64'hd13db50d949ce5e8;
-  wire [`RISCV_FORMAL_XLEN-1:0] result = (rvfi_rs1_rdata + rvfi_rs2_rdata) ^ altops_bitmask;
+  wire [`RISCV_FORMAL_XLEN:0] rs1 = {{`RISCV_FORMAL_XLEN{1'b0}}, rvfi_rs1_rdata};
+  wire [`RISCV_FORMAL_XLEN:0] rs2 = {{`RISCV_FORMAL_XLEN{1'b0}}, rvfi_rs2_rdata};
+  wire [`RISCV_FORMAL_XLEN-1:0] result = ($signed({rs1, rs1}) + $signed({rs2, rs2})) >> `RISCV_FORMAL_XLEN;
 `else
   wire [`RISCV_FORMAL_XLEN-1:0] result = ({`RISCV_FORMAL_XLEN'b0, rvfi_rs1_rdata} * {`RISCV_FORMAL_XLEN'b0, rvfi_rs2_rdata}) >> `RISCV_FORMAL_XLEN;
 `endif