Harmonic's Aristotle adds multi-clock domains, latches and clock gating support

satnam6502 · x · 2026-11-13

Harmonic announced that its formal verification engine Aristotle now supports multiple clock domains, latches, and clock gating, dropping its previous single-ungated-clock restriction. Large designs run on different clocks and exchange data asynchronously, while clock gates built with latches save power; Aristotle can now verify such designs with clocking logic faithfully modeled. The blog demonstrates the features with an asynchronous FIFO using Gray-coded pointers, proving no overflow/underflow, correct data return, and eventual visibility of queued data — all properties proved in 20 minutes — before introducing two bugs to show debugging workflows.

Original post →

Harmonic's Aristotle adds multi-clock domains, latches and clock gating support

More from Infra