這篇介紹Bluespec以及設計示例的文章，是在2021年ICCAD（International Conference On Computer-Aided Design）發佈的論文。達坦科技的open-rdma項目和推廣的MIT體系結構學習社區都用到Bluespec，因此將此論文翻譯成中文，以便大家瞭解2020年Bluespec開源後相關的開源項目。

摘要：bsc編譯器是一個商業可用的編譯器，在過去的二十年中被廣泛使用，於2020年1月作為免費開源工具發佈。本文簡要介紹了bsc及其流程，提供了可用的教程材料，並介紹了多個可重用的開源設計案例，其中許多設計聚焦在RISC-V上（覆蓋了從嵌入式到支持Linux的CPU和系統），所有設計均可部署在FPGA上。

I. 引言

自2000年以來，bsc編譯器及其庫就一直在作為一款商業軟件被開發。二十餘年來，它曾是Bluespec公司的一款授權產品，儘管學術和研究許可證一直以來都是免費提供的。幾家頂級半導體供應商和一家主要的搜索公司曾使用bsc來設計最新ASIC SoCs中複雜的IP。它被許多公司用於基於FPGA的原型開發，並且在許多大學裏用於構建體系結構和複雜IP的研究。

2020年1月，Bluespec公司以BSD 3-Clause許可證的形式免費開源了編譯器、庫以及一個圖形用户界面。這些可以在以下網址找到：

https://github.com/B-Lang-org/bsc

https://github.com/B-Lang-org/bsc-contrib

https://github.com/B-Lang-org/bdw。

bsc編譯器接受以高級硬件描述語言BSV和BH（如下所述）編寫的設計作為輸入，並生成可用於標準RTL工具（仿真、綜合、形式分析等）處理的Verilog代碼。

本文將簡要介紹BSV和BH、bsc及其流程，以及使用BSV/BH編寫的幾個免費開源設計。其中，許多設計都是RISC-V設計（包括CPU、IP和系統），並且這些設計都是高度可複用的，並可在FPGA上運行。

II. BSV和BH高級硬件設計語言的背景

BSV和BH起源於20世紀90年代在麻省理工學院的研究中[10]，當時James Hoe和Arvind確認了將併發原子事務表達的行為編譯高質量Verilog的可行性。這是很有吸引力的，因為它給對複雜併發系統進行形式化規範説明和分析的行為模型（例如，TLA+ [11]，Event-B [12]，UNITY [7]）提供了一種選擇。由於能夠將這樣的形式化規範説明編譯成高質量的硬件，它可以成為自動化實現形式規範説明到實際硬件之間的橋樑。

啓用組合形式驗證一直是BSV/BH的核心動機和特性（例如，請參見MIT的Kami項目，網址為https://github.com/mit-plv/kami）。原子事務語義還能夠在日常的非形式化驗證中幫助工程師增強系統的正確性。

在2000年，Lennart Augustsson在一種新的語言BH（Bluespec Haskell）中實現了這些想法，該語言使用Haskell的語法和語義，包括具有多態和類型類的類型系統、單子和高階函數，從而使其具有靜態展開能力和非常強大的類型抽象和類型檢查能力[2]，[14]。

在2004-2005年，我們創建了BSV，它只是一種新的，類似於SystemVerilog的前端語法[6]，但在其他方面保留了BH的類似於Haskell的表達能力。

在2005年，我們引入了對多個時鐘和復位域的支持。強類型檢查確保不可能將時鐘和復位信號與普通信號混合在一起。通過bsc的靜態檢查保證了正確的時鐘域規範。

A. HLS與RTL、Chisel和其他硬件描述語言的比較

BSV/BH、VHDL、Verilog、SystemVerilog和Chisel[3]都是硬件描述語言（HDL）：設計者直接描述架構和微架構。在這方面，它們與所謂的“HLS”（高級綜合）[9]完全不同，HLS工具會自動生成架構和微架構（這可能是在設計者的高級指導下進行的）。但這並不意味着HDL必須是低級的：強大的抽象和組合機制允許像描述低級微架構一樣流暢地描述高級參數化架構[14]。BSV/BH通過模仿Haskell實現了這一點，而Chisel則通過嵌入到Scala中實現了這一點。

BSV和BH與像Lava[5]這樣側重於強大的、正確的電路結構組合機制，而不關注行為的語言有所不同。與其他直接表達架構的HDL一樣，BSV/BH是通用的，不針對任何特定的應用領域。BSV/BH與所有其他HDL之間最基本、最具廣泛和最重大的區別可能在於選擇併發原子事務作為其表達行為的中心（也是唯一）方式。

III. BSV和BH設計、bsc編譯器和流程

與其他硬件描述語言（HDL）類似，BSV/BH設計是模塊實例化的層次結構，但相比其他HDL，由於受到Haskell語言語義啓發而具有更強大的靜態闡釋能力。

與其他HDL不同的是，在BSV/BH中，行為是通過規則來表示的，這些規則是全局原子事務。在其他HDL中，行為通常是通過同步時鐘過程來表示的。

與其他HDL不同的是，BSV/BH中的模塊間通信是通過從規則（或從其他方法）中調用方法的概念來表達的，而不是基於輸入和輸出信號線路來表達的。方法調用的概念將規則的原子事務語義擴展為可以跨越模塊邊界的，即當設計擴展時，原子性會進行組合。模塊的接口方法構成了一種一等公民的接口類型。

與SystemVerilog類似，模塊、接口和類型可以根據功能劃分為稱為包的源文件。bsc接受BSV或BH源文件（包）並生成可綜合的Verilog代碼，這就意味着可以直接使用現有的FPGA和ASIC綜合工具。bsc通過單獨的包編譯實現了大型系統的快速增量重建。

由bsc生成的Verilog代碼可以在大多數知名的仿真器上運行，包括開源仿真器（Icarus、Verilator、CVC等）和商業仿真器（Synopsys、Cadence、Mentor、Xilinx）。它可以由大多數著名的綜合工具（Design Compiler、Vivado、Quartus以及其他FPGA供應商的工具）進行綜合。

A. 與現有RTL和C語言的互操作性

由BSV/BH中的bsc生成的Verilog可以被實例化在現有的VHDL/Verilog/SystemVerilog模塊中。相反地，BSV/BH具有導入機制，可以在BSV/BH設計內實例化現有的Verilog模塊。因此，可以在現有的流程中自由混合和匹配BSV/BH與現有的RTL。對於仿真，BSV/BH還具有DPI機制，可以導入任意的C代碼。

B. bsc內部實現和可選的圖形用户界面

儘管BSV/BH在語義和類型方面廣泛借鑑了Haskell的思想，但它並不是現有Haskell編譯器或系統內的DSL。bsc是一個完全獨立的、專為此目的而構建的編譯器（但它恰好是用Haskell編寫的）。bsc與其他HDL編譯器（如Verilator和Chisel）的一個核心區別在於規則調度，即生成同步的，帶有時鐘和控制邏輯的verilog代碼，且這些代碼保留了原子事務行為語義。bsc使用開源SAT解算器分析規則條件之間的關係，從而產生優化的控制邏輯。

除了生成Verilog代碼外，bsc還可以生成C代碼，並將其編譯為獨立的可執行仿真器（Bluesim），它與RTL仿真可以達到時鐘週期級別的完全一致，並能夠生成VCD文件。

可以使用API中查詢和控制編譯器生成的中間對象文件。這個API有一個Tcl的Binding實現（bluetcl）；實際上，Bluesim也只是一個Tcl腳本，這個腳本封裝並在內部利用了這些API。

儘管所有BSV/BH的開發都可以通過命令行完成，但Bluespec開發工作站（BDW）（https://github.com/B-Lang-org/bdw）提供了一個GUI界面，用户可以從中探索源代碼層次結構，進行編譯、構建和運行模擬，並在外部的VCD查看器（如GtkWave）上觀察波形。BDW可以配置GtkWave以顯示BSV源代碼級別的波形類型（枚舉、結構體、聯合體、向量），而不是Verilog的扁平信號總線。BDW還提供了規則調度的圖形顯示，以幫助理解bsc如何將原子事務規則映射到時鐘邏輯中。

IV. 教程和書籍

有多種免費和開源的教程資源可供學習BSV/BH和使用相關工具。https://github.com/BSVLang/Main包含了Bluespec公司提供的BSV/BH免費開放培訓課程，以及BSV by Example書籍的免費PDF副本 [15]。在參考文獻[16]中，我們提供了"使用開源BH設計硬件系統和加速器"這個教程的教材鏈接和視頻錄像。此教程是在2020年國際函數式編程大會上進行的。麻省理工學院（美國）、卡內基梅隆大學（美國）、劍橋大學（英國）、首爾國立大學（韓國）、印度馬德拉斯理工學院（印度）和達姆施塔特工業大學（德國）多年來一直在本科和研究生課程中使用BSV進行教學；其中一些教材可以在他們各自的公共網站上獲取。在接下來的章節中列出的開源設計也是學習BSV/BH的豐富示例資源。

V. BSV和BH示例設計

多年來，許多公司都在產品ASIC SoCs中使用BSV和BH來開發複雜的IP子系統。這些包括用於機頂盒的一對多高速視頻數據傳輸器，用於手持設備的顯示控制器以及AI芯片加速器。許多公司利用BSV強大的抽象機制和類型系統，加速在FPGA上的原型設計以及後續的ASIC設計。雖然這些示例展示了BSV/BH和bsc的強大、可擴展和成熟性，但它們並不以開源的形式提供。

然而，Bluespec公司和一些領先的大學提供了許多采用自由開源許可的設計；下面介紹其中的一些樣例。其中大多數設計都相當龐大，並且可能非常具有吸引力。儘管這些設計是用BSV編寫的，但bsc可以將它們編譯成Verilog，並且它們可以作為IP在其他採用RTL設計的項目中使用（參見上文的"互操作性"）。

A. 開源RISC-V處理器（Bluespec, Inc.）

Bluespec公司開源了一系列的RISC-V處理器設計，從非常小型的（用於嵌入式和微控制器應用）到非常大型和複雜的。它們都可以在https://github.com/bluespec下面的Apache License, Version 2.0下獲取。

• Piccolo: 3級順序流水線，獨立的I和D通道。
• Flute: 5級順序流水線，具有分支預測，獨立的I和D通道。
• Toooba: MIT的RISCY-OOO中的一個軟件包[20]：亂序執行，超標量，深度流水線，分支預測，獨立的具備緩存一致性的I和D通道，多核，緩存一致性。

Piccolo和Flute可以參數化為構建標準的RISC-V非特權ISA選項的任意組合：RV32或RV64，I（整數），M（整數乘法/除法），A（原子操作），C（16位壓縮指令）和FD（單精度和雙精度IEEE浮點）。它們還可以選擇為特權ISA級別M（機器），S（監管者）和U（用户）進行配置。對於S，它們支持標準的Sv32和Sv39虛擬內存方案。因此，它們都支持Linux。此外，這些處理器可以參數化為由簡單到複雜的一系列不同內存系統實現：TCM（緊密耦合內存），僅L1（寫回或寫直通），以及具有緩存一致性的I-L1 + D-L1 + 共享L2。

Toooba中的MIT RISCY-OOO處理器可以根據核心數量、超標量性、投機程度、重排序緩衝區和分支預測的大小和組織形式、MMU和緩存的大小及其組織形式等進行參數化。

B. RISC-V系統的開源IP（Bluespec，Inc.）

以下IP可以在https://github.com/bluespec下面的Apache License, Version 2.0下獲取：

• 調試模塊：與RISC-V處理器相鄰的符合RISC-V規範的硬件模塊，用於遠程GDB控制。
• PLIC（平台級中斷控制器）：符合RISC-V規範的中斷控制器，用於將外部設備的中斷分配給一個或多個RISC-V核心。
• AXI4和AXI4 Lite接口的實現，以及它們的互聯實現。
• 前面部分描述的內存系統（緊密耦合內存，帶或不帶緩存一致性的L1和L2緩存）也可以作為其他RISC-V設計中的IP進行重用。

C. AWSteria用於主機+FPGA系統的 Infra和Connectal

AWSteria Infra是一個使用BSV編寫的系統，用於簡化由主機計算機上的軟件與FPGA上的硬件進行通信的應用程序的設計。圖1顯示了AWSteria Infra和一個應用程序的結構。主機上的C代碼和FPGA上的BSV代碼為應用程序提供了簡單的接口（AXI4和AXI4 Lite）。FPGA上的BSV代碼還提供了對FPGA板上DDR內存的簡單接口（AXI4）。這些接口類似於亞馬遜的aws-fpga開發工具包中提供的所謂“shell”，但可用於更廣泛的平台。

AWSteria Infra實現可用於RTL模擬（使用TCP/IP進行通信），以及用於Xilinx VCU118和AWS F1 FPGA系統（兩者都使用PCIe進行通信）。未來將支持更多平台。它可在Apache License 2.0下的https://github.com/bluespec/AWSteriaInfra獲取。

Connectal也是使用BSV編寫的，具有相同的整體目標，但提供了主機-FPGA通信的“遠程方法”模型，可在雙向上進行通信。它支持更廣泛的平台，可在 MIT 許可下從https://github.com/cambridgehackers/connectal獲取。

D. AWSteria-RISCV-Virtio (Bluespec, Inc.)

AWSteria-RISCV-Virtio是在FPGA上運行的RISC-V系統，可以啓動多用户FreeBSD（它也支持Linux，但尚未測試）。它可以訪問網絡和塊存儲設備，甚至在沒有（可訪問的）內置網絡或存儲設備的雲FPGA板上也可以做到這一點。它使用了一種名為"Virtio"的開放標準[18]，該標準最初用於虛擬化領域，旨在為橫跨多個主機的虛擬機監視器的客户操作系統提供可移植的設備服務。

圖2顯示了AWSteria-RISCV-Virtio中的組件。FPGA端是一個帶有BSV CPU（Flute, Toooba）、調試模塊、PLIC、DDR內存、UART和用於Virtio的MMIO-to-host系統。主機端代碼為RISC-V CPU提供了控制枱TTY I/O、RISC-V CPU的GDB控制以及向RISC-V CPU上的操作系統提供Virtio設備服務（網絡、塊存儲等）。主機端的Virtio設備由TinyEMU提供，這是Fabrice Bellard的用於RISC-V的開源系統仿真器[4]（一個較小且較簡單的版本的QEMU）。主機可以對FPGA DDR進行具有高速緩存一致性的訪問，這是Virtio所需的。

該系統構建在AWSteria Infra（第V-C節）之上，因此可以直接在任何受支持的平台上使用（當前支持RTL仿真、亞馬遜AWS F1和Xilinx VCU118板）。AWSteria-RISCV-Virtio可在https://github.com/GaloisInc/BESSPIN-CloudGFE/tree/rsn3/AWSteriaRISCV Virtio獲取（將很快移至https://github.com/GaloisInc/BESSPIN-CloudGFE）。

E. 安全RISC-V (劍橋大學)

劍橋大學多年來一直在研究CHERI：能力型硬件增強的RISC指令。指令和內存系統被增強為具有“能力”，以實現安全計算，即消除傳統設計中的安全漏洞[19]。這些設計是用BSV編寫的，可在https://github.com/CTSRD-CHERI獲得，採用基於Apache License 2.0的許可證。

F. Shakti RISC-V 處理器(馬德拉斯理工學院)

印度理工學院馬德拉斯分校的Shakti計劃正在構建一系列基於RISC-V的生產級處理器、SoCs、開發板和軟件平台。這些處理器和SoCs是使用BSV語言編寫的，並可在https://gitlab.com/shaktiproject上根據BSD 3-Clause許可證進行獲取。

G. 片上網絡生成器（卡內基梅隆大學）

CMU的Papamichael和Hoe開發了CONNECT，這是一個適用於FPGA的任意拓撲結構的多節點NoC（片上網絡）生成器[17]。CONNECT是他們在MEMOCODE 2011硬件/軟件協同設計競賽中獲獎作品的基礎。最近，CONNECT已以BSD 3-Clause許可證的形式在https://github.com/crossroadsfpga/connect上開源。

H. BlueCheck 通用硬件測試平台 (劍橋大學)

BlueCheck是在BSV中實現的Haskell的QuickCheck [8]，利用BSV包含的與QuickCheck使用相同的Haskell特性：多態類型和類型類、單子和高階函數。就像QuickCheck一樣，它具有以下特點：

• 從接口類型自動生成測試序列，支持覆蓋默認值；
• 迭代加深：生成更長的測試序列；
• 收縮：在找到失敗時自動縮短測試序列；
• 完全可綜合化（以BSV編寫）：Trstbench可以在FPGA上以DUT的速度運行。它可在https://github.com/CTSRD-CHERI/bluecheck上獲取，遵循BERI硬件-軟件許可證第1.0版。

原文鏈接：

https://woset-workshop.github.io/PDFs/2021/a02.pdf

往期回顧

MIT體系結構公開課學習社區2.0版正式上線啦～

開源芯片社區雙週報 No.6

達坦科技（DatenLord）專注下一代雲計算——“天空計算”的基礎設施技術，致力於拓寬雲計算的邊界。達坦科技打造的新一代開源跨雲存儲平台DatenLord，通過軟硬件深度融合的方式打通雲間壁壘，實現數據高效跨雲訪問，建立海量異地、異構數據的統一存儲訪問機制，為雲上應用提供高性能安全存儲支持。以滿足不同行業客户對海量數據跨雲、跨數據中心高性能訪問的需求。

公眾號：達坦科技DatenLord

DatenLord官網：

https://datenlord.github.io/zh-cn/

知乎賬號：

https://www.zhihu.com/org/da-tan-ke-ji

B站：

https://space.bilibili.com/2017027518

郵箱：info@datenlord.com