Design And Formal Verification Of The Hardware Platform Based Programmable Logic

The safe hardware platform is accomplished through advanced computer and electronic technology. With the development of computer and electronic, the capability of system increasing while the complexity increasing. Hardware platform as a important part of safe-critical system, safety is vital importance. The safety of the hardware platform must be fully concerned at the design phase, for fear the disfigurement of design will be result in the hidden safety trouble existing in the system. Due to the systems developing to the large scale, high performance, high complexity direction, it can not accomplish with the simulation alone. So in the design phase of hardware platform, need to use the formal verification to validate it. It is necessary to validate the correct and the maturity of the hardware platform.CBTC system is the background of this paper, analysis the requirement of hardware platform. Trough to compare some different kinds of platform architecture, select the 2×2-out-of-2 as the design architecture. On the base of analysis architecture of safe computer, combine with the requirement of CBTC, propose a new system architecture.Safety and currency are the emphases of the safe hardware platform in this paper. The methods to achieve specific functionality of safety, currency and scheduling strategy are described in this paper. The safety of the platform is ensured by use of the micro-synchronization and the data compare with hardware. The currency of the platform is ensured by provision of the processor, data frame and interface.The safe compare core is the important part of the safe hardware platform. The safe compare core is design and complement based on the programmable logic. With programmable logic not only can cut the size of circuit, but also increase the stability of circuit. While the advanced tools will save the time of system design. In the implement phase, the safe compare core is divided into some sub-module with different function. To accomplish and simulate any sub-module ensure the result of design correct.The formal verification of the platform based on assert. The simulation can only ensure the result correct, but face the complex system, simulation without end is unpractical. In order to avoid the design error, use PSL to validate the compare core, make formal verification of the validity and integrality of the compare core design. When the assert fail, the error can be detected. Analysis the error and modify the design, then simulate it again. After simulation, make formal verification again, until there is no error in the design.Paper research a new platform architecture, and use the programmable logic to achieve. Then, the design verified through assert. At last, we get a non-bug, high efficiency and currency safe hardware platform.