From 0a1612699cb7c559b504a80addb676a15d6ee0bb Mon Sep 17 00:00:00 2001 From: Sukhman Kahlon Date: Fri, 15 Aug 2025 15:08:13 -0700 Subject: [PATCH 01/29] copilot: Add hello world example for FPGA. Refs #657. We need an example that demonstrates how to work with FPGAs using Copilot. This will help users start with copilot-bluespec, and also help validate our work. This commit adds a hello world example that demonstrates how to control 4 LEDs from 4 switches. The tutorial describes how to install Vivado, create the spec, compile it (in bluespec and then verilog), and upload it to the board. --- .../examples/fpga/HelloWorld/HelloWorld.hs | 19 + copilot/examples/fpga/HelloWorld/README.md | 557 ++++++++++++++++++ copilot/examples/fpga/HelloWorld/Top.bs | 17 + .../examples/fpga/HelloWorld/constraints.xdc | 17 + copilot/examples/fpga/HelloWorld/mkTop.v | 75 +++ 5 files changed, 685 insertions(+) create mode 100644 copilot/examples/fpga/HelloWorld/HelloWorld.hs create mode 100644 copilot/examples/fpga/HelloWorld/README.md create mode 100644 copilot/examples/fpga/HelloWorld/Top.bs create mode 100644 copilot/examples/fpga/HelloWorld/constraints.xdc create mode 100644 copilot/examples/fpga/HelloWorld/mkTop.v diff --git a/copilot/examples/fpga/HelloWorld/HelloWorld.hs b/copilot/examples/fpga/HelloWorld/HelloWorld.hs new file mode 100644 index 000000000..c694c8f2e --- /dev/null +++ b/copilot/examples/fpga/HelloWorld/HelloWorld.hs @@ -0,0 +1,19 @@ +module Main where + +import Language.Copilot +import Copilot.Compile.Bluespec + +-- Define switches input +sw :: Stream Word8 +sw = extern "sw" Nothing + +-- Define LEDS output +leds :: Stream Word8 +leds = sw + +spec = do + trigger "leds" true [arg leds] + +main = do + spec' <- reify spec + compile "HelloWorld" spec' diff --git a/copilot/examples/fpga/HelloWorld/README.md b/copilot/examples/fpga/HelloWorld/README.md new file mode 100644 index 000000000..78ecd1aa8 --- /dev/null +++ b/copilot/examples/fpga/HelloWorld/README.md @@ -0,0 +1,557 @@ +# Hello World Example on an FPGA Board + +Copilot is a programming language for hard real-time systems. + +This tutorial shows how to use Copilot to control LEDs from hardware switches. +The demonstration serves as an introduction of the complete toolchain needed to +integrate Copilot into hardware projects. The specification is verified via the +onboard LEDs on an Artix-7 XC7A35T FPGA, using AMD/Xilinx Vivado Design Suite. + +This page lists all the necessary applications and auxiliary files required to +run Copilot onto an FPGA. Specifically, this page shows: + +- How to install the necessary dependencies. +- How to create Copilot code that invokes the Bluespec backend. +- How to compile the Bluespec files into Verilog. +- How to run and test the design on an FPGA board. + +## Table of Contents + +- [Installation](#installation) +- [Example](#example) + - [Hello World Code](#hello-world-code) + - [Compiling Copilot into Bluespec](#compiling-copilot-into-bluespec) + - [Compiling Bluespec to Verilog](#compiling-bluespec-to-verilog) +- [Running the Hello World Example on Vivado](#running-the-hello-world-example-on-vivado) +- [Acknowledgements](#acknowledgments) + +# Installation +[(Back to top)](#table-of-contents) + +## Vivado 2025.1 + +Vivado can be installed through terminal as suggested by the following process. +The steps provided are for a Vivado version that is ~50 GB less than the one +directly available on the AMD website. If issues arise, see the official +[Vivado +documentation](https://docs.amd.com/r/en-US/ug910-vivado-getting-started/Installing-the-Vivado-Design-Suite) +for an alternative installation method. + +1. Create an account on the +[AMD](https://www.amd.com/en/registration/create-account.html) website, which +allows downloading the Vivado Design Suite. + +2. Download the [Vivado +Edition 2025.1](https://www.xilinx.com/member/forms/download) +specific for your device and verify the information required by AMD. + +3. Open the command terminal, navigate to the directory containing the + downloaded Vivado installation file, and adjust the permissions of the file + so that it can be executed: + + ```sh + $ chmod a+x FPGAs_AdaptiveSoCs_Unified_SDI_2025.1_0530_0145_.bin + ``` + Replace `` with your operating system. + +4. Run the installation program: + + ```sh + $ ./FPGAs_AdaptiveSoCs_Unified_SDI_2025.1_0530_0145_.bin + ``` + +5. An installation window will pop up. Follow the installation prompt. When + the window *Select Product to Install* is shown, select the product + *Vivado*. Then, select the *Vivado ML Standard* edition from the two + options. In the *Vivado ML Standard* window, in the subcategory *Devices*, + select the FPGA board that you're working with (in our case the *7 Series*). + Hit *install* when prompted. The download should be ~20 GB to 50 GB. + +6. Ensure that the directory where you choose to install Vivado has + read/write permissions. If the candidate installation + directory is highlighted red, it means it has the wrong permissions and/or + owner. If that happens, change the owner into a different user, or try to + run the binary installer as sudo (root) by running the command: + ```sh + $ sudo ./FPGAs_AdaptiveSoCs_Unified_SDI_2025.1_0530_0145_.bin + ``` + + The rest of the instructions assume you have installed Vivado under + `/tools`. Adjust paths accordingly as needed. + +7. Install the drivers with: + + ```sh + $ source /tools/Xilinx/2025.1/Vivado/.settings64-Vivado.sh + $ sudo /tools/Xilinx/2025.1/data/xicom/cable_drivers//install_script/install_drivers/install_drivers + ``` + + The terminal should show a message indicating that the drivers were + installed successfully. A sample output is included below. Note that the + installation path may be different on your computer. + +
Terminal Output (click to expand) + + ``` + INFO: Installing cable drivers. + INFO: Script name = /tools/Xilinx/2025.1/data/xicom/cable_drivers/lin64/install_script/install_drivers/install_drivers + INFO: HostName = iron-B650M-C-V2-Y1 + INFO: RDI_BINROOT= /tools/Xilinx/2025.1/data/xicom/cable_drivers/lin64/install_script/install_drivers + INFO: Current working dir = /home/iron/Downloads + INFO: Kernel version = 6.8.0-60-generic. + INFO: Arch = x86_64. + Successfully installed Digilent Cable Drivers + --File /etc/udev/rules.d/52-xilinx-ftdi-usb.rules does not exist. + --File version of /etc/udev/rules.d/52-xilinx-ftdi-usb.rules = 0000. + --Updating rules file. + --File /etc/udev/rules.d/52-xilinx-pcusb.rules does not exist. + --File version of /etc/udev/rules.d/52-xilinx-pcusb.rules = 0000. + --Updating rules file. + + INFO: Digilent Return code = 0 + INFO: Xilinx Return code = 0 + INFO: Xilinx FTDI Return code = 0 + INFO: Return code = 0 + INFO: Driver installation successful. + CRITICAL WARNING: Cable(s) on the system must be unplugged then plugged back in order for the driver scripts to update the cables. + ``` +
+ +8. Verify that Vivado has been installed on your device by running the + following command and checking that you see version information + being printed: + + ```sh + $ vivado -version + vivado v2025.1 (64-bit) + Tool Version Limit: 2025.05 + SW Build 6140274 on Wed May 21 22:58:25 MDT 2025 + IP Build 6138677 on Thu May 22 03:10:11 MDT 2025 + SharedData Build 6139179 on Tue May 20 17:58:58 MDT 2025 + Copyright 1986-2022 Xilinx, Inc. All Rights Reserved. + Copyright 2022-2025 Advanced Micro Devices, Inc. All Rights Reserved. + ``` + +# Example + +## Hello World Code +[(Back to top)](#table-of-contents) + +This example shows how Copilot can be used to control LEDs using switches. We +use four switches and four LEDs available on the FPGA board. + +The main Copilot specification is created in a file `HelloWorld.hs`. The final +contents of that file is available in the [Copilot +repository](https://github.com/Copilot-Language/copilot/tree/master/copilot/examples/fpga/HelloWorld/HelloWorld.hs). +The same directory contains any auxiliary files needed to run the code onto an +FPGA board. + +The first definition in a Copilot specification is a module declaration, which +should always refer to the module as the `Main` module: + +```haskell +module Main where +``` + +Next, we import the main definitions of the Copilot language, as well as the +Bluespec backend: + +```haskell +import Copilot.Compile.Bluespec +import Language.Copilot +``` + +Copilot normally represents data as infinite successions of values or +*streams*. Streams whose values are provided by input devices are considered +external inputs for this specification or *externs*. Because switches are +inputs to the Copilot logic, we define the current value of the state of the +switches as an extern carrying values of typed 8-bit unsigned integer, or +`Word8`: + +```haskell +sw :: Stream Word8 +sw = extern "sw" Nothing +``` + +The four least-significant bits of the current value of `sw` represent the +current state of each of the four switches on the board, respectively. + +Next, we define the current value of the four LEDs in a similar way. To make +the state of the LEDs match that of the switches, we state that their values +are the same: + +```haskell +leds :: Stream Word8 +leds = sw +``` + +To connect the current values of the LEDs to the actual LEDs on the board, we +must communicate the current values as outputs of the specification which we do +with a *trigger*: + +```haskell +spec = do + trigger "leds" true [arg leds] +``` + +In the above trigger definition, `"leds"` is the name of the output, whereas +`leds` (without double quotes) is a Copilot stream that, at each point in time, +will contain the current values that the LEDs should have. + +We instruct Copilot to compile the file and generate Bluespec when the Copilot +spec is executed: + +```haskell +main = do + spec' <- reify spec + compile "HelloWorld" spec' +``` + +## Compiling Copilot into Bluespec +[(Back to top)](#table-of-contents) + +Copilot and Bluespec compiler must be installed on the device (see +[Copilot](https://github.com/Copilot-Language/copilot) and +[Bluespec](https://github.com/Copilot-Language/copilot-bluespec) for +installation instructions). + +In the terminal, navigate to the directory that has the `HelloWorld.hs` +example. Compile the Copilot specification into Bluespec by running: + +```shell +$ runhaskell HelloWorld.hs +``` + +This command generates three Bluespec files in the same directory: +`HelloWorld.bs`, `HelloWorldIfc.bs` and `HelloWorldTypes.bs`. These files make +up the internal logic and interface in Verilog. For reference, the expected +content of these files is included below. The specific content may change +slightly across versions of Copilot. + +
+Contents of generated Bluespec files (click to expand) + +**`HelloWorld.bs`** + +```bluespec +package HelloWorld where { +import FloatingPoint; + +import Vector; + +import HelloWorldTypes; + +import HelloWorldIfc; + +import BluespecFP; + +mkHelloWorld :: Prelude.Module HelloWorldIfc -> + Prelude.Module Prelude.Empty; +mkHelloWorld ifcMod = + module { + ifc <- ifcMod; + let { leds_0_guard :: Prelude.Bool; + leds_0_guard = Prelude.True; + leds_0_arg0 :: Prelude.UInt 8; + leds_0_arg0 = ifc.sw._read; }; + rules { + + "leds_0": when leds_0_guard ==> ifc.leds leds_0_arg0 + } + }; +} +``` + +**`HelloWorldIfc.bs`** + +```bluespec +package HelloWorldIfc where { +import FloatingPoint; + +import Vector; + +import HelloWorldTypes; + +interface HelloWorldIfc = { + leds :: Prelude.UInt 8 -> Prelude.Action; + sw :: Prelude.Reg (Prelude.UInt 8) +} +} +``` + +**`HelloWorldTypes.bs`** + +```bluespec +package HelloWorldTypes where { +import FloatingPoint; + +import Vector +} +``` +
+ +In the same directory, create a new file named `Top.bs`. This file serves as +top-level Bluespec module, connects the three generated files together and +contains the interface definitions. This file will later be compiled into +Verilog and deployed onto the FPGA. + +We define both the `helloWorldIfc` and `mkTop` modules. When `HelloWorld.bs` is +compiled, it makes `leds` an output, which translates to an *action* method in +Bluespec. Since an *action* method updates state rather than directly driving a +signal, we need a way to hold its value, so we create the register `led_reg`, +which stores the LEDs' value. The *type* of `led_reg` must match the *type* of +`leds` in `HelloWorldIfc.bs`. + +```bluespec +package Top where + + import HelloWorld + import HelloWorldIfc + import HelloWorldTypes + + helloWorldIfc :: Prelude.Module HelloWorldIfc + helloWorldIfc = + module + -- Register that connects the LEDs to values produced by Copilot + led_reg :: Prelude.Reg (Prelude.UInt 8) <- mkReg 0 + interface + leds reg = action + led_reg := reg + + mkTop :: Prelude.Module Empty + mkTop = mkHelloWorld helloWorldIfc +``` +## Compiling Bluespec to Verilog +[(Back to top)](#table-of-contents) + +We use the Bluespec compiler to generate Verilog output using the top-level +module. `mkTop` is a function in the `Top.bs` file that instantiates the +top-level module of the design. In the terminal, we run the following command: + +```shell +$ bsc -verilog -g mkTop -u Top.bs +``` + +This step generates the Verilog code that can be compiled to run onto the FPGA +board. We can ignore the warnings shown in terminal output, but we must ensure +that the file `mkTop.v` is successfully created in the current directory. + +To program the code onto the FPGA, the ports declarations and assignments need +modifications. In the `Top.bs` file, the module that had the register and +interface for the LEDs and switches is defined in `helloWorldIfc`. Due to this, +when compiling into Verilog, the Top level module does not have `sw` and `leds` +defined in its port declaration. This has to be modified manually. + +The following `mkTop.v` lines list the module ports in the `Top.bs` file. These +are the external signals that connect to this module: + +```verilog +module mkTop(CLK, + RST_N); + input CLK; + input RST_N; +``` + +We modify `mkTop` and add the input port `sw` and output port `leds` inside the +module port because these signals will externally connect to the FPGA. The FPGA +is limited to 4 LEDs and 4 switches. Alongside the existing definitions, we +need to *assign* the value of `ifc_led_reg$D_IN`, which is an internal wire +created by the Verilog code to the output `leds`. We *assign* the output `leds` +to the register. This register was defined in our `Top.bs` and appears as an +internal register `ifc_led_reg` and its current contents appears as the value +in `leds`. The value is updated on every rising edge of the `CLK`. + +For reference, the complete contents of the modified `mkTop.v` is included +below. + +
+Contents of modified `mkTop.v` file (click to expand) + +```verilog +// +// Generated by Bluespec Compiler, version 2025.01.1 (build 65e3a87a) +// +// Further modified by Sukhman Kahlon. +// +// On Thu Aug 14 14:52:29 PDT 2025 +// +// +// Ports: +// Name I/O size props +// CLK I 1 clock +// RST_N I 1 reset +// +// No combinational paths from inputs to outputs +// +// + +`ifdef BSV_ASSIGNMENT_DELAY +`else + `define BSV_ASSIGNMENT_DELAY +`endif + +`ifdef BSV_POSITIVE_RESET + `define BSV_RESET_VALUE 1'b1 + `define BSV_RESET_EDGE posedge +`else + `define BSV_RESET_VALUE 1'b0 + `define BSV_RESET_EDGE negedge +`endif + +module mkTop(CLK, + RST_N, + sw, + leds); + input CLK; + input RST_N; + input [3:0] sw; + output [3:0] leds; + + assign leds[3:0] = ifc_led_reg[3:0]; + + // register ifc_led_reg + reg [7 : 0] ifc_led_reg; + wire [7 : 0] ifc_led_reg$D_IN; + wire ifc_led_reg$EN; + + // register ifc_led_reg + assign ifc_led_reg$D_IN = sw[3:0]; + assign ifc_led_reg$EN = 1'd1 ; + + // handling of inlined registers + + always@(posedge CLK) + begin + if (RST_N == `BSV_RESET_VALUE) + begin + ifc_led_reg <= `BSV_ASSIGNMENT_DELAY 8'd0; + end + else + begin + if (ifc_led_reg$EN) + ifc_led_reg <= `BSV_ASSIGNMENT_DELAY ifc_led_reg$D_IN; + end + end + + // synopsys translate_off + `ifdef BSV_NO_INITIAL_BLOCKS + `else // not BSV_NO_INITIAL_BLOCKS + initial + begin + ifc_led_reg = 8'hAA; + end + `endif // BSV_NO_INITIAL_BLOCKS + // synopsys translate_on +endmodule // mkTop +``` +
+ +This code will be copied to Vivado and replace the default empty module created +by Vivado. + +To interface between the FPGA board and the code, a constraints file needs to +be created and is dependent on the type of FPGA board used. Please refer to the +reference manual for your specific FPGA board, to assign pins for LEDs +accordingly. Digilent offers I/O pins for the respective boards on the +[Digilent Github Repository](https://github.com/Digilent/digilent-xdc). + +Ensure the name of the external pins after `get_ports` matches the inputs / +outputs created in the port declaration. In this example, `CLK`, `RST_N`, +`leds`, and `sw` *must* be assigned. For reference, here is the constraints +file assigning LED 4-7 for the Arty 35T CSG324-1 to the output `leds`, and +setting the switches and period accordingly. + +
+Contents of constraints file `new_constraints.xdc` (click to expand) + +```xdc +set_property -dict { PACKAGE_PIN E3 IOSTANDARD LVCMOS33 } [get_ports CLK] +create_clock -add -name sys_clk_pin -period 10.00 -waveform {0 5} [get_ports CLK] + +set_property PACKAGE_PIN C2 [get_ports RST_N] +set_property IOSTANDARD LVCMOS33 [get_ports RST_N] + +# Switches +set_property -dict { PACKAGE_PIN A8 IOSTANDARD LVCMOS33 } [get_ports { sw[0] }]; #IO_L12N_T1_MRCC_16 Sch=sw[0] +set_property -dict { PACKAGE_PIN C11 IOSTANDARD LVCMOS33 } [get_ports { sw[1] }]; #IO_L13P_T2_MRCC_16 Sch=sw[1] +set_property -dict { PACKAGE_PIN C10 IOSTANDARD LVCMOS33 } [get_ports { sw[2] }]; #IO_L13N_T2_MRCC_16 Sch=sw[2] +set_property -dict { PACKAGE_PIN A10 IOSTANDARD LVCMOS33 } [get_ports { sw[3] }]; #IO_L14P_T2_SRCC_16 Sch=sw[3] + +# LEDs +set_property -dict { PACKAGE_PIN H5 IOSTANDARD LVCMOS33 } [get_ports { leds[0] }]; #IO_L24N_T3_35 Sch=led[4] +set_property -dict { PACKAGE_PIN J5 IOSTANDARD LVCMOS33 } [get_ports { leds[1] }]; #IO_25_35 Sch=led[5] +set_property -dict { PACKAGE_PIN T9 IOSTANDARD LVCMOS33 } [get_ports { leds[2] }]; #IO_L24P_T3_A01_D17_14 Sch=led[6] +set_property -dict { PACKAGE_PIN T10 IOSTANDARD LVCMOS33 } [get_ports { leds[3] }]; #IO_L24N_T3_A00_D16_14 Sch=led[7] +``` +
+ +# Running the Hello World Example on Vivado +[(Back to top)](#table-of-contents) + +Once installed, open the Vivado Design Suite. + +1. Click *Create Project* > *Next* > *Project Name:* `HelloWorld` and choose +the desired location. + +2. Select *Create Project Subdirectory* > *Next* > *RTL Project* > *Next*. + +3. Select *Do not specify sources at this time* > *Next*. + +4. Search for the board / chip. In this example, the board used is +`xc7a35tcsg324-1`. The project should be created and initialized. + +6. Once the Vivado workspace opens, under the *Sources* tab, select *+* > *Add +or create design sources* > *Next* > *Create File*. + +7. Introduce the following values: + - *File Type*: `Verilog` + - *File Name*: `mkTop` + - *File Location*: `` + +8. Under the *Sources* tab, select *+* > *Add or create constraints* > *Next* > + *Create File*. + +10. Introduce the following values: + - *File Type*: `XDC` + - *File Name*: `new_constraints` + - *File Location*: `` + +11. From the *Sources* drop down, select *Design Sources* and open the +created design file `mkTop.v`. + +12. Copy the contents of the Verilog code `mkTop.v` as previously modified. + +13. From the *Sources* drop down, select *Constraints* and select the created +constraints file `new_constraints.xdc`. + +14. Copy and modify the constraints file according to the specific FPGA board +that aligns with the project. + +15. To run and compile the code, on the left-hand bar labeled *Flow Navigator*, +under *Project Manager* > *Program and Debug*, Select *Generate Bitstream* to +compile the code. + +16. Once bitsream generation is completed. Navigate under *Hardware Manager* > +*Open Target* > *Plug in your FPGA board via USB* > *Auto Connect* > *Program +Device*. + +The LEDs on your FPGA board should now display the LEDs counting up in +correspondence to its binary value. + +# Acknowledgements +[(Back to top)](#table-of-contents) + +This tutorial has been created by Sukhman Kahlon. + +Special thanks to the following individuals and teams for their guidance and +support throughout this project: + +Pavlo Vlastos – for providing clear and helpful instructions on setting up +Vivado. + +Ryan Scott and the Bluespec team – for their assistance with `copilot-bluespec` +and Bluespec. + +Ivan Perez – for his support with Copilot and set up for this example. + +Kaveh Zare - for sampling the tutorial and providing feedback. diff --git a/copilot/examples/fpga/HelloWorld/Top.bs b/copilot/examples/fpga/HelloWorld/Top.bs new file mode 100644 index 000000000..9e9f00c76 --- /dev/null +++ b/copilot/examples/fpga/HelloWorld/Top.bs @@ -0,0 +1,17 @@ +package Top where + + import HelloWorld + import HelloWorldIfc + import HelloWorldTypes + + helloWorldIfc :: Prelude.Module HelloWorldIfc + helloWorldIfc = + module + -- Register that connects the LEDs to values produced by Copilot + led_reg :: Prelude.Reg (Prelude.UInt 8) <- mkReg 0 + interface + led reg = action + led_reg := reg + + mkTop :: Prelude.Module Prelude.Empty + mkTop = mkHelloWorld helloWorldIfc diff --git a/copilot/examples/fpga/HelloWorld/constraints.xdc b/copilot/examples/fpga/HelloWorld/constraints.xdc new file mode 100644 index 000000000..119f897f3 --- /dev/null +++ b/copilot/examples/fpga/HelloWorld/constraints.xdc @@ -0,0 +1,17 @@ +set_property -dict { PACKAGE_PIN E3 IOSTANDARD LVCMOS33 } [get_ports CLK] +create_clock -add -name sys_clk_pin -period 10.00 -waveform {0 5} [get_ports CLK] + +set_property PACKAGE_PIN C2 [get_ports RST_N] +set_property IOSTANDARD LVCMOS33 [get_ports RST_N] + +# Switches +set_property -dict { PACKAGE_PIN A8 IOSTANDARD LVCMOS33 } [get_ports { sw[0] }]; #IO_L12N_T1_MRCC_16 Sch=sw[0] +set_property -dict { PACKAGE_PIN C11 IOSTANDARD LVCMOS33 } [get_ports { sw[1] }]; #IO_L13P_T2_MRCC_16 Sch=sw[1] +set_property -dict { PACKAGE_PIN C10 IOSTANDARD LVCMOS33 } [get_ports { sw[2] }]; #IO_L13N_T2_MRCC_16 Sch=sw[2] +set_property -dict { PACKAGE_PIN A10 IOSTANDARD LVCMOS33 } [get_ports { sw[3] }]; #IO_L14P_T2_SRCC_16 Sch=sw[3] + +# LEDs +set_property -dict { PACKAGE_PIN H5 IOSTANDARD LVCMOS33 } [get_ports { leds[0] }]; #IO_L24N_T3_35 Sch=led[4] +set_property -dict { PACKAGE_PIN J5 IOSTANDARD LVCMOS33 } [get_ports { leds[1] }]; #IO_25_35 Sch=led[5] +set_property -dict { PACKAGE_PIN T9 IOSTANDARD LVCMOS33 } [get_ports { leds[2] }]; #IO_L24P_T3_A01_D17_14 Sch=led[6] +set_property -dict { PACKAGE_PIN T10 IOSTANDARD LVCMOS33 } [get_ports { leds[3] }]; #IO_L24N_T3_A00_D16_14 Sch=led[7] diff --git a/copilot/examples/fpga/HelloWorld/mkTop.v b/copilot/examples/fpga/HelloWorld/mkTop.v new file mode 100644 index 000000000..23ecef6ab --- /dev/null +++ b/copilot/examples/fpga/HelloWorld/mkTop.v @@ -0,0 +1,75 @@ +// +// Generated by Bluespec Compiler, version 2025.01.1 (build 65e3a87a) +// +// Further modified by Sukhman Kahlon. +// +// On Thu Aug 14 14:52:29 PDT 2025 +// +// +// Ports: +// Name I/O size props +// CLK I 1 clock +// RST_N I 1 reset +// +// No combinational paths from inputs to outputs +// +// + +`ifdef BSV_ASSIGNMENT_DELAY +`else + `define BSV_ASSIGNMENT_DELAY +`endif + +`ifdef BSV_POSITIVE_RESET + `define BSV_RESET_VALUE 1'b1 + `define BSV_RESET_EDGE posedge +`else + `define BSV_RESET_VALUE 1'b0 + `define BSV_RESET_EDGE negedge +`endif + +module mkTop(CLK, + RST_N, + sw, + leds); + input CLK; + input RST_N; + input [3:0] sw; + output [3:0] leds; + + assign leds[3:0] = ifc_led_reg[3:0]; + + // register ifc_led_reg + reg [7 : 0] ifc_led_reg; + wire [7 : 0] ifc_led_reg$D_IN; + wire ifc_led_reg$EN; + + // register ifc_led_reg + assign ifc_led_reg$D_IN = sw[3:0]; + assign ifc_led_reg$EN = 1'd1 ; + + // handling of inlined registers + + always@(posedge CLK) + begin + if (RST_N == `BSV_RESET_VALUE) + begin + ifc_led_reg <= `BSV_ASSIGNMENT_DELAY 8'd0; + end + else + begin + if (ifc_led_reg$EN) + ifc_led_reg <= `BSV_ASSIGNMENT_DELAY ifc_led_reg$D_IN; + end + end + + // synopsys translate_off + `ifdef BSV_NO_INITIAL_BLOCKS + `else // not BSV_NO_INITIAL_BLOCKS + initial + begin + ifc_led_reg = 8'hAA; + end + `endif // BSV_NO_INITIAL_BLOCKS + // synopsys translate_on +endmodule // mkTop From 47f83a0d2744b0019437e3baf7e7a2f691808889 Mon Sep 17 00:00:00 2001 From: Sukhman Kahlon Date: Thu, 21 Aug 2025 16:19:06 -0700 Subject: [PATCH 02/29] copilot: Document changes in CHANGELOG. Refs #657. --- copilot/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index e92d2fe91..edb13dcd5 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,3 +1,6 @@ +2025-08-21 + * Add hello world example for FPGA. (#657) + 2025-07-07 * Version bump (4.5). (#642) From 8c588539f7522594b0b6872d53c47c875bc7a8ad Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 1 Sep 2025 03:47:43 +0000 Subject: [PATCH 03/29] copilot-visualizer: Relax version constraint on `ogma-extra`. Refs #645. In order to keep Copilot effectively working in the current Haskell ecosystem, as well as new versions of GHC, we need to extend the versions of dependencies that Copilot can be installed with. The package `ogma-extra` has seen release 1.9, but copilot-visualizer depend on versions prior to 1.7. This commit relaxes the version constraint of on `ogma-extra` to allow installation of `copilot-visualizer` with versions in the 1.9 series. --- copilot-visualizer/copilot-visualizer.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal index f0f59c93d..cf1399573 100644 --- a/copilot-visualizer/copilot-visualizer.cabal +++ b/copilot-visualizer/copilot-visualizer.cabal @@ -61,7 +61,7 @@ library filepath >= 1.4.2 && < 1.6, hint >= 0.9.0 && < 1.10, pretty >= 1.0 && < 1.2, - ogma-extra >= 1.6.0 && < 1.7, + ogma-extra >= 1.6.0 && < 1.10, text >= 1.2.3.1 && < 2.2, websockets >= 0.12.7 && < 0.14, From 7f6042049506600a59edcb153cf532dee64fd154 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 1 Sep 2025 03:50:17 +0000 Subject: [PATCH 04/29] copilot-visualizer: Document changes in CHANGELOG. Refs #645. --- copilot-visualizer/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 91c4b41fd..2b2449afa 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,3 +1,6 @@ +2025-08-31 + * Relax version constraint on `ogma-extra`. (#645) + 2025-07-07 * Version bump (4.5). (#642) * Include in mainline. (#624) From 70544fb89c82d09d66e0bfef256fec863cc70bb7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 10:21:46 +0000 Subject: [PATCH 05/29] copilot-theorem: Remove unused function Copilot.Theorem.Misc.SExpr.parseSExpr. Refs #661. The function `copilot-theorem:Copilot.Theorem.Misc.SExpr.parseSExpr` is not used anywhere in the implementation. The module is internal and not exposed to the user, so that function does not have and cannot have any users. This commit removes the function, as well as another definition in the module only used by `parseSExpr`, and an import only used by those two functions. --- .../src/Copilot/Theorem/Misc/SExpr.hs | 37 +------------------ 1 file changed, 1 insertion(+), 36 deletions(-) diff --git a/copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs b/copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs index f828850b2..cb7d35ff3 100644 --- a/copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs +++ b/copilot-theorem/src/Copilot/Theorem/Misc/SExpr.hs @@ -2,10 +2,9 @@ {-# LANGUAGE Safe #-} -- | A representation for structured expression trees, with support for pretty --- printing and for parsing. +-- printing. module Copilot.Theorem.Misc.SExpr where -import Text.ParserCombinators.Parsec import Text.PrettyPrint.HughesPJ as PP hiding (char, Str) import Control.Monad @@ -70,37 +69,3 @@ toDoc shouldIndent printAtom expr = case expr of doc $$ indent (toDoc shouldIndent printAtom s) | otherwise = doc <+> toDoc shouldIndent printAtom s - --- | Parser for strings of characters separated by spaces into a structured --- tree. --- --- Parentheses are interpreted as grouping elements, that is, defining a --- 'List', which may be empty. -parser :: GenParser Char st (SExpr String) -parser = - choice [try unitP, nodeP, leafP] - - where - symbol = oneOf "!#$%&|*+-/:<=>?@^_~." - lonelyStr = many1 (alphaNum <|> symbol) - - unitP = string "()" >> return unit - - leafP = atom <$> lonelyStr - - nodeP = do void $ char '(' - spaces - st <- sepBy parser spaces - spaces - void $ char ')' - return $ List st - --- | Parser for strings of characters separated by spaces into a structured --- tree. --- --- Parentheses are interpreted as grouping elements, that is, defining a --- 'List', which may be empty. -parseSExpr :: String -> Maybe (SExpr String) -parseSExpr str = case parse parser "" str of - Left s -> error (show s) -- Nothing - Right t -> Just t From 2d601665aef9b79007e701c937139e8653248905 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 10:23:29 +0000 Subject: [PATCH 06/29] copilot-theorem: Removed unnecessary dependency on parsec. Refs #661. The function `copilot-theorem:Copilot.Theorem.Misc.SExpr.parseSExpr` is not used anywhere in the implementation. The module is internal and not exposed to the user, so that function does not have and cannot have any users. A prior commit has removed the function, which was the only user of the `parsec` library across `copilot-theorem`, thus rendering that dependency no longer necessary. This commit removes that dependency from the Cabal file. --- copilot-theorem/copilot-theorem.cabal | 1 - 1 file changed, 1 deletion(-) diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index 47cd076b0..f120240cb 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -54,7 +54,6 @@ library , libBF >= 0.6.2 && < 0.7 , mtl >= 2.0 && < 2.4 , panic >= 0.4.0 && < 0.5 - , parsec >= 2.0 && < 3.2 , parameterized-utils >= 2.1.1 && < 2.2 , pretty >= 1.0 && < 1.2 , process >= 1.6 && < 1.7 From b0d5e2bc652ff4cb3cd15e977ee49e503501dafa Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 10:27:31 +0000 Subject: [PATCH 07/29] copilot-theorem: Document changes in CHANGELOG. Refs #661. --- copilot-theorem/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index da078ea43..cd1fcbb93 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,3 +1,6 @@ +2025-09-07 + * Remove unused function Copilot.Theorem.Misc.SExpr.parseSExpr. (#661) + 2025-07-07 * Version bump (4.5). (#642) * Removed unused pragmas. (#613) From 3614cc1cf37fceed88bf325352d0559bd31d96ce Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 08/29] copilot-core: Version bump (4.5.1). Refs #666. --- copilot-core/copilot-core.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/copilot-core/copilot-core.cabal b/copilot-core/copilot-core.cabal index ffd4031a9..78e2d5808 100644 --- a/copilot-core/copilot-core.cabal +++ b/copilot-core/copilot-core.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-core -version: 4.5 +version: 4.5.1 synopsis: An intermediate representation for Copilot. description: Intermediate representation for Copilot. From 4af76e9b143c67b4f1a49b65eb8297a356c0ee6d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 09/29] copilot-bluespec: Version bump (4.5.1). Refs #666. --- copilot-bluespec/copilot-bluespec.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-bluespec/copilot-bluespec.cabal b/copilot-bluespec/copilot-bluespec.cabal index 90d9f89d1..f62cb2432 100644 --- a/copilot-bluespec/copilot-bluespec.cabal +++ b/copilot-bluespec/copilot-bluespec.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-bluespec -version : 4.5 +version : 4.5.1 synopsis : A compiler for Copilot targeting FPGAs. description : This package is a back-end from Copilot to FPGAs in Bluespec. @@ -44,7 +44,7 @@ library , filepath >= 1.4 && < 1.6 , pretty >= 1.1.2 && < 1.2 - , copilot-core >= 4.5 && < 4.6 + , copilot-core >= 4.5.1 && < 4.6 , language-bluespec >= 0.1 && < 0.2 exposed-modules : Copilot.Compile.Bluespec From c4a80ceef2c5e2ca47ec44023ea2f9fdeb06d8ff Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 10/29] copilot-c99: Version bump (4.5.1). Refs #666. --- copilot-c99/copilot-c99.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal index 17ec0d950..b33f4e5bc 100644 --- a/copilot-c99/copilot-c99.cabal +++ b/copilot-c99/copilot-c99.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-c99 -version : 4.5 +version : 4.5.1 synopsis : A compiler for Copilot targeting C99. description : This package is a back-end from Copilot to C. @@ -45,7 +45,7 @@ library , mtl >= 2.2 && < 2.4 , pretty >= 1.1 && < 1.2 - , copilot-core >= 4.5 && < 4.6 + , copilot-core >= 4.5.1 && < 4.6 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.3 && < 0.4 From f13c9f567c4abfdca96284b7a473f0fc77bbd070 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 11/29] copilot-prettyprinter: Version bump (4.5.1). Refs #666. --- copilot-prettyprinter/copilot-prettyprinter.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-prettyprinter/copilot-prettyprinter.cabal b/copilot-prettyprinter/copilot-prettyprinter.cabal index 2953cfef6..a5acd909f 100644 --- a/copilot-prettyprinter/copilot-prettyprinter.cabal +++ b/copilot-prettyprinter/copilot-prettyprinter.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-prettyprinter -version: 4.5 +version: 4.5.1 synopsis: A prettyprinter of Copilot Specifications. description: A prettyprinter of Copilot specifications. @@ -45,7 +45,7 @@ library base >= 4.9 && < 5, pretty >= 1.0 && < 1.2, - copilot-core >= 4.5 && < 4.6 + copilot-core >= 4.5.1 && < 4.6 exposed-modules: From 808c8c66529c5036dccf29b6c51200b101e7ddd7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 12/29] copilot-interpreter: Version bump (4.5.1). Refs #666. --- copilot-interpreter/copilot-interpreter.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/copilot-interpreter/copilot-interpreter.cabal b/copilot-interpreter/copilot-interpreter.cabal index 4bcfb3138..b6b2c4fe7 100644 --- a/copilot-interpreter/copilot-interpreter.cabal +++ b/copilot-interpreter/copilot-interpreter.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-interpreter -version: 4.5 +version: 4.5.1 synopsis: Interpreter for Copilot. description: Interpreter for Copilot. @@ -44,7 +44,7 @@ library base >= 4.9 && < 5, pretty >= 1.0 && < 1.2, - copilot-core >= 4.5 && < 4.6 + copilot-core >= 4.5.1 && < 4.6 exposed-modules: From 680dbd6119e28210b10dc25e5474522ed004033f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 13/29] copilot-theorem: Version bump (4.5.1). Refs #666. --- copilot-theorem/copilot-theorem.cabal | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/copilot-theorem/copilot-theorem.cabal b/copilot-theorem/copilot-theorem.cabal index f120240cb..86bb1c68c 100644 --- a/copilot-theorem/copilot-theorem.cabal +++ b/copilot-theorem/copilot-theorem.cabal @@ -14,7 +14,7 @@ description: . -version : 4.5 +version : 4.5.1 license : BSD3 license-file : LICENSE maintainer : Ivan Perez @@ -62,8 +62,8 @@ library , xml >= 1.3 && < 1.4 , what4 >= 1.3 && < 1.8 - , copilot-core >= 4.5 && < 4.6 - , copilot-prettyprinter >= 4.5 && < 4.6 + , copilot-core >= 4.5.1 && < 4.6 + , copilot-prettyprinter >= 4.5.1 && < 4.6 exposed-modules : Copilot.Theorem , Copilot.Theorem.Prove From 67977320ff07b2d9be7fa1d636d7ead2c0230e69 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 14/29] copilot-language: Version bump (4.5.1). Refs #666. --- copilot-language/copilot-language.cabal | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/copilot-language/copilot-language.cabal b/copilot-language/copilot-language.cabal index e9d4de9a9..7d02c0bfc 100644 --- a/copilot-language/copilot-language.cabal +++ b/copilot-language/copilot-language.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-language -version: 4.5 +version: 4.5.1 synopsis: A Haskell-embedded DSL for monitoring hard real-time distributed systems. description: @@ -42,9 +42,9 @@ library , data-reify >= 0.6 && < 0.7 , mtl >= 2.0 && < 3 - , copilot-core >= 4.5 && < 4.6 - , copilot-interpreter >= 4.5 && < 4.6 - , copilot-theorem >= 4.5 && < 4.6 + , copilot-core >= 4.5.1 && < 4.6 + , copilot-interpreter >= 4.5.1 && < 4.6 + , copilot-theorem >= 4.5.1 && < 4.6 exposed-modules: Copilot.Language , Copilot.Language.Operators.BitWise From d1b0ffdf8e514113b57c4df4339db83a1c447613 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 15/29] copilot-libraries: Version bump (4.5.1). Refs #666. --- copilot-libraries/copilot-libraries.cabal | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/copilot-libraries/copilot-libraries.cabal b/copilot-libraries/copilot-libraries.cabal index 214fe7dc4..3402b5296 100644 --- a/copilot-libraries/copilot-libraries.cabal +++ b/copilot-libraries/copilot-libraries.cabal @@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-libraries -version: 4.5 +version: 4.5.1 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language. @@ -38,10 +38,10 @@ library build-depends: base >= 4.9 && < 5 - , containers >= 0.4 && < 0.8 - , mtl >= 2.0 && < 2.4 - , parsec >= 2.0 && < 3.2 - , copilot-language >= 4.5 && < 4.6 + , containers >= 0.4 && < 0.8 + , mtl >= 2.0 && < 2.4 + , parsec >= 2.0 && < 3.2 + , copilot-language >= 4.5.1 && < 4.6 exposed-modules: Copilot.Library.Libraries From eec16989d5f0110dec1750de83db1a521f5a4fb2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 16/29] copilot-verifier: Version bump (4.5.1). Refs #666. --- copilot-verifier/copilot-verifier.cabal | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index 8b915e154..808ac3823 100644 --- a/copilot-verifier/copilot-verifier.cabal +++ b/copilot-verifier/copilot-verifier.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: copilot-verifier -Version: 4.5 +Version: 4.5.1 Author: Galois Inc. Maintainer: rscott@galois.com Copyright: (c) Galois, Inc 2021-2024 @@ -45,9 +45,9 @@ common bldflags bv-sized >= 1.0.0 && < 1.1, bytestring, containers >= 0.5.9.0, - copilot-c99 >= 4.5 && < 4.6, - copilot-core >= 4.5 && < 4.6, - copilot-theorem >= 4.5 && < 4.6, + copilot-c99 >= 4.5.1 && < 4.6, + copilot-core >= 4.5.1 && < 4.6, + copilot-theorem >= 4.5.1 && < 4.6, crucible >= 0.7.1 && < 0.8, crucible-llvm >= 0.7 && < 0.8, crux >= 0.7.1 && < 0.8, @@ -80,10 +80,10 @@ library copilot-verifier-examples hs-source-dirs: examples build-depends: case-insensitive, - copilot >= 4.5 && < 4.6, - copilot-language >= 4.5 && < 4.6, - copilot-libraries >= 4.5 && < 4.6, - copilot-prettyprinter >= 4.5 && < 4.6, + copilot >= 4.5.1 && < 4.6, + copilot-language >= 4.5.1 && < 4.6, + copilot-libraries >= 4.5.1 && < 4.6, + copilot-prettyprinter >= 4.5.1 && < 4.6, copilot-verifier exposed-modules: Copilot.Verifier.Examples From d7c1281ae06f74b8b7d2140725d71126bb9a2dd3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 17/29] copilot-visualizer: Version bump (4.5.1). Refs #666. --- copilot-visualizer/copilot-visualizer.cabal | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/copilot-visualizer/copilot-visualizer.cabal b/copilot-visualizer/copilot-visualizer.cabal index cf1399573..c88f26f1f 100644 --- a/copilot-visualizer/copilot-visualizer.cabal +++ b/copilot-visualizer/copilot-visualizer.cabal @@ -1,6 +1,6 @@ cabal-version: >= 1.10 name: copilot-visualizer -version: 4.5 +version: 4.5.1 synopsis: Visualizer for Copilot. description: Visualizer for Copilot. @@ -65,10 +65,10 @@ library text >= 1.2.3.1 && < 2.2, websockets >= 0.12.7 && < 0.14, - copilot >= 4.5 && < 4.6, - copilot-core >= 4.5 && < 4.6, - copilot-interpreter >= 4.5 && < 4.6, - copilot-language >= 4.5 && < 4.6 + copilot >= 4.5.1 && < 4.6, + copilot-core >= 4.5.1 && < 4.6, + copilot-interpreter >= 4.5.1 && < 4.6, + copilot-language >= 4.5.1 && < 4.6 exposed-modules: @@ -121,7 +121,7 @@ executable tikz-example build-depends: base >= 4.9 && < 5, - copilot >= 4.5 && < 4.6, + copilot >= 4.5.1 && < 4.6, copilot-visualizer if flag(examples) From d1d2b270598cf398de857c3ae289e8b37f6549f9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:56:58 -0700 Subject: [PATCH 18/29] copilot: Version bump (4.5.1). Refs #666. --- copilot/copilot.cabal | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/copilot/copilot.cabal b/copilot/copilot.cabal index 6d9570b19..a15dd5cf3 100644 --- a/copilot/copilot.cabal +++ b/copilot/copilot.cabal @@ -1,5 +1,5 @@ name: copilot -version: 4.5 +version: 4.5.1 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE @@ -52,12 +52,12 @@ library , directory >= 1.3 && < 1.4 , filepath >= 1.4 && < 1.6 - , copilot-core >= 4.5 && < 4.6 - , copilot-theorem >= 4.5 && < 4.6 - , copilot-language >= 4.5 && < 4.6 - , copilot-libraries >= 4.5 && < 4.6 - , copilot-c99 >= 4.5 && < 4.6 - , copilot-prettyprinter >= 4.5 && < 4.6 + , copilot-core >= 4.5.1 && < 4.6 + , copilot-theorem >= 4.5.1 && < 4.6 + , copilot-language >= 4.5.1 && < 4.6 + , copilot-libraries >= 4.5.1 && < 4.6 + , copilot-c99 >= 4.5.1 && < 4.6 + , copilot-prettyprinter >= 4.5.1 && < 4.6 exposed-modules: Language.Copilot, Language.Copilot.Main From 051b91322eec26cc5aae4efb401b4ca12cf81b70 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 19/29] copilot-core: Document changes in CHANGELOG. Refs #666. --- copilot-core/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-core/CHANGELOG b/copilot-core/CHANGELOG index 810d39b24..62e89d1ef 100644 --- a/copilot-core/CHANGELOG +++ b/copilot-core/CHANGELOG @@ -1,3 +1,6 @@ +2025-09-07 + * Version bump (4.5.1). (#666) + 2025-07-07 * Version bump (4.5). (#642) * Remove deprecated fields of Copilot.Core.Expr.UExpr. (#636) From fda59ae9fef63606bb655c6fd7b7ea9f8dacd688 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 20/29] copilot-bluespec: Document changes in CHANGELOG. Refs #666. --- copilot-bluespec/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-bluespec/CHANGELOG b/copilot-bluespec/CHANGELOG index ccfaad8ab..e7472493b 100644 --- a/copilot-bluespec/CHANGELOG +++ b/copilot-bluespec/CHANGELOG @@ -1,3 +1,6 @@ +2025-09-07 + * Version bump (4.5.1). (#666) + 2025-07-07 * Version bump (4.5). (#642) * Include `copilot-bluespec` in mainline `copilot` repo. (#623) From 7448c20bc13adc1a1d2aedc74a1cac24219ee8b3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 21/29] copilot-c99: Document changes in CHANGELOG. Refs #666. --- copilot-c99/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 7b7d3aeb6..e5f0b606d 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,3 +1,6 @@ +2025-09-07 + * Version bump (4.5.1). (#666) + 2025-07-07 * Version bump (4.5). (#642) From fb15c4ee661b2c6da8745ee6a2ffc962b9cd93e7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 22/29] copilot-prettyprinter: Document changes in CHANGELOG. Refs #666. --- copilot-prettyprinter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-prettyprinter/CHANGELOG b/copilot-prettyprinter/CHANGELOG index 8f94d9fa6..73ca7c5bf 100644 --- a/copilot-prettyprinter/CHANGELOG +++ b/copilot-prettyprinter/CHANGELOG @@ -1,3 +1,6 @@ +2025-09-07 + * Version bump (4.5.1). (#666) + 2025-07-07 * Version bump (4.5). (#642) From 65c53b3ea01a33e60b803fecabc9399adb2bda45 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 23/29] copilot-interpreter: Document changes in CHANGELOG. Refs #666. --- copilot-interpreter/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-interpreter/CHANGELOG b/copilot-interpreter/CHANGELOG index cd1e6b431..e819c4162 100644 --- a/copilot-interpreter/CHANGELOG +++ b/copilot-interpreter/CHANGELOG @@ -1,3 +1,6 @@ +2025-09-07 + * Version bump (4.5.1). (#666) + 2025-07-07 * Version bump (4.5). (#642) From 4406c1844bd33e32864efaea71473459c1e6a6e7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 24/29] copilot-theorem: Document changes in CHANGELOG. Refs #666. --- copilot-theorem/CHANGELOG | 1 + 1 file changed, 1 insertion(+) diff --git a/copilot-theorem/CHANGELOG b/copilot-theorem/CHANGELOG index cd1fcbb93..621417e73 100644 --- a/copilot-theorem/CHANGELOG +++ b/copilot-theorem/CHANGELOG @@ -1,4 +1,5 @@ 2025-09-07 + * Version bump (4.5.1). (#666) * Remove unused function Copilot.Theorem.Misc.SExpr.parseSExpr. (#661) 2025-07-07 From 6034ccfd294454190470fa96cb46ca46f5598b92 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 25/29] copilot-language: Document changes in CHANGELOG. Refs #666. --- copilot-language/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-language/CHANGELOG b/copilot-language/CHANGELOG index 60112d6f8..ed8ebbebb 100644 --- a/copilot-language/CHANGELOG +++ b/copilot-language/CHANGELOG @@ -1,3 +1,6 @@ +2025-09-07 + * Version bump (4.5.1). (#666) + 2025-07-07 * Version bump (4.5). (#642) From bd1c2ce43b15e68bf1b086cb2f40fbb9edb9d32b Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 26/29] copilot-libraries: Document changes in CHANGELOG. Refs #666. --- copilot-libraries/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-libraries/CHANGELOG b/copilot-libraries/CHANGELOG index c724f29b5..5d4323d7f 100644 --- a/copilot-libraries/CHANGELOG +++ b/copilot-libraries/CHANGELOG @@ -1,3 +1,6 @@ +2025-09-07 + * Version bump (4.5.1). (#666) + 2025-07-07 * Version bump (4.5). (#642) From fe74b7b0686eef85bbf68f96c48bb3924cc74987 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 27/29] copilot-verifier: Document changes in CHANGELOG. Refs #666. --- copilot-verifier/CHANGELOG | 3 +++ 1 file changed, 3 insertions(+) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index 59ac57d9a..e8b89e276 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,3 +1,6 @@ +2025-09-07 + * Version bump (4.5.1). (#666) + 2025-07-07 * Version bump (4.5). (#642) * Include `copilot-verifier` in mainline `copilot` repo. (#622) From e8a1af051cf43545dfc35302a27dc3032a38fc96 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 28/29] copilot-visualizer: Document changes in CHANGELOG. Refs #666. --- copilot-visualizer/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-visualizer/CHANGELOG b/copilot-visualizer/CHANGELOG index 2b2449afa..cf9f151fb 100644 --- a/copilot-visualizer/CHANGELOG +++ b/copilot-visualizer/CHANGELOG @@ -1,4 +1,5 @@ -2025-08-31 +2025-09-07 + * Version bump (4.5.1). (#666) * Relax version constraint on `ogma-extra`. (#645) 2025-07-07 From 4615b1a78b36768d6c271ddea5e399a56b342243 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 7 Sep 2025 14:58:31 -0700 Subject: [PATCH 29/29] copilot: Document changes in CHANGELOG. Refs #666. --- copilot/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot/CHANGELOG b/copilot/CHANGELOG index edb13dcd5..7b69ed049 100644 --- a/copilot/CHANGELOG +++ b/copilot/CHANGELOG @@ -1,4 +1,5 @@ -2025-08-21 +2025-09-07 + * Version bump (4.5.1). (#666) * Add hello world example for FPGA. (#657) 2025-07-07