The switching element was designed using a Hardware Description Language: Qudos HDL. This is a simple HDL that allows the structure of hardware to be specified. It does not allow behaviour to be specified directly. To formally verify the switching element, we needed a structural description of the implementation in a language with a formally defined semantics. Without this no formal reasoning about the behaviour of the circuit is possible. Unfortunately, Qudos HDL does not have a formal semantics. We therefore manually translated the original descriptions to HOL-HDL. This is a subset of the HOL logic with the flavour of a hardware description language. It allows descriptions to be given which are very similar to descriptions in Qudos HDL. The translation could have been done completely mechanically, involving only the changing of syntax. However, we made some superficial changes to the description. They did not alter the design, only the description of it. Both descriptions were intended to describe the same collection of logic gates. Two kinds of changes were made: adding extra layers to the hierarchy and simplifying the description using features of HOL which were not available in Qudos HDL. For example, in HOL we were able to represent the data inputs and outputs as words containing 4 bytes, rather than as unstructured 32-bit words as was necessary in Qudos HDL.