Formal Verification

[maxhaton]

What facilities (and case studies/flows of) for Formal Verification exist in Bluespec?

[thoughtpolice]

The answers to this are complex without knowing exactly what kind of properties you want to hold. So I'll make a few points:

• Traditionally, the FOSS EDA community refers to "formal verification" as meaning, broadly speaking, "tools for doing bounded model checking and property specification of synchronous digital logic." It's a way of viewing circuits as logical primitives and showing that certain behaviors or properties do, or do not, exist in some manner, for some amounts of time, etc.

  Generally speaking, formal verification is largely a toolchain question. The most prominent open source example of this is Symbiyosys, which works on Verilog, and uses many open source components to perform verification. And the Bluespec compiler outputs Verilog! So you can do some kinds of things already. You could, for instance, use Yosys or Symbiyosys to prove that two Bluespec circuits are equivalent, which broadly comes down to a SAT problem.

• Bluespec as a language, however, does not provide much in the way of formal verification primitives known to Verilog. These primitives, known as SystemVerilog Assertions do exist, but are relatively undocumented and still experimental. These SVAs are very useful because you can put them in your design and they will be emitted in the resulting Verilog, to be checked by your tools. But most people don't use them, because...

• Bluespec makes it much easier to write correct designs, so the need for them appears much less often! The reason for this is due, in my opinion, to two features: the guarded atomic actions that define Bluespec, and the "compile time language" that lets you abstract things more easily. When bsc compiles your circuit, it inserts scheduling logic that automatically manages the rules you've defined and ensures they execute properly, with as much concurrency as possible. But every rule appears as if it executes atomically, as a single action. This property, called "One Rule At A Time" means you, as a human, have an easier job reasoning about circuits. But it has other concrete benefits: in Bluespec, you'll never need to manage any valid or ready handshake signals, any enable or reset lines, etc. These lead to a significant source of bugs.

  Second, the productive programming language that exists at "compile time", which is a variant of Haskell hiding in a Verilog trenchcoat, allows you to abstract rules and build correct, high level circuits easily. For example, it is nearly impossible to incorrectly wire two AXI4 endpoints together when using a primitive like mkConnection(client, server). This function builds modules, rules, and wires them together for you automatically, which is a level of abstraction that just doesn't exist in Verilog-level HDLs. There are tons of examples of functionality like this all throughout the Bluespec Prelude; FIFOs, BRAMs, etc all are built on these ideas.

Unfortunately I don't know of any case studies on using Bluespec or impacts on correctness, but personally I find it to be much easier to reason about the correctness of my designs in terms of concurrency, synchronous logic, etc. Instead you have to worry about things like method concurrency, rule conflicts, etc. But I find most of these don't impact correctness so much as performance, so the iterative method for design is a bit different...

[quark17]

I believe that there has been a variety of research that could be listed here. As @thoughtpolice suggests, "formal verification" is a broad term that can include many different things. And I think a lot of different groups have explored in different directions, under this umbrella -- though only touching on the tip of the iceberg of what is possible, I believe. Unfortunately, I have not kept track of this work, so I'm not able to list it; but I'm hoping that the people who do know more will comment here and share that. @thoughtpolice has made a good start of it, with some good points -- thanks! I can add a few things.

Folks at MIT have looked at using Coq (formal proof language) for working formally with Bluespec-style hardware. They have a project called Kami -- here is the webapge, with links to the researchers involved and some of the papers: https://plv.csail.mit.edu/kami/

One of the Kami researchers, Adam Chlipala, gave this talk on their formal verification of RISC-V hardware: https://www.youtube.com/watch?v=4DYVJdHMV5k

Galois is a company that develops security solutions and does a lot of work with languages, cryptography, and formal verification. They have done some work with Bluespec. Here is a paper on using their formal tools, extended to include a subset of BSV, for validating a RISC-V extension written in BSV: https://carrv.github.io/2018/papers/CARRV_2018_paper_5.pdf

Here's an overview of formal methods, given by Galois at a RISC-V workshop, and that mentions their SAW tool for BSV and their BESSPIN tool that supports multiple HDLs: https://riscv.org/wp-content/uploads/2018/12/13.35-Kiniry-Zimmerman-Formal-Methods-Need-Not-Be-Black-Magic.pdf

Galois' website has more links: https://galois.com/research-development/software-correctness/

Under the broad umbrella, there's even this older work by Shukla and Singh, about proving that the output of BSC implements the input design (along with other "model checking" problems, such as properties of the BSV design): https://link.springer.com/chapter/10.1007/978-3-540-85114-1_18

I imagine you can find links to other work like this by doing a web search of "Bluespec" plus related terms ("Formal Verification", "Coq", etc).

It probably doesn't count as "formal", but it's worth noting that the folks at the University of Cambridge developed a tool called Bluecheck that has been successfully used by many people. It is based on a software verification tool called QuickCheck, but it operates on Bluespec designs. You specify the atomic actions on a design and provide a golden model, and the tool will construct sequences of actions and test that the design and the model have the same behavior; and if a mismatch is found, the tool will reduce that sequence to a smallest sequence, as a minimal test case. /~https://github.com/CTSRD-CHERI/bluecheck

It's also worth noting that BSC does have some flags for dumping an elaborated, pre-scheduled design in a formal language. This was experimental work that was done for a researcher, but I don't know if anything came of it. One of the languages is SRI's SAL (Symbolic Analysis Language). The hidden flag -ddumpSAL can be used to dump the design; it will make use of primitives that need to be defined separately. The testsuite has examples in bsc.misc/sal/. Similarly, BSC can dump the design in a lambda calculus representation, with the -ddumpLambdaCalculus flag, and examples are in bsc.misc/lambda_calculus/. More info on SAL can be found here: http://sal.csl.sri.com

[quark17]

I'll add that Thomas Bourgeat, a grad student at MIT working with Arvind and Adam Chlipala, just defended his thesis, "Specification and verification of sequential machines in rule-based hardware languages". It involved formally proving the correctness of a family of pipelined processors, written in a rule-based BSV-like language.

They have a 2020 paper, "The Essence of Bluespec: A Core Language for Rule-Based Hardware Design", in which they defined a subset of BSV (called Kôika) that they can represent with Coq. Kôika tools are available on github](/~https://github.com/mit-plv/koika), including a formally verified compiler.

[maxhaton]

I was keeping it vague as to not preemptively deter any juicy info - thanks for the responses

[quark17]

I thought I'd also mention Andy Wright's recent PhD thesis (at MIT), Modular SMT-Based Verification of Rule-Based Hardware Designs. The abstract:

The highly-concurrent nature of hardware logic designs makes their design and verification difficult. Bluespec SystemVerilog (BSV) simplifies this problem by introducing the rule-level abstraction. Modules are expressed in terms of guarded atomic actions that appear to fire in a sequential order, even when multiple rules fire concurrently per clock cycle. This allows designers to think about concurrent systems one step at a time.

This thesis aims to make hardware verification easier by leveraging the rule-level abstraction for verification using SMT-based verification, e.g. bounded and unbounded model checking. The main aspect of the rule-level abstraction taken advantage of is the modularity. Rule-level modules can only be interacted with through their interface methods, so if a module looks the same as its specification with respect to the legal sequences of method calls, then they can be used interchangeably without affecting the outer module. A modular verification technique that is based off of this idea can be used to replace complex submodules with simpler versions that reduce the complexity and the number of steps required for unbounded model checking. This modular verification methodology can take many problems that are infeasible for unbounded model checking and makes them feasible. Other aspects of rule-level hardware design languages (HDLs) are taken advantage of during verification such as the use of uninterpreted functions and abstract types.

In this thesis, I present Spec 'n' Check, a rule-level hardware description language (HDL) inspired by BSV that is designed to support modular SMT-based verification and easy specification. To fully support SMT-based verification, we present formal semantics for Spec 'n' Check along with a symbolic representation of the semantics that can be used in SMT solvers. We also present what it means for a module to implement a specification and the related metatheorems that describe how the implements relation can be used to verify larger modules. We show that with this work, it is possible to formally verify a RISC-V pipelined processor implemented in the synthesizable subset of Spec 'n' Check against an ISA specification in a matter of minutes of SMT solver run time. This is only possible thanks to module refinement and abstraction of the control and status register file (CSRF) and the memory system, and the use of uninterpreted functions.

[thoughtpolice]

Looks like a great thesis! I'd love to give it a skim but it looks like the defense won't be for a few months. I'll keep a tab in my bookmarks, though...