Lecture

High-Level Synthesis: Formally Verified Elastic Circuits

Related lectures (31)

FPGA Programming with Speedgoat: Real-Time Signal Processing

Focuses on implementing a square function generator using Speedgoat FPGA technology and real-time signal processing techniques.

FPGA Programming with Speedgoat: A Comprehensive Overview

Covers FPGA programming with Speedgoat, focusing on synthesis, design practices, and practical examples.

Instruction Set Extensions: High-Level Synthesis Techniques

Covers instruction set extensions and high-level synthesis techniques for optimizing embedded processors.

Digital Systems Design: Course Overview

Covers the organization, focus, methodology, and tools used in designing digital systems.

Field Programmable Gate Arrays (FPGAs)

Covers the basic principles and architecture of Field Programmable Gate Arrays (FPGAs) and their implementation options for digital circuits.

From Algorithms to Architectures

Explores the transition from algorithms to hardware architectures in digital system design, covering isomorphic architectures, VHDL implementation, and hardware efficiency metrics.

Hardware Description Languages

Explores the history and significance of Hardware Description Languages in automating design processes and describing parallel hardware.

Digital Logic Circuits: CMOS and Verilog Design

Discusses digital logic circuits, CMOS technology, and Verilog for circuit design.

Formally Verified Chisel Designs

Explores formally verifying Chisel designs using SMT solvers and covers examples like delayed assertions and proofs by induction.

Finite State Machines (FSMs)

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

Hoare Logic: Foundations and Applications

Covers Hoare Logic, its foundations, applications, and significance in program verification.

Lambda Calculus and Type Safety: An Overview

Provides an overview of lambda calculus, type safety, and type inference in programming languages.

Programmable Logic Devices: PAL, GAL, CPLD

Covers PAL, GAL, CPLD, and the transition to FPGAs using HDLs.

Quantum and Nanocomputing

Covers quantum and nanocomputing, focusing on molecules as conductive elements, molecular transistors, and field coupling elements.

Parallel Port & Nios II Interrupts

Covers the design of a programmable parallel port interface for an Avalon bus and the architecture of the Nios II processor.

An Introduction to Iris: Higher-Order Concurrent Separation Logic

Introduces Iris, a logical framework for reasoning about safety and correctness of concurrent higher-order imperative programs, emphasizing its unique characteristics and applications.

Generating a CLK Generator (PLL) IP in Vivado

Covers the process of generating a Clock Generator (PLL) IP in Vivado using the Clocking Wizard tool.

VHDL for Synthesis

Covers basic VHDL constructs for RTL design, including arithmetic, multiplexers, registers, and instantiation.

Compiler verification: Challenges and Benefits

Explores the challenges and benefits of compiler verification, emphasizing the importance of verifying compilers for critical software.

Foundations of Software

Covers the basics of induction, syntax, abstract vs. concrete syntax, and operational semantics for Booleans.