Add details of LionOS/Serengeti talks

content/downunderflow/2026/talks.csv

@@ -1,7 +1,6 @@
 Day,Time,Type,Title,Presenter,Abstract,Youtube,Slides
 Sat,9:00,Break,"Doors open, mingle with a coffee",,,,
-Sat,10:00,Normal,Opening,FOSSi Foundation team,Welcome to Down Underflow! All you need to know to have a successful conference.,,
-Sat,10:15,Normal,Cocotb: An Introduction and Update,Julius Baxter,An introduction to and round up of the latest and greatest from the [Cocotb project](https://www.cocotb.org/): chip development and verification turbocharger in Python.,,
+Sat,10:00,Normal,Opening,FOSSi Foundation team,Welcome to Down Underflow! Conference opening presentation.,,
 Sat,10:45,Normal,wafer.space: 1000 parts for $7k,Tim Ansell,An update on [wafer.space](https://wafer.space/).,,,
 Sat,11:15,Normal,OpenROAD in the Classroom: RTL to GDS flow,Samuel Tensingh,"This talk shares lessons from one of the early structured uses of the [OpenROAD RTL-to-GDS flow](https://github.com/the-openroad-project) in an Australian ASIC training course delivered through the [Semiconductor Sector Service Bureau (S3B)](https://s3b.au/). The course used a fully open-source flow built around [Yosys](https://github.com/YosysHQ/yosys) for synthesis, [OpenSTA](https://github.com/The-OpenROAD-Project/OpenSTA) for timing analysis, OpenDP for placement, TritonCTS for clock tree synthesis, and TritonRoute for routing. The presentation focuses on practical flow behaviour, setup and integration challenges, and recurring issues observed in real student designs. It concludes with concrete suggestions on how the community can make OpenROAD easier to use, more reliable, and better suited for teaching and large-scale training.",,,
 Sat,12:00,Break,"Lunch",,,,
@@ -11,8 +10,9 @@ Sat,14:00,Normal,hdlworkflow: Seamless FPGA workflows,Scott Huynh,"All HDL simul
 Sat,14:30,Normal,Hardware Hackademia - Open-Source Hardware Security Education at UNSW,Hammond Pearce,"In 2025 I launched COMP6420 Hardware Security at UNSW. This new course explores the principles and practices of hardware security, covering topics such as side-channel attacks, hardware trojans, cryptographic implementations in hardware, and more. Everything is designed around practical hands-on experiences and labs, ensuring that students not only learn the theoretical aspects of hardware security but also how to apply these concepts in real-world scenarios. In this talk, I will discuss how I achieved this through the use of the open-source OSS-CAD-Suite as well as the development of a bespoke educational hardware platform, the Hackster, which I also release under CC BY-SA.",,
 Sat,15:00,Normal,Zamlet: A mesh network based vector processing unit,Ben Reynwar,"This presentation will cover [Zamlet](https://github.com/benreynwar/zamlet), a RISC-V vector processing unit that scales to large numbers of lanes using a mesh network for interlane communication rather than a crossbar. I'll present some modelling work and some initial area estimates.",,
 Sat,15:30,Normal,A Language Abstraction for Custom CMOS Circuit Optimization,Zachary Sisco,"Despite the growing importance of custom blocks and cells in modern chips, custom-circuit design still relies heavily on manual optimization. In this talk, we argue that a language-driven representation and toolchain for transistor-level netlists can serve as infrastructure to enable transistor-level design automation for optimizations that scale to larger designs. This talk will present one step in this direction: We introduce TransiLog, a DSL for CMOS transistor networks. TransiLog combines behavioral and topological semantics to represent transistor-level structures. Using state-of-the-art rewriting techniques, we show how to optimize transistor netlists for multiple PPA goals using the same representation. TransiLog also emits SPICE netlists compatible with existing transistor-level physical design backends and offers a foundation for future hybrid flows that combine custom-circuit and cell-level optimization.",,
-Sat,16:00,Normal,Sealing the hardware-software contract with LionsOS on Serengeti using time protection and device verification,"Lesley Rossouw, Liam Murphy, Julia Vassiliki","The group will present their work on the [Serengeti SoC](https://github.com/au-ts/serengeti) and [LionOS](https://github.com/au-ts/lionsos)",,
-Sat,16:45,Normal,MockingBoard: A Remote ASIC Prototyping Farm,Daniel Ruelas-Petrisko,"ASIC prototyping flows struggle with complicated toolchain management, ad-hoc debug infrastructure and tight coupling to vendor IP. This talk will describe a flexible approach to engineering emulation clusters, scaling from budget FPGAs to large emulation platforms.",,
-
+Sat,16:00,Normal,Sealing the hardware-software contract with LionsOS on Serengeti using time protection and device verification,"Lesley Rossouw, Liam Murphy, Julia Vassiliki","The hardware-software contract underpins all modern software development, and yet it has grown hazy in sophisticated modern SoC designs. Increasingly complex microarchitecture opens new vulnerabilities in hardware which may be exploited by software and device drivers often have no contract with the hardware beyond the lossy specifications of vendor datasheets. Using a trustworthy OS and open-source SoC platform in [LionsOS](https://github.com/au-ts/lionsos) and [Serengeti](https://github.com/au-ts/serengeti), we seek to develop a trustworthy hardware-software contract using several new methods. For this talk, we present two of these methods.
 
+First, we will discuss our 'time protection' project. Contemporary hardware is unable to systematically prevent the existence of timing channels and we seek to close them using a combination of hardware and software features. We argue that time protection is a fundamental OS mechanism, and discuss its implementation on [Serengeti/CVA6](https://github.com/au-ts/serengeti) as CPU architectures do not provide the necessary hardware primitives.
 
+Secondly, we will present our device interface formalism project. Bugs in device drivers cause many vulnerabilities in operating systems, often resulting from violations of the device's protocol or faults in device designs. With a formal model of devices, formal methods can prove the absence of these bugs in drivers, but the accuracy of models derived from datasheets is limited. We solve this by verifying the model against the device's Verilog implementation, simultaneously establishing the absence of device faults.",,
+Sat,16:45,Normal,MockingBoard: A Remote ASIC Prototyping Farm,Daniel Ruelas-Petrisko,"ASIC prototyping flows struggle with complicated toolchain management, ad-hoc debug infrastructure and tight coupling to vendor IP. This talk will describe a flexible approach to engineering emulation clusters, scaling from budget FPGAs to large emulation platforms.",,