Skip to content

Commit

Permalink
ISA DV plan (#1618)
Browse files Browse the repository at this point in the history
  • Loading branch information
AyoubJalali authored Nov 12, 2023
1 parent 7872d01 commit 39d26fb
Show file tree
Hide file tree
Showing 6 changed files with 1,642 additions and 135 deletions.
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

0 comments on commit 39d26fb

Please sign in to comment.