Return to Video

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

  • 0:00 - 0:16
    34c3 intro
  • 0:16 - 0:23
    Herald: The next talk is called "End-to-
    end formal ISA verification of RISC-V
  • 0:23 - 0:28
    processors with riscv-formal". I have no
    idea what this means, but I'm very excited
  • 0:28 - 0:34
    to understand what it means and Clifford
    promised he's going to make sure everyone
  • 0:34 - 0:39
    will. Clifford has been very known in the
    open-source and free-software... free-
  • 0:39 - 0:45
    source... oh my gosh... free-and-open-
    source community and especially he's known
  • 0:45 - 0:50
    for the project IceStorm. Please help me
    welcome Clifford!
  • 0:50 - 0:57
    applause
  • 0:57 - 1:12
    inaudible
    Clifford: RISC-V is an open instruction
  • 1:12 - 1:17
    set architecture. It's an open ISA, so
    it's not a processor, but it's a processor
  • 1:17 - 1:23
    specification -- an ISA specification --
    that is free to use for everyone and if
  • 1:23 - 1:27
    you happen to have already implemented
    your own processor at one point in time,
  • 1:27 - 1:31
    you might know that it's actually much
    easier to implement a processor than to
  • 1:31 - 1:36
    implement all the tools that you need to
    compile programs for your processor. And
  • 1:36 - 1:40
    if you use something like RISC-V, then you
    can reuse the tools that are already out
  • 1:40 - 1:45
    there, so that's a great benefit. However,
    for this endeavor we need processors that
  • 1:45 - 1:50
    actually really compatible to each other:
    Processors that implement the RISC-V ISA
  • 1:50 - 1:55
    correctly. So, with many other ISAs, we
    start with one processor and we say "Oh,
  • 1:55 - 2:00
    that's the processor" and later on, we
    figure out there was a bug, and what
  • 2:00 - 2:03
    people sometimes do is, they just change
    the specification, so that the
  • 2:03 - 2:07
    specification all fits the hardware they
    actually have. We can't do something like
  • 2:07 - 2:10
    that with RISC-V, but there are many
    implementations out there, all being
  • 2:10 - 2:14
    developed in parallel to fit the same
    specification, so we want to have some
  • 2:14 - 2:21
    kind of means to make sure that all these
    processors actually agree about what the
  • 2:21 - 2:27
    ISA specification is. So, what's formal
    verification? Formal verification is a
  • 2:27 - 2:33
    super-broad term. In the context of this
    talk, I'm talking about hardware model
  • 2:33 - 2:38
    checking. More specifically, I'm talking
    about checking of so-called "safety
  • 2:38 - 2:43
    properties". So, we have some hardware
    design and we have an initial state and we
  • 2:43 - 2:49
    would like to know if this hardware design
    can reach a bad state from the initial
  • 2:49 - 2:55
    state. That's formally the problem that we
    are trying to solve here. And there are
  • 2:55 - 3:00
    two means to do that, two different
    categories of proofs that are bounded and
  • 3:00 - 3:05
    unbounded proofs, and with the bounded
    proofs we only prove that it's impossible
  • 3:05 - 3:08
    to reach a bad state within a certain
    number of cycles.
  • 3:08 - 3:12
    So, we give a maximum bound for the length
    of a counterexample and with unbounded
  • 3:12 - 3:18
    proofs, we prove that a bad state can
    actually never be reached. So, unbounded
  • 3:18 - 3:23
    proofs are, of course, better -- if you
    can make an unbounded proof -- but in many
  • 3:23 - 3:29
    cases, this is very hard to achieve, but
    bounded proofs is something that we can
  • 3:29 - 3:36
    do, so I'm talking about bounded proofs
    here for the most part. So, what's end-to-
  • 3:36 - 3:41
    end formal verification? Because that's
    also in my title. So, historically when
  • 3:41 - 3:45
    you formally verify something like a
    processor, you break down the processor in
  • 3:45 - 3:50
    many small components and then you write
    properties for each component and prove
  • 3:50 - 3:55
    for each component individually that they
    adhere to the properties and then you make
  • 3:55 - 3:59
    a more abstract proof, that if you put in
    system together from components that have
  • 3:59 - 4:04
    this property, then this system will have
    the properties that you want. With end-to-
  • 4:04 - 4:10
    end verification, we treat the processors
    one huge black box and just ask the
  • 4:10 - 4:16
    question "Does this one huge thing fit our
    specification? Have the properties that we
  • 4:16 - 4:22
    want?" That has a couple of advantages:
    It's much, much easier this way to take
  • 4:22 - 4:26
    one specification and port it from one
    processor to another, because we don't
  • 4:26 - 4:32
    care about how the processor is built
    internally, and it's much easier to take
  • 4:32 - 4:36
    the specification that we have and
    actually match it to other specifications
  • 4:36 - 4:40
    of the ISA, because we have a
    specification that says, what is the
  • 4:40 - 4:45
    overall behavior we expect from our
    processor. But the big disadvantage, of
  • 4:45 - 4:50
    cause, is that it's computationally much
    more expensive to do end-to-end formal
  • 4:50 - 4:55
    verifications and doing this end-to-end
    verification of a processor against an ISA
  • 4:55 - 4:59
    specification is something that
    historically was always fueled as the
  • 4:59 - 5:04
    textbook example of things that you can't
    do with formal methods, but fortunately
  • 5:04 - 5:09
    the solvers... they became much better in
    the last couple of years and now if we use
  • 5:09 - 5:14
    the right tricks, we can do stuff like
    that with the solvers we have nowadays.
  • 5:14 - 5:20
    So, that's riscv-formal. riscv-formal is a
    framework that allows us to do end-to-end
  • 5:20 - 5:24
    formal verification of RISC-V processors
    against a formal version of the ISA
  • 5:24 - 5:30
    specification. So, riscv-formal is not a
    formally verified processor. Instead, if
  • 5:30 - 5:35
    you happen to have a RISC-V processor, you
    can use riscv-formal to prove that your
  • 5:35 - 5:41
    processor confirms to the ISA
    specification. For the most part, this is
  • 5:41 - 5:46
    using bounded methods. Theoretically, you
    could do unbounded proofs with riscv-
  • 5:46 - 5:52
    formal, but it's not the main use case.
    So, it's good for what we call "bug
  • 5:52 - 5:56
    hunting", because maybe there is a
    counterexample that would show, that the
  • 5:56 - 6:03
    processor could diverge from the desired
    behavior with 1000 or 5000 cycles, but
  • 6:03 - 6:07
    usually, when you have something like a
    processor and you can't reach a bad state
  • 6:07 - 6:12
    within the very short bounds, you have
    high confidence that actually your
  • 6:12 - 6:17
    processor implements the ISA correctly.
    So, if you have a processor and you would
  • 6:17 - 6:22
    like to integrate it with riscv-formal,
    you need to do 2 things: You need to add a
  • 6:22 - 6:28
    special trace port to your processor; it's
    called the RVFI trace port -- riscv-formal
  • 6:28 - 6:32
    interface trace port. And you have to
    configure riscv-formal so that riscv-
  • 6:32 - 6:40
    formal understands the attributes of your
    processor. So, for example, RISC-V is
  • 6:40 - 6:45
    available in a 32-bit and a 64-bit
    version. You have to tell riscv-formal, if
  • 6:45 - 6:51
    you want to verify a 32-bit or 64-bit
    processor. RISC-V is a modular ISA, so
  • 6:51 - 6:54
    there're a couple of extensions and you
    have to tell riscv-formal, which
  • 6:54 - 6:59
    extensions your processor
    actually implements.
  • 6:59 - 7:05
    And then there're a couple of other things
    that are transparent for a userland
  • 7:05 - 7:13
    process, like if unaligned loads or stores
    are supported by the hardware natively,
  • 7:13 - 7:18
    because RISC-V... the spec only says, that
    when you do an unaligned load or store,
  • 7:18 - 7:24
    then a userspace program can expect this
    load or store to succeed, but it might
  • 7:24 - 7:28
    take a long time, because there might be a
    machine interrupt handler that is
  • 7:28 - 7:35
    emulating an unaligned load store by doing
    alligned loads and stores, but if we do
  • 7:35 - 7:41
    this formal verification of the processor,
    then the riscv-formal framework must be
  • 7:41 - 7:45
    aware: "What is the expected behavior for
    your course?", "Should it trap when it
  • 7:45 - 7:51
    sees an unaligned load store or should it
    just perform the load store unaligned?"
  • 7:51 - 7:54
    So, what does this interface look like
    that you need to implement in your
  • 7:54 - 7:59
    processor if you would like to use riscv-
    formal? This is the current version of the
  • 7:59 - 8:04
    riscv-formal interface. Right now, there
    is no support for floating-point
  • 8:04 - 8:09
    instructions and there is no support for
    CSRs, but this is on the to-do list, so
  • 8:09 - 8:14
    this interface will grow larger and larger
    when we add these additional features, but
  • 8:14 - 8:18
    all these additional features will be
    optional. And one of the reasons is that
  • 8:18 - 8:22
    some might implement just small
    microcontrollers that actually don't have
  • 8:22 - 8:30
    floating-point cores or that don't have
    support for the privileged specification,
  • 8:30 - 8:35
    so they don't have CSRs. Through this
    interface, whenever the core retires an
  • 8:35 - 8:41
    instruction, it documents which
    instruction it retired; so it tells us
  • 8:41 - 8:46
    "This is the instruction where I retired;
    this was the program counter where I found
  • 8:46 - 8:50
    the instruction; this is the program
    counter for the next instruction; these
  • 8:50 - 8:54
    are the registers that I read and these
    are the values that I've observed in the
  • 8:54 - 8:58
    register file; this is the register that
    I've written and this is the value that I
  • 8:58 - 9:01
    have written to the register file"
    All that stuff.
  • 9:01 - 9:07
    So, in short, what we document through the
    riscv-formal interface, is the part of the
  • 9:07 - 9:12
    processor state that is observed by an
    instruction and the change to the state of
  • 9:12 - 9:17
    the processor that is performed by an
    instruction -- like changes to the
  • 9:17 - 9:24
    register file or changes to the program
    counter. And of course, most processors
  • 9:24 - 9:29
    actually are superscalar, even those
    processors that say they're non-
  • 9:29 - 9:34
    superscalar. In-order pipelines usually
    can do stuff like retire memory load
  • 9:34 - 9:38
    instructions out of order, in parallel to
    another instruction that does not write
  • 9:38 - 9:44
    the register, things like that. So, even
    with processors we usually don't think of
  • 9:44 - 9:49
    as superscalar processors, even with those
    processors, we need the capability to
  • 9:49 - 9:54
    retire more than one instruction each
    cycle and this can be done with this
  • 9:54 - 10:04
    "NRET" parameter. And we see all the ports
    5 times wider if NRET is 5. Okay, so then
  • 10:04 - 10:08
    we have a processor that implements this
    interface. What is the verification
  • 10:08 - 10:14
    strategy that riscv-formal follows in
    order to do this proof to formally verify
  • 10:14 - 10:21
    that our processor's actually correct? So,
    there is not one big proof that we run.
  • 10:21 - 10:27
    Instead, there is a large number of very
    small proofs that we run. This is the most
  • 10:27 - 10:33
    important trick when it comes to this and
    there are 2 categories of proofs: One
  • 10:33 - 10:38
    category is what I call the "instruction
    checks". We have one of those proofs for
  • 10:38 - 10:43
    each instruction in the ISA specification
    and each of the channels in the riscv-
  • 10:43 - 10:48
    formal interface. So, this is easily a
    couple of hundred proofs right there
  • 10:48 - 10:52
    because you easily have 100 instructions
    and if you have 2 channels, you already
  • 10:52 - 10:58
    have 200 proofs that you have to run. And
    what this instruction checks do, they
  • 10:58 - 11:04
    reset the processor or they started a
    symbolic state, if you would like to run a
  • 11:04 - 11:09
    unbounded proof, let the process run for a
    certain number of cycles and then it
  • 11:09 - 11:15
    assumes that in the last cycle, the
    processor will retire a certain
  • 11:15 - 11:17
    instruction. So, if this
    check checks if the "add"
  • 11:17 - 11:21
    instruction works correctly, it assumes
    that the last instruction retired in the
  • 11:21 - 11:28
    last cycle of this bounder checked will be
    an "add" instruction and then it looks at
  • 11:28 - 11:34
    all the interfaces on the riscv-formal
    interface, to make sure that this is
  • 11:34 - 11:37
    compliant with an "add" instruction. It
    checks if the instruction has been decoded
  • 11:37 - 11:42
    correctly; it checks if the register value
    we write to the register file is actually
  • 11:42 - 11:47
    the sum of the values we read from the
    register file. All that kind of stuff.
  • 11:47 - 11:51
    But, of course, if you just have these
    instruction checks, there is still a
  • 11:51 - 11:56
    certain verification gap, because the core
    might lie to us: The core might say "Oh, I
  • 11:56 - 12:00
    write this value to the register file",
    but then not write the value to the
  • 12:00 - 12:06
    register file, so we have to have a
    separate set of proofs that do not look at
  • 12:06 - 12:11
    the entire riscv-formal interface in one
    cycle, but look at only a small fraction
  • 12:11 - 12:16
    of the riscv- formal interface, but over a
    span of cycles. So, for example, there is
  • 12:16 - 12:20
    one check that says "If I write the
    register and then later I read the
  • 12:20 - 12:25
    register, I better read back the value
    that I've written to the register file"
  • 12:25 - 12:34
    and this I call "consistency checks". So,
    that's I think what I said already... So
  • 12:34 - 12:40
    for each instruction with riscv-formal, we
    have a instruction model that looks like
  • 12:40 - 12:46
    that. So, these are 2 slides: The first
    slides is just the interface there we have
  • 12:46 - 12:52
    a couple of signals from this riscv-formal
    interface that we read like the
  • 12:52 - 12:58
    instruction that we are executing, the
    program counter where we found this
  • 12:58 - 13:04
    instruction, the register values we read,
    and then we have a couple of signals that
  • 13:04 - 13:10
    are generated by our specification that
    are output of this specification module.
  • 13:10 - 13:18
    Like, which registers should we read?
    Which registers should we write? What
  • 13:18 - 13:22
    values should we write to that register?
    Stuff like that. So, that's the interface.
  • 13:22 - 13:27
    It's the same all the instructions and
    then we have a body that looks more
  • 13:27 - 13:31
    like that. For all the instructions that
    just decodes the instruction, checks if
  • 13:31 - 13:35
    this is actually the instruction the check
    is for. So, in this case it's an "add
  • 13:35 - 13:42
    immediate" instruction. And then you have
    things like the line near the bottom above
  • 13:42 - 13:46
    "default assignments": "assign
    spec_pc_wdata", for example, says "Okay,
  • 13:46 - 13:55
    the next PC must be 4 bytes later than the
    PC for this instruction. We must increment
  • 13:55 - 13:59
    the program counter by a value of 4 when
    we execute this instruction." Things like
  • 13:59 - 14:10
    that. So, you might see, there is no
    assert here, there are no assertions,
  • 14:10 - 14:14
    because this is just the model of what
    kind of behavior we would expect. And then
  • 14:14 - 14:18
    there is a wrapper that instantiates this
    and instantiates the call and builds the
  • 14:18 - 14:23
    proof and there are the assertions. The
    main reason why we don't have assertions
  • 14:23 - 14:28
    here, but instead we output the desired
    behavior here, is because I can also
  • 14:28 - 14:33
    generate monitor cores that can run
    alongside your core and check in
  • 14:33 - 14:38
    simulation or an emulation, an FPGA, if
    your core is doing the right thing. That
  • 14:38 - 14:44
    can be very, very helpful if you have a
    situation where you run your core for
  • 14:44 - 14:50
    maybe days and then you have some
    observable behavior that's not right, but
  • 14:50 - 14:54
    maybe there are thousands, even million,
    cycles between the point where you can
  • 14:54 - 14:58
    observe that something is wrong and the
    point where the process actually started
  • 14:58 - 15:03
    diverging from what the specification said
    and if you can use a monitor core like
  • 15:03 - 15:10
    that, then it's much easier to find bugs
    like this. Okay, so some examples of those
  • 15:10 - 15:15
    consistency checks.; the list is actually
    not complete and it varies a little bit
  • 15:15 - 15:20
    from processor to processor what kind of
    consistency checks we can actually run
  • 15:20 - 15:26
    with the processor we are looking at.
    There is a check if the program counter
  • 15:26 - 15:30
    for one instruction - so I have an
    instruction it says "This is the program
  • 15:30 - 15:32
    counter for the instruction and this is
    the program counter for the next
  • 15:32 - 15:37
    instruction" -- and then we can look at
    the next instruction and we can see is...
  • 15:37 - 15:41
    the program counter for that instruction
    actually approved the next program counter
  • 15:41 - 15:46
    value for the previous instruction and
    they must link together like that, but the
  • 15:46 - 15:52
    core might retire instructions out of
    order. So it might be, that we see the
  • 15:52 - 15:56
    first instruction for us and then the
    second instruction later, but it's also
  • 15:56 - 15:59
    possible that we will see the second
    instruction first and then the first
  • 15:59 - 16:04
    instruction later and because of that,
    there're 2 different checks: One for a
  • 16:04 - 16:09
    pair in the non-reversed order and for a
    pair of instruction in the reversed order.
  • 16:09 - 16:13
    There is one check that checks, if
    register value reads and writes are
  • 16:13 - 16:21
    consistent. There is one check that sees,
    if the processor is alive, so when I give
  • 16:21 - 16:29
    the processor certain fairness constrains,
    that the memory will always return, memory
  • 16:29 - 16:33
    reads at number of cycles, things like
    that, then I can use this to prove that
  • 16:33 - 16:37
    the process will not just suddenly freeze.
    This is very important and this will also
  • 16:37 - 16:41
    prove that the processor is not skipping
    instruction indices, which is very
  • 16:41 - 16:46
    important, because some of the other
    checks actually depend on the processor
  • 16:46 - 16:51
    behaving in this way. And so forth. So,
    there are couple of these consistency
  • 16:51 - 16:55
    checks and it's a nice exercise to sit
    down in a group of people and go through
  • 16:55 - 17:01
    the list of consistency checks and see
    which which set of them actually is
  • 17:01 - 17:06
    meaningful or which set of them actually
    leaves an interesting verification gap and
  • 17:06 - 17:12
    we still need to add checks for this or
    that processor then. Okay, so what kind of
  • 17:12 - 17:20
    bugs can it find? That's a super-hard
    question, because it's really hard to give
  • 17:20 - 17:26
    a complete list. It can definitely find
    incorrect single-threaded instruction
  • 17:26 - 17:29
    semantics. So, if you
    just implement a instruction
  • 17:29 - 17:34
    incorrectly in your core, then this will
    find it; no question about it. It can find
  • 17:34 - 17:39
    a lot of bugs and things like bypassing
    and forwarding and pipeline interlocks,
  • 17:39 - 17:47
    things like that. Things where you reorder
    stuff in a way you shouldn't reorder them,
  • 17:47 - 17:52
    freezes if you have this lifeness check,
    some bugs related to memory interfaces and
  • 17:52 - 17:59
    load/store consistency and things like
    that, but that depends on things like the
  • 17:59 - 18:04
    size of your cache lines, if this is a
    feasible proof or not. Bugs that we can't
  • 18:04 - 18:09
    find yet with riscv-formal are things that
    are not yet covered with the riscv-formal
  • 18:09 - 18:13
    interface, like the floating-point stuff
    or CSRs, but this is all on the to-do
  • 18:13 - 18:18
    list, so they are actively working on that
    and a year from now, this stuff will be
  • 18:18 - 18:25
    included. And anything related to
    concurrency between multiple heats. So
  • 18:25 - 18:28
    far, my excuse for that was, that the
    RISC-V memory model is not completely
  • 18:28 - 18:34
    specified yet, so I would not actually
    know what to check exactly, but right now
  • 18:34 - 18:39
    the RISC-V memory model is in the process
    of being finalized, so I won't have this
  • 18:39 - 18:46
    excuse for much, much longer. So, the
    processors currently supported PicoRV32,
  • 18:46 - 18:51
    which is my own processor, then RISC-V
    Rocket, which is probably the most famous
  • 18:51 - 18:57
    RISC-V implementation, and VexRiscv. And
    there are also a couple of others, but
  • 18:57 - 19:04
    they are not part of the open source
    release of riscv-formal. So, if you would
  • 19:04 - 19:11
    like to add support to riscv-formal for
    your RISC-V processor, then just check out
  • 19:11 - 19:16
    the riscv-formal repository, look at the
    "cores" directory, see which of the
  • 19:16 - 19:20
    supported cores's most closely to the code
    that you actually have and then just copy
  • 19:20 - 19:28
    that directory and make a couple of small
    modifications. So, I have a few minutes
  • 19:28 - 19:34
    left to talk about things like cut-points
    and blackboxes and other abstractions. So,
  • 19:34 - 19:38
    the title of this slide could just be
    "abstractions", because cut-points and
  • 19:38 - 19:42
    blackboxes are just abstractions.
    The idea behind an abstraction and formal
  • 19:42 - 19:48
    methods is that I switch out part of my
    design with a different part with a
  • 19:48 - 19:55
    different circuit that is less
    constrained, it includes the behavior of
  • 19:55 - 19:59
    the original circuit, but might do other
    stuff as well. So, the textbook example
  • 19:59 - 20:03
    would be, I have a design with a counter
    and usually the counter would just
  • 20:03 - 20:09
    increment in steps of 1, but now I create
    an abstraction that can skip numbers and
  • 20:09 - 20:16
    will just increment in strictly increasing
    steps. And this, of course, includes the
  • 20:16 - 20:20
    behavior of the original design, so if I
    can prove a property with this abstraction
  • 20:20 - 20:25
    in place instead of the just-increment-
    by-1 counter, then we have proven even a
  • 20:25 - 20:30
    stronger property and that includes the
    same property for the thing in the
  • 20:30 - 20:36
    original design. And actually this idea of
    abstractions works very well with riscv-
  • 20:36 - 20:41
    formal. So, the main reason why we do
    abstractions is because it leads to easier
  • 20:41 - 20:47
    proofs. So, for example, consider an
    instruction checker that just checks if
  • 20:47 - 20:52
    the core implements the "add" instruction
    correctly. For this checker, we don't
  • 20:52 - 20:56
    actually need a register file that's
    working. We could replace the register
  • 20:56 - 21:01
    file by something that just ignores all
    writes to it and whenever we read
  • 21:01 - 21:04
    something from the register file, it
    returns an arbitrary value. That would
  • 21:04 - 21:10
    still include the behavior of a core with
    a functional register file, but, because
  • 21:10 - 21:14
    the instruction checker does not care
    about consistency between register file
  • 21:14 - 21:18
    writes and register file reads, we can
    still prove that the instruction is
  • 21:18 - 21:23
    implemented correctly, and therefore we
    get an easier proof. Of course, we can't
  • 21:23 - 21:27
    use this abstraction for all those proofs,
    because the other proofs that actually
  • 21:27 - 21:33
    check if my register file works as I would
    expect it to work, but if we go through
  • 21:33 - 21:37
    the list of proofs and we run all these
    proofs independently, then you will see
  • 21:37 - 21:42
    that for each of them, it's possible to
    abstract away a large portion of your
  • 21:42 - 21:47
    processor and therefore yield
    and an easier proof.
  • 21:47 - 21:51
    Depending on what kind of solvers you use,
    some solvers're actually very capable of
  • 21:51 - 21:55
    finding these kind of abstractions
    themselves. So in that cases, it doesn't
  • 21:55 - 21:59
    really help by adding these abstractions
    manually, but just realizing that the
  • 21:59 - 22:04
    potential for these abstractions is there,
    is something that's very useful when
  • 22:04 - 22:09
    guiding your decisions how to split up a
    large verification problem into smaller
  • 22:09 - 22:13
    verification problems, because you would
    like to split up the problem in a way so
  • 22:13 - 22:17
    that the solver is always capable of
    finding useful abstractions that actually
  • 22:17 - 22:28
    lead to easier circuits to prove. With a
    bounded check, we also have the questions
  • 22:28 - 22:33
    of what bounds do we use. Of course,
    larger bounds are better, but larger
  • 22:33 - 22:42
    bounds also yield something that is harder
    to compute, and if you have a small bound,
  • 22:42 - 22:45
    then you have a proof that runs very, very
    quickly, but maybe you're not very
  • 22:45 - 22:50
    confident that it actually has proven
    something that's relevant for you. So, I
  • 22:50 - 22:57
    propose 2 solutions for this: The first
    solution is, you can use the same solvers
  • 22:57 - 23:02
    to find traces that cover certain events
    and you could write a list and say "I
  • 23:02 - 23:07
    would like to see 1 memory read and 1
    memory write and at least one ALU
  • 23:07 - 23:11
    instruction executed" and things like
    that. And then, you can ask the solver
  • 23:11 - 23:19
    "What is the shortest trace that would
    actually satisfy all this stuff?" And when
  • 23:19 - 23:25
    that's a trace of, say 25 cycles, then you
    know "Okay, when I look at a prove that's
  • 23:25 - 23:30
    25 cyclic deep, I know at least these are
    the cases that are going to be covered."
  • 23:30 - 23:35
    But more important, I think, is: Usually
    when you have a processor, you already
  • 23:35 - 23:41
    found bugs and it's a good idea to not
    just fix the bugs and forget about them,
  • 23:41 - 23:47
    but preserve some way of re-introducing
    the bugs, just to see if your testing
  • 23:47 - 23:52
    framework works. So,
    if you have already a couple of bugs
  • 23:52 - 23:55
    and you know "It took me a week to find
    that and took me a month to find that",
  • 23:55 - 24:01
    the best thing is to just add the bugs to
    your design again and see "What are the
  • 24:01 - 24:05
    bounds that are necessary for riscv-formal
    to actually discover those bugs" and then
  • 24:05 - 24:09
    you will have some degree of confidence
    that other similar bugs would also have
  • 24:09 - 24:16
    been found with the same bounds. So,
    "Results": I have found bugs in pretty much
  • 24:16 - 24:23
    every implementation I looked at; I found
    bugs in all 3 processors; we found bugs in
  • 24:23 - 24:28
    Spike, which is the official implementation
    of RISC-V in C and I found
  • 24:28 - 24:34
    a way to formally verify my specification
    against Spike and in some cases where I found
  • 24:34 - 24:37
    the difference between my specification
    and Spike, it turned out, it
  • 24:37 - 24:42
    was actually a bug in the English language
    specification. So, because of that, I also
  • 24:42 - 24:48
    found bugs in the English language
    specification with riscv-formal. "Future
  • 24:48 - 24:54
    work": Multipliers already supported,
    floating-point is still on the to-do list,
  • 24:54 - 25:02
    64-bit is half done. We would like to add
    support for CSRs. We would like to add
  • 25:02 - 25:06
    support for more cores, but this is
    something that I would like to do slowly,
  • 25:06 - 25:11
    because adding more cores also means we
    have less flexibility with changing
  • 25:11 - 25:18
    things. And better integration with non-
    free tools, because right now all of that
  • 25:18 - 25:23
    runs with open source tools that I also
    happen to write -- so, I wrote those
  • 25:23 - 25:28
    tools, but some people actually don't want
    to use my open source tools; they would
  • 25:28 - 25:31
    like to use the commercial tools -- and
    it's the to-do list that I have better
  • 25:31 - 25:36
    integration with those tools. Maybe,
    because I don't get licenses to those
  • 25:36 - 25:41
    tools, so we will see how this works.
    That's it. Do we have still time for
  • 25:41 - 26:03
    questions?
    applause
  • 26:03 - 26:05
    Clifford: So, I'd say we start with
    questions at 1.
  • 26:05 - 26:11
    Herald: I'm sorry; here we go. We have 2
    questions; we have time for 2 questions
  • 26:11 - 26:16
    and we're going to start with microphone
    number 1, please.
  • 26:16 - 26:23
    M1: Hello, thanks for your talk and for
    your work. First question: You told about
  • 26:23 - 26:27
    riscv-formal interface.
    Clifford: Yes.
  • 26:27 - 26:34
    M1: So, does vendor ship the final
    processor with this interface available?
  • 26:34 - 26:40
    Clifford: Oh, that's a great question,
    thank you. This interface has only output
  • 26:40 - 26:45
    ports and actually when you implement this
    interface, you should not add something to
  • 26:45 - 26:49
    your design that's not needed to generate
    those output ports. So, what you can do
  • 26:49 - 26:54
    is, you can take the version of your core
    with that interface, the version of the
  • 26:54 - 26:58
    core without that interface. Then, in your
    synthesis script, just remove those output
  • 26:58 - 27:04
    ports and then run a formal equivalence
    check between that version and the version
  • 27:04 - 27:11
    that you actually deploy on your ASIC.
    M1: Thanks; and one short question: When
  • 27:11 - 27:17
    people say formal verification, usually
    others think "Oh, if it is verified, it is
  • 27:17 - 27:26
    excellent, absolutely excellent. Do you
    plan to say that it will find all the
  • 27:26 - 27:31
    erato for the processor?
    Clifford: Well, it depends on what kind of
  • 27:31 - 27:36
    proof you run. The most work I do is with
    bounded proofs and there you only get a
  • 27:36 - 27:41
    certain degree of confidence, because you
    only see bugs that can occur within a
  • 27:41 - 27:46
    certain number of cycles from reset, but
    if you want, you can also run a complete
  • 27:46 - 27:53
    proof, where you start with a symbolic
    state instead of a reset state and then
  • 27:53 - 27:58
    you can can make sure that you actually
    check the entire reachable state space,
  • 27:58 - 28:02
    but that's a very, very hard thing to do
    So, that's not a weekend project. Just
  • 28:02 - 28:06
    adding the riscv-formal interface and
    running some bounded proofs is probably a
  • 28:06 - 28:11
    weekend project if you already have
    your RISC-V processor.
  • 28:11 - 28:13
    M1: Thank you.
    Herald: Thank you. We actually do not have
  • 28:13 - 28:18
    time for any more questions, but there
    will be time after the talk to ask you
  • 28:18 - 28:22
    questions... maybe?
    Clifford: Yeah. So, maybe you can find me
  • 28:22 - 28:27
    at the open FPGA assembly, which is part
    of the hardware hacking area.
  • 28:27 - 28:33
    Herald: Super. Very great job to put that
    much information into 30 minutes. Please
  • 28:33 - 28:36
    help me thank Cliff
    for his wonderful talk.
  • 28:36 - 28:44
    applause
  • 28:44 - 28:49
    34c3 outro
  • 28:49 - 29:06
    subtitles created by c3subtitles.de
    in the year 2018. Join, and help us!
Title:
34C3 - End-to-end formal ISA verification of RISC-V processors with riscv-formal
Description:

more » « less
Video Language:
English
Duration:
29:06

English subtitles

Revisions Compare revisions