VELDT-getting-started VS lion

Absolutely! I have also written a guide to getting started with Clash and the VELDT. It starts with a basic counter and builds incrementally to a UART. Definitely check out the Clash website for examples, documentation, tutorials, and blog posts! The Clash website is my go-to resource.

In terms of not just code, but also text, https://github.com/standardsemiconductor/VELDT-getting-started is a really great tutorial

I've been starting to dabble with digital logic design via Clash (https://clash-lang.org/), and there is a very cool-looking RISC-V SoC project done in that tool that looks fairly serious: https://github.com/standardsemiconductor/lion.

That’s fascinating about the M1. In retrospect it seems like kind of a no-brainer but I doubt I would have thought of it.

SPARC had different memory models at different ISA revs IIRC: it’s been like 20 years since I was dealing with SPARC so I might be misremembering the details. Alpha would have been a better example.

RISC-V is really interesting. I’ve been slowly working through this: https://github.com/standardsemiconductor/lion, highly recommend!

Interesting. Actually, you may be just the person to answer my question: Is it possible/plausible to run a Cardano node on Lion OS on a RISC-V machine? IMO, it would be great for the community if we could run all Cardano stake pools on end to end formally verified machines using open source core and hardware.

Lion: A formally verified, 5-stage pipeline RISC-V core\ (30 comments)

In addition, you can actually set the riscv-formal suite to verify correctness by k-induction: https://github.com/SymbioticEDA/riscv-formal/pull/28 https://symbiyosys.readthedocs.io/en/latest/quickstart.html#beyond-bounded-model-checks although I concur that by looking at https://github.com/standardsemiconductor/lion/blob/main/lion-formal/app/Main.hs the lion core is only verified with BMC.