diff options
| author | Philipp Tomsich <philipp.tomsich@vrull.eu> | 2023-05-29 21:11:07 +0200 |
|---|---|---|
| committer | Philipp Tomsich <philipp.tomsich@vrull.eu> | 2023-05-29 23:18:47 +0200 |
| commit | 3fca4c87b98ebac2c1ecb174e22b4f57c3b1d4ee (patch) | |
| tree | 686cd88aa17626b1f4c7ab8baaa11879121787ed | |
| parent | 80b4eaf40f67f87bfd719ea08dfae37a657478e7 (diff) | |
| download | sail-riscv-update-copyright-headers.zip sail-riscv-update-copyright-headers.tar.gz sail-riscv-update-copyright-headers.tar.bz2 | |
apply_headers: regenerate copyright headersupdate-copyright-headers
91 files changed, 1075 insertions, 79 deletions
diff --git a/handwritten_support/mem_metadata.lem b/handwritten_support/mem_metadata.lem index b056bf4..eadcada 100644 --- a/handwritten_support/mem_metadata.lem +++ b/handwritten_support/mem_metadata.lem @@ -6,7 +6,7 @@ (* in the prover_snapshots directory (which include copies of their *) (* licences), is subject to the BSD two-clause licence below. *) (* *) -(* Copyright (c) 2017-2021 *) +(* Copyright (c) 2017-2023 *) (* Prashanth Mundkur *) (* Rishiyur S. Nikhil and Bluespec, Inc. *) (* Jon French *) @@ -23,6 +23,8 @@ (* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo *) (* Peter Rugg *) (* Aril Computer Corp., for contributions by Scott Johnson *) +(* Philipp Tomsich *) +(* VRULL GmbH, for contributions by its employees *) (* *) (* All rights reserved. *) (* *) diff --git a/handwritten_support/mem_metadata.v b/handwritten_support/mem_metadata.v index 43f617b..dfdbec2 100644 --- a/handwritten_support/mem_metadata.v +++ b/handwritten_support/mem_metadata.v @@ -6,7 +6,7 @@ (* in the prover_snapshots directory (which include copies of their *) (* licences), is subject to the BSD two-clause licence below. *) (* *) -(* Copyright (c) 2017-2021 *) +(* Copyright (c) 2017-2023 *) (* Prashanth Mundkur *) (* Rishiyur S. Nikhil and Bluespec, Inc. *) (* Jon French *) @@ -23,6 +23,8 @@ (* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo *) (* Peter Rugg *) (* Aril Computer Corp., for contributions by Scott Johnson *) +(* Philipp Tomsich *) +(* VRULL GmbH, for contributions by its employees *) (* *) (* All rights reserved. *) (* *) diff --git a/handwritten_support/riscv_extras.lem b/handwritten_support/riscv_extras.lem index 93f19ab..a476136 100644 --- a/handwritten_support/riscv_extras.lem +++ b/handwritten_support/riscv_extras.lem @@ -6,7 +6,7 @@ (* in the prover_snapshots directory (which include copies of their *) (* licences), is subject to the BSD two-clause licence below. *) (* *) -(* Copyright (c) 2017-2021 *) +(* Copyright (c) 2017-2023 *) (* Prashanth Mundkur *) (* Rishiyur S. Nikhil and Bluespec, Inc. *) (* Jon French *) @@ -23,6 +23,8 @@ (* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo *) (* Peter Rugg *) (* Aril Computer Corp., for contributions by Scott Johnson *) +(* Philipp Tomsich *) +(* VRULL GmbH, for contributions by its employees *) (* *) (* All rights reserved. *) (* *) diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index bf3e7bc..ca1c555 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -6,7 +6,7 @@ (* in the prover_snapshots directory (which include copies of their *) (* licences), is subject to the BSD two-clause licence below. *) (* *) -(* Copyright (c) 2017-2021 *) +(* Copyright (c) 2017-2023 *) (* Prashanth Mundkur *) (* Rishiyur S. Nikhil and Bluespec, Inc. *) (* Jon French *) @@ -23,6 +23,8 @@ (* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo *) (* Peter Rugg *) (* Aril Computer Corp., for contributions by Scott Johnson *) +(* Philipp Tomsich *) +(* VRULL GmbH, for contributions by its employees *) (* *) (* All rights reserved. *) (* *) diff --git a/handwritten_support/riscv_extras_fdext.lem b/handwritten_support/riscv_extras_fdext.lem index 893c39a..b91e571 100644 --- a/handwritten_support/riscv_extras_fdext.lem +++ b/handwritten_support/riscv_extras_fdext.lem @@ -6,7 +6,7 @@ (* in the prover_snapshots directory (which include copies of their *) (* licences), is subject to the BSD two-clause licence below. *) (* *) -(* Copyright (c) 2017-2021 *) +(* Copyright (c) 2017-2023 *) (* Prashanth Mundkur *) (* Rishiyur S. Nikhil and Bluespec, Inc. *) (* Jon French *) @@ -23,6 +23,8 @@ (* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo *) (* Peter Rugg *) (* Aril Computer Corp., for contributions by Scott Johnson *) +(* Philipp Tomsich *) +(* VRULL GmbH, for contributions by its employees *) (* *) (* All rights reserved. *) (* *) diff --git a/handwritten_support/riscv_extras_sequential.lem b/handwritten_support/riscv_extras_sequential.lem index ddfe74f..41ca9c6 100644 --- a/handwritten_support/riscv_extras_sequential.lem +++ b/handwritten_support/riscv_extras_sequential.lem @@ -6,7 +6,7 @@ (* in the prover_snapshots directory (which include copies of their *) (* licences), is subject to the BSD two-clause licence below. *) (* *) -(* Copyright (c) 2017-2021 *) +(* Copyright (c) 2017-2023 *) (* Prashanth Mundkur *) (* Rishiyur S. Nikhil and Bluespec, Inc. *) (* Jon French *) @@ -23,6 +23,8 @@ (* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo *) (* Peter Rugg *) (* Aril Computer Corp., for contributions by Scott Johnson *) +(* Philipp Tomsich *) +(* VRULL GmbH, for contributions by its employees *) (* *) (* All rights reserved. *) (* *) diff --git a/model/main.sail b/model/main.sail index e4b1e0d..6887120 100644 --- a/model/main.sail +++ b/model/main.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/prelude.sail b/model/prelude.sail index fbf30ff..24363b9 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/prelude_mapping.sail b/model/prelude_mapping.sail index b6dfe6c..343df86 100644 --- a/model/prelude_mapping.sail +++ b/model/prelude_mapping.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/prelude_mem.sail b/model/prelude_mem.sail index 4588d38..1b27d49 100644 --- a/model/prelude_mem.sail +++ b/model/prelude_mem.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/prelude_mem_metadata.sail b/model/prelude_mem_metadata.sail index 2752d27..e714189 100644 --- a/model/prelude_mem_metadata.sail +++ b/model/prelude_mem_metadata.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_addr_checks.sail b/model/riscv_addr_checks.sail index 5211dcb..33091d9 100644 --- a/model/riscv_addr_checks.sail +++ b/model/riscv_addr_checks.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_addr_checks_common.sail b/model/riscv_addr_checks_common.sail index 0194372..0557906 100644 --- a/model/riscv_addr_checks_common.sail +++ b/model/riscv_addr_checks_common.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_analysis.sail b/model/riscv_analysis.sail index 598763d..02f5d95 100644 --- a/model/riscv_analysis.sail +++ b/model/riscv_analysis.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_csr_ext.sail b/model/riscv_csr_ext.sail index 230ee19..6a69606 100644 --- a/model/riscv_csr_ext.sail +++ b/model/riscv_csr_ext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 31872d3..e3f8f5b 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_decode_ext.sail b/model/riscv_decode_ext.sail index e943ec5..b6b4bb8 100644 --- a/model/riscv_decode_ext.sail +++ b/model/riscv_decode_ext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_ext_regs.sail b/model/riscv_ext_regs.sail index 1cd82f3..1ff956e 100644 --- a/model/riscv_ext_regs.sail +++ b/model/riscv_ext_regs.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_fdext_control.sail b/model/riscv_fdext_control.sail index 7e299a7..8724db8 100644 --- a/model/riscv_fdext_control.sail +++ b/model/riscv_fdext_control.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_fdext_regs.sail b/model/riscv_fdext_regs.sail index a5377b1..d2af59f 100644 --- a/model/riscv_fdext_regs.sail +++ b/model/riscv_fdext_regs.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_fetch.sail b/model/riscv_fetch.sail index 3120cc6..7a083a7 100644 --- a/model/riscv_fetch.sail +++ b/model/riscv_fetch.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_fetch_rvfi.sail b/model/riscv_fetch_rvfi.sail index 5c7ba3b..de17b8f 100644 --- a/model/riscv_fetch_rvfi.sail +++ b/model/riscv_fetch_rvfi.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_flen_D.sail b/model/riscv_flen_D.sail index d945a2f..4c924b5 100644 --- a/model/riscv_flen_D.sail +++ b/model/riscv_flen_D.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_flen_F.sail b/model/riscv_flen_F.sail index b540cf8..358e14b 100644 --- a/model/riscv_flen_F.sail +++ b/model/riscv_flen_F.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_freg_type.sail b/model/riscv_freg_type.sail index c092f34..816fb90 100644 --- a/model/riscv_freg_type.sail +++ b/model/riscv_freg_type.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 22523e2..6e64101 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail index b6d792c..d2d7832 100644 --- a/model/riscv_insts_base.sail +++ b/model/riscv_insts_base.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_begin.sail b/model/riscv_insts_begin.sail index f5cc2e4..fae285c 100644 --- a/model/riscv_insts_begin.sail +++ b/model/riscv_insts_begin.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_cdext.sail b/model/riscv_insts_cdext.sail index 77a6302..dd95469 100644 --- a/model/riscv_insts_cdext.sail +++ b/model/riscv_insts_cdext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_cext.sail b/model/riscv_insts_cext.sail index 0155515..42bc2e7 100644 --- a/model/riscv_insts_cext.sail +++ b/model/riscv_insts_cext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_cfext.sail b/model/riscv_insts_cfext.sail index 9aa94ef..b952901 100644 --- a/model/riscv_insts_cfext.sail +++ b/model/riscv_insts_cfext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail index b5542ea..ff1c4c1 100644 --- a/model/riscv_insts_dext.sail +++ b/model/riscv_insts_dext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_end.sail b/model/riscv_insts_end.sail index a94b88a..6a1af88 100644 --- a/model/riscv_insts_end.sail +++ b/model/riscv_insts_end.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail index 7bfc43f..c7e1541 100644 --- a/model/riscv_insts_fext.sail +++ b/model/riscv_insts_fext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_hints.sail b/model/riscv_insts_hints.sail index d9beeed..bc803fa 100644 --- a/model/riscv_insts_hints.sail +++ b/model/riscv_insts_hints.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_mext.sail b/model/riscv_insts_mext.sail index c6bb91f..de0e093 100644 --- a/model/riscv_insts_mext.sail +++ b/model/riscv_insts_mext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_next.sail b/model/riscv_insts_next.sail index 98147f4..584f1cc 100644 --- a/model/riscv_insts_next.sail +++ b/model/riscv_insts_next.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_rmem.sail b/model/riscv_insts_rmem.sail index e4970dc..230a347 100644 --- a/model/riscv_insts_rmem.sail +++ b/model/riscv_insts_rmem.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_zba.sail b/model/riscv_insts_zba.sail index 355f1b4..20bd7fe 100644 --- a/model/riscv_insts_zba.sail +++ b/model/riscv_insts_zba.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* ****************************************************************** */ union clause ast = RISCV_SLLIUW : (bits(6), regidx, regidx) diff --git a/model/riscv_insts_zbb.sail b/model/riscv_insts_zbb.sail index 311445c..2536011 100644 --- a/model/riscv_insts_zbb.sail +++ b/model/riscv_insts_zbb.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* ****************************************************************** */ union clause ast = RISCV_RORIW : (bits(5), regidx, regidx) diff --git a/model/riscv_insts_zbc.sail b/model/riscv_insts_zbc.sail index ac74b50..e237c97 100644 --- a/model/riscv_insts_zbc.sail +++ b/model/riscv_insts_zbc.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* ****************************************************************** */ union clause ast = RISCV_CLMUL : (regidx, regidx, regidx) diff --git a/model/riscv_insts_zbkb.sail b/model/riscv_insts_zbkb.sail index a4d8fc4..fd993d9 100644 --- a/model/riscv_insts_zbkb.sail +++ b/model/riscv_insts_zbkb.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* ****************************************************************** */ union clause ast = ZBKB_RTYPE : (regidx, regidx, regidx, brop_zbkb) diff --git a/model/riscv_insts_zbkx.sail b/model/riscv_insts_zbkx.sail index 0a155c2..1d4d7ca 100644 --- a/model/riscv_insts_zbkx.sail +++ b/model/riscv_insts_zbkx.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* ****************************************************************** */ union clause ast = RISCV_XPERM8 : (regidx, regidx, regidx) diff --git a/model/riscv_insts_zbs.sail b/model/riscv_insts_zbs.sail index 9e017cd..0a79dd6 100644 --- a/model/riscv_insts_zbs.sail +++ b/model/riscv_insts_zbs.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* ****************************************************************** */ union clause ast = ZBS_IOP : (bits(6), regidx, regidx, biop_zbs) diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail index 2b425dc..9a7f05c 100644 --- a/model/riscv_insts_zfa.sail +++ b/model/riscv_insts_zfa.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* FLI.H */ union clause ast = RISCV_FLI_H : (bits(5), regidx) diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail index 9bb06cb..fa388c2 100644 --- a/model/riscv_insts_zfh.sail +++ b/model/riscv_insts_zfh.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* **************************************************************** */ /* This file specifies the instructions in the Zfh extension */ /* (half precision floating point). */ diff --git a/model/riscv_insts_zicond.sail b/model/riscv_insts_zicond.sail index 7ecfcb3..a1f4c02 100644 --- a/model/riscv_insts_zicond.sail +++ b/model/riscv_insts_zicond.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + union clause ast = ZICOND_RTYPE : (regidx, regidx, regidx, zicondop) mapping clause encdec = ZICOND_RTYPE(rs2, rs1, rd, RISCV_CZERO_EQZ) if haveZicond() diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 5fd0f4f..b932834 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_insts_zkn.sail b/model/riscv_insts_zkn.sail index 89f81fa..c52e20d 100644 --- a/model/riscv_insts_zkn.sail +++ b/model/riscv_insts_zkn.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* * Scalar Cryptography Extension - Scalar SHA256 instructions (RV32/RV64) * ---------------------------------------------------------------------- diff --git a/model/riscv_insts_zks.sail b/model/riscv_insts_zks.sail index 153e1be..cdd8fd3 100644 --- a/model/riscv_insts_zks.sail +++ b/model/riscv_insts_zks.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* * Scalar Cryptography Extension - Scalar SM3 instructions * ---------------------------------------------------------------------- diff --git a/model/riscv_jalr_rmem.sail b/model/riscv_jalr_rmem.sail index a327dff..e9e4cbd 100644 --- a/model/riscv_jalr_rmem.sail +++ b/model/riscv_jalr_rmem.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail index d115744..9d370c6 100644 --- a/model/riscv_jalr_seq.sail +++ b/model/riscv_jalr_seq.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_mem.sail b/model/riscv_mem.sail index 37799d4..5e50fc7 100644 --- a/model/riscv_mem.sail +++ b/model/riscv_mem.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_misa_ext.sail b/model/riscv_misa_ext.sail index 94b9400..bc6396f 100644 --- a/model/riscv_misa_ext.sail +++ b/model/riscv_misa_ext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_next_control.sail b/model/riscv_next_control.sail index 2f63b87..432fd0d 100644 --- a/model/riscv_next_control.sail +++ b/model/riscv_next_control.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_next_regs.sail b/model/riscv_next_regs.sail index 1def582..507f50c 100644 --- a/model/riscv_next_regs.sail +++ b/model/riscv_next_regs.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_pc_access.sail b/model/riscv_pc_access.sail index 8c0e066..9c3c742 100644 --- a/model/riscv_pc_access.sail +++ b/model/riscv_pc_access.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index ea27f48..aed9966 100644 --- a/model/riscv_platform.sail +++ b/model/riscv_platform.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 064d058..998fb92 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index 43e2d5d..9b76c2d 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_pte.sail b/model/riscv_pte.sail index a95b20d..90345cc 100644 --- a/model/riscv_pte.sail +++ b/model/riscv_pte.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_ptw.sail b/model/riscv_ptw.sail index 1a128d2..2b7ef45 100644 --- a/model/riscv_ptw.sail +++ b/model/riscv_ptw.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_reg_type.sail b/model/riscv_reg_type.sail index dcc278b..5428587 100644 --- a/model/riscv_reg_type.sail +++ b/model/riscv_reg_type.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_regs.sail b/model/riscv_regs.sail index a65c6c5..8391ef0 100644 --- a/model/riscv_regs.sail +++ b/model/riscv_regs.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 5daddcb..9f94c47 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_step.sail b/model/riscv_step.sail index d1d0e47..ebf3b3f 100644 --- a/model/riscv_step.sail +++ b/model/riscv_step.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_step_common.sail b/model/riscv_step_common.sail index 7284dc7..2e81035 100644 --- a/model/riscv_step_common.sail +++ b/model/riscv_step_common.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_step_ext.sail b/model/riscv_step_ext.sail index e2abd8d..2232c72 100644 --- a/model/riscv_step_ext.sail +++ b/model/riscv_step_ext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_step_rvfi.sail b/model/riscv_step_rvfi.sail index 816d809..585e643 100644 --- a/model/riscv_step_rvfi.sail +++ b/model/riscv_step_rvfi.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_sync_exception.sail b/model/riscv_sync_exception.sail index 2fe2dd6..65ce95f 100644 --- a/model/riscv_sync_exception.sail +++ b/model/riscv_sync_exception.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6ec39d1..c2d9680 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_sys_exceptions.sail b/model/riscv_sys_exceptions.sail index 94e57dc..c5867de 100644 --- a/model/riscv_sys_exceptions.sail +++ b/model/riscv_sys_exceptions.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 129ba92..ecc7735 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -23,7 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ -/* VRULL GmbH, for contributions by Philipp Tomsich */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_termination_common.sail b/model/riscv_termination_common.sail index be0ee3e..fb8bdf0 100644 --- a/model/riscv_termination_common.sail +++ b/model/riscv_termination_common.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_termination_rv32.sail b/model/riscv_termination_rv32.sail index ad31925..f08162a 100644 --- a/model/riscv_termination_rv32.sail +++ b/model/riscv_termination_rv32.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_termination_rv64.sail b/model/riscv_termination_rv64.sail index 6b40f20..dcd09b4 100644 --- a/model/riscv_termination_rv64.sail +++ b/model/riscv_termination_rv64.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_types.sail b/model/riscv_types.sail index bfb176e..728c1d2 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -23,7 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ -/* VRULL GmbH, for contributions by Philipp Tomsich */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_types_common.sail b/model/riscv_types_common.sail index b624f12..6080f30 100644 --- a/model/riscv_types_common.sail +++ b/model/riscv_types_common.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_types_ext.sail b/model/riscv_types_ext.sail index 2ca3002..771ef6d 100644 --- a/model/riscv_types_ext.sail +++ b/model/riscv_types_ext.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_types_kext.sail b/model/riscv_types_kext.sail index 78a4754..e3019ec 100644 --- a/model/riscv_types_kext.sail +++ b/model/riscv_types_kext.sail @@ -1,3 +1,73 @@ +/*=======================================================================================*/ +/* RISCV Sail Model */ +/* */ +/* This Sail RISC-V architecture model, comprising all files and */ +/* directories except for the snapshots of the Lem and Sail libraries */ +/* in the prover_snapshots directory (which include copies of their */ +/* licences), is subject to the BSD two-clause licence below. */ +/* */ +/* Copyright (c) 2017-2023 */ +/* Prashanth Mundkur */ +/* Rishiyur S. Nikhil and Bluespec, Inc. */ +/* Jon French */ +/* Brian Campbell */ +/* Robert Norton-Wright */ +/* Alasdair Armstrong */ +/* Thomas Bauereiss */ +/* Shaked Flur */ +/* Christopher Pulte */ +/* Peter Sewell */ +/* Alexander Richardson */ +/* Hesham Almatary */ +/* Jessica Clarke */ +/* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ +/* Peter Rugg */ +/* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ +/* */ +/* All rights reserved. */ +/* */ +/* This software was developed by the above within the Rigorous */ +/* Engineering of Mainstream Systems (REMS) project, partly funded by */ +/* EPSRC grant EP/K008528/1, at the Universities of Cambridge and */ +/* Edinburgh. */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contract FA8650-18-C-7809 ("CIFV"), and */ +/* under DARPA contract HR0011-18-C-0016 ("ECATS") as part of the DARPA */ +/* SSITH research programme. */ +/* */ +/* This project has received funding from the European Research Council */ +/* (ERC) under the European Union’s Horizon 2020 research and innovation */ +/* programme (grant agreement 789108, ELVER). */ +/* */ +/* */ +/* Redistribution and use in source and binary forms, with or without */ +/* modification, are permitted provided that the following conditions */ +/* are met: */ +/* 1. Redistributions of source code must retain the above copyright */ +/* notice, this list of conditions and the following disclaimer. */ +/* 2. Redistributions in binary form must reproduce the above copyright */ +/* notice, this list of conditions and the following disclaimer in */ +/* the documentation and/or other materials provided with the */ +/* distribution. */ +/* */ +/* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' */ +/* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED */ +/* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A */ +/* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR */ +/* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, */ +/* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT */ +/* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF */ +/* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND */ +/* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, */ +/* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT */ +/* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF */ +/* SUCH DAMAGE. */ +/*=======================================================================================*/ + /* * This file contains types, mappings and functions used across the * cryptography extension instructions. diff --git a/model/riscv_vmem_common.sail b/model/riscv_vmem_common.sail index c77eb38..adf903f 100644 --- a/model/riscv_vmem_common.sail +++ b/model/riscv_vmem_common.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_vmem_rv32.sail b/model/riscv_vmem_rv32.sail index 4da87fd..ba29332 100644 --- a/model/riscv_vmem_rv32.sail +++ b/model/riscv_vmem_rv32.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_vmem_rv64.sail b/model/riscv_vmem_rv64.sail index 191427b..ecb705e 100644 --- a/model/riscv_vmem_rv64.sail +++ b/model/riscv_vmem_rv64.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_vmem_sv32.sail b/model/riscv_vmem_sv32.sail index d2e86e3..7531e9d 100644 --- a/model/riscv_vmem_sv32.sail +++ b/model/riscv_vmem_sv32.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_vmem_sv39.sail b/model/riscv_vmem_sv39.sail index a6c64e1..1c5a224 100644 --- a/model/riscv_vmem_sv39.sail +++ b/model/riscv_vmem_sv39.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_vmem_sv48.sail b/model/riscv_vmem_sv48.sail index 57ebf8c..1beea32 100644 --- a/model/riscv_vmem_sv48.sail +++ b/model/riscv_vmem_sv48.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_vmem_tlb.sail b/model/riscv_vmem_tlb.sail index 69b4958..39d696d 100644 --- a/model/riscv_vmem_tlb.sail +++ b/model/riscv_vmem_tlb.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_vmem_types.sail b/model/riscv_vmem_types.sail index 44aba0e..15cb95b 100644 --- a/model/riscv_vmem_types.sail +++ b/model/riscv_vmem_types.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_xlen32.sail b/model/riscv_xlen32.sail index c4f0034..eb0ae8a 100644 --- a/model/riscv_xlen32.sail +++ b/model/riscv_xlen32.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/riscv_xlen64.sail b/model/riscv_xlen64.sail index c980550..65c4696 100644 --- a/model/riscv_xlen64.sail +++ b/model/riscv_xlen64.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index 60e5f33..4e1941c 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -6,7 +6,7 @@ /* in the prover_snapshots directory (which include copies of their */ /* licences), is subject to the BSD two-clause licence below. */ /* */ -/* Copyright (c) 2017-2021 */ +/* Copyright (c) 2017-2023 */ /* Prashanth Mundkur */ /* Rishiyur S. Nikhil and Bluespec, Inc. */ /* Jon French */ @@ -23,6 +23,8 @@ /* Microsoft, for contributions by Robert Norton-Wright and Nathaniel Wesley Filardo */ /* Peter Rugg */ /* Aril Computer Corp., for contributions by Scott Johnson */ +/* Philipp Tomsich */ +/* VRULL GmbH, for contributions by its employees */ /* */ /* All rights reserved. */ /* */ |