34C3 - End-to-end formal ISA verification of RISC-V processors with riscv-formal

34c3 intro

Herald: The next talk is called "End-to-
end formal ISA verification of RISC-V

processors with riscv-formal". I have no
idea what this means, but I'm very excited

to understand what it means and Clifford
promised he's going to make sure everyone

will. Clifford has been very known in the
open-source and free-software... free-

source... oh my gosh... free-and-open-
source community and especially he's known

for the project IceStorm. Please help me
welcome Clifford!

applause

inaudible
Clifford: RISC-V is an open instruction

set architecture. It's an open ISA, so
it's not a processor, but it's a processor

specification -- an ISA specification --
that is free to use for everyone and if

you happen to have already implemented
your own processor at one point in time,

you might know that it's actually much
easier to implement a processor than to

implement all the tools that you need to
compile programs for your processor. And

if you use something like RISC-V, then you
can reuse the tools that are already out

there, so that's a great benefit. However,
for this endeavor we need processors that

actually really compatible to each other:
Processors that implement the RISC-V ISA

correctly. So, with many other ISAs, we
start with one processor and we say "Oh,

that's the processor" and later on, we
figure out there was a bug, and what

people sometimes do is, they just change
the specification, so that the

specification all fits the hardware they
actually have. We can't do something like

that with RISC-V, but there are many
implementations out there, all being

developed in parallel to fit the same
specification, so we want to have some

kind of means to make sure that all these
processors actually agree about what the

ISA specification is. So, what's formal
verification? Formal verification is a

super-broad term. In the context of this
talk, I'm talking about hardware model

checking. More specifically, I'm talking
about checking of so-called "safety

properties". So, we have some hardware
design and we have an initial state and we

would like to know if this hardware design
can reach a bad state from the initial

state. That's formally the problem that we
are trying to solve here. And there are

two means to do that, two different
categories of proofs that are bounded and

unbounded proofs, and with the bounded
proofs we only prove that it's impossible

to reach a bad state within a certain
number of cycles.

So, we give a maximum bound for the length
of a counterexample and with unbounded

proofs, we prove that a bad state can
actually never be reached. So, unbounded

proofs are, of course, better -- if you
can make an unbounded proof -- but in many

cases, this is very hard to achieve, but
bounded proofs is something that we can

do, so I'm talking about bounded proofs
here for the most part. So, what's end-to-

end formal verification? Because that's
also in my title. So, historically when

you formally verify something like a
processor, you break down the processor in

many small components and then you write
properties for each component and prove

for each component individually that they
adhere to the properties and then you make

a more abstract proof, that if you put in
system together from components that have

this property, then this system will have
the properties that you want. With end-to-

end verification, we treat the processors
one huge black box and just ask the

question "Does this one huge thing fit our
specification? Have the properties that we

want?" That has a couple of advantages:
It's much, much easier this way to take

one specification and port it from one
processor to another, because we don't

care about how the processor is built
internally, and it's much easier to take

the specification that we have and
actually match it to other specifications

of the ISA, because we have a
specification that says, what is the

overall behavior we expect from our
processor. But the big disadvantage, of

cause, is that it's computationally much
more expensive to do end-to-end formal

verifications and doing this end-to-end
verification of a processor against an ISA

specification is something that
historically was always fueled as the

textbook example of things that you can't
do with formal methods, but fortunately

the solvers... they became much better in
the last couple of years and now if we use

the right tricks, we can do stuff like
that with the solvers we have nowadays.

So, that's riscv-formal. riscv-formal is a
framework that allows us to do end-to-end

formal verification of RISC-V processors
against a formal version of the ISA

specification. So, riscv-formal is not a
formally verified processor. Instead, if

you happen to have a RISC-V processor, you
can use riscv-formal to prove that your

processor confirms to the ISA
specification. For the most part, this is

using bounded methods. Theoretically, you
could do unbounded proofs with riscv-

formal, but it's not the main use case.
So, it's good for what we call "bug

hunting", because maybe there is a
counterexample that would show, that the

processor could diverge from the desired
behavior with 1000 or 5000 cycles, but

usually, when you have something like a
processor and you can't reach a bad state

within the very short bounds, you have
high confidence that actually your

processor implements the ISA correctly.
So, if you have a processor and you would

like to integrate it with riscv-formal,
you need to do 2 things: You need to add a

special trace port to your processor; it's
called the RVFI trace port -- riscv-formal

interface trace port. And you have to
configure riscv-formal so that riscv-

formal understands the attributes of your
processor. So, for example, RISC-V is

available in a 32-bit and a 64-bit
version. You have to tell riscv-formal, if

you want to verify a 32-bit or 64-bit
processor. RISC-V is a modular ISA, so

there're a couple of extensions and you
have to tell riscv-formal, which

extensions your processor
actually implements.

And then there're a couple of other things
that are transparent for a userland

process, like if unaligned loads or stores
are supported by the hardware natively,

because RISC-V... the spec only says, that
when you do an unaligned load or store,

then a userspace program can expect this
load or store to succeed, but it might

take a long time, because there might be a
machine interrupt handler that is

emulating an unaligned load store by doing
alligned loads and stores, but if we do

this formal verification of the processor,
then the riscv-formal framework must be

aware: "What is the expected behavior for
your course?", "Should it trap when it

sees an unaligned load store or should it
just perform the load store unaligned?"

So, what does this interface look like
that you need to implement in your

processor if you would like to use riscv-
formal? This is the current version of the

riscv-formal interface. Right now, there
is no support for floating-point

instructions and there is no support for
CSRs, but this is on the to-do list, so

this interface will grow larger and larger
when we add these additional features, but

all these additional features will be
optional. And one of the reasons is that

some might implement just small
microcontrollers that actually don't have

floating-point cores or that don't have
support for the privileged specification,

so they don't have CSRs. Through this
interface, whenever the core retires an

instruction, it documents which
instruction it retired; so it tells us

"This is the instruction where I retired;
this was the program counter where I found

the instruction; this is the program
counter for the next instruction; these

are the registers that I read and these
are the values that I've observed in the

register file; this is the register that
I've written and this is the value that I

have written to the register file"
All that stuff.

So, in short, what we document through the
riscv-formal interface, is the part of the

processor state that is observed by an
instruction and the change to the state of

the processor that is performed by an
instruction -- like changes to the

register file or changes to the program
counter. And of course, most processors

actually are superscalar, even those
processors that say they're non-

superscalar. In-order pipelines usually
can do stuff like retire memory load

instructions out of order, in parallel to
another instruction that does not write

the register, things like that. So, even
with processors we usually don't think of

as superscalar processors, even with those
processors, we need the capability to

retire more than one instruction each
cycle and this can be done with this

"NRET" parameter. And we see all the ports
5 times wider if NRET is 5. Okay, so then

we have a processor that implements this
interface. What is the verification

strategy that riscv-formal follows in
order to do this proof to formally verify

that our processor's actually correct? So,
there is not one big proof that we run.

Instead, there is a large number of very
small proofs that we run. This is the most

important trick when it comes to this and
there are 2 categories of proofs: One

category is what I call the "instruction
checks". We have one of those proofs for

each instruction in the ISA specification
and each of the channels in the riscv-

formal interface. So, this is easily a
couple of hundred proofs right there

because you easily have 100 instructions
and if you have 2 channels, you already

have 200 proofs that you have to run. And
what this instruction checks do, they

reset the processor or they started a
symbolic state, if you would like to run a

unbounded proof, let the process run for a
certain number of cycles and then it

assumes that in the last cycle, the
processor will retire a certain

instruction. So, if this
check checks if the "add"

instruction works correctly, it assumes
that the last instruction retired in the

last cycle of this bounder checked will be
an "add" instruction and then it looks at

all the interfaces on the riscv-formal
interface, to make sure that this is

compliant with an "add" instruction. It
checks if the instruction has been decoded

correctly; it checks if the register value
we write to the register file is actually

the sum of the values we read from the
register file. All that kind of stuff.

But, of course, if you just have these
instruction checks, there is still a

certain verification gap, because the core
might lie to us: The core might say "Oh, I

write this value to the register file",
but then not write the value to the

register file, so we have to have a
separate set of proofs that do not look at

the entire riscv-formal interface in one
cycle, but look at only a small fraction

of the riscv- formal interface, but over a
span of cycles. So, for example, there is

one check that says "If I write the
register and then later I read the

register, I better read back the value
that I've written to the register file"

and this I call "consistency checks". So,
that's I think what I said already... So

for each instruction with riscv-formal, we
have a instruction model that looks like

that. So, these are 2 slides: The first
slides is just the interface there we have

a couple of signals from this riscv-formal
interface that we read like the

instruction that we are executing, the
program counter where we found this

instruction, the register values we read,
and then we have a couple of signals that

are generated by our specification that
are output of this specification module.

Like, which registers should we read?
Which registers should we write? What

values should we write to that register?
Stuff like that. So, that's the interface.

It's the same all the instructions and
then we have a body that looks more

like that. For all the instructions that
just decodes the instruction, checks if

this is actually the instruction the check
is for. So, in this case it's an "add

immediate" instruction. And then you have
things like the line near the bottom above

"default assignments": "assign
spec_pc_wdata", for example, says "Okay,

the next PC must be 4 bytes later than the
PC for this instruction. We must increment

the program counter by a value of 4 when
we execute this instruction." Things like

that. So, you might see, there is no
assert here, there are no assertions,

because this is just the model of what
kind of behavior we would expect. And then

there is a wrapper that instantiates this
and instantiates the call and builds the

proof and there are the assertions. The
main reason why we don't have assertions

here, but instead we output the desired
behavior here, is because I can also

generate monitor cores that can run
alongside your core and check in

simulation or an emulation, an FPGA, if
your core is doing the right thing. That

can be very, very helpful if you have a
situation where you run your core for

maybe days and then you have some
observable behavior that's not right, but

maybe there are thousands, even million,
cycles between the point where you can

observe that something is wrong and the
point where the process actually started

diverging from what the specification said
and if you can use a monitor core like

that, then it's much easier to find bugs
like this. Okay, so some examples of those

consistency checks.; the list is actually
not complete and it varies a little bit

from processor to processor what kind of
consistency checks we can actually run

with the processor we are looking at.
There is a check if the program counter

for one instruction - so I have an
instruction it says "This is the program

counter for the instruction and this is
the program counter for the next

instruction" -- and then we can look at
the next instruction and we can see is...

the program counter for that instruction
actually approved the next program counter

value for the previous instruction and
they must link together like that, but the

core might retire instructions out of
order. So it might be, that we see the

first instruction for us and then the
second instruction later, but it's also

possible that we will see the second
instruction first and then the first

instruction later and because of that,
there're 2 different checks: One for a

pair in the non-reversed order and for a
pair of instruction in the reversed order.

There is one check that checks, if
register value reads and writes are

consistent. There is one check that sees,
if the processor is alive, so when I give

the processor certain fairness constrains,
that the memory will always return, memory

reads at number of cycles, things like
that, then I can use this to prove that

the process will not just suddenly freeze.
This is very important and this will also

prove that the processor is not skipping
instruction indices, which is very

important, because some of the other
checks actually depend on the processor

behaving in this way. And so forth. So,
there are couple of these consistency

checks and it's a nice exercise to sit
down in a group of people and go through

the list of consistency checks and see
which which set of them actually is

meaningful or which set of them actually
leaves an interesting verification gap and

we still need to add checks for this or
that processor then. Okay, so what kind of

bugs can it find? That's a super-hard
question, because it's really hard to give

a complete list. It can definitely find
incorrect single-threaded instruction

semantics. So, if you
just implement a instruction

incorrectly in your core, then this will
find it; no question about it. It can find

a lot of bugs and things like bypassing
and forwarding and pipeline interlocks,

things like that. Things where you reorder
stuff in a way you shouldn't reorder them,

freezes if you have this lifeness check,
some bugs related to memory interfaces and

load/store consistency and things like
that, but that depends on things like the

size of your cache lines, if this is a
feasible proof or not. Bugs that we can't

find yet with riscv-formal are things that
are not yet covered with the riscv-formal

interface, like the floating-point stuff
or CSRs, but this is all on the to-do

list, so they are actively working on that
and a year from now, this stuff will be

included. And anything related to
concurrency between multiple heats. So

far, my excuse for that was, that the
RISC-V memory model is not completely

specified yet, so I would not actually
know what to check exactly, but right now

the RISC-V memory model is in the process
of being finalized, so I won't have this

excuse for much, much longer. So, the
processors currently supported PicoRV32,

which is my own processor, then RISC-V
Rocket, which is probably the most famous

RISC-V implementation, and VexRiscv. And
there are also a couple of others, but

they are not part of the open source
release of riscv-formal. So, if you would

like to add support to riscv-formal for
your RISC-V processor, then just check out

the riscv-formal repository, look at the
"cores" directory, see which of the

supported cores's most closely to the code
that you actually have and then just copy

that directory and make a couple of small
modifications. So, I have a few minutes

left to talk about things like cut-points
and blackboxes and other abstractions. So,

the title of this slide could just be
"abstractions", because cut-points and

blackboxes are just abstractions.
The idea behind an abstraction and formal

methods is that I switch out part of my
design with a different part with a

different circuit that is less
constrained, it includes the behavior of

the original circuit, but might do other
stuff as well. So, the textbook example

would be, I have a design with a counter
and usually the counter would just

increment in steps of 1, but now I create
an abstraction that can skip numbers and

will just increment in strictly increasing
steps. And this, of course, includes the

behavior of the original design, so if I
can prove a property with this abstraction

in place instead of the just-increment-
by-1 counter, then we have proven even a

stronger property and that includes the
same property for the thing in the

original design. And actually this idea of
abstractions works very well with riscv-

formal. So, the main reason why we do
abstractions is because it leads to easier

proofs. So, for example, consider an
instruction checker that just checks if

the core implements the "add" instruction
correctly. For this checker, we don't

actually need a register file that's
working. We could replace the register

file by something that just ignores all
writes to it and whenever we read

something from the register file, it
returns an arbitrary value. That would

still include the behavior of a core with
a functional register file, but, because

the instruction checker does not care
about consistency between register file

writes and register file reads, we can
still prove that the instruction is

implemented correctly, and therefore we
get an easier proof. Of course, we can't

use this abstraction for all those proofs,
because the other proofs that actually

check if my register file works as I would
expect it to work, but if we go through

the list of proofs and we run all these
proofs independently, then you will see

that for each of them, it's possible to
abstract away a large portion of your

processor and therefore yield
and an easier proof.

Depending on what kind of solvers you use,
some solvers're actually very capable of

finding these kind of abstractions
themselves. So in that cases, it doesn't

really help by adding these abstractions
manually, but just realizing that the

potential for these abstractions is there,
is something that's very useful when

guiding your decisions how to split up a
large verification problem into smaller

verification problems, because you would
like to split up the problem in a way so

that the solver is always capable of
finding useful abstractions that actually

lead to easier circuits to prove. With a
bounded check, we also have the questions

of what bounds do we use. Of course,
larger bounds are better, but larger

bounds also yield something that is harder
to compute, and if you have a small bound,

then you have a proof that runs very, very
quickly, but maybe you're not very

confident that it actually has proven
something that's relevant for you. So, I

propose 2 solutions for this: The first
solution is, you can use the same solvers

to find traces that cover certain events
and you could write a list and say "I

would like to see 1 memory read and 1
memory write and at least one ALU

instruction executed" and things like
that. And then, you can ask the solver

"What is the shortest trace that would
actually satisfy all this stuff?" And when

that's a trace of, say 25 cycles, then you
know "Okay, when I look at a prove that's

25 cyclic deep, I know at least these are
the cases that are going to be covered."

But more important, I think, is: Usually
when you have a processor, you already

found bugs and it's a good idea to not
just fix the bugs and forget about them,

but preserve some way of re-introducing
the bugs, just to see if your testing

framework works. So,
if you have already a couple of bugs

and you know "It took me a week to find
that and took me a month to find that",

the best thing is to just add the bugs to
your design again and see "What are the

bounds that are necessary for riscv-formal
to actually discover those bugs" and then

you will have some degree of confidence
that other similar bugs would also have

been found with the same bounds. So,
"Results": I have found bugs in pretty much

every implementation I looked at; I found
bugs in all 3 processors; we found bugs in

Spike, which is the official implementation
of RISC-V in C and I found

a way to formally verify my specification
against Spike and in some cases where I found

the difference between my specification
and Spike, it turned out, it

was actually a bug in the English language
specification. So, because of that, I also

found bugs in the English language
specification with riscv-formal. "Future

work": Multipliers already supported,
floating-point is still on the to-do list,

64-bit is half done. We would like to add
support for CSRs. We would like to add

support for more cores, but this is
something that I would like to do slowly,

because adding more cores also means we
have less flexibility with changing

things. And better integration with non-
free tools, because right now all of that

runs with open source tools that I also
happen to write -- so, I wrote those

tools, but some people actually don't want
to use my open source tools; they would

like to use the commercial tools -- and
it's the to-do list that I have better

integration with those tools. Maybe,
because I don't get licenses to those

tools, so we will see how this works.
That's it. Do we have still time for

questions?
applause

Clifford: So, I'd say we start with
questions at 1.

Herald: I'm sorry; here we go. We have 2
questions; we have time for 2 questions

and we're going to start with microphone
number 1, please.

M1: Hello, thanks for your talk and for
your work. First question: You told about

riscv-formal interface.
Clifford: Yes.

M1: So, does vendor ship the final
processor with this interface available?

Clifford: Oh, that's a great question,
thank you. This interface has only output

ports and actually when you implement this
interface, you should not add something to

your design that's not needed to generate
those output ports. So, what you can do

is, you can take the version of your core
with that interface, the version of the

core without that interface. Then, in your
synthesis script, just remove those output

ports and then run a formal equivalence
check between that version and the version

that you actually deploy on your ASIC.
M1: Thanks; and one short question: When

people say formal verification, usually
others think "Oh, if it is verified, it is

excellent, absolutely excellent. Do you
plan to say that it will find all the

erato for the processor?
Clifford: Well, it depends on what kind of

proof you run. The most work I do is with
bounded proofs and there you only get a

certain degree of confidence, because you
only see bugs that can occur within a

certain number of cycles from reset, but
if you want, you can also run a complete

proof, where you start with a symbolic
state instead of a reset state and then

you can can make sure that you actually
check the entire reachable state space,

but that's a very, very hard thing to do
So, that's not a weekend project. Just

adding the riscv-formal interface and
running some bounded proofs is probably a

weekend project if you already have
your RISC-V processor.

M1: Thank you.
Herald: Thank you. We actually do not have

time for any more questions, but there
will be time after the talk to ask you

questions... maybe?
Clifford: Yeah. So, maybe you can find me

at the open FPGA assembly, which is part
of the hardware hacking area.

Herald: Super. Very great job to put that
much information into 30 minutes. Please

help me thank Cliff
for his wonderful talk.

applause

34c3 outro

subtitles created by c3subtitles.de
in the year 2018. Join, and help us!