| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-08-27 | Initial; working SAIL RISC-V regs | Aditya Naik | |
| The register definition along with read/write functions for registers are lowered to Coq. The FIRRTL annotation does not work as expected. | |||
![]() |
index : firrtl-coq | |
| Formal verification of FIRRTL components using Coq definitions generated from SAIL RISC-V specs | Aditya N. Naik |
| summaryrefslogtreecommitdiff |
| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-08-27 | Initial; working SAIL RISC-V regs | Aditya Naik | |
| The register definition along with read/write functions for registers are lowered to Coq. The FIRRTL annotation does not work as expected. | |||