Skip to content
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
6 changes: 6 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -101,9 +101,15 @@ For booting operating system images, see the information under the
- Zvbc extension for vector carryless multiplication, v1.0
- Zvkb extension for vector cryptography bit-manipulation, v1.0
- Zvkg extension for vector GCM/GMAC, v1.0
- Zvkn extension for vector crytography NIST Algorithm Suite
- Zvknc extension for vector crytography NIST Algorithm Suite with carryless multiply
- Zvkned extension for vector cryptography NIST Suite: Vector AES Block Cipher, v1.0
- Zvkng extension for vector crytography NIST Algorithm Suite with GCM
- Zvknha and Zvknhb extensions for vector cryptography NIST Suite: Vector SHA-2 Secure Hash, v1.0
- Zvks extension for vector crytography ShangMi Algorithm Suite
- Zvksc extension for vector crytography ShangMi Algorithm Suite with carryless multiplication
- Zvksed extension for vector cryptography ShangMi Suite: SM4 Block Cipher, v1.0
- Zvksg extension for vector crytography ShangMi Algorithm Suite with GCM
- Zvksh extension for vector cryptography ShangMi Suite: SM3 Secure Hash, v1.0
- Zvkt extension for vector data independent execution latency, v1.0 (no impact on model)
- Machine, Supervisor, and User modes
Expand Down
46 changes: 46 additions & 0 deletions model/riscv_extensions.sail
Original file line number Diff line number Diff line change
Expand Up @@ -287,6 +287,46 @@ enum clause extension = Ext_Zvkt
mapping clause extensionName = Ext_Zvkt <-> "zvkt"
function clause hartSupports(Ext_Zvkt) = config extensions.Zvkt.supported
function clause currentlyEnabled(Ext_Zvkt) = hartSupports(Ext_Zvkt)
// The following extensions are superset/shorthand extensions. They cannot be
// directly configured in the config file and are automatically supported when
// all their required subset extensions are supported.
enum clause extension = Ext_Zvkn
mapping clause extensionName = Ext_Zvkn <-> "zvkn"
function clause hartSupports(Ext_Zvkn) =
hartSupports(Ext_Zvkned) &
hartSupports(Ext_Zvknhb) &
hartSupports(Ext_Zvkb) &
hartSupports(Ext_Zvkt)
function clause currentlyEnabled(Ext_Zvkn) = hartSupports(Ext_Zvkn)
// NIST Algorithm Suite with carryless multiply
enum clause extension = Ext_Zvknc
mapping clause extensionName = Ext_Zvknc <-> "zvknc"
function clause hartSupports(Ext_Zvknc) = hartSupports(Ext_Zvkn) & hartSupports(Ext_Zvbc)
function clause currentlyEnabled(Ext_Zvknc) = hartSupports(Ext_Zvknc)
// NIST Algorithm Suite with GCM
enum clause extension = Ext_Zvkng
mapping clause extensionName = Ext_Zvkng <-> "zvkng"
function clause hartSupports(Ext_Zvkng) = hartSupports(Ext_Zvkn) & hartSupports(Ext_Zvkg)
function clause currentlyEnabled(Ext_Zvkng) = hartSupports(Ext_Zvkng)
// ShangMi Algorithm Suite
enum clause extension = Ext_Zvks
mapping clause extensionName = Ext_Zvks <-> "zvks"
function clause hartSupports(Ext_Zvks) =
hartSupports(Ext_Zvksed) &
hartSupports(Ext_Zvksh) &
hartSupports(Ext_Zvkb) &
hartSupports(Ext_Zvkt)
function clause currentlyEnabled(Ext_Zvks) = hartSupports(Ext_Zvks)
// ShangMi Algorithm Suite with carryless multiplication
enum clause extension = Ext_Zvksc
mapping clause extensionName = Ext_Zvksc <-> "zvksc"
function clause hartSupports(Ext_Zvksc) = hartSupports(Ext_Zvks) & hartSupports(Ext_Zvbc)
function clause currentlyEnabled(Ext_Zvksc) = hartSupports(Ext_Zvksc)
// ShangMi Algorithm Suite with GCM
enum clause extension = Ext_Zvksg
mapping clause extensionName = Ext_Zvksg <-> "zvksg"
function clause hartSupports(Ext_Zvksg) = hartSupports(Ext_Zvks) & hartSupports(Ext_Zvkg)
function clause currentlyEnabled(Ext_Zvksg) = hartSupports(Ext_Zvksg)

// Count Overflow and Mode-Based Filtering
enum clause extension = Ext_Sscofpmf
Expand Down Expand Up @@ -405,10 +445,16 @@ let extensions_ordered_for_isa_string = [
Ext_Zvbc,
Ext_Zvkb,
Ext_Zvkg,
Ext_Zvkn,
Ext_Zvknc,
Ext_Zvkned,
Ext_Zvkng,
Ext_Zvknha,
Ext_Zvknhb,
Ext_Zvks,
Ext_Zvksc,
Ext_Zvksed,
Ext_Zvksg,
Ext_Zvksh,
Ext_Zvkt,

Expand Down
8 changes: 7 additions & 1 deletion model/riscv_termination.sail
Original file line number Diff line number Diff line change
Expand Up @@ -91,8 +91,14 @@ termination_measure virtual_memory_supported(_) = 3

function hartSupports_measure(ext : extension) -> int =
match ext {
Ext_C => 2,
Ext_D => 1,
Ext_Zvkn => 1,
Ext_Zvks => 1,
Ext_C => 2,
Ext_Zvknc => 2,
Ext_Zvkng => 2,
Ext_Zvksc => 2,
Ext_Zvksg => 2,
_ => 0,
}

Expand Down
Loading