RISCV: herd vs. operational models






Models, test set, and logs

The herd model consists in two cat files: riscv-defs.cat and riscv.cat. We also provide an, equivalent, total order version of model total.cat, which follows the ISA document better. The cat.tar archive gathers the above mentioned cat models.

Our test base consists in 7251 tests.

We have 7251 results out of those 7251 tests in the log Herd.

We have 7251 results out of 7251 tests in the log Op.

Reference tests

This table lists “reference” test inspired from the documentation. Column “Kind” is the intended result, “Herd” and “Op” are the current results of the herd and operational models. Beware: work in progress.

There are 49 such tests
 KindHerdOp
ISA01RequireRequireRequire
ISA02AllowAllowAllow
ISA03+SB01ForbidForbidForbid
ISA03+SB02AllowAllowAllow
ISA03+SIMPLERequireRequireRequire
ISA03+SIMPLE+BISAllowAllowAllow
ISA-Rel-AcqAllowForbidForbid
ISA-DEP-ADDRForbidForbidForbid
ISA-DEP-CTRLForbidForbidForbid
ISA-DEP-SUCCESSForbidAllowAllow
ISA-DEP-SUCCESS-SUCCESSForbidAllowAllow
ISA-MP-DEP-SUCCESSForbidAllowAllow
ISA-MP-DEP-SUCCESS-SWAPForbidAllowAllow
ISA-MP-DEP-SUCCESS-SWAP-SIMPLEForbidAllowAllow
ISA-MP-DEP-SUCCESS-SUCCESSForbidAllowAllow
ISA-MP-DEP-ADDR-LR-SUCCESSForbidForbidForbid
ISA-MP-DEP-ADDR-LR-FAILAllowAllowAllow
ISA-LB-DEP-ADDR-SUCCESSForbidForbidForbid
ISA-LB-DEP-ADDR2-SUCCESSAllowAllowAllow
ISA-LB-DEP-ADDR3-SUCCESSForbidForbidForbid
ISA-S-DEP-ADDR-SUCCESSForbidForbidForbid
ISA-LB-DEP-DATA-SUCCESSForbidAllowAllow
ISA-S-DEP-DATA-SUCCESSForbidAllowAllow
ISA-2+2W-SUCCESSAllowForbidForbid
ISA-MP-DEP-WW-SUCCESSAllowForbidForbid
ISA09AllowAllowAllow
ISA09+BISAllowAllowAllow
ISA10AllowAllowAllow
ISA10+BISForbidForbidForbid
ISA10+TERAllowAllowAllow
ISA11AllowForbidForbid
ISA11+BISAllowAllowAllow
ISA12AllowAllowAllow
ISA13ForbidForbidForbid
ISA13+BISForbidForbidForbid
ISA14ForbidForbidForbid
ISA14+BISForbidForbidForbid
ISA14+NEWForbidForbidForbid
ISA14+TERForbidForbidForbid
ISA15AllowAllowAllow
ISA16ForbidForbidForbid
ISA17ForbidAllowAllow
ISA18ForbidAllowAllow
ISA-OLD+BISAllowForbidForbid
ISA-OLD+TERAllowForbidForbid
ISA-DEP-WW-DATAForbidForbidForbid
ISA-DEP-WW-ADDRForbidForbidForbid
ISA-DEP-WW-CTRLForbidForbidForbid
ISA-DEP-WR-ADDRForbidForbidForbid

Store conditional instructions

A second table lists a few tests that involve store conditional instructions:

There are 16 such tests
 KindHerdVariantOp
Andy22ForbidForbidForbid
Andy25ForbidForbidForbid
Andy26ForbidForbidForbid
Andy27+FILTERForbidForbidForbid
ISA-MP-DEP-ADDR-LR-FAILAllowAllowAllow
ISA-MP-DEP-ADDR-LR-SUCCESSForbidForbidForbid
LB+addr+addrpx-poxp+VARAllowAllowAllow
LB+addr+addrpx-poxp+VAR2AllowAllowAllow
LR-SC-NOT-FENCEForbidForbidForbid
LR-SC-diff-loc1ForbidAllowAllow
LR-SC-diff-loc2ForbidAllowAllow
LR-SC-diff-loc3ForbidAllowForbid
LR-SC-diff-loc4ForbidAllowForbid
MP+Data-XX-AddrAllowAllowAllow
SWAP-LR-SCRequireRequireRequire
SWAP-LR-SC+FULLRequireRequireRequire

Some tests of interest

Testing .aq.rl on AMO’s (SC) and on LR-SC pairs (RCsc).

Also testing ppo rule 12:

a and b are loads, and there exists some store m between a and b in program order such that m has an address or data dependency on a, and b reads a value written by m

We test: (1) normal usage: a is load; (2) extension: a is store conditonal.

There are 7 such tests
 KindHerdVariantOp
AMO-FENCEForbidForbidForbid
LR-SC-NOT-FENCEForbidForbidForbid
PPOLDSTLD01ForbidForbidForbid
PPOLDSTLD02ForbidForbidForbid
R+fence.w.w+fence.tsoAllowAllowAllow
R+fence.w.w+posxp-addrForbidForbidForbid
SWAP-LR-SC+FULLRequireRequireRequire

Comparing models

Comparing with previous versions


This document was translated from LATEX by HEVEA.