Formally Verifying Asynchronous Components
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.
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.
$anyconst description is specific to
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
you can think of it as a register with no initial statement that doesn’t
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
this value needs to be declared earlier in the file
as a positive or negative edge trigger based upon some pre-existing clock.
however, extends this behavior by making
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
$global_clock is one of the keys to this whole
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
magic, you’ll need to add
clk2fflogic to your
script file. Alternatively, if you are using
you can instead add
multiclock on to the options section. You can
see an example of this
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.
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
designer normally needs to build, since most
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,
design makes a perfect example of an
design which can be
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
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.
the key piece we are missing is a pair of
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
leg of the clock domain with its respective enable, and
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_sel is ever true, and by clock
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
The outgoing clock should only transition when one of the incoming clocks transitions.
The output clock’s high or low pulse width is no less than the width of the fastest clock
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
$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
is true, clock
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
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
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
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
ticked between clock swaps, we can now ask the formal tools to
a clock transition from A to B where A is at least twice as fast as
and again from
Now, if everything works, then when we run
cover, and using the
cover task defined by the
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?
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.
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
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
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
i_sel select line would defeat the purpose of our clock
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
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
in its cover mode. Our
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.
A is the failsafe clock, and
B stops transitioning, then you
can’t switch from
B back to
A using this
b_sel depends upon both a positive and a negative transition from
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.)
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.
And he said unto them, It is not for you to know the times or the seasons, which the Father hath put in His own power. (Acts 1:7)