FPGA Design & Verification of Fixed Priority Arbiter

Introduction

Arbiters are devices that arbitrate between multiple requesters and issue a single grant, based on a specified arbitration scheme. Common schemes include Fixed Priority and Round Robin. In a Fixed Priority arbiter, the requests are granted based on a fixed priority scheme. This Fixed Priority Arbiter is purely combinational, that is, there are no flops in between the inputs and outputs. The Fixed Priority Arbiter can be used to service multiple interrupts to a processor based on a fixed priority scheme.

Inspiration

I was inspired by Day 14 of QuickSilicon's 21 days of RTL challenge, to implement a Fixed Priority Combinational Arbiter https://quicksilicon.in/course/21daysofrtl/module/day-14

Mr. Rahul Behl, the instructor left a comment on the QuickSilicon platform that really struck me: "The testcase will show PASSED as long as the RTL and testbench compile, but it doesn't imply that the implemented logic is correct."

Initial design: Arbiter with break

I decided to take up the challenge and started coding. I came up with this design:

module arbiter #(
  parameter NUM_PORTS = 4
)(
    input       wire[NUM_PORTS-1:0] req_i,
    output      wire[NUM_PORTS-1:0] gnt_o   // One-hot grant signal
);
  logic [NUM_PORTS-1:0]gnt;
  always_comb begin
    gnt = 0;
    for (int i = 0; i < NUM_PORTS; i++)
       priority if (req_i[i]) begin
         gnt[i] = 1'b1;
         break;
       end else begin
         gnt[i] = 1'b0;
       end
  end    
  assign gnt_o = gnt;

endmodule

QuickSilicon's results

This RTL design does not compile on QuickSilicon's platform.

Simulation with Verilator on EDA Playground

I wondered if it would compile with Verilator. It did! You can run it in inside your web browser here: https://www.edaplayground.com/x/SN4u

Testbench compiles and the test passes!

Synthesis on FPGA board using Vivado

Time for Lint, Synthesis and Implementation on my Nexys A7 FPGA Board using Vivado.

+-------------------------+------+-------+------------+-----------+-------+
|        Site Type        | Used | Fixed | Prohibited | Available | Util% |
+-------------------------+------+-------+------------+-----------+-------+
| Slice LUTs*             |    2 |     0 |          0 |     63400 | <0.01 |
|   LUT as Logic          |    2 |     0 |          0 |     63400 | <0.01 |
|   LUT as Memory         |    0 |     0 |          0 |     19000 |  0.00 |
| Slice Registers         |    0 |     0 |          0 |    126800 |  0.00 |
|   Register as Flip Flop |    0 |     0 |          0 |    126800 |  0.00 |
|   Register as Latch     |    0 |     0 |          0 |    126800 |  0.00 |
| F7 Muxes                |    0 |     0 |          0 |     31700 |  0.00 |
| F8 Muxes                |    0 |     0 |          0 |     15850 |  0.00 |
| Unique Control Sets     |    0 |       |          0 |     15850 |  0.00 |
+-------------------------+------+-------+------------+-----------+-------+

2 Slice LUTs got inferred with this code. Not bad.

Video demo on FPGA Board

I programmed my FPGA board and voila! It works! Atleast, it seems to. Because I can only test for a few inputs, I don't know if it works for all combinations.

Model checking

Model checking can help here. The code did not compile as is by the HW-CBMC tool.

It's because the break statement is not supported for synthesis by the HW-CBMC tool. Hmmm...if only I could replace the break statement with some alternate syntax....

I searched online and luckily, someone else has asked the same question on the Electrical Engineering Stack Exchange. frank_010 if you are reading this, thank you!

Dave Rich's answer really helped me:

One can easily re-write this without a break statement, a synthesis tool can too.

Modified Design: Arbiter breakout

I added a breakout bit to break out of the loop instead of the break statement.

bit breakout;
  always_comb begin
    gnt = 0;
    breakout = 0;
    for (int i = 0; i < NUM_PORTS; i++)
      if (!breakout) 
        priority if (req_i[i]) begin
	  gnt[i] = 1'b1;
          breakout = 1;
        end    
  end

Formal Proof of Arbiter breakout

It is now getting compiled by CBMC, and the tool could find no counterexample.

Properties and Symbolic Variable Approach:

I used a symbolic variable approach for the formal proof. Symbolic variables are abstract variables that we constrain meaningfully. The tool is allowed to search for a counterexample that satisfies the constraints. The constraints are simply to ensure that the request is within the boundary of the request array; the tool is free to find a counterexample for any valid index of the request array. If no counterexample is found, the tool proves that the properties hold for all valid indices.

1. Highest possible priority request should always be granted. req[0] has highest priority, so it should always be granted.

2. Safety property: PRIORITY_CHECK_1 ensures that a higher priority request isn't left ungranted when a lower priority request is granted.

3. Liveness property: PRIORITY_CHECK_2 ensures that a higher priority request is always granted over a lower priority request.

4. No spurious grants: At all times, there should be no grant without its corresponding request being raised.

5. One and only one grant for a non-zero request: Arbiters always grant only one request at a time.

6. Cover properties: A few cover properties to cover interesting cases like no request, all requests, highest priority request and lowest priority request, to ensure we haven't overcontrained our formal environment.

// Declare 2 symbolic variables
  int m, n;  

  VALID_REQ_1: assume property ((m >= 0) && (m < NUM) && $stable(m));

  VALID_REQ_2: assume property ((n >= 0) && (n < NUM) && $stable(n)); 

  // Highest priority request is always granted
  HIGHEST_PRIORITY_REQ: assert property (req_i[0] |-> gnt_o[0]); 
 
  // PRIORITY_CHECK_1: If a request is granted, there should be no request of a higher priority active.
  // This check is only concerned with the higher priority requests and it is
  // a safety check. 
  PRIORITY_CHECK_1: assert property ((m > 0) && (m > n) && req_i[m] && gnt_o[m] |-> (req_i[n] == 0));
     
  // PRIORITY_CHECK_2: If there are 2 requests, then the one with higher                 priority needs to be granted.
  // This check is concerned with lower priority requests and it is a liveness
  // check.
  PRIORITY_CHECK_2: assert property ((m < n) && req_i[m] && req_i[n] && ($countones(req_i) == 2) |-> gnt_o[m]);

  // No grant without its request
  assert property (gnt_o[m] |-> req_i[m]);

  // Not more than 1 grant for any non-zero number of requests        
  ONE_HOT_ARBITER: assert property (req_i |-> $onehot(gnt_o));

  // Cover highest priority request
  cover property (req_i[0]);

  // Cover lowest priority request
  cover property (req_i[NUM-1]);

  // Cover all requests high
  cover property ($countones(req_i) == NUM);

  // Cover all requests low
  cover property ($countones(req_i) == 0);

SystemVerilog Assertions Source code

Respin on FPGA

Lint is clean, synthesis done, implementation done, generating bitstream...

Wait a minute! This schematic is something different. It definitely is much more easier on the eyes! Fewer gates, an engineer's dream!

+-------------------------+------+-------+------------+-----------+-------+
|        Site Type        | Used | Fixed | Prohibited | Available | Util% |
+-------------------------+------+-------+------------+-----------+-------+
| Slice LUTs              |    0 |     0 |          0 |     63400 |  0.00 |
|   LUT as Logic          |    0 |     0 |          0 |     63400 |  0.00 |
|   LUT as Memory         |    0 |     0 |          0 |     19000 |  0.00 |
| Slice Registers         |    0 |     0 |          0 |    126800 |  0.00 |
|   Register as Flip Flop |    0 |     0 |          0 |    126800 |  0.00 |
|   Register as Latch     |    0 |     0 |          0 |    126800 |  0.00 |
| F7 Muxes                |    0 |     0 |          0 |     31700 |  0.00 |
| F8 Muxes                |    0 |     0 |          0 |     15850 |  0.00 |
| Unique Control Sets     |    0 |       |          0 |     15850 |  0.00 |
+-------------------------+------+-------+------------+-----------+-------+

Whoa! Zero utilization! Too good to be true!

I programmed my FPGA board again and only the first LED glowed, no matter which switch I toggled. At this point, I don't really know what's going on. It could be an issue with the Vivado synthesis tool.

A closer look at the Vivado synthesized schematic reveals that the req is not connected to the grant and the inputs of the grant are constant, with the zeroeth input tied to 1 and the others tied to zero. That's why there are no LUTs inferred!

Synthesizing Arbiter Breakout in Yosys

Undeterred, I decided to try out a different synthesis tool. Yosys, being free and open-source, fit the bill. The syntax wasn't supported by the default frontend, so I switched to the Yosys-Slang frontend, and it worked!

plugin -i slang
read_slang arbiter_breakout.sv --top arbiter_breakout
hierarchy -check -top arbiter_breakout
proc
clean
opt_expr
clean
show

Synthesizing Arbiter with break in Yosys

Let's see how the arbiter with the break statement synthesizes in Yosys:

read_slang arbiter.sv --top arbiter
hierarchy -check -top arbiter
proc
clean
opt_expr
clean
show

Formal Equivalence Check between the 2 arbiters

The schematics are not the same, but are they equivalent? Let's set up a formal equivalence check between the 2 arbiters:

read_slang arbiter.sv --top arbiter
read_slang arbiter_breakout.sv --top arbiter_breakout
miter -equiv -make_assert -make_outputs arbiter arbiter_breakout miter
flatten miter
sat -verify -prove-asserts -show-inputs -show-outputs miter

Results:

The Formal equivalence check between 2 arbiters holds true in Yosys.

Simulation of Arbiter Breakout with Verilator on EDA Playground

I simulated it with the same testbench and it passes again.

Try it out here.

The formal equivalence check and simulation of both arbiters show identical behaviour.

Logic Utilization of Arbiter Break vs Arbiter Breakout in Yosys

Arbiter breakout:

=== arbiter_breakout ===

   Number of wires:                 12
   Number of wire bits:             24
   Number of public wires:           7
   Number of public wire bits:      16
   Number of memories:               0
   Number of memory bits:            0
   Number of processes:              0
   Number of cells:                 15
     $lut                            3
     IBUF_VPR                        4
     OBUFT_VPR                       4
     T_INV                           4

Arbiter break:

=== arbiter ===

   Number of wires:                  8
   Number of wire bits:             20
   Number of public wires:           3
   Number of public wire bits:      12
   Number of memories:               0
   Number of memory bits:            0
   Number of processes:              0
   Number of cells:                 15
     $lut                            3
     IBUF_VPR                        4
     OBUFT_VPR                       4
     T_INV                           4

They have the same LUT and cell utilization in Yosys!

Loading design on FPGA using OpenFPGALoader

I used F4PGA to generate the bitstream. Since F4PGA does not support the Slang plugin out of the box, I used a separate installation of Yosys from Git with Slang installed to parse the file and then wrote to a Verilog file using write_verilog command. This Verilog file was then used in the F4PGA makefile.

openFPGALoader -c digilent fixed_priority_combination_arbiter/build/nexys4ddr/arbiter_breakout.bit 
openFPGALoader -c digilent fixed_priority_combination_arbiter/build/nexys4ddr/arbiter.bit

Not surprisingly, both designs have the same behaviour when flashed on the FPGA Board.

Mutation Coverage with Yosys

I found an issue with

gnt = 0;

when running MCY, since EBMC model checking tool models uninitialized signal as zero. This was causing an "equivalence gap" - where the Formal Property check would fail while the Equivalence check would pass. This is because the synthesis tool can optimize the undefined behaviour as Don't Cares, which can cause unintended behaviour. For a Don't Care, it doesn't matter if it gets mutated to a constant zero or a constant one, the result would be the same for the equivalence checker.

I decided it would be better to replace this with

gnt = '0;

to explicitly force all bits to zero unless a request is there.

I also added an additional check for unknown values on the grant signal.

With this change, the Equivalence Gap issue got fixed. There were Uncovered mutations. By analysing the design mutation, I concluded the tool is not checking properties for all values, instead it is checking only for the highest value. This can also be seen in the screenshot of the proof.

To confirm, I tried replacing the property by enumerating the possible values, like this:

NO_GRANT_WITHOUT_REQUEST_3: assert property (gnt_o[3] |-> req_i[3]);

  NO_GRANT_WITHOUT_REQUEST_2: assert property (gnt_o[2] |-> req_i[2]);

  NO_GRANT_WITHOUT_REQUEST_1: assert property (gnt_o[1] |-> req_i[1]);
  
  NO_GRANT_WITHOUT_REQUEST_0: assert property (gnt_o[0] |-> req_i[0]);

And then the coverage is 100%

It seems to be an issue with HW-CBMC, hence filed it on GitHub: https://github.com/diffblue/hw-cbmc/issues/1689

Conclusion

• This project highlights the use of free and open source tools that can succeed even when proprietary tools fail.
• Vivado has an issue with synthesis
• The benefits of using formal equivalence checking.
• Always verify the output of your tool.
• Mutation Coverage with Yosys is a very useful technique and complimentary to Formal Verification.