[Script Info]
Title: 
[Events]
Format: Layer, Start, End, Style, Name, MarginL, MarginR, MarginV, Effect, Text
Dialogue: 0,0:00:00.00,0:00:15.74,Default,,0000,0000,0000,,{\i1}34c3 intro{\i0}
Dialogue: 0,0:00:15.74,0:00:22.80,Default,,0000,0000,0000,,Herald: The next talk is called "End-to-\Nend formal ISA verification of RISC-V
Dialogue: 0,0:00:22.80,0:00:28.41,Default,,0000,0000,0000,,processors with riscv-formal". I have no\Nidea what this means, but I'm very excited
Dialogue: 0,0:00:28.41,0:00:33.54,Default,,0000,0000,0000,,to understand what it means and Clifford\Npromised he's going to make sure everyone
Dialogue: 0,0:00:33.54,0:00:39.32,Default,,0000,0000,0000,,will. Clifford has been very known in the\Nopen-source and free-software... free-
Dialogue: 0,0:00:39.32,0:00:45.22,Default,,0000,0000,0000,,source... oh my gosh... free-and-open-\Nsource community and especially he's known
Dialogue: 0,0:00:45.22,0:00:50.30,Default,,0000,0000,0000,,for the project IceStorm. Please help me\Nwelcome Clifford!
Dialogue: 0,0:00:50.30,0:00:57.26,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:00:57.26,0:01:12.17,Default,,0000,0000,0000,,{\i1}inaudible{\i0}\NClifford: RISC-V is an open instruction
Dialogue: 0,0:01:12.17,0:01:17.19,Default,,0000,0000,0000,,set architecture. It's an open ISA, so\Nit's not a processor, but it's a processor
Dialogue: 0,0:01:17.19,0:01:22.86,Default,,0000,0000,0000,,specification -- an ISA specification --\Nthat is free to use for everyone and if
Dialogue: 0,0:01:22.86,0:01:26.79,Default,,0000,0000,0000,,you happen to have already implemented\Nyour own processor at one point in time,
Dialogue: 0,0:01:26.79,0:01:30.88,Default,,0000,0000,0000,,you might know that it's actually much\Neasier to implement a processor than to
Dialogue: 0,0:01:30.88,0:01:35.56,Default,,0000,0000,0000,,implement all the tools that you need to\Ncompile programs for your processor. And
Dialogue: 0,0:01:35.56,0:01:39.75,Default,,0000,0000,0000,,if you use something like RISC-V, then you\Ncan reuse the tools that are already out
Dialogue: 0,0:01:39.75,0:01:45.17,Default,,0000,0000,0000,,there, so that's a great benefit. However,\Nfor this endeavor we need processors that
Dialogue: 0,0:01:45.17,0:01:50.28,Default,,0000,0000,0000,,actually really compatible to each other:\NProcessors that implement the RISC-V ISA
Dialogue: 0,0:01:50.28,0:01:54.97,Default,,0000,0000,0000,,correctly. So, with many other ISAs, we\Nstart with one processor and we say "Oh,
Dialogue: 0,0:01:54.97,0:01:59.66,Default,,0000,0000,0000,,that's the processor" and later on, we\Nfigure out there was a bug, and what
Dialogue: 0,0:01:59.66,0:02:03.05,Default,,0000,0000,0000,,people sometimes do is, they just change\Nthe specification, so that the
Dialogue: 0,0:02:03.05,0:02:06.77,Default,,0000,0000,0000,,specification all fits the hardware they\Nactually have. We can't do something like
Dialogue: 0,0:02:06.77,0:02:09.86,Default,,0000,0000,0000,,that with RISC-V, but there are many\Nimplementations out there, all being
Dialogue: 0,0:02:09.86,0:02:14.44,Default,,0000,0000,0000,,developed in parallel to fit the same\Nspecification, so we want to have some
Dialogue: 0,0:02:14.44,0:02:20.67,Default,,0000,0000,0000,,kind of means to make sure that all these\Nprocessors actually agree about what the
Dialogue: 0,0:02:20.67,0:02:27.08,Default,,0000,0000,0000,,ISA specification is. So, what's formal\Nverification? Formal verification is a
Dialogue: 0,0:02:27.08,0:02:32.96,Default,,0000,0000,0000,,super-broad term. In the context of this\Ntalk, I'm talking about hardware model
Dialogue: 0,0:02:32.96,0:02:38.23,Default,,0000,0000,0000,,checking. More specifically, I'm talking\Nabout checking of so-called "safety
Dialogue: 0,0:02:38.23,0:02:43.16,Default,,0000,0000,0000,,properties". So, we have some hardware\Ndesign and we have an initial state and we
Dialogue: 0,0:02:43.16,0:02:48.54,Default,,0000,0000,0000,,would like to know if this hardware design\Ncan reach a bad state from the initial
Dialogue: 0,0:02:48.54,0:02:55.28,Default,,0000,0000,0000,,state. That's formally the problem that we\Nare trying to solve here. And there are
Dialogue: 0,0:02:55.28,0:03:00.18,Default,,0000,0000,0000,,two means to do that, two different\Ncategories of proofs that are bounded and
Dialogue: 0,0:03:00.18,0:03:05.09,Default,,0000,0000,0000,,unbounded proofs, and with the bounded\Nproofs we only prove that it's impossible
Dialogue: 0,0:03:05.09,0:03:07.72,Default,,0000,0000,0000,,to reach a bad state within a certain\Nnumber of cycles.
Dialogue: 0,0:03:07.72,0:03:12.41,Default,,0000,0000,0000,,So, we give a maximum bound for the length\Nof a counterexample and with unbounded
Dialogue: 0,0:03:12.41,0:03:18.24,Default,,0000,0000,0000,,proofs, we prove that a bad state can\Nactually never be reached. So, unbounded
Dialogue: 0,0:03:18.24,0:03:23.06,Default,,0000,0000,0000,,proofs are, of course, better -- if you\Ncan make an unbounded proof -- but in many
Dialogue: 0,0:03:23.06,0:03:28.56,Default,,0000,0000,0000,,cases, this is very hard to achieve, but\Nbounded proofs is something that we can
Dialogue: 0,0:03:28.56,0:03:35.88,Default,,0000,0000,0000,,do, so I'm talking about bounded proofs\Nhere for the most part. So, what's end-to-
Dialogue: 0,0:03:35.88,0:03:40.53,Default,,0000,0000,0000,,end formal verification? Because that's\Nalso in my title. So, historically when
Dialogue: 0,0:03:40.53,0:03:45.11,Default,,0000,0000,0000,,you formally verify something like a\Nprocessor, you break down the processor in
Dialogue: 0,0:03:45.11,0:03:49.55,Default,,0000,0000,0000,,many small components and then you write\Nproperties for each component and prove
Dialogue: 0,0:03:49.55,0:03:54.51,Default,,0000,0000,0000,,for each component individually that they\Nadhere to the properties and then you make
Dialogue: 0,0:03:54.51,0:03:59.29,Default,,0000,0000,0000,,a more abstract proof, that if you put in\Nsystem together from components that have
Dialogue: 0,0:03:59.29,0:04:04.23,Default,,0000,0000,0000,,this property, then this system will have\Nthe properties that you want. With end-to-
Dialogue: 0,0:04:04.23,0:04:10.34,Default,,0000,0000,0000,,end verification, we treat the processors\None huge black box and just ask the
Dialogue: 0,0:04:10.34,0:04:15.71,Default,,0000,0000,0000,,question "Does this one huge thing fit our\Nspecification? Have the properties that we
Dialogue: 0,0:04:15.71,0:04:22.19,Default,,0000,0000,0000,,want?" That has a couple of advantages:\NIt's much, much easier this way to take
Dialogue: 0,0:04:22.19,0:04:26.46,Default,,0000,0000,0000,,one specification and port it from one\Nprocessor to another, because we don't
Dialogue: 0,0:04:26.46,0:04:31.85,Default,,0000,0000,0000,,care about how the processor is built\Ninternally, and it's much easier to take
Dialogue: 0,0:04:31.85,0:04:35.97,Default,,0000,0000,0000,,the specification that we have and\Nactually match it to other specifications
Dialogue: 0,0:04:35.97,0:04:39.52,Default,,0000,0000,0000,,of the ISA, because we have a\Nspecification that says, what is the
Dialogue: 0,0:04:39.52,0:04:45.19,Default,,0000,0000,0000,,overall behavior we expect from our\Nprocessor. But the big disadvantage, of
Dialogue: 0,0:04:45.19,0:04:49.70,Default,,0000,0000,0000,,cause, is that it's computationally much\Nmore expensive to do end-to-end formal
Dialogue: 0,0:04:49.70,0:04:55.24,Default,,0000,0000,0000,,verifications and doing this end-to-end\Nverification of a processor against an ISA
Dialogue: 0,0:04:55.24,0:04:59.14,Default,,0000,0000,0000,,specification is something that\Nhistorically was always fueled as the
Dialogue: 0,0:04:59.14,0:05:03.55,Default,,0000,0000,0000,,textbook example of things that you can't\Ndo with formal methods, but fortunately
Dialogue: 0,0:05:03.55,0:05:08.67,Default,,0000,0000,0000,,the solvers... they became much better in\Nthe last couple of years and now if we use
Dialogue: 0,0:05:08.67,0:05:14.48,Default,,0000,0000,0000,,the right tricks, we can do stuff like\Nthat with the solvers we have nowadays.
Dialogue: 0,0:05:14.48,0:05:19.57,Default,,0000,0000,0000,,So, that's riscv-formal. riscv-formal is a\Nframework that allows us to do end-to-end
Dialogue: 0,0:05:19.57,0:05:24.46,Default,,0000,0000,0000,,formal verification of RISC-V processors\Nagainst a formal version of the ISA
Dialogue: 0,0:05:24.46,0:05:29.85,Default,,0000,0000,0000,,specification. So, riscv-formal is not a\Nformally verified processor. Instead, if
Dialogue: 0,0:05:29.85,0:05:35.23,Default,,0000,0000,0000,,you happen to have a RISC-V processor, you\Ncan use riscv-formal to prove that your
Dialogue: 0,0:05:35.23,0:05:40.98,Default,,0000,0000,0000,,processor confirms to the ISA\Nspecification. For the most part, this is
Dialogue: 0,0:05:40.98,0:05:46.12,Default,,0000,0000,0000,,using bounded methods. Theoretically, you\Ncould do unbounded proofs with riscv-
Dialogue: 0,0:05:46.12,0:05:52.23,Default,,0000,0000,0000,,formal, but it's not the main use case.\NSo, it's good for what we call "bug
Dialogue: 0,0:05:52.23,0:05:56.02,Default,,0000,0000,0000,,hunting", because maybe there is a\Ncounterexample that would show, that the
Dialogue: 0,0:05:56.02,0:06:02.51,Default,,0000,0000,0000,,processor could diverge from the desired\Nbehavior with 1000 or 5000 cycles, but
Dialogue: 0,0:06:02.51,0:06:06.67,Default,,0000,0000,0000,,usually, when you have something like a\Nprocessor and you can't reach a bad state
Dialogue: 0,0:06:06.67,0:06:11.86,Default,,0000,0000,0000,,within the very short bounds, you have\Nhigh confidence that actually your
Dialogue: 0,0:06:11.86,0:06:16.91,Default,,0000,0000,0000,,processor implements the ISA correctly.\NSo, if you have a processor and you would
Dialogue: 0,0:06:16.91,0:06:22.47,Default,,0000,0000,0000,,like to integrate it with riscv-formal,\Nyou need to do 2 things: You need to add a
Dialogue: 0,0:06:22.47,0:06:27.61,Default,,0000,0000,0000,,special trace port to your processor; it's\Ncalled the RVFI trace port -- riscv-formal
Dialogue: 0,0:06:27.61,0:06:31.79,Default,,0000,0000,0000,,interface trace port. And you have to\Nconfigure riscv-formal so that riscv-
Dialogue: 0,0:06:31.79,0:06:39.52,Default,,0000,0000,0000,,formal understands the attributes of your\Nprocessor. So, for example, RISC-V is
Dialogue: 0,0:06:39.52,0:06:44.77,Default,,0000,0000,0000,,available in a 32-bit and a 64-bit\Nversion. You have to tell riscv-formal, if
Dialogue: 0,0:06:44.77,0:06:51.02,Default,,0000,0000,0000,,you want to verify a 32-bit or 64-bit\Nprocessor. RISC-V is a modular ISA, so
Dialogue: 0,0:06:51.02,0:06:54.12,Default,,0000,0000,0000,,there're a couple of extensions and you\Nhave to tell riscv-formal, which
Dialogue: 0,0:06:54.12,0:06:59.35,Default,,0000,0000,0000,,extensions your processor\Nactually implements.
Dialogue: 0,0:06:59.35,0:07:04.51,Default,,0000,0000,0000,,And then there're a couple of other things\Nthat are transparent for a userland
Dialogue: 0,0:07:04.51,0:07:12.63,Default,,0000,0000,0000,,process, like if unaligned loads or stores\Nare supported by the hardware natively,
Dialogue: 0,0:07:12.63,0:07:18.01,Default,,0000,0000,0000,,because RISC-V... the spec only says, that\Nwhen you do an unaligned load or store,
Dialogue: 0,0:07:18.01,0:07:23.98,Default,,0000,0000,0000,,then a userspace program can expect this\Nload or store to succeed, but it might
Dialogue: 0,0:07:23.98,0:07:28.40,Default,,0000,0000,0000,,take a long time, because there might be a\Nmachine interrupt handler that is
Dialogue: 0,0:07:28.40,0:07:34.95,Default,,0000,0000,0000,,emulating an unaligned load store by doing\Nalligned loads and stores, but if we do
Dialogue: 0,0:07:34.95,0:07:40.85,Default,,0000,0000,0000,,this formal verification of the processor,\Nthen the riscv-formal framework must be
Dialogue: 0,0:07:40.85,0:07:44.99,Default,,0000,0000,0000,,aware: "What is the expected behavior for\Nyour course?", "Should it trap when it
Dialogue: 0,0:07:44.99,0:07:50.96,Default,,0000,0000,0000,,sees an unaligned load store or should it\Njust perform the load store unaligned?"
Dialogue: 0,0:07:50.96,0:07:54.25,Default,,0000,0000,0000,,So, what does this interface look like\Nthat you need to implement in your
Dialogue: 0,0:07:54.25,0:07:59.49,Default,,0000,0000,0000,,processor if you would like to use riscv-\Nformal? This is the current version of the
Dialogue: 0,0:07:59.49,0:08:03.93,Default,,0000,0000,0000,,riscv-formal interface. Right now, there\Nis no support for floating-point
Dialogue: 0,0:08:03.93,0:08:09.15,Default,,0000,0000,0000,,instructions and there is no support for\NCSRs, but this is on the to-do list, so
Dialogue: 0,0:08:09.15,0:08:14.32,Default,,0000,0000,0000,,this interface will grow larger and larger\Nwhen we add these additional features, but
Dialogue: 0,0:08:14.32,0:08:18.14,Default,,0000,0000,0000,,all these additional features will be\Noptional. And one of the reasons is that
Dialogue: 0,0:08:18.14,0:08:22.40,Default,,0000,0000,0000,,some might implement just small\Nmicrocontrollers that actually don't have
Dialogue: 0,0:08:22.40,0:08:29.51,Default,,0000,0000,0000,,floating-point cores or that don't have\Nsupport for the privileged specification,
Dialogue: 0,0:08:29.51,0:08:35.33,Default,,0000,0000,0000,,so they don't have CSRs. Through this\Ninterface, whenever the core retires an
Dialogue: 0,0:08:35.33,0:08:40.75,Default,,0000,0000,0000,,instruction, it documents which\Ninstruction it retired; so it tells us
Dialogue: 0,0:08:40.75,0:08:45.83,Default,,0000,0000,0000,,"This is the instruction where I retired;\Nthis was the program counter where I found
Dialogue: 0,0:08:45.83,0:08:49.94,Default,,0000,0000,0000,,the instruction; this is the program\Ncounter for the next instruction; these
Dialogue: 0,0:08:49.94,0:08:53.81,Default,,0000,0000,0000,,are the registers that I read and these\Nare the values that I've observed in the
Dialogue: 0,0:08:53.81,0:08:58.03,Default,,0000,0000,0000,,register file; this is the register that\NI've written and this is the value that I
Dialogue: 0,0:08:58.03,0:09:00.64,Default,,0000,0000,0000,,have written to the register file"\NAll that stuff.
Dialogue: 0,0:09:00.64,0:09:06.95,Default,,0000,0000,0000,,So, in short, what we document through the\Nriscv-formal interface, is the part of the
Dialogue: 0,0:09:06.95,0:09:12.27,Default,,0000,0000,0000,,processor state that is observed by an\Ninstruction and the change to the state of
Dialogue: 0,0:09:12.27,0:09:16.98,Default,,0000,0000,0000,,the processor that is performed by an\Ninstruction -- like changes to the
Dialogue: 0,0:09:16.98,0:09:24.31,Default,,0000,0000,0000,,register file or changes to the program\Ncounter. And of course, most processors
Dialogue: 0,0:09:24.31,0:09:28.98,Default,,0000,0000,0000,,actually are superscalar, even those\Nprocessors that say they're non-
Dialogue: 0,0:09:28.98,0:09:33.58,Default,,0000,0000,0000,,superscalar. In-order pipelines usually\Ncan do stuff like retire memory load
Dialogue: 0,0:09:33.58,0:09:38.08,Default,,0000,0000,0000,,instructions out of order, in parallel to\Nanother instruction that does not write
Dialogue: 0,0:09:38.08,0:09:43.67,Default,,0000,0000,0000,,the register, things like that. So, even\Nwith processors we usually don't think of
Dialogue: 0,0:09:43.67,0:09:48.68,Default,,0000,0000,0000,,as superscalar processors, even with those\Nprocessors, we need the capability to
Dialogue: 0,0:09:48.68,0:09:53.71,Default,,0000,0000,0000,,retire more than one instruction each\Ncycle and this can be done with this
Dialogue: 0,0:09:53.71,0:10:03.84,Default,,0000,0000,0000,,"NRET" parameter. And we see all the ports\N5 times wider if NRET is 5. Okay, so then
Dialogue: 0,0:10:03.84,0:10:07.85,Default,,0000,0000,0000,,we have a processor that implements this\Ninterface. What is the verification
Dialogue: 0,0:10:07.85,0:10:14.27,Default,,0000,0000,0000,,strategy that riscv-formal follows in\Norder to do this proof to formally verify
Dialogue: 0,0:10:14.27,0:10:20.72,Default,,0000,0000,0000,,that our processor's actually correct? So,\Nthere is not one big proof that we run.
Dialogue: 0,0:10:20.72,0:10:26.99,Default,,0000,0000,0000,,Instead, there is a large number of very\Nsmall proofs that we run. This is the most
Dialogue: 0,0:10:26.99,0:10:32.56,Default,,0000,0000,0000,,important trick when it comes to this and\Nthere are 2 categories of proofs: One
Dialogue: 0,0:10:32.56,0:10:37.62,Default,,0000,0000,0000,,category is what I call the "instruction\Nchecks". We have one of those proofs for
Dialogue: 0,0:10:37.62,0:10:42.88,Default,,0000,0000,0000,,each instruction in the ISA specification\Nand each of the channels in the riscv-
Dialogue: 0,0:10:42.88,0:10:48.47,Default,,0000,0000,0000,,formal interface. So, this is easily a\Ncouple of hundred proofs right there
Dialogue: 0,0:10:48.47,0:10:52.12,Default,,0000,0000,0000,,because you easily have 100 instructions\Nand if you have 2 channels, you already
Dialogue: 0,0:10:52.12,0:10:58.47,Default,,0000,0000,0000,,have 200 proofs that you have to run. And\Nwhat this instruction checks do, they
Dialogue: 0,0:10:58.47,0:11:04.08,Default,,0000,0000,0000,,reset the processor or they started a\Nsymbolic state, if you would like to run a
Dialogue: 0,0:11:04.08,0:11:09.20,Default,,0000,0000,0000,,unbounded proof, let the process run for a\Ncertain number of cycles and then it
Dialogue: 0,0:11:09.20,0:11:14.54,Default,,0000,0000,0000,,assumes that in the last cycle, the\Nprocessor will retire a certain
Dialogue: 0,0:11:14.54,0:11:16.77,Default,,0000,0000,0000,,instruction. So, if this\Ncheck checks if the "add"
Dialogue: 0,0:11:16.77,0:11:21.41,Default,,0000,0000,0000,,instruction works correctly, it assumes\Nthat the last instruction retired in the
Dialogue: 0,0:11:21.41,0:11:27.81,Default,,0000,0000,0000,,last cycle of this bounder checked will be\Nan "add" instruction and then it looks at
Dialogue: 0,0:11:27.81,0:11:33.55,Default,,0000,0000,0000,,all the interfaces on the riscv-formal\Ninterface, to make sure that this is
Dialogue: 0,0:11:33.55,0:11:37.27,Default,,0000,0000,0000,,compliant with an "add" instruction. It\Nchecks if the instruction has been decoded
Dialogue: 0,0:11:37.27,0:11:42.22,Default,,0000,0000,0000,,correctly; it checks if the register value\Nwe write to the register file is actually
Dialogue: 0,0:11:42.22,0:11:47.48,Default,,0000,0000,0000,,the sum of the values we read from the\Nregister file. All that kind of stuff.
Dialogue: 0,0:11:47.48,0:11:51.03,Default,,0000,0000,0000,,But, of course, if you just have these\Ninstruction checks, there is still a
Dialogue: 0,0:11:51.03,0:11:56.41,Default,,0000,0000,0000,,certain verification gap, because the core\Nmight lie to us: The core might say "Oh, I
Dialogue: 0,0:11:56.41,0:12:00.02,Default,,0000,0000,0000,,write this value to the register file",\Nbut then not write the value to the
Dialogue: 0,0:12:00.02,0:12:06.16,Default,,0000,0000,0000,,register file, so we have to have a\Nseparate set of proofs that do not look at
Dialogue: 0,0:12:06.16,0:12:11.25,Default,,0000,0000,0000,,the entire riscv-formal interface in one\Ncycle, but look at only a small fraction
Dialogue: 0,0:12:11.25,0:12:15.85,Default,,0000,0000,0000,,of the riscv- formal interface, but over a\Nspan of cycles. So, for example, there is
Dialogue: 0,0:12:15.85,0:12:20.20,Default,,0000,0000,0000,,one check that says "If I write the\Nregister and then later I read the
Dialogue: 0,0:12:20.20,0:12:24.93,Default,,0000,0000,0000,,register, I better read back the value\Nthat I've written to the register file"
Dialogue: 0,0:12:24.93,0:12:33.90,Default,,0000,0000,0000,,and this I call "consistency checks". So,\Nthat's I think what I said already... So
Dialogue: 0,0:12:33.90,0:12:40.17,Default,,0000,0000,0000,,for each instruction with riscv-formal, we\Nhave a instruction model that looks like
Dialogue: 0,0:12:40.17,0:12:45.92,Default,,0000,0000,0000,,that. So, these are 2 slides: The first\Nslides is just the interface there we have
Dialogue: 0,0:12:45.92,0:12:51.94,Default,,0000,0000,0000,,a couple of signals from this riscv-formal\Ninterface that we read like the
Dialogue: 0,0:12:51.94,0:12:58.19,Default,,0000,0000,0000,,instruction that we are executing, the\Nprogram counter where we found this
Dialogue: 0,0:12:58.19,0:13:04.08,Default,,0000,0000,0000,,instruction, the register values we read,\Nand then we have a couple of signals that
Dialogue: 0,0:13:04.08,0:13:09.90,Default,,0000,0000,0000,,are generated by our specification that\Nare output of this specification module.
Dialogue: 0,0:13:09.90,0:13:17.60,Default,,0000,0000,0000,,Like, which registers should we read?\NWhich registers should we write? What
Dialogue: 0,0:13:17.60,0:13:22.13,Default,,0000,0000,0000,,values should we write to that register?\NStuff like that. So, that's the interface.
Dialogue: 0,0:13:22.13,0:13:26.74,Default,,0000,0000,0000,,It's the same all the instructions and\Nthen we have a body that looks more
Dialogue: 0,0:13:26.74,0:13:31.19,Default,,0000,0000,0000,,like that. For all the instructions that\Njust decodes the instruction, checks if
Dialogue: 0,0:13:31.19,0:13:34.78,Default,,0000,0000,0000,,this is actually the instruction the check\Nis for. So, in this case it's an "add
Dialogue: 0,0:13:34.78,0:13:42.03,Default,,0000,0000,0000,,immediate" instruction. And then you have\Nthings like the line near the bottom above
Dialogue: 0,0:13:42.03,0:13:46.29,Default,,0000,0000,0000,,"default assignments": "assign\Nspec_pc_wdata", for example, says "Okay,
Dialogue: 0,0:13:46.29,0:13:54.68,Default,,0000,0000,0000,,the next PC must be 4 bytes later than the\NPC for this instruction. We must increment
Dialogue: 0,0:13:54.68,0:13:58.86,Default,,0000,0000,0000,,the program counter by a value of 4 when\Nwe execute this instruction." Things like
Dialogue: 0,0:13:58.86,0:14:09.51,Default,,0000,0000,0000,,that. So, you might see, there is no\Nassert here, there are no assertions,
Dialogue: 0,0:14:09.51,0:14:13.64,Default,,0000,0000,0000,,because this is just the model of what\Nkind of behavior we would expect. And then
Dialogue: 0,0:14:13.64,0:14:17.77,Default,,0000,0000,0000,,there is a wrapper that instantiates this\Nand instantiates the call and builds the
Dialogue: 0,0:14:17.77,0:14:23.08,Default,,0000,0000,0000,,proof and there are the assertions. The\Nmain reason why we don't have assertions
Dialogue: 0,0:14:23.08,0:14:27.82,Default,,0000,0000,0000,,here, but instead we output the desired\Nbehavior here, is because I can also
Dialogue: 0,0:14:27.82,0:14:32.75,Default,,0000,0000,0000,,generate monitor cores that can run\Nalongside your core and check in
Dialogue: 0,0:14:32.75,0:14:38.16,Default,,0000,0000,0000,,simulation or an emulation, an FPGA, if\Nyour core is doing the right thing. That
Dialogue: 0,0:14:38.16,0:14:43.94,Default,,0000,0000,0000,,can be very, very helpful if you have a\Nsituation where you run your core for
Dialogue: 0,0:14:43.94,0:14:49.94,Default,,0000,0000,0000,,maybe days and then you have some\Nobservable behavior that's not right, but
Dialogue: 0,0:14:49.94,0:14:53.71,Default,,0000,0000,0000,,maybe there are thousands, even million,\Ncycles between the point where you can
Dialogue: 0,0:14:53.71,0:14:58.14,Default,,0000,0000,0000,,observe that something is wrong and the\Npoint where the process actually started
Dialogue: 0,0:14:58.14,0:15:03.38,Default,,0000,0000,0000,,diverging from what the specification said\Nand if you can use a monitor core like
Dialogue: 0,0:15:03.38,0:15:10.23,Default,,0000,0000,0000,,that, then it's much easier to find bugs\Nlike this. Okay, so some examples of those
Dialogue: 0,0:15:10.23,0:15:15.41,Default,,0000,0000,0000,,consistency checks.; the list is actually\Nnot complete and it varies a little bit
Dialogue: 0,0:15:15.41,0:15:20.08,Default,,0000,0000,0000,,from processor to processor what kind of\Nconsistency checks we can actually run
Dialogue: 0,0:15:20.08,0:15:26.48,Default,,0000,0000,0000,,with the processor we are looking at.\NThere is a check if the program counter
Dialogue: 0,0:15:26.48,0:15:30.10,Default,,0000,0000,0000,,for one instruction - so I have an\Ninstruction it says "This is the program
Dialogue: 0,0:15:30.10,0:15:32.34,Default,,0000,0000,0000,,counter for the instruction and this is\Nthe program counter for the next
Dialogue: 0,0:15:32.34,0:15:37.33,Default,,0000,0000,0000,,instruction" -- and then we can look at\Nthe next instruction and we can see is...
Dialogue: 0,0:15:37.33,0:15:40.92,Default,,0000,0000,0000,,the program counter for that instruction\Nactually approved the next program counter
Dialogue: 0,0:15:40.92,0:15:46.37,Default,,0000,0000,0000,,value for the previous instruction and\Nthey must link together like that, but the
Dialogue: 0,0:15:46.37,0:15:52.13,Default,,0000,0000,0000,,core might retire instructions out of\Norder. So it might be, that we see the
Dialogue: 0,0:15:52.13,0:15:55.65,Default,,0000,0000,0000,,first instruction for us and then the\Nsecond instruction later, but it's also
Dialogue: 0,0:15:55.65,0:15:58.67,Default,,0000,0000,0000,,possible that we will see the second\Ninstruction first and then the first
Dialogue: 0,0:15:58.67,0:16:03.58,Default,,0000,0000,0000,,instruction later and because of that,\Nthere're 2 different checks: One for a
Dialogue: 0,0:16:03.58,0:16:08.94,Default,,0000,0000,0000,,pair in the non-reversed order and for a\Npair of instruction in the reversed order.
Dialogue: 0,0:16:08.94,0:16:13.48,Default,,0000,0000,0000,,There is one check that checks, if\Nregister value reads and writes are
Dialogue: 0,0:16:13.48,0:16:21.05,Default,,0000,0000,0000,,consistent. There is one check that sees,\Nif the processor is alive, so when I give
Dialogue: 0,0:16:21.05,0:16:29.14,Default,,0000,0000,0000,,the processor certain fairness constrains,\Nthat the memory will always return, memory
Dialogue: 0,0:16:29.14,0:16:32.60,Default,,0000,0000,0000,,reads at number of cycles, things like\Nthat, then I can use this to prove that
Dialogue: 0,0:16:32.60,0:16:37.46,Default,,0000,0000,0000,,the process will not just suddenly freeze.\NThis is very important and this will also
Dialogue: 0,0:16:37.46,0:16:41.46,Default,,0000,0000,0000,,prove that the processor is not skipping\Ninstruction indices, which is very
Dialogue: 0,0:16:41.46,0:16:45.62,Default,,0000,0000,0000,,important, because some of the other\Nchecks actually depend on the processor
Dialogue: 0,0:16:45.62,0:16:51.10,Default,,0000,0000,0000,,behaving in this way. And so forth. So,\Nthere are couple of these consistency
Dialogue: 0,0:16:51.10,0:16:55.38,Default,,0000,0000,0000,,checks and it's a nice exercise to sit\Ndown in a group of people and go through
Dialogue: 0,0:16:55.38,0:17:00.68,Default,,0000,0000,0000,,the list of consistency checks and see\Nwhich which set of them actually is
Dialogue: 0,0:17:00.68,0:17:05.80,Default,,0000,0000,0000,,meaningful or which set of them actually\Nleaves an interesting verification gap and
Dialogue: 0,0:17:05.80,0:17:11.79,Default,,0000,0000,0000,,we still need to add checks for this or\Nthat processor then. Okay, so what kind of
Dialogue: 0,0:17:11.79,0:17:19.95,Default,,0000,0000,0000,,bugs can it find? That's a super-hard\Nquestion, because it's really hard to give
Dialogue: 0,0:17:19.95,0:17:26.21,Default,,0000,0000,0000,,a complete list. It can definitely find\Nincorrect single-threaded instruction
Dialogue: 0,0:17:26.21,0:17:28.88,Default,,0000,0000,0000,,semantics. So, if you\Njust implement a instruction
Dialogue: 0,0:17:28.88,0:17:34.35,Default,,0000,0000,0000,,incorrectly in your core, then this will\Nfind it; no question about it. It can find
Dialogue: 0,0:17:34.35,0:17:38.74,Default,,0000,0000,0000,,a lot of bugs and things like bypassing\Nand forwarding and pipeline interlocks,
Dialogue: 0,0:17:38.74,0:17:46.60,Default,,0000,0000,0000,,things like that. Things where you reorder\Nstuff in a way you shouldn't reorder them,
Dialogue: 0,0:17:46.60,0:17:51.95,Default,,0000,0000,0000,,freezes if you have this lifeness check,\Nsome bugs related to memory interfaces and
Dialogue: 0,0:17:51.95,0:17:58.61,Default,,0000,0000,0000,,load/store consistency and things like\Nthat, but that depends on things like the
Dialogue: 0,0:17:58.61,0:18:04.11,Default,,0000,0000,0000,,size of your cache lines, if this is a\Nfeasible proof or not. Bugs that we can't
Dialogue: 0,0:18:04.11,0:18:09.28,Default,,0000,0000,0000,,find yet with riscv-formal are things that\Nare not yet covered with the riscv-formal
Dialogue: 0,0:18:09.28,0:18:13.18,Default,,0000,0000,0000,,interface, like the floating-point stuff\Nor CSRs, but this is all on the to-do
Dialogue: 0,0:18:13.18,0:18:18.28,Default,,0000,0000,0000,,list, so they are actively working on that\Nand a year from now, this stuff will be
Dialogue: 0,0:18:18.28,0:18:24.65,Default,,0000,0000,0000,,included. And anything related to\Nconcurrency between multiple heats. So
Dialogue: 0,0:18:24.65,0:18:28.21,Default,,0000,0000,0000,,far, my excuse for that was, that the\NRISC-V memory model is not completely
Dialogue: 0,0:18:28.21,0:18:33.79,Default,,0000,0000,0000,,specified yet, so I would not actually\Nknow what to check exactly, but right now
Dialogue: 0,0:18:33.79,0:18:38.56,Default,,0000,0000,0000,,the RISC-V memory model is in the process\Nof being finalized, so I won't have this
Dialogue: 0,0:18:38.56,0:18:45.74,Default,,0000,0000,0000,,excuse for much, much longer. So, the\Nprocessors currently supported PicoRV32,
Dialogue: 0,0:18:45.74,0:18:50.74,Default,,0000,0000,0000,,which is my own processor, then RISC-V\NRocket, which is probably the most famous
Dialogue: 0,0:18:50.74,0:18:56.52,Default,,0000,0000,0000,,RISC-V implementation, and VexRiscv. And\Nthere are also a couple of others, but
Dialogue: 0,0:18:56.52,0:19:04.04,Default,,0000,0000,0000,,they are not part of the open source\Nrelease of riscv-formal. So, if you would
Dialogue: 0,0:19:04.04,0:19:11.16,Default,,0000,0000,0000,,like to add support to riscv-formal for\Nyour RISC-V processor, then just check out
Dialogue: 0,0:19:11.16,0:19:15.95,Default,,0000,0000,0000,,the riscv-formal repository, look at the\N"cores" directory, see which of the
Dialogue: 0,0:19:15.95,0:19:20.21,Default,,0000,0000,0000,,supported cores's most closely to the code\Nthat you actually have and then just copy
Dialogue: 0,0:19:20.21,0:19:27.80,Default,,0000,0000,0000,,that directory and make a couple of small\Nmodifications. So, I have a few minutes
Dialogue: 0,0:19:27.80,0:19:33.98,Default,,0000,0000,0000,,left to talk about things like cut-points\Nand blackboxes and other abstractions. So,
Dialogue: 0,0:19:33.98,0:19:37.92,Default,,0000,0000,0000,,the title of this slide could just be\N"abstractions", because cut-points and
Dialogue: 0,0:19:37.92,0:19:41.76,Default,,0000,0000,0000,,blackboxes are just abstractions.\NThe idea behind an abstraction and formal
Dialogue: 0,0:19:41.76,0:19:48.22,Default,,0000,0000,0000,,methods is that I switch out part of my\Ndesign with a different part with a
Dialogue: 0,0:19:48.22,0:19:54.64,Default,,0000,0000,0000,,different circuit that is less\Nconstrained, it includes the behavior of
Dialogue: 0,0:19:54.64,0:19:59.04,Default,,0000,0000,0000,,the original circuit, but might do other\Nstuff as well. So, the textbook example
Dialogue: 0,0:19:59.04,0:20:03.34,Default,,0000,0000,0000,,would be, I have a design with a counter\Nand usually the counter would just
Dialogue: 0,0:20:03.34,0:20:08.61,Default,,0000,0000,0000,,increment in steps of 1, but now I create\Nan abstraction that can skip numbers and
Dialogue: 0,0:20:08.61,0:20:15.86,Default,,0000,0000,0000,,will just increment in strictly increasing\Nsteps. And this, of course, includes the
Dialogue: 0,0:20:15.86,0:20:20.04,Default,,0000,0000,0000,,behavior of the original design, so if I\Ncan prove a property with this abstraction
Dialogue: 0,0:20:20.04,0:20:24.89,Default,,0000,0000,0000,,in place instead of the just-increment-\Nby-1 counter, then we have proven even a
Dialogue: 0,0:20:24.89,0:20:29.62,Default,,0000,0000,0000,,stronger property and that includes the\Nsame property for the thing in the
Dialogue: 0,0:20:29.62,0:20:35.69,Default,,0000,0000,0000,,original design. And actually this idea of\Nabstractions works very well with riscv-
Dialogue: 0,0:20:35.69,0:20:40.95,Default,,0000,0000,0000,,formal. So, the main reason why we do\Nabstractions is because it leads to easier
Dialogue: 0,0:20:40.95,0:20:46.54,Default,,0000,0000,0000,,proofs. So, for example, consider an\Ninstruction checker that just checks if
Dialogue: 0,0:20:46.54,0:20:52.28,Default,,0000,0000,0000,,the core implements the "add" instruction\Ncorrectly. For this checker, we don't
Dialogue: 0,0:20:52.28,0:20:56.02,Default,,0000,0000,0000,,actually need a register file that's\Nworking. We could replace the register
Dialogue: 0,0:20:56.02,0:21:00.58,Default,,0000,0000,0000,,file by something that just ignores all\Nwrites to it and whenever we read
Dialogue: 0,0:21:00.58,0:21:04.29,Default,,0000,0000,0000,,something from the register file, it\Nreturns an arbitrary value. That would
Dialogue: 0,0:21:04.29,0:21:09.87,Default,,0000,0000,0000,,still include the behavior of a core with\Na functional register file, but, because
Dialogue: 0,0:21:09.87,0:21:13.61,Default,,0000,0000,0000,,the instruction checker does not care\Nabout consistency between register file
Dialogue: 0,0:21:13.61,0:21:17.93,Default,,0000,0000,0000,,writes and register file reads, we can\Nstill prove that the instruction is
Dialogue: 0,0:21:17.93,0:21:22.89,Default,,0000,0000,0000,,implemented correctly, and therefore we\Nget an easier proof. Of course, we can't
Dialogue: 0,0:21:22.89,0:21:27.10,Default,,0000,0000,0000,,use this abstraction for all those proofs,\Nbecause the other proofs that actually
Dialogue: 0,0:21:27.10,0:21:33.33,Default,,0000,0000,0000,,check if my register file works as I would\Nexpect it to work, but if we go through
Dialogue: 0,0:21:33.33,0:21:37.43,Default,,0000,0000,0000,,the list of proofs and we run all these\Nproofs independently, then you will see
Dialogue: 0,0:21:37.43,0:21:41.96,Default,,0000,0000,0000,,that for each of them, it's possible to\Nabstract away a large portion of your
Dialogue: 0,0:21:41.96,0:21:47.38,Default,,0000,0000,0000,,processor and therefore yield\Nand an easier proof.
Dialogue: 0,0:21:47.38,0:21:51.17,Default,,0000,0000,0000,,Depending on what kind of solvers you use,\Nsome solvers're actually very capable of
Dialogue: 0,0:21:51.17,0:21:54.78,Default,,0000,0000,0000,,finding these kind of abstractions\Nthemselves. So in that cases, it doesn't
Dialogue: 0,0:21:54.78,0:21:59.47,Default,,0000,0000,0000,,really help by adding these abstractions\Nmanually, but just realizing that the
Dialogue: 0,0:21:59.47,0:22:04.49,Default,,0000,0000,0000,,potential for these abstractions is there,\Nis something that's very useful when
Dialogue: 0,0:22:04.49,0:22:09.02,Default,,0000,0000,0000,,guiding your decisions how to split up a\Nlarge verification problem into smaller
Dialogue: 0,0:22:09.02,0:22:12.61,Default,,0000,0000,0000,,verification problems, because you would\Nlike to split up the problem in a way so
Dialogue: 0,0:22:12.61,0:22:17.10,Default,,0000,0000,0000,,that the solver is always capable of\Nfinding useful abstractions that actually
Dialogue: 0,0:22:17.10,0:22:27.70,Default,,0000,0000,0000,,lead to easier circuits to prove. With a\Nbounded check, we also have the questions
Dialogue: 0,0:22:27.70,0:22:32.85,Default,,0000,0000,0000,,of what bounds do we use. Of course,\Nlarger bounds are better, but larger
Dialogue: 0,0:22:32.85,0:22:41.86,Default,,0000,0000,0000,,bounds also yield something that is harder\Nto compute, and if you have a small bound,
Dialogue: 0,0:22:41.86,0:22:45.34,Default,,0000,0000,0000,,then you have a proof that runs very, very\Nquickly, but maybe you're not very
Dialogue: 0,0:22:45.34,0:22:49.97,Default,,0000,0000,0000,,confident that it actually has proven\Nsomething that's relevant for you. So, I
Dialogue: 0,0:22:49.97,0:22:57.35,Default,,0000,0000,0000,,propose 2 solutions for this: The first\Nsolution is, you can use the same solvers
Dialogue: 0,0:22:57.35,0:23:02.49,Default,,0000,0000,0000,,to find traces that cover certain events\Nand you could write a list and say "I
Dialogue: 0,0:23:02.49,0:23:07.41,Default,,0000,0000,0000,,would like to see 1 memory read and 1\Nmemory write and at least one ALU
Dialogue: 0,0:23:07.41,0:23:10.69,Default,,0000,0000,0000,,instruction executed" and things like\Nthat. And then, you can ask the solver
Dialogue: 0,0:23:10.69,0:23:18.83,Default,,0000,0000,0000,,"What is the shortest trace that would\Nactually satisfy all this stuff?" And when
Dialogue: 0,0:23:18.83,0:23:24.57,Default,,0000,0000,0000,,that's a trace of, say 25 cycles, then you\Nknow "Okay, when I look at a prove that's
Dialogue: 0,0:23:24.57,0:23:29.79,Default,,0000,0000,0000,,25 cyclic deep, I know at least these are\Nthe cases that are going to be covered."
Dialogue: 0,0:23:29.79,0:23:34.73,Default,,0000,0000,0000,,But more important, I think, is: Usually\Nwhen you have a processor, you already
Dialogue: 0,0:23:34.73,0:23:41.27,Default,,0000,0000,0000,,found bugs and it's a good idea to not\Njust fix the bugs and forget about them,
Dialogue: 0,0:23:41.27,0:23:46.61,Default,,0000,0000,0000,,but preserve some way of re-introducing\Nthe bugs, just to see if your testing
Dialogue: 0,0:23:46.61,0:23:51.51,Default,,0000,0000,0000,,framework works. So,\Nif you have already a couple of bugs
Dialogue: 0,0:23:51.51,0:23:55.12,Default,,0000,0000,0000,,and you know "It took me a week to find\Nthat and took me a month to find that",
Dialogue: 0,0:23:55.12,0:24:00.55,Default,,0000,0000,0000,,the best thing is to just add the bugs to\Nyour design again and see "What are the
Dialogue: 0,0:24:00.55,0:24:04.61,Default,,0000,0000,0000,,bounds that are necessary for riscv-formal\Nto actually discover those bugs" and then
Dialogue: 0,0:24:04.61,0:24:09.01,Default,,0000,0000,0000,,you will have some degree of confidence\Nthat other similar bugs would also have
Dialogue: 0,0:24:09.01,0:24:15.78,Default,,0000,0000,0000,,been found with the same bounds. So,\N"Results": I have found bugs in pretty much
Dialogue: 0,0:24:15.78,0:24:23.03,Default,,0000,0000,0000,,every implementation I looked at; I found\Nbugs in all 3 processors; we found bugs in
Dialogue: 0,0:24:23.03,0:24:28.14,Default,,0000,0000,0000,,Spike, which is the official implementation\Nof RISC-V in C and I found
Dialogue: 0,0:24:28.14,0:24:33.76,Default,,0000,0000,0000,,a way to formally verify my specification\Nagainst Spike and in some cases where I found
Dialogue: 0,0:24:33.76,0:24:37.25,Default,,0000,0000,0000,,the difference between my specification\Nand Spike, it turned out, it
Dialogue: 0,0:24:37.25,0:24:41.83,Default,,0000,0000,0000,,was actually a bug in the English language\Nspecification. So, because of that, I also
Dialogue: 0,0:24:41.83,0:24:47.95,Default,,0000,0000,0000,,found bugs in the English language\Nspecification with riscv-formal. "Future
Dialogue: 0,0:24:47.95,0:24:53.52,Default,,0000,0000,0000,,work": Multipliers already supported,\Nfloating-point is still on the to-do list,
Dialogue: 0,0:24:53.52,0:25:01.60,Default,,0000,0000,0000,,64-bit is half done. We would like to add\Nsupport for CSRs. We would like to add
Dialogue: 0,0:25:01.60,0:25:06.12,Default,,0000,0000,0000,,support for more cores, but this is\Nsomething that I would like to do slowly,
Dialogue: 0,0:25:06.12,0:25:10.65,Default,,0000,0000,0000,,because adding more cores also means we\Nhave less flexibility with changing
Dialogue: 0,0:25:10.65,0:25:17.97,Default,,0000,0000,0000,,things. And better integration with non-\Nfree tools, because right now all of that
Dialogue: 0,0:25:17.97,0:25:22.60,Default,,0000,0000,0000,,runs with open source tools that I also\Nhappen to write -- so, I wrote those
Dialogue: 0,0:25:22.60,0:25:27.58,Default,,0000,0000,0000,,tools, but some people actually don't want\Nto use my open source tools; they would
Dialogue: 0,0:25:27.58,0:25:31.26,Default,,0000,0000,0000,,like to use the commercial tools -- and\Nit's the to-do list that I have better
Dialogue: 0,0:25:31.26,0:25:35.75,Default,,0000,0000,0000,,integration with those tools. Maybe,\Nbecause I don't get licenses to those
Dialogue: 0,0:25:35.75,0:25:41.05,Default,,0000,0000,0000,,tools, so we will see how this works.\NThat's it. Do we have still time for
Dialogue: 0,0:25:41.05,0:26:02.71,Default,,0000,0000,0000,,questions?\N{\i1}applause{\i0}
Dialogue: 0,0:26:02.71,0:26:05.38,Default,,0000,0000,0000,,Clifford: So, I'd say we start with\Nquestions at 1.
Dialogue: 0,0:26:05.38,0:26:11.24,Default,,0000,0000,0000,,Herald: I'm sorry; here we go. We have 2\Nquestions; we have time for 2 questions
Dialogue: 0,0:26:11.24,0:26:15.72,Default,,0000,0000,0000,,and we're going to start with microphone\Nnumber 1, please.
Dialogue: 0,0:26:15.72,0:26:22.78,Default,,0000,0000,0000,,M1: Hello, thanks for your talk and for\Nyour work. First question: You told about
Dialogue: 0,0:26:22.78,0:26:26.69,Default,,0000,0000,0000,,riscv-formal interface.\NClifford: Yes.
Dialogue: 0,0:26:26.69,0:26:34.20,Default,,0000,0000,0000,,M1: So, does vendor ship the final\Nprocessor with this interface available?
Dialogue: 0,0:26:34.20,0:26:39.53,Default,,0000,0000,0000,,Clifford: Oh, that's a great question,\Nthank you. This interface has only output
Dialogue: 0,0:26:39.53,0:26:45.29,Default,,0000,0000,0000,,ports and actually when you implement this\Ninterface, you should not add something to
Dialogue: 0,0:26:45.29,0:26:49.23,Default,,0000,0000,0000,,your design that's not needed to generate\Nthose output ports. So, what you can do
Dialogue: 0,0:26:49.23,0:26:53.51,Default,,0000,0000,0000,,is, you can take the version of your core\Nwith that interface, the version of the
Dialogue: 0,0:26:53.51,0:26:58.48,Default,,0000,0000,0000,,core without that interface. Then, in your\Nsynthesis script, just remove those output
Dialogue: 0,0:26:58.48,0:27:03.72,Default,,0000,0000,0000,,ports and then run a formal equivalence\Ncheck between that version and the version
Dialogue: 0,0:27:03.72,0:27:10.82,Default,,0000,0000,0000,,that you actually deploy on your ASIC.\NM1: Thanks; and one short question: When
Dialogue: 0,0:27:10.82,0:27:17.38,Default,,0000,0000,0000,,people say formal verification, usually\Nothers think "Oh, if it is verified, it is
Dialogue: 0,0:27:17.38,0:27:26.22,Default,,0000,0000,0000,,excellent, absolutely excellent. Do you\Nplan to say that it will find all the
Dialogue: 0,0:27:26.22,0:27:30.65,Default,,0000,0000,0000,,erato for the processor?\NClifford: Well, it depends on what kind of
Dialogue: 0,0:27:30.65,0:27:35.99,Default,,0000,0000,0000,,proof you run. The most work I do is with\Nbounded proofs and there you only get a
Dialogue: 0,0:27:35.99,0:27:40.83,Default,,0000,0000,0000,,certain degree of confidence, because you\Nonly see bugs that can occur within a
Dialogue: 0,0:27:40.83,0:27:46.16,Default,,0000,0000,0000,,certain number of cycles from reset, but\Nif you want, you can also run a complete
Dialogue: 0,0:27:46.16,0:27:52.54,Default,,0000,0000,0000,,proof, where you start with a symbolic\Nstate instead of a reset state and then
Dialogue: 0,0:27:52.54,0:27:57.51,Default,,0000,0000,0000,,you can can make sure that you actually\Ncheck the entire reachable state space,
Dialogue: 0,0:27:57.51,0:28:01.51,Default,,0000,0000,0000,,but that's a very, very hard thing to do\NSo, that's not a weekend project. Just
Dialogue: 0,0:28:01.51,0:28:05.73,Default,,0000,0000,0000,,adding the riscv-formal interface and\Nrunning some bounded proofs is probably a
Dialogue: 0,0:28:05.73,0:28:10.56,Default,,0000,0000,0000,,weekend project if you already have\Nyour RISC-V processor.
Dialogue: 0,0:28:10.56,0:28:13.40,Default,,0000,0000,0000,,M1: Thank you.\NHerald: Thank you. We actually do not have
Dialogue: 0,0:28:13.40,0:28:17.92,Default,,0000,0000,0000,,time for any more questions, but there\Nwill be time after the talk to ask you
Dialogue: 0,0:28:17.92,0:28:22.13,Default,,0000,0000,0000,,questions... maybe?\NClifford: Yeah. So, maybe you can find me
Dialogue: 0,0:28:22.13,0:28:27.39,Default,,0000,0000,0000,,at the open FPGA assembly, which is part\Nof the hardware hacking area.
Dialogue: 0,0:28:27.39,0:28:32.74,Default,,0000,0000,0000,,Herald: Super. Very great job to put that\Nmuch information into 30 minutes. Please
Dialogue: 0,0:28:32.74,0:28:35.83,Default,,0000,0000,0000,,help me thank Cliff\Nfor his wonderful talk.
Dialogue: 0,0:28:35.83,0:28:44.23,Default,,0000,0000,0000,,{\i1}applause{\i0}
Dialogue: 0,0:28:44.23,0:28:49.45,Default,,0000,0000,0000,,{\i1}34c3 outro{\i0}
Dialogue: 0,0:28:49.45,0:29:06.00,Default,,0000,0000,0000,,subtitles created by c3subtitles.de\Nin the year 2018. Join, and help us!