Formal Codesign and Implementation for Multifunction Vehicle Bus Circuits

Classical hardware development approaches for critical embedded systems are inefficient. Extensive resources must be committed before traditional hardware development can commence. Thus, an efficient method for circuit development is urgently required. In this paper, a computer-aided formal development method for a multifunction vehicle bus (MVB) is addressed. First, a formal modeling language is defined and its semantics are analyzed. Then, in terms of the modeling language, a formal computer-aided-design method is proposed for the design of complex MVB circuits. Core modules are modeled by extended timed automata. After the functionality of the model has been verified, the formal model is automatically converted into the hardware description language (HDL) code. Furthermore, code optimization algorithms are proposed to enhance the quality of the generated HDL code. Finally, the optimal formal MVB is designed and implemented as a circuit.