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.

Author: CharlyCst

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);

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)