Proposal for a Tutorial on Copilot BlueSpec #651
sukhmankkahlon
started this conversation in
General
Replies: 1 comment
-
|
Thank you for writing this up! Having a complete, end-to-end tutorial like this is incredibly useful. Some suggestions/questions:
|
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
Uh oh!
There was an error while loading. Please reload this page.
-
Copilot BlueSpec Counter Example on a FPGA Board V2
With Minimal Modifications in Verilog Generated Code
Copilot is a runtime verification framework for hard real-time systems.
This repository includes an example, Counter.hs, which demonstrates how Copilot's Haskell code can be compiled to Bluespec, then further compiled to Verilog, and ultimately deployed onto an FPGA board. The output of the program will be verified via LEDs on the FPGA.
This example serves as a starting point for users interested in integrating Copilot into their own verification workflows or real-time hardware projects. It showcases the full toolchain from Haskell to hardware implementation.
The compiled Verilog code will be programmed onto the FPGA (Artix-7 XC7A35T) using Xilinx Vivado.
Vivado Installation •
Example •
Acknowledgements •
Table of Contents
Vivado Installation
(Back to top)
Vivado 2025.1
Vivado can be installed through terminal as suggested by this process.
VivadoVivado ML Standard7 Series (or whichever device you're working with)/tools/forXilinx.If the candidate installation directory is highlighted red it has wrong permissions and/or owner. Please see
Step 6.b.b) Change the owner into a different user. If this does not work, see
Step 6.cc) Try to run the binary installer as sudo (root).
installwhen prompted. The download should be ~20 GB to 50 GB. After installation run:source /tools/Xilinx/2025.1/Vivado/.settings64-Vivado.shThe terminal should display the following output:
Terminal Output
Successful Installation Output
Troubleshooting
(Back to top)
The installation provided is for a Vivado version that is ~ 50 GB less than the one through direct installation from the AMD website. If issues arise from the provided installation process, there are tutorials provided online that provide alternate methods of installation.
Example
Counter Example Code
(Back to top)
The Counter.hs example is provided in the examples directory of the main repository. This example is subject to change. The current Counter.hs code simply increments up to the specified value 256 and resets back to 0.
In this tutorial, Counter.hs needs to have the modifications below in order to be displayed onto LEDS on an FPGA board.
Once the existing
Counter.hscode has been downloaded, the pre-existing code should be modified to import the bluespec backend rather than the C99 backend.will be replaced with
As mentioned, the original code increments to the value 256. Due to physical limitations of the FPGA Board consisting of only 4 LEDS, the code will be modified and limited to a value under 4 bits. The variable
count_maxwill carry this value. This values maximum number has to be less than or equal to 16 to stay in the 4 bits range. The value 7 was randomly picked for this examplescount_maxso that it's clear that the board is behaving as we expect. The expectations are that the LEDs will increment up to the binary valuecount_max - 1, which in our case is 6 and then reset. We construct the Stream asInt32because the resettable counter function provided expects aStream Int32. This will be true for all definitions and declarations.Create and set the maximum counter value to your desired value.
The original system clock is too fast for the human eye to percieve changes on the LEDS. To combat this, we create a constant
Stream Int32value that will be used to slow down the clock speed. This speed dictates the LEDS switch rate and can be adjusted to the users preference. In this example we have chosen the value 50,000,000 (50M) cycles which corresponds to the counters incrementing speed.Using the counter function provided in Counter.hs. A
clk_dividercounter needs to be created to generate the slower clock cycle so the incrementation will be visible on the LEDS. Theresetfor theclk_divideris triggered only when the counter reaches the valueclk_led + 1.This setup mimics the existing
bytecounterdefinition. (Down Below)The name will be changed to
clk_dividerand a new modulo value to control the slower clock rate:Now we adjust the
bytecounterdefinition to create the counter that will be displayed on the FPGA board using thecount_maxvalue. When definingbytecounterwe expect the counter to only increment and reset when certain conditions occur. To ensure this, we do not set the Boolean value directly in the definition forbytecounter, but instead create a certain set condition forincandreset. When we definebytecounter,the counter will only increment when our previous counters value matches the value we set for the slower clock cycle. We setincequivalent to(clk_divider == clk_led)to ensure this happens. In ourresetdefintion, the modulo value must be replaced by our variablecount_max. Defining the modulo values with variables allows minimum changes for the user if they choose to change the LED clock speed or the LED counter.Provided are the
bytecountersadditions and changes.Bluespec requires a different main declaration then the one required for C99 compiling. Renaming the file that will be generated once the Haskell code is compiled is necessary as the current name clashes with a preexisting package file from the Bluespec prelude. The name of the generated Bluespec files will be
CountersUp.Will be replaced by
The fully modified
Counter.hscode in Copilot is provided below.In the terminal, navigate to the directory that stores the modified
Counter.hsexample.In your shell, based off the assumption that Copilot and Bluespec compiler are installed on your device (see Copilot and Bluespec for installation instructions) run this command:
This command will generate 3 files in Bluespec in the same directory provided. Verify the following contents of the files:
CountersUp.bs,CountersUpIfc.bsandCountersUpTypes.bs.CountersUp.bs
CountersUpIfc.bs
CountersUpTypes.bs
In your terminal, run the following command.
This step generates the Verilog code that will be implemented onto your FPGA board. Ignore the warnings shown in terminal output, but ensure that the file
mkTop.vis successfully created in your current directory. To program the counter onto the FPGA, additional port declarations and assignments are required in themkTopmodule.The module
mkTopneeds the output portledsinside the parenthesis. Alongside the existing input definitions, define a 4 bit output defining theledsas anoutput.Insied the module body, assign the
ledsto the registers3_0. THe values held ins3_0corresponds to thebytecounterthat was created in our original Copilot code.The following mkTop.v input/output and port declarations are generated by the bsc compiler:
Replace / add the following lines mentioned above:
For reference, the complete contents of mkTop.v after applying the changes are included below:
mkTop.v
This code will be implemented into the design source file created on Vivado by replacing the preexisting 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 you used. Please refer to the reference manual for your specific FPGA board to assign pins for LEDs accordingly.
Keep in mind that the
ledsvariable name from the port declaration must match the constaints file. For reference, here is the constraints file assigning LED 4-7 for the Arty 35T CSG324-1 to the output leds.new_constraints.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 U18 [get_ports RST_N] set_property IOSTANDARD LVCMOS33 [get_ports RST_N] # LEDs for output (first 4 LEDs specific to my board) set_property PACKAGE_PIN H5 [get_ports {leds[0]}] set_property PACKAGE_PIN J5 [get_ports {leds[1]}] set_property PACKAGE_PIN T9 [get_ports {leds[2]}] set_property PACKAGE_PIN T10 [get_ports {leds[3]}] # Set IOSTANDARD for all LED outputs set_property IOSTANDARD LVCMOS33 [get_ports {leds[*]}]Running the Counter Example on Vivado
(Back to top)
Once installed, open your Vivado Design Suite.
Create Project>Next> Project Name :CountersUpand choose the desired location.Create Project Subdirectory>Next>RTL Project>Do not specify sources at this time>Next>xc7a35tcsg324-1for the project device used in this example.The project should be created and initialized.
Sourcestab.+>Add or create design sources>Next>Create File>VerilogFile Name:
mkTopFile Location:
<Local to Project>Sourcestab again.+>Add or create constraints>Next>Create File>XDCFile Name:
new_constraintsFile Location:
<Local to Project>Sourcesdrop down, selectDesign Sourcesand select the created design filemkTop.mkTop.vthat was previously modified.Sourcesdrop down, selectConstraintsand select the created constraint filenew_constraints.xdc.Flow Navigator, underProject Manager>Program and Debug> SelectGenerate Bitstreamto compile the code.Hardware Manager>Open Target> Plug in your FPGA board via USB. >Auto Connect>Program DeviceThe LEDS on your FPGA board should now display the LEDS counting up in correspondence to its binary value.
Pictures
(Back to top)
The images show the Arty 7 displaying the binary values up to 6.
Binary 0
0000Binary 1
0001Binary 2
0010Binary 3
0011Binary 4
0100Binary 5
0101Binary 6
0110Acknowledgements
(Back to top)
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.
Beta Was this translation helpful? Give feedback.
All reactions