Hi, Haskell has a rich history of embedded hardware description languages. Here's one more for the list. Inspired by the work of Arvind, Hoe, and all the sharp folks at Bluespec, Atom is a small HDL that compiles conditional term rewriting systems down to Verilog RTL. In Atom, a circuit description is composed of a set of state elements (registers) and a set of rules. Each rule has two components: an enabling condition and a collection of actions, or state updates. When a rule is enabled, it's actions may be selected to execute atomically. In contrast to Verilog "always" blocks, multiple rules can write to the same state element. Here's an enabled counter in Atom: counter :: Int -> Signal -> System Signal counter width enable = do count <- reg "count" width 0 rule "updateCount" $ do when enable count <== value count +. one width return $ value count Enjoy! http://funhdl.org/ -Tom A few details: The Atom compiler attempts to maximize the number of rules that can execute in a given clock cycle without breaking the semantics of "one-rule-at-a-time". For simplicity, rules are assigned a global, linear priority. Data dependencies between rules form a graph. A acyclic graph is ideal, because all rules become "sequentially composable". The compiler attempts to order the rules to minimize the number of edges feeding back from lower to higher priority rules. This is equivalent to the feedback arc set problem. (Atom's FAS optimization is pretty poor at the moment.) In a rule-data dependency graph, many of the edges are irrelevent because pairs of rules are often mutually exclusive, ie. can not be enabled at the same time. MiniSat is used to hunt and prune edges from mutually exclusive rules. By only looking back to primary inputs and registers, the SAT procedure is not guaranteed to find all mutually exclusive rules, but it does a pretty good job.