**Are you an EPFL student looking for a semester project?**

Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.

Lecture# Formally Verified Chisel Designs

Description

This lecture covers the concept of formally verifying Chisel designs using SMT solvers. It explains Chisel as a hardware construction language in Scala, the use of SMT solvers to prove hardware design properties, and examples like delayed assertions and proofs by induction on state. It also delves into formal verification of communication protocols like AXI4, emphasizing the importance of loop invariants, preconditions, and postconditions in digital circuit design.

Official source

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

In course

Related concepts (44)

Instructor

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

In digital circuit design, register-transfer level (RTL) is a design abstraction which models a synchronous digital circuit in terms of the flow of digital signals (data) between hardware registers, and the logical operations performed on those signals. Register-transfer-level abstraction is used in hardware description languages (HDLs) like Verilog and VHDL to create high-level representations of a circuit, from which lower-level representations and ultimately actual wiring can be derived.

A finite-state machine (FSM) or finite-state automaton (FSA, plural: automata), finite automaton, or simply a state machine, is a mathematical model of computation. It is an abstract machine that can be in exactly one of a finite number of states at any given time. The FSM can change from one state to another in response to some inputs; the change from one state to another is called a transition. An FSM is defined by a list of its states, its initial state, and the inputs that trigger each transition.

In automata theory, a finite-state machine is called a deterministic finite automaton (DFA), if each of its transitions is uniquely determined by its source state and input symbol, and reading an input symbol is required for each state transition. A nondeterministic finite automaton (NFA), or nondeterministic finite-state machine, does not need to obey these restrictions. In particular, every DFA is also an NFA. Sometimes the term NFA is used in a narrower sense, referring to an NFA that is not a DFA, but not in this article.

Digital electronics is a field of electronics involving the study of digital signals and the engineering of devices that use or produce them. This is in contrast to analog electronics and analog signals. Digital electronic circuits are usually made from large assemblies of logic gates, often packaged in integrated circuits. Complex devices may have simple electronic representations of Boolean logic functions. The binary number system was refined by Gottfried Wilhelm Leibniz (published in 1705) and he also established that by using the binary system, the principles of arithmetic and logic could be joined.

A finite-state transducer (FST) is a finite-state machine with two memory tapes, following the terminology for Turing machines: an input tape and an output tape. This contrasts with an ordinary finite-state automaton, which has a single tape. An FST is a type of finite-state automaton (FSA) that maps between two sets of symbols. An FST is more general than an FSA. An FSA defines a formal language by defining a set of accepted strings, while an FST defines relations between sets of strings.

Related lectures (45)

Finite State Machines (FSMs)EE-334: Digital systems design

Explores Finite State Machines (FSMs) in digital system design, covering Mealy and Moore FSMs, state diagrams, VHDL implementation, and state encoding.

Verifying Programs with Stainless: Part 2CS-550: Formal verification

Focuses on using Stainless for program verification, demonstrating the process of verifying programs and ensuring correctness.

Logic Systems: Sequential and Combinatorial CircuitsEE-110: Logic systems (for MT)

Covers fundamental concepts of logic systems, including sequential and combinatorial circuits, state diagrams, and finite state machines.

Hardware Verification using High-Level Design Languages

Explores challenges in hardware verification, clear specifications, speculation harm, and cycle-precise semantics.

Arbiter FSM & FPGA ImplementationEE-334: Digital systems design

Covers the design of an Arbiter FSM in VHDL for digital system design, emphasizing access timing management.