No Reset Signal for DUT in Chisel Formal

[B10615053]

I tried to verify following Register File with Chisel Formal, and I got an assertion failed.

[RFFormal] found an assertion violation 0 steps after reset!
Assertion failed: RS2 Index:   2, Data Expected: 0x00000001, Data Actual: 0x80000000

To solve this problem, I dumped the waveform file, and found out the DUT didn't seem to be Reset. If the DUT had been Reset, the io_dataRS2 should be 0 instead of 8000_0000. I also found the register in the RFFormal was not been Reset. My running environment are listed below:

• Operating System: Ubuntu 20.04.5 LTS
• Java: openjdk version 11.0.17 2022-10-18
• Chisel: 3.5.4
• ChiselTest: 0.5.2

My Chisel code are listed as following:

• Register File

  package cpu
  
  import chisel3._
  import chisel3.util._
  
  // Register File IO Port
  class RFIO() extends Bundle 
  {
    // Read
    val addrRS1 = Input(UInt(5.W))
    val addrRS2 = Input(UInt(5.W))
    val dataRS1 = Output(UInt(32.W))
    val dataRS2 = Output(UInt(32.W))
    // Write
    val wen = Input(Bool())
    val addrRD = Input(UInt(5.W))
    val dataRD = Input(UInt(32.W))
  }
  
  // General Purpose Register
  class RF() extends Module 
  {
    // Register File IO
    val io = IO(new RFIO())
    // Register File
    val rf = Mem(32, UInt(32.W))
  
    io.dataRS1 := 0.U
    when (io.addrRS1 =/= 0.U)
    {
        io.dataRS1 := rf(io.addrRS1)
    }
    io.dataRS2 := 0.U
    when (io.addrRS2 =/= 0.U)
    {
        io.dataRS2 := rf(io.addrRS2)
    }
    when(io.wen && (io.addrRD =/= 0.U)) 
    {
        rf(io.addrRD) := io.dataRD
    }
  }

• Chisel Formal

  package cpu
  
  import chisel3._
  import chisel3.util._
  import chisel3.testers._
  import chiseltest._
  import chiseltest.formal._
  import chiseltest.simulator.WriteVcdAnnotation
  import org.scalatest.flatspec.AnyFlatSpec
  
  class RFFormal extends Module
  {
    val dut = Module(new RF)
  
    // Arbitrary inputs
    val io = IO(new RFIO())
  
    // Connect the input to module
    io <> dut.io
  
    // Correct Result
    val register = Mem(32, UInt(32.W))
    val ansrdata1 = Mux(io.addrRS1.orR, register(io.addrRS1), 0.U)
    val ansrdata2 = Mux(io.addrRS2.orR, register(io.addrRS2), 0.U)
    when(io.wen & io.addrRD.orR) 
    {
        register(io.addrRD) := io.dataRD
    }
  
    // Assertion
    assert(ansrdata1 === dut.io.dataRS1, "RS1 Index: %d, Data Expected: 0x%x, Data Actual: 0x%x", io.addrRS1, ansrdata1, dut.io.dataRS1)
    assert(ansrdata2 === dut.io.dataRS2, "RS2 Index: %d, Data Expected: 0x%x, Data Actual: 0x%x", io.addrRS2, ansrdata2, dut.io.dataRS2)
  }
  
  class RFTest extends AnyFlatSpec with ChiselScalatestTester with Formal 
  {
    "Test RF with Formal Verification" should "PASS" in 
    {
        verify(new RFFormal, Seq(BoundedCheck(6)))
    }
  }

[ekiwi]

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: https://github.com/ucb-bar/chiseltest/blob/0894e8fba74674bcd32e7070211b40eb5be1b20b/src/test/scala/chiseltest/formal/MemoryTests.scala#L179

Please let me know if this fixes your issue.

[B10615053]

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:

[ekiwi]

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.