Computing systems are everywhere in nowadays life, but when we think of them, most of us think of “desktop” computers, like PCs, laptops, mainframes and servers. But there is another type of computing systems that is far more common: embedded computing systems. They are computing systems embedded within electronic devices, intuitively nearly any computing system other than a desktop computer. Their main features are: • billions of units produced yearly, versus millions of desktop units • several tens, maybe hundreds, per household and per automobile • they are: • single-functioned as they execute a single program, repeatedly • tightly-constrained in terms of low cost, low power, small size, speed, etc. • reactive and real-time, as they continually reacts to changes in the system’s environment and must compute results in real-time without delay Designing embedded systems requires: • knowledge of what the hardware is and does (combinational circuits, sequential circuits, Finite State Machines, register-transfer level systems) • knowledge of design methodologies for each of the previous classes, the approach being oriented to automated synthesis • acquaintance with a Hardware Description Language and ability to describe designed hardware resorting to it • skills to use CAD tools for description, simulation and synthesis. In this context, the course aims to provide adequate knowledge of hardware and hardware design methodologies, ranging from combinational circuits, to sequential circuits, Finite State Machines and register-transfer level systems. VHDL is the Hardware Description Language used, whereas Verilog is introduced by difference. The emphasis is not on the syntax of the language, rather on hardware design. Constructs and features of the language are introduced whenever they serve the purpose of illustrating new concepts in the hardware. The teaching methodology is thus not language-oriented, rather design-oriented. The development of a sound and structured hardware design methodology is one of the core goals of the Course. The course completes the design methodologies acquired in previous basic digital design courses and extends them to the register-transfer level, where the FSM-D model is adopted (Finite State Machine with Datapath) to overcome the limits of the classical FSM when bigger systems are considered, where operations and control coexist. The free Xilinx design toolkit Vivado HL WebPACK Edition is used to describe, simulate and synthesize complex systems in a lab-based hands-on experience. As simulation-based verification can’t be exhaustive in real-world designs, verification techniques based on formal methods, in particular combinational and sequential equivalence check and model checking, are introduced.