Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

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.

This video is available exclusively on Mediaspace for a restricted audience. Please log in to MediaSpace to access it if you have the necessary permissions.

Watch on Mediaspace

Official source

Related concepts (32)

Postcondition

In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions within the code itself. Often, postconditions are simply included in the documentation of the affected section of code. For example: The result of a factorial is always an integer and greater than or equal to 1.

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.

Finite-state machine

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.

Chisel (programming language)

The Constructing Hardware in a Scala Embedded Language (Chisel) is an open-source hardware description language (HDL) used to describe digital electronics and circuits at the register-transfer level. Chisel is based on Scala as an embedded domain-specific language (DSL). Chisel inherits the object-oriented and functional programming aspects of Scala for describing digital hardware. Using Scala as a basis allows describing circuit generators. High quality, free access documentation exists in several languages.

Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Related lectures (49)

Verifying Programs with Stainless: Part 2

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

Introduction to Stainless: First Steps with Stainless

Introduces the Stainless verification tool with examples of verifying commutativity properties and arithmetic operations.

Verifying Compiler: Spec# Approach

Explores the Spec# programming system, focusing on a verifying compiler for C# 2.0.

Logic Systems: Sequential and Combinatorial Circuits Log in to Mediaspace to watch this video

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

Digital Systems: Flip-Flops, Registers, and Counters Log in to Mediaspace to watch this video

Provides an overview of flip-flops, registers, and counters in digital systems.

Related concepts (32)

Postcondition

Finite-state machine

Chisel (programming language)

Formal verification