BSV by Example - The next-generation language for electronic system design


  BSV by Example.pdf (Size: 1.23 MB / Downloads: 0)

Introduction

BSV (Bluespec SystemVerilog) is a language used in the design of electronic systems (ASICs, FPGAs
and systems). BSV is used across the spectrum of applications|processors, memory subsystems,
interconnects, DMAs and data movers, multimedia and communication I/O devices, multimedia and
communication codecs and processors, signal processing accelerators, high-performance computing
accelerators, etc. BSV is also used across markets|from low-power, portable consumer items to
enterprise-class server-room systems.
Being both a very high-level language as well as fully synthesizable to hardware, it is used in many
design activities, as described below. This combination of high level and full synthesizability enables
many of these activities that were previously only done in software simulation now to be moved
easily to FPGA-based execution (whether the design is eventually bound for ASICs or FPGAs).
This can speed up execution by three to six orders of magnitude (1000x to 1,000,000x). Such
a dramatic speedup not only accelerates existing activities, but enables new activities that were
simply not feasible before (such as cycle-accurate multi-core processor architecture models running
real operating systems and real applications).

Design activities where BSV is used

Executable Specications (synthesizable). For today's complex systems, a specication written in
a human language (like English) is likely to be imprecise, incomplete or even infeasible and self-
contradictory in its requirements. A specication in BSV addresses these concerns, because of its
precise semantics and executability on real data. Fleshing out a spec in this way is also called spec
validation.
Virtual Platforms (synthesizable). Today's chips are dominated by the volume and complexity of
the software that runs on them. It is no longer acceptable to have to wait for chips to be available
before developing software. Virtual Platforms enable software development and testing to begin as
early as day one.

Key ideas in BSV

BSV borrows powerful ideas that have been developed over several decades in advanced formal
specication and programming languages. These can be classied into two groups|behavior and
structure.

Behavior

BSV's behavioral model is popular among formal specication languages for complex concurrent
systems. We call them Atomic Rules and Interfaces, but in the literature they also go by various
names such as Term Rewriting Systems, Guarded Atomic Actions, and Rewrite Rules. Well-known
formal specication languages that use a similar model include Guarded Commands (Dijkstra);
TLA+ (Lamport); UNITY (Chandy and Mishra); and Z, B and EventB (Abrial).
The reasons BSV and all these formal specication languages choose this model are:
 Parallelism: The model of atomic rules is fundamentally parallel, unlike many other approaches
that graft a parallel extension on top of a sequential language (such as those based on C++).
This is ideally suited for the massive, ne-grain, heterogeneous parallelism that is everywhere
in complex hardware designs and distributed systems.
 Correctness: The atomicity of rules is a powerful tool in thinking about correct behavior
in the presence of complex parallelism. A key concept in correct systems is the invariant,
which represents a correctness condition that one expects to be maintained in a system (such
as, \A cache line can be in the DIRTY state in only one of the multiple caches", or \The
counter in the DMA is equal to the number of bytes transferred"). Atomicity of rules allows
reasoning about invariants one rule at-at-time. Without atomicity, one has to worry about all
possible interleavings of parallel activities, an exercise that quickly becomes too complex both
for humans and for formal verication systems.