diff options
| -rw-r--r-- | doc/ReadingGuide.md | 5 | ||||
| -rw-r--r-- | model/CMakeLists.txt | 5 | ||||
| -rw-r--r-- | model/core/extensions.sail | 83 | ||||
| -rw-r--r-- | model/core/sys_regs.sail | 4 | ||||
| -rw-r--r-- | model/extensions/cfi/zicfilp_regs.sail | 4 | ||||
| -rw-r--r-- | model/postlude/step.sail | 10 | ||||
| -rw-r--r-- | model/riscv.sail_project | 13 | ||||
| -rw-r--r-- | model/sys/vmem.sail | 2 | ||||
| -rw-r--r-- | model/sys/vmem_utils.sail | 6 | ||||
| -rw-r--r-- | model/termination/termination.sail | 102 |
10 files changed, 108 insertions, 126 deletions
diff --git a/doc/ReadingGuide.md b/doc/ReadingGuide.md index 7c57870..aeff0b6 100644 --- a/doc/ReadingGuide.md +++ b/doc/ReadingGuide.md @@ -251,10 +251,7 @@ Vector (`V`) and cryptography (`Zk*`) extensions. ### Other modules -The `termination` module specifies -[functions](../model/termination/termination.sail) that are used to prove -loop termination for theorem prover backends of Sail. The -`unit_tests` module collects Sail unit tests for the specification. +The `unit_tests` module collects Sail unit tests for the specification. The `main` module provides a [`main()`](../model/main/main.sail) function that is used in other Sail backends. diff --git a/model/CMakeLists.txt b/model/CMakeLists.txt index 957ab3c..191e77f 100644 --- a/model/CMakeLists.txt +++ b/model/CMakeLists.txt @@ -35,8 +35,6 @@ execute_process( ${SAIL_BIN} ${project_file} --require-version ${SAIL_REQUIRED_VER} - # include termination.sail in the list of dependencies - --variable "TERMINATION_FILE = true" --all-modules --list-files OUTPUT_VARIABLE sail_list_files @@ -380,7 +378,6 @@ foreach (xlen IN ITEMS 32 64) --config ${config_file} # Input files. ${SAIL_MODULES} - --variable "TERMINATION_FILE = true" ${project_file} ) add_custom_command( @@ -448,7 +445,6 @@ foreach (xlen IN ITEMS 32 64) ${lean_sail_common} ${lean_sail_default} ${SAIL_MODULES} - --variable "TERMINATION_FILE = true" ${project_file} ) add_custom_command( @@ -467,7 +463,6 @@ foreach (xlen IN ITEMS 32 64) ${lean_sail_common} ${lean_sail_executable} ${SAIL_MODULES} - --variable "TERMINATION_FILE = true" ${project_file} ) diff --git a/model/core/extensions.sail b/model/core/extensions.sail index fe1de4a..48453b6 100644 --- a/model/core/extensions.sail +++ b/model/core/extensions.sail @@ -19,14 +19,31 @@ scattered mapping extensionName val hartSupports : extension -> bool scattered function hartSupports +function hartSupports_measure(ext : extension) -> int = + match ext { + Ext_D => 1, // > F + Ext_Sstvecd => 1, // > S + Ext_Ssu64xl => 1, // > S + Ext_Zvkn => 1, // > Zvkned + Ext_Zvks => 1, // > Zvksed + + Ext_C => 2, // > D + Ext_Zvknc => 2, // > Zvkn + Ext_Zvkng => 2, // > Zvkn + Ext_Zvksc => 2, // > Zvks + Ext_Zvksg => 2, // > Zvks + + _ => 0, + } + +termination_measure hartSupports(ext) = hartSupports_measure(ext) + // Function used to determine if an extension is currently enabled in the model. // This means an extension is supported, *and* any necessary bits are set in the // relevant CSRs (misa, mstatus, etc.) to enable its use. It is possible for some // extensions to be supported in hardware, but temporarily disabled via a CSR, in // which case this function should return false. -// Note: when adding a new extension, adjust the associated termination measure -// in the file termination.sail, as explained in the comment in -// that file. +// Note: when adding a new extension, adjust the `currentlyEnabled_measure` below. val currentlyEnabled : extension -> bool scattered function currentlyEnabled @@ -479,6 +496,66 @@ enum clause extension = Ext_Smcntrpmf mapping clause extensionName = Ext_Smcntrpmf <-> "smcntrpmf" function clause hartSupports(Ext_Smcntrpmf) = config extensions.Smcntrpmf.supported +// When adding a new extension X, we need to make sure that if X being enabled +// depends on Y being enabled, then the value associated to X is _greater_ than +// the value associated to Y. The default value is 2, so that if it does not +// depend on anything or only on extensions A, B, C, D, F, M, S, Zve32x, Zvl* or Zicsr, +// nothing needs to be done. + +function currentlyEnabled_measure(ext : extension) -> int = + match ext { + Ext_A => 0, + Ext_B => 0, + Ext_C => 0, + Ext_M => 0, + Ext_Zicsr => 0, + Ext_Zvl128b => 0, + Ext_Zvl32b => 0, + Ext_Zvl64b => 0, + + Ext_D => 1, // > Zicsr + Ext_F => 1, // > Zicsr + Ext_S => 1, // > Zicsr + Ext_Zaamo => 1, // > A + Ext_Zalrsc => 1, // > A + Ext_Zca => 1, // > C + Ext_Zfinx => 1, // > Zicsr + Ext_Zicntr => 1, // > Zicsr + Ext_Zihpm => 1, // > Zicsr + Ext_Zve32x => 1, // > Zvl32b + + // Note: even though these match the default case, making them explicit to + // annotate the chain of dependencies + Ext_Sv39 => 2, // > S + Ext_Zfh => 2, // > F + Ext_Zhinx => 2, // > Zfinx + Ext_Zvbb => 2, // > Zve32x + Ext_Zve32f => 2, // > Zve32x + Ext_Zve64x => 2, // > Zve32x + + Ext_Svrsw60t59b => 3, // > Sv39 + Ext_Zfhmin => 3, // > Zfh + Ext_Zhinxmin => 3, // > Zhinx + Ext_Zicfilp => 3, // > get_xLPE + Ext_Zvbc => 3, // > Zve64x + Ext_Zve64f => 3, // > Zve64x + Ext_Zvfbfmin => 3, // > Zve32f + Ext_Zvkb => 3, // > Zvbb + Ext_Zvknhb => 3, // > Zve64x + + Ext_H => 4, // > virtual_mem_supported + Ext_Zve64d => 4, // > Zve64f + Ext_Zvfbfwma => 4, // > Zvfbfmin + Ext_Zvfh => 4, // > Zfhmin + + Ext_V => 5, // > Zve64d + Ext_Zvfhmin => 5, // > Zvfh + + _ => 2 + } + +termination_measure currentlyEnabled(ext) = currentlyEnabled_measure(ext) + let extensions_ordered_for_isa_string = [ // Single letter extensions. Ext_M, diff --git a/model/core/sys_regs.sail b/model/core/sys_regs.sail index d21e370..a844ff2 100644 --- a/model/core/sys_regs.sail +++ b/model/core/sys_regs.sail @@ -146,6 +146,10 @@ function virtual_memory_supported() -> bool = { currentlyEnabled(Ext_Sv32) | currentlyEnabled(Ext_Sv39) | currentlyEnabled(Ext_Sv48) | currentlyEnabled(Ext_Sv57) } +// This measure needs to be > currentlyEnabled_measure(Ext_Sv{32,39,48,57}), +// currently all equal to 2, see currentlyEnabled_measure in extensions.sail +termination_measure virtual_memory_supported(_) = 3 + // // Illegal values legalized to least privileged mode supported. // Note: the only valid combinations of supported modes are M, M+U, M+S+U. diff --git a/model/extensions/cfi/zicfilp_regs.sail b/model/extensions/cfi/zicfilp_regs.sail index ee8d3cf..6d15680 100644 --- a/model/extensions/cfi/zicfilp_regs.sail +++ b/model/extensions/cfi/zicfilp_regs.sail @@ -32,6 +32,10 @@ function get_xLPE(p : Privilege) -> bool = VirtualUser => internal_error(__FILE__, __LINE__, "Hypervisor extension not supported"), } +// This measure needs to be > currentlyEnabled_measure(Ext_S), currently equal +// to 1, see currentlyEnabled_measure in extensions.sail +termination_measure get_xLPE(_) = 2 + function clause currentlyEnabled(Ext_Zicfilp) = currentlyEnabled(Ext_Zicsr) & hartSupports(Ext_Zicfilp) & get_xLPE(cur_privilege) diff --git a/model/postlude/step.sail b/model/postlude/step.sail index e8a800f..7bf3cc5 100644 --- a/model/postlude/step.sail +++ b/model/postlude/step.sail @@ -296,3 +296,13 @@ function loop () : unit -> unit = { } } } + +// Termination measures for loops are not supported by the Lean backend, so they +// should be guarded by this condition: +$iftarget coq + +// The top-level loop isn't terminating, but we put a limit so that it can still +// be included in the Coq output +termination_measure loop while 100 + +$endif diff --git a/model/riscv.sail_project b/model/riscv.sail_project index 1bdda62..c2a4bbd 100644 --- a/model/riscv.sail_project +++ b/model/riscv.sail_project @@ -1,4 +1,3 @@ -variable TERMINATION_FILE = false variable RMEM = false prelude { @@ -477,18 +476,8 @@ postlude { postlude/model.sail } -termination { - after postlude - requires prelude, core, sys, extensions - - files - if $TERMINATION_FILE then - termination/termination.sail - else [] -} - unit_tests { - after termination + after postlude requires prelude, core, sys, exceptions, postlude files diff --git a/model/sys/vmem.sail b/model/sys/vmem.sail index 875ba7a..45150c2 100644 --- a/model/sys/vmem.sail +++ b/model/sys/vmem.sail @@ -156,6 +156,8 @@ function pt_walk( } } +termination_measure pt_walk(_,_,_,_,_,_,_,level,_, _) = level + // **************************************************************** // Architectural SATP CSR diff --git a/model/sys/vmem_utils.sail b/model/sys/vmem_utils.sail index c07b661..1b6216c 100644 --- a/model/sys/vmem_utils.sail +++ b/model/sys/vmem_utils.sail @@ -172,6 +172,9 @@ function vmem_read_addr(vaddr, offset, width, acc, aq, rl, res) = { Ok(data) } +// This lets the Rocq extraction know why the repeat loop above terminates +termination_measure vmem_read_addr repeat n + val vmem_write_addr : forall 'width, is_mem_width('width). (virtaddr, int('width), bits(8 * 'width), MemoryAccessType(ext_access_type), bool, bool, bool) -> result(bool, ExecutionResult) @@ -227,6 +230,9 @@ function vmem_write_addr(vaddr, width, data, acc, aq, rl, res) = { Ok(write_success) } +// This lets the Rocq extraction know why the repeat loop above terminates +termination_measure vmem_write_addr repeat n + val vmem_read : forall 'width, is_mem_width('width). (regidx, xlenbits, int('width), MemoryAccessType(ext_access_type), bool, bool, bool) -> result(bits(8 * 'width), ExecutionResult) diff --git a/model/termination/termination.sail b/model/termination/termination.sail deleted file mode 100644 index 5964abd..0000000 --- a/model/termination/termination.sail +++ /dev/null @@ -1,102 +0,0 @@ -// ======================================================================================= -// This Sail RISC-V architecture model, comprising all files and -// directories except where otherwise noted is subject the BSD -// two-clause license in the LICENSE file. -// -// SPDX-License-Identifier: BSD-2-Clause -// ======================================================================================= - -termination_measure pt_walk(_,_,_,_,_,_,_,level,_, _) = level - -// When adding a new extension X, we need to make sure that if X being enabled -// depends on Y being enabled, then the value associated to X is _greater_ than -// the value associated to Y. The default value is 2, so that if it does not -// depend on anything or only on extensions A, B, C, D, F, M, S, Zve32x, Zvl* or Zicsr, -// nothing needs to be done. -function currentlyEnabled_measure(ext : extension) -> int = - match ext { - Ext_Zicsr => 0, - Ext_A => 1, - Ext_B => 1, - Ext_C => 1, - Ext_D => 1, - Ext_F => 1, - Ext_M => 1, - Ext_S => 1, - Ext_V => 5, - Ext_H => 4, - Ext_Smcntrpmf => 3, - Ext_Zabha => 3, - Ext_Zacas => 3, - Ext_Za64rs => 3, - Ext_Za128rs => 3, - Ext_Zcb => 3, - Ext_Zcd => 3, - Ext_Zcf => 3, - Ext_Zcmop => 3, - Ext_Zfhmin => 3, - Ext_Zhinx => 3, - Ext_Zicfilp => 3, - Ext_Zvl32b => 0, - Ext_Zvl64b => 0, - Ext_Zvl128b => 0, - Ext_Zvl256b => 0, - Ext_Zvl512b => 0, - Ext_Zvl1024b => 0, - Ext_Zve32x => 1, - Ext_Zvfbfmin => 3, - Ext_Zvfbfwma => 4, - Ext_Zve64f => 3, - Ext_Zve64d => 4, - Ext_Zvfh => 4, - Ext_Zvfhmin => 5, - Ext_Zvbb => 6, - Ext_Zvbc => 6, - Ext_Zvkb => 7, - Ext_Zvkg => 6, - Ext_Zvkned => 6, - Ext_Zvknha => 6, - Ext_Zvknhb => 6, - Ext_Zvksed => 6, - Ext_Zvksh => 6, - Ext_Sscofpmf => 3, - Ext_Svrsw60t59b => 3, - Ext_Zhinxmin => 4, - _ => 2 - } - -termination_measure currentlyEnabled(ext) = currentlyEnabled_measure(ext) -termination_measure virtual_memory_supported(_) = 3 - -// get_xLPE() and currentlyEnabled() are mutually recursive -termination_measure get_xLPE(_) = 2 - -function hartSupports_measure(ext : extension) -> int = - match ext { - Ext_D => 1, - Ext_V => 1, - Ext_Zvkn => 1, - Ext_Zvks => 1, - Ext_C => 2, - Ext_Zvknc => 2, - Ext_Zvkng => 2, - Ext_Zvksc => 2, - Ext_Zvksg => 2, - Ext_Sstvecd => 1, - Ext_Ssu64xl => 1, - _ => 0, - } - -termination_measure hartSupports(ext) = hartSupports_measure(ext) - -// Termination measures for loops are not supported by the Lean backend, so they -// should be guarded by this condition: -$iftarget coq - -termination_measure vmem_write_addr repeat n -termination_measure vmem_read_addr repeat n - -// The top-level loop isn't terminating, but we put a limit so that it can still be included in the Coq output -termination_measure loop while 100 - -$endif |