What's wrong with this assertion?

[danielkasza]

trafficstars

This passes:

class TestModule extends Module with Formal {
    val io = IO(new Bundle {
        val in = Input(Bool())
        val a = Output(Bool())
        val b = Output(Bool())
    })

    val aReg = RegInit(true.B)
    val bReg = RegInit(true.B)
    io.a := aReg
    io.b := bReg

    aReg :=  io.in
    bReg :=  io.in

    assert(aReg === bReg)
}

This does not:

class TestModule extends Module with Formal {
    val io = IO(new Bundle {
        val in = Input(Bool())
        val a = Output(Bool())
        val b = Output(Bool())
    })

    val aReg = RegInit(true.B)
    val bReg = RegInit(false.B)
    io.a := aReg
    io.b := bReg

    aReg :=  io.in
    bReg := !io.in

    assert(aReg ^ bReg)
}

Failed to assert condition at (filename:line)

I suspect that this has to do with how Chisel treats reset values on registers, but I am not sure. Can you help me understand what's wrong here?

[danielkasza]

It looks like it works if I do:

    when (numResets > 0.U) {
        assert(aReg ^ bReg === true.B)
    }

Would it make sense to move that check inside assert? I think that would be consistent with how Chisel modules are normally used. Another assert function could be provided for the special case when you care about behavior before a reset.

[tdb-alcorn]

This is a reasonable idea: make the default use of assert the one we usually want. I don't see any reason not to do this, but I will bring it up at the next chisel dev meeting to see if there are any good objections. If we're clear, I'll make the change. If you're keen to submit a patch implementing this, that would also be welcome!