The Application Of Automata Theory In The Verification PSL

With the development of information technology, the size and the complexity of integrate circuits grow up quickly and the time of verification in the development cycle is enhanced. Moreover, the competition in the IC market is intense. To ensure the validity of design and to shorten the time-to-market as could as possible is a key for a product to make success. Those also bring high requirements to verification technology and methodology. To ensure the validity of design is to ensure that the implement of design should accord with the specification of design. Consequently, the language for specification should be expressive for use and have the precision to describe the requirement. At the same time, the usage of the language should be easy. PSL is the one of the languages which meets all characters above.PSL could be used to describe assertion. Furthermore, the assertion may be embedded in the design, which provides many advantages for verification and shortens the verification time effectively. The more attractive point in PSL is that it may be used as the input of dynamic verification and as the formal specification language of formal verification tools. On account of these merits, PSL have been developed as an industrial standard of property specification language.This dissertation discusses how to implement the PSL-based dynamic verification and the formal one based on the automata theory. According to dynamic verification PSL, this dissertation introduces a type of automata named sequence automata and how to encodes the PSL property using the sequence automata. According to model checking PSL, this dissertation brings a different method to translate PSL to Buchi automata, which is based on the method of translation LTL to Buchi automata.