Test Results

396 tests  ±0   396 ✅ ±0   0s ⏱️ ±0s
  4 suites ±0     0 💤 ±0 
  1 files   ±0     0 ❌ ±0 

Results for commit 7eea7ac. ± Comparison against base commit 07fa23e.

♻️ This comment has been updated with latest results.

The 'n produced in here, and I believe it can't be 0.

/* num_elem means max(VLMAX,VLEN/SEW)) according to Section 5.4 of RVV spec */
val get_num_elem : (int, int) -> nat
function get_num_elem(LMUL_pow, SEW) = {
  let LMUL_pow_reg = if LMUL_pow < 0 then 0 else LMUL_pow;
  /* Ignore lmul < 1 so that the entire vreg is read, allowing all masking to
   * be handled in init_masked_result */
  let num_elem = 2 ^ (LMUL_pow_reg) * VLEN / SEW;
  assert(num_elem > 0);
  num_elem
}

And the result of this commit run with riscv-vector-tests is in here

I'm really curious about the code below...
The function get_num_elem has a assert inside that it returns a number bigger than 0. See get_num_elem function.
But in the code below, If it doesn't have a assert('n > 0);, It won't compile and shows a type error.
And I think is really silly for write assert('n > 0); like hundres of times.

Maybe this should be supported by sail to remember the range of a funtion return value? idk...

let num_elem = get_num_elem(LMUL_pow, SEW);

if illegal_normal(vd, vm) then { handle_illegal(); return RETIRE_FAIL };

let 'n = num_elem;
let 'm = SEW;

Type error:
model/riscv_insts_vext_arith.sail:58.31-64:
58 |  let vm_val  : bits('n)     = read_vmask(num_elem, vm, 0b00000);
   |                               ^-------------------------------^
   | Could not resolve quantifiers for read_vmask
   | * 'n > 0

I'm really curious about the code below... The function get_num_elem has a assert inside that it returns a number bigger than 0. See get_num_elem function. But in the code below, If it doesn't have a assert('n > 0);, It won't compile and shows a type error. And I think is really silly for write assert('n > 0); like hundres of times.

Maybe this should be supported by sail to remember the range of a funtion return value? idk...

It should work if you make get_num_elem's return type { 'n, 'n > 0. int('n)}. At the moment it's just nat, which allows zero.

But I would recommend not trying to fix the types in this PR! I started going down that route and you end up rewriting half the vector code and never finishing (I have also done the same for the virtual memory code, though that is a less code so I've almost finished). Let's use asserts temporarily and then we can gradually fix the types and remove the asserts.

I change the def below, change 'n >= 0 to 'n > 0. Because it all use get_num_elem to produce it.

val process_rfvv_widen: forall 'n 'm 'p, 'n > 0 & 'm in {8, 16, 32, 64}. (rfvvfunct6, bits(1), regidx, regidx, regidx, int('n), int('m), int('p)) -> Retired
function process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow) = {

function clause execute(RFVVTYPE(funct6, vm, vs2, vs1, vd)) = {
  let SEW      = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem_vs = get_num_elem(LMUL_pow, SEW);

  if funct6 == FVV_VFWREDOSUM | funct6 == FVV_VFWREDUSUM then
    process_rfvv_widen(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow)
  else
    process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_pow)
}