search

riscv / sail-riscv

Sail RISC-V model
https://lists.riscv.org/g/tech-golden-model
Other
430 stars 158 forks source link

Add >=0 constraints to quot_round_zero and rem_round_zero #553

Open Timmmm opened 2 days ago

Timmmm commented 2 days ago

The type declarations for those division operators are missing >0 and >=0 constraints.

See https://github.com/riscv/sail-riscv/pull/552/files#r1768223964

Alasdair commented 2 days ago

I had a go at doing this. It should be possible, but there are a few places where we will need to add explicit asserts for divisors, even if it looks somewhat obvious:

  if EMUL_pow < 0 then nf / (2 ^ (0 - EMUL_pow)) <= 8

This is never division by zero, but it requires reasoning about non-linear arithmetic to prove it which the SMT solver can't do.

Timmmm commented 2 days ago

Hmm isn't the output of 2 ^ always greater than zero? That does feel obvious...

Alasdair commented 2 days ago

Yes, but in practice the SMT solver just gives up whenever it sees 2 ^ n and n isn't bounded. I have a fallback routine that replaces 2 ^ with an arbitrary function that is equivalent up to 2 ^ 64 so I can check any problem that is unsatisfiable for such a function must be unsatisfiable in general, and I could improve that fallback to handle this case but it doesn't work without an explicit assert right now.

Alasdair commented 2 days ago

That does mean the other solution is to really understand the vector spec and add tight bounds to every variable.