Skip to content
Rivoryxa Technologies
Discuss a problem

Showing two hardware loop guards need a software rule

Two coverage holes in a RISC-V core's controller that only badly placed hardware loops can reach. We proved both unreachable while software follows the rule.

Open source RISC-V core, coverage hole 1006Outcome: Waiver, with a software rule
View the issue Read the full report

1The issue

Lines 632 and 642 of the core's controller stop a jump being issued twice at the end of a hardware loop, one line for each of the two loops. Hardware loops let the core repeat a block of code without branch instructions. The false side of each guard was never covered. The core's maintainers waived both after an equivalence check showed that removing the lines leaves the outputs unchanged.

The points on the issue

Hardware aloneReachable. A formal search reaches both lines in 9 cycles when the two loop end addresses are one instruction apart.
Software follows the loop nesting ruleCan never happen on either line. Proven with formal verification under that rule.
Software breaks the ruleHarmless. The guard only blocks a duplicate jump.

2What we did

  1. 1Found that the false side needs the two loop end addresses to differ by exactly one instruction, 4 bytes. The nesting rule puts the outer end at least two instructions past the inner end.
  2. 2Checked this with a solver. The guard is impossible with the rule and possible without it.
  3. 3Proved both lines unreachable on the design with an induction proof, using one assumption: the two end addresses never differ by exactly 4 bytes.

3Result

Both lines can be waived with a software rule, now backed by a formal proof instead of the equivalence argument.

The waiver holds only while software obeys the stated rule. If software can break it, the code is reachable.

Read the full report

Have a coverage hole like this one?

Describe the problem in a few lines. An engineer replies, and we agree the scope together.

Discuss a verification problem