18 ms·
Lion: A formally verified, 5-stage pipeline RISC-V core
- ACAVJW4H 6y agoIs anyone aware of a manufactured and distributed fully open-source risc-v CPU? Maybe one using skywater-pdk
- gchadwick 6y agoTake a look at the projects going into the skywater-pdk shuttle https://efabless.com/open_mpw_shuttle_project_mpw_one https://efabless.com/open_mpw_shuttle_project_mpw_one there are multiple RISC-V CPUs. Manufacturing is currently in progress. 'Distributed' is the tricky point, what counts as 'Distributed' in your eyes? The Skywater MPW is producing ~50 devices for each project I think, I'm sure some of those containing RISC-V CPUs will be distributed around to a few people but there won't be easy general availability of just being able to buy one.
- baybal2 6y agoSkywater can do much more, but the stupid "harness" eats tons of space, a majority of it.
- gchadwick 6y ago> but the stupid "harness" eats tons of space, a majority of it. I can't blame them for wanting the harness. By having a constant across everything that tapes-out where there are issues with dead or partially working chips it should be easier to track down what's going wrong. The specific project or something more general with the library, process or tools. There's lot of designs from people new to ASIC flows or without much experience in them, the harness allows efabless to help support people with bring-up. Yes for an experienced ASIC designer it may be an annoyance but you are getting entirely free tape-outs of this. If you want to pay efabless or another company for a tape-out you can do your own thing with skywater PDK. As for the majority of space are you sure? Take this project with layout photo: https://efabless.com/projects/34 https://efabless.com/projects/34 to my eye the 'project' area which is the larger of the two distinct rectangular regions (the bottom smaller one is the harness) looks to be getting the lion's share of the area.
- deleted 6y ago[deleted]
- gchadwick 6y agoLooks like an interesting project, though I would note they've just done the 'easy' part so far. As far as I can see it's base RV32I no CSRs, exception/interrupt support, PMP or other MMU. These are the features where the bugs tend to lie and also complicate your formal verification. Still you have to start somewhere, I will be interested to see their progress as they tackle the things listed above.
- tachyonbeam 6y agoI'm kind of skeptical of formal verification. For instance, it wouldn't have prevented bugs like spectre or meltdown. It can only tell you that your implementation matches some spec, but your spec can still be incomplete or buggy. At the end of the day, there's no substitute for extensive real-world testing.
- sanxiyn 6y agoFormal verification catches a lot of bugs, some of which won't be caught by usual testing. It's still valuable even if it doesn't catch all bugs. I just think it as a more efficient way to run exhaustive testing.
- aseipp 6y agoThis is such a funny post because formal verification techniques tend to see a lot of success in the hardware world, from lightweight ones to heavy ones, much more so than software, because many behaviors can be bounded over some finite amount of time (or inductively proven over all time, or equivalence checking, etc), and because hardware designs have massive incentives to get it right the first time and not blow a billion dollars on a mistake. If you write the basic cookie cutter "but but but, it's all just a spec, so we can't ever know anything!!!" it should be a requirement to submit a 5 page essay describing the algorithms/theory behind formal verification techniques, so they can prove they understand them, as opposed to only "understanding" how to make cookie-cutter bait posts.
- DSingularity 6y ago
- amelius 6y agoDoes this verify for side-channel attacks?
- 0xTJ 6y agoI don't see why it would. Verified doesn't mean unhackable (including physically), it means correct.
- GregarianChild 6y agoI'm a bit reluctant to reply without having looked at the article in detail, but I feel confident that the answer must be negative! Why? Because the very concept of side-channel depends on attacker capability! For example, does your attacker have physical access to the processor or not? With physical access you can exploit channels like power consumption through differential power analysis, or shoot laser pulses at target transistors to flip them and induce the processor to leak secrets. OTOH, without physical access, those channels don't meaningfully exist and you need to rely on, for example, speculation failure attacks and exfiltration via cache timing. So what counts as a side-channel is attacker-capability dependent.
- londons_explore 6y agoA good middle ground is to say "no secret data should be leaked via timing of operations". Ie. a high security and a low security thread on the same CPU should not be able to get clues about what data the other has in its address space. Offering stricter protection than that is pretty hard - simply the fact that one thread is using the floating point units a lot and causing the CPU to throttle is an info leak, so I don't think it's possible to really prevent small leaks of flow control information.
- GregarianChild 6y agoThis is a good middle ground, but ... ... leakage by timing side-channels depends in parts on how accurate your time-measurements are (e.g. Javascript's timer resolution was degraded, in order to make transient failure attacks like Spectre harder [1]). I totally agree with your second point and believe, but cannot prove, that no current processor with any competitive performance is free from timing side-channels, the best we can currently do is put upper bounds on leakage rate. There are just so many other timing side channels, e.g. port contention [2]. They just keep popping up ... Another dimension is the very meaning of thread. Presumably, as an end-user, you care about the threads/processes that the operating systems defines. But they don't map one-to-one to hardware threads, cores etc. Indeed I would argue that processors don't have threads in the sense that end-users care about. So the relevant security property must be regarding a hardware/software interface. Quite how to nail down this isolation property is active research I think. See e.g. [3] for work from 2016 in this direction. Yet another dimension to this is through passwords and similar mechanisms: presumably you want to allow doing things like "sudo" so a low-priority thread can increase priority, provided the former knows the right password. But the very act of supplying a false password, leaks a tiny bit of information (that can be quantified in terms of Shannon-style information theory) about the password's search space. [1] https://hackaday.com/2018/01/06/lowering-javascript-timer-resolution-thwarts-meltdown-and-spectre/ https://hackaday.com/2018/01/06/lowering-javascript-timer-re... [2] A. Bhattacharyya, A. Sandulescu, M. Neugschwandtner, A. Sorniotti, B. Falsafi, M. Payer, A. Kurmus, SMoTherSpectre: Exploiting Speculative Execution through Port Contention. https://arxiv.org/abs/1903.01843 https://arxiv.org/abs/1903.01843 [3] D. Costanzo, Z. Shao, R. Gu, End-to-end verification of information flow security for C and assembly programs. https://6826.csail.mit.edu/2019/papers/certikos-sec.pdf https://6826.csail.mit.edu/2019/papers/certikos-sec.pdf
- fuklief 6y agoSo what kind of formal verification is it ? Is it proof assistant, model checking ? And what does it verify ? It's not really clear from a first glance.
- sanxiyn 6y agoThis uses riscv-formal. The default way to use riscv-formal is bounded model checking. It verifies all single instructions and some consistency checks, e.g. register read matches last logical register write in presence of reordering.
- the_duke 6y agoWouldn't many bugs only surface in multi-instruction and status register interactions? But those are also probably way harder to verify.
- sanxiyn 6y agoConsistency checks do check multiple instructions. Status registers are work in progress.
- GregarianChild 6y agoThat's interesting! What kind of consistency checks (other than register state being preserved by commands that do not write to the register in question)? Is there some standard best practise?
- fctorial 6y agoWhat is this project? Can anyone ELI5?
- addaon 6y agoA core is the part of a processor that actually runs instructions -- a processor consists of one or more cores, peripherals, etc. Software consists of a sequence of instructions ("add A and B") that, together, accomplish a goal. But even perfect software is only correct if the core that it runs on is correct. Historically, there have been a small number of high-profile correctness issues in various processor cores (e.g. Intel's Pentium FDIV bug), and almost every processor has a number of small correctness issues documented in errata -- or, not yet discovered. In designing and building a processor, correctness is important, and hard -- generally, much more time is spent testing and demonstrating correctness of a core than actually designing it. Formal verification aims to not just test and demonstrate correctness, but prove it. That is, under certain assumptions, one can prove that, for example, the actual transistors used to implement "add A and B", when connected in the intended way, have the same semantics ("do the same thing") as "add A and B". In the extreme case, formal methods can replace testing. In practice, they can replace some portion of testing; but those assumptions that they're built on can be a bit shaky. Formal methods can also be /hard/ -- it can take more time to prove something correct than to just test it thoroughly enough to convince everyone. But, when done right, it does lead to higher confidence overall.
- marcodiego 6y agoWhat is the chace of RISC-V becoming and x86 or arm alternative free from binary blobs and (IME|PSP)-like traps?
- coldtea 6y agoSlim. Somebody will have to build from high end designs, spend billions doing so, and those would be the same commercial companies, which (if adopt RISC-V) will add their own proprietary spin. https://twitter.com/marcan42/status/1366631459000258565 https://twitter.com/marcan42/status/1366631459000258565 https://twitter.com/marcan42/status/1366631470110965760 https://twitter.com/marcan42/status/1366631470110965760 https://twitter.com/marcan42/status/1366631471188828164 https://twitter.com/marcan42/status/1366631471188828164
- rjsw 6y agoThe BeagleV [1] looks much like many ARM dev boards. It will probably still have a binary blob for the GPU though, they are proposing to use an Imagination design. [1] https://beagleboard.org/beaglev https://beagleboard.org/beaglev
- matthewmacleod 6y agoProbably minimal. There is nothing preventing an x86 or ARM CPU without these today, and CPU architecture has ~zero impact on the business decision to rely on binary blobs or proprietary system controllers.
- TrueDuality 6y agoThere is also nothing preventing someone making a hardware RISC-V core from including additional hardware, custom instructions, or proprietary blobs.
- Narishma 6y agoMaybe in a couple of decades.
- spamizbad 6y agoI think RISC-V, without some additional extension(s) and maybe some rework, will have trouble scaling the levels necessary to be competitive performance-wise with smartphone devices or data centers the way ARM v8 is. Erin Shepherd did a good write-up why: https://gist.github.com/erincandescent/8a10eeeea1918ee4f9d9982f7618ef68 https://gist.github.com/erincandescent/8a10eeeea1918ee4f9d99... David Chisnall’s critique is also worth a read: https://lobste.rs/s/icegvf/will_risc_v_revolutionize_computing#c_8wbb6t https://lobste.rs/s/icegvf/will_risc_v_revolutionize_computi... With that said for applications that are sensitive to power or transistor counts it wouldn’t surprise me if it takes over the low to midrange MCU market 10 years from now.
- random_savv 6y agoSo if I wanted to take this and start selling processors, how far am I? What comes next?
- seanmclo 6y agoDecide what process node this is aiming for, circuit layout, synthesis, working with a nanofab to actually build the thing, and assuming that there are bugs in there still, multiple rounds of post silicon debug. It's a long and expensive road ahead if you want this as a real product.
- seanmclo 6y agoI've been looking for an alternative hardware description language to Verilog/SystemVerilog because they're not very readable languages. But after skimming this source code, my initial thought is that I hope Haskell doesn't take off. This is extremely difficult to read. Maybe I just don't know Haskell well enough, though.
- jeff_ciesielski 6y ago(From someone who is working on a rv32im implementation in Clash) I really love writing RTL in haskell when compared to verilog/vhdl, but as a language I think it suffers from the same thing a lot of other languages do: too many ways to do the same thing. Mix that with a language that encourages meta-programming and you've got yourself a recipe for every complex haskell project basically becoming it's own little DSL. It's also often made worse because so much haskell is written by type-theorists and mathematicians churning out symbol-soup without a thought for the rest of us plebs. IMO this is actually pretty readable and the implementation is stitched together nicely. There are some haskell/ml-isms like lenses/monad transformers/partial functions sprinkled in there that complicate a casual read-through, but if you've got a grasp on those most of this is reasonably clear. It isn't the most complex beast (as others have pointed out, it skips things like the Zicsr and M extensions which add significant complexity) but it could serve very well as say, a companion core to some more complex piece of hardware. Perhaps one that requires reconfigurable logic that would be impractical in silicon but doesn't require realtime interrupts or fast math?
- GregarianChild 6y agoThe RISC-V ecosystem is quite fond of Chisel [1]. A new kid on the block is LLHD [2]. There are numerous others. [1] https://github.com/lowRISC/chisel https://github.com/lowRISC/chisel [2] https://llhd.io/ https://llhd.io/
- gpanders 6y agoI want Chisel to succeed so badly. I'm so sick and tired of writing VHDL. Verilog is no better. Also it looks like LLHD is perhaps analogous to LLVM in that they offer an intermediate representation instead of providing a language that you code in yourself. Chisel also offers this via FIRRTL [1]. I can't decide whether to be excited about the fact that there are multiple ideas in this space or frustrated that these disparate teams aren't simply collaborating. [1]: https://github.com/chipsalliance/firrtl https://github.com/chipsalliance/firrtl
- herodoturtle 6y ago"RISC architecture is gonna change everything" :)
- msla 6y ago"Posted from my ARM-based cell phone." Or, hell, some ARM-based Mac, these days.
- UncleOxidant 6y agoHadn't heard of the VELDT board that this design targets, but it looks like it's based on the Lattice ICE40 which means you can use the open source yosys/symbiflow tools.
- vzaliva 6y agoThe term "formally verified" could be misleading. Some people assume it means "100% bug free". Whenever someone claims something is formlally verified one should ask what properties were verified exactly. In this work the approach they use (bounded model checking) could find some bugs on a subset of RISCV archictecure they formalized. I recommend looking at their slides for better understanding of the scope of the work: http://www.clifford.at/papers/2017/riscv-formal/slides.pdf http://www.clifford.at/papers/2017/riscv-formal/slides.pdf Nevertheless it is definetely a very impressive work and pracrically useful.
- mhh__ 6y agoThere are many (probably apocryphal) tales of "formally" verified systems being turned on then immediately crashing for this very reason
- capableweb 6y agoIn the end it's up to the reader to understand what it means. Many think "100% test coverage" is something you should strive towards as they think it means less bugs while in reality it just means that the test runner at one point or another accessed that line of code.