Skip to content

Commit

Permalink
Merge pull request #13 from fennecJ/Update_Readme
Browse files Browse the repository at this point in the history 
Update Readme.md
  • Loading branch information
@fennecJ
fennecJ authored Dec 28, 2024
2 parents 3dc048b + 7b38fc1 commit 49d9023
Show file tree
Hide file tree
Showing 16 changed files with 960 additions and 61 deletions.
74 changes: 74 additions & 0 deletions Contribute.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
## Contribution Guide

This repository uses [Verible](https://github.com/chipsalliance/verible) as a linter and formatter to maintain code quality.

### Getting Started

To contribute, you will need to install Verible. The recommended approach is to install the pre-built binary:

1. Navigate to the directory where you want to install Verible:
```bash
cd "$DIR_YOU_WANT_INSTALL_VERIBLE"
```

2. Download the pre-built binary:
```bash
wget https://github.com/chipsalliance/verible/releases/download/v0.0-3824-g14eed6a0/verible-v0.0-3824-g14eed6a0-linux-static-x86_64.tar.gz
```

3. Extract the downloaded file:
```bash
tar -zxvf verible-v0.0-3824-g14eed6a0-linux-static-x86_64.tar.gz
```

4. Add Verible to your `PATH` by updating your `~/.bashrc` file:
```bash
export PATH=$DIR_YOU_WANT_INSTALL_VERIBLE/verible-v0.0-3824-g14eed6a0/bin:$PATH
```

### Setting up Pre-commit Hooks

This project also uses `pre-commit` to enforce code standards. Follow these steps to set it up:

1. Install `pre-commit` using pip:
```bash
pip install pre-commit
```

2. Clone the repository and navigate to the project directory:
```bash
git clone https://github.com/fennecJ/formal_RV12
cd formal_RV12
```

3. Install the pre-commit hooks:
```bash
pre-commit install
```

### Formatting and Linting Before Committing

Before committing your changes, ensure your code is properly formatted and free of linting issues by running the following commands:

1. To format the source code, run:
```bash
verible-verilog-format --flagfile=.verible-format-flags --inplace property/isa.sv
```

2. To check for linting issues, run:
```bash
verible-verilog-lint --rules_config=.verible.rules property/isa.sv
# There should be no output if no linting issues are found.
```

Once these steps are complete and there are no issues, you're ready to contribute!

### Disabling Format for Specific Code Blocks

If you prefer to retain your custom code style in certain sections, you can instruct the formatter to ignore specific code blocks by using the following annotations:

```verilog
// verilog_format: off
// Your custom code here...
// verilog_format: on
```
83 changes: 83 additions & 0 deletions RV12/ROA_LOGIC_LICENSE.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
---
title: Non-Commercial License Agreement
---
# Non-Commercial License Agreement

PLEASE CAREFULLY REVIEW THE FOLLOWING TERMS AND CONDITIONS BEFORE DOWNLOADING AND USING THE LICENSED MATERIALS. THIS LICENSE AGREEMENT (“AGREEMENT”) IS A LEGAL AGREEMENT BETWEEN YOU (EITHER A SINGLE INDIVIDUAL, OR A SINGLE LEGAL ENTITY)(“YOU”) AND ROA LOGIC BV (“ROA LOGIC”) COVERING THE PRODUCTS OR SERVICES YOU PURCHASE FROM ROA LOGIC.

By downloading and/or using or installing products from Roa Logic you automatically agree to and are bound by the terms and conditions of this agreement.

PLEASE NOTE THAT THIS AGREEMENT IS INTENDED FOR NON-COMMERCIAL USE OF THE PRODUCT. IF YOU INTENT TO USE ROA LOGIC PRODUCTS FOR COMMERCIAL PURPOSES, THEN PLEASE CONTACT [email protected] TO ARRANGE AN AGREEMENT WITH US BASED ON OUR COMMERCIAL LICENSE TERMS

## 1. DEFINITIONS

“Intellectual Property” means any or all of the following and all rights in, arising out of, or associated with:


1. all inventions (whether patentable or not), invention disclosures, improvements, trade secrets, proprietary information, know how, technology, algorithms, techniques, methods, devices, technical data, customer lists, and all documentation embodying or evidencing any of the foregoing;
2. all computer software, source codes, object codes, firmware, development tools, files, records, data, and all media on which any of the foregoing is recorded

“Product” means an Intellectual Property block consisting of, but not limited to, Verilog, VHDL, and/or SystemVerilog design files, specifications, block diagrams and documentation.

“Physical Implementation” means any implementation in programmable or non-programmable technologies including, but not limited to Field Programmable Gate Arrays (FPGAs), Complex Programmable Logic Devices (CPLDs), Application Specific Integrated Circuits (ASICs), Application Specific Standard Products (ASSPs)

“Silicon Device(s)” means any customer Physical Implementation containing a unique part number.

“You” the opposite contract party as referred to in article 6:231, subsection c, of the Dutch Civil Code, being the party to whom an offer is made by Roa Logic, or with whom an agreement is concluded by Roa Logic, or to whom the Product is supplied.

## 2. LICENSE TO USE

Roa Logic hereby grants you the following limited, non-exclusive, non-transferable, no-charge, and royalty-free licenses to use, modify, and distribute the Product provided you do so for non-commercial (personal, educational, research and development, demonstration) purposes:

1. Copyright license
2. Patent license, where such license only applies to those patent claims licensable by Roa Logic.

Specifically you are allowed to:

1. Use the Product in your design to create, simulate, implement, manufacture, and use a Silicon Device provided you don’t do so to make a profit
2. Distribute the Product, provided the original disclaimer and copyright notice are retained and this Agreement is part of the distribution.

Specifically you are allowed to:

1. Use the Product in your design to create, simulate, implement, manufacture, and use a Silicon Device provided you don’t do so to make a profit
2. Distribute the Product, provided the original disclaimer and copyright notice are retained and this Agreement is part of the distribution.

## 3. OWNERSHIP

The Product, its documentation, and any associated material is owned by Roa Logic and is protected by copyright and other intellectual property right laws.

Any modification or addition to the Product, documentation, and any associated materials or derivatives thereof, that You intentionally submit to Roa Logic for inclusion in the Product will become part of the Product and thus owned and copyrighted by Roa Logic.

By submitting any material for inclusion you wave any ownership, copyright, and patent rights and claims for the use of the submitted material in the Product. “Submitting” means any form of electronic, verbal, or written communication sent to Roa Logic or its representatives, including, but not limited to, email, mailing lists, source repositories, and issue tracking systems for the purpose of discussing and improving the Product.

You shall not remove any copyright, disclaimers, or other notices from any parts of the Product.

## 4. RIGHT OF EQUITABLE RELIEF

You acknowledge and agree that violation of this agreement may cause Roa Logic irreparable injury for which an adequate remedy at law may not be available. Therefore Roa Logic shall be entitled to seek all remedies that may be available under equity, including immediate injunctive relief, in addition to whatever remedies may be available at law.

## 5. DISCLAIMER OF WARRANTY

The Product is provided “AS IS”. Roa Logic has no obligation to provide maintenance or support services in connection with the Product.

ROA LOGIC DISCLAIMS ALL WARRANTIES, CONDITIONS AND REPRESENTATIONS, EXPRESS, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT LIMITED TO, THOSE RELATED TO MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, SATISFACTORY QUALITY, ACCURACY OR COMPLETENESS OR RESULTS, CONFORMANCE WITH DESCRIPTION, AND NON-INFRINGEMENT.

## 6. LIMITATION OF LIABILITY

TO THE MAXIMUM EXTENT PERMITTED BY LAW, IN NO EVENT SHALL ROA LOGIC BE LIABLE TO YOU OR ANY THIRD PARTY FOR ANY INDIRECT, SPECIAL, CONSEQUENTIAL OR INCIDENTAL DAMAGES WHATSOEVER (INCLUDING, BUT NOT LIMITED TO, DAMAGES FOR LOSS OF PROFIT, BUSINESS INTERRUPTIONS OR LOSS OF INFORMATION) ARISING OUT OF THE USE OR INABILITY TO USE THE PRODUCT WHETHER BASED ON A CLAIM UNDER CONTRACT, TORT OR OTHER LEGAL THEORY, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGES.

## 7. EXPORT RESTRICTIONS

The Product may be subject to U.S. or E.U. export laws and may be subject to export or import regulations in other countries. You agree to comply fully with all laws and regulations of the United States, European Union, and other countries to ensure that the product is not:


1. exported directly, or indirectly, in violation of export laws;
2. intended to be used for any purposes prohibited by export laws, including, but not limited to, nuclear, chemical, or biological weapons proliferation.

## 8. APPLICABLE LAW AND CHOICE OF FORUM

All agreements and contracts between you and Roa Logic, which these conditions are applicable to, shall be governed by Dutch law with the exclusion of the uniform UN Convention on Contracts for the International Sale of Goods (CISG) and other bilateral or multilateral treaties for the purpose of unifying international sales.

The competent courts in the district where Roa Logic has its registered office in the Netherlands has jurisdiction over all disputes concerning rights and obligations associated with the contractual relations.

Conversion: If any clause or sentence of this agreement is held by a court of law to be illegal or unenforceable, the remaining provisions of the agreement remain in effect. The failure of Roa Logic to enforce any of the provisions in the agreement does not constitute a waiver of Roa Logic’s rights to enforce any provision of the agreement in the future.
81 changes: 20 additions & 61 deletions Readme.md
View file
Original file line number Diff line number Diff line change
@@ -1,74 +1,33 @@
## Contribution Guide

This repository uses [Verible](https://github.com/chipsalliance/verible) as a linter and formatter to maintain code quality.

### Getting Started

To contribute, you will need to install Verible. The recommended approach is to install the pre-built binary:

1. Navigate to the directory where you want to install Verible:
```bash
cd "$DIR_YOU_WANT_INSTALL_VERIBLE"
```
# An SVA(system verilog assertion) based formal verification example on RV12 with a subset of RV32I ISA

2. Download the pre-built binary:
```bash
wget https://github.com/chipsalliance/verible/releases/download/v0.0-3824-g14eed6a0/verible-v0.0-3824-g14eed6a0-linux-static-x86_64.tar.gz
```
This project implements an end-to-end verification[^1] approach for a CPU based on the RV32I ISA specification.

3. Extract the downloaded file:
```bash
tar -zxvf verible-v0.0-3824-g14eed6a0-linux-static-x86_64.tar.gz
```
The CPU under test is a modified version of an older commit from the [RV12](https://github.com/RoaLogic/RV12) repository, included here under Roa Logic's Non-Commercial License Agreement for educational and research purposes.

4. Add Verible to your `PATH` by updating your `~/.bashrc` file:
```bash
export PATH=$DIR_YOU_WANT_INSTALL_VERIBLE/verible-v0.0-3824-g14eed6a0/bin:$PATH
```
Verification focuses on a subset of RV32I instructions: `XORI`, `BLT`, `JAL`, `LB`, and `AUIPC`, representing the five main
instruction types (`I`, `B`, `J`, `L`, and `U`). Other instructions within the same type can likely be handled by referencing these examples.

### Setting up Pre-commit Hooks
**Running Formal Verification with JasperGold**

This project also uses `pre-commit` to enforce code standards. Follow these steps to set it up:
To perform formal verification with SystemVerilog Assertions, we use Cadence's JasperGold Formal Engine to execute our test suite, with TCL script `isa.tcl`.

1. Install `pre-commit` using pip:
```bash
pip install pre-commit
```
## Detailed of implementation and result
The implementation can be find in directory `property`.
Details of our design considerations and implementation thoughts are discussed in [Report.md](./Report.md).

2. Clone the repository and navigate to the project directory:
```bash
git clone https://github.com/fennecJ/formal_RV12
cd formal_RV12
```

3. Install the pre-commit hooks:
```bash
pre-commit install
```

### Formatting and Linting Before Committing

Before committing your changes, ensure your code is properly formatted and free of linting issues by running the following commands:
## Contribution Guide
Refer to [Contribute.md](./Contribute.md) if you want to contribute to this repo

1. To format the source code, run:
```bash
verible-verilog-format --flagfile=.verible-format-flags --inplace property/isa.sv
```
## License

2. To check for linting issues, run:
```bash
verible-verilog-lint --rules_config=.verible.rules property/isa.sv
# There should be no output if no linting issues are found.
```
This repository contains code under multiple licenses:

Once these steps are complete and there are no issues, you're ready to contribute!
1. **Roa Logic Code**
Portions of this repository include code sourced from Roa Logic, which is distributed under their Non-Commercial License Agreement. These parts are strictly for non-commercial purposes. See [`ROA_LOGIC_LICENSE.md`](./RV12/ROA_LOGIC_LICENSE.md) for details.

### Disabling Format for Specific Code Blocks
2. **MIT License**
All other parts of the code are licensed under the MIT License. See [`MIT_LICENSE.md`](./property/MIT_LICENSE.md) for details.

If you prefer to retain your custom code style in certain sections, you can instruct the formatter to ignore specific code blocks by using the following annotations:
If you intend to use this repository, please ensure compliance with the respective licenses.

```verilog
// verilog_format: off
// Your custom code here...
// verilog_format: on
```
[^1]: [End-to-End Verification of ARM Processors with ISA-Formal](https://alastairreid.github.io/papers/cav2016_isa_formal.pdf)
Loading

0 comments on commit 49d9023

Please sign in to comment.