From Formal Specifications to Simulations: Generating Executable Hardware Models for Early Validation

Abstract Formal specification techniques have been introduced to address the ambiguities inherent in natural-language hardware specifications. One such approach is the Universal Specification Format (USF), which provides a machine-readable, formal reference for Register-Transfer Level (RTL) verification. However, verifying against USF requires that the specification itself is functionally correct, which is typically assessed through use-case simulation. To this end, we present a model-driven code generator transforming static USF specifications into executable software simulations that abstract cycle-accurate timing. These simulations express hardware behavior by reordering state updates and employing event-based statements that mirror handshake protocols at the component interface. Additionally, the simulations incorporate automated activity checks that can detect specification gaps at runtime, thereby reducing manual validation effort. We evaluate the approach on hardware components spanning functional units, peripheral devices, and a RISC-V core, demonstrating the versatility of the simulation method and reusability of its generator. The simulations operate at a higher level of abstraction than RTL and, for most evaluated components, run faster than their corresponding RTL simulations. For the randomized instruction-memory workload used in the evaluation of the RISC-V model, the automatically generated functional model executes 11.0 million instructions per second without manual optimization. By providing fast, early-available simulations, our approach helps shorten validation cycles, ultimately reducing the risk of costly design flaws.