From 9f9d1a731c090044c80120962522f3248dd01206 Mon Sep 17 00:00:00 2001 From: Charly Castes Date: Thu, 26 Dec 2024 12:00:50 +0100 Subject: [PATCH] Verify CSR read: add support for seed register The seed register can only be decoded with crypto extensions enabled. This commit makes them available during model checking to ensure we pass the CSR read tests. --- model_checking/src/lib.rs | 9 +-------- model_checking/src/symbolic.rs | 1 + 2 files changed, 2 insertions(+), 8 deletions(-) diff --git a/model_checking/src/lib.rs b/model_checking/src/lib.rs index 9831a547..ec317fc6 100644 --- a/model_checking/src/lib.rs +++ b/model_checking/src/lib.rs @@ -75,14 +75,7 @@ pub fn read_csr() { // Infinite number of pmps for the formal verification ctx.nb_pmp = usize::MAX; - let mut csr_register = generate_csr_register(); - - let is_seed = csr_register == 0b000000010101; - - // TODO: Adapt the last registers for the symbolic verification - if is_seed { - csr_register = 0; - } + let csr_register = generate_csr_register(); // Read value from Miralis let decoded_csr = mctx.decode_csr(csr_register as usize); diff --git a/model_checking/src/symbolic.rs b/model_checking/src/symbolic.rs index 32490a4b..98ef3dde 100644 --- a/model_checking/src/symbolic.rs +++ b/model_checking/src/symbolic.rs @@ -156,6 +156,7 @@ pub fn new_symbolic_contexts() -> (VirtContext, MiralisContext, SailVirtCtx) { // Initialize Miralis's own context let mut hw = unsafe { Arch::detect_hardware() }; hw.available_reg.nb_pmp = 64; // We assume 64 PMPs during model checking + hw.extensions.has_crypto_extension = true; // Needed for Seed register let mctx = MiralisContext::new(hw, Plat::get_miralis_start(), 0x1000); (ctx, mctx, sail_ctx)