No Reset Signal for DUT in Chisel Formal about chiseltest HOT 3 CLOSED

Memories are not reset by default since that is the behavior you would expect on an ASIC. Thus your two memories will start out with potentially different data and thus your check fails. You can initialize both memories to zero through a firrtl annotation:

Please let me know if this fixes your issue.

from chiseltest.

Hi @ekiwi , I appreciate your reply.
Add the following code indeed solve the Reset problem.

// Initial with all zeros
annotate(new ChiselAnnotation {
        override def toFirrtl = MemoryScalarInitAnnotation(rf.toTarget, 0)
})

But I was facing another issue of dumping waveform with following command.

testOnly cpu.RFTest -- -DwriteVcd=1

Why won't this generate vcd waveform file under test_run_dir direcotry?
Will Seq(BoundedCheck(6)) generate a cover waveform of 6 cycle clock?
Thank you again for the help！:smile:

from chiseltest.

Why won't this generate vcd waveform file under test_run_dir direcotry?

The formal verify command only generates a VCD if it find an assertion violation. No flag needed in that case.

Will Seq(BoundedCheck(6)) generate a cover waveform of 6 cycle clock?

Unfortunately cover trace generation is not implemented yet :(.
Haven't had time to work on that.

from chiseltest.