Formal Method for Verifying SpaceWire Encoding Circuit by Applying Theorem Proving
SpaceWire bus is applied in Space Solar Telescope(SST) project.Testing and simulation are the main methods for verification of SpaceWire bus,but these verifications are incomplete.This study focused on verifying whether the DS encoder circuit developed for SST had faithfully implemented the specification in SpaceWire standard.With the aid of HOL4 tool,this equivalence checking was carried out in a formal verification method,theorem proving.It overcame the limitation of testing and simulation.