Posted on November 5, 2019
Categories: idris, soc, hardware, substructural-type-systems, dependent-types, border-patrol, tdd, systems
On Tuesday 05 November 2019, Jan gave the School Seminar at the University of St Andrews School of Computer Science. His talk discussed recent results in developing formalisms to support hardware orchestration.
The abstract is:
Two important aspects in hardware design are the safe routing of signals between modules, and ensuring that ports are correctly connected. Well-known hardware description languages such as SystemVerilog, provide nominal checking over these aspects. Thus, leaving correctness checks over module orchestration to be performed post-design-time using static analyses, testing, and during synthesis.
Using a mixture of dependent and quantitative typing, we can lift external correctness checks over module connections directly into the type-system. With this approach we can detect more errors at design time, enhance the safety of our hardware designs, and thus increase design productivity.
In this talk I will introduce and discuss LightClick, an orchestration language for hardware design that exemplifies our approach. LightClick uses quantitative typing to ensure linear usage of ports, and dependent types to ensure that port compatibility is a decidable compile-time check. I will show how LightClick can be used to model simple hardware designs, how SystemVerilog stubs are generated from designs using staged interpretation.
Slides are not available.