WB2AXIP

https://github.com/zipcpu/wb2axip
Admin
WB2AXIP is a library of formally verified, full-throughput bus interconnects, bridges, and...
Tokens:47,973
Snippets:401
Trust Score:9
Update:1 day ago
Show doc for...
Tokens:
Raw
### Response delay counting with maximum limit

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/demo2019.pdf

Counts cycles with outstanding requests and no acknowledgment, asserting the delay stays below MAX_ACK_DELAY. Ensures all requests get responses.

```systemverilog
always @ (posedge i_clk)
    if (i_reset || outstanding == 0 || ack)
        ack_delay <= 0;
    else // if (outstanding > 0)
        ack_delay <= ack_delay + 1;

always @ (*)
    assert (ack_delay < MAX_ACK_DELAY);
```

--------------------------------

### Basic Counter Verilog Module

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/demo2019.pdf

Defines a 16-bit counter with a parameter START_COUNT set to 16'h3ff. The counter decrements on each clock edge and asserts that it never exceeds the start count. Used as the design under test for formal verification.

```verilog
parameter [15:0] START_COUNT = 16'h3ff;
reg [15:0] counter;
initial counter = START_COUNT;
always @ (posedge i_clk)
    counter <= counter - 1;
assert property (@ (posedge i_clk)
    counter <= START_COUNT);
```

--------------------------------

### Initial value criteria example: f_past_valid and reset assumptions

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/orconf2019.pdf

Shows a common pattern for handling initial values in formal verification, where f_past_valid is initialized to 0 and set on the first clock edge. The code assumes !S_AXI_ARVALID and asserts !S_AXI_RVALID on the first clock tick, addressing cores that require multiple clocks to reset, such as Xilinx AXI implementations needing 16 clocks.

```verilog
always @ (*)
    if ( !f_past_valid ) begin // i.e. if first clock tick
        assume ( !S_AXI_ARVALID );
        //... assert ( !S_AXI_RVALID );
    end

initial f_past_valid = 0;
always @ (posedge S_AXI_ACLK )
    f_past_valid <= 1;
```

--------------------------------

### Stall counting with maximum limit

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/demo2019.pdf

Counts consecutive stalls and asserts the count stays below MAX_STALL_COUNT. Ensures all responses get accepted within a bounded number of stalls.

```systemverilog
always @ (posedge i_clk)
    if (i_reset || !request || !stall)
        stall_count <= 0;
    else // if (request && stall)
        stall_count <= stall_count + 1;

always @ (*)
    assert (stall_count < MAX_STALL_COUNT);
```

--------------------------------

### No Lockups: ack delay bounded (assert property)

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/busprops.pdf

Asserts that when there is an outstanding request and no acknowledgment is currently being given, the acknowledgment delay counter f_ack_delay remains below MAXIMUM_DELAY on the next clock edge. Ensures requests eventually get a response.

```systemverilog
assert property (@(posedge i_clk) (f_outstanding > 0)&&(!o_ack) |=> (f_ack_delay < MAXIMUM_DELAY));
```

--------------------------------

### AXI Master Logic Form #2

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/chexpo-2021.pdf

Alternative AXI master logic: on reset, clear VALID and DATA; when VALID and READY, move to next beat or end transaction; when not VALID, consider starting a transaction.

```verilog
if (!ARESETN) begin
    VALID <= 0;
    (DATA <= defaults;)
end else if (VALID && READY) // Move on to next beat
    // or end the transaction
end else if (!VALID) // Consider starting a transaction
```

--------------------------------

### SymbiYosys Configuration File for Counter

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/demo2019.pdf

Configuration file for SymbiYosys to run a bounded model check (mode prove) on the counter design. It reads the Verilog file, prepares the top module, and uses the smtbmc engine.

```sby
[tasks]
prf

[options]
prf: mode prove

[engines smtbmc]

[script]
read -formal counter.v
prep -top counter

[files]
counter.v
```

--------------------------------

### Assertion for reset behavior

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/demo2019.pdf

Formal property checking that on reset, the counter equals START_COUNT at the next clock edge.

```SystemVerilog
assert property (@ (posedge i_clk) i_reset |=> (counter == START_COUNT) );
```

--------------------------------

### TinyTPU state machine case (Verilog)

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/chexpo-2021.pdf

Verilog case statement from TinyTPU that selects state based on AWVALID and ARVALID. It handles write and read address states, but the design is broken and few simulation environments could trigger the bug.

```verilog
if (!ARESETN) begin
  //...
end else case (state)
  IDLE : //...
  case ({AWVALID, ARVALID})
    2'b10 : state <= WRITE_ADDRESS;
    2'b01 : state <= READ_ADDRESS;
    default :
  endcase
endcase
```

--------------------------------

### Reset: assume master signals and assert slave outputs

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/busprops.pdf

After reset, the master must deassert ARVALID and the slave must deassert RVALID. The first property assumes the master behavior, the second asserts the slave output.

```systemverilog
// The s l a v eassume m a s t e r s i g n a l s assume p r o p e r t y (@ (posedge i_clk) !S_AXI_ARESETN |= >!S_AXI_ARVALID);
```

```systemverilog
// A s s e r t s i t sown o u t p u t s a s s e r t p r o p e r t y (@ (posedge i_clk) !S_AXI_ARESETN |= >!S_AXI_RVALID);
```

--------------------------------

### Reset: no request after reset (assume property)

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/busprops.pdf

Assumes that after a reset, i_request is not asserted on the next clock edge. This constrains the environment to not issue requests during reset.

```systemverilog
assume property (@(posedge i_clk) i_reset |=> !i_request);
```

--------------------------------

### Assert property for stalled channel

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/demo2019.pdf

Formal property: when request and stall are high, data must remain stable. Used to verify that a stalled channel does not change its output.

```systemverilog
assert property (@(posedge i_clk)
    request && stall |=> request && $stable(data) );
```

--------------------------------

### Counter reset logic with always block

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/demo2019.pdf

Adds a reset condition to the counter logic. On reset, the counter is set to START_COUNT; otherwise, it decrements when counter > 0.

```Verilog
always @ (posedge i_clk)
    if (i_reset)
        counter <= START_COUNT;
    else if (counter > 0)
        counter <= counter - 1;
```

--------------------------------

### Vivado AXI Stream Template (tlast_delay)

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/chexpo-2021.pdf

This logic from Vivado's AXI stream template didn't work. It delays tlast by one clock cycle, but the formal trace showed TLAST violating handshaking rules, causing the last beat to be ignored.

```verilog
assign tlast = (read_ptr == NWORDS - 1);

always @(posedge ACLK)
    if (!ARESETN)
        tlast_delay <= 0;
    else
        tlast_delay <= tlast;
```

--------------------------------

### No Lockups: bound response delay

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/busprops.pdf

Asserts that when there is an outstanding request and RVALID is low, the acknowledgment delay (f_ack_delay) must stay below MAXIMUM_DELAY, preventing lockups.

```systemverilog
a s s e r t p r o p e r t y (@ (posedge i_clk) (f_outstanding > 0)&&(! S_AXI_RVALID) |´ > (f_ack_delay < MAXIMUM_DELAY) );
```

--------------------------------

### Reset: no ack after reset (assert property)

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/busprops.pdf

Asserts that after a reset, o_ack is not asserted on the next clock edge. Used to verify the bus clears all acknowledgments following a reset.

```systemverilog
assert property (@(posedge i_clk) i_reset |=> !o_ack);
```

--------------------------------

### Stalls: assume and assert stable signals during stall

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/busprops.pdf

When the bus is stalled (ARVALID without ARREADY, or RVALID without RREADY), the request must not change. The first property assumes the master keeps ARVALID and ARADDR stable; the second asserts the slave keeps RVALID and RDATA stable.

```systemverilog
assume p r o p e r t y (@ (posedge i_clk) (S_AXI_ARESETN) && S_AXI_ARVALID &&!S_AXI_ARREADY |= > S_AXI_ARVALID && $ s t a b l e (S_AXI_ARADDR) );
```

```systemverilog
a s s e r t p r o p e r t y (@ (posedge i_clk) (S_AXI_ARESETN) && S_AXI_RVALID &&!S_AXI_RREADY |= > S_AXI_RVALID && $ s t a b l e (S_AXI_RDATA) );
```

--------------------------------

### AXI Handshaking Properties

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/chexpo-2021.pdf

Formal properties for AXI handshaking: reset clears requests and stalled channels must not change data. The first property asserts VALID is low after reset; the second asserts that when VALID is high and READY is low, VALID remains high and DATA is stable.

```systemverilog
assert property (@(posedge ACLK) !ARESETN |=> !VALID);
```

```systemverilog
assert property (@(posedge ACLK) disable iff (!ARESETN) VALID && !READY |=> VALID && $stable(DATA));
```

--------------------------------

### Reset: outstanding count cleared after reset (assert property)

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/busprops.pdf

Asserts that after a reset, the outstanding request counter f_outstanding is zero on the next clock edge. Verifies that all pending transactions are cleared.

```systemverilog
assert property (@(posedge i_clk) i_reset |=> (f_outstanding == 0));
```

--------------------------------

### Extra Acks: no RVALID without outstanding request

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/busprops.pdf

Asserts that the slave does not assert RVALID when there is no outstanding request (f_outstanding == 0).

```systemverilog
a s s e r t p r o p e r t y (@ (posedge i_clk) (f_outstanding == 0 ) |´ >!S_AXI_RVALID);
```

--------------------------------

### AXI_READ_OUTPUT_P process (VHDL)

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/chexpo-2021.pdf

VHDL process from Xilinx Ethernet-Lite IP after a fix. It resets S_AXI_RDATA to zeros on active reset and updates it when S_AXI_RREADY is high. Beware that the first read result might be invalid.

```vhdl
AXI_READ_OUTPUT_P : process (S_AXI_ACLK) is
begin
  if (S_AXI_ACLK'event and S_AXI_ACLK = '1') then
    if (S_AXI_ARESETN = RST_ACTIVE) then
      S_AXI_RDATA <= (others => '0');
    elsif S_AXI_RREADY = '1' then
      S_AXI_RDATA <= IP2Bus_Data;
    end if;
  end if;
end process AXI_READ_OUTPUT_P;
```

--------------------------------

### Extra Acks: no ack without outstanding request (assert property)

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/busprops.pdf

Asserts that when the outstanding request counter is zero, o_ack is not asserted on the next clock edge. Prevents acknowledgments without a prior request.

```systemverilog
assert property (@(posedge i_clk) (f_outstanding == 0) |=> !o_ack);
```

--------------------------------

### AXI_READ_VALID_P process (VHDL)

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/chexpo-2021.pdf

VHDL process from Xilinx Ethernet-Lite IP that handles AXI read valid signal. It resets S_AXI_RVALID on active reset and updates it when S_AXI_RREADY is high. The formal tool held S_AXI_RREADY low long enough to trigger a bug.

```vhdl
AXI_READ_VALID_P : process (S_AXI_ACLK) is
begin
  if (S_AXI_ACLK'event and S_AXI_ACLK = '1') then
    if (S_AXI_ARESETN = RST_ACTIVE) then
      S_AXI_RVALID <= '0';
    elsif S_AXI_RREADY = '1' then
      S_AXI_RVALID <= rvalid;
    end if;
  end if;
end process AXI_READ_VALID_P;
```

--------------------------------

### Stalls: request stable during stall (assert property)

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/busprops.pdf

Asserts that when a request is active and the bus is stalled (and not in reset), the request and its details remain stable on the next clock edge. Ensures the request does not change while stalled.

```systemverilog
assert property (@(posedge i_clk) i_request && o_stall && (!i_reset) |=> i_request && $stable(request_details));
```

--------------------------------

### AXI Master Logic Form #1

Source: https://github.com/zipcpu/wb2axip/blob/master/doc/chexpo-2021.pdf

A common structure for AXI master logic: on reset, clear VALID and DATA; when not VALID or READY, allow changes; when valid_will_be_zero, data can be reset.

```verilog
if (!ARESETN) begin
    VALID <= 0;
    (DATA <= defaults;)
end else if (!VALID || READY) // VALID and data can change
    if (valid_will_be_zero) // Data can be reset
```
Tokens:
Raw