Yosys error out of bound expression

I wonder what is happening in this example. Seems like computed ranges in generate blocks are problematic. Is this an issue of the code or some Yosis limitation?

Example follows:

`timescale 1ns / 1ps

module constant_value(out1); parameter BITSIZE_out1=1, value=0; // OUT output [BITSIZE_out1-1:0] out1; assign out1 = value; endmodule

module register_SE(clock, reset, in1, wenable, out1); parameter BITSIZE_in1=1, BITSIZE_out1=1; // IN input clock; input reset; input [BITSIZE_in1-1:0] in1; input wenable; // OUT output [BITSIZE_out1-1:0] out1; reg [BITSIZE_out1-1:0] reg_out1; assign out1 = reg_out1; always @(posedge clock) if (wenable) reg_out1 <= in1; endmodule

module top(clock, reset, in1, in2, in3, sel_LOAD, sel_STORE, S_oe_ram, S_we_ram, S_addr_ram, S_Wdata_ram, Sin_Rdata_ram, S_data_ram_size, Sin_DataRdy, out1, Sout_Rdata_ram, Sout_DataRdy, proxy_in1, proxy_in2, proxy_in3, proxy_sel_LOAD, proxy_sel_STORE, proxy_out1, dout_a, dout_b, memory_addr_a, memory_addr_b, din_value_aggregated, be, bram_write); parameter BITSIZE_in1=1, BITSIZE_in2=1, BITSIZE_in3=1, BITSIZE_out1=1, BITSIZE_S_addr_ram=1, BITSIZE_S_Wdata_ram=8, BITSIZE_Sin_Rdata_ram=8, BITSIZE_Sout_Rdata_ram=8, BITSIZE_S_data_ram_size=1, address_space_begin=0, address_space_rangesize=4, BUS_PIPELINED=1, BRAM_BITSIZE=32, PRIVATE_MEMORY=0, USE_SPARSE_MEMORY=1, BITSIZE_proxy_in1=1, BITSIZE_proxy_in2=1, BITSIZE_proxy_in3=1, BITSIZE_proxy_out1=1, BITSIZE_dout_a=1, BITSIZE_dout_b=1, BITSIZE_memory_addr_a=1, BITSIZE_memory_addr_b=1, BITSIZE_din_value_aggregated=1, BITSIZE_be=1, nbit_read_addr=32, n_byte_on_databus=4, n_mem_elements=4, n_bytes=4; // IN input clock; input reset; input [BITSIZE_in1-1:0] in1; input [BITSIZE_in2-1:0] in2; input [BITSIZE_in3-1:0] in3; input sel_LOAD; input sel_STORE; input S_oe_ram; input S_we_ram; input [BITSIZE_S_addr_ram-1:0] S_addr_ram; input [BITSIZE_S_Wdata_ram-1:0] S_Wdata_ram; input [BITSIZE_Sin_Rdata_ram-1:0] Sin_Rdata_ram; input [BITSIZE_S_data_ram_size-1:0] S_data_ram_size; input Sin_DataRdy; input [BITSIZE_proxy_in1-1:0] proxy_in1; input [BITSIZE_proxy_in2-1:0] proxy_in2; input [BITSIZE_proxy_in3-1:0] proxy_in3; input proxy_sel_LOAD; input proxy_sel_STORE; input [BITSIZE_dout_a-1:0] dout_a; input [BITSIZE_dout_b-1:0] dout_b; // OUT output [BITSIZE_out1-1:0] out1; output [BITSIZE_Sout_Rdata_ram-1:0] Sout_Rdata_ram; output Sout_DataRdy; output [BITSIZE_proxy_out1-1:0] proxy_out1; output [BITSIZE_memory_addr_a-1:0] memory_addr_a; output [BITSIZE_memory_addr_b-1:0] memory_addr_b; output [BITSIZE_din_value_aggregated-1:0] din_value_aggregated; output [BITSIZE_be-1:0] be; output bram_write; ifndef __ICARUS__ function integer log2; input integer value; integer temp_value; begin temp_value = value-1; for (log2=0; temp_value>0; log2=log2+1) temp_value = temp_value>>1; end endfunctionendif ifdef __ICARUS__ parameter nbit_addr = BITSIZE_S_addr_ram/*n_bytes == 1 ? 1 : $clog2(n_bytes)*/; parameter nbits_address_space_rangesize = $clog2(address_space_rangesize); parameter nbits_byte_offset = n_byte_on_databus==1 ? 1 : $clog2(n_byte_on_databus);else parameter nbit_addr = BITSIZE_S_addr_ram/n_bytes == 1 ? 1 : log2(n_bytes)/; parameter nbits_address_space_rangesize = log2(address_space_rangesize); parameter nbits_byte_offset = n_byte_on_databus==1 ? 1 : log2(n_byte_on_databus); `endif

function [n_byte_on_databus2-1:0] CONV; input [n_byte_on_databus2-1:0] po2; begin case (po2) 1:CONV=(1<<1)-1; 2:CONV=(1<<2)-1; 4:CONV=(1<<4)-1; 8:CONV=(1<<8)-1; 16:CONV=(1<<16)-1; 32:CONV=(1<<32)-1; default:CONV=-1; endcase end endfunction wire [2BRAM_BITSIZE-1:0] dout; wire [2BRAM_BITSIZE-1:0] out1_shifted; wire [2BRAM_BITSIZE-1:0] S_Wdata_ram_int; wire cs, oe_ram_cs, we_ram_cs; wire [n_byte_on_databus2-1:0] conv_in; wire [n_byte_on_databus*2-1:0] conv_out; wire [nbits_byte_offset-1:0] byte_offset; wire [BITSIZE_in2-1:0] tmp_addr; wire [nbit_addr-1:0] relative_addr;

reg we_ram_cs_delayed; reg oe_ram_cs_delayed; reg [nbits_byte_offset-1:0] delayed_byte_offset;

assign tmp_addr = (proxy_sel_LOAD||proxy_sel_STORE) ? proxy_in2 : in2;

generate genvar j0_a; for (j0_a=0; j0_a<n_byte_on_databus; j0_a=j0_a+1) begin : dout_a_computation assign dout[(j0_a+18-1):j0_a8] = dout_a[j0_a+18-1:j0_a8]; end endgenerate

endmodule

This is the error output:

ERROR: Range select out of bounds on signal `dout_a’ at main_minimal_interface.v:149!

Clifford Wolf has written a nice tool, yosys-smtbmc, based upon his
yosys synthesys tool, that allows you to apply
formal methods
to your Verilog code. The promise of
formal methods
is that you can then mathematically prove that your code works, or if not
then the formal solver should be able to tell you where your code is failing.

I’ve only been working with these
methods
for a week or so, but already there are some things I can share.

The first project I tried applying these formal methods to was a simple
SPI-based A/D converter. This particular
controller is designed to interact with a
Digilent product containing a
MEMs based microphone. I’ve had
the project
built for some time, although I’ll admit I’ve never actually done anything
more with it than plug it in.

Since the project is simple enough, I
thought I’d try applying
formal methods
to it, to prove that my controller worked. Sure, I had a test
bench
that I had built some time earlier to convince me that the project worked.
The design worked
well against this test
bench,
so I didn’t expect to find many problems using
formal methods.

Imagine my surprise when I found several bugs instead. Not only that, many of
those bugs were within my FIFO
implementation–something
that I’d passed from one project to another for some time. You see, when I
built my FIFO I only tested
it in a fashion such as a “reasonable” person might use it. Under this
“reasonable use” scenario, the
FIFO
had done well.

The formal prover, however, didn’t limit itself to what I considered
“reasonable” usage of the
FIFO.
It created underruns and overruns, wrote to the
FIFO
when it was full, and read from the
FIFO
when it was empty.
It even wrote and read from the empty
FIFO
on the same clock, and it wrote and read from the full
FIFO
on the same clock as well.
When the internal logic didn’t “match” the criteria I gave the solver, it then
showed me where my FIFO
code
didn’t properly handle these conditions.

I guess I just didn’t have that much creativity when I created my test
bench
in the first place.

Was the result worth it? Keep in mind, I’ve never used
these methods
before. So did I think it was worth it? I think so. I haven’t “proved”
all of my projects yet, nor do I know if I will be able to, but I have added
proofs to some of them—and found bugs as a result.

Today, though, I’d like to share some of what I have learned.

State Sets

If you’ve never worked with
formal methods
before, the basic concept is that you will
go through your code and declare which states are valid and which are not.
You’ll then use a theorem prover to mathematically prove that you can
never enter an invalid state from a valid one. If the prover cannot
prove this, then typically you will have either a bug in your
code, or a bug in your formal assertions.

You can think of the “state” as the values in all of your
flip-flops,
together with the values of all of your inputs.

The first step in yosys-smtbmc based theorem solving is the bounded model
checker (BMC), figuratively shown in Fig 1. This
part of the theorem solver starts your design in its initial state,
and then walks through all of the state transitions that it can, stepping your
logic forward from one time step to the next, just to see if any set of
conditions will drive your model to an invalid state.

This may be the most straightforward part of using yosys-smtbmc, and the
easiest to understand. The problem with the BMC step is that your time is
limited. Therefore, you will only want to allow the BMC step to check some
finite number of transitions. This number needs to be chosen carefully,
otherwise there may be states you might eventually get into over time that it
won’t find.

You can also find these additional states via the second step:
the induction step.

The induction step is just like the mathematical
induction you learned in
Pre-calculus. You
first prove that some property is true for the first value,
n=1. This was the purpose of the BMC step above. If it is true for this
base case, you then proceed with the inductive step. This step assumes that
your logic is within some initially valid state, say state n, and it then
tries to prove that your logic will only transition to a valid state,
say state n+1.

That’s the idea.

In practice, I’ve struggled with this induction step. The challenge
to the designer with the induction step is that you have to declare every
unreachable state as invalid, or it might start processing from an
unreachable state you aren’t expecting. As figure 2 shows, states
that are neither valid nor invalid,
but still states that the design will never reach, may easily become starting
states for induction. It is therefore up to the designer to clearly
indicate that all states must be either valid or invalid.

Let me try to explain this a touch better. In a moment we’ll go over some
System Verilog statements that
yosys
will recognize. These statements declare only the state that you cannot
get to. They do this by either reducing the size of the total state space
examined, or by declaring particular states to be illegal. That part is the
job of the formal specification designer. The job of the
formal method
is to determine which states may be reached, and to then cross check these
states against the illegal ones.

Perhaps a simple table, such as the one in Fig 4, might help to explain this.

What you want to know, as a designer, is whether or not there is any way that
you might reach an invalid state from a valid one. Hence, you want to know if a
particular illegal state is reachable from a valid state. This is the
purpose of formal methods.

The part I struggled with while working through the induction step is that any
state that isn’t declared to be invalid might be a starting point for
induction–even if the state is unreachable.

This should help give you an idea, should you try working with
formal methods
yourself, that you need to make certain that unreachable states
are either declared to be invalid or removed from the set of possible states.

Speaking of, that’s our next step: discussing how to declare states to be
invalid when using yosys.

Formal Declarations

yosys
can be made to understand some basic formal statements, drawn from a
subset of the System Verilog formal verification language. This can be
frustrating for a new user of
formal methods with
yosys,
since most of the material on line discusses the full System Verilog formal
description language subset. What yosys
supports is much less than that. Basically,
yosys supports assert(), assume(),
restrict(), and some expressions about transitions. Let’s examine those
formal verification statements here.

The first statement of interest is the assert() statement. At first blush,
this statement works very much like the assert() statement within C/C++.
The value given to the assert() statement must be true, or you your design
isn’t working as desired. assert()s do more than that, though.
assert()s declare states that are invalid within your design.

We’ll come back to that thought in a moment.

The other thing you need to know about assert()s is that within a simulation,
if the assert() is ever not true, the simulation will halt on a failure.
This allows you focus on what caused the problem within your design.

The next basic statement is the assume() statement. This statement is like
the assert(), but with the exception that the theorem prover doesn’t try to
prove that the assume() statement is true. Instead, it forces the assume()
to be true. Any logic path that would cause the assume() to be false
is quietly culled. From the perspective of the state space that will be
examined, the assume() statement removes particular states from the
realm of possibilities.

For example,

initial	last_clk = 1'b0;
always @($global_clock)
	assume(i_clk == !last_clk);

will force the i_clk input to the design to toggle with every
simulation step (that’s the meaning of the $global_clock–it’s true on
every change of the time step). States and state transitions where the
clock doesn’t toggle are just quietly removed from the realm of possibility.

assume() statements have one more feature: if during a simulation the
condition is invalid, the simulation will halt with an error just as it would
if the assert() statement were false.

The restrict() instruction is similar to the assume() instruction.
Like assume(), restrict() also reduces the size of the state space that
the theorem prover needs to work within. In that way, a restrict statement
is much like an assume() statement.
However, unlike the assume() statement, the simulator will ignore any
restrict() statements within your code.

I’ve also found several functions to be very valuable: $past(),
$stable(), $rose(), and $fell(). Since these are important,
let’s work our way through them.

The $past() function has the form of $past(expression, N), for arbitrary
expressions, and positive integers, N. This statement returns the value
of the expression N clocks ago. Hence, $past(expression,1) references what
the expression evaluated to during the last clock. The number of clocks
parameter, N, defaults to one, so $past(expression) is just the same as
$past(expression,1).

System Verilog allows two more arguments to the $past() function for a total
of four. Not so with yosys, however you
may not find these extra arguments necessary either. For example, the fourth
System Verilog argument to the $past() function specifies what clock and
clock edge you are referencing the $past() expression from. Instead,
yosys
only allows expressions of $past() values within a clocked
always block, and so it uses the clock specified in the always statement to
define the clock the $past() function is relative to.

There is one other trick with the $past() function: prior to the first
clock, the $past value is undefined and often assumed to be zero by many
formal theorem solvers. You’ll need to be careful, therefore, not to expect
the $past value to reference any initial value within your logic.

For this reason, I’ve gotten in the habit of creating a signal to tell me if
the past value is valid, such as:

initial	f_past_valid = 1'b0;
always @(posedge i_clk)
	f_past_valid <= 1'b1;

I can then use f_past_valid as part of an expression to determine whether or
not the inputs to a wishbone
slave will not
change once the strobe goes high until the stall line is low. Remember how
we discussed
that with wishbone nothing happens
until (i_wb_stb)&&(!o_wb_stall)? This means that once the
wishbone master
asserts the strobe signal, i_wb_stb, that it is likely to wait for the
o_wb_stall signal to lower before changing the bus request details.
To capture this thought, we’ll assume that once i_wb_stb
goes high, none of the bus request information will change until the
clock after o_wb_stall goes low:

always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_wb_stb))&&($past(o_wb_stall)))
	begin
		assume(i_wb_stb);
		assume(i_wb_we   == $past(i_wb_we));
		assume(i_wb_addr == $past(i_wb_addr));
		assume(i_wb_data == $past(i_wb_data));
		assume(i_wb_sel  == $past(i_wb_sel ));
	end

Alternatively, instead of assuming that the current value was equal to the
last value, we could have instead assumed that these values were $stable()
for the same effect:

always @(posedge i_clk)
	if ((f_past_valid)&&($past(i_wb_stb))&&($past(o_wb_stall)))
	begin
		assume(i_wb_stb);
		assume($stable(i_wb_we));
		assume($stable(i_wb_addr));
		assume($stable(i_wb_data));
		assume($stable(i_wb_sel));
	end

The last of the basic commands you’ll want to know is the $rose() command.
This command returns true or false depending on whether the signal given to
it has risen (positive edge) over the last clock period or not.

This particular function is very useful for telling the theorem prover that
your inputs are only going to change on the positive edge of the clock,

always @($global_clock)
	// If it isn't the positive edge ...
	if (!$rose(i_wb_clk))
	begin
		// Then nothing changes
		assume(i_wb_stb);
		assume($stable(i_wb_we));
		assume($stable(i_wb_addr));
		assume($stable(i_wb_data));
		assume($stable(i_wb_sel));
	end

A similar $fell() primitive exists as well for testing negative clock edges.

yosys provides one more helpful feature.
Anytime you use
yosys
to generate a formal description of your code,
yosys defines the FORMAL flag. Hence, you
can surround your formal properties with ifdefs, as in:

`ifdef	FORMAL
// ...
always @(posedge i_clk)
	assert(!illegal_state);
// ...
`endif

These, therefore, are your basic formal declaration statements:
assert(), assume(), and restrict(). They are helped by the functions
$stable(), $past(), $rose(), $fell(), and perhaps some others that I
haven’t learned yet. (Remember, this is only my first week.) assert()
declares statements to be illegal, and assume() and restrict() are used
to limit the size of the state space.

With these basic principles, let’s look at some formal theorem proving
concepts.

Basic concept

The basic approach to formally describing your program is to assume() that
the inputs will be valid, and then to assert() that the outputs are valid.
You may also wish along the way to assert() particular internal states
are valid as well.

This works until you aggregate up one level, so that you have a higher level
module instantiating a lower level one. In that case, you want to assert()
the values that will be passed to the lower level module rather than
assume()ing them.

A FIFO example

Let’s work our way through a simple example–that of a
FIFO.
In this case, we’ll examine the
FIFO
I just worked with for my SPI-based microphone
ADC core.

As you may remember from our last
FIFO discussion, a
FIFO depends upon two
memory pointers: the write pointer, r_first, and the read pointer, r_last.
The only time r_first and r_last are equal is when the
FIFO is empty.
Likewise, the number of items within the
FIFO is
determined by r_first minus r_last.

There are some other rules associated with these two variables.
The first is that we cannot be allowed to read from the
FIFO
any time it is empty. The second rule is that we cannot
write to the FIFO when it
is full, unless we are also reading from the
FIFO at the same time.
Any attempt to read from an empty
FIFO, or write to a full
FIFO should generate an error.

In order to keep the state transitions from being dependent upon the
number of items in the
FIFO, I pre-compute two values:
will_overflow, which is true if the next write will overflow the
FIFO, and
will_underflow, which will be true if the next read will read from an
empty FIFO.

Further, this particular
FIFO also returns
a status value indicating 1) how many items are in the
FIFO,
2) whether or not the FIFO is non-empty, and 3) whether or not the
FIFO
is past half-full.

All of these details may also be derived from r_first and r_last alone. If
they don’t match, the FIFO
is in an illegal state. Therefore, these properties are a perfect match
for learning
formal methods

The first step is to gate all of our work so that the synthesis tool will
ignore it, unless we are working with the
formal verification methods.

`ifdef	FORMAL
// ... ALl of our formal specifications go here
`endif // This goes at the end of our formal specification

Next, within this FORMAL block we want to make certain that the assumptions
we are going to make regarding our inputs will become asserts when this core
is included into a larger design. We’ll do this by creating an ASSUME macro
that we can use to constrain our inputs.

`ifdef	SMPLFIFO
`define	ASSUME	assume
`else
`define	ASSUME	assert
`endif

Remember that you only want to constrain via ASSUME statements about
parameters that can be set by a higher level module, not external inputs.

Earlier, I described what it would take to assume that the clock toggles.
We’ll repeat that here. We’re also going to insist that this
FIFO
starts in it’s reset state, by insisting that the i_rst line is initially
valid.

initial restrict(i_rst);

always @($global_clock)
begin
	restrict(i_clk == !f_last_clk);
	f_last_clk <= i_clk;

Before leaving this beginning statement, let’s also insist that our
inputs only change on the positive edge of the clock.

	if (!$rose(i_clk))
	begin
		`ASSUME($stable(i_rst));
		`ASSUME($stable(i_wr));
		`ASSUME($stable(i_data));
		`ASSUME($stable(i_rd));
	end
end

We also discussed above the need to know whether the $past() function
would return valid results. We’ll use the f_past_valid register for this
purpose.

initial	f_past_valid = 1'b0;
always @(posedge i_clk)
	f_past_valid <= 1'b1;

This also highlights the fact that your formal verification logic may have
and use registers, just like the rest of your logic–even though you won’t
be using it within your design other than for formal verification.

Next, let’s look at making sure that our helper logic works.

First, the r_fill output should be equal to the number of
FIFO
memory entries that are full. This is given by the difference between
r_first and r_last. Above, we chose to use a clocked register to hold this
value. We did this for timing reasons, but there is the possibility that
we got this wrong. So, let’s check it here. Formally, one might say that
the state where r_fill doesn’t equal this difference is an illegal state.

assign	f_fill = r_first - r_last;
always @(posedge i_clk)
begin
	assert(f_fill == r_fill);

Now, let’s move on to our empty flag. Any time the
FIFO
is empty, we want to set the will_underflow flag. In addition, we want
o_empty_n to be true any time we are not empty. As I mentioned before, the
FIFO
is empty any time r_first is equal to r_last. We can use f_fill from
above for this purpose.

	if (f_fill == 0)
	begin
		assert(will_underflow);
		assert(!o_empty_n);
	end else begin
		assert(!will_underflow);
		assert(o_empty_n);
	end

In a similar value, any time the fill is one less than the number of items
in the buffer, then the buffer is “full”. Let’s make sure we got that logic
right too.

		if (f_fill == {(LGFLEN){1'b1}})
			assert(will_overflow);
		else
			assert(!will_overflow);

The
FIFO
code
also has a value, r_next, which is supposed to
reference the next value to be read. To know if we got this right, let’s add
one to the r_last pointer,

assign	f_next = r_last + 1'b1;

and then look to see if r_next equals this as desired,

	assert(r_next == f_next);
end

Finally, let’s examine the pointers under overflow and underflow conditions.
First, on any reset, both pointers will be set to zero and any output error
will be cleared.

always @(posedge i_clk)
if (f_past_valid)
begin
	if ($past(i_rst))
		assert(!o_err);
	else begin

If we are not in reset, we might have an underflow. Let’s check. If the
FIFO
was empty on the last clock, and if there was a request to read from the
FIFO
on that clock, then we had an underflow. In that case, assert that the
FIFO
read pointer, r_last, has not changed as a result.

		// Underflow detection
		if (($past(i_rd))&&($past(r_fill == 0)))
		begin
			// This core doesn't report underflow errors,
			// but quietly ignores them
			//
			// assert(o_err);
			//
			// On an underflow, we need to be careful not
			// to advance the pointer.
			assert(r_last == $past(r_last));
		end

Had this pointer changed, the
FIFO
might accidentally jump from the empty state to the full state with garbage in
the buffer. We want to avoid this.

We do almost the same thing on an overflow condition, but there are just a
couple differences.
First, in the case of a read and write on the same clock while we are full,
no overflow has taken place. Hence we need to check that a write without
a read has taken place. That’s the first difference. The second difference
is that this core reports overflow conditions, but not underflow conditions.
Hence, we assert that o_err is true on any overflow. Likewise, on any
overflow we also assert that the r_first pointer hasn’t changed.

		//
		// Overflow detection
		if (($past(i_wr))&&(!$past(i_rd))
				&&($past(will_overflow)))
		begin
			// Make sure we report this result
			assert(o_err);

			// Make sure we didn't advance our write
			// pointer on overflow
			assert(r_first == $past(r_first));
		end
	end
end

As with the underflow, a pointer change during an overflow condition can be
catastrophic as well. It could cause the
FIFO
to suddenly become empty, losing any of the data within it. This formal
check about tells the theorem prover that doing so would be illegal, and that
we want to know if anything would create such a condition.

What we haven’t discussed are the
instructions for installing
yosys,
SymbiYosys,
and the various theorem provers. These may be found
on line.
Neither have we discussed the
Makefile
I used to coordinate the proof, nor the yosys
config
that I used. Feel free to examine these on your own if you would like.

What did I find?

You may recall from earlier that I found several errors in my
FIFO as a result of using
these methods. If you are reading this, then you may be wondering just how
significant those errors were. Here are some of the things I found:

• Originally, I had said that a write during an underflow would only
  take you out of the underflow condition if there was no read at the same
  time. This is wrong.

  A write to an empty
  FIFO
  will always succeed, independent of whether or not a read is taking place
  at the same time, and a read from an empty
  FIFO
  should always fail–independent of a write taking place at the same time.

  Fixing this required several changes throughout.

• I hadn’t initialized all of my variables. In particular, r_next and
  r_fill weren’t originally initialized.

• When calculating the number of elements in the
  FIFO,
  I had assumed that if the will_overflow value was true that any write to
  the FIFO would
  overflow the FIFO.
  This isn’t the case. If will_overflow is true, then any write without a
  concurrent read will overflow the
  FIFO.
  A read and write during the same clock period will not overflow the
  FIFO.

If you’d like, all of the changes are captured within the
github repository
on line, so you can review what I found
here.

Final Thoughts

Please keep in mind, I’m only a beginner at
formal methods.
I’ve never used any of them before this week, but I’ve already found several
problems in my own code using them. Are
formal methods
worth the effort? Well, for me and in this example, they were.

I’d like to come back to this topic in the future after I’ve learned some
more. I’d also like to apply these methods to many other problems as well.
However, I’ve also got some problems which I’m not yet certain how to prove.
For example, while I’ve managed to prove a low level QSPI flash
driver,
I have yet to figure out how to prove the entire protocol. Likewise, I’ve
managed to prove that my UART transmitter
(lite) works,
but not yet the receiver or the entire IP
core including the wishbone
interface.

For now, I think I’ll just see if I can’t prove my
WB to AXI4 bridge next.
I think that would be useful for all.