I just acknowledged how underrated Your content is, compared to i.e. Ben Eater videos. Yes, nMigen is definitely on more abstract level than gates and adder chips. It took me some time watching Your videos to become fluent enough, to get knowledge of the circuit design/operation details and faster understand what's the code doing. I guess knowledge entry barrier affect TH-cam reach algorithm, but there's nothing You can do about it - the topic is just uncommon. I just wanted to thank You for sharing Your extraordinary knowledge as accessible as possible. Not to mention having no income for doing this... Hats off to You.
Hardcore? Please! I'm just a big fan, you really are an inspiration to higher level developers like myself. I tuned into one of your live streams over a year ago, and it was like a celebrity was talking to me directly when you answered a few of my questions on the stream. One thing I do miss was the long play streams where I could put you on in the background and I could work away be productive knowing someone else in the room was being productive also. I believe you used to do this yourself with other youtubers? Keep being awesome Robert!
Hi, I just found your videos. I have experience with operating systems, but not that much experience with hardware. This is a very cool project. idk if someone else mentions this in a future video's comments, but I have answers to some of your questions. SBREAK is used to implement breakpoints. When you set a breakpoint the debugger finds the first assembly instruction that is on the breakpointed line and then replaces it with the breakpoint instruction. (On x86 the breakpoint instruction is 0x03). When the breakpoint instruction is hit the process being debugged is stopped and the debugger is notified by the OS. When the user presses continue in the debugger the instruction that was replaced with the breakpoint is emulated in software and the registers/memory are modified to be as they would be if the instruction were executed by the CPU. SCALL and other software interrupt generating instructions are usually used by user processes to get services from the OS, but they are also frequently used before the OS is loaded. A computer's BIOS usually provides interrupts that are used by the bootloader to load files from storage before the bootloader/OS is able to load its drivers. Asynchronous interrupts are interrupts that do not occur as part of the execution of the current instruction. eg: timer interrupts, hardware interrupts, IO, interrupts caused by other cores in multi-core systems that are handled by this core, etc. Synchronous interrupts are interrupts that occur as part of an instructions execution. eg: SCALL, SBREAK, illegal instruction, unmapped memory, unaligned memory access, unaligned jumps, etc. Usually in simple CPU implementations, asynchronous interrupts cause cause a latch to be set, and at the start of each instruction's execution the latch is checked. If the latch is set then the asynchronous interrupt is handled, otherwise the instruction is executed. Furthermore, disabling interrupts DOES NOT mean that interrupts that arrive while interrupts are disabled are ignored. Instead, the latch will stay set until interrupts are re-enabled, then the CPU will handle the interrupt. With regard to synchronous interrupts, most CPU implementations will not write results to registers/PC/memory/IO until the end phase of an instruction, when it is known that the instruction will not fault. That way if an instruction is found be faulty the CPU can discard the work it has done and trap to the handler immediately. My last comment is that the illegal instructions should not result is the CPU halting. The RISC-V ISA explicitly contemplates setting a handler for unsupported instructions, reading the faulting instruction, emulating it in software, and returning to the execution. This would allow a RISC-V CPU w/o HW support for extensions like division/multiplication to have compatibility with code that uses those instructions through emulation. Sorry, if this was too long. Keep up the amazing videos. :)
you are NOT a true fan if you have watched this far in the series you are ONLY a true fan if you: - Have multiple flat blades - Spin around really fast - Move air around
24:30 this seems slightly dangerous - I'd relax it to rs1: [0, 1], rs2: [0, 1, 2, 3], rd: [0, 1, 2]. This way all the possible register aliasing problems are checked too. *edit: allow rs2, not rd, to use register 3. this improves performance on instructions that do not use rs2
Yes, I was actually thinking about that, but then the thought flew away somewhere, maybe under the sofa, and I couldn't find it again. You reminded me! It is a good idea to check that all registers may also be the same.
@30, about the ECALL. You normally serve ALL interrupt sources before returning: all exceptions and/or multiple interrupts. ERET will then always go to the right place and all interrupts will have been served including an possile ECALL.
If ECALL/EBREAK are your only non-fatal exceptions, do you even need to materialize an exception line for them? Have fatal exceptions raise an actual wire, and have those be directly handled on the sequencer.
An argument for running it on an xxxl compute optimized aws instance at the end, when you are ready to do full induction. The argument is: it will take slightly less than a year wall time to finish.
An idea: Couldn't you do bounded model checking as a "crude" check, like you're doing now. Then once you have the entire system built, without errors on that check. Then you go back and formally verify the code with proffmode, retroactively adding the asserts so the instructions doesn't change on you? I ofcause realize, that this will be very time consuming and tedious, and maybe even difficult because of the vast codebase. Although it would be a great way to iron out any bugs, and also a good quality assurance of the code itself and the code comments :)
Yes, usually cover first, to make sure it does what you think it does, then BMC to see if there's something you missed, then prove to make sure that unbounded checking also works.
I was just thinking about how long would it take to formally verify it in the proof mode. And wow few days is a lot. Also I cant wait for when you start to convert the code into real logic gates and other parts. The nmigen code is just too confusing to me and I get lost fast. But I get that formal verification is awesome and powerful.
I admit to not understanding the "map it to the formal spec" suggestion, but it does sound interesting. Would it be possible to ask you to elaborate on your proposal?
@@ivankrasin2399 there is a formal definition of the correct behavior of a RISC-V implementation, which could be combined with the LMARV model to validate it's behaviour.
@@microcolonel You mean the one that Claire Wolf put together? That's where I got the idea from, but since I am not implementing the full spec, I don't think I would be able to use the formal model.
If the core has Only one Interrupt Pin, then how does it recognize whether it is an Internal Interrupt or an External Interrupt? Does External Logic keep track of this
@22, you tell you are not supporting software interrupts but before you told you are going to support ecall, with is a software interrupt. Or am i confusing the two?
Couldn't you just make the return address from the interrupt + ebreak decrement PC by 4 or something? There's got to be a clean way to handle this, otherwise it probably wouldn't be this way in the spec...
I just acknowledged how underrated Your content is, compared to i.e. Ben Eater videos.
Yes, nMigen is definitely on more abstract level than gates and adder chips. It took me some time watching Your videos to become fluent enough, to get knowledge of the circuit design/operation details and faster understand what's the code doing. I guess knowledge entry barrier affect TH-cam reach algorithm, but there's nothing You can do about it - the topic is just uncommon.
I just wanted to thank You for sharing Your extraordinary knowledge as accessible as possible. Not to mention having no income for doing this... Hats off to You.
Happy to be one of your hardcore viewers 😸
Really looking forward to see how this turns out.
Hardcore? Please! I'm just a big fan, you really are an inspiration to higher level developers like myself.
I tuned into one of your live streams over a year ago, and it was like a celebrity was talking to me directly when you answered a few of my questions on the stream.
One thing I do miss was the long play streams where I could put you on in the background and I could work away be productive knowing someone else in the room was being productive also. I believe you used to do this yourself with other youtubers?
Keep being awesome Robert!
I should do another long stream :)
Hi, I just found your videos. I have experience with operating systems, but not that much experience with hardware. This is a very cool project. idk if someone else mentions this in a future video's comments, but I have answers to some of your questions.
SBREAK is used to implement breakpoints. When you set a breakpoint the debugger finds the first assembly instruction that is on the breakpointed line and then replaces it with the breakpoint instruction. (On x86 the breakpoint instruction is 0x03). When the breakpoint instruction is hit the process being debugged is stopped and the debugger is notified by the OS. When the user presses continue in the debugger the instruction that was replaced with the breakpoint is emulated in software and the registers/memory are modified to be as they would be if the instruction were executed by the CPU.
SCALL and other software interrupt generating instructions are usually used by user processes to get services from the OS, but they are also frequently used before the OS is loaded. A computer's BIOS usually provides interrupts that are used by the bootloader to load files from storage before the bootloader/OS is able to load its drivers.
Asynchronous interrupts are interrupts that do not occur as part of the execution of the current instruction. eg: timer interrupts, hardware interrupts, IO, interrupts caused by other cores in multi-core systems that are handled by this core, etc. Synchronous interrupts are interrupts that occur as part of an instructions execution. eg: SCALL, SBREAK, illegal instruction, unmapped memory, unaligned memory access, unaligned jumps, etc.
Usually in simple CPU implementations, asynchronous interrupts cause cause a latch to be set, and at the start of each instruction's execution the latch is checked. If the latch is set then the asynchronous interrupt is handled, otherwise the instruction is executed. Furthermore, disabling interrupts DOES NOT mean that interrupts that arrive while interrupts are disabled are ignored. Instead, the latch will stay set until interrupts are re-enabled, then the CPU will handle the interrupt.
With regard to synchronous interrupts, most CPU implementations will not write results to registers/PC/memory/IO until the end phase of an instruction, when it is known that the instruction will not fault. That way if an instruction is found be faulty the CPU can discard the work it has done and trap to the handler immediately.
My last comment is that the illegal instructions should not result is the CPU halting. The RISC-V ISA explicitly contemplates setting a handler for unsupported instructions, reading the faulting instruction, emulating it in software, and returning to the execution. This would allow a RISC-V CPU w/o HW support for extensions like division/multiplication to have compatibility with code that uses those instructions through emulation.
Sorry, if this was too long. Keep up the amazing videos. :)
you are NOT a true fan if you have watched this far in the series
you are ONLY a true fan if you:
- Have multiple flat blades
- Spin around really fast
- Move air around
24:30 this seems slightly dangerous - I'd relax it to rs1: [0, 1], rs2: [0, 1, 2, 3], rd: [0, 1, 2]. This way all the possible register aliasing problems are checked too.
*edit: allow rs2, not rd, to use register 3. this improves performance on instructions that do not use rs2
Yes, I was actually thinking about that, but then the thought flew away somewhere, maybe under the sofa, and I couldn't find it again. You reminded me! It is a good idea to check that all registers may also be the same.
Looking forwards to the next video!
@30, about the ECALL. You normally serve ALL interrupt sources before returning: all exceptions and/or multiple interrupts. ERET will then always go to the right place and all interrupts will have been served including an possile ECALL.
Do you think you might do proof by induction later? Once the project is nearly complete?
Thanks for keeping us updated. This is such a cool project
It might be a good idea to do that at some point.
If ECALL/EBREAK are your only non-fatal exceptions, do you even need to materialize an exception line for them? Have fatal exceptions raise an actual wire, and have those be directly handled on the sequencer.
An argument for running it on an xxxl compute optimized aws instance at the end, when you are ready to do full induction.
The argument is: it will take slightly less than a year wall time to finish.
An idea:
Couldn't you do bounded model checking as a "crude" check, like you're doing now.
Then once you have the entire system built, without errors on that check. Then you go back and formally verify the code with proffmode, retroactively adding the asserts so the instructions doesn't change on you?
I ofcause realize, that this will be very time consuming and tedious, and maybe even difficult because of the vast codebase. Although it would be a great way to iron out any bugs, and also a good quality assurance of the code itself and the code comments :)
Yes, usually cover first, to make sure it does what you think it does, then BMC to see if there's something you missed, then prove to make sure that unbounded checking also works.
No... you're hardcore!
I was just thinking about how long would it take to formally verify it in the proof mode. And wow few days is a lot. Also I cant wait for when you start to convert the code into real logic gates and other parts. The nmigen code is just too confusing to me and I get lost fast. But I get that formal verification is awesome and powerful.
Excellent, it'd be cool to go back and map it to the formal spec. :+ )
I admit to not understanding the "map it to the formal spec" suggestion, but it does sound interesting. Would it be possible to ask you to elaborate on your proposal?
@@ivankrasin2399 there is a formal definition of the correct behavior of a RISC-V implementation, which could be combined with the LMARV model to validate it's behaviour.
@@microcolonel You mean the one that Claire Wolf put together? That's where I got the idea from, but since I am not implementing the full spec, I don't think I would be able to use the formal model.
If the core has Only one Interrupt Pin, then how does it recognize whether it is an Internal Interrupt or an External Interrupt? Does External Logic keep track of this
@22, you tell you are not supporting software interrupts but before you told you are going to support ecall, with is a software interrupt. Or am i confusing the two?
Couldn't you just make the return address from the interrupt + ebreak decrement PC by 4 or something?
There's got to be a clean way to handle this, otherwise it probably wouldn't be this way in the spec...
30:14 no you