LMARV-1 reboot part 5: formal verification of the CPU

This part explains a bit about a more rigorous version of the formal verification that I've been doing -- prove mode. And we build the CPU by hooking up all the cards, and then formally verifying it.
Also, for some reason at the end I channel Cody's Lab.
github repo for code: github.com/RobertBaruch/riscv...
RISC-V specs: riscv.org/technical/specifica...
nMigen tutorial: github.com/RobertBaruch/nmige...

[@gsuberland]

So glad the theme song is back.

[@esra_erimez]

I love this series.

[@KaneYork]

Wow, that talk about why formal induction works and how to use it was actually very helpful!

[@MichaelFJ1969]

This is one of the best explanations of formal verification and induction. Thank you for making this and all the other videos!

[@KingJellyfishII]

I love the idea of just incrementing the higher bits of the memories that hold the registers, if there are enough bits could that be hooked up to another incrementer/decrementer to implement a super fast pushall and popall?

[@gudenau]

This is a very interesting video. I think I kinda understand.

[@lawrencemanning]

Do you really need traps if you are not doing OS level code, or is the plan to port an OS to your TTL RISCV?

[@RobertBaruch]

I need traps to handle interrupts. Otherwise the only other way to handle external signals is to poll for them, and who wants to do that?

[@kayakMike1000]

Polling is fine, but let's do it in hardware.

[@KaneYork]

Hmm, when you're asserting about the illegal instruction symbol, you didn't consider several categories of instructions that should be illegal - e.g. OP-FP, or compressed or extended instructions. 44:30

[@RobertBaruch]

The standard seems to indicate that if you don't implement an extension, you get to decide what to do when you encounter instructions in that extension. I decided to just skip over the instruction :)

[@JonSeverinsson]

​@@RobertBaruch I don't think you are reading that quite right (or otherwise I'm not ;-) ). Any instruction that you don't implement is supposed to generate a "Illegal instruction" trap. But any instruction encoding not specified in the base instruction set or a supported extension can be reused for an instruction in a custom extension if you want to (Though if you use any instruction encoding other than those explicitly reserved for custom extensions, [i.e. major opcodes custom-0, custom-1, custom-2, and custom-3] it would be a non-conforming custom extension). I *guess* you could create a non-conforming custom extension that uses all instruction encodings not used by RV32I and then not document the behaviour of most of you custom instructions, but that would be seriously bad manner. Also, that would prevent software emulation of unsupported extensions, which can be quite useful.

[@RobertBaruch]

@@JonSeverinsson Well, 2.2 says that "The behavior upon decoding a reserved instruction is unspecified" so that covers the "holes" in instructions. But I suppose it does make sense that if an extension is not supported, then an instruction in that extension should generate a trap, so that either an exception is signaled, or the execution environment implementation could emulate the instruction. In that case I should probably just lock everything down and throw an illegal instruction exception.

[@gudenau]

Why is PC 32 bits if everything is aligned on a 32 bit boundary? It could be 30 bits and save a little bit of resources.

[@TomStorey96]

32 bits is 4 bytes. If you remove any of those bits you only make things more difficult in other ways.

[@kitlith]

So, something's starting to bug me with this "cards on a bus" architecture. The sequencer is intended to be its own card, yes? The problem is that each new instruction/extension will end up needing to also touch the sequencer card. So you can't just "throw in a card that implements the bit manipulation extension", you also have to replace the sequencer card. Personally, this makes it a bit moot -- you may as well have the alu, sequencer, registers, etc., all on a single board and then just use the cards for CSRs and peripherals. now, i'm sure you can add things to the bus to external cards can implement new extensions/instructions, but i feel like it'd be simpler if that's how everything worked in the first place. idk.

[@colejohnson66]

There’s two (well, three) solutions: a “coprocessor flag” that signals another card to do something and throw an illegal instruction exception if nothing responds. The other option is to have a way for the sequencer to know about coprocessors (like an I2C side bus for communications) and what opcodes they support, then when a “new” instruction is reached, see if a “coprocessor” claims to support it and toss control over to that card (by doing nothing and letting the card deal with the instruction) until it’s done. The third “solution” is to just do nothing which would possibly require a new sequencer card for each extension. I’m reminded of Intel when the x87 was a physical (optional) coprocessor. If a 0xD? byte was reached (as the first of an instruction), the main CPU would just ignore it and the x87/FPU would work in the background to compute the result. Then the FPU would tell the CPU that it was done so the CPU could get the result.

[@KaneYork]

The processor is actually not responsible for swapping registers during a trap. Instead, the handler must swap mscratch to obtain access to the register storage space. See 3.1.14 and the MRET/SRET instruction, which only pops the privilege and interrupt enable stacks.

[@RobertBaruch]

Correct, but the usual way the trap handler runs is to push/pop all registers. I just shortcut that by doing it in hardware.

[@jecelassumpcaojr890]

@@RobertBaruch Here is a RISC-V with the option of a different bank of registers for interrupts: github.com/darklife/darkriscv Note that while the counter CSRs were part of the 32I base instruction set until recently, they have become optional in the latest revision (now they are extension Zicsr in chapters 9 and 10)

[@lukasschwager5876]

@@RobertBaruch I think, the correct (i. e. standard conforming) way would be, that you create an instruction set extension to do that. That means, that the interrupt handler would be called as the standard describes and then performs a register swap instruction. There is plenty of space in the opcode matrix to do that. Also this would mean, that you could possibly do it as an optimization for for function calls. Instead of pushing the arguments to the stack, the caller would now copy the arguments to a fresh bank of registers, then switch to it and call the function. I imagine this being a big performance boost for some programs. That would mean, that you need to change the api though.

[@RobertBaruch]

@@lukasschwager5876 Actually, now that I think about it -- automatically swapping the register page might not be great, since a trap might want to know what the registers were when the trap happened. So then yeah, a register page swap instruction would be in the CUSTOM extension.