Merge pull request #618 from powdr-labs/remu-instruction

remu instruction
powdr-labs · Oct 2, 2023 · 055199d · 055199d
2 parents e231006 + 27da6f0
commit 055199d
Show file tree

Hide file tree

Showing 3 changed files with 173 additions and 15 deletions.
diff --git a/riscv/src/compiler.rs b/riscv/src/compiler.rs
@@ -67,12 +67,12 @@ impl Architecture for RiscvArchitecture {
     fn instruction_ends_control_flow(instr: &str) -> bool {
         match instr {
             "li" | "lui" | "la" | "mv" | "add" | "addi" | "sub" | "neg" | "mul" | "mulhu"
-            | "divu" | "xor" | "xori" | "and" | "andi" | "or" | "ori" | "not" | "slli" | "sll"
-            | "srli" | "srl" | "srai" | "seqz" | "snez" | "slt" | "slti" | "sltu" | "sltiu"
-            | "sgtz" | "beq" | "beqz" | "bgeu" | "bltu" | "blt" | "bge" | "bltz" | "blez"
-            | "bgtz" | "bgez" | "bne" | "bnez" | "jal" | "jalr" | "call" | "ecall" | "ebreak"
-            | "lw" | "lb" | "lbu" | "lh" | "lhu" | "sw" | "sh" | "sb" | "nop" | "fence"
-            | "fence.i" | "amoadd.w.rl" | "amoadd.w" => false,
+            | "divu" | "remu" | "xor" | "xori" | "and" | "andi" | "or" | "ori" | "not" | "slli"
+            | "sll" | "srli" | "srl" | "srai" | "seqz" | "snez" | "slt" | "slti" | "sltu"
+            | "sltiu" | "sgtz" | "beq" | "beqz" | "bgeu" | "bltu" | "blt" | "bge" | "bltz"
+            | "blez" | "bgtz" | "bgez" | "bne" | "bnez" | "jal" | "jalr" | "call" | "ecall"
+            | "ebreak" | "lw" | "lb" | "lbu" | "lh" | "lhu" | "sw" | "sh" | "sb" | "nop"
+            | "fence" | "fence.i" | "amoadd.w.rl" | "amoadd.w" => false,
             "j" | "jr" | "tail" | "ret" | "unimp" => true,
             _ => {
                 panic!("Unknown instruction: {instr}");
@@ -535,6 +535,7 @@ fn preamble() -> String {
     reg X[<=];
     reg Y[<=];
     reg Z[<=];
+    reg W[<=];
     reg tmp1;
     reg tmp2;
     reg tmp3;
@@ -734,8 +735,6 @@ fn preamble() -> String {
         { Y_b7 } in { bytes };
         { Y_b8 } in { bytes };
 
-        col witness remainder; 
-
         col witness REM_b1;
         col witness REM_b2;
         col witness REM_b3;
@@ -746,20 +745,21 @@ fn preamble() -> String {
         { REM_b4 } in { bytes };
     }
 
-    // implements Z = Y / X, stores remainder in `remainder`.
-    instr divu Y, X -> Z {
+    // implements Z = Y / X and W = Y % X.
+    instr divremu Y, X -> Z, W {
+        // main division algorithm:
         // Y is the known dividend
         // X is the known divisor
         // Z is the unknown quotient
-        // main division algorithm;
+        // W is the unknown remainder
         // if X is zero, remainder is set to dividend, as per RISC-V specification:
-        X * Z + remainder = Y,
+        X * Z + W = Y,
 
         // remainder >= 0:
-        remainder = REM_b1 + REM_b2 * 0x100 + REM_b3 * 0x10000 + REM_b4 * 0x1000000,
+        W = REM_b1 + REM_b2 * 0x100 + REM_b3 * 0x10000 + REM_b4 * 0x1000000,
 
         // remainder < divisor, conditioned to X not being 0:
-        (1 - XIsZero) * (X - remainder - 1 - Y_b5 - Y_b6 * 0x100 - Y_b7 * 0x10000 - Y_b8 * 0x1000000) = 0,
+        (1 - XIsZero) * (X - W - 1 - Y_b5 - Y_b6 * 0x100 - Y_b7 * 0x10000 - Y_b8 * 0x1000000) = 0,
 
         // in case X is zero, we set quotient according to RISC-V specification
         XIsZero * (Z - 0xffffffff) = 0,
@@ -788,6 +788,10 @@ fn runtime() -> &'static str {
 .globl __udivdi3
 .set __udivdi3@plt, __udivdi3
 
+.globl __umoddi3@plt
+.globl __umoddi3
+.set __umoddi3@plt, __umoddi3
+
 .globl memcpy@plt
 .globl memcpy
 .set memcpy@plt, memcpy
@@ -1004,7 +1008,11 @@ fn process_instruction(instr: &str, args: &[Argument]) -> Vec<String> {
         }
         "divu" => {
             let (rd, r1, r2) = rrr(args);
-            only_if_no_write_to_zero(format!("{rd} <=Z= divu({r1}, {r2});"), rd)
+            only_if_no_write_to_zero(format!("{rd}, tmp1 <== divremu({r1}, {r2});"), rd)
+        }
+        "remu" => {
+            let (rd, r1, r2) = rrr(args);
+            only_if_no_write_to_zero(format!("tmp1, {rd} <== divremu({r1}, {r2});"), rd)
         }
 
         // bitwise

diff --git a/riscv/tests/instruction_tests/generated/remu.S b/riscv/tests/instruction_tests/generated/remu.S
@@ -0,0 +1,109 @@
+# 0 "sources/remu.S"
+# 0 "<built-in>"
+# 0 "<command-line>"
+# 1 "/usr/include/stdc-predef.h" 1 3 4
+# 0 "<command-line>" 2
+# 1 "sources/remu.S"
+# See LICENSE for license details.
+
+#*****************************************************************************
+# remu.S
+#-----------------------------------------------------------------------------
+
+# Test remu instruction.
+
+
+# 1 "sources/riscv_test.h" 1
+# 11 "sources/remu.S" 2
+# 1 "sources/test_macros.h" 1
+
+
+
+
+
+
+#-----------------------------------------------------------------------
+# Helper macros
+#-----------------------------------------------------------------------
+# 20 "sources/test_macros.h"
+# We use a macro hack to simpify code generation for various numbers
+# of bubble cycles.
+# 36 "sources/test_macros.h"
+#-----------------------------------------------------------------------
+# RV64UI MACROS
+#-----------------------------------------------------------------------
+
+#-----------------------------------------------------------------------
+# Tests for instructions with immediate operand
+#-----------------------------------------------------------------------
+# 92 "sources/test_macros.h"
+#-----------------------------------------------------------------------
+# Tests for vector config instructions
+#-----------------------------------------------------------------------
+# 120 "sources/test_macros.h"
+#-----------------------------------------------------------------------
+# Tests for an instruction with register operands
+#-----------------------------------------------------------------------
+# 148 "sources/test_macros.h"
+#-----------------------------------------------------------------------
+# Tests for an instruction with register-register operands
+#-----------------------------------------------------------------------
+# 242 "sources/test_macros.h"
+#-----------------------------------------------------------------------
+# Test memory instructions
+#-----------------------------------------------------------------------
+# 319 "sources/test_macros.h"
+#-----------------------------------------------------------------------
+# Test branch instructions
+#-----------------------------------------------------------------------
+# 404 "sources/test_macros.h"
+#-----------------------------------------------------------------------
+# Test jump instructions
+#-----------------------------------------------------------------------
+# 433 "sources/test_macros.h"
+#-----------------------------------------------------------------------
+# RV64UF MACROS
+#-----------------------------------------------------------------------
+
+#-----------------------------------------------------------------------
+# Tests floating-point instructions
+#-----------------------------------------------------------------------
+# 569 "sources/test_macros.h"
+#-----------------------------------------------------------------------
+# Pass and fail code (assumes test num is in x28)
+#-----------------------------------------------------------------------
+# 581 "sources/test_macros.h"
+#-----------------------------------------------------------------------
+# Test data section
+#-----------------------------------------------------------------------
+# 12 "sources/remu.S" 2
+
+
+.globl __runtime_start; __runtime_start:
+
+  #-------------------------------------------------------------
+  # Arithmetic tests
+  #-------------------------------------------------------------
+
+  test_2: li x10, 2; ebreak; li x1, 20; li x2, 6; remu x3, x1, x2;; li x29, 2; li x28, 2; bne x3, x29, fail;;
+  test_3: li x10, 3; ebreak; li x1, -20; li x2, 6; remu x3, x1, x2;; li x29, 2; li x28, 3; bne x3, x29, fail;;
+  test_4: li x10, 4; ebreak; li x1, 20; li x2, -6; remu x3, x1, x2;; li x29, 20; li x28, 4; bne x3, x29, fail;;
+  test_5: li x10, 5; ebreak; li x1, -20; li x2, -6; remu x3, x1, x2;; li x29, -20; li x28, 5; bne x3, x29, fail;;
+
+  test_6: li x10, 6; ebreak; li x1, -1<<31; li x2, 1; remu x3, x1, x2;; li x29, 0; li x28, 6; bne x3, x29, fail;;
+  test_7: li x10, 7; ebreak; li x1, -1<<31; li x2, -1; remu x3, x1, x2;; li x29, -1<<31; li x28, 7; bne x3, x29, fail;;
+
+  test_8: li x10, 8; ebreak; li x1, -1<<31; li x2, 0; remu x3, x1, x2;; li x29, -1<<31; li x28, 8; bne x3, x29, fail;;
+  test_9: li x10, 9; ebreak; li x1, 1; li x2, 0; remu x3, x1, x2;; li x29, 1; li x28, 9; bne x3, x29, fail;;
+  test_10: li x10, 10; ebreak; li x1, 0; li x2, 0; remu x3, x1, x2;; li x29, 0; li x28, 10; bne x3, x29, fail;;
+
+  bne x0, x28, pass; fail: unimp;; pass: ___pass: j ___pass;
+
+
+
+  .data
+.balign 4;
+
+
+
+
diff --git a/riscv/tests/instruction_tests/sources/remu.S b/riscv/tests/instruction_tests/sources/remu.S
@@ -0,0 +1,41 @@
+# See LICENSE for license details.
+
+#*****************************************************************************
+# remu.S
+#-----------------------------------------------------------------------------
+#
+# Test remu instruction.
+#
+
+#include "riscv_test.h"
+#include "test_macros.h"
+
+RVTEST_RV32U
+RVTEST_CODE_BEGIN
+
+  #-------------------------------------------------------------
+  # Arithmetic tests
+  #-------------------------------------------------------------
+
+  TEST_RR_OP( 2, remu,   2,  20,   6 );
+  TEST_RR_OP( 3, remu,   2, -20,   6 );
+  TEST_RR_OP( 4, remu,  20,  20,  -6 );
+  TEST_RR_OP( 5, remu, -20, -20,  -6 );
+
+  TEST_RR_OP( 6, remu,      0, -1<<31,  1 );
+  TEST_RR_OP( 7, remu, -1<<31, -1<<31, -1 );
+
+  TEST_RR_OP( 8, remu, -1<<31, -1<<31, 0 );
+  TEST_RR_OP( 9, remu,      1,      1, 0 );
+  TEST_RR_OP(10, remu,      0,      0, 0 );
+
+  TEST_PASSFAIL
+
+RVTEST_CODE_END
+
+  .data
+RVTEST_DATA_BEGIN
+
+  TEST_DATA
+
+RVTEST_DATA_END