Formal semantics of BSV (Bluespec SystemVerilog), given as a Haskell Program and accompanying document
BSV is a High-level Hardware Design Language (HLHDL), taking its inspirations from Haskell and Term Rewriting Systems. A commercial implementation of BSV (a compiler from BSV into Verilog) has been available from Bluespec, Inc. (www.bluespec.com) since 2004, and has been used for several industrial-strength hardware designs. There is a growing interest in formal verification of hardware designs. BSV is attractive because of its clean semantics and formal foundations.
This repository is an independent, implementation-independent formal specification of BSV semantics. It is an executable semantics, given as a Haskell program, in the directory Haskell_code. That directory also contains several example (kernel) BSV programs, and transcripts of example runs through the semantic function. It is a dynamic semantics, describing direct execution of the abstract syntax of a (parsed) program, and thus takes no position on pre-computation of rule schedules; it just describes correct execution of any given rule schedule.
All of this is explained in detail in the accompanying document: Paper/BSV_Semantics.pdf