Cover is not yet implemented for Chiseltest

[Gallagator]

Cover statements are not yet possible. Something like:

class Foo() extends Module {
  val out = IO(Output(Bool()))
  val i = Counter(10)
  out := i === 9
  cover(out)
}

verified with:

verify((new Foo), CVC4EngineAnnotation, CoverCheck(10))

Which should generate a trace showing that it is possible for out to go high.

[ekiwi]

Thanks for filing this issue. This feature is indeed missing.

[Gallagator]

I've had a bit of free time lately and I figured this would be easy given that this is similar to implementing k-induction. Unfortunately, it seems there is no signal label for the Cover statement like there is for assert (IsBad), or assume(IsConstraint). I could add it here by the looks of it but firrtl doesn't seem to be maintained anymore. Should we be trying to move to circt? Maybe I should just submit a pr to firrtl? I hope you could give me some advice!

[ekiwi]

My advice would be to pre-process the firrtl. I.e., write a firrtl pass that removes all assert statements and changes all cover statements to asserts. That should be a relatively simple transform. You might be inspired by: https://github.com/ucb-bar/firrtl2/blob/main/src/main/scala/firrtl2/transforms/formal/RemoveVerificationStatements.scala

Edit: assume statements should actually stay in the circuit since you want to find a way to reach the cover point that obeys the assumptions.