How to add options while using treadle to make random validif answer?

[wky17]

when I running a validif lofirrtl statement like:
io_out <= validif(UInt<1>("h0"), io_in)
I always get io_out equals toio_in, even the answer should be invalid. I've found that there is an option on this validlf, named ValidIfIsRandomAnnotation.
I added this annotation to treadle tester like this:

object TreadleTestHarness {
  val shell: Shell = new Shell("tr-validif-random") with FirrtlCli
  def apply(
             annotationSeq: AnnotationSeq = Seq.empty,
             flags:         Array[String] = Array.empty
           )(thunk:         TreadleTester => Unit
           ): Unit = {
    val allAnnotations = shell.parse(flags, annotationSeq)
    Logger.makeScope(allAnnotations) {
      val tester = TreadleTester(annotationSeq)
      thunk(tester)
      tester.finish
    }
  }
}

TreadleTestHarness(annotationSeq = Seq(FirrtlSourceAnnotation(file), ValidIfIsRandomAnnotation)) { tester => ...}

but nothing happens, I still get io_out equals to io_in, so how can I get random value when the variable is invalid?

[ekiwi]

I assume the problem here is that the firrtl compiler removes the validif before it ever gets to treadle and currently there is no work around for this.

[ekiwi]

If you use the formal verification in chiseltest, that will actually correctly handle the validif in that it allows any value if the condition is false.