openrisc / mor1kx

mor1kx - an OpenRISC 1000 processor IP core
Other
490 stars 146 forks source link

Formal: Wishbone Interface #133

Closed Harshitha172000 closed 3 years ago

Harshitha172000 commented 3 years ago

Formally verifying properties of "B3_READ_BURSTING"/"B3_REGISTERED_FEEDBACK" wishbone. Property checks for IBUS_BRIDGE pass, but DBUS_BRIDGE fails in some cases. "CLASSIC" Wishbone is not reset, so many properties of this interface are not satisfied. The maximum request value is set to 16, which can be increased but should choose 'F_LGDEPTH' carefully, or else the test won't pass f_outstanding validations.

stffrdhrn commented 3 years ago

Please resolve conflicts