If you are a beginning FPGA designer, the first example you will be given to learn is that of a counter. It’s sort of a tradition. Class room exercises all illustrate concepts with simple counters. If you ask a question, the instructor will go to the board and start his explanation with a counter. At least, that’s what I would do if I trying to teach an Verilog concept.
But just how useful is a counter in the end anyway?
Let’s try examining a counter all the way from an irrelevant classroom discussion to a vital system component.
How can this be? Well, one peripheral necessary to any multitasking operating system, whether Unix, Linux, Windows, or some other O/S, is an interval timer. An interval timer is little more than a reconfigurable counter. All it does is issue an interrupt to the CPU at a periodic interval.
Embedded systems, such as those found within FPGA’s, have an additional timing need. These systems often need to insert known delays between different operations. Instead of an interval timer, these systems need what are known as “one-shot” timers. Once programmed, they generate an interrupt after the programmed delay takes place and then they return to idle.
The ZipCPU wrapper known as the ZipSystem has three such timers within it, shown in Fig 1 as “Generic Timers (x3)”. I call these timers ZipTimers. Each of these ZipTimers supports generating either a regular interrupt or a one-shot delay based interrupt. These ZipTimers have been a part of the ZipSystem since I started. Their simplicity makes them perfect candidates for beginner exercises, and even better candidates for learning formal verification.
The ZipTimer has two capabilities beyond the traditional beginner’s counter exercise. These are first the ability to be programmed over a wishbone bus, and second the ability to interrupt the CPU when the specified delay runs out.
Therefore, let’s examine this timer peripheral as an exercise in learning Verilog, formal verification, and connecting a simple item to a bus using AutoFPGA. Along the way, I’ll do my best to avoid calling this a “counter example”.
The Beginner’s Exercise
Hopefully everyone reading this blog has at one time built a countdown timer in Verilog. Indeed, I use a basic countdown timer as one of the first examples in the Formal Verification course I now teach. Below is the simple example timer that we’ll start with today.
This counter starts at zero. Any time an
i_start signal takes place, the
counter is set to
TIMEOUT and then counts down to zero, as illustrated in
Fig 2. Note that
setting this counter to
TIMEOUT doesn’t guarantee that it will take
TIMEOUT clock ticks until it returns to zero–it is possible the
signal resets this counter back to
TIMEOUT before it hits zero.
We’ll also create an interrupt signal that we will set anytime the counter becomes zero.
That’s not all that hard, right?
Did you notice the subtlety associated with checking
One of my readers pointed this out. If
i_start happens to be true on the
same cycle that
o_int might be true on a clock cycle
r_value != 0. Yes, this is a bug. It’ll come back in the next section
as well. However, I’m going to leave this bug in place because this was how I
originally designed the
this bug within it. (Oops!) It wasn’t until years later when I attempted to
formally verify the
presented below that I discovered this subtlety.
For now, let’s just peel this onion back a bit further.
The problem with the above implementation of a counter is that it isn’t very
reusable. If you are going to generate a counter that will be
then you’ll want to add a
bus interface .
If we use the
(i_wb_stb)&&(i_wb_we) is true, and the address reflects our
timer’s address, then we can reload our timer from
This would give us a more adaptable, configurable timer. Such a
could easily become a
This works fine for
implementations, but what if you want this counter to run in a context
initial statements are
ignored? In that case,
you need an
i_reset input. On a reset, that is when
i_reset is high,
the counter should return to idle,
r_value == 0.
In a similar fashion, with only a tiny adjustment, we can use this module
to count events. We’ll use an incoming
i_ce signal to denote when an event
has taken place. Examples of such events include not only clock cycles
i_ce=1), but also incoming or outgoing samples in a
system, or lines or frames in a video system. All of these options can
be created by appropriately setting an
i_ce input to one any time the
timer is to
Put together, our original counter now becomes,
That’s quite the configurable counter, no?
We can do this if the current counter state data is always valid on the
Voila! A simple, wishbone bus controlled count-down timer!
The former code works great for a one-shot timer. However, if you want to create a timer that interrupts the CPU every 10ms (as an example), only to be reset by the CPU in an interrupt service routine, then you will find that the interval pseudorandomly walks in phase. The intervals will all be longer then 10ms. How can we fix this?
As before, we’ll generate an interrupt anytime this timer hits zero,
This is almost identical to our original counter above, save that every time
it resets it goes back to
r_interval_count instead of the original
r_interval_count is programmable from the
we now have a programmable interrupt
How hard can this be?
In this case, the devil is in the details.
Look closer. Do you see any of the problems with this implementation? For example, what happens if you want to switch from a 4-second intervals to 10ms intervals? Just how many counts will that first 10ms interval contain? Up to 4 seconds?
If that’s not the response you want, then how should this timer respond?
While we consider this, let’s also consider merging the countdown timer together with the interval timer in a way that both respond to bus requests. Here’s the capability or requirement we’ll build to then:
On any reset, the counter will set itself to zero and wait to be configured
This matches the count-down timer behavior we discussed above.
On any write, the counter will assume the value written to it, as shown in Fig 4 as the
New Counterbits, and will then start counting down. If the number written was a zero, then the counter will stay at zero and stop.
Again, this matches the count-down timer behavior we originally discussed.
If the high bit is set upon any write, shown as
Rin Fig 4 above, then the timer will enter into interval mode. In all other cases, the timer will be started as a one-shot countdown timer.
This is our first break from the original countdown timer’s functionality, allowing us to run in an interval timer mode.
Further, if set to interval mode, then the value written to the timer will become the interval definition. Hence, when the timer finishes counting down to zero, we’ll just automatically restart it again with the same
New Countervalue just written to it.
On writing a zero to the counter, all ongoing counts will be ended and the counter will return to idle. Any interval capability will be turned off.
We’ll also use a global CE register,
i_ce. This will allow you to count down things other than clock cycles. Perhaps you can count incoming samples on an interface. Perhaps you want to count video frames. Perhaps you want to count finished instructions. All of these can be implemented with an appropriate connection to this
Simple enough? Almost.
If low logic is a priority, and it has always been a priority for me, then
you’ll also want to be able to configure this peripheral for just the amount
of logic necessary. We’ll use the parameter
VW to control how many bits
are in our counter. We’ll also use
BW to be the width of the data
bus–nominally 32 bits. Finally we’ll use the one bit parameter,
RELOADABLE to control whether or not this timer offers an
mode or not. For example, if you know you are only ever going to measure
20ms intervals from a 100MHz clock, then you won’t ever need any
Simple enough now? I thought so. Let’s dive into a walk through of the code.
We’ll walk through the code of the ZipTimer in two separate sections. First, we’ll discuss the traditional Verilog code. Then we’ll move from that to the formal properties section. Once we’ve finished discussing the formal properties within the code, I show how to connect a peripheral like this to an AutoFPGA based design.
Normally I skip the front matter of a Verilog file when blogging, so as to
only focus on the relevant portions. In this case, I’ll show the three
BW, containing the size of the bus,
VW, containing the
number of bits in our counter, and
RELOADABLE–set to one if we want
to support an
capability in addition to the one-shot timer capability.
I’ll also simplify the write command below to a
wb_write flag. Since you’ll
see this often below, here’s the declaration.
We’ll also use a flag
r_running to keep track of whether or not the
r_running any time it is non-zero, or any time it is
zero and about to reload for the next interval. If we wanted to, it would
make sense to scribble in our
at this point that,
The contrary case, where
r_running is not true, will be a little more
difficult to specify so we’ll save it until we have to think our way through it
in the next section. Either way, when we get to building our
section, we’ll then copy our scribbled notes over
so we can place all of our
in one place.
Moving on, if you recall from above, we used a
option to select whether or not this
ability, or just a one-shot capability. Hence, if
RELOADABLE is true
then we’ll include this
capability itself centers around two registers. The
r_auto_reload, is a single bit flag telling us whether or not the
needs to be restarted once it hits zero. The second register will tell us
what our interval is should
r_auto_reload be set–but we’ll get to that
in a moment.
Initially, I cleared this
r_auto_reload value upon any reset and set it
on any write where the most significant bit is set.
This approach failed when I tried to
When I dug a bit deeper, I realized that the
interval could never be allowed to be zero. Were it zero, this would
r_running assertion we placed into our notes above.
Hence, I rewrote the
r_auto_reload logic above into,
The big difference is that in order to create an interval timer, you need to not only set the high order bit but you must also provide a non-zero interval length.
The second item worth commenting on here is the assign statement.
By assigning to a global
wire value within a
generate block, I
can then use this
wire value throughout the rest of my design without
needing to waste
RELOADABLE is false and I don’t need them.
Optimizations within the synthesizer will then remove any extra logic dependent
upon these values.
The next register associated with the
capability is the
r_interval_count register–containing the the interval
length expressed as value to reset our register to after it reaches zero.
On any write, we’ll set this interval count to the information found on the
r_auto_reload we just dealt with
above will determine whether or not this
r_interval_count is relevant or not.
Finally, if we are building without the
capability, we’ll set both of these values,
to zero. The synthesizer will then remove any of the relevant
Let’s now dig into the core of this count-down timer: the counter’s value,
r_value. This follows primarily from the counter we started with, corrected
by our discussion above, but now with the changes necessary to handle both an
capability as well as a one-shot countdown
Otherwise, we’ll adjust the
i_ce is true and the
is currently running. As you may remember from above, the
r_running any time
r_value it is nonzero, or we are in
r_auto_reload is true).
If the counter is not zero, we’ll count down.
Once it reaches zero, we’ll restart it if we are in
mode. In this mode,
auto_reload will be true.
auto_reload is not set then once the counter reaches zero, the
The next register in our implementation is
r_zero is a helper
register. It needs to
be equivalent to
r_value == 0. (We’ll prove that these two expressions
evaluate to the same value in a moment.) By setting
r_zero on the clock
r_value reaches zero, we relieve some of the timing stress within
this module. Hence, instead of an always block that depends upon whether
r_value == 0, such as the original designs we started out with,
they can instead depend upon a single pre-calculated single-bit value
The final required piece of logic is the
o_int. While we might consider setting the
r_zero, we’d then get lots of
every time the counter was idle. We’d also get lots of
between any pair of
i_ce strobes while the counter was waiting to reload.
Hence, we’ll only set the
r_value transitions to zero, or more explicitly any time it is
equal to one and the
i_ce register is high.
Other wishbone return return values follow from our prior discussion:
That’s all it takes to generate a timer peripheral for a CPU. It’s a bit more than the simple counter we started out with. In the next section, we’ll discuss how we might go about formally verifying this timer.
The formal proof
If you just want a quick reminder, there are two basic operators we’ll be using
assume() operator restricts the size of the possible state space
will examine. The
assert() operator defines which states within
this group are illegal. The formal engine will try all possible logic threads
to find one where the
expression inside the
assert() statement can be made to be false.
To know which of
assert() to use for any particular
property, I follow the rule shown in Fig 5. Hence, we’ll
any properties about our inputs, and we’ll
assert() any properties
about our own internal state or any outputs we might produce.
There is a third operator we’ll be using as well. This is the
operator. As we use it below, this operator returns the value of the
item within it one clock ago. The problem with the
$past operator is that
it tends to misbehave prior to the beginning of time. Hence, any time you
see me using this you’ll also see
f_past_valid in the condition list.
As with most of my
sections, they start with the definition of the
I just mentioned. We discussed this above, and in more detail
Basically, any assertion regarding something one clock in the
initial settings, will fail.
By checking for
f_past_valid being true as part of a formal logic
test, I can then use
$past() expressions in any
assert() statements below
without worrying about whether or not the logic being referenced occurred
before time began.
The next order of business is bounding the
i_reset signal. This signal needs
to be true initially. We’ll also insist that it’s true any time
is false. Aren’t these two the same condition? Not quite. While they are
very similar, they are separate conditions. This second
condition specifies that any time the induction engine tries to set
f_past_valid to false, then the
i_reset line must also be true which will
then force the design into its initial state.
If we do this properly, we can use
f_past_valid being false as an indication
that our design should be in its reset state. In a similar fashion, on the
clock following any
i_reset, the design should also be in its reset state.
We’ll pull any value from above that has an
initial statement or responds
i_reset signal, and insist on either condition that the registers
have the same value. We’ll also desk check our design to make certain that
registers set via an
initial statement are also responsive to an
and vice-versa. That is, an
initial statement should set the register
to the same value that an
i_reset would set them to.
Let’s now move on to some internal consistency checks. For example, we
stated above that we wanted
r_zero to be equivalent to
Let’s now assert that this relationship holds.
Likewise, anytime our value is non-zero the timer should be running.
In a similar fashion, any time we are in interval mode we should be running.
Perhaps you may recall these from our scribbled notes above as well?
Further, if our parameter
RELOADABLE is false, then
also be false.
auto_reload is true, we should have a non-zero interval
Those are the simple properties. The next several are more complex.
Our next step will be to work through the properties associated with
For the first of these more complex properties, we’ll say that any
r_value==0, i.e. any time the
has stopped counting down, then it should stay that way. However, if you try
to express this simply,
you might be surprised that your assertion doesn’t hold. You’ll first find
that following a
r_value might be something other than zero.
You’ll then discover that, by design, following an automatic reload it won’t
be zero either. Hence, the actual property is a touch more complex.
Next, let’s consider the case where
r_value was equal to zero on the last
clock, but isn’t equal to zero any more. Specifically, we want to test
whether the interval
started over on a reload as desired.
In this case, the simple property has several exceptions to it. The counter
won’t move to its reload value following a reset, nor will it necessarily
move to its reload value following a
Finally, it should only restart if
i_ce is true, and in all other
cases remain where it was.
Now let’s consider the case where the
r_value is not equal to zero on
the last clock. While I’d like to write the assertion that,
the formal engine again corrects me with several traces showing why this
isn’t the case. The first trace reminds me that, following a reset,
r_value will be zero. Once I fix that and try again, the second trace
reminds me that
r_value can be anything
Rather than running the formal tools again, I go back and desk check this
time to discover that
i_ce isn’t true on the last clock then
r_value shouldn’t change.
This brings us to the following property,
How about a bus write? Following a bus write, we want our counter to have the data written to it in our value. The exception is a reset. If a bus write and a reset occur on the same clock, we’d rather reset.
This also applies to the interval length. Following a bus write, if the value is non-zero, and if this module is built with the interval timer capability, then the high bit will determine whether or not we enter into interval timer mode.
We’re almost done. Before leaving, we need to double check our output
o_int, should be set any time
r_value transitions from
0. Or, at least, that was my original thought. Then as I worked through
this logic using formal
I realized there were some exceptions.
wire should be zero as well. This will allow us to turn the timer off by
simply writing a zero to it. Likewise, if
i_ce wasn’t true on the last clock, then we didn’t just hit zero and the
should be clear again.
So when should the output
be set? Any time we transition to zero.
Hence, it should be set following the clock where
i_ce was high and
r_value was a one.
Our last formal properties are associated with the wishbone bus. At first glance, these properties below may just appear like restatements of the logic above. In many ways they are. However, by placing these here I know I won’t carelessly adjust this interface logic while trying to optimize things.
That’s the last of our formal properties. Did you notice along the way how the formal engine helped us find the right properties for our code? That it found subtleties like the reset condition that needed to be checked for? Not only that, did you notice how the formal engine helped us flesh out the final details in our timer implementation?
These are all reasons why I have now started using formal methods before ever writing a test bench or running a simulation. Using formal methods helps me discover details I might otherwise not think about.
We have one more task before we are done: connecting this timer to the rest of our design. If you are using AutoFPGA, that’s just as easy as adding the configuration file for this timer to the AutoFPGA command line. Alternatively, we could connect this to the bus interconnect by hand, but I think you’ll find it simpler to use AutoFPGA.
Normally this isn’t necessary with the ZipCPU since the ZipTimer is already connected manually within the ZipSystem module, shown above in Fig 1. Two recent AutoFPGA based designs, one for the MAX-1000 and another for the TinyFPGA (neither quite complete), however, don’t use the ZipSystem but rather the bare ZipBones ZipCPU wrapper, shown in Fig 6.
You may recall from the general format of an
configuration file that the entries consist of
@KEY=VALUE pairs. They are
primarily used to tell
what text to copy and paste into a set of various project files.
VALUE takes less than a line, the
@KEY=VALUE definition can be
placed on a single line. Otherwise, all of the lines following
consist of the
VALUE for that key. Likewise, if the
VALUE is numeric,
you can have
calculate the value by placing a
$ between the
@ and the
KEY and so use
@$KEY=EXPRESSION form. Finally, to reference
@KEYONE=VALONE, from within another, you would reference
@$(KEYONE) within the value portion of the second
Perhaps this would make more sense if we walked through an example.
component description begins with a
@PREFIX tag. This defines the beginning
of the component, as well as providing a name for the component.
I chose to call this device a
bustimer. Unlike other timers that might be
internal to other portions of the design, this one can be accessed from the
main wishbone bus–hence
If you are following along from the
file, you can skip to the
@PREFIX=bustimer line. The information prior
defines how to connect the
wrapper to the bus. A watchdog timer definition follows this one, all within
doesn’t require it, I often define a
@DEVID tag. I
primarily use this tag for contexts that don’t like lower case.
doesn’t do anything fancy with this tag, other then paste it into other
tags as I tell it to below.
file of an
based project starts with a series of
ifdef’s just before the
module declaration. This allows a user to select
some items and not others, as well as capturing a set of dependencies of what
items depend upon others. In this case, we have no dependencies, but we’ll
still create an
define line in case something else depends upon this
Now let’s connect our timer to a
Specifically, we want to connect this component to the system
by default named
We’ll also declare that this
slave whose result is always available and that never stalls,
@SLAVE.TYPE=SINGLE, and one that has only a single address,
Actually connecting this to a
depends upon the code we want to place into our
file. This is the purpose of the
@MAIN.INSERT tag. Code within
this tag will get copied directly (after variable name substitution) into the
While you don’t need to reference the
@$(PREFIX) tag at all, I often use this
to help keep the names unique within any given design. Once the pattern
matching takes place, these lines will just turn into:
You don’t need to define the
will define these for you once you tell it that this item is a
will also create a
bustimer_sel wire. This wire will be true any time this
component’s address is selected. You do need to connect these wires to your
component, as we’ve done above.
The last wire,
bustimer_int, is also defined automatically by
part of generating and connecting up the
wires. In our case, we have a programmable interrupt controller
defined elsewhere in the
with the name of
buspic. Hence, all we need to tell
is that we have an
bustimer_int, that needs to be connected to the
after assigning this peripheral to interrupt control wire number one.
The last two parts deal with non-Verilog parts of the design. The first of
these deals with connecting this device to the external debugging
Specifically, we’ll want to create a register,
R_BUSTIMER, with the human
BUSTIMER. These next three lines adjust the files
First, upon reading these lines,
will place a definition into the
output file, defining an
R_BUSTIMER identifier to be equivalent to the address of this
register. This will tell external host components where in the memory
space to access this register when using
will also place references to this register into
contains a mapping between the computer regiser name
and the user name for this register,
BUSTIMER. As a result, you can then
wbregs program, a variant of the old fashioned
peek and poke hardware interface,
to read from the
with the command
wbregs bustimer, or to write to it via
wbregs bustimer newvalue.
(I have another version of this program called
avregs for use with the
The last item places a reference to this bus timer into the board.h file. This file would be used by the ZipCPU to know if the bus timer was built into the design and, if so, what address that timer was placed into.
Remember, the goal of AutoFPGA is to make the inclusion of bus components into a design easier. Hence, by placing these few lines into an AutoFPGA configuration file, this bus timer will be included into the design. Removing these lines from the AutoFPGA configuration will seemlessly remove this bus timer from the design.
We’ve now gone over everything it takes to create a useful countdown timer within an FPGA design–whether a “one-shot” timer, or a fully programmable interval timer. Once put together, the final Verilog code isn’t all that much more difficult than the original counter we started out from. What may surprise you, though, is how much work we went through to place such a simple counter into a design. Not only did we formally verify our timer, but then we also had to connect it to the wishbone bus within the design. We also dealt with several subtle issues associated with making a timer useful along the way.
What can you use such a timer for?
We’ve already discussed how this can be the centerpiece of the multitasking implementation within an Operating System. Upon any timer interrupt, the Operating System can then swap user tasks or processes. Should the Lord will, I’ll come back and share how one ZipCPU implementation uses this interrupt for exactly that purpose.
There’s another valuable use of a timer such as this–one which may not be as obvious. In the presentation above, we discussed wiring the interrupt wire to the CPU’s interrupt controller. If you instead connected the interrupt output to the reset wire for the CPU, you would have created a watchdog timer.
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)