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.

Store conditional instructions

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

• “Andy” tests (initial tests by Andy Wrigth), illustrate various scenarios of dependences, most often through the result resgister of store conditional instructions. It is fascinating that herd and rmem systematically oppose one another here.
• The remaining two tests (initial tests by Shaked Flur) illustrate a point about the existence of non-existence of address dependencies when store conditional instructions fail.

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.

• Comparing the Herd (axiomatic) and Op (operational) models
  • Allowed by Herd, forbidden by Op
  • Allowed by Op, forbidden by Herd
• Comparing Variant with Herd
  • Allowed by Variant, forbidden by Herd
  • Allowed by Herd, forbidden by Variant

• Herd model
  • New behaviours
  • Behaviours suppressed
• Operational model
  • New behaviours
  • Behaviours suppressed

This document was translated from L^AT_EX by H^EV^EA.