  IP-based software design is a crucial research field that aims to improve
efficiency and reliability by reusing complex software components known as
intellectual property (IP) components. To ensure the reusability of these
components, particularly in security-sensitive software systems, it is
necessary to analyze the requirements and perform formal verification for each
IP component. However, converting the requirements of IP components from
natural language descriptions to temporal logic and subsequently conducting
formal verification demands domain expertise and non-trivial manpower. This
paper presents a case study on software IP components derived from aerospace
embedded systems, with the objective of automating the requirement analysis and
verification process. The study begins by employing Large Language Models to
convert unstructured natural language into formal specifications. Subsequently,
three distinct verification techniques are employed to ascertain whether the
source code meets the extracted temporal logic properties. By doing so, five
real-world IP components from the China Academy of Space Technology (CAST) have
been successfully verified.
