Readon

> I think it is related with the generating method of pastValid. Adding xxx.initial(False) is also a more generic solution. I will write a minimal example to test it first.

I have test with [rtcclock/rtcstopwatch](https://github.com/ZipCPU/rtcclock/blob/0bc3c7fe83fbb17d7e2fbc0dbf8166e5ab2b6734/bench/formal/rtcstopwatch.sby#L1) by replace the f_past_valid logic with above then validation failed. The correct version should be ``` verilog reg f_past_valid; initial f_past_valid = 1'b0; always @(posedge...

> ```scala > initial(False) > ``` The problem is that at the beginning of prove the value of registers can be any value, so there are cases formal_with_past reg ===...

> So > > ```verilog > reg f_past_valid; > initial f_past_valid = 1'b0; > always @(posedge i_clk) > f_past_valid end > > always @(posedge clk) begin > formal_with_past > Let's...

> > By definition, it has no relation with reset at all, there should be extra code to work with that. > > Does it make sense to trigger on...

One more thing, would be notice here. When verify an async logic, the clocks are generated from global clock where pastValid would be designwise valid after the first global clock....

> Wouldn't the pastValidAfterReset also use the resetKind = BOOT ? => initial reg = 0 The thing is that there are no reset for global clock domain. But pastValidAfterReset...

> Fixed in [2c20f1c](https://github.com/SpinalHDL/SpinalHDL/commit/2c20f1c8d9a29d595e618ac30fada3812feb5fea) It's a little bit complicated, the name of those signal should be different with clock domain too. And the pastValid signal could be design wise, because...

> > It's a little bit complicated, the name of those signal should be different with clock domain too. > > So, as the name is set with setWeakName, name...

I find that it's about recompile calss in "tester" subproject.