Finding Hardware Bugs - Computerphile Transcript, AI Summary & Key Points

00:00 What my research team and I have been most interested in in the last few years is trying to make EDA tools more reliable. So, by EDA tools, I mean these are the the tools that hardware engineers use to make hardware. The basic kind of flow would be your your your hardware engineer would come up with a design for what they want the functionality of your hardware to be.

00:29 Uh and they'll agonize over making sure it's all correct and it's efficient and all these good things. Then, they will feed that human-readable design into these EDA tools. So, EDA is electronic design automation and they they they have fancy names like elaborators and synthesis tools and place and route is is one of them. So, it's kind of a sequence of tools that And eventually, what comes out at the the far end um is is something that could literally go on a piece of hardware like we have here.

01:05 So, this is So, underneath this big heat sink is an FPGA. So, it's a computer chip that you can implement whatever design you like. FPGAs are sitting in a a weird in-between state between you've on the one hand, you've got sort of traditional computer chips where their functionality is completely fixed at the time that they're manufactured. Uh so, they might be called ASICs, so application-specific integrated circuit.

01:34 Um on the kind of other hand, you might have um a processor, which is a sort of general-purpose processor, CPU, and that can do whatever you like because you just need to feed it a series of instructions. >> software. >> The right software, exactly. And it will do whatever you like. The FPGAs are sort of in between that because they are it it is it's just a computer chip, but it's set up in such a way that you can change what what those individual gates on the chip do um by feeding it a new uh implementation if you

02:12 like. Um so uh yeah, so it's it's sort of in between. And and that implementation, could you use the same FPGA for two different things or does does it get set what at some point? Is there like a point where you go I'm going to make this do that and now it is that? So so the FPGA stands for field programmable gate array. So array of these logic gates, field as in out in the field it can be reprogrammed.

02:39 Okay. So and it only takes, you know, a fraction of a second to to reprogram it and you can reprogram it any number of times you like. The goal of these EDA tools is um yeah, so uh a a hardware designer has what they want to to build, pass it through all of these tools and it will end up as at the end of the day it's a sequence of zeros and ones that you feed in through one of these ports on this board that will end up configuring that chip.

03:06 Okay. To do what you want it to do. Okay. And what we've been interested in is can we trust those tools to do the right thing? Right. Cuz as I said, the process is that this hardware design is hard. Um and the designer will spend ages agonizing over you know, getting the maximum possible performance and uh everything is working correctly in all of the possible edge cases.

03:39 And then they have to offload that design into this sequence of tools. Mhm. At which point you know, it's a it's like hopefully these tools are preserving what I designed so that what actually ends up on there is correct. When you say trusting, do you mean trusting in terms of kind of nefarious activities or do you mean just trusting in terms of hopefully this will do what I want it to do?

04:04 I'm I mean the latter. I mean I mean that if the EDA tool has a bug in it, that could cause bugs in your tool. It's It's like proliferation of bugs in a way. If there's a bug in the tool itself rather than anything you've done, that's a nightmare to debug. What we set out to do was um try to find bugs in in these EDA tools and the tool that we were particularly focusing on them in the projects that I talked about today um was the place and route tools.

04:38 So, this is the stage in the hardware design where you have Maybe I'll start I'll try drawing something. Um So, you have uh your design for your hardware. So, perhaps just do a very simple version. Maybe I have some sort of gate like that and maybe I have a inverter and maybe one more gate over here. And maybe my design says, "Right, what What I want the computation to do is connect that to that.

05:12 Maybe this is going to come round like that and these two are going to be fed by that. Maybe that's that's my hardware design." So, now I give that to the place and route tool and what that tool will do is it will say, "Right, so this gate here I'm going to put that maybe here on the uh on the FPGA. And this uh this OR gate maybe I'm going to locate that one there.

05:41 And this inverter, I think there's a good space for that just there. So, that's the placing. And then the routing would be right. I've got to make sure that this this component on the FPGA I've activated all of the routing machinery so that that links up to that and this bit it better link rounds to that in the correct way and I've got to mirror that connection like that.

06:02 That's got to connect to an input. So, the result of the place and route might look something like that. And we set out to try and find out does the tool always do this transformation correctly? We used a technique called fuzzing. So, it's a way of testing where you are basically generating a whole load of random inputs. So, what we did was we came up with a program that would produce random hardware designs.

06:26 Something like this just like what I drew here where I just put some random gates in. I connect them in a random way but magnify that up. Pretty big, quite complicated. There are a few subtleties to doing that because you've got to make sure that there are certain restrictions on you don't want to go having certain certain kind of loops would cause problems.

06:46 Probably what I drew here for instance is I I should that that doesn't look very good today. It looks a bit too too many cycles there. You've got to watch out for that kind of thing. But yeah, what we then have is a whole load of basically meaningless hardware designs but superficially valid. Feed them into the tool, see what comes out and compare what comes out with what went in using what's called an equivalence checker which itself is another EDA tool that people use and if the equivalence checker says actually

07:13 that's what's coming what's come out is not the same as what came in then we investigate and then we say all right, I think we might have found a bug. Okay. On that investigation, do you have to then get into the into the you know, the source code of whatever's doing the placing and the routing? Wow, yeah. So, this this is one of one of the things about the hardware design industry is it compared to um the more more software side mostly it's all commercial.

07:45 It's all closed source. There's no chance unless we actually work for these big chip companies, we're not looking at their source code. So, the best we can realistically do once we have a case where we've got some hardware design here that we can see is producing something that's not equivalent. Um best we can really do is just try and understand what is like what's the crux of the problem here.

08:10 Um So, can we minimize that design, chop away all of the bits that are not relevant to triggering the bug, and end up with a really small design maybe it's just got a handful of gates that still triggers the bug because that is that's our best attempt to understanding the the the the root of the bug, and we can file that as a bug report to the vendors.

08:34 So, this is a slightly simplified version of a bug that that we found. Um so, what the design had in it was So, the main component was it's called a lookup table, which is basically a a table. It has a whole bunch of rows in it, and each row has some data. And the way that you can use this lookup table is you have some input wires coming in that say which row of the table I would like to come out on this output wire.

09:14 Um I think they in this particular case there were maybe about four input wires. And again, in this randomly generated design, what we had was we had this input was fixed at a zero. Input was fixed also at a and one was a zero as well. And here we had a zero that was passing through an inverter. So, becoming >> gate. >> a not gate, yes. So, we had 0 0 0 1.

09:49 Which meant that we were requesting row one of this table to come out. Which is this row. Here, assuming that the first row is row zero. So, that was producing 0 0 in output Y. Um So, we gave a design basically like this with a couple of extra components here and there, but these were the main ones. We gave this design to the place and route tool. And what the place and route tool did was during placing and routing it it had an idea, or at least this is how we told told it among ourselves.

10:26 Um it had an idea that it doesn't need this inverter because it looked at the contents of this lookup table, and it said, "Well, look, row one, which is the one you're asking for, that's actually the same content as row zero." I wrote these zeros and ones quite carefully. Ah, okay. So, if that doesn't match if it's 0 1, it's going to give the same result in that instance.

10:48 >> Exactly. So, how about I just get rid of this inverter and just put a the zero here, that will send out this row instead of this row, but what comes out will be exactly the same, and I'm using fewer gates. So, you know, better energy efficiency, so it's smaller circuits. This is This is all good, right? So, the place and route tool thought it was being very clever with this.

11:10 Unfortunately, it had neglected that this was a slightly special lookup table, which has an additional couple of ports on the top. On the top of my diagram. Um this port here, if you set that high, then you're saying I would like to reconfigure the contents of this table. So, um you set the way you you do it you set that wire to go high and then this wire here you feed in a sequence like 0 1 0 1 1 0 etc.

11:44 And those sequence of zeros and ones will replace whatever's in this all of these entries in the table. >> the look up table. >> that's exactly what you call it. It's a It's a dynamic look up table. Right. Uh or dynamically reconfigured look up table is the fancy name for it. What this uh person or tool had failed to notice um is that this uh wire here was constantly set to high which meant that whatever was coming in on this wire was constantly repopulating this table with well whatever was whatever this wire was

12:16 connected to on some external input which means that although the initial contents of the table was such that that inverter could be removed once new data has come in you can't make that same assumption. So, it was completely wrong to remove that inverter and that was the crux of the bug. I think there is plenty of scope to continue studying these uh EDA tools and there are lots of EDA tools and I think there's plenty of scope for developing new techniques to find more bugs in more tools.

12:42 You certainly could carry on doing this uh this kind of work for a while. But, the other thing that we've been looking at kind of concurrently with this is saying well you know is it possible to build different EDA tools that do not have bugs in? Which on the face of it maybe seems a bit a bit ambitious um but there there is um uh there are these techniques uh called formal verification or foundational verification and it it's it's basically about saying can we make a mathematical proof that this piece of software and

13:23 ultimately the EDA tool is just a piece of software um can we make a mathematical proof that that software does what it's supposed to do, which is, you know, always preserve your design in this case. Um, and you prove it just like a mathematical theorem. Um, you know, the the story I the way I um talk about this often is you imagine, you know, a mathematician who has a um uh come up with a new proof of I don't know if it's Fermat's Last Theorem or some some famous theorem, and they present their their proof, and what

13:56 it consists of is um oh, when I tried out the theorem on a whole loads and loads and loads of numbers, and it worked every time. It it it the two sides lined up. The other mathematicians would laugh at them. Now, that that doesn't count. It has to be a general watertight argument that works for all possible numbers. Um well, you know, the state of building software is basically we we we write the software, we run loads and loads of tests through it, see that it seems to be giving the right result, and call it a day.

14:33 Um, what the world of formal verification is saying is, well, can we take those ideas from math and actually make a theorem about this piece of software that says it really will always do the right thing. So, this is what we've been trying to do for the EDA tools. So, we've got So, one project from a couple of years ago was building a verified synthesis tool.

14:55 We're currently working on building a verified equivalence checker. That was the EDA tool that would check your design before and after some transformation. Um so, the and if if that all works out, then all this bug finding techniques, they should become a bit more redundant. With maths, let's be honest, you know, these theorems or things they're trying to prove, there could be thousands of bits of computation in a in a program, how can you are they all interrelated connect together?

15:26 Surely it's an impossible task compared to say mathematics and that's you know me but not being down on mathematics. I just think there's you know it's there's just so much more to it. Yes, no no that's very completely correct. Fermat's Last Theorem for instance my example just then um exceedingly concise statement but incredibly deep and you know it takes enormous expertise to be able to prove that kind of thing.

15:56 And you're right that any substantial piece of software is just inherently you know it's big and so if you imagine turning that into a mathematical theorem, you're certainly not going to get anything that fits on a mathematician's blackboard. But it tends not to be anywhere near as deep. It's big because that that whole theorem has got to capture the source code of the program the how the programming language in which you've written the program works, the something about the computer that you're running that program on.

16:28 You've got to capture all of this. Imagine writing that out as a theorem is is is ridiculous. Um but yeah the hope is that then when it comes to actually proving that theorem it should nothing's easy but it's it's not the kind of it's not like proving Fermat's Last Theorem. And indeed um because so and the and the way you can get around the fact that it's so cumbersome is you use a computer.

16:54 Maybe you saw this coming but um I was hoping that was where we're going. Indeed. So so we you have nowadays these these um they're basically programming languages for proof. Yeah, I think we've used some of them on the channel Lean and things like this before. Indeed. So you've got Lean, you've got Rock, you've got Isabelle and and a few others. So I think of these as programming languages for doing mathematical proofs.

17:19 Um and they're programming languages in the sense that it means that the computer can understand the proof and the computer token it means that the computer can help you write the proof at least fill in the the boring details. You know, you know, if you've got some massive case split you need to do the computer can help you generate all of those cases.

17:35 Um and it can also check the proof for you. Um So, yeah, that that's I think ultimately where we're where we're heading. The fuzzer is going to generate some program. So, what's in this program is going to be randomly determined by the fuzzer. However, the program is going to be an entirely deterministic program. We can give this program to GCC. We can give it to clang.