What does the formal verification flow/s look like for it?
He knew that the resistor was to limit current, and he knew about parallel and series circuits, so he just used one resistor on the other side of the LEDs instead of 8 of them... and then wondered why the LED brightness changed with the number of lit LEDs.
Hardware isn't the same as software... it's easy to forget that sometimes. 8)
nMigen is a pretty fledgling project so there aren't a ton of big projects in it yet, but for example Luna (from the makers of the HackRF) implements a full USB stack including USB3 support, with enough abstraction that you can create a USB-serial converter inside your FPGA using two I/Os for full-speed USB and wire it into the rest of your project in about ten lines of Python.
Migen, the Python-based project nMigen is based off, has been around for longer and has some large projects, such as LiteX which uses Migen to glue together entire SoCs, including peripheral cores such as GigE, DDR3/4, SATA, PCIe, etc, all written in Migen, and is pretty widely used. It also pulls in Verilog/VHDL designs (such as many of its CPU core choices) since it's easy to pull in those from the Python side.
For example, both:
x = Signal(4, true)
y = signed(4)
I will agree with you on the syntax, however. It’s caused by the fact that you’re not synthesizing your program, but writing code that generates code.
nmigen is a library, not a language. So it has to use what’s available to it. The upside is you don’t have to write tokenizers, parsers, etc, but the downside is it looks “hackish”.
m.d.comb += x.eq(y + 1)
Robert Baruch has a nice tutorial on nmigen: https://github.com/RobertBaruch/nmigen-tutorial
That said, high-level HDLs like nMigen are very promising for education, and I hope more people take the same first steps as the article's author did. It's a fun field.
And along those lines, here's hoping that MIT updates their free 6.004 edX course to reflect the in-person class' new RISC-V focus soon.
While it hasn't been uploaded into Open Courseware yet you can simply get it directly from the web site. Though you "have to be logged in", materials can be downloaded without logging in if you use a search engine to find what you're looking for, e.g. https://6004.mit.edu/web/_static/spring21/resources/fa20/L02... which talks about RISC-V
Someone above has mentioned Robert Baruch too: https://github.com/RobertBaruch/nmigen-tutorial
I also found this helpful: http://blog.lambdaconcept.com/doku.php?id=nmigen:tutorial
And there is of course the IRC channel if you want to ask people questions, #nmigen on irc.freenode.net
>"Despite being faster than schematics entry, hardware design with Verilog and VHDL remains tedious and inefficient for several reasons. The event-driven model introduces issues and manual coding that are unnecessary for synchronous circuits, which represent the lion's share of today's logic designs."
I think what they mean is that when you're defining synchronous logic in (System)Verilog or VHDL, the behaviour of that synchronous logic is defined as being in response to an event. For example, look through a Verilog codebase and you'll probably see lots of blocks that look like the following:
always @(posedge clock) begin
... // Some logic
Looking first at combinational logic: As the simulator goes through the "initial" code, it will set variables to new values. These value changes will activate event listeners throughout the code ("always @ *" or "assign" in Verilog), which represent combinational logic. So if variable "myvar" is updated, and it is an input to an adder in some other module, the always statement which updates the adder output will be triggered. Whenever a combinational event is triggered here at time 0, it is "scheduled" to be resolved at time 0 + delta, where delta just represents a time after time 0, but before time 0.000...01.
Alternatively, you can schedule events with a specific delay, such as setting up a clock signal to wait 0.5ns and then toggle. You can then setup event listeners to react to the rising edge of this clock signal ("always @ posedge" in Verilog), giving you synchronous logic.
Typically, a simulation will involve a bunch of setup a time 0, combinationally getting every variable to its initial condition. Then there will be no more events scheduled at the current simulator time, so the simulator advances until the next time it has an event scheduled (such as the clock edge at 0.5ns). That value changes from that event will likely trigger many more combinational events that will be resolved before moving onto the next clock edge.
When considering how this looks in actual hardware, you can still consider clocked elements as being event driven, but it's not obvious that it makes sense to think of combinational gates that way. Still, the tools are designed to construct a circuit that gives you the same result as the event driven semantics, as long as you meet timing constraints.
I'm not a simulator expert, so I may be slightly off in my explanation, but hopefully that gives you the general idea!
It's coursework that takes you from knowing nothing about hardware design to designing your own RISC-V In-Order Five stage architecture. As far as I know a few students have actually done the work to run this on an FPGA, but for the most part you will have the luxury of an emulator, giving you things like stack traces compared to the model execution for all the test programs etc. Execution trace example shown here: https://github.com/PeterAaser/RISCV-FiveStage/blob/master/Im...
Has RISC-V made the good tradeoffs? We'll have to wait a long time (until someone tries to make a high performance RISC-V instead of glorified microcontrollers) to know..
Note though that the RISC-V is a cleaned up MIPS ISA beside being open it doesn't bring much novelty (nothing to improve security or GCs) with the (significant) exception of the (unstable) vector ISA.