-require_xpr64;
-if(zext32(RS2) == 0)
- RD = UINT64_MAX;
+require_extension('M');
+require_rv64;
+reg_t lhs = zext32(RS1);
+reg_t rhs = zext32(RS2);
+if(rhs == 0)
+ WRITE_RD(UINT64_MAX);
else
- RD = sext32(zext32(RS1) / zext32(RS2));
+ WRITE_RD(sext32(lhs / rhs));