Intertwined development and formal verification of a 60× bus model

We describe a project in which the IBM/Motorola 60× bus protocol was incrementally modeled at an abstract level in Verilog and verified using Motorola´s Verdict model checker. The primary purpose of the modeling activity was to acquaint verification personnel with details of the 60× bus protocol and to document specific properties of the 60× bus that are necessary to guarantee compliance with hand-written protocol documentation. Our Verilog 60× bus model documents the 60× bus protocol for other Motorola business units