diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,11 @@ + + +# Revision history for `clash-vexriscv` + +## 0.1.0 -- 2026-05-19 + +* First version. Released on an unsuspecting world. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,202 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,111 @@ + + +# clash-vexriscv +This package provides a VexRiscv CPU core for use in Clash designs. + +## Dependencies +For building the CPU, the following software needs to be installed and available +in the `PATH`: + +- a recent JDK installation +- SBT, the scala build tool +- a recent C compiler +- `verilator` +- `make` for building the verilated library and FFI code + +## Limitations + * The core will generate as part of your project's setup. This means that configuration cannot be based on parts of your design. E.g., whether or not to activate the floating point extension on the CPU will have to be decided before integration in the project. + * The package is currently hardcoded to expect a Wishbone and JTAG bus. + * The setup procedure currently compiles the Verilated Verilog itself, bypassing Cabal. This means Cabal compiler flags have no effect. + +## Integration +This package does not give you a VexRiscv core directly, but offers the necessary +tools to generate one as part of a Cabal package. You will have to do two things: + + * Provide a (Scala-based) configuration file for the VexRiscv + * Integrate `clash-vexriscv` with your Cabal project + +### Example project +A complete example project is provided in the [`../clash-vexriscv-example/`](../clash-vexriscv-example/) directory. This example demonstrates: + +- A minimal Cabal project setup for using `clash-vexriscv` +- A VexRiscv CPU configuration file (`data/MyProject.scala`) with: + - Basic RiscV ISA components (IBus, DBus, CSR, decoder, register file, ALU) + - Simple hazard handling + - Branch prediction + - JTAG debug interface + - Wishbone memory buses for instruction and data access + +You can use this as a template for your own integration project. + +### CPU configuration +VexRiscv is a very configurable CPU as shown by a great number of [demo configurations](https://github.com/SpinalHDL/VexRiscv/tree/master/src/main/scala/vexriscv/demo). This package is currently hardcoded to need two things: + + * A Wishbone interface + * A debug (JTAG) interface + +It also expects SpinalHDL to generate all Verilog names with a certain prefix. This is all handled by this [example configuration](../clash-vexriscv-example/data/MyProject.scala). Place the configuration in a folder, e.g. `data` and give it a recognizable name. In our example, this is `MyProject`. If you change the filename, don't forget to change the object name in the configuration file too. + +### Cabal integration +In the root of your package, add `Setup.hs`: + +```haskell +import Distribution.Simple +import VexRiscv.Setup (addVexRiscvHooks) + +main :: IO () +main = defaultMainWithHooks (addVexRiscvHooks simpleUserHooks "data" ["MyProject"]) +``` + +Then, in your Cabal file, set the build type to `Custom`, add your configuration, and add a `custom-setup`: + +```cabal +build-type: Custom + +extra-source-files: + data/*.Scala + +custom-setup + setup-depends: + base, + Cabal, + clash-vexriscv +``` + +In your `library` section, add the following: + +```cabal + other-modules: + VexRiscv_MyProject + autogen-modules: + VexRiscv_MyProject +``` + +If you picked another name than `MyProject`, replace that part of the module name. The module will export a single function: + +```haskell +vexRiscv :: + forall dom. + (HasCallStack, KnownDomain dom) => + DumpVcd -> + Clock dom -> + MinCyclesReset dom 2 -> + Signal dom CpuIn -> + Signal dom JtagIn -> + ( Signal dom CpuOut + , Signal dom JtagOut + ) +``` + +Good luck! + +## Notes for using the core: + +- The contents of memories need to be stored in little endian. This means that + for example the contents of an ELF file need to be endian-swapped before being + used as the contents of the instruction storage. + This applies to all storages. diff --git a/clash-vexriscv.cabal b/clash-vexriscv.cabal new file mode 100644 --- /dev/null +++ b/clash-vexriscv.cabal @@ -0,0 +1,176 @@ +cabal-version: 3.8 +name: clash-vexriscv +version: 0.1 +synopsis: VexRiscv CPU core for use in Clash designs +description: + Provides the tooling to integrate a + CPU core into a Clash + design. The package does not offer a CPU directly; instead it provides + Cabal @Setup.hs@ hooks that generate a CPU from a Scala-based + configuration at build time, together with the Haskell bindings + (FFI, blackboxes, simulation helpers) needed to use the resulting core + from Clash. +License: Apache-2.0 +license-file: LICENSE +author: QBayLogic B.V. +maintainer: devops@qbaylogic.com +Copyright: Copyright © 2022 Google LLC +build-type: Simple +category: Development + +extra-doc-files: + README.md + CHANGELOG.md + +data-files: + data/vexriscv/build.sbt + data/vexriscv/ffi/*.cpp + data/vexriscv/ffi/*.h + data/vexriscv/lib/*.jar + data/vexriscv/lib/*.py + data/vexriscv/Makefile + data/vexriscv/project/build.properties + data/vexriscv/project/Dependencies.scala + +common common-options + default-extensions: + BangPatterns + BinaryLiterals + ConstraintKinds + DataKinds + DefaultSignatures + DeriveAnyClass + DeriveDataTypeable + DeriveFoldable + DeriveFunctor + DeriveGeneric + DeriveLift + DeriveTraversable + DerivingStrategies + InstanceSigs + KindSignatures + LambdaCase + NoStarIsType + PackageImports + PolyKinds + RankNTypes + ScopedTypeVariables + StandaloneDeriving + TupleSections + TypeApplications + TypeFamilies + TypeOperators + ViewPatterns + + -- TemplateHaskell is used to support convenience functions such as + -- 'listToVecTH' and 'bLit'. + TemplateHaskell + QuasiQuotes + + -- Prelude isn't imported by default as Clash offers Clash.Prelude + NoImplicitPrelude + + -- See https://github.com/clash-lang/clash-compiler/pull/2511 + if impl(ghc >= 9.4) + CPP-Options: -DCLASH_OPAQUE=OPAQUE + else + CPP-Options: -DCLASH_OPAQUE=NOINLINE + + ghc-options: + -Wall -Wcompat + + -- Plugins to support type-level constraint solving on naturals + -fplugin GHC.TypeLits.Extra.Solver + -fplugin GHC.TypeLits.Normalise + -fplugin GHC.TypeLits.KnownNat.Solver + + -- Clash needs access to the source code in compiled modules + -fexpose-all-unfoldings + + -- Worker wrappers introduce unstable names for functions that might have + -- blackboxes attached for them. You can disable this, but be sure to add + -- a no-specialize pragma to every function with a blackbox. + -fno-worker-wrapper + -- clash-prelude will set suitable version bounds for the plugins + build-depends: + base >= 4.18 && < 4.22, + clash-prelude >= 1.9.0, + containers >= 0.6 && < 0.9, + ghc-typelits-natnormalise, + ghc-typelits-extra, + ghc-typelits-knownnat, + + other-modules: Paths_clash_vexriscv + autogen-modules: Paths_clash_vexriscv + +library + import: common-options + hs-source-dirs: src + default-language: Haskell2010 + exposed-modules: + VexRiscv + VexRiscv.BlackBox + VexRiscv.ClockTicks + VexRiscv.Paths + VexRiscv.FFI + VexRiscv.Internal + VexRiscv.JtagTcpBridge + VexRiscv.Random + VexRiscv.Reset + VexRiscv.Setup + VexRiscv.VecToTuple + + build-depends: + async, + bytestring >= 0.10 && < 0.13, + Cabal >= 3.14 && < 4, + clash-lib, + clash-prelude >= 1.10 && < 1.12, + clash-protocols, + containers, + deepseq, + directory >= 1.3 && < 1.4, + extra, + filepath, + Glob, + hashable, + infinite-list, + interpolate, + mtl, + network, + pretty-show, + process >= 1.6 && < 1.8, + random, + tagged, + template-haskell, + temporary, + text, + include-dirs: data/vexriscv + cxx-sources: data/vexriscv/ffi/impl.cpp + cxx-options: -std=c++11 + extra-libraries: stdc++ + +test-suite unittests + import: common-options + hs-source-dirs: tests/unittests + default-language: Haskell2010 + type: exitcode-stdio-1.0 + main-is: main.hs + ghc-options: -Wall -Wcompat -threaded -rtsopts + other-modules: + Tests.Extra + Tests.VexRiscv.ClockTicks + Tests.VexRiscv.Random + Tests.VexRiscv.Reset + build-depends: + HUnit, + base, + clash-prelude-hedgehog, + clash-vexriscv, + bytestring, + hedgehog >= 1.5 && < 1.8, + tasty >= 1.4 && < 1.6, + tasty-hedgehog, + tasty-hunit, + tasty-th, + template-haskell, diff --git a/data/vexriscv/Makefile b/data/vexriscv/Makefile new file mode 100644 --- /dev/null +++ b/data/vexriscv/Makefile @@ -0,0 +1,98 @@ +# SPDX-FileCopyrightText: 2022 Google LLC +# +# SPDX-License-Identifier: CC0-1.0 + +CLASH_VEXRISCV_DATA_DIR = $(dir $(MAKEFILE_LIST)) +SCALA_CONFIG_DIR = SCALA_CONFIG_DIR-you-have-to-set-this-as-an-argument +CPU_NAME = CPU_NAME-you-have-to-set-this-as-an-argument + +VERILATOR_DIR = verilator +VERILATOR_FLAGS = -CFLAGS '-O3 -fPIC' -Wno-fatal +1364-2001ext+v --trace + +N := $(patsubst -j%,%,$(filter -j%,$(MAKEFLAGS))) + +VERILATOR_CFLAGS = $(shell pkg-config --cflags verilator) +FFI_CPPFLAGS = $(VERILATOR_CFLAGS) -fPIC -O3 -I$(VERILATOR_DIR) + +# XXX: Frustratingly, REPL only works with dynamic libraries, but Cabal prefers +# static ones. On the flip side, normal *runs* only work with static +# libraries. We therefore put them into separate directories so that we +# can easily pick the right one depending on the use-case. +all: ../static/lib$(CPU_NAME)VexRiscvFFI.a ../dynamic/lib$(CPU_NAME)VexRiscvFFI.so + +clean: + rm -rf *.o *.v *.a *.so *.sbt ffi lib project src $(VERILATOR_DIR) target + +build.sbt: $(CLASH_VEXRISCV_DATA_DIR)/build.sbt $(CLASH_VEXRISCV_DATA_DIR)/Makefile + cp $(CLASH_VEXRISCV_DATA_DIR)/build.sbt build.sbt + +project/%: $(CLASH_VEXRISCV_DATA_DIR)/project/% $(CLASH_VEXRISCV_DATA_DIR)/Makefile + mkdir -p project + cp $< $@ + +lib/vexriscv.jar: ../../vexriscv.jar $(CLASH_VEXRISCV_DATA_DIR)/Makefile + mkdir -p lib + cp ../../vexriscv.jar $@ + +ffi/%: $(CLASH_VEXRISCV_DATA_DIR)/ffi/% $(CLASH_VEXRISCV_DATA_DIR)/Makefile + mkdir -p ffi + cp $< $@ + sed -i 's/__CPU_NAME__/$(CPU_NAME)/g' $@ + +src/main/scala/cpu/%: $(SCALA_CONFIG_DIR)/% $(CLASH_VEXRISCV_DATA_DIR)/Makefile + mkdir -p src/main/scala/cpu + cp $< $@ + +$(CPU_NAME)VexRiscv.v: src/main/scala/cpu/$(CPU_NAME).scala lib/vexriscv.jar build.sbt project/build.properties project/Dependencies.scala $(CLASH_VEXRISCV_DATA_DIR)/Makefile + # XXX: SBT cannot build in parallel without issues, so we separate the compile + # and runMain steps and guard the former with a lock file. + flock $(HOME)/.sbt-lock sbt compile + sbt "runMain cpu.$(CPU_NAME)" + sed -i -E '/\/\/ Git hash :.*$$/d' $(CPU_NAME)VexRiscv.v + +$(VERILATOR_DIR)/V$(CPU_NAME)VexRiscv.mk $(VERILATOR_DIR)/V$(CPU_NAME)VexRiscv.h: $(CPU_NAME)VexRiscv.v $(CLASH_VEXRISCV_DATA_DIR)/Makefile + verilator $(VERILATOR_FLAGS) --cc -Mdir $(VERILATOR_DIR) $(CPU_NAME)VexRiscv.v + +$(VERILATOR_DIR)/V$(CPU_NAME)VexRiscv__ALL.a: $(VERILATOR_DIR)/V$(CPU_NAME)VexRiscv.mk $(CLASH_VEXRISCV_DATA_DIR)/Makefile + cd $(VERILATOR_DIR); make -f V$(CPU_NAME)VexRiscv.mk -j $(N) + +impl.o: ffi/impl.cpp ffi/interface.h $(VERILATOR_DIR)/V$(CPU_NAME)VexRiscv.h $(CLASH_VEXRISCV_DATA_DIR)/Makefile + $(CXX) $(FFI_CPPFLAGS) -c ffi/impl.cpp -o impl.o + +vimpl.o: ffi/vimpl.cpp ffi/interface.h $(shell pkg-config --variable=includedir verilator)/verilated.h $(shell pkg-config --variable=includedir verilator)/verilated_vcd_c.h $(VERILATOR_DIR)/V$(CPU_NAME)VexRiscv.h $(CLASH_VEXRISCV_DATA_DIR)/Makefile + $(CXX) $(FFI_CPPFLAGS) -c ffi/vimpl.cpp -o vimpl.o + +verilated_vcd_c.o: $(shell pkg-config --variable=includedir verilator)/verilated_vcd_c.cpp $(CLASH_VEXRISCV_DATA_DIR)/Makefile + $(CXX) $(FFI_CPPFLAGS) -c $(shell pkg-config --variable=includedir verilator)/verilated_vcd_c.cpp -o verilated_vcd_c.o + +verilated.o: $(shell pkg-config --variable=includedir verilator)/verilated.cpp $(CLASH_VEXRISCV_DATA_DIR)/Makefile + $(CXX) $(FFI_CPPFLAGS) -c $(shell pkg-config --variable=includedir verilator)/verilated.cpp -o verilated.o + +verilated_threads.o: $(shell pkg-config --variable=includedir verilator)/verilated_threads.cpp $(CLASH_VEXRISCV_DATA_DIR)/Makefile + $(CXX) $(FFI_CPPFLAGS) -c $(shell pkg-config --variable=includedir verilator)/verilated_threads.cpp -o verilated_threads.o + +V$(CPU_NAME)VexRiscv__ALL.a: $(VERILATOR_DIR)/V$(CPU_NAME)VexRiscv__ALL.a $(CLASH_VEXRISCV_DATA_DIR)/Makefile + cp $(VERILATOR_DIR)/V$(CPU_NAME)VexRiscv__ALL.a V$(CPU_NAME)VexRiscv__ALL.a + +lib$(CPU_NAME)VexRiscvFFI.a: V$(CPU_NAME)VexRiscv__ALL.a vimpl.o impl.o verilated.o verilated_threads.o verilated_vcd_c.o $(CLASH_VEXRISCV_DATA_DIR)/Makefile + rm -f libVexRiscvFFI.a + cp V$(CPU_NAME)VexRiscv__ALL.a lib$(CPU_NAME)VexRiscvFFI.a + ar r \ + lib$(CPU_NAME)VexRiscvFFI.a \ + vimpl.o \ + impl.o \ + verilated.o \ + verilated_threads.o \ + verilated_vcd_c.o + +lib$(CPU_NAME)VexRiscvFFI.so: lib$(CPU_NAME)VexRiscvFFI.a $(CLASH_VEXRISCV_DATA_DIR)/Makefile + rm -f lib$(CPU_NAME)VexRiscvFFI.so + $(CXX) -shared -o lib$(CPU_NAME)VexRiscvFFI.so -Wl,--whole-archive lib$(CPU_NAME)VexRiscvFFI.a -Wl,--no-whole-archive + +../static/lib$(CPU_NAME)VexRiscvFFI.a: lib$(CPU_NAME)VexRiscvFFI.a $(CLASH_VEXRISCV_DATA_DIR)/Makefile + mkdir -p ../static + cp lib$(CPU_NAME)VexRiscvFFI.a ../static + +../dynamic/lib$(CPU_NAME)VexRiscvFFI.so: lib$(CPU_NAME)VexRiscvFFI.so $(CLASH_VEXRISCV_DATA_DIR)/Makefile + mkdir -p ../dynamic + cp lib$(CPU_NAME)VexRiscvFFI.so ../dynamic diff --git a/data/vexriscv/build.sbt b/data/vexriscv/build.sbt new file mode 100644 --- /dev/null +++ b/data/vexriscv/build.sbt @@ -0,0 +1,26 @@ +// SPDX-FileCopyrightText: 2022 Google LLC +// +// SPDX-License-Identifier: Apache-2.0 + +import Dependencies._ + +val spinalVersion = "1.12.0" + +ThisBuild / scalaVersion := "2.12.18" +ThisBuild / version := "0.1.0-SNAPSHOT" +ThisBuild / organization := "com.google" +ThisBuild / organizationName := "Google" + +lazy val root = (project in file(".")) + .settings( + name := "vexriscv-generator", + libraryDependencies ++= Seq( + "com.github.spinalhdl" %% "spinalhdl-core" % spinalVersion, + "com.github.spinalhdl" %% "spinalhdl-lib" % spinalVersion, + compilerPlugin("com.github.spinalhdl" %% "spinalhdl-idsl-plugin" % spinalVersion), + "org.scalatest" %% "scalatest" % "3.2.17", + "org.yaml" % "snakeyaml" % "1.8" + ), + ) + +// See https://www.scala-sbt.org/1.x/docs/Using-Sonatype.html for instructions on how to publish to Sonatype. diff --git a/data/vexriscv/ffi/impl.cpp b/data/vexriscv/ffi/impl.cpp new file mode 100644 --- /dev/null +++ b/data/vexriscv/ffi/impl.cpp @@ -0,0 +1,229 @@ +// SPDX-FileCopyrightText: 2022 Google LLC +// +// SPDX-License-Identifier: Apache-2.0 + +#include "interface.h" + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +typedef struct { + int server_socket, client_handle; + struct sockaddr_in server_addr; + struct sockaddr_storage server_storage; + + uint32_t timer; + socklen_t addr_size; + uint32_t self_sleep; + uint32_t check_new_connections_timer; + uint8_t rx_buffer[100]; + int32_t rx_buffer_size; + int32_t rx_buffer_remaining; + JTAG_INPUT prev_input; +} vexr_jtag_bridge_data; + +extern "C" { +vexr_jtag_bridge_data *vexr_jtag_bridge_init(uint16_t port); +void vexr_jtag_bridge_step(vexr_jtag_bridge_data *d, const JTAG_OUTPUT *output, + JTAG_INPUT *input); +void vexr_jtag_bridge_shutdown(vexr_jtag_bridge_data *bridge_data); +} + +static bool set_socket_blocking_enabled(int fd, bool blocking); +static void connection_reset(vexr_jtag_bridge_data *bridge_data); + +vexr_jtag_bridge_data *vexr_jtag_bridge_init(uint16_t port) { + vexr_jtag_bridge_data *d = new vexr_jtag_bridge_data; + + d->prev_input = {0, 0, 0}; + + d->timer = 0; + d->self_sleep = 0; + d->check_new_connections_timer = 0; + d->rx_buffer_size = 0; + d->rx_buffer_remaining = 0; + + d->server_socket = socket(PF_INET, SOCK_STREAM, 0); + assert(d->server_socket != -1); + int flag = 1; + setsockopt(d->server_socket, /* socket affected */ + IPPROTO_TCP, /* set option at TCP level */ + TCP_NODELAY, /* name of option */ + (char *)&flag, /* the cast is historical cruft */ + sizeof(int) /* length of option value */ + ); + + set_socket_blocking_enabled(d->server_socket, 0); + + d->server_addr.sin_family = AF_INET; + d->server_addr.sin_port = htons(port); + d->server_addr.sin_addr.s_addr = inet_addr("127.0.0.1"); + memset(d->server_addr.sin_zero, '\0', sizeof(d->server_addr.sin_zero)); + + bind(d->server_socket, (struct sockaddr *)&d->server_addr, + sizeof(d->server_addr)); + + listen(d->server_socket, 1); + + d->client_handle = -1; + d->addr_size = sizeof(d->server_storage); + + return d; +} + +void vexr_jtag_bridge_step(vexr_jtag_bridge_data *d, const JTAG_OUTPUT *output, + JTAG_INPUT *input) { + *input = d->prev_input; + + if (d->timer != 0) { + d->timer -= 1; + return; + } + + d->check_new_connections_timer++; + if (d->check_new_connections_timer == 200) { + d->check_new_connections_timer = 0; + int new_client_handle = accept( + d->server_socket, (struct sockaddr *)&d->server_storage, &d->addr_size); + if (new_client_handle != -1) { + if (d->client_handle != -1) { + connection_reset(d); + } + d->client_handle = new_client_handle; + } else if (d->client_handle == -1) { + d->self_sleep = 200; + } + } + + if (d->self_sleep) { + d->self_sleep--; + return; + } + + if (d->client_handle != -1) { + int n; + + if (d->rx_buffer_remaining == 0) { + if (ioctl(d->client_handle, FIONREAD, &n) != 0) { + connection_reset(d); + return; + } + if (n >= 1) { + d->rx_buffer_size = + read(d->client_handle, &d->rx_buffer, sizeof(d->rx_buffer)); + if (d->rx_buffer_size < 0) { + connection_reset(d); + return; + } + d->rx_buffer_remaining = d->rx_buffer_size; + } else { + d->self_sleep = 30; + return; + } + } + + if (d->rx_buffer_remaining != 0) { + char command = + d->rx_buffer[d->rx_buffer_size - (d->rx_buffer_remaining--)]; + switch (command) { + case 'R': { // Read request + char tdo_value = (output->tdo != 0) ? '1' : '0'; + if (send(d->client_handle, &tdo_value, 1, 0) == -1) { + printf("[REMOTE_BITBANG] send failed\n"); + connection_reset(d); + } + + break; + } + case '0' ... '7': { // Write tck, tms, tdi + uint8_t value = command - '0'; + input->tck = (value & 4) != 0; + input->tms = (value & 2) != 0; + input->tdi = (value & 1) != 0; + d->prev_input = *input; + break; + } + case 'Q': { // Quit + printf("[REMOTE_BITBANG] Received `Q`, closing socket.\n"); + connection_reset(d); + // Consider terminating the simulation here + printf("[REMOTE_BITBANG] Simulation will not be terminated.\n"); + break; + } + case 'B': { // Blink on + // Do not print anything, it will flood the output + break; + } + case 'b': { // Blink off + // Do not print anything, it will flood the output + break; + } + case 'r': { // Reset 0 0 + printf("[REMOTE_BITBANG] Command 'r': Reset 0 0 not implemented\n"); + break; + } + case 's': { // Reset 0 1 + printf("[REMOTE_BITBANG] Command 's': Reset 0 1 not implemented\n"); + break; + } + case 't': { // Reset 1 1 + printf("[REMOTE_BITBANG] Command 't': Reset 1 1 not implemented\n"); + break; + } + case 'u': { // Reset 1 0 + printf("[REMOTE_BITBANG] Command 'u': Reset 1 0 not implemented\n"); + break; + } + default: { + printf("[REMOTE_BITBANG] Unknown command: %c\n", command); + connection_reset(d); + break; + } + } + } + } + + d->timer = 3; +} + +void vexr_jtag_bridge_shutdown(vexr_jtag_bridge_data *bridge_data) { + if (bridge_data->client_handle != -1) { + shutdown(bridge_data->client_handle, SHUT_RDWR); + usleep(100); + } + if (bridge_data->server_socket != -1) { + close(bridge_data->server_socket); + usleep(100); + } +} + +/** Returns true on success, or false if there was an error */ +static bool set_socket_blocking_enabled(int fd, bool blocking) { + if (fd < 0) + return false; + +#ifdef WIN32 + unsigned long mode = blocking ? 0 : 1; + return (ioctlsocket(fd, FIONBIO, &mode) == 0) ? true : false; +#else + int flags = fcntl(fd, F_GETFL, 0); + if (flags < 0) + return false; + flags = blocking ? (flags & ~O_NONBLOCK) : (flags | O_NONBLOCK); + return (fcntl(fd, F_SETFL, flags) == 0) ? true : false; +#endif +} + +static void connection_reset(vexr_jtag_bridge_data *bridge_data) { + printf("[JTAG BRIDGE] closed connection\n"); + shutdown(bridge_data->client_handle, SHUT_RDWR); + bridge_data->client_handle = -1; +} diff --git a/data/vexriscv/ffi/interface.h b/data/vexriscv/ffi/interface.h new file mode 100644 --- /dev/null +++ b/data/vexriscv/ffi/interface.h @@ -0,0 +1,67 @@ +// SPDX-FileCopyrightText: 2022 Google LLC +// +// SPDX-License-Identifier: Apache-2.0 + +#ifndef VEX_RISCV_FFI_H +#define VEX_RISCV_FFI_H + +#include + +typedef int bit; + +typedef struct { + bit reset; + bit timerInterrupt; + bit externalInterrupt; + bit softwareInterrupt; +} NON_COMB_INPUT; + +typedef struct { + bit iBusWishbone_ACK; + uint32_t iBusWishbone_DAT_MISO; + bit iBusWishbone_ERR; + + bit dBusWishbone_ACK; + uint32_t dBusWishbone_DAT_MISO; + bit dBusWishbone_ERR; + + bit jtag_TCK; + bit jtag_TMS; + bit jtag_TDI; +} COMB_INPUT; + +typedef struct { + bit iBusWishbone_CYC; + bit iBusWishbone_STB; + bit iBusWishbone_WE; + uint32_t iBusWishbone_ADR; + uint32_t iBusWishbone_DAT_MOSI; + uint8_t iBusWishbone_SEL; + uint8_t iBusWishbone_CTI; + uint8_t iBusWishbone_BTE; + + bit dBusWishbone_CYC; + bit dBusWishbone_STB; + bit dBusWishbone_WE; + uint32_t dBusWishbone_ADR; + uint32_t dBusWishbone_DAT_MOSI; + uint8_t dBusWishbone_SEL; + uint8_t dBusWishbone_CTI; + uint8_t dBusWishbone_BTE; + + bit ndmreset; + bit stoptime; + bit jtag_TDO; +} OUTPUT; + +typedef struct { + bit tck; + bit tms; + bit tdi; +} JTAG_INPUT; + +typedef struct { + bit tdo; +} JTAG_OUTPUT; + +#endif diff --git a/data/vexriscv/ffi/vimpl.cpp b/data/vexriscv/ffi/vimpl.cpp new file mode 100644 --- /dev/null +++ b/data/vexriscv/ffi/vimpl.cpp @@ -0,0 +1,148 @@ +// SPDX-FileCopyrightText: 2022 Google LLC +// +// SPDX-License-Identifier: Apache-2.0 +#include "V__CPU_NAME__VexRiscv.h" +#include "interface.h" +#include "verilated.h" +#include +#include + +// Unique function names for: V__CPU_NAME__VexRiscv +extern "C" { +V__CPU_NAME__VexRiscv *V__CPU_NAME__VexRiscv_init(); +VerilatedVcdC *V__CPU_NAME__VexRiscv_init_vcd(V__CPU_NAME__VexRiscv *top, + const char *path); +void V__CPU_NAME__VexRiscv_shutdown(V__CPU_NAME__VexRiscv *top); + +void V__CPU_NAME__VexRiscv_init_stage1(VerilatedVcdC *vcd, + uint64_t dom_period_fs, + V__CPU_NAME__VexRiscv *top, + const NON_COMB_INPUT *input, + OUTPUT *output); +void V__CPU_NAME__VexRiscv_init_stage2(V__CPU_NAME__VexRiscv *top, + const COMB_INPUT *input); +void V__CPU_NAME__VexRiscv_step_rising_edge(VerilatedVcdC *vcd, + V__CPU_NAME__VexRiscv *top, + uint64_t time_add, + const NON_COMB_INPUT *input, + OUTPUT *output); +void V__CPU_NAME__VexRiscv_step_falling_edge(VerilatedVcdC *vcd, + V__CPU_NAME__VexRiscv *top, + uint64_t time_add, + const COMB_INPUT *input); +} + +V__CPU_NAME__VexRiscv *V__CPU_NAME__VexRiscv_init() { + VerilatedContext *ctx = new VerilatedContext; + V__CPU_NAME__VexRiscv *v = new V__CPU_NAME__VexRiscv(ctx); + v->clk = false; + return v; +} + +VerilatedVcdC *V__CPU_NAME__VexRiscv_init_vcd(V__CPU_NAME__VexRiscv *top, + const char *path) { + VerilatedVcdC *vcd = new VerilatedVcdC; + Verilated::traceEverOn(true); + top->trace(vcd, 99); + vcd->open(path); + return vcd; +} + +static void set_non_comb_inputs(V__CPU_NAME__VexRiscv *top, + const NON_COMB_INPUT *input) { + top->reset = input->reset; + top->timerInterrupt = input->timerInterrupt; + top->externalInterrupt = input->externalInterrupt; + top->softwareInterrupt = input->softwareInterrupt; +} + +static void set_comb_inputs(V__CPU_NAME__VexRiscv *top, + const COMB_INPUT *input) { + top->iBusWishbone_ACK = input->iBusWishbone_ACK; + top->iBusWishbone_DAT_MISO = input->iBusWishbone_DAT_MISO; + top->iBusWishbone_ERR = input->iBusWishbone_ERR; + top->dBusWishbone_ACK = input->dBusWishbone_ACK; + top->dBusWishbone_DAT_MISO = input->dBusWishbone_DAT_MISO; + top->dBusWishbone_ERR = input->dBusWishbone_ERR; + top->jtag_tck = input->jtag_TCK; + top->jtag_tms = input->jtag_TMS; + top->jtag_tdi = input->jtag_TDI; +} + +static void set_outputs(V__CPU_NAME__VexRiscv *top, OUTPUT *output) { + output->iBusWishbone_CYC = top->iBusWishbone_CYC; + output->iBusWishbone_STB = top->iBusWishbone_STB; + output->iBusWishbone_WE = top->iBusWishbone_WE; + output->iBusWishbone_ADR = top->iBusWishbone_ADR; + output->iBusWishbone_DAT_MOSI = top->iBusWishbone_DAT_MOSI; + output->iBusWishbone_SEL = top->iBusWishbone_SEL; + output->iBusWishbone_CTI = top->iBusWishbone_CTI; + output->iBusWishbone_BTE = top->iBusWishbone_BTE; + output->dBusWishbone_CYC = top->dBusWishbone_CYC; + output->dBusWishbone_STB = top->dBusWishbone_STB; + output->dBusWishbone_WE = top->dBusWishbone_WE; + output->dBusWishbone_ADR = top->dBusWishbone_ADR; + output->dBusWishbone_DAT_MOSI = top->dBusWishbone_DAT_MOSI; + output->dBusWishbone_SEL = top->dBusWishbone_SEL; + output->dBusWishbone_CTI = top->dBusWishbone_CTI; + output->dBusWishbone_BTE = top->dBusWishbone_BTE; + output->ndmreset = top->ndmreset; + output->stoptime = top->stoptime; + output->jtag_TDO = top->jtag_tdo; +} + +void V__CPU_NAME__VexRiscv_init_stage1(VerilatedVcdC *vcd, + uint64_t dom_period_fs, + V__CPU_NAME__VexRiscv *top, + const NON_COMB_INPUT *input, + OUTPUT *output) { + VerilatedContext *ctx = top->contextp(); + set_non_comb_inputs(top, input); + top->eval(); + if (vcd != NULL) { + vcd->dump(ctx->time()); + } + set_outputs(top, output); + ctx->timeInc(dom_period_fs); +} + +void V__CPU_NAME__VexRiscv_init_stage2(V__CPU_NAME__VexRiscv *top, + const COMB_INPUT *input) { + set_comb_inputs(top, input); +} + +void V__CPU_NAME__VexRiscv_step_rising_edge(VerilatedVcdC *vcd, + V__CPU_NAME__VexRiscv *top, + uint64_t time_add, + const NON_COMB_INPUT *input, + OUTPUT *output) { + VerilatedContext *ctx = top->contextp(); + set_non_comb_inputs(top, input); + top->clk = true; + top->eval(); + if (vcd != NULL) { + vcd->dump(ctx->time()); + } + set_outputs(top, output); + ctx->timeInc(time_add); +} + +void V__CPU_NAME__VexRiscv_step_falling_edge(VerilatedVcdC *vcd, + V__CPU_NAME__VexRiscv *top, + uint64_t time_add, + const COMB_INPUT *input) { + VerilatedContext *ctx = top->contextp(); + set_comb_inputs(top, input); + top->clk = false; + top->eval(); + if (vcd != NULL) { + vcd->dump(ctx->time()); + } + ctx->timeInc(time_add); +} + +void V__CPU_NAME__VexRiscv_shutdown(V__CPU_NAME__VexRiscv *top) { + VerilatedContext *ctx = top->contextp(); + delete top; + delete ctx; +} diff --git a/data/vexriscv/lib/build-vexriscv.py b/data/vexriscv/lib/build-vexriscv.py new file mode 100644 --- /dev/null +++ b/data/vexriscv/lib/build-vexriscv.py @@ -0,0 +1,38 @@ +#!/usr/bin/env python3 +""" +Usage: + + python3 build-vexriscv.py +""" +# SPDX-FileCopyrightText: 2022 Google LLC +# +# SPDX-License-Identifier: Apache-2.0 + +import glob +import os +import shutil +import subprocess +import sys +import tempfile + +def main(repo, commit_hash): + if glob.glob(f"vexriscv_*-{commit_hash}.jar"): + print(f"JAR for commit {commit_hash} already exists, not rebuilding.") + return + + with tempfile.TemporaryDirectory() as temp_dir: + # Build new JAR + subprocess.check_call(["git", "clone", repo, temp_dir]) + subprocess.check_call(["git", "checkout", commit_hash], cwd=temp_dir) + subprocess.check_call(["flock", "/tmp/lock", "sbt", "package"], cwd=temp_dir) + + # Find and copy new JAR + jar_path = glob.glob(os.path.join(temp_dir, "target", "scala-*", "vexriscv_*.jar"))[0] + jar_filename = os.path.basename(jar_path) + jar_base, jar_ext = os.path.splitext(jar_filename) + new_jar_filename = f"{jar_base}-{commit_hash}{jar_ext}" + shutil.move(jar_path, new_jar_filename) + + +if __name__ == '__main__': + main(sys.argv[1], sys.argv[2]) diff --git a/data/vexriscv/lib/vexriscv_2.12-2.0.0-09aa2d6881e36201775eee46b54d9f292ee4b10f.jar b/data/vexriscv/lib/vexriscv_2.12-2.0.0-09aa2d6881e36201775eee46b54d9f292ee4b10f.jar new file mode 100644 # file too large to diff: data/vexriscv/lib/vexriscv_2.12-2.0.0-09aa2d6881e36201775eee46b54d9f292ee4b10f.jar diff --git a/data/vexriscv/project/Dependencies.scala b/data/vexriscv/project/Dependencies.scala new file mode 100644 --- /dev/null +++ b/data/vexriscv/project/Dependencies.scala @@ -0,0 +1,9 @@ +// SPDX-FileCopyrightText: 2022 Google LLC +// +// SPDX-License-Identifier: CC0-1.0 + +import sbt._ + +object Dependencies { + lazy val scalaTest = "org.scalatest" %% "scalatest" % "3.2.11" +} diff --git a/data/vexriscv/project/build.properties b/data/vexriscv/project/build.properties new file mode 100644 --- /dev/null +++ b/data/vexriscv/project/build.properties @@ -0,0 +1,5 @@ +# SPDX-FileCopyrightText: 2022 Google LLC +# +# SPDX-License-Identifier: CC0-1.0 + +sbt.version=1.10.1 diff --git a/src/VexRiscv.hs b/src/VexRiscv.hs new file mode 100644 --- /dev/null +++ b/src/VexRiscv.hs @@ -0,0 +1,14 @@ +-- SPDX-FileCopyrightText: 2025 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 + +module VexRiscv ( + CpuIn (..), + CpuOut (..), + DumpVcd (..), + Jtag, + JtagIn (..), + JtagOut (..), +) where + +import VexRiscv.Internal diff --git a/src/VexRiscv/BlackBox.hs b/src/VexRiscv/BlackBox.hs new file mode 100644 --- /dev/null +++ b/src/VexRiscv/BlackBox.hs @@ -0,0 +1,216 @@ +-- SPDX-FileCopyrightText: 2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PostfixOperators #-} +{-# OPTIONS_HADDOCK hide #-} + +module VexRiscv.BlackBox where + +import Prelude + +import Clash.Core.TermLiteral (TermLiteral (termToData)) +import Control.Monad.State (State) +import Data.Either (lefts) +import Data.List.Infinite (Infinite (..), (...)) +import Data.String (fromString) +import Data.Text (Text) +import Data.Text.Prettyprint.Doc.Extra (Doc) +import GHC.Stack (HasCallStack) +import Text.Show.Pretty (ppShow) + +import Clash.Backend (Backend) +import Clash.Netlist.Types (BlackBox (BBFunction), BlackBoxContext, TemplateFunction (..)) + +import qualified Clash.Netlist.BlackBox.Types as N +import qualified Clash.Netlist.Id as Id +import qualified Clash.Netlist.Types as N +import qualified Clash.Primitives.DSL as DSL + +listToTup5 :: (HasCallStack) => [a] -> (a, a, a, a, a) +listToTup5 [a, b, c, d, e] = (a, b, c, d, e) +listToTup5 _ = error "listToTup5: list must have 5 elements" + +listToTup3 :: (HasCallStack) => [a] -> (a, a, a) +listToTup3 [a, b, c] = (a, b, c) +listToTup3 _ = error "listToTup3: list must have 3 elements" + +vexRiscvBBF :: (HasCallStack) => N.BlackBoxFunction +vexRiscvBBF _isD _primName args _resTys + | moduleNameTerm : verilogTerm : _ <- lefts args = + case (termToData moduleNameTerm, termToData verilogTerm) of + (Left term, _) -> pure $ Left $ "vexRiscvBBF: expected module name as string literal, got: " ++ show term + (_, Left term) -> pure $ Left $ "vexRiscvBBF: expected verilog source as string literal, got: " ++ show term + (Right moduleName, Right verilog) -> + pure $ Right (bbMeta moduleName verilog, bb) + where + bbMeta moduleName verilog = + N.emptyBlackBoxMeta + { N.bbKind = N.TDecl + , N.bbIncludes = [((moduleName, "v"), BBFunction (show 'vexRiscvVerilogTF) 0 (vexRiscvVerilogTF verilog))] + } + + bb :: N.BlackBox + bb = N.BBFunction (show 'vexRiscvTF) 0 vexRiscvTF +vexRiscvBBF _isD _primName _args _resTys = pure $ Left "vexRiscvBBF: unexpected arguments" + +vexRiscvVerilogTF :: String -> TemplateFunction +vexRiscvVerilogTF verilog = TemplateFunction [] (const True) $ \_bbCtx -> do + pure $ fromString verilog + +vexRiscvTF :: TemplateFunction +vexRiscvTF = + let moduleName :< verilog :< clk :< rst :< cpuIn :< jtagIn :< _ = (0 ...) + in TemplateFunction [moduleName, verilog, clk, rst, cpuIn, jtagIn] (const True) vexRiscvTF# + +vexRiscvTF# :: (Backend backend) => BlackBoxContext -> State backend Doc +vexRiscvTF# bbCtx + | [moduleNameExpr, _verilog, clk, rst, cpuIn, jtagIn] <- map fst (DSL.tInputs bbCtx) + , Just moduleName <- DSL.getStr moduleNameExpr + , [outTy@(N.Product _ _ [cpuOutTy, jtagOutTy])] <- map snd (N.bbResults bbCtx) + , N.Product _ _ [iWishboneM2Sty, dWishboneM2Sty, ndmresetTy, stoptimeTy] <- cpuOutTy + , N.Product _ _ [adrTy, datMosiTy, selTy, _lockTy, cycTy, stbTy, weTy, ctiTy, bteTy] <- iWishboneM2Sty + , tdoTy <- jtagOutTy = do + let + compName :: Text + compName = fromString moduleName + + instName <- Id.make (compName <> "_inst") + DSL.declarationReturn bbCtx (compName <> "_block") $ do + ( timerInterrupt + , externalInterrupt + , softwareInterrupt + , iBusWbS2M + , dBusWbS2M + ) <- + listToTup5 <$> DSL.deconstructProduct cpuIn ["timerInt", "extInt", "softInt", "iBusWbS2M", "dBusWbS2M"] + + ( iBusWishbone_DAT_MISO + , iBusWishbone_ACK + , iBusWishbone_ERR + , _iBusWishbone_STL + , _iBusWishbone_RTY + ) <- + listToTup5 <$> DSL.deconstructProduct iBusWbS2M ["i_rdata", "i_ack", "i_err", "i_stall", "i_retry"] + + ( dBusWishbone_DAT_MISO + , dBusWishbone_ACK + , dBusWishbone_ERR + , _dBusWishbone_STL + , _dBusWishbone_RTY + ) <- + listToTup5 <$> DSL.deconstructProduct dBusWbS2M ["d_rdata", "d_ack", "d_err", "d_stall", "d_retry"] + + ( tck + , tms + , tdi + ) <- + listToTup3 <$> DSL.deconstructProduct jtagIn ["tck", "tms", "tdi"] + + iBusWishbone_CYC <- DSL.declare "i_cyc" cycTy + iBusWishbone_STB <- DSL.declare "i_stb" stbTy + iBusWishbone_WE <- DSL.declare "i_we" weTy + iBusWishbone_ADR <- DSL.declare "i_adr" adrTy + iBusWishbone_DAT_MOSI <- DSL.declare "i_dat_mosi" datMosiTy + iBusWishbone_SEL <- DSL.declare "i_sel" selTy + iBusWishbone_CTI <- DSL.declare "i_cti" ctiTy + iBusWishbone_BTE <- DSL.declare "i_bte" bteTy + + dBusWishbone_CYC <- DSL.declare "d_cyc" cycTy + dBusWishbone_STB <- DSL.declare "d_stb" stbTy + dBusWishbone_WE <- DSL.declare "d_we" weTy + dBusWishbone_ADR <- DSL.declare "d_adr" adrTy + dBusWishbone_DAT_MOSI <- DSL.declare "d_dat_mosi" datMosiTy + dBusWishbone_SEL <- DSL.declare "d_sel" selTy + dBusWishbone_CTI <- DSL.declare "d_cti" ctiTy + dBusWishbone_BTE <- DSL.declare "d_bte" bteTy + + tdo <- DSL.declare "tdo" tdoTy + + ndmreset <- DSL.declare "ndmreset" ndmresetTy + stoptime <- DSL.declare "stoptime" stoptimeTy + + let + generics = [] + + inps :: [(Text, DSL.TExpr)] + inps = + [ ("clk", clk) + , ("reset", rst) + , ("timerInterrupt", timerInterrupt) + , ("externalInterrupt", externalInterrupt) + , ("softwareInterrupt", softwareInterrupt) + , ("iBusWishbone_DAT_MISO", iBusWishbone_DAT_MISO) + , ("iBusWishbone_ACK", iBusWishbone_ACK) + , ("iBusWishbone_ERR", iBusWishbone_ERR) + , ("dBusWishbone_DAT_MISO", dBusWishbone_DAT_MISO) + , ("dBusWishbone_ACK", dBusWishbone_ACK) + , ("dBusWishbone_ERR", dBusWishbone_ERR) + , ("jtag_tms", tms) + , ("jtag_tdi", tdi) + , ("jtag_tck", tck) + ] + + outs :: [(Text, DSL.TExpr)] + outs = + [ ("iBusWishbone_CYC", iBusWishbone_CYC) + , ("iBusWishbone_STB", iBusWishbone_STB) + , ("iBusWishbone_WE", iBusWishbone_WE) + , ("iBusWishbone_ADR", iBusWishbone_ADR) + , ("iBusWishbone_DAT_MOSI", iBusWishbone_DAT_MOSI) + , ("iBusWishbone_SEL", iBusWishbone_SEL) + , ("iBusWishbone_CTI", iBusWishbone_CTI) + , ("iBusWishbone_BTE", iBusWishbone_BTE) + , ("dBusWishbone_CYC", dBusWishbone_CYC) + , ("dBusWishbone_STB", dBusWishbone_STB) + , ("dBusWishbone_WE", dBusWishbone_WE) + , ("dBusWishbone_ADR", dBusWishbone_ADR) + , ("dBusWishbone_DAT_MOSI", dBusWishbone_DAT_MOSI) + , ("dBusWishbone_SEL", dBusWishbone_SEL) + , ("dBusWishbone_CTI", dBusWishbone_CTI) + , ("dBusWishbone_BTE", dBusWishbone_BTE) + , ("jtag_tdo", tdo) + , ("ndmreset", ndmreset) + , ("stoptime", stoptime) + ] + + DSL.instDecl N.Empty (Id.unsafeMake compName) instName generics inps outs + + let + iWishboneOut = + DSL.constructProduct + iWishboneM2Sty + [ iBusWishbone_ADR + , iBusWishbone_DAT_MOSI + , iBusWishbone_SEL + , DSL.litTExpr (DSL.B False) + , iBusWishbone_CYC + , iBusWishbone_STB + , iBusWishbone_WE + , iBusWishbone_CTI + , iBusWishbone_BTE + ] + + dWishboneOut = + DSL.constructProduct + dWishboneM2Sty + [ dBusWishbone_ADR + , dBusWishbone_DAT_MOSI + , dBusWishbone_SEL + , DSL.litTExpr (DSL.B False) + , dBusWishbone_CYC + , dBusWishbone_STB + , dBusWishbone_WE + , dBusWishbone_CTI + , dBusWishbone_BTE + ] + + pure + [ DSL.constructProduct + outTy + [ DSL.constructProduct cpuOutTy [iWishboneOut, dWishboneOut, ndmreset, stoptime] + , tdo + ] + ] +vexRiscvTF# bbCtx = error (ppShow bbCtx) diff --git a/src/VexRiscv/ClockTicks.hs b/src/VexRiscv/ClockTicks.hs new file mode 100644 --- /dev/null +++ b/src/VexRiscv/ClockTicks.hs @@ -0,0 +1,412 @@ +-- SPDX-FileCopyrightText: 2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE NamedFieldPuns #-} + +{- | Utilities dealing with clock ticks and edges (and absolute+relative + event timings) in Clash. + +This file was added when we were working on adding JTAG support on a +separate domain. For that, handling two different clocks and their edges +(and timing for simulation) was important. + +We decided to keep JTAG on the CPU domain, so all functions except +'singleClockEdgesRelative' and 'singleClockEdgesAbsolute' are unused. + + +TODO: Figure out whether we want to upstream as is, or whether we want to + generalize to /N/ clocks first. +-} +module VexRiscv.ClockTicks ( + ClockEdgeAB (..), + clockTicksAbsolute, + clockTicksRelative, + clockEdgesAbsolute, + clockEdgesRelative, + singleClockEdgesAbsolute, + singleClockEdgesRelative, +) where + +import Clash.Promoted.Nat (snatToNum) +import Clash.Signal ( + ActiveEdge (..), + Clock, + KnownDomain, + SActiveEdge (..), + SDomainConfiguration (..), + activeEdge, + knownDomain, + ) +import Clash.Signal.Internal (Clock (..), ClockAB (..), Femtoseconds (..), Signal ((:-))) +import Data.Coerce (coerce) +import Data.Int (Int64) +import Data.List (mapAccumL) +import Data.Ord () +import Prelude + +{- | Given two clocks, produce a list of clock ticks indicating which clock +(or both) ticked. Can be used in components handling multiple clocks, such +as @unsafeSynchronizer@ or dual clock FIFOs. In contrast to 'clockTicks', +this version also produces the absolute time at which the tick happened. + +If your primitive does not care about coincided clock edges, it should - by +convention - replace it by @ClockB:ClockA:@. + +Returned time is in /femtoseconds/. +-} +clockTicksAbsolute :: + (KnownDomain domA, KnownDomain domB) => + Clock domA -> + Clock domB -> + [(Int64, ClockAB)] +clockTicksAbsolute clkA clkB = + clockTicksEitherAbsolute (toEither clkA) (toEither clkB) + +{- | Given two clocks, produce a list of clock ticks indicating which clock +(or both) ticked. Can be used in components handling multiple clocks, such +as @unsafeSynchronizer@ or dual clock FIFOs. In contrast to 'clockTicks', +this version also produces the time since the last tick. Note that the first +"time since last tick" is always zero. + +If your primitive does not care about coincided clock edges, it should - by +convention - replace it by @ClockB:ClockA:@. + +Returned time is in /femtoseconds/. +-} +clockTicksRelative :: + (KnownDomain domA, KnownDomain domB) => + Clock domA -> + Clock domB -> + [(Int64, ClockAB)] +clockTicksRelative clkA clkB = + clockTicksEitherRelative (toEither clkA) (toEither clkB) + +{- | Given two clocks, produce a list of clock ticks indicating which clock +(or both) ticked. Can be used in components handling multiple clocks, such +as @unsafeSynchronizer@ or dual clock FIFOs. + +If your primitive does not care about coincided clock edges, it should - by +convention - replace it by @ClockEdgeB edgeB : ClockEdgeA edgeA:@. + +Returned time is in /femtoseconds/. +-} +clockEdgesAbsolute :: + forall domA domB. + (KnownDomain domA, KnownDomain domB) => + Clock domA -> + Clock domB -> + [(Int64, ClockEdgeAB)] +clockEdgesAbsolute clkA clkB = + clockEdgesEitherAbsolute + (toActiveEdge (activeEdge @domA)) + (toActiveEdge (activeEdge @domB)) + (toEither clkA) + (toEither clkB) + +{- | Given two clocks, produce a list of clock ticks indicating which clock +(or both) ticked. Can be used in components handling multiple clocks, such +as @unsafeSynchronizer@ or dual clock FIFOs. + +If your primitive does not care about coincided clock edges, it should - by +convention - replace it by @ClockEdgeB edgeB : ClockEdgeA edgeA:@. + +Returned time is in /femtoseconds/. +-} +clockEdgesRelative :: + forall domA domB. + (KnownDomain domA, KnownDomain domB) => + Clock domA -> + Clock domB -> + [(Int64, ClockEdgeAB)] +clockEdgesRelative clkA clkB = + clockEdgesEitherRelative + (toActiveEdge (activeEdge @domA)) + (toActiveEdge (activeEdge @domB)) + (toEither clkA) + (toEither clkB) + +{- | Given a clock, produce a list of clock edges and the time at which the +edge occurs. + +This can be used for simulating designs that need to advance time to get +accurate traces. + +Returned time is in /femotseconds/. +-} +singleClockEdgesAbsolute :: + forall dom. + (KnownDomain dom) => + Clock dom -> + [(Int64, ActiveEdge)] +singleClockEdgesAbsolute clk = + singleClockEdgesEitherAbsolute + (toActiveEdge (activeEdge @dom)) + (toEither clk) + +{- | Given a clock, produce a list of clock edges and the time since the last +edge. + +This can be used for simulating designs that need to advance time to get +accurate traces. + +Returned time is in /femotseconds/. +-} +singleClockEdgesRelative :: + forall dom. + (KnownDomain dom) => + Clock dom -> + [(Int64, ActiveEdge)] +singleClockEdgesRelative clk = + singleClockEdgesEitherRelative + (toActiveEdge (activeEdge @dom)) + (toEither clk) + +-- | GADT version of 'ActiveEdge' to 'ActiveEdge' conversion +toActiveEdge :: SActiveEdge edge -> ActiveEdge +toActiveEdge SRising = Rising +toActiveEdge SFalling = Falling + +toEither :: + forall dom. + (KnownDomain dom) => + Clock dom -> + Either Int64 (Signal dom Int64) +toEither (Clock _ maybePeriods) + | Just periods <- maybePeriods = + Right (unFemtosecondsSignal periods) + | SDomainConfiguration{sPeriod} <- knownDomain @dom = + -- Convert to femtoseconds - dynamic clocks use them + Left (1000 * snatToNum sPeriod) + where + -- Coerce whole signal instead of `fmap coerce` to prevent useless constructor + -- packing and unpacking. + unFemtosecondsSignal :: Signal dom Femtoseconds -> Signal dom Int64 + unFemtosecondsSignal = coerce + +{- | Given two clock periods, produce a list of clock ticks indicating which clock +(or both) ticked. Can be used in components handling multiple clocks, such +as @unsafeSynchronizer@ or dual clock FIFOs. In contrast to 'clockTicksEither', +this version also produces the absolute time at which the event happened. + +If your primitive does not care about coincided clock edges, it should - by +convention - replace it by @ClockB:ClockA:@. +-} +clockTicksEitherAbsolute :: + Either Int64 (Signal domA Int64) -> + Either Int64 (Signal domB Int64) -> + [(Int64, ClockAB)] +clockTicksEitherAbsolute clkA clkB = + case (clkA, clkB) of + (Left tA, Left tB) | tA == tB -> zip (iterate (+ tA) 0) (repeat ClockAB) + (Left tA, Left tB) -> goStatic 0 0 tA tB + (Right tA, Right tB) -> goDynamic 0 0 tA tB + (Left tA, Right tB) -> clockTicksEitherAbsolute (Right (pure tA)) (Right tB) + (Right tA, Left tB) -> clockTicksEitherAbsolute (Right tA) (Right (pure tB)) + where +{- FOURMOLU_DISABLE -} + goStatic :: Int64 -> Int64 -> Int64 -> Int64 -> [(Int64, ClockAB)] + goStatic absTimeA absTimeB tA tB = + case compare absTimeA absTimeB of + LT -> (absTimeA, ClockA) : goStatic (absTimeA + tA) absTimeB tA tB + EQ -> (absTimeA, ClockAB) : goStatic (absTimeA + tA) (absTimeB + tB) tA tB + GT -> (absTimeB, ClockB) : goStatic absTimeA (absTimeB + tB) tA tB + + goDynamic :: Int64 -> Int64 -> Signal domA Int64 -> Signal domB Int64 -> [(Int64, ClockAB)] + goDynamic absTimeA absTimeB tsA@(~(tA :- tsA0)) tsB@(~(tB :- tsB0)) = + -- Even though we lazily match on the signal's constructor, this shouldn't + -- build up a significant chain of chunks as 'absTimeX' gets evaluated + -- every iteration. + case compare absTimeA absTimeB of + LT -> (absTimeA, ClockA) : goDynamic (absTimeA + tA) absTimeB tsA0 tsB + EQ -> (absTimeA, ClockAB) : goDynamic (absTimeA + tA) (absTimeB + tB) tsA0 tsB0 + GT -> (absTimeB, ClockB) : goDynamic absTimeA (absTimeB + tB) tsA tsB0 +{- FOURMOLU_ENABLE -} + +{- | Given two clock periods, produce a list of clock ticks indicating which clock +(or both) ticked. Can be used in components handling multiple clocks, such +as @unsafeSynchronizer@ or dual clock FIFOs. In contrast to 'clockTicksEither', +this version also produces the time since the last event. + +If your primitive does not care about coincided clock edges, it should - by +convention - replace it by @ClockB:ClockA:@. +-} +clockTicksEitherRelative :: + Either Int64 (Signal domA Int64) -> + Either Int64 (Signal domB Int64) -> + [(Int64, ClockAB)] +clockTicksEitherRelative clkA clkB = zip relativeTimestamps ticks + where + relativeTimestamps = 0 : zipWith (-) (drop 1 timestamps) timestamps + (timestamps, ticks) = unzip (clockTicksEitherAbsolute clkA clkB) + +-- | Flip edge from rising to falling, and vice versa +oppositeEdge :: ActiveEdge -> ActiveEdge +oppositeEdge Rising = Falling +oppositeEdge Falling = Rising + +data ClockEdgeAB + = ClockEdgeA !ActiveEdge + | ClockEdgeB !ActiveEdge + | ClockEdgeAB !ActiveEdge !ActiveEdge + deriving (Show, Eq) + +{- | Given two clock periods, produce a list of clock ticks indicating which clock +(or both) ticked. Can be used in components handling multiple clocks, such +as @unsafeSynchronizer@ or dual clock FIFOs. In contrast to 'clockTicksEither', +this version also produces the absolute time at which the event happened. + +If your primitive does not care about coincided clock edges, it should - by +convention - replace it by @ClockEdgeB edgeB : ClockEdgeA edgeA:@. +-} +clockEdgesEitherAbsolute :: + -- | First active edge for clock A + ActiveEdge -> + -- | First active edge for clock B + ActiveEdge -> + -- | Clock periods for clock A + Either Int64 (Signal domA Int64) -> + -- | Clock periods for clock B + Either Int64 (Signal domB Int64) -> + [(Int64, ClockEdgeAB)] +clockEdgesEitherAbsolute firstEdgeA firstEdgeB clkA clkB = + case (clkA, clkB) of + (Left tA, Left tB) | tA == tB -> goSame (halve tA) + (Left tA, Left tB) -> goStatic 0 0 firstEdgeA firstEdgeB (halve tA) (halve tB) + (Right tA, Right tB) -> goDynamic 0 0 firstEdgeA firstEdgeB (halves tA) (halves tB) + (Left tA, Right tB) -> + clockEdgesEitherAbsolute firstEdgeA firstEdgeB (Right (pure tA)) (Right tB) + (Right tA, Left tB) -> + clockEdgesEitherAbsolute firstEdgeA firstEdgeB (Right tA) (Right (pure tB)) + where + halves = go . fmap halve + where + go ((t0, t1) :- ts) = t0 :- t1 :- go ts + + halve t = + ( t `div` 2 + , t - (t `div` 2) + ) + + goSame :: (Int64, Int64) -> [(Int64, ClockEdgeAB)] + goSame (t0, t1) = + zip + (snd $ mapAccumL (\acc t -> (acc + t, acc)) 0 (cycle [t0, t1])) + ( cycle + [ ClockEdgeAB firstEdgeA firstEdgeB + , ClockEdgeAB (oppositeEdge firstEdgeA) (oppositeEdge firstEdgeB) + ] + ) + +{- FOURMOLU_DISABLE -} + goStatic :: + Int64 -> + Int64 -> + ActiveEdge -> + ActiveEdge -> + (Int64, Int64) -> + (Int64, Int64) -> + [(Int64, ClockEdgeAB)] + goStatic absTimeA absTimeB !edgeA !edgeB (tA0, tA1) (tB0, tB1) = + case compare absTimeA absTimeB of + -- XXX: Sorry for breaking the 80/90 limit. I have no idea how to break this + -- over multiple lines without sacrificing readability. + LT -> (absTimeA, ClockEdgeA edgeA) : goStatic (absTimeA + tA0) absTimeB (oppositeEdge edgeA) edgeB (tA1, tA0) (tB0, tB1) + EQ -> (absTimeA, ClockEdgeAB edgeA edgeB) : goStatic (absTimeA + tA0) (absTimeB + tB0) (oppositeEdge edgeA) (oppositeEdge edgeB) (tA1, tA0) (tB1, tB0) + GT -> (absTimeB, ClockEdgeB edgeB) : goStatic absTimeA (absTimeB + tB0) edgeA (oppositeEdge edgeB) (tA0, tA1) (tB1, tB0) + + goDynamic :: + Int64 -> + Int64 -> + ActiveEdge -> + ActiveEdge -> + Signal domA Int64 -> + Signal domB Int64 -> + [(Int64, ClockEdgeAB)] + goDynamic absTimeA absTimeB edgeA edgeB tsA@(~(tA :- tsA0)) tsB@(~(tB :- tsB0)) = + -- Even though we lazily match on the signal's constructor, this shouldn't + -- build up a significant chain of chunks as 'absTimeX' gets evaluated + -- every iteration. + case compare absTimeA absTimeB of + -- XXX: Sorry for breaking the 80/90 limit. I have no idea how to break this + -- over multiple lines without sacrificing readability. + LT -> (absTimeA, ClockEdgeA edgeA) : goDynamic (absTimeA + tA) absTimeB (oppositeEdge edgeA) edgeB tsA0 tsB + EQ -> (absTimeA, ClockEdgeAB edgeA edgeB) : goDynamic (absTimeA + tA) (absTimeB + tB) (oppositeEdge edgeA) (oppositeEdge edgeB) tsA0 tsB0 + GT -> (absTimeB, ClockEdgeB edgeB) : goDynamic absTimeA (absTimeB + tB) edgeA (oppositeEdge edgeB) tsA tsB0 +{- FOURMOLU_ENABLE -} + +{- | Given two clock periods, produce a list of clock ticks indicating which clock +(or both) ticked. Can be used in components handling multiple clocks, such +as @unsafeSynchronizer@ or dual clock FIFOs. In contrast to 'clockTicksEither', +this version also produces the time since the last event. For the first edge +the time since the last event is set to zero. + +If your primitive does not care about coincided clock edges, it should - by +convention - replace it by @ClockEdgeB edgeB : ClockEdgeA edgeA:@. +-} +clockEdgesEitherRelative :: + -- | First active edge for clock A + ActiveEdge -> + -- | First active edge for clock B + ActiveEdge -> + Either Int64 (Signal domA Int64) -> + Either Int64 (Signal domB Int64) -> + [(Int64, ClockEdgeAB)] +clockEdgesEitherRelative firstEdgeA firstEdgeB clkA clkB = zip relativeTimestamps ticks + where + relativeTimestamps = 0 : zipWith (-) (drop 1 timestamps) timestamps + (timestamps, ticks) = unzip (clockEdgesEitherAbsolute firstEdgeA firstEdgeB clkA clkB) + +{- | Given the clock periods of a single clock, produce a list of clock edges +and the (absolute) times when these edges are occurring. + +Same as 'singleClockEdgesEitherRelative', but produces absolute times +(in /femotseconds/). +-} +singleClockEdgesEitherAbsolute :: + ActiveEdge -> + Either Int64 (Signal dom Int64) -> + [(Int64, ActiveEdge)] +singleClockEdgesEitherAbsolute firstEdge clk = + case clk of + Left t -> goStatic 0 firstEdge (halve t) + Right t -> goDynamic 0 firstEdge (halves t) + where + halves = go . fmap halve + where + go ((t0, t1) :- ts) = t0 :- t1 :- go ts + + halve t = + ( t `div` 2 + , t - (t `div` 2) + ) + + goStatic :: + Int64 -> + ActiveEdge -> + (Int64, Int64) -> + [(Int64, ActiveEdge)] + goStatic absTime !currentEdge (t0, t1) = + (absTime, currentEdge) : goStatic (absTime + t0) (oppositeEdge currentEdge) (t1, t0) + + goDynamic :: + Int64 -> + ActiveEdge -> + Signal domA Int64 -> + [(Int64, ActiveEdge)] + goDynamic absTime !currentEdge ~(t :- ts1) = + (absTime, currentEdge) : goDynamic (absTime + t) (oppositeEdge currentEdge) ts1 + +{- | Given the clock periods of a single clock, produce a list of clock edges +and the (relative) times since the last edge occurred. + +Same as 'singleClockEdgesEitherAbsolute', but produces relative times +(in /femotseconds/). +-} +singleClockEdgesEitherRelative :: + ActiveEdge -> + Either Int64 (Signal dom Int64) -> + [(Int64, ActiveEdge)] +singleClockEdgesEitherRelative firstEdge clk = zip relativeTimestamps edges + where + relativeTimestamps = 0 : zipWith (-) (drop 1 timestamps) timestamps + (timestamps, edges) = unzip (singleClockEdgesEitherAbsolute firstEdge clk) diff --git a/src/VexRiscv/FFI.hsc b/src/VexRiscv/FFI.hsc new file mode 100644 --- /dev/null +++ b/src/VexRiscv/FFI.hsc @@ -0,0 +1,220 @@ +-- SPDX-FileCopyrightText: 2022-2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 + +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE ForeignFunctionInterface #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +module VexRiscv.FFI where + +import Foreign.Storable +import Foreign.Ptr +import Prelude +import Clash.Prelude +import Data.Word + +#include "ffi/interface.h" + +data VexRiscvJtagBridge + +foreign import ccall unsafe "vexr_jtag_bridge_init" vexrJtagBridgeInit :: Word16 -> IO (Ptr VexRiscvJtagBridge) +foreign import ccall unsafe "vexr_jtag_bridge_step" vexrJtagBridgeStep :: Ptr VexRiscvJtagBridge -> Ptr JTAG_OUTPUT -> Ptr JTAG_INPUT -> IO () +foreign import ccall unsafe "vexr_jtag_bridge_shutdown" vexrJtagBridgeShutdown :: Ptr VexRiscvJtagBridge -> IO () + +-- | CPU input that cannot combinatorially depend on the CPU output +data NON_COMB_INPUT = NON_COMB_INPUT + { reset :: Bit + , timerInterrupt :: Bit + , externalInterrupt :: Bit + , softwareInterrupt :: Bit + } + +-- | CPU input that can combinatorially depend on the CPU output +data COMB_INPUT = COMB_INPUT + { iBusWishbone_ACK :: Bit + , iBusWishbone_DAT_MISO :: Word32 + , iBusWishbone_ERR :: Bit + + , dBusWishbone_ACK :: Bit + , dBusWishbone_DAT_MISO :: Word32 + , dBusWishbone_ERR :: Bit + + , jtag_TCK :: Bit + , jtag_TMS :: Bit + , jtag_TDI :: Bit + } + deriving (Show) + +data OUTPUT = OUTPUT + { iBusWishbone_CYC :: Bit + , iBusWishbone_STB :: Bit + , iBusWishbone_WE :: Bit + , iBusWishbone_ADR :: Word32 + , iBusWishbone_DAT_MOSI :: Word32 + , iBusWishbone_SEL :: Word8 + , iBusWishbone_CTI :: Word8 + , iBusWishbone_BTE :: Word8 + + , dBusWishbone_CYC :: Bit + , dBusWishbone_STB :: Bit + , dBusWishbone_WE :: Bit + , dBusWishbone_ADR :: Word32 + , dBusWishbone_DAT_MOSI :: Word32 + , dBusWishbone_SEL :: Word8 + , dBusWishbone_CTI :: Word8 + , dBusWishbone_BTE :: Word8 + + , ndmreset :: Bit + , stoptime :: Bit + + , jtag_TDO :: Bit + } + deriving (Show) + +data JTAG_INPUT = JTAG_INPUT + { tck :: Bit + , tms :: Bit + , tdi :: Bit + } + deriving (Show) + +data JTAG_OUTPUT = JTAG_OUTPUT + { tdo :: Bit + } + deriving (Show) + +instance Storable Bit where + alignment = alignment . bitToBool + sizeOf = sizeOf . bitToBool + peek = fmap boolToBit . peek . castPtr + poke ptr = poke (castPtr ptr) . bitToBool + +instance Storable NON_COMB_INPUT where + alignment _ = #alignment NON_COMB_INPUT + sizeOf _ = #size NON_COMB_INPUT + {-# INLINE peek #-} + peek ptr = const NON_COMB_INPUT <$> pure () + <*> (#peek NON_COMB_INPUT, reset) ptr + <*> (#peek NON_COMB_INPUT, timerInterrupt) ptr + <*> (#peek NON_COMB_INPUT, externalInterrupt) ptr + <*> (#peek NON_COMB_INPUT, softwareInterrupt) ptr + + {-# INLINE poke #-} + poke ptr this = do + (#poke NON_COMB_INPUT, reset) ptr (reset this) + (#poke NON_COMB_INPUT, timerInterrupt) ptr (timerInterrupt this) + (#poke NON_COMB_INPUT, externalInterrupt) ptr (externalInterrupt this) + (#poke NON_COMB_INPUT, softwareInterrupt) ptr (softwareInterrupt this) + return () + +instance Storable COMB_INPUT where + alignment _ = #alignment COMB_INPUT + sizeOf _ = #size COMB_INPUT + {-# INLINE peek #-} + peek ptr = const COMB_INPUT <$> pure () + <*> (#peek COMB_INPUT, iBusWishbone_ACK) ptr + <*> (#peek COMB_INPUT, iBusWishbone_DAT_MISO) ptr + <*> (#peek COMB_INPUT, iBusWishbone_ERR) ptr + <*> (#peek COMB_INPUT, dBusWishbone_ACK) ptr + <*> (#peek COMB_INPUT, dBusWishbone_DAT_MISO) ptr + <*> (#peek COMB_INPUT, dBusWishbone_ERR) ptr + <*> (#peek COMB_INPUT, jtag_TCK) ptr + <*> (#peek COMB_INPUT, jtag_TMS) ptr + <*> (#peek COMB_INPUT, jtag_TDI) ptr + + {-# INLINE poke #-} + poke ptr this = do + (#poke COMB_INPUT, iBusWishbone_ACK) ptr (iBusWishbone_ACK this) + (#poke COMB_INPUT, iBusWishbone_DAT_MISO) ptr (iBusWishbone_DAT_MISO this) + (#poke COMB_INPUT, iBusWishbone_ERR) ptr (iBusWishbone_ERR this) + + (#poke COMB_INPUT, dBusWishbone_ACK) ptr (dBusWishbone_ACK this) + (#poke COMB_INPUT, dBusWishbone_DAT_MISO) ptr (dBusWishbone_DAT_MISO this) + (#poke COMB_INPUT, dBusWishbone_ERR) ptr (dBusWishbone_ERR this) + + (#poke COMB_INPUT, jtag_TCK) ptr (jtag_TCK this) + (#poke COMB_INPUT, jtag_TMS) ptr (jtag_TMS this) + (#poke COMB_INPUT, jtag_TDI) ptr (jtag_TDI this) + return () + +instance Storable OUTPUT where + alignment _ = #alignment OUTPUT + sizeOf _ = #size OUTPUT + {-# INLINE peek #-} + peek ptr = const OUTPUT <$> pure () + <*> (#peek OUTPUT, iBusWishbone_CYC) ptr + <*> (#peek OUTPUT, iBusWishbone_STB) ptr + <*> (#peek OUTPUT, iBusWishbone_WE) ptr + <*> (#peek OUTPUT, iBusWishbone_ADR) ptr + <*> (#peek OUTPUT, iBusWishbone_DAT_MOSI) ptr + <*> (#peek OUTPUT, iBusWishbone_SEL) ptr + <*> (#peek OUTPUT, iBusWishbone_CTI) ptr + <*> (#peek OUTPUT, iBusWishbone_BTE) ptr + + <*> (#peek OUTPUT, dBusWishbone_CYC) ptr + <*> (#peek OUTPUT, dBusWishbone_STB) ptr + <*> (#peek OUTPUT, dBusWishbone_WE) ptr + <*> (#peek OUTPUT, dBusWishbone_ADR) ptr + <*> (#peek OUTPUT, dBusWishbone_DAT_MOSI) ptr + <*> (#peek OUTPUT, dBusWishbone_SEL) ptr + <*> (#peek OUTPUT, dBusWishbone_CTI) ptr + <*> (#peek OUTPUT, dBusWishbone_BTE) ptr + + <*> (#peek OUTPUT, ndmreset) ptr + <*> (#peek OUTPUT, stoptime) ptr + + <*> (#peek OUTPUT, jtag_TDO) ptr + + {-# INLINE poke #-} + poke ptr this = do + (#poke OUTPUT, iBusWishbone_CYC) ptr (iBusWishbone_CYC this) + (#poke OUTPUT, iBusWishbone_STB) ptr (iBusWishbone_STB this) + (#poke OUTPUT, iBusWishbone_WE) ptr (iBusWishbone_WE this) + (#poke OUTPUT, iBusWishbone_ADR) ptr (iBusWishbone_ADR this) + (#poke OUTPUT, iBusWishbone_DAT_MOSI) ptr (iBusWishbone_DAT_MOSI this) + (#poke OUTPUT, iBusWishbone_SEL) ptr (iBusWishbone_SEL this) + (#poke OUTPUT, iBusWishbone_CTI) ptr (iBusWishbone_CTI this) + (#poke OUTPUT, iBusWishbone_BTE) ptr (iBusWishbone_BTE this) + + (#poke OUTPUT, dBusWishbone_CYC) ptr (dBusWishbone_CYC this) + (#poke OUTPUT, dBusWishbone_STB) ptr (dBusWishbone_STB this) + (#poke OUTPUT, dBusWishbone_WE) ptr (dBusWishbone_WE this) + (#poke OUTPUT, dBusWishbone_ADR) ptr (dBusWishbone_ADR this) + (#poke OUTPUT, dBusWishbone_DAT_MOSI) ptr (dBusWishbone_DAT_MOSI this) + (#poke OUTPUT, dBusWishbone_SEL) ptr (dBusWishbone_SEL this) + (#poke OUTPUT, dBusWishbone_CTI) ptr (dBusWishbone_CTI this) + (#poke OUTPUT, dBusWishbone_BTE) ptr (dBusWishbone_BTE this) + + (#poke OUTPUT, ndmreset) ptr (ndmreset this) + (#poke OUTPUT, stoptime) ptr (stoptime this) + + (#poke OUTPUT, jtag_TDO) ptr (jtag_TDO this) + return () + +instance Storable JTAG_OUTPUT where + alignment _ = #alignment JTAG_OUTPUT + sizeOf _ = #size JTAG_OUTPUT + {-# INLINE peek #-} + peek ptr = const JTAG_OUTPUT <$> pure () + <*> (#peek JTAG_OUTPUT, tdo) ptr + + {-# INLINE poke #-} + poke ptr this = do + (#poke JTAG_OUTPUT, tdo) ptr (tdo this) + +instance Storable JTAG_INPUT where + alignment _ = #alignment JTAG_INPUT + sizeOf _ = #size JTAG_INPUT + {-# INLINE peek #-} + peek ptr = const JTAG_INPUT <$> pure () + <*> (#peek JTAG_INPUT, tck) ptr + <*> (#peek JTAG_INPUT, tms) ptr + <*> (#peek JTAG_INPUT, tdi) ptr + + {-# INLINE poke #-} + poke ptr this = do + (#poke JTAG_INPUT, tck) ptr (tck this) + (#poke JTAG_INPUT, tms) ptr (tms this) + (#poke JTAG_INPUT, tdi) ptr (tdi this) + return () diff --git a/src/VexRiscv/Internal.hs b/src/VexRiscv/Internal.hs new file mode 100644 --- /dev/null +++ b/src/VexRiscv/Internal.hs @@ -0,0 +1,267 @@ +-- SPDX-FileCopyrightText: 2022-2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE CPP #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -fconstraint-solver-iterations=10 #-} +{-# OPTIONS_HADDOCK hide #-} + +module VexRiscv.Internal where + +import Clash.Prelude +import Protocols +import Protocols.Experimental.Wishbone +import Protocols.Idle + +import VexRiscv.FFI +import VexRiscv.Random (unsafeMakeDefinedRandom) + +import Clash.Annotations.Primitive (HDL (Verilog), Primitive (InlineYamlPrimitive), hasBlackBox) +import Clash.Signal.Internal (Signal ((:-)), hzToFs, unFemtoseconds) +import Data.Bifunctor (first) +import Data.String.Interpolate (i) +import Data.Word (Word64) +import Foreign.C.String (CString, newCString) +import Foreign.Marshal (alloca) +import Foreign.Ptr (Ptr, nullPtr) +import Foreign.Storable (peek, poke) +import GHC.IO (unsafeInterleaveIO, unsafePerformIO) +import GHC.Stack (HasCallStack) +import VexRiscv.BlackBox (vexRiscvBBF) +import VexRiscv.ClockTicks (singleClockEdgesRelative) +import VexRiscv.Reset (MinCyclesReset, fromMinCycles) + +-- Opaque types for Verilator C++ model +data VexRiscv +data VerilatedVcdC + +data JtagIn = JtagIn + { testClock :: "TCK" ::: Bit + , testModeSelect :: "TMS" ::: Bit + , testDataIn :: "TDI" ::: Bit + } + deriving (Generic, Eq, NFDataX, ShowX, BitPack) + +data JtagOut = JtagOut + { testDataOut :: "TDO" ::: Bit + } + deriving (Generic, NFDataX, ShowX, Eq, BitPack) + +data CpuIn = CpuIn + { timerInterrupt :: "TIMER_INTERRUPT" ::: Bit + , externalInterrupt :: "EXTERNAL_INTERRUPT" ::: Bit + , softwareInterrupt :: "SOFTWARE_INTERRUPT" ::: Bit + , iBusWbS2M :: "IBUS_IN_" ::: WishboneS2M 4 + , dBusWbS2M :: "DBUS_IN_" ::: WishboneS2M 4 + } + deriving (Generic, NFDataX, ShowX, Eq, BitPack) + +data CpuOut = CpuOut + { iBusWbM2S :: "IBUS_OUT_" ::: WishboneM2S 30 4 + , dBusWbM2S :: "DBUS_OUT_" ::: WishboneM2S 30 4 + , ndmreset :: "RST" ::: Bit + -- ^ Peripheral reset produced by `EmbeddedRiscvJtag` plugin. + , stoptime :: "STOPTIME" ::: Bit + -- ^ Seems to be some kind of debug signal produced by the `CsrPlugin`. + } + deriving (Generic, NFDataX, ShowX, Eq, BitPack) + +inputToNonCombInput :: Bool -> CpuIn -> NON_COMB_INPUT +inputToNonCombInput rst cpuIn = + NON_COMB_INPUT + { reset = boolToBit (unsafeMakeDefinedRandom rst) + , timerInterrupt = unsafeMakeDefinedRandom timerInterrupt + , externalInterrupt = unsafeMakeDefinedRandom externalInterrupt + , softwareInterrupt = unsafeMakeDefinedRandom softwareInterrupt + } + where + CpuIn{timerInterrupt, externalInterrupt, softwareInterrupt} = cpuIn + +inputToCombInput :: CpuIn -> JtagIn -> COMB_INPUT +inputToCombInput cpuIn jtagIn = + COMB_INPUT + { iBusWishbone_ACK = boolToBit (unsafeMakeDefinedRandom iBusAck) + , iBusWishbone_DAT_MISO = unpack (unsafeMakeDefinedRandom iBusDat) + , iBusWishbone_ERR = boolToBit (unsafeMakeDefinedRandom iBusErr) + , dBusWishbone_ACK = boolToBit (unsafeMakeDefinedRandom dBusAck) + , dBusWishbone_DAT_MISO = unpack (unsafeMakeDefinedRandom dBusDat) + , dBusWishbone_ERR = boolToBit (unsafeMakeDefinedRandom dBusErr) + , jtag_TCK = (unsafeMakeDefinedRandom testClock) + , jtag_TMS = (unsafeMakeDefinedRandom testModeSelect) + , jtag_TDI = (unsafeMakeDefinedRandom testDataIn) + } + where + CpuIn{iBusWbS2M, dBusWbS2M} = cpuIn + JtagIn{testClock, testModeSelect, testDataIn} = jtagIn + WishboneS2M{acknowledge = iBusAck, readData = iBusDat, err = iBusErr} = iBusWbS2M + WishboneS2M{acknowledge = dBusAck, readData = dBusDat, err = dBusErr} = dBusWbS2M + +outputToCpuOut :: OUTPUT -> CpuOut +outputToCpuOut OUTPUT{..} = + CpuOut + { iBusWbM2S = + WishboneM2S + { addr = truncateB (pack iBusWishbone_ADR) + , writeData = pack (iBusWishbone_DAT_MOSI) + , busSelect = unpack (truncateB (pack iBusWishbone_SEL)) + , lock = False + , busCycle = bitToBool iBusWishbone_CYC + , strobe = bitToBool iBusWishbone_STB + , writeEnable = bitToBool iBusWishbone_WE + , cycleTypeIdentifier = unpack (truncateB (pack iBusWishbone_CTI)) + , burstTypeExtension = unpack (truncateB (pack iBusWishbone_BTE)) + } + , dBusWbM2S = + WishboneM2S + { addr = truncateB (pack dBusWishbone_ADR) + , writeData = pack (dBusWishbone_DAT_MOSI) + , busSelect = unpack (truncateB (pack dBusWishbone_SEL)) + , lock = False + , busCycle = bitToBool dBusWishbone_CYC + , strobe = bitToBool dBusWishbone_STB + , writeEnable = bitToBool dBusWishbone_WE + , cycleTypeIdentifier = unpack (truncateB (pack dBusWishbone_CTI)) + , burstTypeExtension = unpack (truncateB (pack dBusWishbone_BTE)) + } + , ndmreset = ndmreset + , stoptime = stoptime + } + +outputToJtagOut :: OUTPUT -> JtagOut +outputToJtagOut OUTPUT{jtag_TDO} = JtagOut{testDataOut = jtag_TDO} + +data DumpVcd = DumpVcd FilePath | NoDumpVcd + +data Jtag (dom :: Domain) + +instance Protocol (Jtag dom) where + type Fwd (Jtag dom) = Signal dom JtagIn + type Bwd (Jtag dom) = Signal dom JtagOut + +instance IdleCircuit (Jtag dom) where + idleFwd _ = pure $ JtagIn 0 0 0 + idleBwd _ = pure $ JtagOut 0 + +{- | Generic simulation function that takes FFI function pointers +This allows different generated modules to use the same simulation logic +-} +vexRiscvSim :: + forall dom. + (HasCallStack, KnownDomain dom) => + -- | c_init + IO (Ptr VexRiscv) -> + -- | c_init_vcd + (Ptr VexRiscv -> CString -> IO (Ptr VerilatedVcdC)) -> + -- | c_init_stage1 + (Ptr VerilatedVcdC -> Word64 -> Ptr VexRiscv -> Ptr NON_COMB_INPUT -> Ptr OUTPUT -> IO ()) -> + -- | c_init_stage2 + (Ptr VexRiscv -> Ptr COMB_INPUT -> IO ()) -> + -- | c_step_rising + (Ptr VerilatedVcdC -> Ptr VexRiscv -> Word64 -> Ptr NON_COMB_INPUT -> Ptr OUTPUT -> IO ()) -> + -- | c_step_falling + (Ptr VerilatedVcdC -> Ptr VexRiscv -> Word64 -> Ptr COMB_INPUT -> IO ()) -> + -- Simulation inputs + DumpVcd -> + Clock dom -> + MinCyclesReset dom 2 -> + Signal dom CpuIn -> + Signal dom JtagIn -> + -- Simulation outputs + (Signal dom CpuOut, Signal dom JtagOut) +vexRiscvSim c_init c_init_vcd c_init_stage1 c_init_stage2 c_step_rising c_step_falling dumpVcd clk rst cpuInput jtagInput = unsafePerformIO $ do + let + domPeriodFs = hzToFs (natToNum @(PeriodToHz (Max 1 (DomainPeriod dom)))) + domPeriodFsWord64 = fromIntegral (unFemtoseconds domPeriodFs) :: Word64 + + -- Initialize the CPU + v <- c_init + vcd <- case dumpVcd of + NoDumpVcd -> pure nullPtr + DumpVcd path -> do + vcdPath <- newCString path + c_init_vcd v vcdPath + + let + initStage1 vPtr nonCombInput = + alloca $ \nonCombInputFFI -> alloca $ \outputFFI -> do + poke nonCombInputFFI nonCombInput + c_init_stage1 vcd domPeriodFsWord64 vPtr nonCombInputFFI outputFFI + peek outputFFI + {-# NOINLINE initStage1 #-} + + initStage2 vPtr combInput = + alloca $ \combInputFFI -> do + poke combInputFFI combInput + c_init_stage2 vPtr combInputFFI + {-# NOINLINE initStage2 #-} + + stepRising vPtr fsSinceLastEvent nonCombInput = + alloca $ \nonCombInputFFI -> alloca $ \outputFFI -> do + poke nonCombInputFFI nonCombInput + c_step_rising vcd vPtr fsSinceLastEvent nonCombInputFFI outputFFI + peek outputFFI + {-# NOINLINE stepRising #-} + + stepFalling vPtr fsSinceLastEvent combInput = + alloca $ \combInputFFI -> do + poke combInputFFI combInput + c_step_falling vcd vPtr fsSinceLastEvent combInputFFI + {-# NOINLINE stepFalling #-} + + simInitThenCycles :: Signal dom NON_COMB_INPUT -> Signal dom COMB_INPUT -> IO (Signal dom OUTPUT) + simInitThenCycles (cnc :- cncs) ~(cc :- ccs) = do + let ticks = first fromIntegral <$> singleClockEdgesRelative clk + out0 <- initStage1 v cnc + stage2Out <- unsafeInterleaveIO (initStage2 v cc) + out1 <- unsafeInterleaveIO (simCycles ticks cncs ccs) + pure $ out0 :- (stage2Out `seq` out1) + + simCycles :: [(Word64, ActiveEdge)] -> Signal dom NON_COMB_INPUT -> Signal dom COMB_INPUT -> IO (Signal dom OUTPUT) + simCycles ((fsSinceLastEvent, Rising) : ts) (cnc :- cncs) ccs = do + out0 <- stepRising v fsSinceLastEvent cnc + out1 <- unsafeInterleaveIO (simCycles ts cncs ccs) + pure $ out0 :- out1 + simCycles ((fsSinceLastEvent, Falling) : ts) cncs (cc :- ccs) = do + stepFalling v fsSinceLastEvent cc + simCycles ts cncs ccs + simCycles [] _ _ = error "Empty ticks: should never happen" + + output <- + simInitThenCycles + (inputToNonCombInput <$> unsafeToActiveHigh (fromMinCycles rst) <*> cpuInput) + (inputToCombInput <$> cpuInput <*> jtagInput) + pure + ( outputToCpuOut <$> output + , outputToJtagOut <$> output + ) +{-# INLINE vexRiscvSim #-} + +vexRiscvSynth :: + -- | Verilog module name + String -> + -- | Verilog source + String -> + Clock dom -> + MinCyclesReset dom 2 -> + Signal dom CpuIn -> + Signal dom JtagIn -> + (Signal dom CpuOut, Signal dom JtagOut) +vexRiscvSynth !_ !_ !_ !_ !_ !_ = (error msg, error msg) + where + msg = "vexRiscvSynth: not implemented" +{-# OPAQUE vexRiscvSynth #-} +{-# ANN vexRiscvSynth hasBlackBox #-} +{-# ANN + vexRiscvSynth + ( let primName = 'vexRiscvSynth + tfName = 'vexRiscvBBF + in InlineYamlPrimitive + [Verilog] + [i|BlackBoxHaskell: + name: #{primName} + templateFunction: #{tfName} + workInfo: Always + |] + ) + #-} diff --git a/src/VexRiscv/JtagTcpBridge.hs b/src/VexRiscv/JtagTcpBridge.hs new file mode 100644 --- /dev/null +++ b/src/VexRiscv/JtagTcpBridge.hs @@ -0,0 +1,52 @@ +-- SPDX-FileCopyrightText: 2023 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE RecordWildCards #-} + +module VexRiscv.JtagTcpBridge (vexrJtagBridge, defaultIn) where + +import Clash.Prelude +import Clash.Signal.Internal +import Foreign +import Network.Socket (PortNumber) +import System.IO.Unsafe (unsafePerformIO) + +import VexRiscv.FFI +import VexRiscv.Internal + +defaultIn :: JtagIn +defaultIn = JtagIn{testClock = low, testModeSelect = low, testDataIn = low} + +{-# NOINLINE inner #-} +inner :: (t -> IO JtagIn) -> Signal dom t -> Signal dom JtagIn +inner jtagBridgeStep (o :- outs) = unsafePerformIO $ do + in' <- jtagBridgeStep o + let ins' = inner jtagBridgeStep outs + pure $ in' :- (in' `deepseqX` ins') + +vexrJtagBridge :: PortNumber -> IO (Signal dom JtagOut -> Signal dom JtagIn) +vexrJtagBridge port = do + (_, jtagBridgeStep) <- vexrJtagBridge' port + pure (inner jtagBridgeStep) + +vexrJtagBridge' :: + PortNumber -> + IO + ( IO () + , -- \^ delete function + JtagOut -> IO JtagIn + ) +-- \^ step function + +vexrJtagBridge' port = do + bridge <- vexrJtagBridgeInit (fromIntegral port) + let + shutDown = vexrJtagBridgeShutdown bridge + + step JtagOut{..} = alloca $ \outFFI -> alloca $ \inFFI -> do + poke outFFI (JTAG_OUTPUT testDataOut) + vexrJtagBridgeStep bridge outFFI inFFI + JTAG_INPUT{..} <- peek inFFI + let input = JtagIn{testClock = tck, testModeSelect = tms, testDataIn = tdi} + pure input + pure (shutDown, step) diff --git a/src/VexRiscv/Paths.hs b/src/VexRiscv/Paths.hs new file mode 100644 --- /dev/null +++ b/src/VexRiscv/Paths.hs @@ -0,0 +1,9 @@ +-- SPDX-FileCopyrightText: 2025 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 + +module VexRiscv.Paths ( + module Paths_clash_vexriscv, +) where + +import Paths_clash_vexriscv diff --git a/src/VexRiscv/Random.hs b/src/VexRiscv/Random.hs new file mode 100644 --- /dev/null +++ b/src/VexRiscv/Random.hs @@ -0,0 +1,54 @@ +-- SPDX-FileCopyrightText: 2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE CPP #-} + +module VexRiscv.Random where + +import Clash.Prelude + +-- See https://github.com/clash-lang/clash-compiler/issues/2707 +#if __GLASGOW_HASKELL__ < 902 +import Numeric.Natural +#endif + +import Clash.Sized.Internal.BitVector +import Data.Bifunctor (bimap) +import GHC.IO (unsafePerformIO) +import System.Random + +{- | Unsafe version of 'makeDefinedRandom' with a NOINLINE pragma to avoid +compiler optimizations. +-} +unsafeMakeDefinedRandom :: (DefinedRandom a) => a -> a +unsafeMakeDefinedRandom = unsafePerformIO . makeDefinedRandom +{-# NOINLINE unsafeMakeDefinedRandom #-} + +{- | A class for types that can be (partially) undefined whose undefined values +can be replaced with defined random values. +-} +class DefinedRandom a where + makeDefinedRandom :: a -> IO a + +instance DefinedRandom Bool where + makeDefinedRandom b + | hasUndefined b = randomIO + | otherwise = pure b + +instance DefinedRandom Bit where + makeDefinedRandom b + | hasUndefined b = Bit 0 <$> randomRIO (0, 1) + | otherwise = pure b + +instance (KnownNat n) => DefinedRandom (BitVector n) where + makeDefinedRandom :: (KnownNat n) => BitVector n -> IO (BitVector n) + makeDefinedRandom bv@(ensureSpine -> BV mask dat) + | mask == 0 = pure bv + | otherwise = do + let maxVal = natToNum @(2 ^ n - 1) + randomNat <- genNatural (0, maxVal) + pure $ BV 0 (((maxVal `xor` mask) .&. dat) .|. (mask .&. randomNat)) + +-- | Generate a random natural number in the given inclusive range. +genNatural :: (Natural, Natural) -> IO Natural +genNatural = fmap fromInteger . randomRIO . bimap toInteger toInteger diff --git a/src/VexRiscv/Reset.hs b/src/VexRiscv/Reset.hs new file mode 100644 --- /dev/null +++ b/src/VexRiscv/Reset.hs @@ -0,0 +1,124 @@ +-- SPDX-FileCopyrightText: 2025 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE RoleAnnotations #-} + +{- | This module contains definitions and utility for VexriscV's reset input. +The reset is required to be asserted for at least two cycles. Otherwise +the CPU will be in an undefined state. +-} +module VexRiscv.Reset ( + MinCyclesReset, -- We dont export the constructor to enforce usage of the safe functions + fromMinCycles, + toMinCycles, + unsafeToMinCycles, + convert, + extend, + fromExtended, + or, + unsafeOr, +) where + +import Clash.Explicit.Prelude hiding (extend, or) +import qualified Clash.Explicit.Prelude as CE + +-- | Data type that contains a reset that is asserted for at least @n@ cycles. +data MinCyclesReset (dom :: Domain) (n :: Nat) = MinCyclesReset (Reset dom) + +type role MinCyclesReset nominal nominal + +-- | Extract the underlying reset from a 'MinCyclesReset', this discards the minimum cycles information. +fromMinCycles :: MinCyclesReset dom n -> Reset dom +fromMinCycles (MinCyclesReset rst) = rst + +{- | Convert a regular reset into a 'MinCyclesReset'. If the resulting minimum cycle count is higher than 1, +`holdReset` is used to extend the reset duration to match the new minimum cycle count. +-} +toMinCycles :: + forall n dom. + (KnownDomain dom, KnownNat n) => + Clock dom -> + Reset dom -> + MinCyclesReset dom n +toMinCycles clk rst = convert clk (MinCyclesReset @_ @1 rst) + +{- | Convert a regular reset into a 'MinCyclesReset'. + +This function is unsafe because it does not insert any logic to ensure the reset is actually +asserted for the required number of cycles. The caller must ensure that the provided reset meets +this requirement. +-} +unsafeToMinCycles :: + forall n dom. + (KnownDomain dom) => + Reset dom -> + MinCyclesReset dom n +unsafeToMinCycles = MinCyclesReset + +{- | Coerces a 'MinCyclesReset' into another 'MinCyclesReset' with a different minimum cycle count. +If the resulting minimum cycle count is higher than the original, `holdReset` is used to extend the reset duration. +to match the new minimum cycle count. + +If the resulting minimum cycle count is lower than the original, the reset is returned as-is. +This is safe because the original reset already satisfies the higher minimum cycle requirement. +-} +convert :: + forall n m dom. + (KnownDomain dom, KnownNat n, KnownNat m) => + Clock dom -> + MinCyclesReset dom n -> + MinCyclesReset dom m +convert clk (MinCyclesReset rst) = MinCyclesReset $ case compareSNat (SNat @(n + 1)) (SNat @m) of + SNatLE -> holdReset clk enableGen (SNat @(m - n)) rst + SNatGT -> rst + +{- | Extends a 'MinCyclesReset' to a new 'MinCyclesReset' with a higher minimum cycle count. +This is done by using `holdReset` to ensure the reset is asserted for the required number of cycles. +-} +extend :: + forall n m dom. + (KnownDomain dom, KnownNat n, KnownNat m, n <= m) => + Clock dom -> + MinCyclesReset dom n -> + MinCyclesReset dom m +extend = convert + +{- | Converts a 'MinCyclesReset' with a higher minimum cycle count to one with a lower minimum cycle count. +This does not insert any logic and the resulting reset will still be asserted for the higher minimum cycle count. +This is safe because the original reset already satisfies the higher minimum cycle requirement. +-} +fromExtended :: + forall n m dom. + (KnownNat n, KnownNat m, n <= m) => + MinCyclesReset dom m -> + MinCyclesReset dom n +fromExtended (MinCyclesReset rst) = MinCyclesReset rst + +{- | Combine two 'MinCyclesReset's into one that is asserted for at least +the maximum of the two input minimum cycles. +-} +or :: + forall n m dom. + (KnownDomain dom, HasSynchronousReset dom, KnownNat n, KnownNat m) => + Clock dom -> + MinCyclesReset dom n -> + MinCyclesReset dom m -> + MinCyclesReset dom (Max n m) +or = unsafeOr + +{- | Unsafely combine two 'MinCyclesReset's into one that is asserted for at least +the maximum of the two input minimum cycles. +-} +unsafeOr :: + forall n m dom. + (KnownDomain dom, KnownNat n, KnownNat m) => + Clock dom -> + MinCyclesReset dom n -> + MinCyclesReset dom m -> + MinCyclesReset dom (Max n m) +unsafeOr clk rstL0 rstR0 = + MinCyclesReset + $ CE.unsafeOrReset rstL1 rstR1 + where + rstL1 = fromMinCycles $ convert @n @(Max n m) clk rstL0 + rstR1 = fromMinCycles $ convert @m @(Max n m) clk rstR0 diff --git a/src/VexRiscv/Setup.hs b/src/VexRiscv/Setup.hs new file mode 100644 --- /dev/null +++ b/src/VexRiscv/Setup.hs @@ -0,0 +1,345 @@ +-- SPDX-FileCopyrightText: 2025 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE PackageImports #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE NoFieldSelectors #-} +{-# LANGUAGE NoImplicitPrelude #-} + +module VexRiscv.Setup ( + addVexRiscvHooks, + VexRiscvSource (..), +) where + +import Prelude + +import Control.Concurrent.Async (mapConcurrently_) +import Control.Monad (when) +import Data.Maybe (fromMaybe) +import Data.String.Interpolate (i) +import Distribution.PackageDescription ( + BuildInfo (extraLibDirs, extraLibs), + Library (libBuildInfo), + PackageDescription (library), + ) +import Distribution.Simple (UserHooks (confHook)) +import Distribution.Simple.LocalBuildInfo ( + Component (CLib), + LocalBuildInfo (localPkgDescr), + componentBuildDir, + interpretSymbolicPathLBI, + ) +import Distribution.Simple.Setup (CommonSetupFlags (setupVerbosity), ConfigFlags (configCommonFlags), fromFlag) +import Distribution.Simple.Utils (info, notice) +import Distribution.Types.LocalBuildInfo (allTargetsInBuildOrder') +import Distribution.Types.TargetInfo ( + TargetInfo (targetCLBI, targetComponent), + ) +import Distribution.Utils.Path (makeSymbolicPath) +import Distribution.Verbosity (Verbosity) +import GHC.Stack (HasCallStack) +import System.Directory ( + copyFile, + createDirectoryIfMissing, + doesFileExist, + getHomeDirectory, + makeAbsolute, + ) +import System.Exit (ExitCode (ExitSuccess)) +import System.FilePath (()) +import System.FilePath.Glob (glob) +import System.Process ( + CreateProcess (cwd), + proc, + readCreateProcessWithExitCode, + readProcess, + ) +import "extra" Data.List.Extra (trim) + +import qualified VexRiscv.Paths as Paths_clash_vexriscv + +{- | Specifies how to obtain the VexRiscv JAR file. + +The JAR file contains the compiled VexRiscv Scala classes needed to generate +Verilog from Scala CPU configurations. +-} +data VexRiscvSource + = -- | Use the bundled VexRiscv JAR included with @clash-vexriscv@ + VexRiscvBundled + | VexRiscvJar + { path :: FilePath + -- ^ Path to pre-built VexRiscv JAR file + } + | -- | Build from a Git repository at the specified commit/tag/branch + VexRiscvGit + { url :: String + , ref :: String + -- ^ Commit hash, tag, or branch name + } + +{- | Add VexRiscv build hooks to existing UserHooks. + +This function modifies the confHook to build VexRiscv libraries and update +the package build configuration. + +Example usage with a Git source: + +> main :: IO () +> main = defaultMainWithHooks $ +> addVexRiscvHooks simpleUserHooks "data" ["MyProject"] $ +> VexRiscvGit "https://github.com/SpinalHDL/VexRiscv.git" "7f2bccbef256b3ad40fb8dc8ba08a266f9c6256b" + +Example usage with a pre-built JAR: + +> main :: IO () +> main = defaultMainWithHooks $ +> addVexRiscvHooks simpleUserHooks "data" ["MyProject"] $ +> VexRiscvJar "path/to/vexriscv.jar" + +Finally, usage with the bundled JAR: + +> main :: IO () +> main = defaultMainWithHooks $ +> addVexRiscvHooks simpleUserHooks "data" ["MyProject"] VexRiscvBundled +-} +addVexRiscvHooks :: + UserHooks -> + -- | Configuration directory containing Scala files + FilePath -> + -- | List of CPU names to build + [FilePath] -> + -- | Source for VexRiscv JAR + VexRiscvSource -> + UserHooks +addVexRiscvHooks hooks configDir cpuNames vexriscvSource = + hooks + { confHook = \(genericPkgDesc, hookedBuildInfo) configFlags -> do + lbi <- confHook hooks (genericPkgDesc, hookedBuildInfo) configFlags + makeVexRiscvFromLocalBuildInfo lbi configFlags configDir cpuNames vexriscvSource + } + +makeVexRiscvFromLocalBuildInfo :: + (HasCallStack) => + LocalBuildInfo -> + ConfigFlags -> + FilePath -> + [FilePath] -> + VexRiscvSource -> + IO LocalBuildInfo +makeVexRiscvFromLocalBuildInfo lbi configFlags configDir cpuNames vexriscvSource = do + let + pkg = localPkgDescr lbi + verbosity = fromFlag (setupVerbosity (configCommonFlags configFlags)) + + -- Find the main library component + case library pkg of + Nothing -> error "No main library found in package" + Just lib -> do + let + allTargets = allTargetsInBuildOrder' pkg lbi + mainLibTarget = case [t | t <- allTargets, CLib lib' <- [targetComponent t], lib == lib'] of + (t : _) -> t + [] -> error "Could not find ComponentLocalBuildInfo for main library" + clbi = targetCLBI mainLibTarget + buildDir <- makeAbsolute (interpretSymbolicPathLBI lbi (componentBuildDir lbi clbi)) + let + autogenDir = buildDir "autogen" + libsDir = autogenDir "libs" + + -- XXX: Be very careful about the order of these directories. If the dynamic + -- one appears first, the REPL will break. + staticLibsDirSymbolic = makeSymbolicPath (libsDir "static") + dynamicLibsDirSymbolic = makeSymbolicPath (libsDir "dynamic") + + createDirectoryIfMissing True autogenDir + prepareVexRiscvJar verbosity autogenDir vexriscvSource + mapConcurrently_ (makeVexRiscv verbosity autogenDir configDir) cpuNames + + return $ + updateLibBuildInfo lbi $ + \buildInfo -> + buildInfo + { extraLibDirs = staticLibsDirSymbolic : dynamicLibsDirSymbolic : extraLibDirs buildInfo + , extraLibs = map (++ "VexRiscvFFI") cpuNames ++ extraLibs buildInfo + } + +prepareVexRiscvJar :: (HasCallStack) => Verbosity -> FilePath -> VexRiscvSource -> IO () +prepareVexRiscvJar verbosity autogenDir vexriscvSource = do + buildVexRiscvPy <- Paths_clash_vexriscv.getDataFileName ("data" "vexriscv" "lib" "build-vexriscv.py") + homeDir <- getHomeDirectory + + jarPath <- case vexriscvSource of + VexRiscvBundled -> do + dataDir <- Paths_clash_vexriscv.getDataFileName ("data" "vexriscv" "lib") + jarPaths <- glob (dataDir "vexriscv_*.jar") + jarPath <- case jarPaths of + [p] -> pure p + [] -> error "No bundled VexRiscv JAR found" + _ -> error "Multiple bundled VexRiscv JARs found" + info verbosity $ "Using bundled VexRiscv JAR: " ++ jarPath + return jarPath + VexRiscvJar p -> do + info verbosity $ "Using pre-built VexRiscv JAR: " ++ p + return p + VexRiscvGit url ref -> do + runCommand + verbosity + autogenDir + "flock" + [ homeDir ".sbt-lock" + , "python3" + , buildVexRiscvPy + , url + , ref + ] + + jars <- glob (autogenDir "vexriscv_*-" <> ref <> ".jar") + case jars of + [p] -> return p + [] -> error $ "No JAR file found for VexRiscv Git ref: " ++ ref + _ -> error $ "Multiple JAR files found for VexRiscv Git ref: " ++ ref + + copyIfChanged jarPath (autogenDir "vexriscv.jar") + +makeVexRiscv :: (HasCallStack) => Verbosity -> FilePath -> FilePath -> FilePath -> IO () +makeVexRiscv verbosity autogenDir configDir cpuName = do + let libraryDir = autogenDir "libs" cpuName ++ "VexRiscv" + createDirectoryIfMissing True libraryDir + dataDir <- Paths_clash_vexriscv.getDataDir + let clashVexriscvDataDir = dataDir "data" "vexriscv" + configDirAbs <- makeAbsolute configDir + + notice verbosity $ "Building VexRiscv_" ++ cpuName ++ ".." + runCommand + verbosity + libraryDir + "make" + [ "-f" + , clashVexriscvDataDir "Makefile" + , "-C" + , libraryDir + , "SCALA_CONFIG_DIR=" ++ configDirAbs + , "CPU_NAME=" ++ cpuName + , "-j" + ] + + verilogSource <- readFile (libraryDir cpuName ++ "VexRiscv.v") + + -- -- Generate Haskell module + let haskellModuleSource = generateHaskellModule cpuName verilogSource + writeFile (autogenDir "VexRiscv_" ++ cpuName ++ ".hs") haskellModuleSource + +-- Helper to update library build info in package description +updateLibBuildInfo :: LocalBuildInfo -> (BuildInfo -> BuildInfo) -> LocalBuildInfo +updateLibBuildInfo lbi f = + lbi + { localPkgDescr = + pkg + { library = + Just $ + lib + { libBuildInfo = f libBuild + } + } + } + where + pkg = localPkgDescr lbi + lib = fromMaybe (error "updateLibBuildInfo: unexpected empty library in package description") (library pkg) + libBuild = libBuildInfo lib + +copyIfChanged :: FilePath -> FilePath -> IO () +copyIfChanged src dst = do + dstExists <- doesFileExist dst + if dstExists + then do + sha512Src <- sha512 src + sha512Dst <- sha512 dst + when (sha512Src /= sha512Dst) $ do + copyFile src dst + else do + copyFile src dst + +sha512 :: FilePath -> IO String +sha512 path = do + out <- trim <$> readProcess "sha512sum" [path] "" + case words out of + (digest : _) -> return digest + _ -> error $ "sha512: unexpected output from sha512sum for file: " ++ path ++ ": " ++ out + +runCommand :: Verbosity -> FilePath -> String -> [String] -> IO () +runCommand verbosity workDir cmd args = do + info verbosity $ "Running: " ++ cmd ++ " " ++ unwords args + (exitCode, stdout, stderr) <- + readCreateProcessWithExitCode (proc cmd args){cwd = Just workDir} "" + when (exitCode /= ExitSuccess) $ do + error $ + "Command failed: " + ++ cmd + ++ "\nstdout: " + ++ stdout + ++ "\nstderr: " + ++ stderr + +generateHaskellModule :: String -> String -> String +generateHaskellModule cpuName verilogSource = + [i| +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ForeignFunctionInterface #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} + +{-# OPTIONS_GHC -fexpose-all-unfoldings #-} + +module VexRiscv_#{cpuName} ( + vexRiscv, +) where + +import Prelude +import Clash.Prelude (Clock, KnownDomain, Signal, clashSimulation) +import Data.Word (Word64) +import Foreign.C.String (CString) +import Foreign.Ptr (Ptr) +import GHC.Stack (HasCallStack) +import VexRiscv (CpuIn, CpuOut, DumpVcd, JtagIn, JtagOut) +import VexRiscv.Internal (VexRiscv, VerilatedVcdC, vexRiscvSim, vexRiscvSynth) +import VexRiscv.FFI (COMB_INPUT, NON_COMB_INPUT, OUTPUT) +import VexRiscv.Reset (MinCyclesReset) + +-- FFI declarations for: V#{cpuName}VexRiscv +foreign import ccall unsafe "V#{cpuName}VexRiscv_init" + c_init :: IO (Ptr VexRiscv) + +foreign import ccall unsafe "V#{cpuName}VexRiscv_init_vcd" + c_init_vcd :: Ptr VexRiscv -> CString -> IO (Ptr VerilatedVcdC) + +-- TODO: +-- foreign import ccall unsafe "V#{cpuName}VexRiscv_shutdown" +-- c_shutdown :: Ptr VexRiscv -> IO () + +foreign import ccall unsafe "V#{cpuName}VexRiscv_init_stage1" + c_init_stage1 :: Ptr VerilatedVcdC -> Word64 -> Ptr VexRiscv -> Ptr NON_COMB_INPUT -> Ptr OUTPUT -> IO () + +foreign import ccall unsafe "V#{cpuName}VexRiscv_init_stage2" + c_init_stage2 :: Ptr VexRiscv -> Ptr COMB_INPUT -> IO () + +foreign import ccall unsafe "V#{cpuName}VexRiscv_step_rising_edge" + c_step_rising :: Ptr VerilatedVcdC -> Ptr VexRiscv -> Word64 -> Ptr NON_COMB_INPUT -> Ptr OUTPUT -> IO () + +foreign import ccall unsafe "V#{cpuName}VexRiscv_step_falling_edge" + c_step_falling :: Ptr VerilatedVcdC -> Ptr VexRiscv -> Word64 -> Ptr COMB_INPUT -> IO () + +-- | VexRiscv CPU simulation function +vexRiscv :: + forall dom. + (HasCallStack, KnownDomain dom) => + DumpVcd -> + Clock dom -> + MinCyclesReset dom 2 -> + Signal dom CpuIn -> + Signal dom JtagIn -> + (Signal dom CpuOut, Signal dom JtagOut) +vexRiscv dumpVcd clk rst cpuIn jtagIn + | clashSimulation = vexRiscvSim c_init c_init_vcd c_init_stage1 c_init_stage2 c_step_rising c_step_falling dumpVcd clk rst cpuIn jtagIn + | otherwise = vexRiscvSynth "#{cpuName}VexRiscv" #{show verilogSource} clk rst cpuIn jtagIn +{-# OPAQUE vexRiscv #-} +|] diff --git a/src/VexRiscv/VecToTuple.hs b/src/VexRiscv/VecToTuple.hs new file mode 100644 --- /dev/null +++ b/src/VexRiscv/VecToTuple.hs @@ -0,0 +1,282 @@ +-- SPDX-FileCopyrightText: 2022-2023 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeFamilyDependencies #-} +-- Purpose of this module +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} + +module VexRiscv.VecToTuple (VecToTuple (..)) where + +import Clash.Prelude +import Data.Tagged (Tagged (..)) + +#if MIN_VERSION_base(4,18,0) +import Data.Tuple (Solo(MkSolo)) +#elif MIN_VERSION_base(4,16,0) +import Data.Tuple (Solo(Solo)) +#endif + +class VecToTuple a where + type TupType a = r | r -> a + vecToTuple :: a -> TupType a + +-- | Silly instance +instance VecToTuple (Vec 0 a) where + type TupType (Vec 0 a) = Tagged a () + vecToTuple Nil = Tagged () + +#if MIN_VERSION_base(4,18,0) +instance VecToTuple (Vec 1 a) where + type TupType (Vec 1 a) = Solo a + vecToTuple (a0 :> Nil) = MkSolo a0 +#elif MIN_VERSION_base(4,16,0) +instance VecToTuple (Vec 1 a) where + type TupType (Vec 1 a) = Solo a + vecToTuple (a0 :> Nil) = Solo a0 +#endif + +instance VecToTuple (Vec 2 a) where + type TupType (Vec 2 a) = (a, a) + vecToTuple (a0 :> a1 :> Nil) = (a0, a1) + +instance VecToTuple (Vec 3 a) where + type TupType (Vec 3 a) = (a, a, a) + vecToTuple (a0 :> a1 :> a2 :> Nil) = (a0, a1, a2) + +instance VecToTuple (Vec 4 a) where + type TupType (Vec 4 a) = (a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> Nil) = (a0, a1, a2, a3) + +instance VecToTuple (Vec 5 a) where + type TupType (Vec 5 a) = (a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> Nil) = (a0, a1, a2, a3, a4) + +instance VecToTuple (Vec 6 a) where + type TupType (Vec 6 a) = (a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> Nil) = (a0, a1, a2, a3, a4, a5) + +instance VecToTuple (Vec 7 a) where + type TupType (Vec 7 a) = (a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> Nil) = (a0, a1, a2, a3, a4, a5, a6) + +instance VecToTuple (Vec 8 a) where + type TupType (Vec 8 a) = (a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7) + +instance VecToTuple (Vec 9 a) where + type TupType (Vec 9 a) = (a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8) + +instance VecToTuple (Vec 10 a) where + type TupType (Vec 10 a) = (a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9) + +instance VecToTuple (Vec 11 a) where + type TupType (Vec 11 a) = (a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) + +instance VecToTuple (Vec 12 a) where + type TupType (Vec 12 a) = (a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) + +instance VecToTuple (Vec 13 a) where + type TupType (Vec 13 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) + +instance VecToTuple (Vec 14 a) where + type TupType (Vec 14 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) + +instance VecToTuple (Vec 15 a) where + type TupType (Vec 15 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) + +instance VecToTuple (Vec 16 a) where + type TupType (Vec 16 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) + +instance VecToTuple (Vec 17 a) where + type TupType (Vec 17 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16) + +instance VecToTuple (Vec 18 a) where + type TupType (Vec 18 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17) + +instance VecToTuple (Vec 19 a) where + type TupType (Vec 19 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18) + +instance VecToTuple (Vec 20 a) where + type TupType (Vec 20 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19) + +instance VecToTuple (Vec 21 a) where + type TupType (Vec 21 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20) + +instance VecToTuple (Vec 22 a) where + type TupType (Vec 22 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21) + +instance VecToTuple (Vec 23 a) where + type TupType (Vec 23 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22) + +instance VecToTuple (Vec 24 a) where + type TupType (Vec 24 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23) + +instance VecToTuple (Vec 25 a) where + type TupType (Vec 25 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24) + +instance VecToTuple (Vec 26 a) where + type TupType (Vec 26 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25) + +instance VecToTuple (Vec 27 a) where + type TupType (Vec 27 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26) + +instance VecToTuple (Vec 28 a) where + type TupType (Vec 28 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27) + +instance VecToTuple (Vec 29 a) where + type TupType (Vec 29 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28) + +instance VecToTuple (Vec 30 a) where + type TupType (Vec 30 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29) + +instance VecToTuple (Vec 31 a) where + type TupType (Vec 31 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30) + +instance VecToTuple (Vec 32 a) where + type TupType (Vec 32 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31) + +instance VecToTuple (Vec 33 a) where + type TupType (Vec 33 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32) + +instance VecToTuple (Vec 34 a) where + type TupType (Vec 34 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33) + +instance VecToTuple (Vec 35 a) where + type TupType (Vec 35 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34) + +instance VecToTuple (Vec 36 a) where + type TupType (Vec 36 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35) + +instance VecToTuple (Vec 37 a) where + type TupType (Vec 37 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36) + +instance VecToTuple (Vec 38 a) where + type TupType (Vec 38 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37) + +instance VecToTuple (Vec 39 a) where + type TupType (Vec 39 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38) + +instance VecToTuple (Vec 40 a) where + type TupType (Vec 40 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39) + +instance VecToTuple (Vec 41 a) where + type TupType (Vec 41 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40) + +instance VecToTuple (Vec 42 a) where + type TupType (Vec 42 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41) + +instance VecToTuple (Vec 43 a) where + type TupType (Vec 43 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42) + +instance VecToTuple (Vec 44 a) where + type TupType (Vec 44 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43) + +instance VecToTuple (Vec 45 a) where + type TupType (Vec 45 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44) + +instance VecToTuple (Vec 46 a) where + type TupType (Vec 46 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45) + +instance VecToTuple (Vec 47 a) where + type TupType (Vec 47 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46) + +instance VecToTuple (Vec 48 a) where + type TupType (Vec 48 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47) + +instance VecToTuple (Vec 49 a) where + type TupType (Vec 49 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48) + +instance VecToTuple (Vec 50 a) where + type TupType (Vec 50 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49) + +instance VecToTuple (Vec 51 a) where + type TupType (Vec 51 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50) + +instance VecToTuple (Vec 52 a) where + type TupType (Vec 52 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51) + +instance VecToTuple (Vec 53 a) where + type TupType (Vec 53 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> a52 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52) + +instance VecToTuple (Vec 54 a) where + type TupType (Vec 54 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> a52 :> a53 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53) + +instance VecToTuple (Vec 55 a) where + type TupType (Vec 55 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> a52 :> a53 :> a54 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54) + +instance VecToTuple (Vec 56 a) where + type TupType (Vec 56 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> a52 :> a53 :> a54 :> a55 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55) + +instance VecToTuple (Vec 57 a) where + type TupType (Vec 57 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> a52 :> a53 :> a54 :> a55 :> a56 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56) + +instance VecToTuple (Vec 58 a) where + type TupType (Vec 58 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> a52 :> a53 :> a54 :> a55 :> a56 :> a57 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56, a57) + +instance VecToTuple (Vec 59 a) where + type TupType (Vec 59 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> a52 :> a53 :> a54 :> a55 :> a56 :> a57 :> a58 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56, a57, a58) + +instance VecToTuple (Vec 60 a) where + type TupType (Vec 60 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> a52 :> a53 :> a54 :> a55 :> a56 :> a57 :> a58 :> a59 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56, a57, a58, a59) + +instance VecToTuple (Vec 61 a) where + type TupType (Vec 61 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> a52 :> a53 :> a54 :> a55 :> a56 :> a57 :> a58 :> a59 :> a60 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56, a57, a58, a59, a60) + +instance VecToTuple (Vec 62 a) where + type TupType (Vec 62 a) = (a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a, a) + vecToTuple (a0 :> a1 :> a2 :> a3 :> a4 :> a5 :> a6 :> a7 :> a8 :> a9 :> a10 :> a11 :> a12 :> a13 :> a14 :> a15 :> a16 :> a17 :> a18 :> a19 :> a20 :> a21 :> a22 :> a23 :> a24 :> a25 :> a26 :> a27 :> a28 :> a29 :> a30 :> a31 :> a32 :> a33 :> a34 :> a35 :> a36 :> a37 :> a38 :> a39 :> a40 :> a41 :> a42 :> a43 :> a44 :> a45 :> a46 :> a47 :> a48 :> a49 :> a50 :> a51 :> a52 :> a53 :> a54 :> a55 :> a56 :> a57 :> a58 :> a59 :> a60 :> a61 :> Nil) = (a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31, a32, a33, a34, a35, a36, a37, a38, a39, a40, a41, a42, a43, a44, a45, a46, a47, a48, a49, a50, a51, a52, a53, a54, a55, a56, a57, a58, a59, a60, a61) diff --git a/tests/unittests/Tests/Extra.hs b/tests/unittests/Tests/Extra.hs new file mode 100644 --- /dev/null +++ b/tests/unittests/Tests/Extra.hs @@ -0,0 +1,36 @@ +-- SPDX-FileCopyrightText: 2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 + +module Tests.Extra where + +import Data.Functor ((<&>)) +import Language.Haskell.TH (mkName) +import Language.Haskell.TH.Lib +import Prelude + +{- | Generate a do-expression where each statement is a call to @test@ and the +arguments are determined by the carthesian product of given argument names. + +For example: + +> carthesianProductTests ["x", "y"] +> ======> +> do +> test x x +> test x y +> test y x +> test y y +-} +carthesianProductTests :: [String] -> ExpQ +carthesianProductTests names = + doE $ + cartProd names <&> \(aName, bName) -> + noBindS $ + let + aExp = varE (mkName aName) + bExp = varE (mkName bName) + in + [|test $aExp $bExp|] + where + cartProd xs = [(a, b) | a <- xs, b <- xs] diff --git a/tests/unittests/Tests/VexRiscv/ClockTicks.hs b/tests/unittests/Tests/VexRiscv/ClockTicks.hs new file mode 100644 --- /dev/null +++ b/tests/unittests/Tests/VexRiscv/ClockTicks.hs @@ -0,0 +1,338 @@ +-- SPDX-FileCopyrightText: 2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE TemplateHaskell #-} +-- Clock definitions aren't much more readable with top level signatures.. +{-# OPTIONS_GHC -Wno-missing-signatures #-} +-- Suppress Clash domain warnings +{-# OPTIONS_GHC -Wno-orphans #-} + +module Tests.VexRiscv.ClockTicks where + +import Clash.Explicit.Prelude hiding (d107, d122, d61) +import Clash.Signal.Internal (ClockAB (..), Femtoseconds (..), clockTicks, dynamicClockGen) +import Data.Bifunctor (second) +import Data.Int (Int64) +import Data.Maybe (catMaybes) +import Test.Tasty +import Test.Tasty.HUnit +import Test.Tasty.TH + +import qualified Data.List as L +import qualified Prelude as P + +import Tests.Extra (carthesianProductTests) +import VexRiscv.ClockTicks ( + ClockEdgeAB (..), + clockEdgesAbsolute, + clockEdgesRelative, + clockTicksAbsolute, + clockTicksRelative, + ) + +createDomain vSystem{vName = "R61", vPeriod = 61} +createDomain vSystem{vName = "R107", vPeriod = 107} +createDomain vSystem{vName = "R122", vPeriod = 122} + +createDomain vSystem{vName = "F61", vPeriod = 61, vActiveEdge = Falling} +createDomain vSystem{vName = "F107", vPeriod = 107, vActiveEdge = Falling} +createDomain vSystem{vName = "F122", vPeriod = 122, vActiveEdge = Falling} + +createDomain vSystem{vName = "D61", vPeriod = 61} +createDomain vSystem{vName = "D107", vPeriod = 107} +createDomain vSystem{vName = "D122", vPeriod = 122} + +r61 = clockGen @R61 +r107 = clockGen @R107 +r122 = clockGen @R122 + +f61 = clockGen @F61 +f107 = clockGen @F107 +f122 = clockGen @F122 + +{- | Used in production code. We're seeing strange things there, so we add some +tests here making sure that it's not this module messing up. +-} +createDomain vXilinxSystem{vName = "CPU"} +createDomain vXilinxSystem{vName = "JTAG", vPeriod = hzToPeriod 50_000} + +-- | Clock whose clock period differs slightly from 61 ps every tick +d61 :: Clock D61 +d61 = dynamicClockGen (fromList periods) + where + -- Note that the random values are subtracted as femtoseconds. This makes sure + -- we end up with periods that are not divisable by 2, triggering an interesting + -- test case. + periods = P.cycle $ (\r -> Femtoseconds (1000 * 61 + r)) <$> rands + rands = [2, 3, 5, 8, -1, 7, -8, -2, -5, -7, -10, -9, 1, -3, 10, 0, 6, -6, 9, -4, 4] + +-- | Clock whose clock period differs slightly from 107 ps every tick +d107 :: Clock D107 +d107 = dynamicClockGen (fromList periods) + where + periods = P.cycle $ (\r -> Femtoseconds (1000 * 107 + r)) <$> rands + rands = [-1, -5, -3, 2, -8, -4, 8, -9, 9, 5, -6, 1, 6, 4, 0, 3, 7, -2, -7, 10, -10] + +-- | Clock whose clock period differs slightly from 122 ps every tick +d122 :: Clock D122 +d122 = dynamicClockGen (fromList periods) + where + periods = P.cycle $ (\r -> Femtoseconds (1000 * 122 + r)) <$> rands + rands = [0, 3, -8, -6, 10, -9, -4, -3, 5, 1, -10, 8, -1, 4, 6, -5, 2, -7, -2, 9, 7] + +{- | Compare to "infinite" lists, by comparing the first /N/ samples. See +implemenation for the value of /N/. +-} +infEq :: (Eq a, Show a) => [a] -> [a] -> Assertion +infEq as bs = let n = 10000 in P.take n as @=? P.take n bs + +-- | Convert specific edges of 'ClockEdgeAB' to 'ClockAB'. +toClockAB :: ActiveEdge -> ActiveEdge -> ClockEdgeAB -> Maybe ClockAB +toClockAB filterA filterB = go + where + go (ClockEdgeA edge) | edge == filterA = Just ClockA + go (ClockEdgeB edge) | edge == filterB = Just ClockB + go (ClockEdgeAB edgeA edgeB) + | edgeA == filterA && edgeB == filterB = Just ClockAB + | edgeA == filterA = Just ClockA + | edgeB == filterB = Just ClockB + go _ = Nothing + +clockToActiveEdge :: forall dom. (KnownDomain dom) => Clock dom -> ActiveEdge +clockToActiveEdge _clk = case activeEdge @dom of + SRising -> Rising + SFalling -> Falling + +clockToPeriod :: forall dom a. (Integral a, KnownDomain dom) => Clock dom -> a +clockToPeriod _clk = snatToNum (clockPeriod @dom) + +-- | Convert specific edges of 'ClockEdgeAB' to 'ClockAB'. +toClockABs :: ActiveEdge -> ActiveEdge -> [ClockEdgeAB] -> [ClockAB] +toClockABs filterA filterB = catMaybes . P.map (toClockAB filterA filterB) + +-- | Convert a list of relative event timestamps to a list of absolute timestamps +relativeToAbsolute :: [Int64] -> [Int64] +relativeToAbsolute = snd . L.mapAccumL (\acc t -> let new = acc + t in (new, new)) 0 + +-- | Convert a list of absolute event timestamps to a list of relative timestamps +absoluteToRelative :: [Int64] -> [Int64] +absoluteToRelative absoluteTimestamps = + 0 : P.zipWith (-) (P.drop 1 absoluteTimestamps) absoluteTimestamps + +unzipFirst :: ([a] -> [b]) -> [(a, c)] -> [(b, c)] +unzipFirst f (P.unzip -> (as, cs)) = P.zip (f as) cs + +unzipSecond :: ([a] -> [b]) -> [(c, a)] -> [(c, b)] +unzipSecond f (P.unzip -> (cs, as)) = P.zip cs (f as) + +{- | Check that 'clockTicksAbsolute' produces the same ratio of clock ticks as +@clash-prelude@'s 'clockTicks' +-} +case_eqClockTicksAbsolute :: Assertion +case_eqClockTicksAbsolute = + $(carthesianProductTests ["r61", "r107", "r122", "d61", "d107", "d122", "f61", "f107", "f122"]) + where + test a b = fmap snd (clockTicksAbsolute a b) `infEq` clockTicks a b + +{- | Check that 'clockTicksRelative' produces the same ratio of clock ticks as +@clash-prelude@'s 'clockTicks' +-} +case_eqClockTicksRelative :: Assertion +case_eqClockTicksRelative = + $(carthesianProductTests ["r61", "r107", "r122", "d61", "d107", "d122", "f61", "f107", "f122"]) + where + test a b = fmap snd (clockTicksRelative a b) `infEq` clockTicks a b + +{- | Check that 'clockEdgesAbsolute' produces the same ratio of clock ticks as +@clash-prelude@'s 'clockTicks' +-} +case_eqClockEdgesAbsolute :: Assertion +case_eqClockEdgesAbsolute = + $(carthesianProductTests ["r61", "r107", "r122", "d61", "d107", "d122", "f61", "f107", "f122"]) + where + test a b = go a b (clockEdgesAbsolute a b) `infEq` clockTicks a b + go a b = toClockABs (clockToActiveEdge a) (clockToActiveEdge b) . fmap snd + +{- | Check that 'clockEdgesRelative' produces the same ratio of clock ticks as +@clash-prelude@'s 'clockTicks' +-} +case_eqClockEdgesRelative :: Assertion +case_eqClockEdgesRelative = + $(carthesianProductTests ["r61", "r107", "r122", "d61", "d107", "d122", "f61", "f107", "f122"]) + where + test a b = go a b (clockEdgesRelative a b) `infEq` clockTicks a b + go a b = toClockABs (clockToActiveEdge a) (clockToActiveEdge b) . fmap snd + +{- | Check that 'clockEdgesAbsolute' produces the same ratio of clock ticks and +same timestamps as 'clockTicksAbsolute'. +-} +case_eqClockEdgesTicksAbsolute :: Assertion +case_eqClockEdgesTicksAbsolute = + $(carthesianProductTests ["r61", "r107", "r122", "d61", "d107", "d122", "f61", "f107", "f122"]) + where + test a b = go a b (clockEdgesAbsolute a b) `infEq` clockTicksAbsolute a b + + go a b (P.unzip -> (times, edges)) = + catMaybes (P.zipWith (liftA2 (,)) maybeTimes maybeEdges) + where + maybeTimes = Just <$> times + maybeEdges = toClockAB (clockToActiveEdge a) (clockToActiveEdge b) <$> edges + +{- | Check that 'clockEdgesRelative' produces the same ratio of clock ticks and +same timestamps as 'clockTicksRelative'. +-} +case_eqClockEdgesTicksRelative :: Assertion +case_eqClockEdgesTicksRelative = + $(carthesianProductTests ["r61", "r107", "r122", "d61", "d107", "d122", "f61", "f107", "f122"]) + where + test a b = go a b (clockEdgesRelative a b) `infEq` clockTicksRelative a b + + go a b (P.unzip -> (relativeTimes, edges)) = + unzipFirst + absoluteToRelative + (catMaybes (P.zipWith (liftA2 (,)) maybeAbsoluteTimes maybeEdges)) + where + maybeAbsoluteTimes :: [Maybe Int64] + maybeAbsoluteTimes = Just <$> absoluteTimes + + absoluteTimes :: [Int64] + absoluteTimes = relativeToAbsolute relativeTimes + + maybeEdges :: [Maybe ClockAB] + maybeEdges = toClockAB (clockToActiveEdge a) (clockToActiveEdge b) <$> edges + +{- | Check that `clockTicksRelative` has a sane time in between events when it +gets passed two of the same clocks. +-} +case_sanityClockTicksRelativeSame :: Assertion +case_sanityClockTicksRelativeSame = do + test r61 + test r107 + test r122 + test f122 + test f107 + test f122 + where + test c = clockTicksRelative c c `infEq` expected c + expected c = P.zip (0 : P.repeat (1000 * clockToPeriod c)) (P.repeat ClockAB) + +{- | Check that `clockTicksRelative` has a sane time in between events when it +gets passed one fast clock and one slow clock, where the fast clock is exactly +twice as fast as the slow clock. +-} +case_sanityClockTicksRelativeDouble :: Assertion +case_sanityClockTicksRelativeDouble = do + test r61 r122 + where + test c0 c1 = clockTicksRelative c0 c1 `infEq` expected c0 c1 + expected c0 _c1 = P.zip (0 : P.repeat (1000 * clockToPeriod c0)) (P.cycle [ClockAB, ClockA]) + +{- | Check that `clockTicksRelative` has a sane time in between events when it +gets passed two of the same clocks. +-} +case_sanityClockEdgesRelativeSame :: Assertion +case_sanityClockEdgesRelativeSame = do + test r61 + test r107 + test r122 + test f122 + test f107 + test f122 + where + test c = clockTicksRelative c c `infEq` expected c + expected c = P.zip (0 : P.repeat (1000 * clockToPeriod c)) (P.repeat ClockAB) + +{- | Check that `clockTicksRelative` has a sane time in between events when it +gets passed one fast clock and one slow clock, where the fast clock is exactly +twice as fast as the slow clock. +-} +case_sanityClockEdgesRelativeDouble :: Assertion +case_sanityClockEdgesRelativeDouble = do + test r61 r122 + where + test c0 c1 = clockEdgesRelative c0 c1 `infEq` expected c0 c1 + expected c0 _c1 = + P.zip + (0 : P.repeat ((1000 * clockToPeriod c0) `div` 2)) + ( P.cycle + [ ClockEdgeAB Rising Rising + , ClockEdgeA Falling + , ClockEdgeAB Rising Falling + , ClockEdgeA Falling + ] + ) + +-- | Make sure that swapping the arguments makes no difference for timing calculations +case_flipped :: Assertion +case_flipped = + $(carthesianProductTests ["r61", "r107", "r122", "d61", "d107", "d122", "f61", "f107", "f122"]) + where + test a b = do + clockEdgesAbsolute a b `infEq` P.map (second flipClockEdge) (clockEdgesAbsolute b a) + clockEdgesRelative a b `infEq` P.map (second flipClockEdge) (clockEdgesRelative b a) + clockTicksAbsolute a b `infEq` P.map (second flipClock) (clockTicksAbsolute b a) + clockTicksRelative a b `infEq` P.map (second flipClock) (clockTicksRelative b a) + + flipClockEdge :: ClockEdgeAB -> ClockEdgeAB + flipClockEdge (ClockEdgeA edge) = ClockEdgeB edge + flipClockEdge (ClockEdgeB edge) = ClockEdgeA edge + flipClockEdge (ClockEdgeAB edgeA edgeB) = ClockEdgeAB edgeB edgeA + + flipClock :: ClockAB -> ClockAB + flipClock ClockA = ClockB + flipClock ClockB = ClockA + flipClock ClockAB = ClockAB + +{- | Check results produced by 'clockTicksAbsolute' and 'clockEdgesAbsolute' manually +to rule out functions in "ClockTicks" causing the strange behavior we're seeing +in production. +-} +case_sanityJtagCpu :: Assertion +case_sanityJtagCpu = do + expectedAbsJtagEdges `infEq` P.map fst absJtagEdges + expectedAbsJtagTicks `infEq` P.map fst absJtagTicks + expectedAbsCpuEdges `infEq` P.map fst absCpuEdges + expectedAbsCpuTicks `infEq` P.map fst absCpuTicks + where + -- JTAG + expectedAbsJtagEdges = [0, halfJtagPeriodFs ..] + expectedAbsJtagTicks = [0, jtagPeriodFs ..] + + halfJtagPeriodFs = jtagPeriodFs `div` 2 + jtagPeriodFs = 1000 * clockToPeriod jtagClk :: Int64 + + isJtagEdge (ClockEdgeA _) = False + isJtagEdge _ = True + + isJtagTick ClockA = False + isJtagTick _ = True + + absJtagEdges = filter (isJtagEdge . snd) absEdges + absJtagTicks = filter (isJtagTick . snd) absTicks + + -- CPU + expectedAbsCpuEdges = [0, halfCpuPeriodFs ..] + expectedAbsCpuTicks = [0, cpuPeriodFs ..] + + halfCpuPeriodFs = cpuPeriodFs `div` 2 + cpuPeriodFs = 1000 * clockToPeriod cpuClk :: Int64 + + isCpuEdge (ClockEdgeB _) = False + isCpuEdge _ = True + + isCpuTick ClockB = False + isCpuTick _ = True + + absCpuEdges = filter (isCpuEdge . snd) absEdges + absCpuTicks = filter (isCpuTick . snd) absTicks + + -- BOTH + absTicks = clockTicksAbsolute cpuClk jtagClk + absEdges = clockEdgesAbsolute cpuClk jtagClk + + cpuClk = clockGen @CPU + jtagClk = clockGen @JTAG + +tests :: TestTree +tests = $(testGroupGenerator) diff --git a/tests/unittests/Tests/VexRiscv/Random.hs b/tests/unittests/Tests/VexRiscv/Random.hs new file mode 100644 --- /dev/null +++ b/tests/unittests/Tests/VexRiscv/Random.hs @@ -0,0 +1,46 @@ +-- SPDX-FileCopyrightText: 2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +module Tests.VexRiscv.Random where + +import Clash.Hedgehog.Sized.BitVector +import Clash.Prelude +import Hedgehog +import Test.Tasty +import Test.Tasty.Hedgehog + +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +import VexRiscv.Random + +tests :: TestTree +tests = + testGroup + "VexRiscv.Random" + [ testProperty "genNatural" prop_genNatural + , testProperty "makeDefinedRandomBitVector" prop_makeDefinedRandomBitVector + , testProperty "makeDefinedRandomBit" prop_makeDefinedRandomBit + ] + +prop_genNatural :: Property +prop_genNatural = property $ do + lo <- forAll $ Gen.integral (Range.linear 0 (shiftL 1 1024)) + hi <- forAll $ Gen.integral (Range.linear lo (shiftL 1 1024)) + n <- evalIO $ genNatural (lo, hi) + assert ((n >= lo) && (n <= hi)) + +prop_makeDefinedRandomBitVector :: Property +prop_makeDefinedRandomBitVector = property $ do + someBv <- forAll $ (genSomeBitVector @0) (Range.linear 0 1024) genBitVector + case someBv of + SomeBitVector SNat bv -> do + definedBv <- evalIO $ makeDefinedRandom bv + assert (not $ hasUndefined definedBv) + assert (definedBv <= maxBound) + +prop_makeDefinedRandomBit :: Property +prop_makeDefinedRandomBit = property $ do + b <- forAll $ genBit + definedB <- evalIO $ makeDefinedRandom b + assert (not $ hasUndefined definedB) diff --git a/tests/unittests/Tests/VexRiscv/Reset.hs b/tests/unittests/Tests/VexRiscv/Reset.hs new file mode 100644 --- /dev/null +++ b/tests/unittests/Tests/VexRiscv/Reset.hs @@ -0,0 +1,220 @@ +-- SPDX-FileCopyrightText: 2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE TemplateHaskell #-} +{-# OPTIONS_GHC -Wno-missing-signatures #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Tests.VexRiscv.Reset where + +import Clash.Explicit.Prelude hiding (or, unsafeOrReset) +import Hedgehog ((===)) +import Test.Tasty +import Test.Tasty.Hedgehog (testProperty) +import Test.Tasty.TH +import VexRiscv.Reset as MinReset + +import qualified Clash.Explicit.Prelude as CE +import qualified Data.List as L +import qualified Hedgehog as H +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range + +-- | Test domain with a known period and synchronous reset +createDomain vSystem{vName = "TestDom", vResetKind = Synchronous} + +testClk :: Clock TestDom +testClk = clockGen @TestDom + +{- | Generator for a random reset signal that is randomly asserted or deasserted +during the first 50 cycles. After that the reset will be deasserted. +-} +genReset :: forall dom. (KnownDomain dom) => H.Gen (Reset dom) +genReset = do + resetValues <- Gen.list (Range.linear 1 50) Gen.bool + pure $ unsafeFromActiveHigh $ fromList (resetValues <> L.repeat False) + +-- | `MinCyclesReset` version of `genReset` +genMinCyclesReset :: forall dom n. (KnownDomain dom, KnownNat n) => SNat n -> H.Gen (MinCyclesReset dom n) +genMinCyclesReset snat = do + resetValues <- genReset + let extendedReset = holdReset clockGen enableGen snat resetValues + pure $ unsafeToMinCycles @n extendedReset + +{- | Check if a list of boolean samples represents a reset where ALL assertion sequences +are at least n consecutive cycles. Returns False if any assertion sequence is shorter than n cycles. +-} +isResetAtLeastN :: Int -> [Bool] -> Bool +isResetAtLeastN n samples = not (null durations) && all (>= n) durations + where + durations = getResetDurations samples + +-- | Extract the lengths of all consecutive True sequences from a list of booleans +getResetDurations :: [Bool] -> [Int] +getResetDurations samples = L.reverse $ fst $ L.foldl' go ([], 0) samples + where + go (acc, 0) False = (acc, 0) + go (acc, current) False = (current : acc, 0) + go (acc, current) True = (acc, current + 1) + +-- | Sample a reset signal to a finite list of booleans +sampleReset :: (KnownDomain dom) => Reset dom -> [Bool] +sampleReset rst = sampleN 100 (unsafeToActiveHigh rst) + +-- | Helper to use forAll with Reset, showing only the asserted portion of the sampled reset signal +forAllReset :: + forall dom m. + (Monad m, KnownDomain dom) => + H.Gen (Reset dom) -> + H.PropertyT m (Reset dom) +forAllReset gen = H.forAllWith showReset gen + where + showReset rst = "Reset" <> show (L.reverse $ L.dropWhile not $ L.reverse $ sampleReset rst) + +-- | Helper to use forAll with MinCyclesReset, showing only the asserted portion of the sampled reset signal +forAllMinReset :: + forall dom n m. + (Monad m, KnownDomain dom, KnownNat n) => + H.Gen (MinCyclesReset dom n) -> + H.PropertyT m (MinCyclesReset dom n) +forAllMinReset gen = H.forAllWith showMinReset gen + where + showMinReset minRst = + let rst = fromMinCycles minRst + in "MinCyclesReset" <> show (L.reverse $ L.dropWhile not $ L.reverse $ sampleReset rst) + +-- ** Properties for MinCyclesReset functions ** + +-- | Property: genMinCyclesReset should generate resets where all assertion sequences are at least n cycles +prop_genMinCyclesReset_valid :: H.Property +prop_genMinCyclesReset_valid = H.property $ do + minReset <- forAllMinReset (genMinCyclesReset @TestDom d5) + let samples = sampleReset $ fromMinCycles minReset + -- All assertion sequences should be at least 5 cycles + H.footnote $ "Reset durations: " <> show (getResetDurations samples) + H.assert $ isResetAtLeastN 5 samples + +-- | Property: Coercing a single-cycle reset to n cycles should extend all assertions to exactly n cycles +prop_convert_exactness :: H.Property +prop_convert_exactness = H.property $ do + let reset1 = unsafeFromActiveHigh $ riseEvery @TestDom testClk resetGen enableGen d10 + minReset7 = convert @1 @7 testClk (toMinCycles testClk reset1) + samples = sampleReset $ fromMinCycles minReset7 + durations = getResetDurations samples + + H.footnote $ "Reset durations: " <> show durations + H.assert $ all (== 7) $ L.drop 1 durations -- Ignore startup behavior + +-- | Property: fromMinCycles . toMinCycles should preserve the reset signal +prop_roundtrip_to_from :: H.Property +prop_roundtrip_to_from = H.property $ do + reset0 <- forAllReset (genReset @TestDom) + let reset1 = fromMinCycles $ toMinCycles @1 testClk reset0 + samples0 = sampleReset reset0 + samples1 = sampleReset reset1 + + samples1 === samples0 + +-- | Property: Coercing from lower to higher minimum cycles should extend all assertion sequences +prop_convert_extends_reset :: H.Property +prop_convert_extends_reset = H.property $ do + minReset2 <- forAllMinReset (genMinCyclesReset @TestDom d2) + let minReset5 = convert @2 @5 testClk minReset2 + reset5 = fromMinCycles minReset5 + samples = sampleReset reset5 + + -- All assertion sequences should be at least 5 cycles + H.assert $ isResetAtLeastN 5 samples + +-- | Property: Coercing twice should extend all assertions to the final target cycle count +prop_convert_extends_exactness = H.property $ do + let reset1 = CE.orReset resetGen $ unsafeFromActiveHigh $ riseEvery @TestDom testClk resetGen enableGen d10 + minReset3 = convert @1 @3 testClk (toMinCycles testClk reset1) + minReset6 = convert @3 @6 testClk minReset3 + samples = sampleReset $ fromMinCycles minReset6 + durations = getResetDurations samples + + H.footnote $ "Reset1" <> show (L.take 20 $ sampleReset reset1) + H.footnote $ "Reset3" <> show (L.take 20 $ sampleReset $ fromMinCycles minReset3) + H.footnote $ "Reset6" <> show (L.take 20 $ sampleReset $ fromMinCycles minReset6) + H.footnote $ "Reset durations: " <> show durations + H.assert $ all (== 6) $ L.drop 1 durations -- Ignore startup behavior + +-- | Property: Coercing from higher to lower minimum cycles should not shorten assertion sequences +prop_convert_preserves_longer_reset :: H.Property +prop_convert_preserves_longer_reset = H.property $ do + minReset10 <- forAllMinReset (genMinCyclesReset @TestDom d10) + let minReset5 = convert @10 @5 testClk minReset10 + reset5 = fromMinCycles minReset5 + samples = sampleReset reset5 + + -- All assertion sequences should still be at least 10 cycles (not shortened) + H.assert $ isResetAtLeastN 10 samples + +-- | Property: Coercing to the same minimum cycles should be identity +prop_convert_identity :: H.Property +prop_convert_identity = H.property $ do + minReset <- forAllMinReset (genMinCyclesReset @TestDom d5) + let convertd = convert @5 @5 testClk minReset + samples0 = sampleReset $ fromMinCycles minReset + samples1 = sampleReset $ fromMinCycles convertd + + samples0 === samples1 + +-- | Property: extend should extend all assertion sequences to the target cycle count +prop_extend_extends :: H.Property +prop_extend_extends = H.property $ do + minReset2 <- forAllMinReset (genMinCyclesReset @TestDom @2 d2) + let minReset8 = MinReset.extend @2 @8 testClk minReset2 + samples = sampleReset $ fromMinCycles minReset8 + + -- All assertion sequences should be at least 8 cycles + H.assert $ isResetAtLeastN 8 samples + +-- | Property: fromExtended should preserve the underlying reset signal unchanged +prop_fromExtended_preserves :: H.Property +prop_fromExtended_preserves = H.property $ do + minReset10 <- forAllMinReset (genMinCyclesReset @TestDom d10) + let minReset5 = fromExtended @5 minReset10 + samples5 = sampleReset $ fromMinCycles minReset5 + samples10 = sampleReset $ fromMinCycles minReset10 + + -- Both should have the same underlying signal + samples5 === samples10 + +-- | Property: or should combine two resets using OR logic +prop_or_combines :: H.Property +prop_or_combines = H.property $ do + minReset5 <- forAllMinReset (genMinCyclesReset @TestDom d5) + minReset3 <- forAllMinReset (genMinCyclesReset d3) + let combined = or testClk minReset5 minReset3 + samples5 = sampleReset $ fromMinCycles minReset5 + samples3 = sampleReset $ fromMinCycles $ convert @3 @5 testClk minReset3 + samplesOr = sampleReset $ fromMinCycles combined + + samplesOr === L.zipWith (||) samples5 samples3 + +-- | Property: or with noReset should preserve the active reset +prop_or_left_identity :: H.Property +prop_or_left_identity = H.property $ do + minReset5 <- forAllMinReset (genMinCyclesReset @TestDom d5) + let combined = or testClk minReset5 (unsafeToMinCycles @3 $ CE.noReset) + samples = sampleReset $ fromMinCycles minReset5 + samplesOr = sampleReset $ fromMinCycles combined + + samplesOr === samples + +-- | Property: or with noReset on the left should preserve the active reset +prop_or_right_identity :: H.Property +prop_or_right_identity = H.property $ do + minReset5 <- forAllMinReset (genMinCyclesReset @TestDom d5) + let combined = or testClk (unsafeToMinCycles @3 $ CE.noReset) minReset5 + samples = sampleReset $ fromMinCycles minReset5 + samplesOr = sampleReset $ fromMinCycles combined + + samplesOr === samples + +tests :: TestTree +tests = $(testGroupGenerator) diff --git a/tests/unittests/main.hs b/tests/unittests/main.hs new file mode 100644 --- /dev/null +++ b/tests/unittests/main.hs @@ -0,0 +1,33 @@ +-- SPDX-FileCopyrightText: 2024 Google LLC +-- +-- SPDX-License-Identifier: Apache-2.0 + +module Main where + +import Test.Tasty +import Test.Tasty.Hedgehog +import Prelude + +import qualified Tests.VexRiscv.ClockTicks +import qualified Tests.VexRiscv.Random +import qualified Tests.VexRiscv.Reset + +tests :: TestTree +tests = + testGroup + "Tests" + [ Tests.VexRiscv.ClockTicks.tests + , Tests.VexRiscv.Random.tests + , Tests.VexRiscv.Reset.tests + ] + +setDefaultHedgehogTestLimit :: HedgehogTestLimit -> HedgehogTestLimit +setDefaultHedgehogTestLimit (HedgehogTestLimit Nothing) = HedgehogTestLimit (Just 1000) +setDefaultHedgehogTestLimit opt = opt + +main :: IO () +main = + defaultMain $ + adjustOption + setDefaultHedgehogTestLimit + tests