# On Benefits of Modeling the HPDcache in LNT

Zachary Assoumani, César Fuguet, Radu Mateescu, Wendelin Serwe

► To cite this version:

Zachary Assoumani, César Fuguet, Radu Mateescu, Wendelin Serwe. On Benefits of Modeling the HPDcache in LNT. RISC-V 2025 -RISC-V Summit Europe, May 2025, Paris, France. pp.1-1, 2025. hal-05106202

HAL Id: hal-05106202

https://inria.hal.science/hal-05106202v1

Submitted on 10 Jun 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# On Benefits of Modeling the HPDcache in LNT

Zachary Assoumani — César Fuguet — Radu Mateescu — Wendelin Serwe

Inria Center at Université Grenoble Alpes

## LNT MODEL

<figure><img src="image_2.png" /></figure>

https://github.com/openhwgroup/cv-hpdcache/

<figure><img src="image_3.png" /></figure>

$$1 \text{ component} = \frac{1 \text{ LNT process}}{1 \text{ LNT process}}$$

<figure><img src="image_4.png" /></figure>

```c
int rtab_find_ready(int last) {
    int i = (last + 1) % RTAB_NENTRIES;
    for (;;) {
        if (rtab[i].valid && rtab[i].ll_head &&
            (rtab[i].deps == 0))
            return i;
        if (i == last)
            return -1;
        i := (i + 1) % RTAB_NENTRIES;
    }
}
```

pseudocode function...
...to LNT function

```c
function rtab_find_ready(rtab:RTAB_Array, last:int): int is
    var i:int in i := (last + 1) mod RTAB_NENTRIES;
    loop
        if rtab[Nat (i)].valid and rtab[Nat (i)].ll_head and
           (rtab[Nat (i)].deps == NoDeps) then
            return i
        elsif i == last then
            return -1
        end if;
        i := (i + 1) mod RTAB_NENTRIES
    end loop
end var end function
```

<figure><img src="image_5.png" /></figure>

ETAPS Test-of-Time Tool
Award Winner in 2023

## BENEFITS: FORMAL ANALYSIS WITH CADP

### Model checking (EVALUATOR)

Temporal logic formula: RVWMO safety property

```c
[ true*.
  {REQ ?any ?any ?s:nat ?t1:nat ?a:string}.
  not ({RSP_W ?any !s !t1} or {RSP_R ?any !s !t1})*.
  {REQ ?any ?any !s ?t2:nat !a where t1 <> t2}.
  not ({RSP_W ?any !s !t1} or {RSP_R ?any !s !t1})*.
  {RSP_W ?any !s !t2} or {RSP_R ?any !s !t2}
] false
```

Counterexample trace

```
<initial state>
...
"CRI_REQ !STORE !D2 !1 !1 !A2"
"CRI_RSP_W !D2 !1 !1"
"CMI_REQ_W !A2 !D2"
"CRI_REQ !STORE !D2 !1 !2 !A1"
"CRI_RSP_W !D2 !1 !2"
"CRI_REQ !STORE !D2 !1 !3 !A1"
"CRI_REQ !STORE !D2 !1 !4 !A1"
"CMI_RSP_W !A2 !D2"
"CMI_REQ_W !A1 !D2«
"RTAB_REQ !STORE !D2 !1 !3 !A1"
"CMI_RSP_W !A1 !D2"
"RTAB_REQ !STORE !D2 !1 !4 !A1"
"CRI_RSP_W !D2 !1 !4"
<goal state>
```

<figure><img src="image_6.png" /></figure>

### Interactive step-by-step simulation (OCIS)

<figure><img src="image_7.png" /></figure>

<figure><img src="image_8.png" /></figure>

<figure><img src="image_9.png" /></figure>

<figure><img src="image_10.png" /></figure>

<figure><img src="image_11.png" /></figure>

PROGRAMME
DE RECHERCHE
CLOUD

<figure><img src="image_12.png" /></figure>

UGA
Université
Grenoble Alpes