- Apr 22, 2021
- Apr 14, 2021
- Apr 10, 2021
-
-
Kia authored
-
- Apr 06, 2021
- Apr 05, 2021
- Apr 03, 2021
-
-
Kia authored
seems to work, i think we should write the shift register so we can do the proof against the golden model (which uses a nonsynthesizable RAM)
-
Kia authored
-
Kia authored
-
Kia authored
-
Kia authored
-
Kia authored
-
Kia authored
we can make this read-only because the only write that happens is for the parse tree and there's no read/write, it can be done with a straightforward gearbox, i believe.
-
- Mar 29, 2021
-
-
Kia authored
-
Kia authored
-
Kia authored
make it work in general case with non-unitary bit widths. also k-induction doesn't require more than 1 step!
-
Kia authored
remove superfluous asserts. at least i think they're superfluous, we still need to check with different upstream/downstream widths.
-
Kia authored
-
- Mar 24, 2021