skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Modular Hardware Design with Timeline Types
Modular design is a key challenge for enabling large-scale reuse of hardware modules. Unlike software, however, hardware designs correspond to physical circuits and inherit constraints from them. Timing constraints—which cycle a signal arrives, when an input is read—and structural constraints—how often a multiplier accepts new inputs—are fundamental to hardware interfaces. Existing hardware design languages do not provide a way to encode these constraints; a user must read documentation, build scripts, or in the worst case, a module’s implementation to understand how to use it. We present Filament, a language for modular hardware design that supports the specification and enforcement of timing and structural constraints for statically scheduled pipelines. Filament usestimeline types, which describe the intervals of clock-cycle time when a given signal is available or required. Filament enablessafe compositionof hardware modules, ensures that the resulting designs are correctly pipelined, and predictably lowers them to efficient hardware.  more » « less
Award ID(s):
1845952 2124045 1909073
PAR ID:
10603057
Author(s) / Creator(s):
 ;  ;  
Publisher / Repository:
Association for Computing Machinery (ACM)
Date Published:
Journal Name:
Proceedings of the ACM on Programming Languages
Volume:
7
Issue:
PLDI
ISSN:
2475-1421
Format(s):
Medium: X Size: p. 343-367
Size(s):
p. 343-367
Sponsoring Org:
National Science Foundation
More Like this
  1. This paper examines a family of designs for magnetic cubes and counts how many configurations are possible for each design as a function of the number of modules. Magnetic modular cubes are cubes with magnets arranged on their faces. The magnets are positioned so that each face has either magnetic south or north pole outward. Moreover, we require that the net magnetic moment of the cube passes through the center of opposing faces. These magnetic arrangements enable coupling when cube faces with opposite polarity are brought in close proximity and enable moving the cubes by controlling the orientation of a global magnetic field. This paper investigates the 2D and 3D shapes that can be constructed by magnetic modular cubes, and describes all possible magnet arrangements that obey these rules. We select ten magnetic arrangements and assign a "color" to each of them for ease of visualization and reference. We provide a method to enumerate the number of unique polyominoes and polycubes that can be constructed from a given set of colored cubes. We use this method to enumerate all arrangements for up to 20 modules in 2D and 16 modules in 3D. We provide a motion planner for 2D assembly and through simulations compare which arrangements require fewer movements to generate and which arrangements are more common. Hardware demonstrations explore the self-assembly and disassembly of these modules in 2D and 3D. 
    more » « less
  2. K2 is a new architecture and verification approach for hardware security modules (HSMs). The K2 architecture's rigid separation between I/O, storage, and computation over secret state enables modular proofs and allows for software development and verification independent of hardware development and verification while still providing correctness and security guarantees about the composed system. For a key step of verification, K2 introduces a new tool called Chroniton that automatically proves timing properties of software running on a particular hardware implementation, ensuring the lack of timing side channels at a cycle-accurate level. 
    more » « less
  3. null (Ed.)
    RNA origami is a framework for the modular design of nanoscaffolds that can be folded from a single strand of RNA and used to organize molecular components with nanoscale precision. The design of genetically expressible RNA origami, which must fold cotranscriptionally, requires modelling and design tools that simultaneously consider thermodynamics, the folding pathway, sequence constraints and pseudoknot optimization. Here, we describe RNA Origami Automated Design software (ROAD), which builds origami models from a library of structural modules, identifies potential folding barriers and designs optimized sequences. Using ROAD, we extend the scale and functional diversity of RNA scaffolds, creating 32 designs of up to 2,360 nucleotides, five that scaffold two proteins, and seven that scaffold two small molecules at precise distances. Micrographic and chromatographic comparisons of optimized and non-optimized structures validate that our principles for strand routing and sequence design substantially improve yield. By providing efficient design of RNA origami, ROAD may simplify the construction of custom RNA scaffolds for nanomedicine and synthetic biology. 
    more » « less
  4. Abstract The high-luminosity upgrade of the LHC brings unprecedented requirements for real-time and precision bunch-by-bunch online luminosity measurement and beam-induced background monitoring. A key component of the CMS Beam Radiation, Instrumentation and Luminosity system is a stand-alone luminometer, the Fast Beam Condition Monitor (FBCM), which is fully independent from the CMS central trigger and data acquisition services and able to operate at all times with a triggerless readout. FBCM utilizes a dedicated front-end application-specific integrated circuit (ASIC) to amplify the signals from CO2-cooled silicon-pad sensors with a timing resolution of a few nanoseconds, which enables the measurement of the beam-induced background. FBCM uses a modular design with two half-disks of twelve modules at each end of CMS, with four service modules placed close to the outer edge to reduce radiation-induced aging. The electronics system design adapts several components from the CMS Tracker for power, control and read-out functionalities. The dedicated FBCM23 ASIC contains six channels and adjustable shaping time to optimize the noise with regards to sensor leakage current. Each ASIC channel outputs a single binary high-speed asynchronous signal carrying time-of-arrival and time-over-threshold information. The chip output signal is digitized,encoded, and sent via a radiation-hard gigabit transceiverand an optical link to the back-end electronics for analysis. This paper reports on the updated design of the FBCM detector and the ongoing testing program. 
    more » « less
  5. Nadel, Alexander; Rozier, Kristin Yvonne (Ed.)
    Symbolic execution is a powerful verification tool for hardware designs, in particular for security validation. However, symbolic execution suffers from the path explosion problem in which the number of paths to explore grows exponentially with the number of branches in the design. We introduce a new approach, piecewise composition, which leverages the modular structure of hardware to transfer the work of path exploration to SMT solvers. Piecewise composition works by recognizing that independent parts of a design can each be explored once, and the exploration reused. A hardware design with N independent always blocks and at most b branch points per block will require exploration of O((2^b)N) paths in a single clock cycle with our approach compared to O(2^(bN)) paths using traditional symbolic execution. We present Sylvia, a symbolic execution engine implementing piecewise composition. The engine operates directly over RTL without requiring translation to a netlist or software simulation. We evaluate our tool on multiple open-source SoC and CPU designs, including the OR1200 and PULPissimo RISC-V SoC. The piecewise composition technique reduces the number of paths explored by an order of magnitude and reduces the runtime by 97% compared to our baseline. Using 84 properties from the security literature we find assertion violations in open-source designs that traditional model checking and formal verification tools do not find. 
    more » « less