+#if AO_USB_DEVICE_ID_SERIAL
+static uint8_t ao_usb_serial[2 + 48];
+
+/* Convert a 32-bit value to 8 hexidecimal UCS2 characters */
+static void
+hex_to_ucs2(uint32_t in, uint8_t *out)
+{
+ int i;
+
+ for (i = 28; i >= 0; i -= 4) {
+ uint8_t bits = (in >> i) & 0xf;
+ *out++ = (bits < 10) ? ('0' + bits) : ('a' + bits);
+ *out++ = 0;
+ }
+}
+
+/* Encode the device ID (96 bits) in hexidecimal to use as a device
+ * serial number
+ */
+static void
+ao_usb_serial_init(void)
+{
+ ao_usb_serial[0] = 50; /* length */
+ ao_usb_serial[1] = AO_USB_DESC_STRING;
+ hex_to_ucs2(stm_device_id.u_id0, ao_usb_serial + 2 + 0);
+ hex_to_ucs2(stm_device_id.u_id1, ao_usb_serial + 2 + 16);
+ hex_to_ucs2(stm_device_id.u_id2, ao_usb_serial + 2 + 32);
+}
+#endif
+