To date, our formal verification efforts have primarily centered around synchronous designs using yosys, that is those designs where all logic transitions on the same clock edge, rather than looking at asynchronous designs. The one exception so far has been the description of how to get an asynchronous reset to pass induction. I’d like to move beyond this simple example towards verifying a full asynchronous FIFO design, but that’s going to require a bit more background in how to formally verify an asynchronous design in general. Today, therefore, let’s examine how to formally verify an asynchronous component that crosses between clock domains.

If you aren’t familiar with formal verification, you might wish to go back and review our introductory article on the topic. You might also find the induction exercise to be valuable as well.

Today, let’s demonstrate how these same formal verification concepts apply an asynchronous design with two clocks within it. In this case, we’ll examine a clock switch. Such a switch takes two clock inputs and one line to select between them. In our case, the two separate clocks makes a perfect example of how formal methods can be applied to an asynchronous design.

# Two Clocks

The first and most important step is to somehow describe both clocks via formal properties to the SMT solver. This step is really independent of anything you might wish to verify, and it applies to any asynchronous design. Once you learn the simple trick involved, you’ll then notice that other asynchronous verification proofs follow the exact same approach.

Specifically, we need to provide some assumptions to describe the two clocks which will be the inputs to our clock switch design. Why assumptions? Because these clocks will be inputs, and the basic rule is that you should always make assumptions about your inputs, and assertions about your local state and any outputs.

Perhaps you may remember our earlier discussion of how to create a fractional clock divider? In that article, we used the top bit of a counter as a divided clock.

Clocks like this one that are generated from logic are often called logic clocks. Logic clocks are distinguished from regular clocks in that are generated from logic within the design, rather than external hardware or internal PLLs, and are then distributed across the design and used like a clock. In general, you don’t want to transition on the positive or negative edge of any logic clock. Doing so will make it harder to achieve timing closure, and it will add additional clock domain crossing requirements to your design. Further, if this divided clock isn’t placed on the clock network, then it might be seen to rise (or fall) at inconsistent times across the design.

All of these are “bad” hardware consequences.

None of these problems, however, will keep us from using the transitions of this divided clock as a formal constraint on our clock input, so that’s exactly what we are about to do.

We’ll start out by creating counters, `f_*_count`, and increments, `f_*_step`, for each input clock.

In order to handle properties associated with any particular speed, we’ll allow these increments to be completely arbitrary.

The `\$anyconst` description is specific to yosys. It means that these values will have a constant value given to them–any value. It’s roughly the same as having an extra unconstrained input to the design and then forcing it to be `\$stable`. Alternatively, you can think of it as a register with no initial statement that doesn’t produce a yosys warning on synthesis.

However, these arbitrary constant values aren’t quite what we want yet. For example, any increment having a zero value would indicate a clock that doesn’t tick. This is bad, so we’ll force the increments to be greater than zero.

In a similar fashion, we can also constrain the clocks so that the fastest one, whichever that one might be, takes four simulation time steps per cycle.

This will help make certain that there is always a positive edge to the clock at least once per cycle.

Now that we have an increment, we just add this increment to our counters on every formal step–one counter per incoming clock.

Let me draw your attention to the `\$global_clock` statement within the always header. In SystemVerilog, this value needs to be declared earlier in the file as a positive or negative edge trigger based upon some pre-existing clock. Yosys, however, extends this behavior by making `\$global_clock` the formal verification time step. Every time step is now examined by the formal engine, not just those times described by an edge of a clock but intermediate times as well. It’s for this reason that we can use `\$global_clock` in this circumstance. Indeed, `\$global_clock` is one of the keys to this whole operation.

Our last formal property will be to assume that our incoming clock signals are identical to the most significant bits of our counters.

Simple enough? We’ve just assumed the presence of two dissimilar clocks coming into our design. We’ve also allowed them to have arbitrary phases and frequencies with respect to each other.

There is one more required piece of yosys, magic, you’ll need to add `clk2fflogic` to your yosys script file. Alternatively, if you are using SymbiYosys, you can instead add `multiclock on` to the options section. You can see an example of this SymbiYosys script here.

No more setup work is required–we’ve just formally assumed the existence of two separate and dissimilar clock inputs. In the next section, we’ll examine a clock switch design and discuss how we might formally verify that it is glitch free.

# A Clock Switch

At this point in our article, I usually present a working design that would use the principle under discussion and formal verify it. Sadly, I only have a couple of asynchronous designs to share. I just haven’t had the need to build that many. That said, neither my formal proof of Cliff Cumming’s asynchronous FIFO design, nor the proof of my UART receiver would be appropriate for a beginning blog post on asynchronous formal verification despite the fact that both proofs use the techniques discussed here.

So let’s try something simpler. Let’s instead examine a clock switch.

A clock switch is a design component that takes two clock inputs and a switch input, and produces one of the two clocks as its output dependent upon how the switch is set. It’s not something an FPGA designer normally needs to build, since most FPGA vendor libraries provide similar components which will be known to work on their parts. As an example, Xilinx offers a `BUFGMUX` design element with similar capabilities. However, for today’s purpose, a clock switch design makes a perfect example of an asynchronous design which can be formally verified.

Clock switches are very important parts of a failsafe designs. A failsafe design can start with one clock and then switch to the second clock once it stabilizes. In a similar fashion, if the second clock becomes unstable or otherwise unusable, then the clock switch should return the design to the original clock. A third use for a clock switch would be in a power sensitive design. In such a power sensitive design, the clock might be switched between a fast and a slow clock in order to control how much power the design is using at any given time.

So, how would you build a clock switch?

A straight forward clock switch design might look like,

Sadly, this doesn’t work. The problem is that the switch input `i_sel` is asynchronous to at least one of the two clock domains if not both. The output clock period might therefore be something other than the period of either clock if `i_sel` changes mid clock. Worse, the period could easily be shorter then the minimum pulse width of this design.

A little googling turns up a fascinating article on EE Times discussing, “Techniques to make clock switching glitch free.” In the article, Mahmud provides just the logic we need.

According to the article, the key piece we are missing is a pair of synchronizers. Since the clock select input isn’t guaranteed to be synchronous to either clock, it must be synchronized into each clock’s domain. Once the clock select line has been split and synchronized into each respective clock domain, the output clock can then be synthesized by `and`ing each leg of the clock domain with its respective enable, and `or`ing the result together.

This sounds simple enough. Indeed, the article and the picture are so clear that writing out the design is quite straightforward.

Notice that this synchronizer uses both edges of the clock to synchronize on. This would be a bad idea in an FPGA, since you have no control over how far apart the design elements are. However, this isn’t quite the same problem on an ASIC, as this design could be delivered as an internally routed black box.

The logic for B’s side is identical, save that it is based upon the negation of our select signal.

As the final step, the output clock is determined by clock `A` if `a_sel` is ever true, and by clock `B` if `b_sel` is true.

This design would be bad practice within an FPGA. Besides transitioning on both positive and negative edges of a clock, we are also sourcing a clock from combinational logic. Both of these are big no-no’s in any FPGA. design. If you want a clock switch within your FPGA. design logic, use the vendor supplied black box that implements something approximating (or better than) the above logic.

Shall we see if we can formally verify whether this circuit truly works?

# Formally Verifying the clock switch

Our first formal verification step is to determine what the “contract” is that this design needs to meet. Specifically, we want to make certain that

1. The outgoing clock should only transition when one of the incoming clocks transitions.

2. The output clock’s high or low pulse width is no less than the width of the fastest clock

3. We can switch from one clock to another

Let’s work through these one by one. The first criteria is easy: if neither input clock rises, then we’ll assert that the output doesn’t rise either.

Notice how I needed to add an exception for the asynchronous reset. Hence this property will only hold as long as the reset line remains inactive (high).

Likewise, if neither input falls, then the output shouldn’t fall either.

If you don’t recognize the `f_past_valid` signal, we’ve discussed it many times on this blog. It is necessitated by the fact that on the initial time step, `\$rose()`, `\$fell()`, and `\$past()` are not well defined. Instead, we set the `f_past_valid` just after that initial time step, and then start checking on every step thereafter.

The second criteria is a little harder to describe. Indeed, our design choice to use a fractional clock makes this more difficult. Because we are looking at the most significant bit of a counter, it’s not immediately apparent how long each clock should be high. Without a divide operator to tell us how long we’d expect each clock leg to be high or low we’re sort of stuck.

We could switch from the fractional clock division description above to an integer divide:

This would offer some different properties to the clock, so I would encourage anyone interested to try this approach.

For this post, however, we’ll continue with the fractional divider and see if we can’t find a simpler approach.

If you examine the logic for the output clock, `o_clk`, you’ll see that the output clock is determined by either `a_sel` or `b_sel`. If `a_sel` is true, clock `A` is produced. Likewise if `b_sel` is true, then clock B is produced. If neither is true, there should be no clock pulse out. However, both should never be true at the same time.

We might also choose to assert that `a_sel` or `b_sel` would only change on a clock edge.

However, if you examine the design above you’ll see that this is indeed the case by examination—with the exception of the asynchronous reset input. This one piece of our logic might produce a clock glitch, but we’ll assume that if you are using an asynchronous reset then you know what you are doing and you can handle such a glitch.

For our final criteria, let’s count clock ticks in each clock domain. We’ll start with the `A` clock domain.

We’ll do the same in a moment with the `B` clock domain. For now, let’s keep track of the number of clock ticks we’ve had in the `A` domain, and remember this value even after we leave the `A` domain.

We’ll then repeat this logic for the `B` clock domain–both counting how many ticks have taken place since changing, and keeping track of that count once we switch back to `A`s clock.

To make our traces look nice, we’ll assume that there must be at least three clock ticks between switches. Since this minimum duration properties isn’t really a fundamental part of our proof, we’ll place it within an parameterized option to the core.

Using these two measures of the number of times either `A` or `B` has ticked between clock swaps, we can now ask the formal tools to `cover()` a clock transition from A to B where A is at least twice as fast as `B`, and again from `B` to `A`.

Now, if everything works, then when we run SymbiYosys with a `mode` of `cover`, and using the `cover` task defined by the SymbiYosys script, we’ll get two traces of clock transitions.

So we’ve now described two of the three properties above, and hand waved through the third. Will this work?

Not quite.

Should you test this core with only those properties above, you’ll discover as I did that they aren’t sufficient to ensure that this clock switch even worked. You can see the output from SymbiYosys below.

From this, we determine that our assertion from line 184 failed.

## What happened?

If you look near the bottom of the SymbiYosys output, you’ll see a line identifying a counterexample trace. We can use this trace to find out why our proof didn’t work. This trace is shown in Fig 5 below.

If you look closely at the penultimate time step, between 70ns and 80ns, you’ll notice that both `a_sel` and `b_sel` are true at the same time. This should never happen! This violates all of the properties we are hoping to get from this clock divider.

Looking closer, you can see that `i_sel` (shown in red) didn’t simply change from selecting clock A to clock B. Instead, it started out requesting clock `B`, suddenly switched to selecting clock `A`, and then immediately switched back before the synchronizers could settle. Such a signal on then `i_sel` select line would defeat the purpose of our clock switch, so it’s not really all that reasonable.

On the other hand, if we assume that `i_sel` won’t change until the clock transition is complete, then we get a lot farther:

As another way we might express this, we might insist that anytime there is a change propagating through the synchronizers then `i_sel` will be held constant.

Getting this design to pass induction requires some additional properties. For example, we can’t allow the design to be transitioning in both rails at the same time.

With these changes the design passes, proving our first criteria–that the outgoing clock only ever changes on an input clock edge. We also have a meager assurance that the outgoing clock will not be faster than either incoming clock. Perhaps we should examine the third criteria, and see how this switch works when swapping?

As you may recall, our third criteria was whether or not we could switch from one clock to the other or back again. To see whether or not we met this criteria, we’ll need to run SymbiYosys in its cover mode. Our script has a `cover` task defined within it that does just that. The result is two generated clock traces that illustrate how clock transitions might happen.

The first trace shows that a design can switch from a faster clock to a slower clock.

The second trace, on the other hand, shows the clock switching from a slower clock to a faster clock.

But what about the idea of a failsafe clock? Didn’t we say that one reason for using a clock switch is to be able to have a failsafe clock, where if one dies then the other one picks back up?

This particular design doesn’t support a failsafe clock. If `A` is the failsafe clock, and `B` stops transitioning, then you can’t switch from `B` back to `A` using this design since `b_sel` depends upon both a positive and a negative transition from clock `B`.

Even though this clock switch design doesn’t offer a failsafe capability, you should now understand the tools necessary to prove that your own design, perhaps even one with a failsafe capability, would work—but only in an ASIC design of course! (Remember, the clock switch is not appropriate for an FPGA design for the reasons given above.)

## Next Steps

Let’s think about what we just did. We just verified that a design with three asynchronous inputs “works”. This involved formally describing two dissimilar clocks with arbitrary phases and frequencies. These techniques apply well beyond this simple clock switch design. These techniques can be used in any asynchronous design component to verify that your logic is working as desired–in spite of whatever clock phases or frequencies might be given to it.

While working with asynchronous inputs isn’t common, there are times and places for doing so. I’ve already mentioned some examples above: an asynchronous reset, a serial port receiver, or perhaps a circuit that must read memory at one clock rate and feed a video stream at another rate. In all of these cases, knowing how to formally verify your component in spite of any multiple clock domains will be a valuable tool.

The next step in this short series on asynchronous logic will be to take Cliff Cummings’ asynchronous FIFO design, and apply the same basic formal verification steps we just applied above.

As an added bonus in this process, you should be able to then turn around and formally verify any modifications you need to make to his design to meet your particular design requirements.