PLARCH 2023
who it's for
hardware verification engineers, hardware designers, formal methods engineers, compiler engineers, security researchers, accelerator architects, rtl designers
topics
Sail to Clash translation; symbolic RTL timing verification; Serberus LLVM passes; Coq cycle-accurate semantics; Tags token model for dataflow; DSLs for sparse accelerators; PEak single-source hardware spec; axiomatic memory-model extraction; probabilistic DPOR stimulus generation; formal verification of non-blocking caches; CHERI library compartmentalisation; ChatGPT-assisted secure malloc
| title | author | length |
|---|---|---|
| Semi-Automated Translation of a Formal ISA Specification to Hardware | Harlan Kringen, Zachary D. Sisco, Jonathan Balkind, Timothy Sherwood, Ben Hardekopf | 09m |
Prototype pipeline converts Sail ISA specs into Clash hardware by translating Sail’s monadic effects into monadic stream functions that compile to a naive… | ||
| Leakage models are a leaky abstraction (...) | Anish Athalye, M. Frans Kaashoek, Nickolai Zeldovich, Joseph Tassarotti | 12m |
They verify timing by symbolically executing gate‑level RTL instead of assuming leakage models, translating circuits to Rosette and running a symbolic RTL… | ||
| Hardware-Software Codesign for Mitigating Spectre | Nicholas Mosier, Kate Eselius, Hamed Nemati, John C. Mitchell, Caroline Trippel | 18m |
Claims a provably correct mitigation for data-oblivious (constant-time) code called Serberus, implemented as LLVM passes (fence insertion, function-private… | ||
| Hardware Verification of Timing Side Channel Freedom in the Spectre Era | Stella Lau, Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala | 12m |
Claim: a synthesizable, pipelined two-core RISC-V design plus a hardware security monitor enforces strong timing isolation and is proven equivalent to an… | ||
| Tags: A Framework for Distributed Event Ordering | Paul Mure, Nathan Zhang, Caroline Trippel, Kunle Olukotun | 10m |
Proposes Tags, an abstract token-credit model for reconfigurable dataflow accelerators that concretely defines publish/update/ready functions and per-edge… | ||
| Stellar: A DSL to Build and Explore Sparse Accelerators | Hasan Genc, Hansung Kim, Prashanth Ganesh, Yakun Sophia Shao | 16m |
Stellar is a DSL that decouples function, dataflow, sparse formats and load‑balancing to automatically synthesize sparse accelerators and generates Verilog and… | ||
| PEak: A Single Source of Truth for Hardware Design and Verification | Caleb Donovick, Ross Daly, Jackson Melchert, Leonard Truong, Priyanka Raina, Pat Hanrahan, Clark Barrett | 12m |
PEak is an open-source Python DSL that claims a single source of truth by generating an executable Python model, a SMT formal model, and Magma RTL generation… | ||
| Challenges with Hardware-Software Co-design for Sparse Machine Learning on (...) Dataflow | Rubens Lacouture, Olivia Hsu, Kunle Olukotun, Fredrik Kjolstad | 10m |
Extends the Sparse Abstract Machine (SAM) and a dataflow accelerator model to handle real ML models, adds new hardware primitives (filter block, unary-value… | ||
| They're the same picture: a software-verification flow adapted for hardware verification | Andreas Lööw, Magnus O. Myreen | 15m |
Claims that the CakeML software-verification flow maps to hardware by replacing source functions with shallow-embedded Verilog, compiler correctness with a… | ||
| Design for Hardware Memory Model Verification | Yao Hsiao, Yasas Seneviratne, Tommy Tracy II, Kevin Skadron, Caroline Trippel | 17m |
Toolchain synthesizes an axiomatic MCM from SystemVerilog netlist using static netlist analysis, property generation and model checking, producing a model… | ||
| Nerv: Probabilistic Dynamic Partial Order Reduction for Hardware | Tianrui Wei, Shangyin Tan, Koushik Sen, Krste Asanovic | 10m |
Proposes probabilistic dynamic partial order reduction that records state transitions from warm-up runs, builds a probability table over transaction pairs, and… | ||
| NFC:Next-generation Formal verification for high performance Caches | Tianrui Wei, Jerry Zhao, Krste Asanovic | 12m |
Presents NFC, a formal framework that verifies a multi-banked non-blocking out-of-order data cache and finds 8 bugs in one hour. Uses BMC/abstraction/induction… | ||
| Sandia's Formal Hardware Design and Verification, Present and Future | Noah Evans | 10m |
Sandia applies Yosys and SMT-based equivalence checks to real ASIC designs and finds concrete results — an RTL one‑cycle Verilog RISC‑V spec is proven… | ||
| Silver Oak: Hardware Software Co-Design and Co-Verification in Coq | Ben Blaxill, Samuel Grütter, Jade Philipoom, Satnam Singh | 09m |
A prototype called Silver Oak formalizes parts of the OpenTitan root‑of‑trust in Coq, using Cava for an AES hardware block and Bedrock 2 for the RISC‑V driver… | ||
| Novel Numerical Hardware Design Methodology - From machine readable spec to optimized RTL | Theo Drane, Bill Zorn, Samuel Coward | 12m |
A machine-readable pipeline uses FPCore plus MPFR to simulate thousands of numeric-format variants in under two hours and generates a FPCore-to-bit-accurate… | ||
| Mixed-Abstraction HDLs and A Discussion on Other Aspects of HDL Design | Vighnesh Iyer, Borivoje Nikolic | 16m |
Argues that mixed-abstraction HDLs should compose multiple levels and demonstrates three Scala/Chisel EDSLs: a testbench DSL with an interpreter that schedules… | ||
| New Embedded DSLs for Hardware Design and Verification | Vighnesh Iyer, Kevin Laeufer, Young-Jin Park, Rohit Agarwal, Lixiang Yin, Bryan Ngo, Oliver Yu, Koushik Sen, Borivoje Nikolic | 10m |
Argues for mixed-abstraction HDLs and presents three Scala eDSLs specialized for testbench description, stimulus generation, and control-flow compilation… | ||
| Fearless Hardware Design | Rachit Nigam | 14m |
A new HDL called Filament uses a type system to record timing and structural constraints so code is provably safe across all parameter values: it encodes… | ||
| Library-based Compartmentalisation on CHERI | Dapeng Gao, Robert N. M. Watson | 12m |
Prototype implements a dynamic linker as TCB on Morello/CHERI and demonstrates library-granular compartments enforced by trampoline-mediated transitions… | ||
| Non-Newtonian Hardware Design for Longevity | Guy Wilks, Jonathan Balkind | 08m |
Proposes a modular accelerator methodology called Cohort and shows a hardware prototype: a three-stage multiplier implemented as chained micro-accelerators… | ||
| On the Generality of Matrix Multiplication | Andrew Alex, Zachary D. Sisco, Jonathan Balkind | 10m |
Claims a concrete mapping from a Turing-complete one-instruction-set ISA into sequences of matrix multiplications and uses a Rosette-based synthesizer to… | ||
| ChatGPT, Make a Secure Malloc for me | Jeremy Singer, Zheng Wang | 08m |
Claims a workflow to synthesize production-grade allocators: map high-level allocation and security properties onto processor primitives (eg. CHERI… | ||
| nothing matches | ||