diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 12:29:11 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 12:29:11 +0100 |
| commit | 533bca9426ee3166433b29e84c8f942f7409981b (patch) | |
| tree | 5bfad6d46b06ace593ed7e55da60bf34b8943b67 | |
| parent | f6569b736d4ded08a011f55bd6001c89e899fd5c (diff) | |
| download | vericert-dev/asplos.tar.gz vericert-dev/asplos.zip | |
Annonimize submissiondev/asplos
81 files changed, 120 insertions, 216 deletions
diff --git a/.gitmodules b/.gitmodules deleted file mode 100644 index 64fe9ee..0000000 --- a/.gitmodules +++ /dev/null @@ -1,6 +0,0 @@ -[submodule "lib/CompCert"] - path = lib/CompCert - url = https://github.com/ymherklotz/CompCert.git -[submodule "lib/cohpred"] - path = lib/cohpred - url = https://gitlab.inria.fr/pred-tv/cohpred diff --git a/CITATION.cff b/CITATION.cff deleted file mode 100644 index c114ec6..0000000 --- a/CITATION.cff +++ /dev/null @@ -1,46 +0,0 @@ -# -*- mode: yaml -*- -cff-version: 1.2.0 -message: "If you use this software, please cite it as below." -authors: -- family-names: "Herklotz" - given-names: "Yann" - orcid: "https://orcid.org/0000-0002-2329-1029" -- family-names: "Pollard" - given-names: "James D." - orcid: "https://orcid.org/0000-0003-1404-1527" -- family-names: "Ramanathan" - given-names: "Nadesh" - orcid: "https://orcid.org/0000-0001-9083-8349" -- family-names: "Wickerson" - given-names: "John" - orcid: "https://orcid.org/0000-0001-6735-5533" -title: "Vericert" -version: 1.2.2 -doi: 10.5281/zenodo.5093839 -date-released: 2021-10-01 -url: "https://github.com/ymherklotz/vericert" -preferred-citation: - type: article - authors: - - family-names: "Herklotz" - given-names: "Yann" - orcid: "https://orcid.org/0000-0002-2329-1029" - - family-names: "Pollard" - given-names: "James D." - orcid: "https://orcid.org/0000-0003-1404-1527" - - family-names: "Ramanathan" - given-names: "Nadesh" - orcid: "https://orcid.org/0000-0001-9083-8349" - - family-names: "Wickerson" - given-names: "John" - orcid: "https://orcid.org/0000-0001-6735-5533" - doi: "10.1145/3485494" - journal: "Proc. ACM Program. Lang." - month: 11 - pages: 30 - title: "Formal Verification of High-Level Synthesis" - volume: 5 - year: 2021 - number: OOPSLA - publisher: Association for Computing Machinery - address: New York, NY, USA diff --git a/ChangeLog.org b/ChangeLog.org index 88c0953..baad0ab 100644 --- a/ChangeLog.org +++ b/ChangeLog.org @@ -1,6 +1,6 @@ # -*- fill-column: 80 -*- #+title: Vericert Changelog -#+author: Yann Herklotz +#+author: ___ ___ #+email: git@ymhg.org * Unreleased @@ -1,8 +1,21 @@ -#+title: +#+title: Scheduled Vericert -#+html: <a href="https://vericert.ymhg.org"><img src="https://vericert.ymhg.org/vericert-main.svg" width="100%" height="144" /></a> +* Scheduled Vericert -#+html: <p align=center><a href="https://github.com/ymherklotz/vericert/actions"><img src="https://github.com/ymherklotz/vericert/workflows/CI/badge.svg" /></a> <a href="https://vericert.ymhg.org/"><img src="https://github.com/ymherklotz/vericert-docs/workflows/docs/badge.svg" /></a></p> +This artefact contains modifications to Vericert with a scheduled back end, +together with a forward simulation proof from C to the scheduling language and a +testing backend that is not verified, but goes to Verilog. + +The top-level forward simulation proof can be found in =src/Compiler.v= +(=transf_c_program_correct=). + +There are a couple of =Admitted= theorems in the code, however, these are only +in: =src/hls/DVeriloggenproof.v=, =src/hls/HTLPargen.v= and +=src/hls/ClockRegisters.v=. These translation passes are only used for +benchmarking purposes, and are not used for the =transf_c_program_correct= +theorem. + +* Original README A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [[https://github.com/AbsInt/CompCert][CompCert]]. This ensures the correctness of the C to Verilog translation according to our Verilog semantics and @@ -52,7 +65,7 @@ together with the repository. To clone CompCert together with this project, and correct revision, you can run: #+begin_src shell -git clone -b v1.2.2 --recursive https://github.com/ymherklotz/vericert +git clone -b v1.2.2 --recursive https://github.com/___/vericert #+end_src If the repository is already cloned, you can run the following command to make sure that CompCert is @@ -113,11 +126,11 @@ following: ** Citation -If you use Vericert in any way, please cite it using our [[https://yannherklotz.com/papers/fvhls_oopsla21.pdf][OOPSLA'21 paper]]: +If you use Vericert in any way, please cite it using our [[https://______.com/papers/fvhls_oopsla21.pdf][OOPSLA'21 paper]]: #+begin_src bibtex -@inproceedings{herklotz21_fvhls, - author = {Herklotz, Yann and Pollard, James D. and Ramanathan, Nadesh and Wickerson, John}, +@inproceedings{___21_fvhls, + author = {___, ___ and ___, ___ D. and Ramanathan, ___ and Wickerson, John}, title = {Formal Verification of High-Level Synthesis}, year = {2021}, number = {OOPSLA}, diff --git a/benchmarks/getTanh/getTanh.cpp b/benchmarks/getTanh/getTanh.cpp index cdb1d24..b30f561 100644 --- a/benchmarks/getTanh/getTanh.cpp +++ b/benchmarks/getTanh/getTanh.cpp @@ -2,7 +2,6 @@ Function Name: getTanh Description: This function takes one input array and generates getTanh result for each elements. - Source: https://github.com/JianyiCheng/HLS-benchmarks/blob/master/DSS/getTanh/src/inlined.cpp */ @@ -112,4 +111,4 @@ int main(){ getTanh(A, atanh, sinh, cosh); -}
\ No newline at end of file +} diff --git a/doc/README.org b/doc/README.org index 4113ed9..12c8516 100644 --- a/doc/README.org +++ b/doc/README.org @@ -1,6 +1,6 @@ #+title: Vericert Documentation -The documentation for [[https://github.com/ymherklotz/vericert][Vericert]], which is written in the [[/documentation.org][documentation.org]] file. +The documentation for [[https://github.com/___/vericert][Vericert]], which is written in the [[/documentation.org][documentation.org]] file. * How to develop on documentation diff --git a/doc/common.org b/doc/common.org index aa27264..5299ef1 100644 --- a/doc/common.org +++ b/doc/common.org @@ -1,4 +1,4 @@ -#+author: Yann Herklotz +#+author: ___ ___ #+email: git@ymhg.org #+macro: version 1.2.2 diff --git a/doc/conf.py b/doc/conf.py index 7000f7b..6f6508b 100644 --- a/doc/conf.py +++ b/doc/conf.py @@ -18,8 +18,8 @@ # -- Project information ----------------------------------------------------- project = 'Vericert' -copyright = '2022 Yann Herklotz, John Wickerson' -author = 'Yann Herklotz, John Wickerson' +copyright = '2022 ___ ___, John Wickerson' +author = '___ ___, John Wickerson' # The full version, including alpha/beta/rc tags release = 'v1.2.2' diff --git a/doc/documentation.org b/doc/documentation.org index 5a1bf61..5b02f21 100644 --- a/doc/documentation.org +++ b/doc/documentation.org @@ -1,6 +1,6 @@ #+title: Vericert Manual #+subtitle: Release {{{version}}} -#+author: Yann Herklotz +#+author: ___ ___ #+email: git@ymhg.org #+language: en @@ -30,7 +30,7 @@ called [[https://compcert.org/compcert-C.html][CompCert]] to perform this transl :COPYING: t :END: -Copyright (C) 2019-2022 Yann Herklotz. +Copyright (C) 2019-2022 ___ ___. #+begin_quote Permission is granted to copy, distribute and/or modify this document diff --git a/doc/index.rst b/doc/index.rst index f5a7776..c3a1b29 100644 --- a/doc/index.rst +++ b/doc/index.rst @@ -42,20 +42,20 @@ have all been proven correct, providing a verified translation from C to Verilog Publications ------------ -:OOPSLA '21: Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson. Formal +:OOPSLA '21: ___ ___, ___ D. ___, ___ Ramanathan, and John Wickerson. Formal Verification of High-Level Synthesis. In *Proc. ACM Program. Lang.* 5, OOPSLA, 2021. -:LATTE '21: Yann Herklotz and John Wickerson. High-level synthesis tools should be proven +:LATTE '21: ___ ___ and John Wickerson. High-level synthesis tools should be proven correct. In *Workshop on Languages, Tools, and Techniques for Accelerator Design*, 2021. Mailing lists ------------- -For discussions, you can join the following mailing list: `lists.sr.ht/~ymherklotz/vericert-discuss <https://lists.sr.ht/~ymherklotz/vericert-discuss>`_. +For discussions, you can join the following mailing list: `lists.sr.ht/~___/vericert-discuss <https://lists.sr.ht/~___/vericert-discuss>`_. -For contributing patches to the `sourcehut <https://sr.ht/~ymherklotz/vericert/>`_ repository: -`lists.sr.ht/~ymherklotz/vericert-devel <https://lists.sr.ht/~ymherklotz/vericert-devel>`_. +For contributing patches to the `sourcehut <https://sr.ht/~___/vericert/>`_ repository: +`lists.sr.ht/~___/vericert-devel <https://lists.sr.ht/~___/vericert-devel>`_. Indices ======= diff --git a/doc/man.org b/doc/man.org index cb6143f..03beded 100644 --- a/doc/man.org +++ b/doc/man.org @@ -69,11 +69,11 @@ vericert - A formally verified high-level synthesis tool. * AUTHOR -Written by Yann Herklotz, Michalis Pardalos, James Pollard, Nadesh Ramanathan and John Wickerson. +Written by ___ ___, Michalis Pardalos, ___ ___, ___ Ramanathan and John Wickerson. * COPYRIGHT -Copyright (C) 2019-2022 Yann Herklotz <yann@yannherklotz.com> +Copyright (C) 2019-2022 ___ ___ <___@______.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index 5950e95..021aa53 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) (* Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2019-2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/scripts/docker/Dockerfile b/scripts/docker/Dockerfile index c66df6d..480acc9 100644 --- a/scripts/docker/Dockerfile +++ b/scripts/docker/Dockerfile @@ -9,7 +9,7 @@ ADD legup_polybench_syn.tar.gz /data/legup-polybench-syn ADD legup_polybench_syn_div.tar.gz /data/legup-polybench-syn-div ADD data.tar.gz /data -RUN git clone --recursive https://github.com/ymherklotz/vericert +RUN git clone --recursive https://github.com/___/vericert WORKDIR /vericert RUN git checkout oopsla21 diff --git a/scripts/docker/artifact.org b/scripts/docker/artifact.org index fa0a936..ec8025d 100644 --- a/scripts/docker/artifact.org +++ b/scripts/docker/artifact.org @@ -13,7 +13,7 @@ This artifact should support the claims made in the paper "Formal Verification o The artifact is available on Github, specifically on the ~oopsla21~ branch: -https://github.com/ymherklotz/vericert +https://github.com/___/vericert #+latex: \noindent This release is also archived on Zenodo permanently: @@ -23,7 +23,7 @@ http://doi.org/10.5281/zenodo.5093839 #+latex: \noindent However, for the purposes of this artifact review, a Docker image has been set up: -https://hub.docker.com/repository/docker/ymherklotz/vericert +https://hub.docker.com/repository/docker/___/vericert ** Claims that are not supported by the artifact @@ -38,8 +38,8 @@ In addition to that, the Vivado synthesis tool by Xilinx[fn:3] is also commercia First, the docker image needs to be downloaded and run, which contains the git repository: #+begin_src shell -docker pull ymherklotz/vericert:1.0 -docker run -it ymherklotz/vericert:1.0 sh +docker pull ___/vericert:1.0 +docker run -it ___/vericert:1.0 sh #+end_src Then, one just has to go into the directory which contains the git repository (~/vericert~) and open a ~nix-shell~, which will load a shell with all the correct dependencies loaded: @@ -259,7 +259,7 @@ Where $t$ is the tool being considered. A tex file is included in the ~/data/data~ directory, which unfortunately can only be compiled outside of the docker file, but will recreate the graphs from the paper using the csv files in the directory. This can be achieved using the following commands: #+begin_src shell -docker create ymherklotz/vericert:v1.0 # returns container ID +docker create ___/vericert:v1.0 # returns container ID docker cp $container_id:/data/data . docker rm $container_id cd data @@ -308,7 +308,7 @@ docker run -it <hash> sh The only dependency that is require is nix[fn:7]. Once that is installed, we can clone the Github repository and checkout the ~oopsla21~ branch: #+begin_src shell -git clone https://github.com/ymherklotz/vericert +git clone https://github.com/___/vericert cd vericert git checkout oopsla21 #+end_src diff --git a/scripts/docker/artifact.pdf b/scripts/docker/artifact.pdf Binary files differindex 05ec4fd..d8b7aab 100644 --- a/scripts/docker/artifact.pdf +++ b/scripts/docker/artifact.pdf diff --git a/scripts/quartus_synth.tcl b/scripts/quartus_synth.tcl index 6edbf0c..61a78c8 100644 --- a/scripts/quartus_synth.tcl +++ b/scripts/quartus_synth.tcl @@ -1,6 +1,6 @@ # PRiME pre-KAPow kernel flow # Performs pre-KAPow run steps for instrumenting arbitrary Verilog for power monitoring -# James Davis, 2015 +# ___ Davis, 2015 load_package flow diff --git a/scripts/synth-ssh-bambu.sh b/scripts/synth-ssh-bambu.sh deleted file mode 100755 index 5bc1a4d..0000000 --- a/scripts/synth-ssh-bambu.sh +++ /dev/null @@ -1,28 +0,0 @@ -#!/usr/bin/env bash - -# Assumes that the Verilog is passed on the command line, that the tcl file is in synth.tcl and -# returns encode_report.xml. - -scriptsdir=$(dirname "$(readlink -f "$BASH_SOURCE")") - -num=$1 -bench=$2 -output=$3 -machine=ee-beholder${num}.ee.ic.ac.uk -user=ymh15 -files="$scriptsdir/synth-bambu.tcl $output/$bench/main_top.v" -log="$output/${bench}_synth.log" - -date >$log - -temp=$(ssh $user@$machine "mktemp -d") - ->&2 echo "synthesising $bench $temp" -rsync $files $user@$machine:$temp/ >>$log 2>&1 -ssh $user@$machine \ - "bash -lc 'cd $temp && vivado -mode batch -source synth-bambu.tcl'" \ - >>$log 2>&1 -rsync $user@$machine:$temp/encode_report.xml $output/${bench}_report.xml >>$log 2>&1 -# ssh $user@$machine "rm -rf '$temp'" >>$log 2>&1 -rm -f main.sv >>$log 2>&1 ->&2 echo "done $bench" diff --git a/scripts/synth-ssh.sh b/scripts/synth-ssh.sh deleted file mode 100755 index ca255e1..0000000 --- a/scripts/synth-ssh.sh +++ /dev/null @@ -1,28 +0,0 @@ -#!/usr/bin/env bash - -# Assumes that the Verilog is passed on the command line, that the tcl file is in synth.tcl and -# returns encode_report.xml. - -scriptsdir=$(dirname "$(readlink -f "$BASH_SOURCE")") - -num=$1 -bench=$2 -output=$3 -machine=ee-beholder${num}.ee.ic.ac.uk -user=ymh15 -files="$scriptsdir/synth.tcl $output/$bench.sv" -log="$output/${bench}_synth.log" - -date >$log - -temp=$(ssh $user@$machine "mktemp -d") - ->&2 echo "synthesising $bench $temp" -rsync $files $user@$machine:$temp/ >>$log 2>&1 -ssh $user@$machine \ - "bash -lc 'cd $temp && cp $(basename $bench).sv main.sv && vivado -mode batch -source synth.tcl'" \ - >>$log 2>&1 -rsync $user@$machine:$temp/encode_report.xml $output/${bench}_report.xml >>$log 2>&1 -# ssh $user@$machine "rm -rf '$temp'" >>$log 2>&1 -rm -f main.sv >>$log 2>&1 ->&2 echo "done $bench" diff --git a/scripts/synthesis-results.org b/scripts/synthesis-results.org index 602b2ba..43ca413 100644 --- a/scripts/synthesis-results.org +++ b/scripts/synthesis-results.org @@ -24,11 +24,11 @@ Usage: *synthesis-results* [options...] [files...] * AUTHOR -Written by Yann Herklotz. +Written by ___ ___. * COPYRIGHT -Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com> +Copyright (C) 2022 ___ ___ <___@______.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/scripts/synthesis-results.scm b/scripts/synthesis-results.scm index 3760cfb..db73ed7 100755 --- a/scripts/synthesis-results.scm +++ b/scripts/synthesis-results.scm @@ -1,7 +1,7 @@ #! /usr/local/bin/csi -ss ;; -*- mode: scheme -*- ;; -;; Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com> +;; Copyright (C) 2022 ___ ___ <___@______.com> ;; ;; This program is free software: you can redistribute it and/or modify ;; it under the terms of the GNU General Public License as published by @@ -61,7 +61,7 @@ (print "Usage: " (program-name) " [options...] [files...]") (newline) (print (args:usage opts)) - (print "Report bugs to git at yannherklotz dot com."))) + (print "Report bugs to git at ______ dot com."))) (exit 1)) (define (map-names n) diff --git a/src/Compiler.v b/src/Compiler.v index deb7da2..6b509bb 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -1,7 +1,7 @@ (*| .. Vericert: Verified high-level synthesis. - Copyright (C) 2019-2022 Yann Herklotz <yann@yannherklotz.com> + Copyright (C) 2019-2022 ___ ___ <___@______.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/src/HLSOpts.v b/src/HLSOpts.v index efa7ed0..2b9cd13 100644 --- a/src/HLSOpts.v +++ b/src/HLSOpts.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2019-2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/Simulator.v b/src/Simulator.v index 3df0c7f..ea43e93 100644 --- a/src/Simulator.v +++ b/src/Simulator.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/common/DecEq.v b/src/common/DecEq.v index 5f85e9b..02749a6 100644 --- a/src/common/DecEq.v +++ b/src/common/DecEq.v @@ -1,7 +1,7 @@ (*| .. Vericert: Verified high-level synthesis. - Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + Copyright (C) 2020-2022 ___ ___ <___@______.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index e56bda0..09bc9a6 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -1,7 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2020-2021 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/common/Maps.v b/src/common/Maps.v index cb9dc2c..3c4588c 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -1,7 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2020 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/common/Monad.v b/src/common/Monad.v index 41a57e9..5e9b41e 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/common/NonEmpty.v b/src/common/NonEmpty.v index 01456d0..e149048 100644 --- a/src/common/NonEmpty.v +++ b/src/common/NonEmpty.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021-2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2021-2022 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/common/Optionmonad.v b/src/common/Optionmonad.v index 8112eb9..974d49d 100644 --- a/src/common/Optionmonad.v +++ b/src/common/Optionmonad.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2022 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/common/Show.v b/src/common/Show.v index 20c07e7..3e9a3dc 100644 --- a/src/common/Show.v +++ b/src/common/Show.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2019-2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v index c667fd9..d50f961 100644 --- a/src/common/Statemonad.v +++ b/src/common/Statemonad.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index da046f3..888366a 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -1,7 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2021 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2019-2021 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v index 3a27cc6..7482f85 100644 --- a/src/common/ZExtra.v +++ b/src/common/ZExtra.v @@ -1,7 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2020 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 0a83f02..a18e48f 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2019-2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v index f201914..bbfba72 100644 --- a/src/hls/Abstr.v +++ b/src/hls/Abstr.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021-2023 Yann Herklotz <git@yannherklotz.com> + * Copyright (C) 2021-2023 ___ ___ <git@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/Array.v b/src/hls/Array.v index 8b7d262..2b23c50 100644 --- a/src/hls/Array.v +++ b/src/hls/Array.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 James Pollard <j@mes.dev> + * Copyright (C) 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index 4941b0e..eaf8484 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -1,7 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2020-2022 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/ClockRegisters.v b/src/hls/ClockRegisters.v index fee89fb..fba0027 100644 --- a/src/hls/ClockRegisters.v +++ b/src/hls/ClockRegisters.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2023 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2023 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/CondElim.v b/src/hls/CondElim.v index 9f51053..234f99b 100644 --- a/src/hls/CondElim.v +++ b/src/hls/CondElim.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2022 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/CondElimproof.v b/src/hls/CondElimproof.v index 7e6e035..75d08f6 100644 --- a/src/hls/CondElimproof.v +++ b/src/hls/CondElimproof.v @@ -1,7 +1,7 @@ (*| .. Vericert: Verified high-level synthesis. - Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com> + Copyright (C) 2022 ___ ___ <___@______.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/src/hls/DHTL.v b/src/hls/DHTL.v index 6be82ae..639a98f 100644 --- a/src/hls/DHTL.v +++ b/src/hls/DHTL.v @@ -1,7 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2023 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2020-2023 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/DMemorygen.v b/src/hls/DMemorygen.v index d6c4fe8..0a3f63b 100644 --- a/src/hls/DMemorygen.v +++ b/src/hls/DMemorygen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2021 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/DVeriloggen.v b/src/hls/DVeriloggen.v index 6b47dd0..bf8197e 100644 --- a/src/hls/DVeriloggen.v +++ b/src/hls/DVeriloggen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2023 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2023 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/DVeriloggenproof.v b/src/hls/DVeriloggenproof.v index 197d9a6..a2e953a 100644 --- a/src/hls/DVeriloggenproof.v +++ b/src/hls/DVeriloggenproof.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/DeadBlocks.v b/src/hls/DeadBlocks.v index 644ed1f..4b5388b 100644 --- a/src/hls/DeadBlocks.v +++ b/src/hls/DeadBlocks.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2022 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/FunctionalUnits.v b/src/hls/FunctionalUnits.v index e94b8e8..a87ea50 100644 --- a/src/hls/FunctionalUnits.v +++ b/src/hls/FunctionalUnits.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2021 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/Gible.v b/src/hls/Gible.v index b8feb37..1623e5c 100644 --- a/src/hls/Gible.v +++ b/src/hls/Gible.v @@ -1,7 +1,7 @@ (*| .. Vericert: Verified high-level synthesis. - Copyright (C) 2019-2022 Yann Herklotz <yann@yannherklotz.com> + Copyright (C) 2019-2022 ___ ___ <___@______.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/src/hls/GiblePar.v b/src/hls/GiblePar.v index 69afc27..678525e 100644 --- a/src/hls/GiblePar.v +++ b/src/hls/GiblePar.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-2022 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/GiblePargen.v b/src/hls/GiblePargen.v index e3cfcda..f429c6e 100644 --- a/src/hls/GiblePargen.v +++ b/src/hls/GiblePargen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-2022 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/GiblePargenproof.v b/src/hls/GiblePargenproof.v index 95f0bb1..a4092a3 100644 --- a/src/hls/GiblePargenproof.v +++ b/src/hls/GiblePargenproof.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2023 Yann Herklotz <git@yannherklotz.com> + * Copyright (C) 2020-2023 ___ ___ <git@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/GiblePargenproofBackward.v b/src/hls/GiblePargenproofBackward.v index 43e97a6..4a1cd4a 100644 --- a/src/hls/GiblePargenproofBackward.v +++ b/src/hls/GiblePargenproofBackward.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2023 Yann Herklotz <git@yannherklotz.com> + * Copyright (C) 2023 ___ ___ <git@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/GiblePargenproofCommon.v b/src/hls/GiblePargenproofCommon.v index 73bfa42..7563c9d 100644 --- a/src/hls/GiblePargenproofCommon.v +++ b/src/hls/GiblePargenproofCommon.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2023 Yann Herklotz <git@yannherklotz.com> + * Copyright (C) 2023 ___ ___ <git@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/GiblePargenproofEquiv.v b/src/hls/GiblePargenproofEquiv.v index 6995bf5..dfae67d 100644 --- a/src/hls/GiblePargenproofEquiv.v +++ b/src/hls/GiblePargenproofEquiv.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2023 Yann Herklotz <git@yannherklotz.com> + * Copyright (C) 2023 ___ ___ <git@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/GiblePargenproofForward.v b/src/hls/GiblePargenproofForward.v index 48fe922..add5c48 100644 --- a/src/hls/GiblePargenproofForward.v +++ b/src/hls/GiblePargenproofForward.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2023 Yann Herklotz <git@yannherklotz.com> + * Copyright (C) 2023 ___ ___ <git@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/GibleSeq.v b/src/hls/GibleSeq.v index 61a77e7..b4ab6fb 100644 --- a/src/hls/GibleSeq.v +++ b/src/hls/GibleSeq.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-2022 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/GibleSeqgen.v b/src/hls/GibleSeqgen.v index 127ee53..d1ae6bf 100644 --- a/src/hls/GibleSeqgen.v +++ b/src/hls/GibleSeqgen.v @@ -1,7 +1,7 @@ (*| .. Vericert: Verified high-level synthesis. - Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + Copyright (C) 2020-2022 ___ ___ <___@______.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/src/hls/GibleSeqgenproof.v b/src/hls/GibleSeqgenproof.v index 1d1d4b7..799cfb8 100644 --- a/src/hls/GibleSeqgenproof.v +++ b/src/hls/GibleSeqgenproof.v @@ -1,7 +1,7 @@ (*| .. Vericert: Verified high-level synthesis. - Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + Copyright (C) 2020-2022 ___ ___ <___@______.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/src/hls/HTL.v b/src/hls/HTL.v index 8cebbfd..c6799ec 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -1,7 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2020 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/HTLBlockgen.v b/src/hls/HTLBlockgen.v index 5f40962..2bab011 100644 --- a/src/hls/HTLBlockgen.v +++ b/src/hls/HTLBlockgen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index e493989..b231948 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2023 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2023 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 41a1798..cfbac97 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -1,7 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2020 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 5b179e1..d26948d 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -1,7 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2020 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v index a088a54..ba3bbf1 100644 --- a/src/hls/HashTree.v +++ b/src/hls/HashTree.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021-2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2021-2022 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index ecafc13..9c641e5 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -1,7 +1,7 @@ (*| .. Vericert: Verified high-level synthesis. - Copyright (C) 2021-2022 Yann Herklotz <yann@yannherklotz.com> + Copyright (C) 2021-2022 ___ ___ <___@______.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/src/hls/IfConversionOracle.ml b/src/hls/IfConversionOracle.ml index e9a1563..d2451b7 100644 --- a/src/hls/IfConversionOracle.ml +++ b/src/hls/IfConversionOracle.ml @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2023 Yann Herklotz <git@yannherklotz.com> + * Copyright (C) 2023 ___ ___ <git@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/IfConversionproof.v b/src/hls/IfConversionproof.v index eedb318..ad9c2bd 100644 --- a/src/hls/IfConversionproof.v +++ b/src/hls/IfConversionproof.v @@ -1,7 +1,7 @@ (*| .. Vericert: Verified high-level synthesis. - Copyright (C) 2022 Yann Herklotz <yann@yannherklotz.com> + Copyright (C) 2022 ___ ___ <___@______.com> This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml index 07b1be9..63d1731 100644 --- a/src/hls/Partition.ml +++ b/src/hls/Partition.ml @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-2022 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/Pipeline.v b/src/hls/Pipeline.v index 67ab1f5..f1829ff 100644 --- a/src/hls/Pipeline.v +++ b/src/hls/Pipeline.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-2021 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v index 76634a6..289e962 100644 --- a/src/hls/PipelineOp.v +++ b/src/hls/PipelineOp.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2021 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/PrintDHTL.ml b/src/hls/PrintDHTL.ml index e7a1aaf..2c3b79f 100644 --- a/src/hls/PrintDHTL.ml +++ b/src/hls/PrintDHTL.ml @@ -1,6 +1,6 @@ (* -*- mode: tuareg -*- * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2019-2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml index 5963be0..b84a731 100644 --- a/src/hls/PrintHTL.ml +++ b/src/hls/PrintHTL.ml @@ -1,6 +1,6 @@ (* -*- mode: tuareg -*- * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2019-2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/PrintVerilog.ml b/src/hls/PrintVerilog.ml index 2e0f0e1..343d890 100644 --- a/src/hls/PrintVerilog.ml +++ b/src/hls/PrintVerilog.ml @@ -1,7 +1,7 @@ (* -*- mode: tuareg -*- * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2019-2020 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/PrintVerilog.mli b/src/hls/PrintVerilog.mli index 6a15ee9..ae28219 100644 --- a/src/hls/PrintVerilog.mli +++ b/src/hls/PrintVerilog.mli @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2019-2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/RTLParFU.v b/src/hls/RTLParFU.v index f97ed95..fcc5679 100644 --- a/src/hls/RTLParFU.v +++ b/src/hls/RTLParFU.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-2021 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/RTLParFUgen.v b/src/hls/RTLParFUgen.v index f1b3ba6..8b01b90 100644 --- a/src/hls/RTLParFUgen.v +++ b/src/hls/RTLParFUgen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2021 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2021 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml index 248d0f8..4938a88 100644 --- a/src/hls/Schedule.ml +++ b/src/hls/Schedule.ml @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020-2022 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020-2022 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/ValueInt.v b/src/hls/ValueInt.v index 06b5630..c994f3f 100644 --- a/src/hls/ValueInt.v +++ b/src/hls/ValueInt.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/ValueVal.v b/src/hls/ValueVal.v index 96e0b1c..6564705 100644 --- a/src/hls/ValueVal.v +++ b/src/hls/ValueVal.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 56d7332..f9a3af8 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -1,7 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> - * 2020 James Pollard <j@mes.dev> + * Copyright (C) 2019-2020 ___ ___ <___@______.com> + * 2020 ___ ___ <___> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v index aba2293..c91cf0e 100644 --- a/src/hls/Veriloggen.v +++ b/src/hls/Veriloggen.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index d1494ec..df0c720 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -1,6 +1,6 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2020 ___ ___ <___@______.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by |