Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ISA DVPLAN for embedded config #1618

Merged
merged 1 commit into from
Nov 12, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 35 additions & 5 deletions verif/docs/VerifPlans/ISA_RV32/RISCV_Instructions.rst
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
..
..
Copyright (c) 2023 OpenHW Group
Copyright (c) 2023 Thales DIS design services SAS

Expand Down Expand Up @@ -31,6 +31,7 @@ In this document, we present ISA (Instruction Set Architecture) for C32VA6_v5.0.
* RV32C – Standard Extension for Compressed Instructions
* RV32Zicsr – Standard Extension for CSR Instructions
* RV32Zifencei – Standard Extension for Instruction-Fetch Fence
* RV32Zicond – Standard Extension for Integer Conditional Operations

The base RISC-V ISA has fixed-length 32-bit instructions or 16-bit instructions (the C32VA6_v5.0.0 support C extension), so that must be naturally aligned on 4-byte boundary or 2-byte boundary.
The C32VA6_v5.0.0 supports:
Expand Down Expand Up @@ -451,7 +452,7 @@ Control Transfer Instructions
**Format**: beq rs1, rs2, imm[12:1]

**Description**: takes the branch (pc is calculated using signed arithmetic) if registers rs1 and rs2 are equal.

**Pseudocode**: if (x[rs1] == x[rs2]) pc += sext({imm[12:1], 1’b0}) else pc += 4

**Invalid values**: NONE
Expand All @@ -465,7 +466,7 @@ Control Transfer Instructions
**Description**: takes the branch (pc is calculated using signed arithmetic) if registers rs1 and rs2 are not equal.

**Pseudocode**: if (x[rs1] != x[rs2]) pc += sext({imm[12:1], 1’b0}) else pc += 4

**Invalid values**: NONE

**Exception raised**: no instruction fetch misaligned exception is generated for a conditional branch that is not taken. An Instruction address misaligned exception is raised if the target address is not aligned on 4-byte or 2-byte boundary, because the core supports compressed instructions.
Expand All @@ -479,7 +480,7 @@ Control Transfer Instructions
**Pseudocode**: if (x[rs1] < x[rs2]) pc += sext({imm[12:1], 1’b0}) else pc += 4

**Invalid values**: NONE

**Exception raised**: no instruction fetch misaligned exception is generated for a conditional branch that is not taken. An Instruction address misaligned exception is raised if the target address is not aligned on 4-byte or 2-byte boundary, because the core supports compressed instructions.

- **BLTU**: Branch Less Than Unsigned
Expand Down Expand Up @@ -513,7 +514,7 @@ Control Transfer Instructions
**Description**: takes the branch (pc is calculated using signed arithmetic) if registers rs1 is greater than or equal rs2 (using unsigned comparison).

**Pseudocode**: if (x[rs1] >=u x[rs2]) pc += sext({imm[12:1], 1’b0}) else pc += 4

**Invalid values**: NONE

**Exception raised**: no instruction fetch misaligned exception is generated for a conditional branch that is not taken. An Instruction address misaligned exception is raised if the target address is not aligned on 4-byte or 2-byte boundary, because the core supports compressed instructions.
Expand Down Expand Up @@ -1343,6 +1344,35 @@ RV32Zifencei Instruction-Fetch Fence

**Exception raised**: NONE

RV32Zicond Integer Conditional operations
-------------------------------------------

The instructions follow the format for R-type instructions with 3 operands (i.e., 2 source operands and 1 destination operand). Using these instructions, branchless sequences can be implemented (typically in two-instruction sequences) without the need for instruction fusion, special provisions during the decoding of architectural instructions, or other microarchitectural provisions.

- **CZERO.EQZ**: Conditional zero, if condition is equal to zero

**Format**: czero.eqz rd, rs1, rs2

**Description**: This instruction behaves as if there is a conditional branch dependent on rs2 being equal to zero, wherein it branches to code that writes a 0 into rd when the equivalence is true, and otherwise falls through to code that moves rs1 into rd.

**Pseudocode**: if (x[rs2] == 0) x[rd] = 0 else x[rs1]

**Invalid values**: NONE

**Exception raised**: NONE

- **CZERO.NEZ**: Conditional zero, if condition is nonzero

**Format**: czero.nez rd, rs1, rs2

**Description**: This instruction behaves as if there is a conditional branch dependent on rs2 being not equal to zero, wherein it branches to code that writes a 0 into rd when the equivalence is true, and otherwise falls through to code that moves rs1 into rd

**Pseudocode**: if (x[rs2] != 0) x[rd] = 0 else x[rs1]

**Invalid values**: NONE

**Exception raised**: NONE

Illegal Instruction
---------------------------

Expand Down
142 changes: 142 additions & 0 deletions verif/docs/VerifPlans/ISA_RV32/VP_IP016.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,142 @@
!Feature
next_elt_id: 2
name: RV32Zicond Integer Conditional Instructions
id: 16
display_order: 16
subfeatures: !!omap
- 000_CZERO.EQZ: !Subfeature
name: 000_CZERO.EQZ
tag: VP_ISA_RV32_F016_S000
next_elt_id: 3
display_order: 0
items: !!omap
- '000': !VerifItem
name: '000'
tag: VP_ISA_RV32_F016_S000_I000
description: "czero.eqz rd, rs1, rs2\nif (x[rs2] == 0) x[rd] = 0 else x[rs1]\n
Set rd's value to zero if rs2 is equal to zero, otherwise moves rs1 into
rd"
reqt_doc: ./RISCV_Instructions.rst
ref_mode: page
ref_page: ''
ref_section: ''
ref_viewer: firefox
verif_goals: "Register operands:\n\nAll possible rd registers are used\nAll
possible rs1 registers are used\nAll possible rs2 registers are used\nAll
possible register combinations where rs1 == rd are used\nAll possible register
combinations where rs2 == rd are used"
pfc: 3
test_type: 3
cov_method: 1
cores: 56
coverage_loc: ''
comments: ''
- '001': !VerifItem
name: '001'
tag: VP_ISA_RV32_F016_S000_I001
description: "czero.eqz rd, rs1, rs2\nif (x[rs2] == 0) x[rd] = 0 else x[rs1]\n
Set rd's value to zero if rs2 is equal to zero, otherwise moves rs1 into
rd"
reqt_doc: ./RISCV_Instructions.rst
ref_mode: page
ref_page: ''
ref_section: ''
ref_viewer: firefox
verif_goals: "Input operands:\n\nrs1 value is +ve, -ve and zero\nrs2 value
is +ve, -ve and zero\nAll combinations of rs1 and rs2 +ve, -ve, and zero
values are used\nAll bits of rs1 are toggled\nAll bits of rs2 are toggled"
pfc: -1
test_type: -1
cov_method: -1
cores: 56
coverage_loc: ''
comments: ''
- '002': !VerifItem
name: '002'
tag: VP_ISA_RV32_F016_S000_I002
description: "czero.eqz rd, rs1, rs2\nif (x[rs2] == 0) x[rd] = 0 else x[rs1]\n
Set rd's value to zero if rs2 is equal to zero, otherwise moves rs1 into
rd"
reqt_doc: ./RISCV_Instructions.rst
ref_mode: page
ref_page: ''
ref_section: ''
ref_viewer: firefox
verif_goals: "Output result:\n\nrd value is +ve, -ve and zero\nAll bits of
rd are toggled"
pfc: -1
test_type: -1
cov_method: -1
cores: 56
coverage_loc: ''
comments: ''
- 001_CZERO.NEZ: !Subfeature
name: 001_CZERO.NEZ
tag: VP_ISA_RV32_F016_S001
next_elt_id: 3
display_order: 1
items: !!omap
- '000': !VerifItem
name: '000'
tag: VP_ISA_RV32_F016_S001_I000
description: "czero.nez rd, rs1, rs2\nif (x[rs2] != 0) x[rd] = 0 else x[rs1]\n
Set rd's value to zero if rs2 isn't equal to zero, otherwise moves rs1 into
rd"
reqt_doc: ./RISCV_Instructions.rst
ref_mode: page
ref_page: ''
ref_section: ''
ref_viewer: firefox
verif_goals: "Register operands:\n\nAll possible rd registers are used\nAll
possible rs1 registers are used\nAll possible rs2 registers are used\nAll
possible register combinations where rs1 == rd are used\nAll possible register
combinations where rs2 == rd are used"
pfc: 3
test_type: 3
cov_method: 1
cores: 56
coverage_loc: ''
comments: ''
- '001': !VerifItem
name: '001'
tag: VP_ISA_RV32_F016_S001_I001
description: "czero.nez rd, rs1, rs2\nif (x[rs2] != 0) x[rd] = 0 else x[rs1]\n
Set rd's value to zero if rs2 isn't equal to zero, otherwise moves rs1 into
rd"
reqt_doc: ./RISCV_Instructions.rst
ref_mode: page
ref_page: ''
ref_section: ''
ref_viewer: firefox
verif_goals: "Input operands:\n\nrs1 value is +ve, -ve and zero\nrs2 value
is +ve, -ve and zero\nAll combinations of rs1 and rs2 +ve, -ve, and zero
values are used\nAll bits of rs1 are toggled\nAll bits of rs2 are toggled"
pfc: -1
test_type: -1
cov_method: -1
cores: 56
coverage_loc: ''
comments: ''
- '002': !VerifItem
name: '002'
tag: VP_ISA_RV32_F016_S001_I002
description: "czero.nez rd, rs1, rs2\nif (x[rs2] != 0) x[rd] = 0 else x[rs1]\n
Set rd's value to zero if rs2 isn't equal to zero, otherwise moves rs1 into
rd"
reqt_doc: ./RISCV_Instructions.rst
ref_mode: page
ref_page: ''
ref_section: ''
ref_viewer: firefox
verif_goals: "Output result:\n\nrd value is +ve, -ve and zero\nAll bits of
rd are toggled"
pfc: -1
test_type: -1
cov_method: -1
cores: 56
coverage_loc: ''
comments: ''
vptool_gitrev: '$Id: b0efb3ae3f9057b71a577d43c2b77f1cfb2ef82f $'
io_fmt_gitrev: '$Id: 7ee5d68801f5498a957bcbe23fcad87817a364c5 $'
config_gitrev: '$Id: 0422e19126dae20ffc4d5a84e4ce3de0b6eb4eb5 $'
ymlcfg_gitrev: '$Id: 286c689bd48b7a58f9a37754267895cffef1270c $'
Loading
Loading