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 is neither 1 nor 0, neither true nor false.

This is metastability. Avoid it at all costs.

Fig 1. Synchronizing an Asynchronous Reset

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.

Verilog

For our simple Verilog example, let’s create a synchronous positive logic reset signal from a negative logic asynchronous reset.

Fig 2. Three Flip-flop Asynchronous Reset Synchronizer

The basic code just sets the outgoing reset and the three flip-flop synchronizers to 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 left.

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 default_nettype to none.

`default_nettype	none

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, i_areset_n. 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, o_reset.

module areset(i_clk, i_areset_n, o_reset);
	input	wire	i_clk, i_areset_n;
	output	reg	o_reset;

To handle the synchronization, we’ll use a three clock synchronizer. This requires two internal state bits that we’ll call sync_fifo.

	reg	[1:0]	sync_fifo;

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.

	initial	sync_fifo = 2'h3;
	initial	o_reset = 1'b1;

Enough of the preliminaries. What does it take to synchronize a reset? Just the following four lines of code.

	always @(posedge i_clk or negedge i_areset_n)
	if (!i_areset_n)
		{ o_reset, sync_fifo } <= 3'h7;
	else
		{ o_reset, sync_fifo } <= { sync_fifo, 1'b0 };

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 sync_fifo shift register until it clears the o_reset output.

That’s it. There’s really not that much more to it.

That is, there’s nothing more involved unless you want to formally verify that this operation works as advertised. Hence, let’s look at formally verifying this reset logic in the next section.

Formal Properties

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.

`ifdef	FORMAL
	////////////////////////////////////////////////////
	//
	// Our "contract"
	//
	////////////////////////////////////////////////////
	//

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.

	initial	assume(!i_areset_n);

Our next property is that any time i_areset_n is low (active) our outgoing reset value o_reset must be high (active).

	always @(*)
	if (!i_areset_n)
		assert(o_reset);

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 flip-flops into a metastable state for one clock cycle. While this is a possibility when using o_reset, those flip-flops 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 time o_reset transitions from 1 to 0, i.e. any time it falls, that the clock is also transitioning from 0 to 1 (rising).

	always @($global_clock)
	if ($fell(o_reset))
		assert($rose(i_clk));

As one last part of our formal proof, let’s cover() the release from reset to make certain this design will release from reset like we expect it to.

	always @(*)
		cover(!o_reset);

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.

	////////////////////////////////////////////////////
	//
	// Extras for passing induction
	//
	////////////////////////////////////////////////////

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.

	always @(*)
	if (!o_reset)
		assert(sync_fifo == 2'b00);

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 state.

	always @(*)
		assert(sync_fifo != 2'b01);

Likewise, any time sync_fifo[1] is true, then o_reset should be active.

	always @(*)
	if (sync_fifo[1])
		assert(o_reset);

Finally, any time i_areset_n is active (low), we’ll want to make certain that sync_fifo is in its full reset state as 2'b11.

	always @(*)
	if (!i_areset_n)
		assert(sync_fifo == 2'b11);

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.

SymbiYosys

If you want to prove this design using SymbiYosys, you’ll need to put a SymbiYosys script together to do so. Let’s take a quick moment to build this script.

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.

A SymbiYosys script with tasks in it starts with a [tasks] section declaring the names of the various tasks. In our case, we’ll declare a cover and a prove task.

[tasks]
prove
cover

The second section of the SymbiYosys script describes the options to be given to the formal solver. The mode option selects what mode we wish to run the solvers in. For the prove task, we’ll run in 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 assumes and asserts above. 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 SymbiYosys that we’ll be using the asynchronous or multiple clock capabilities of the formal solvers.

For those who have been following SymbiYosys development, this option replaces the clk2fflogic yosys option.

[options]
prove: mode prove
cover: mode cover
multiclock on

The third section is the [engines] section. This particular design doesn’t really need any particular engine. We’ll pick yices therefore, since it is a good general purpose engine.

[engines]
smtbmc yices

Alternatively, we might have just stated smtbmc without naming the yices engine, since yices is the default engine anyway.

That leaves two sections left. The fourth section lists the commands that yosys itself will use to prepare our design for the formal solver.

[script]
read_verilog -formal areset.v
prep -top areset

The final section lists all the files in our design–in this case, just areset.v.

[files]
areset.v

We’re now ready to run SymbiYosys!

> sby -f areset.sby

There’s really not much more to it. That’s all that’s required to formally verify a simple asynchronous reset design.

Conclusion

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.