Readon

I think this tester should be refacted with BmbMasterAgent and DfiSlaveAgent (need to be newly added). How about comment the failed tester first?

I have tried the tester, the tester fail when I fixed the seed to 1111240514. However, when I use withFstWave in the tester, it would magically pass the test.

> > What version of verilator did you used ? maybe it is also related ? > > v5.024, directly installed using pacman. I tried both mingw-w64-x86_64-verilator and mingw-w64-ucrt-x86_64-verilator. >...

This is the version that I always suggest to use all-in-one environment.

Because of the rolling release of MSYS2, verilator 4.228 could not be found at msys2 repos now. I have rebuild and release it at [here](https://github.com/Readon/MINGW-SpinalHDL/releases/download/0.41/mingw-w64-x86_64-verilator-4.228-1-any.pkg.tar.zst). test and feed back is...

I have repeat all your steps and find that some tester still could not pass the tester for SpinalHDL itself.

The existing Formal facilities is based on VerilogHDL with SymbiYosys only. There might be bunch of things to be added and tested.

> > There might be bunch of things > > What do you mean by that? > > * Are there existing things that are actively being worked on? Where...

> Hi Tom! Avid reader of your blog! I somehow found your post _Under the hood of Formal Verification_ linked above that lead me down a rabbit hole. As I...

There is a related discussion on the property syntax, which might be an option. #689 About to define a new property traits. The existing property is emulated by when clause.