+ Post New Thread
Results 1 to 3 of 3
  1. #1
    Advanced Member level 2
    Points: 3,530, Level: 13

    Join Date
    Feb 2016
    Posts
    680
    Helped
    1 / 1
    Points
    3,530
    Level
    13

    Round-Robin Arbiter Architecture from Efficient microarchitecture for network-on-chip

    I have formally verified a round-robin arbiter code

    Could anyone advise about the various methods of minimizing the combinational delay tcomb penalty mentioned at the end of section 2.3 of Efficient microarchitecture for network-on-chip routers ?


    arbiter.v

    Code Verilog - [expand]
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    17
    18
    19
    20
    21
    22
    23
    24
    25
    26
    27
    28
    29
    30
    31
    32
    33
    34
    35
    36
    37
    38
    39
    40
    41
    42
    43
    44
    45
    46
    47
    48
    49
    50
    51
    52
    53
    54
    55
    56
    57
    58
    59
    60
    61
    62
    63
    64
    65
    66
    67
    68
    69
    70
    71
    72
    73
    74
    75
    76
    77
    78
    79
    80
    81
    82
    83
    84
    85
    86
    87
    88
    89
    90
    91
    92
    93
    94
    95
    96
    97
    98
    99
    100
    101
    102
    103
    104
    105
    106
    107
    108
    109
    110
    111
    112
    113
    114
    115
    116
    117
    118
    119
    120
    121
    122
    123
    124
    125
    126
    127
    128
    129
    130
    131
    132
    133
    134
    135
    136
    137
    138
    139
    140
    141
    
    // Credit : [url]https://www.eevblog.com/forum/fpga/understanding-linear-implementation-of-a-round-robin-arbiter/[/url]
     
    module arbiter #(parameter WIDTH = 4) (clk, reset, req, grant);
     
    input clk, reset;
    input [WIDTH-1:0] req;
    output [WIDTH-1:0] grant; 
     
    // 'grant' is one-hot vector, which means only one client request is granted/given green light to proceed
    // note that 'base' is one-hot vector, 
    // 'base' signal helps round-robin arbiter to decide which 'req' to start servicing
    reg [WIDTH-1:0] base;
     
    always @(posedge clk)
    begin
        if(reset) base <= 1;
     
        else base <= (grant[WIDTH-1]) ? 1 : (grant == 0) ? base : ( grant << 1 );
    end
     
    wire [WIDTH-1:0] priority_in;
    wire [(WIDTH << 1)-1:0] priority_out; // the two leftmost significant bit are left unused
     
    wire [WIDTH-1:0] granting = req & priority_in;
    wire [WIDTH-2:0] approval; // we only have (WIDTH-1) block F
     
    genvar index;
    generate
        for(index = 0; index < WIDTH; index = index + 1)
        begin
            if(index == WIDTH-1) assign grant[index] = (reset) ? 0 : granting[index];
     
            else assign grant[index] = (reset) ? 0 : ( granting[index] | approval[index] );
     
     
            if(index < (WIDTH-1)) assign approval[index] = priority_out[index+WIDTH-1] & req[index];
     
            if(index > 0) assign priority_in[index] = base[index] | priority_out[index-1];
     
            else assign priority_in[index] = base[index];
        end
    endgenerate
     
     
    genvar priority_index;
    generate
        for(priority_index = 0; priority_index < (WIDTH << 1); priority_index = priority_index + 1)
        begin : out_priority    
     
            if(priority_index < (WIDTH))
                assign priority_out[priority_index] = (~req[priority_index]) & priority_in[priority_index];
     
            else assign priority_out[priority_index] = (~req[priority_index-WIDTH]) & priority_out[priority_index-1];
        end
    endgenerate
     
     
    `ifdef FORMAL
     
    initial assume(reset);
    initial assume(req == 0);  // only enable this assume() to test the cover() at line 100 properly
     
    genvar grant_num;
     
    generate 
        for(grant_num = 0; grant_num < WIDTH; grant_num = grant_num + 1)
            
            always @(*) cover(first_clock_had_passed && grant[grant_num]);  // covers grants to each of the clients' request
     
    endgenerate
     
     
    reg [WIDTH-1:0] req_previous;
    always @(posedge clk) req_previous <= req;
     
    always @(posedge clk) cover(!$past(reset) && (grant == 0)); // covers the ability to go to an idle state
     
    // covers the ability to handle requests properly even with ALL requests ON
    always @(posedge clk) cover((&$past(req_previous)) && (&$past(req)) && (&req) && first_clock_had_passed && $past(first_clock_had_passed) && ((grant & $past(req)) == grant)); 
     
     
    reg [WIDTH-1:0] grant_previous;
    always @(posedge clk) grant_previous <= grant;
     
    always @(posedge clk) cover(grant != grant_previous); // covers the ability to switch grants to any other requests
     
    always @(posedge clk) cover(first_clock_had_passed && $past(first_clock_had_passed) && (&req) && (req_previous == 4'b1100) && ($past(req_previous) == 4'b1011)); // covers round-robin ability
    `endif
     
    `ifdef FORMAL
     
    reg first_clock_had_passed;
    initial first_clock_had_passed = 0;
     
    always @(posedge clk) first_clock_had_passed <= 1;
     
    // [url]https://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2[/url]
    wire multiple_requests = (req != 0) && !((req & (req - 1)) == 0);
    wire grant_is_one_hot = (grant != 0) && ((grant & (grant - 1)) == 0);
     
    always @(*)
    begin
        if(reset) assert(grant == 0);
     
        else begin
     
            if (|req) assert(grant_is_one_hot);
     
            else assert(grant == 0);
     
     
            // assertions for round-robin capability
     
            if((req == req_previous) && multiple_requests) 
            // it is possible that the same client files request again after being serviced
                assert((grant & req) != grant_previous); 
        end
    end
     
    always @(posedge clk)
    begin
        if(first_clock_had_passed)
        begin
            // starts round-robin arbiter with req #0 getting prioritized first
            if($past(reset)) assert(base == 1);
     
            // 'grant' is a one-hot signal, but 'req' is not a one-hot signal
            // 'base' is a one-hot signal which rotates
            //  after the corresponding 'req' had been granted/given permission to proceed)
            //  Rotation wraps around upon reaching MSB
     
            else begin
                assert(base == $past(grant[WIDTH-1]) ? 1 : ($past(grant) == 0) ? $past(base) : ($past(grant) << 1) );
                assert(base != 0);
            end
        end
    end
     
    `endif
     
    endmodule


    arbiter.sby

    Code:
    [tasks]
    proof
    cover
    
    [options]
    proof: mode prove
    proof: depth 10
    
    cover: mode cover
    cover: depth 20
    cover: append 8
    
    [engines]
    smtbmc yices
    # smtbmc boolector
    # abc pdr
    # aiger avy
    # aiger suprove
    
    [script]
    read_verilog -formal -sv arbiter.v
    prep -top arbiter
    
    [files]
    arbiter.v

    •   AltAdvertisement

        
       

  2. #2
    Super Moderator
    Points: 31,824, Level: 43
    ads-ee's Avatar
    Join Date
    Sep 2013
    Location
    USA
    Posts
    7,366
    Helped
    1727 / 1727
    Points
    31,824
    Level
    43

    Re: Round-Robin Arbiter Architecture from Efficient microarchitecture for network-on-

    They author is discussing using parallel pre-fix sum type networks to compute the priority. See this wiki page.


    1 members found this post helpful.

    •   AltAdvertisement

        
       

  3. #3
    Advanced Member level 2
    Points: 3,530, Level: 13

    Join Date
    Feb 2016
    Posts
    680
    Helped
    1 / 1
    Points
    3,530
    Level
    13

    Re: Round-Robin Arbiter Architecture from Efficient microarchitecture for network-on-

    in practice, the associated delay penalty can be minimized by computing the intermediate grant signals for the block of R -type cells and the block of F -type cells in parallel and conditionally selecting either set of grants based on the value of the first block’s final priority output.

    As in the case of fixed-priority arbitration, we can further improve delay by replacing the blocks of R-type and F-type cells with prefix networks.
    Thanks for the wikipedia link. However, I am in the dark on how prefix sum could actually replace blocks F and R ?








--[[ ]]--