| With the increasing complexity and wide application of software systems,their correctness and reliability inevitably become the first problems to be solved in today's software systems.For large and complex software systems,traditional testing methods cannot be relied upon to ensure the required reliability and completeness.It is replaced by formal verification,which analyzes,deduces and verifies software systems through mathematical logic,and it has become an important way to ensure the credibility of complex software systems.System verification based on temporal logic is an important method of formal verification.MSVL is just a kind of temporal logic programming language.It is suitable for simulation,modeling and verification of software and hardware system.Compiler and interpreter,as two ways to implement languages,have different performance.As we all know,the compiler's performance in terms of speed and memory footprint is superior.So,for MSVL language,how to design and develop a compiler with superior performance is very important.The main work of this paper is to design and develop an efficient and universal MSVL compiler based on the LLVM framework from lexical analysis,syntax analysis and semantic analysis to IR code generation,optimization and target code generation under the 64-bit Linux platform.In the compiler test phase,in order to get a large number of test cases,we need some tools to quickly convert excellent algorithms in other languages into MSVL programs.The current MSVL ecosystem already has V2 MSVL tools that convert VHDL to MSVL,Veri2 MSVL tools that convert Verilog to MSVL,and C2 MSVL tools that convert C language to MSVL.The C2 MSVL tool can also be used for the conversion of some C ++ programs,but it cannot handle the object-oriented parts of C ++.In response to this defect,we have developed a conversion tool using shell language,which is mainly used to convert C++ to MSVL program with C ++ object-oriented part as the core. |
PDF Full Text Request