Most hardware description languages do not enforce determinacy, meaning that they may yield races. Race conditions pose a problem for the implementation, verification, and validation of hardware. Enforcing determinacy at the modeling level provides a solution to this problem. In this paper, we consider a common model of computation for hardware modeling — a network of cycle-true finite-statemachines with datapaths (FSMDs) — and we identify the conditions under which such models are guaranteed to be race-free. We base our analysis on the Kahn Principle and a formal framework to represent FSMD semantics. We present our conclusions as four simple and easy to enforce modeling rules. A hardware designer that applies those four modeling rules, will thus obtain race-free hardware. 1 Motivation In traditional HDL semantics (VHDL, Verilog or SystemC), race conditions occur when a single global variable is concurrently assigned by different processes. The value stored in the global variable...
Patrick Schaumont, Sandeep K. Shukla, Ingrid Verba