Extended abstract: a formal design approach from software oriented UML descriptions to hardware oriented RTL

In this paper we discuss UML based hardware design approaches that can effectively and efficiently use formal verification methods to analyze and verify designs. We discuss techniques on how to use UML based design analysis for generating reduced models that are used in formal verification. This process typically starts with pure functional analysis of the design targets and then gradually converts them to more structural ones so that the final ones can be considered as register transfer level (RTL) designs. We show how UML diagrams can be used to come up with reduced models that can be used for assume-guarantee reasoning and compositional reasoning. We use a real chip design process as an example and discuss about our design and verification methodology.