You should look into RISC-V as well. Someone posted something about a formally-verified OS that runs on an fpga emulation of risc v. it’s called lion. Super interesting stuff and some among us figure it could be a foundation for an end-to-end formally verified machine. Perhaps virtually zero attack surface area…
I am indeed very interested in RISC-V. It’s one of the reasons that I got an FPGA board in the first place and why I decided to spend a bit extra to get a “grown-up” Xilinx 7 series instead of the cheap Lattice FPGAs. Just wish it were possible to get anywhere near “real” CPU clock speeds on an FPGA and that large enough FPGAs to run some of the really cool designs weren’t so expensive so that I could build my dream, fully-open-source computer.
You should look into RISC-V as well. Someone posted something about a formally-verified OS that runs on an fpga emulation of risc v. it’s called lion. Super interesting stuff and some among us figure it could be a foundation for an end-to-end formally verified machine. Perhaps virtually zero attack surface area…
I am indeed very interested in RISC-V. It’s one of the reasons that I got an FPGA board in the first place and why I decided to spend a bit extra to get a “grown-up” Xilinx 7 series instead of the cheap Lattice FPGAs. Just wish it were possible to get anywhere near “real” CPU clock speeds on an FPGA and that large enough FPGAs to run some of the really cool designs weren’t so expensive so that I could build my dream, fully-open-source computer.