SearcharxivSearch

arXiv subjects

Shreyas Srinivas

Publications and source records attributed to Shreyas Srinivas.

5 recordsLinked to original sources

Experimental Verification of Fast Voltage Droop Correction Circuits

Due to the trend towards minimizing guard bands for energy saving purposes, voltage droops are a key limiting factor for the operational frequency of today's VLSI circuits. Adapting clock frequencies dynamically presents the challenge of metastability in the device that detects and stores the existence of voltage droops. We present an implementation of a fast all-digital circuit for adaptive response to droops using the IHP 130 nm process. The description of the design is presented in an accompanying paper. We experimentally validate the functionality of the design on a test chip.

cs.AR

A Counterexample to EFX $n \ge 3$ Agents, $m \ge n + 5$ Items, Submodular Valuations via SAT-Solving

The existence of EFX allocations is a central open problem in discrete fair division. An allocation is EFX (envy-free up to any good) if no agent envies another agent after the removal of any single good from the other agent's bundle. We resolve this longstanding question by providing the \textbf{first-ever counterexample} to the existence of EFX allocations for agents with monotone valuations, which in turn immediately implies a counterexample for submodular valuations. Specifically, we show that EFX allocations need not exist for instances with $n \ge 3$ agents and $m \ge n+5$ goods. In contrast, we prove that every instance with three agents and seven goods admits an EFX allocation. Both results are obtained via SAT solving. We encode the negation of EFX existence as a SAT instance: satisfiability yields a counterexample, while unsatisfiability establishes universal existence. The correctness of the encoding is formally verified in Lean. Finally, we establish positive guarantees for fair allocations with three agents and an arbitrary number of goods. Although EFX allocations may fail to exist, we prove that every instance with three agents and monotone valuations admits at least one of two natural relaxations of EFX: tEFX, or EF1 and EEFX.

cs.GT

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project successfully determined all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas, by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean. As a result of this project, several new constructions of magmas satisfying specific laws were discovered, and several auxiliary questions were also addressed, such as the effect of restricting attention to finite magmas.

math.RA

Clock Distribution with Gradient TRIX

Gradient clock synchronization (GCS) algorithms minimize the worst-case clock offset between the nodes in a distributed network of diameter $D$ and size $n$. They achieve optimal offsets of $Θ(\log D)$ locally, i.e. between adjacent nodes as shown by Lenzen et al., and $Θ(D)$ globally as shown by Biaz and Welch. As demonstrated in the work of Bund et al., this is a highly promising approach for improved clocking schemes for large-scale synchronous Systems-on-Chip (SoC). Unfortunately, in large systems, faults hinder their practical use. State of the art fault-tolerant, as presented by Bund et al., has a drawback that is fatal in this setting: It relies on node and edge replication. For $f=1$, this translates to at least $16$-fold edge replication and high degree nodes, far from the optimum of $2f+1=3$ for tolerating up to $f$ faulty neighbors. In this work, we present a self-stabilizing GCS algorithm for a grid-like directed graph with optimal node in- and out-degrees of $3$ that tolerates $1$ faulty in-neighbor. If nodes fail with independent probability $p\in o(n^{-1/2})$, it achieves asymptotically optimal local skew of $Θ(\log D)$ with probability $1-o(1)$; this holds under general worst-case assumptions on link delay and clock speed variations, provided they change slowly relative to the speed of the system. The failure probability is the largest possible ensuring that with probabity $1-o(1)$ for each node at most one in-neighbor fails. As modern hardware is clocked at gigahertz speeds and the algorithm can simultaneously sustain a constant number of arbitrary changes due to faults in each clock cycle, this results in sufficient robustness to dramatically increase the size of reliable synchronously clocked SoCs.

cs.DC

Latch Based Design for Fast Voltage Droop Response

We present a latch-based and PLL-free design of the voltage droop correction circuit of Lenzen, Fuegger, Kinali, and Wiederhake\cite{DroopJournal}. Such a circuit dynamically modifies the clock frequency of a digital clock for VLSI systems. Our circuit responds within two clock cycles and halves the length of the synchroniser chain compared to the previous design. Further, we introduce a differential sensor based design for masking latches as a replacement for masking flip flops that the design of \cite{DroopJournal} requires, but leaves unspecified. The use of latches instead of threshold-altered flip flops alters the timing properties of our design and thus the proofs of correctness that accompanied their design require modifications which we present here. This design has been successfully implemented on the IHP 130 nm process technology. The results of the experimental measurements will be discussed in a subsequent publication.

cs.AR