dsleung

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-17 13:26:00 +08:00

c4cbc4bfea Explicitly define reset value in cycle signal for uniqueness check

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-17 13:23:01 +08:00

32388adce0 Make liveness checks pass

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-17 13:08:14 +08:00

b38f19411a Make uniqueness checks pass

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-16 17:12:57 +08:00

e50d35ead5 Remove "Known issues" section in README

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-16 12:30:24 +08:00

a6b072efcf Fix parser error: invalid slice for memory-related instruction checks

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-15 17:13:22 +08:00

ee19bc49e7 Add bounded fairness constraints for liveness check

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-15 16:35:15 +08:00

e3b124f4eb Fix minor bug in SRL instruction specification

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-15 16:12:43 +08:00

c4daa89a88 Fix minor bug in JAL instruction specification

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-15 15:44:23 +08:00

0f4a2a76bd Tweak parameters for Minerva verification tasks

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-07 15:44:24 +08:00

a9f1431959 Record failing instructions in individual instruction checks

dsleung deleted branch fix/shrink-memory from M-Labs/riscv-formal-nmigen

2020-09-07 12:34:22 +08:00

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-09-07 12:32:28 +08:00

d84852e368 Replace unconditional pass and OOM issue with assertion failure

dsleung pushed to fix/shrink-memory at M-Labs/riscv-formal-nmigen

2020-09-04 16:24:44 +08:00

c9132050a8 Shrink memory size and reduce BMC depth to fix memory overconsumption problem

dsleung pushed to fix/shrink-memory at M-Labs/riscv-formal-nmigen

2020-09-03 14:51:58 +08:00

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-08-28 12:33:25 +08:00

d25785c4b4 Update README.md to reflect support for 64-bit ISAs

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-08-28 12:30:48 +08:00

b3acff2bf3 Update README.md

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-08-28 12:21:06 +08:00

e117fad73d Add RV64M Standard Extension

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-08-28 12:04:59 +08:00

9b4644e905 Add REMUW instruction

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-08-28 12:01:09 +08:00

64964655ff Add REMW instruction

dsleung pushed to master at M-Labs/riscv-formal-nmigen

2020-08-28 11:55:19 +08:00

f1a5da1a34 Add DIVUW instruction