Congratulations Clément! actu.epfl.ch/news/superpower…

What we are building will change how mission-critical software is built and verified Here's Rick & Morty to tell you all about @workersio

new job just dropped: Automation Engineer and the funny part is nobody can ask for "10 years of experience" because the job basically didn't exist Serval is already seeing companies hire people specifically for this feels like one of those job titles we're going to see everywhere in a few years:

required reading to get on here talking about formal verification

Job search in AI + FV/compilers #4 I look young, but I’ve been around a little. One thing I’ve been noticing during this job hunt is how hard it is to convey the breadth of my experience in a technical interview. You pick one or two stories, try to make a point, and suddenly the interview is over. There’s a lot that never comes up. So today I want to get a little more technical and tell you about my time at SiFive. There’s floating-point arithmetic, a bug that wasn’t a bug, and a bet that I still intend to collect on. Back in 2016, I went to OPLSS and had such an incredible time that I decided I wanted to return to the US for graduate school. Once I graduated, I spent my time studying for the TOEFL and GRE, working on applications, recommendation letters, and all that stuff. After submitting everything, I randomly saw an email on the Coq mailing list: a company in the Bay Area was hiring a Coq developer. That really grabbed my attention, so I emailed them asking whether they took interns. Next thing I knew, Murali Vijayaraghavan was on a call with me, opening Coq and asking me to prove a version of the pigeonhole principle. I didn’t finish on the call. But he was cool about it and told me to email him the proof once I was done. I got off the call, worked my ass off, and sent it back. Apparently he liked it, because they flew me out to California, and we got started. That first week, boy, I don’t think I’ve ever felt dumber in my life. Murali was showing me the Kami infrastructure, and there was so much to absorb. I would get to the office before him just to review what he had shown me the previous day and do hexadecimal arithmetic in my little notebook so I could follow what he was talking about. Little did I know that this was just my first taste of the entire grad school experience. But eventually things started clicking, and I was implementing floating-point specifications and checking them against the hardware. Let me explain a little about the setup. Kami is a hardware-description language deeply embedded in Coq. You can describe circuits, reason about them using its formal semantics, and compile those descriptions to Verilog: github.com/sifive/Kami The implementation we were checking was written in Chisel, which lets you describe and generate hardware using Scala. So you get to use all kinds of high-level programming to build circuits, which is pretty cool if you ask me. On my side, I was writing specifications in Kami. We would compile those to Verilog and use JasperGold for formal equivalence checking against the hardware generated from Chisel. That was a big part of my job: getting the specifications right, setting up the comparisons, and investigating why things didn’t agree. I worked on rounding, conversions between floating-point formats, conversions to and from integers, and fused multiply-add. Some of the completed equivalence checks had explicit restrictions on the recoded exponent, so the scope of each result mattered. The floating-point project is here: github.com/sifive/FpuKami I remember spending a LOT of time on multiply-add. Looking at ModMulAdd.v certainly brings back memories: github.com/sifive/FpuKami/bl… One annoying detail: as I remember it, the repository was moved at some point, and my contributions didn’t carry over into the history you see there now. So I don’t show up as a contributor. It has also been eight years, and I can’t tell you which parts of the current code are still mine. That particular structure does ring a bell, though! Anyways, I promised some technical content, so let me say this up front: floating point is NASTY. You have a sign, a significand, and an exponent, but only so many bits to store them. Most real numbers aren’t exactly representable. So you need rounding rules, and then rules for what happens near the limits of the format, and then exception flags—and every one of those details is part of the behavior you’re trying to get right. Fused multiply-add, for example, computes a × b + c with a single final rounding. If you round the multiplication first and then do the addition, you can get a different answer. But the example I want to tell you about came from converting a 64-bit float to 32 bits. In June 2018, I sent an email reporting what I thought was a bug. One of my inputs was 0x380fffffc0000001. With rounding toward positive infinity, the result was: 0x00800000 That’s the smallest positive NORMAL binary32 number, 2⁻¹²⁶. But the underflow and inexact flags were both set. Now, we were detecting tininess AFTER rounding. And the result was normal. So why on earth was it raising underflow? I found related cases with other rounding modes too. SoftFloat showed the same behavior. I wrote it up and sent it around, pretty convinced something was wrong. John Hauser replied and pointed me to a FAQ entry he had published less than two weeks earlier. Turns out the implementation was right. Here’s the subtlety: “detect tininess after rounding” doesn’t simply mean “look at the final floating-point result and check whether it’s subnormal.” For the tininess test, you round to the destination precision as though the exponent range were unbounded. Right at the boundary, that hypothetical rounded value can still be below the normal range. But rounding the original value to an actually representable binary32 number can give you the smallest normal number. So you can have a normal final result AND still satisfy the tininess condition. If the result is also inexact, underflow is required. That's floating points for you 😒 The FAQ walks through an example: jhauser.us/arithmetic/SoftFl… I thought I had found a bug in the implementation. What I had actually found was a hole in my understanding of the specification. And honestly, I think that’s a pretty good verification story. You can have a concrete input, a surprising result, and a very convincing explanation of why it must be wrong—and still be the one who needs correcting. But there was another thing I kept questioning: the compiler. We were taking something written in Kami, compiling it to Verilog, and using the result in our equivalence checks. So naturally I wanted to make sure the compilation path was behaving correctly too. During those first few weeks, I kept being extra careful about this. At some point, as I remember it, Murali got a little tired of my questions and made me a bet: if I found a bug, I could ask for whatever I wanted. And ladies and gentlemen, about three months later, I found one. He still owes me a really good reference letter because of that. Looking back, I like that these two stories happened during the same internship. I was learning to question the infrastructure while also learning that my own reading of the standard needed just as much scrutiny. That’s a lot of what I enjoy about formal verification. You get to follow a disagreement all the way down: through the specification, the implementation, the compiler, and the assumptions you put into the check. Sometimes you find a bug. Sometimes you discover that a sentence in the standard means something much more precise than you thought. Anyways, that’s a little of what’s hiding behind “floating-point verification at SiFive” on my CV—and some of the experience I’m bringing to my search for work in formal verification, compilers, and AI-assisted verification.