Formal Verification Support

[huskyii]

In the paper "LLHD: A Multi-level Intermediate Representation for Hardware Description Languages", you stated that LLHD is suitable for formal verification. And I can't find assume/cover/assert instruction in LLHD Language reference. Could you provide some small demo that show its ability for formal verification?

[fabianschuiki]

The current strategy is to have assert/assume/cover be LLHD intrinsics:

call void @llhd.assert(i1 %some_condition);
call void @llhd.assume(i1 %some_condition);
call void @llhd.cover(i1 %some_condition);

These are not yet emitted by the Moore compiler, but that will follow soon.

What needs to be developed/decided is, how we are going to represent temporal logic. The above intrinsics are very convenient for immediate assertions, against a boolean expression. However, concurrent assertions with properties/sequences are a bit more involved, but I definitely want to have a solid story for those. One option would be to introduce an opaque %llhd.sequence type, with intrinsics to describe temporal logic, like call %llhd.sequence @llhd.sequence.or(%llhd.sequence %seqA, %llhd.sequence %seqB). While this is not super-elegant, it would at least allow for the temporal logic to be represented in the LLHD IR graph.

Any feedback or suggestions are highly appreciated!