Clock Domain Crossings
can be difficult to get right. This applies not only
to crossing data and logic from one clock domain to another, but also to
crossing resets from one clock domain to another. The general rule is that all
logic must have a guaranteed settling time before the next rising edge of
the next clock.
If this rule is violated then logic may enter a state that
0, neither true nor false.
This is metastability. Avoid it at all costs.
In the case of an asynchronous reset, it usually doesn’t matter all that much during which clock interval the design enters into the reset state. As long as the reset remains active long enough to fully propagate through the design, everything will eventually enter into this state. What matters is whether or not the whole design leaves the reset state at the same time: on a clock edge.
Fig 1. shows an example of such an asynchronous reset. The negative logic reset comes into the design with no guarantee of being synchronous with the clock. Flip-flops dependent upon that reset may then enter into a metastable state, shown by the pink background in the figure. Logic within the design needs to recognize this reset, and synchronize its release. This is shown by the green region, where the adjusted reset clears and returns to zero at the sime time as the rising edge of the system clock.
You may also notice from Fig 1 that the incoming asynchronous reset signal is based upon negative logic. In other words, to activate the reset the logic needs to be pulled low. This is a common practice in ASIC designs, since it allows a design to start entering into its reset state before sufficient power is available to assert a positive going reset across the entire design–although this isn’t usually required with FPGA designs.
Since the logic necessary to do this is pretty simple, let’s take a look at it in the next section.
For our simple Verilog example, let’s create a synchronous positive logic reset signal from a negative logic asynchronous reset.
The basic code
just sets the outgoing reset and the three
1 anytime the asynchronous reset is true, and then waits for three clock
edges to release. You can see this basic logic pictorially in Fig 2 on the
Since the code
itself is so short, I’ll spend a moment touching on some
details I usually avoid along the way. For example, I (now) always start
any Verilog design by setting the
This one statement is really a blessing when it comes to finding
errors within your code. Verilog specifies that the default synthesizer
behavior upon finding any undeclared identifier
is to assume that the identifier was supposed to reference a
wire, and so
the synthesizer will then quietly declare a
wire for you when you would have
rather had the synthesizer report an error due to your misspelling. By
telling the synthesis tool not to do this, it becomes much easier to catch
errors you might have in your code.
Our module will accept two inputs, and produce one output. The two inputs will
be the clock,
i_clk and the negative going asynchronous reset,
The underscores here have specific meanings.
i_ references an input,
o_ in a moment will reference an output, and in the case of this reset the
_n suffix references negative logic. The last item in our portlist is
our synchronized output signal,
To handle the synchronization, we’ll use a three clock
synchronizer. This requires
two internal state bits that we’ll call
We’ll also assume the design begins in a reset state, and so initialize our synchronization FIFO and our output to start in a reset condition.
Enough of the preliminaries. What does it take to synchronize a reset? Just the following four lines of code.
So how does this work? As shown in Fig 1 above, anytime
i_areset_n goes low
(active), then we set the synchonizer and the output reset registers to all
ones. Otherwise, if
i_areset_n is high (inactive), then on the positive
edge of the clock we’ll shift a zero into and through the the
shift register until it clears the
That’s it. There’s really not that much more to it.
When it comes to formal properties, I’ve recently started including “contracts” into the formal properties I write. I’ve found it valuable to clearly indicate what the minimum you want something to do is. Let’s do that here.
In this case, I can think of four basic properties that are relevant.
The first is our one assumption that we always start in a reset state.
Our next property is that any time
i_areset_n is low (active) our outgoing
o_reset must be high (active).
At this point I can hear someone asking, doesn’t that make this an asynchronous reset as well?
Yes, technically it does. However,
o_reset is guaranteed to also be high
for at least one clock before it is released, so we can (usually) just treat
it as a regular synchronous logic reset as well. There is a risk
that this reset will send some
for one clock cycle.
While this is a possibility when using
will be reset in the next clock interval. If this is not acceptable
for your logic, then just treat
o_reset as an asynchronous reset.
The third part of our contract is that we only ever leave the reset state
on the positive edge of any clock. This property is a little less intuitive
to express as an
assertion. Specifically, we want to assert that any
o_reset transitions from
0, i.e. any time it falls,
that the clock is also transitioning from
As one last part of our
cover() the release from reset to make certain this design will
release from reset like we expect it to.
At this point, if we only wanted to pass a bounded model check we’d be done. If you instead want to prove that this asynchronous reset works, then you’ll need to create some more formal properties.
These extra properties are primarily used to make certain that the induction engine doesn’t find the design in an unreachable state.
For the first of these properties, we’ll assert that any time the design
is not in a reset condition, then the
sync_fifo shift register bits should
be zero as well.
In a similar fashion, the
sync_fifo should never be able to get into
a state where the bits are
2'b01. This property is necessary
to keep the induction stage from starting in this unreachable
Likewise, any time
sync_fifo is true, then
o_reset should be active.
Finally, any time
i_areset_n is active (low), we’ll want to make certain
sync_fifo is in its full reset state as
All four of these criteria are necessary to make certain that the design passes induction.
That also ends the formal properties of our asynchronous reset module.
We’ve discussed SymbiYosys scripts a little on the blog, although we haven’t discussed SymbiYosys tasks much. For this design, we’ll use a SymbiYosys task so that we can have SymbiYosys handle both proveing that our design works, as well as the cover property above.
The second section of the
describes the options to be given to the formal solver. The
selects what mode we wish to run the solvers in. For the
prove task, we’ll
prove mode. This will apply both a bounded model check as well as
the k-induction pass. Passing this task will prove that the safety
properties hold. This applies to all of the
The second mode, used by our
second task, is the
cover mode. We’ll use this to make certain our
cover statement is reached. The final option,
multiclock on, applies
to both tasks. This option tells
that we’ll be using the asynchronous or multiple clock capabilities of the
The third section is the
[engines] section. This particular design doesn’t
really need any particular engine. We’ll pick
therefore, since it is a good general purpose engine.
The final section lists all the files in our design–in this case, just
We’re now ready to run SymbiYosys!
There’s really not much more to it. That’s all that’s required to formally verify a simple asynchronous reset design.
Proving that this asynchronous reset to synchronous release module works may seem trivial, but it does demonstrate a lot of the capabilities of the open source formal tools. For example, did you notice that this proof applies to any clock structure?
There are several other simple designs that can be proven just like this one. Examples include a clock gate, clock switch, input or output DDR components or even SERDES implementations. I discuss each these projects in my Formal Verification course, before offering them as student exercises. If the Lord is willing, we’ll continue with these techniques to create and then formally verify an asynchronous FIFO as a future post.
Come now, and let us reason together, saith the LORD: though your sins be as scarlet, they shall be as white as snow; though they be red like crimson, they shall be as wool. (Is 1:18)