Anton 3 is the newest member in a family of supercomputers specially designed for atomic-level simulation of molecules relevant to biology (e.g., DNA, proteins, and drug molecules). Anton 3 achieves order-of-magnitude improvements in time-to-solution ...

Anton 2 is a second-generation special-purpose supercomputer for molecular dynamics simulations that achieves significant gains in performance, programmability, and capacity compared to its predecessor, Anton 1. The architecture of Anton 2 is tailored ...

Exploiting parallelism to accelerate a computation typically involves dividing it into many small tasks that can be assigned to different processing elements. An efficient execution schedule for these tasks can be difficult or impossible to determine in ...

The ability to perform long, accurate molecular dynamics (MD) simulations involving proteins and other biological macro-molecules could in principle provide answers to some of the most important currently outstanding questions in the fields of biology, ...

Design verification of complex digital circuits typically starts only after the register-transfer level (RTL) description is complete. This frequently makes verification more difficult than necessary because logic that is intrinsically hard to verify, ...

The ability to perform long, accurate molecular dynamics (MD) simulations involving proteins and other biological macro-molecules could in principle provide answers to some of the most important currently outstanding questions in the fields of biology, ...

This special issue is based on innovative ideas presented and discussed during the first International Workshop on Formal Methods for Globally Asynchronous and Locally Synchronous Systems (FMGALS) held in conjunction with the Formal Methods in Europe (...

This paper presents a procedure for the verification of multi-process systems based on considering a series of underapproximated models. The procedure checks models with an increasing set of allowed interleavings of the given set of processes, starting ...

Latency-insensitive systems were recently proposed by Carloni et al. as a correct-by-construction methodology for single-clock system-on-a-chip (SoC) design using predesigned IP blocks. Their approach overcomes the problem of long latencies of global ...

This paper introduces a new method for two-level logic minimization. Unlike previous approaches, the new method uses a SAT solver as an underlying engine. While the overall minimization strategy of the new method is based on the operators as defined in ...

Hybrid dynamic systems include both continuous and discrete state variables. Properties of hybrid systems, which have an infinite state space, can often be verified using ordinary model checking together with a finite-state abstraction. Model checking ...

Asynchronous (or “clock-less”) digital circuit design has received much attention over the past few years, including its introduction into consumer products. One major bottleneck to the further advancement of clock-less design is the lack of optimizing ...

Asynchronous design has been the focus of renewed interest. However, a key bottleneck is the lack of high-quality CAD tools for the synthesis of large-scale systems which also allow design-space exploration. This paper proposes a new synthesis method ...

Integer addition is one of the most important operations in digital computer systems because the performance of processors is significantly influenced by the speed of their adders. This paper proposes a self-timed carry-lookahead adder in which the ...

None of the available minimizers for exact 2-level hazard-free logic minimization can synthesize very large circuits. This limitation has forced researchers to resort to heuristic minimization, or to manual and automated circuit partitioning techniques. ...

Ordered Decision Diagrams (ODDs) as a means for the representation of Boolean functions are used in many applications in CAD. Depending on the decomposition type, various classes of ODDs have been defined, among them being the Ordered Binary Decision ...

Integer addition is one of the mast important operations in digital computer systems because the performance of processors is significantly influenced by the speed of their adders. This paper proposes a delay insensitive, carry-lookahead adder in which ...

We present methods to minimize fixed polarity Reed-Muller expressions (FPRMs), i.e., two-level fixed polarity AND/EXOR canonical representations of Boolean functions, using ordered functional decision diagrams (OFDDs). We investigate the close relation ...