Hello FPGAmigos ! In our previous discussion, we delved into creating a basic testbench using Chisel. Today, we’ll explore Formal Verification using SymbiYosys from YosysHQ. I was guided by the informative slides from ZipCPU. Interestingly, I later realized that Fabien Marteau had already undertaken a similar journey as detailed here. It’s quite intriguing how we both converged on similar solutions. I’ll share some reflective insights on this in today’s blog post.

This blog post isn’t intended to offer a comprehensive explanation of formal verification; I’ve only dabbled in it briefly. Instead, its aim is to highlight a basic use case and assist newcomers. For a more in-depth understanding, ZipCPU has penned numerous articles on the subject and has some excellent slides (available as part of a paid course) which can be accessed here.

The Design

Today’s culprit is a simple counter.

import chisel3._
import chisel3.util._

class Counter(max_count: Int) extends Module{

val io = IO(new Bundle{
	val enable = Input(Bool())
	val count = Output(UInt(log2Ceil(max_count).W))
	val pulse = Output(Bool())
})
val reg_count = RegInit(0.U(log2Ceil(max_count).W))

when(io.enable){
	reg_count := Mux(reg_count===max_count.U, 0.U, reg_count+1.U)
}
io.count := reg_count
io.pulse := reg_count === max_count.U
}

object Main extends App{
(new chisel3.stage.ChiselStage).emitVerilog(new Counter(12), Array("--target-dir", "build/artifacts/netlist/"))
}

What stands out about this example is its simplicity and the way it illuminates a common thought process that can lead to errors. The source code related to this blog post is available on my GitHub. I’ve employed Docker images to work with Chisel, which can be accessed here.

The underlying thought process during the design of this counter was that the “pulse” signal would have a width of 1, implying that it could only be asserted for a single cycle. When integrating it into my design, I tacitly ASSUMED it would always operate in this manner. Which, of course , is not the case. Such oversights often become the root of bugs. This particular bug becomes apparent upon analyzing the design. In fact, I deliberately designed this counter with this specific flaw. If you haven’t spotted it yet, fear not; the beauty of formal verification will help you uncover it.

Formal Verification with SymbiYosys

An Install SymbiYosys

SymbiYosys is an open-source tool that serves as a front-end for the formal verification of designs. In essence, it offers a comprehensive yet user-friendly interface for formal verification, streamlining the complexities of synthesis and the use of formal solver tools.

I adhered to the standard installation process, which can be found here, but executed it within a Dockerfile. I sourced the OSS CAD SUITE release from here. This suite bundles Yosys, SymbiYosys, and numerous formal solvers, saving me the trouble of installing each one individually.

FROM ubuntu:20.04

COPY oss-cad-suite-linux-x64-20231007.tgz /tmp
WORKDIR /tmp
RUN tar -xvf oss-cad-suite-linux-x64-20231007.tgz -C /opt; \
    rm oss-cad-suite-linux-x64-20231007.tgz
ENV PATH /opt/oss-cad-suite/bin:$PATH

You can build it like this:

docker build --progress=plain -t osscad .

SymbiYosys Files

[options]
mode prove
depth 20

[engines]
smtbmc

[script]
read -formal Counter.v
prep -top Counter

[files]
build/artifacts/netlist/Counter.v

The counter.sby file encompasses all the information SymbiYosys requires to validate that the properties your system should always maintain are indeed consistently upheld.

• Options: This section lets you determine the mode and depth. As of now, it’s configured to “prove” with a depth of 20. From my understanding, it utilizes an algorithm to verify that the property remains valid for 20 cycles, followed by another algorithm ensuring its validity for the 21st cycle. It then extrapolates this to infer its perpetual accuracy. That’s my take, but I’d recommend delving into ZipCPU’s slides for a clearer picture. While pinpointing the bug is our current focus, a thorough explanation of how formal verification operates might necessitate additional blog posts or even a full course. SymbiYosys’s primary advantage is its ability to streamline this intricate process.
• Engines: SymbiYosys supports multiple formal solver engines. In this section, you can select your preferred engine(s). A comprehensive list of compatible engines is available here.
• Script: This instructs SymbiYosys on how to handle the files and specifies the primary module.
• Files: Indicates the locations of pertinent files. SymbiYosys will replicate these into a dedicated directory.

For the source files:

1. Chisel will generate a Counter.v in the traget directory () according to the last line of the source file:

(new chisel3.stage.ChiselStage).emitVerilog(new Counter(12), Array("--target-dir", "build/artifacts/netlist/"))

“build/artifacts/netlist/” for me but you can change it. It is also the path to give to the .sby file in the “[files]” section.

2. We need to incorporate the formal assertions and assumptions into our Counter.v file. I’ve created a separate file named formal_counter.sv that exclusively contains these formal assertions and assumptions.

// Spoiler alert : this code is not enough to formally verify your design
`ifdef FORMAL
always @(posedge clk) begin
	assert (count<=12);
end
`endif

3. At this point, my approach mirrors Fabien Marteau’s as described in his blog post. I employed a quick and dirty script to incorporate the contents of the formal verification file. Personally, I used a bash script named “concat.sh” (which can be found in the source), generated by ChatGPT. This script essentially appends the contents of the formal verification file directly into my Counter.v as follows:

./concat.sh formal_counter.sv Counter.v

This method of injection isn’t what I’d term as elegant, and I’ll delve into an alternative idea towards the end of the post.

Finding Assumptions and Assertions

SymbiYosys employs a sophisticated blend of mathematical models and algorithms to rigorously analyze your design. In essence, it conducts what can be described as ‘wise brute forcing’: it systematically and intelligently probes a vast range of possibilities, including some cleverly selected edge cases, to determine if any can violate the set assertions. There’s a catch, though. The sheer range of possibilities means it might also test scenarios that are “illegal” or outside the intended design specifications. As designers, it’s crucial for us to ensure that we initiate from a valid, legal state. This is the role of assumptions. This provides a solid starting point to validate that from such states, our system can’t transition into any undesired or illegal conditions (i.e failling assertions).

Fixing illegal states with assumptions

Let’s configure my counter with a max_count of 12, indicating that I want it to count up to 12 and no further. The intuitive assertion here would be: “the counter value should never exceed 12.”

In Verilog, this would be represented as follows:

`ifdef FORMAL
always @(posedge clk) begin
	assert (count<=12);
end
`endif

Take note of the preprocessor directives “ifdef FORMAL … endif”. All your assertions and assumptions should be enclosed within this scope.

To initiate the formal verification, execute the following command:

sby -f src/formal/counter.sby

Aaaaand … it fails !!

(SymbiYosys generate a trace.vcd, look at the log of the simulation the path is given).

Ta-da! If the starting value in the register is 14, then our assertion fails.

You might argue, “But hold on… I’ll always begin with a reset, which sets the register to 0 initially. If the register starts from 0, there’s no way it can reach 14, so the trace you’re showing me is irrelevant.”

And you’d be spot on! Starting the counter at 14 is, indeed, an unauthorized state. Your reliance on the reset is an unspoken assumption we didn’t formally account for.

This underscores the importance of explicit assumptions. They ensure the solver doesn’t kick off in an illegitimate state, focusing instead on the design’s pertinent states.

Let’s try to add an assumption :

`ifdef FORMAL
initial assume(reset);
always @(posedge clk) begin
	assert (count<=12);
end
`endif

The statement assume(reset) implies that at the commencement of the simulation, the reset should be set to 1.

This felt like a reasonable assumption to me, until… it failed.

Upon the rising edge of the clock, the initial value persists, causing the assertion to fail.

Once more, I realized I had made an oversight—a subconscious assumption—that I wanted the property to remain valid consistently, but only when not in a reset state

Let’s try to correct it:

initial assume(reset);
always @(posedge clk) begin
	if(reset==0)
		assert(io_count <=12);
end

We operate under the assumption that our design is reset at the start of the simulation. Only when the reset is set to 0, do we proceed with testing.

And voilà! It succeeds!

A little difference compared to ZipCPU

In ZipCPU’s slides, there’s a signal named “f_past_valid.” In the context of my example, it would be represented as follows:

reg f_past_valid;
initial f_past_valid = 1'b0;
always @(posedge clk) begin
	f_past_valid = 1'b1;
end

always @(posedge clk) begin
	if(f_past_valid==1)
		assert(io_count <=12);
end

It seems somewhat analogous to what I achieved using my reset. Perhaps this approach is more versatile, especially considering not all modules necessarily come with a reset signal. When in doubt, it might be wise to follow his lead.

Formally verifying the pulse property

Now, we’ll incorporate the pulse assertion to ensure that the pulse signal is consistently asserted for the duration of one clock cycle:

initial assume(reset);
always @(posedge clk) begin
	if(reset==0)
		assert(io_count <=12);
end
always @(posedge clk) begin
	if(reset==0 && $past(io_pulse==1)) 
		assert(io_pulse==0);
end

For every rising edge of the clock post-reset, if the pulse signal (io_pulse) was set to 1 in the previous cycle, it should be 0 in the current one (assertion(io_pulse==0)).

However, upon executing the formal verification, we find that this assertion doesn’t consistently remain valid.

Indeed, if the enable signal is deasserted in the same clock cycle as the pulse signal being asserted, the pulse signal remains active. This means it isn’t always a pulse as originally intended.

Now, let’s move on to the correction:

class Counter(max_count: Int) extends Module{
val io = IO(new Bundle{
	val enable = Input(Bool())
	val count = Output(UInt(log2Ceil(max_count).W))
	val pulse = Output(Bool())
	})

val reg_count = RegInit(0.U(log2Ceil(max_count).W))
when(io.enable){
	reg_count := Mux(reg_count===max_count.U, 0.U, reg_count+1.U)
	io.pulse := reg_count === max_count.U
}
io.count := reg_count
io.pulse := false.B
}

We simply need to ensure that the pulse signal is asserted only when the enable signal is active, and remains inactive otherwise.

Reflections on Formal Assertion Injection

As I mentioned earlier, while tools like the concat.sh script or Martoni’s Python script available on his GitHub serve the purpose, I find them lacking in elegance. In this segment, I’m outlining a feature I envision—though a full discussion of its implementation will be reserved for another blog post. This is primarily because I prefer a singular focus per post, but also to get your insights on the idea (maybe it’s completely misguided).

Initially, I hoped to see this feature integrated at the chisel level. One approach might be to repurpose the Chisel BlackBox or setinline for injections, but I’m skeptical of its success. Moreover, even if it were possible, leveraging functions in unintended ways isn’t particularly elegant either. If you’re aware of a method to achieve this using existing Chisel features, I’d love to read your comments.

I pondered over the idea of extending Chisel’s base type, adding formal assertions to them:

class Pulse extends Bool {
	include_formal("my_formal_file.sv") // a file with only assertions and assumptions
}
// OR
class Pulse extends Bool {
	set_inline_formal("
	always @(posedge clk) begin
	if(reset==0 && $past(io_pulse==1)) 
		assert(io_pulse==0);
	end"
	)
}
class Counter(max_count: int) extends Module {
val io = IO(new Bundle {
	val pulse = Input(Pulse())
})
// ...
}

The resulting counter.v would then directly encompass the formal assertions and assumptions. While Pulse would operate just like a Bool —not triggering any Chisel errors even if used inappropriately—the application of SymbiYosys on the generated counter.v would fail if pulse is incorrectly driven in your design.

However, this approach seems fitting only when testing the module in isolation. As ZipCPU rightly states, “assume the inputs, assert the internals and the outputs.” Hence, if a small module, complete with assumptions on its inputs, is embedded within a larger one, its input assumptions would need to transition into assertions.

Is it worth integrating full Yosys formal verification support into Chisel? (or creating a package for that ?) Does it even make sense or bring any added value? That’s still up in the air—it’s probably wise to liaise with the Chisel community on this.

In an ideal world, I’d be able to craft circuits using data types or interfaces that have elements of formal verification built right into them. Using pulse as a case in point, consider a “count” data type: instead of designating a UInt, we could label a “Counter” that operates just like an UInt but would churn out the following formal assertion:

always @(posedge clk) begin
	assert (count<=max_count);
end

I’m eager to know your thoughts on this concept.

Conclusion

I hope you found this exploration into formal verification enlightening. Personally, I’m convinced that incorporating formal verification into my workflow is essential for producing reliable designs. SymbiYosys, with its user-friendly interface, truly democratizes this process, and I’m grateful to ZipCPU for the invaluable tutorials.

I’d be curious to know about any amusing or unexpected bugs you’ve uncovered in your designs using formal verification.

If this piece resonated with you, please don’t hesitate to bookmark, share, and drop a comment. Your feedback is always appreciated!