Data bus Wishbone Interface Formal Check fails

[Harshitha172000]

Properties that failed:

1. The direction of the write enable shouldn't change within a series of strobe/requests.
2. Within any given bus cycle, the direction may only change when there are no further outstanding requests

Solver picks up a case where the write enable changes due to atomic signal transition.

Code:
https://github.com/openrisc/mor1kx/blob/master/bench/formal/fwb_master.v#L173#L186

Trace showing failure:

[stffrdhrn]

can you put a link to the code, or mention the module where this is happening?

[Harshitha172000]

Wishbone Interface referring to mor1kx.v module.