Change mul formal to new method

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

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;

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;

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