Design with race-free hardware semantics

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-state-machines 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