A verified platform for a gate-level electronic control unit
Sergey Tverdyshev · 2009
We present the formal integration of an automotive bus controller into a formally verified gate-level computer system. This system consists of a complex processor and generic devices which run in parallel. The system specification is an instruction set architecture with concurrently running visible devices. The built system is an electronic control unit which is the base element for a distributed automotive system and its size on an FPGA is ca. 5 M gate equivalents.