For an SOI-FPGA （silicon-on-insulator field programmable gate arrays） （VS1000） fabricated with 0.5 ttm SOI-CMOS （silicon-on-insulator complementary-metal-oxide-semiconductor） process, a complete integrated platf...For an SOI-FPGA （silicon-on-insulator field programmable gate arrays） （VS1000） fabricated with 0.5 ttm SOI-CMOS （silicon-on-insulator complementary-metal-oxide-semiconductor） process, a complete integrated platform of FPGA computer-aided design （CAD） toolset （VDK） is developed, which can convert the Verilog HDL （hardware description language） description into a bitstream and finally download it into an FPGA. Experiments and testing verify that this FPGA CAD works well and efficiently.展开更多
We present a graph-based model of a generic type system for an OO language. The type system supports the features of recursive types, generics and interfaces, which are commonly found in modern OO languages such as Ja...We present a graph-based model of a generic type system for an OO language. The type system supports the features of recursive types, generics and interfaces, which are commonly found in modern OO languages such as Java. In the classical graph theory, we define type graphs, instantia- tion graphs and conjunction graphs that naturally iIlustrate the relations among types, generics and interfaces within complex OO programs. The model employs a combination of nominal and anonymous nodes to represent respectively types that are identified by names and structures, and de- fines graph-based relations and operations on types including equivalence, subtyping, conjunction and instantiation. Algo- rithms based on the graph structures are designed for the im- plementation of the type system. We believe that this type system is important for the development of a graph-based logical foundation of a formal method for verification of and reasoning about OO programs.展开更多
Formal verification of VHSIC Hardware Description Language （VHDL） in Field-Programmable Gate Array （FPGA） design has been discussed for many years. In this paper we provide a practical approach to do so. We presen...Formal verification of VHSIC Hardware Description Language （VHDL） in Field-Programmable Gate Array （FPGA） design has been discussed for many years. In this paper we provide a practical approach to do so. We present a semi-automatic way to verify FPGA VHDL software deadlocks, especially those that reside in automata. A domain is defined to represent the VHDL modules that will be verified; these modules will be transformed into Verilog models and be verified by SMV tools. By analyzing the verification results of SMV, deadlocks can be found; after looking back to the VHDL code, the deadlocking code is located and the problem is solved. VHDL verification is particularly important in safety-critical software. As an example, our solution is applied to a Multifunction Vehicle Bus Controller （MVBC） system for a train. The safety properties were tested well in the development stage, but experienced a breakdown during the long-term software testing stage, which was mainly caused by deadlocks in the VHDL software. In this special case, we managed to locate the VHDL deadlocks and solve the problem by the FPGA deadlock detection approach provided in this paper, which demonstrates that our solution works well.展开更多
文摘For an SOI-FPGA （silicon-on-insulator field programmable gate arrays） （VS1000） fabricated with 0.5 ttm SOI-CMOS （silicon-on-insulator complementary-metal-oxide-semiconductor） process, a complete integrated platform of FPGA computer-aided design （CAD） toolset （VDK） is developed, which can convert the Verilog HDL （hardware description language） description into a bitstream and finally download it into an FPGA. Experiments and testing verify that this FPGA CAD works well and efficiently.
文摘We present a graph-based model of a generic type system for an OO language. The type system supports the features of recursive types, generics and interfaces, which are commonly found in modern OO languages such as Java. In the classical graph theory, we define type graphs, instantia- tion graphs and conjunction graphs that naturally iIlustrate the relations among types, generics and interfaces within complex OO programs. The model employs a combination of nominal and anonymous nodes to represent respectively types that are identified by names and structures, and de- fines graph-based relations and operations on types including equivalence, subtyping, conjunction and instantiation. Algo- rithms based on the graph structures are designed for the im- plementation of the type system. We believe that this type system is important for the development of a graph-based logical foundation of a formal method for verification of and reasoning about OO programs.
文摘Formal verification of VHSIC Hardware Description Language （VHDL） in Field-Programmable Gate Array （FPGA） design has been discussed for many years. In this paper we provide a practical approach to do so. We present a semi-automatic way to verify FPGA VHDL software deadlocks, especially those that reside in automata. A domain is defined to represent the VHDL modules that will be verified; these modules will be transformed into Verilog models and be verified by SMV tools. By analyzing the verification results of SMV, deadlocks can be found; after looking back to the VHDL code, the deadlocking code is located and the problem is solved. VHDL verification is particularly important in safety-critical software. As an example, our solution is applied to a Multifunction Vehicle Bus Controller （MVBC） system for a train. The safety properties were tested well in the development stage, but experienced a breakdown during the long-term software testing stage, which was mainly caused by deadlocks in the VHDL software. In this special case, we managed to locate the VHDL deadlocks and solve the problem by the FPGA deadlock detection approach provided in this paper, which demonstrates that our solution works well.
