diff --git a/model/riscv_csr_map.sail b/model/riscv_csr_map.sail index 31872d3f1..701d9274d 100644 --- a/model/riscv_csr_map.sail +++ b/model/riscv_csr_map.sail @@ -136,6 +136,22 @@ mapping clause csr_name_map = 0x3A0 <-> "pmpcfg0" mapping clause csr_name_map = 0x3A1 <-> "pmpcfg1" mapping clause csr_name_map = 0x3A2 <-> "pmpcfg2" mapping clause csr_name_map = 0x3A3 <-> "pmpcfg3" +mapping clause csr_name_map = 0x3A0 <-> "pmpcfg0" +mapping clause csr_name_map = 0x3A1 <-> "pmpcfg1" +mapping clause csr_name_map = 0x3A2 <-> "pmpcfg2" +mapping clause csr_name_map = 0x3A3 <-> "pmpcfg3" +mapping clause csr_name_map = 0x3A4 <-> "pmpcfg4" +mapping clause csr_name_map = 0x3A5 <-> "pmpcfg5" +mapping clause csr_name_map = 0x3A6 <-> "pmpcfg6" +mapping clause csr_name_map = 0x3A7 <-> "pmpcfg7" +mapping clause csr_name_map = 0x3A8 <-> "pmpcfg8" +mapping clause csr_name_map = 0x3A9 <-> "pmpcfg9" +mapping clause csr_name_map = 0x3AA <-> "pmpcfg10" +mapping clause csr_name_map = 0x3AB <-> "pmpcfg11" +mapping clause csr_name_map = 0x3AC <-> "pmpcfg12" +mapping clause csr_name_map = 0x3AD <-> "pmpcfg13" +mapping clause csr_name_map = 0x3AE <-> "pmpcfg14" +mapping clause csr_name_map = 0x3AF <-> "pmpcfg15" mapping clause csr_name_map = 0x3B0 <-> "pmpaddr0" mapping clause csr_name_map = 0x3B1 <-> "pmpaddr1" mapping clause csr_name_map = 0x3B2 <-> "pmpaddr2" @@ -152,6 +168,55 @@ mapping clause csr_name_map = 0x3BC <-> "pmpaddr12" mapping clause csr_name_map = 0x3BD <-> "pmpaddr13" mapping clause csr_name_map = 0x3BE <-> "pmpaddr14" mapping clause csr_name_map = 0x3BF <-> "pmpaddr15" +mapping clause csr_name_map = 0x3C0 <-> "pmpaddr16" +mapping clause csr_name_map = 0x3C1 <-> "pmpaddr17" +mapping clause csr_name_map = 0x3C2 <-> "pmpaddr18" +mapping clause csr_name_map = 0x3C3 <-> "pmpaddr19" +mapping clause csr_name_map = 0x3C4 <-> "pmpaddr20" +mapping clause csr_name_map = 0x3C5 <-> "pmpaddr21" +mapping clause csr_name_map = 0x3C6 <-> "pmpaddr22" +mapping clause csr_name_map = 0x3C7 <-> "pmpaddr23" +mapping clause csr_name_map = 0x3C8 <-> "pmpaddr24" +mapping clause csr_name_map = 0x3C9 <-> "pmpaddr25" +mapping clause csr_name_map = 0x3CA <-> "pmpaddr26" +mapping clause csr_name_map = 0x3CB <-> "pmpaddr27" +mapping clause csr_name_map = 0x3CC <-> "pmpaddr28" +mapping clause csr_name_map = 0x3CD <-> "pmpaddr29" +mapping clause csr_name_map = 0x3CE <-> "pmpaddr30" +mapping clause csr_name_map = 0x3CF <-> "pmpaddr31" +mapping clause csr_name_map = 0x3D0 <-> "pmpaddr32" +mapping clause csr_name_map = 0x3D1 <-> "pmpaddr33" +mapping clause csr_name_map = 0x3D2 <-> "pmpaddr34" +mapping clause csr_name_map = 0x3D3 <-> "pmpaddr35" +mapping clause csr_name_map = 0x3D4 <-> "pmpaddr36" +mapping clause csr_name_map = 0x3D5 <-> "pmpaddr37" +mapping clause csr_name_map = 0x3D6 <-> "pmpaddr38" +mapping clause csr_name_map = 0x3D7 <-> "pmpaddr39" +mapping clause csr_name_map = 0x3D8 <-> "pmpaddr40" +mapping clause csr_name_map = 0x3D9 <-> "pmpaddr41" +mapping clause csr_name_map = 0x3DA <-> "pmpaddr42" +mapping clause csr_name_map = 0x3DB <-> "pmpaddr43" +mapping clause csr_name_map = 0x3DC <-> "pmpaddr44" +mapping clause csr_name_map = 0x3DD <-> "pmpaddr45" +mapping clause csr_name_map = 0x3DE <-> "pmpaddr46" +mapping clause csr_name_map = 0x3DF <-> "pmpaddr47" +mapping clause csr_name_map = 0x3E0 <-> "pmpaddr48" +mapping clause csr_name_map = 0x3E1 <-> "pmpaddr49" +mapping clause csr_name_map = 0x3E2 <-> "pmpaddr50" +mapping clause csr_name_map = 0x3E3 <-> "pmpaddr51" +mapping clause csr_name_map = 0x3E4 <-> "pmpaddr52" +mapping clause csr_name_map = 0x3E5 <-> "pmpaddr53" +mapping clause csr_name_map = 0x3E6 <-> "pmpaddr54" +mapping clause csr_name_map = 0x3E7 <-> "pmpaddr55" +mapping clause csr_name_map = 0x3E8 <-> "pmpaddr56" +mapping clause csr_name_map = 0x3E9 <-> "pmpaddr57" +mapping clause csr_name_map = 0x3EA <-> "pmpaddr58" +mapping clause csr_name_map = 0x3EB <-> "pmpaddr59" +mapping clause csr_name_map = 0x3EC <-> "pmpaddr60" +mapping clause csr_name_map = 0x3ED <-> "pmpaddr61" +mapping clause csr_name_map = 0x3EE <-> "pmpaddr62" +mapping clause csr_name_map = 0x3EF <-> "pmpaddr63" + /* machine counters/timers */ mapping clause csr_name_map = 0xB00 <-> "mcycle" mapping clause csr_name_map = 0xB02 <-> "minstret" diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 518396f91..496b86065 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -109,6 +109,18 @@ function readCSR csr : csreg -> xlenbits = { (0x3A1, 32) => pmpReadCfgReg(1), // pmpcfg1 (0x3A2, _) => pmpReadCfgReg(2), // pmpcfg2 (0x3A3, 32) => pmpReadCfgReg(3), // pmpcfg3 + (0x3A4, _) => pmpReadCfgReg(4), // pmpcfg4 + (0x3A5, 32) => pmpReadCfgReg(5), // pmpcfg5 + (0x3A6, _) => pmpReadCfgReg(6), // pmpcfg6 + (0x3A7, 32) => pmpReadCfgReg(7), // pmpcfg7 + (0x3A8, _) => pmpReadCfgReg(8), // pmpcfg8 + (0x3A9, 32) => pmpReadCfgReg(9), // pmpcfg9 + (0x3AA, _) => pmpReadCfgReg(10), // pmpcfg10 + (0x3AB, 32) => pmpReadCfgReg(11), // pmpcfg11 + (0x3AC, _) => pmpReadCfgReg(12), // pmpcfg12 + (0x3AD, 32) => pmpReadCfgReg(13), // pmpcfg13 + (0x3AE, _) => pmpReadCfgReg(14), // pmpcfg14 + (0x3AF, 32) => pmpReadCfgReg(15), // pmpcfg15 (0x3B0, _) => pmpaddr0, (0x3B1, _) => pmpaddr1, @@ -126,6 +138,54 @@ function readCSR csr : csreg -> xlenbits = { (0x3BD, _) => pmpaddr13, (0x3BE, _) => pmpaddr14, (0x3BF, _) => pmpaddr15, + (0x3C0, _) => pmpaddr16, + (0x3C1, _) => pmpaddr17, + (0x3C2, _) => pmpaddr18, + (0x3C3, _) => pmpaddr19, + (0x3C4, _) => pmpaddr20, + (0x3C5, _) => pmpaddr21, + (0x3C6, _) => pmpaddr22, + (0x3C7, _) => pmpaddr23, + (0x3C8, _) => pmpaddr24, + (0x3C9, _) => pmpaddr25, + (0x3CA, _) => pmpaddr26, + (0x3CB, _) => pmpaddr27, + (0x3CC, _) => pmpaddr28, + (0x3CD, _) => pmpaddr29, + (0x3CE, _) => pmpaddr30, + (0x3CF, _) => pmpaddr31, + (0x3D0, _) => pmpaddr32, + (0x3D1, _) => pmpaddr33, + (0x3D2, _) => pmpaddr34, + (0x3D3, _) => pmpaddr35, + (0x3D4, _) => pmpaddr36, + (0x3D5, _) => pmpaddr37, + (0x3D6, _) => pmpaddr38, + (0x3D7, _) => pmpaddr39, + (0x3D8, _) => pmpaddr40, + (0x3D9, _) => pmpaddr41, + (0x3DA, _) => pmpaddr42, + (0x3DB, _) => pmpaddr43, + (0x3DC, _) => pmpaddr44, + (0x3DD, _) => pmpaddr45, + (0x3DE, _) => pmpaddr46, + (0x3DF, _) => pmpaddr47, + (0x3E0, _) => pmpaddr48, + (0x3E1, _) => pmpaddr49, + (0x3E2, _) => pmpaddr50, + (0x3E3, _) => pmpaddr51, + (0x3E4, _) => pmpaddr52, + (0x3E5, _) => pmpaddr53, + (0x3E6, _) => pmpaddr54, + (0x3E7, _) => pmpaddr55, + (0x3E8, _) => pmpaddr56, + (0x3E9, _) => pmpaddr57, + (0x3EA, _) => pmpaddr58, + (0x3EB, _) => pmpaddr59, + (0x3EC, _) => pmpaddr60, + (0x3ED, _) => pmpaddr61, + (0x3EE, _) => pmpaddr62, + (0x3EF, _) => pmpaddr63, /* machine mode counters */ (0xB00, _) => mcycle[(sizeof(xlen) - 1) .. 0], @@ -193,10 +253,23 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x344, _) => { mip = legalize_mip(mip, value); Some(mip.bits()) }, // Note: Some(value) returned below is not the legalized value due to locked entries - (0x3A0, _) => { pmpWriteCfgReg(0, value); Some(pmpReadCfgReg(0)) }, // pmpcfg0 - (0x3A1, 32) => { pmpWriteCfgReg(1, value); Some(pmpReadCfgReg(1)) }, // pmpcfg1 - (0x3A2, _) => { pmpWriteCfgReg(2, value); Some(pmpReadCfgReg(2)) }, // pmpcfg2 - (0x3A3, 32) => { pmpWriteCfgReg(3, value); Some(pmpReadCfgReg(3)) }, // pmpcfg3 + (0x3A0, _) => { pmpWriteCfgReg(0, value); Some(pmpReadCfgReg(0)) }, // pmpcfg0 + (0x3A1, 32) => { pmpWriteCfgReg(1, value); Some(pmpReadCfgReg(1)) }, // pmpcfg1 + (0x3A2, _) => { pmpWriteCfgReg(2, value); Some(pmpReadCfgReg(2)) }, // pmpcfg2 + (0x3A3, 32) => { pmpWriteCfgReg(3, value); Some(pmpReadCfgReg(3)) }, // pmpcfg3 + (0x3A4, _) => { pmpWriteCfgReg(4, value); Some(pmpReadCfgReg(4)) }, // pmpcfg4, + (0x3A5, 32) => { pmpWriteCfgReg(5, value); Some(pmpReadCfgReg(5)) }, // pmpcfg5, + (0x3A6, _) => { pmpWriteCfgReg(6, value); Some(pmpReadCfgReg(6)) }, // pmpcfg6, + (0x3A7, 32) => { pmpWriteCfgReg(7, value); Some(pmpReadCfgReg(7)) }, // pmpcfg7, + (0x3A8, _) => { pmpWriteCfgReg(8, value); Some(pmpReadCfgReg(8)) }, // pmpcfg8, + (0x3A9, 32) => { pmpWriteCfgReg(9, value); Some(pmpReadCfgReg(9)) }, // pmpcfg9, + (0x3AA, _) => { pmpWriteCfgReg(10, value); Some(pmpReadCfgReg(10))}, // pmpcfg10, + (0x3AB, 32) => { pmpWriteCfgReg(11, value); Some(pmpReadCfgReg(11))}, // pmpcfg11, + (0x3AC, _) => { pmpWriteCfgReg(12, value); Some(pmpReadCfgReg(12))}, // pmpcfg12, + (0x3AD, 32) => { pmpWriteCfgReg(13, value); Some(pmpReadCfgReg(13))}, // pmpcfg13, + (0x3AE, _) => { pmpWriteCfgReg(14, value); Some(pmpReadCfgReg(14))}, // pmpcfg14, + (0x3AF, 32) => { pmpWriteCfgReg(15, value); Some(pmpReadCfgReg(15))}, // pmpcfg15, + (0x3B0, _) => { pmpaddr0 = pmpWriteAddr(pmpLocked(pmp0cfg), pmpTORLocked(pmp1cfg), pmpaddr0, value); Some(pmpaddr0) }, (0x3B1, _) => { pmpaddr1 = pmpWriteAddr(pmpLocked(pmp1cfg), pmpTORLocked(pmp2cfg), pmpaddr1, value); Some(pmpaddr1) }, @@ -213,7 +286,55 @@ function writeCSR (csr : csreg, value : xlenbits) -> unit = { (0x3BC, _) => { pmpaddr12 = pmpWriteAddr(pmpLocked(pmp12cfg), pmpTORLocked(pmp13cfg), pmpaddr12, value); Some(pmpaddr12) }, (0x3BD, _) => { pmpaddr13 = pmpWriteAddr(pmpLocked(pmp13cfg), pmpTORLocked(pmp14cfg), pmpaddr13, value); Some(pmpaddr13) }, (0x3BE, _) => { pmpaddr14 = pmpWriteAddr(pmpLocked(pmp14cfg), pmpTORLocked(pmp15cfg), pmpaddr14, value); Some(pmpaddr14) }, - (0x3BF, _) => { pmpaddr15 = pmpWriteAddr(pmpLocked(pmp15cfg), false, pmpaddr15, value); Some(pmpaddr15) }, + (0x3BF, _) => { pmpaddr15 = pmpWriteAddr(pmpLocked(pmp15cfg), pmpTORLocked(pmp16cfg), pmpaddr15, value); Some(pmpaddr15) }, + (0x3C0, _) => { pmpaddr16 = pmpWriteAddr(pmpLocked(pmp16cfg), pmpTORLocked(pmp17cfg), pmpaddr16, value); Some(pmpaddr16) }, + (0x3C1, _) => { pmpaddr17 = pmpWriteAddr(pmpLocked(pmp17cfg), pmpTORLocked(pmp18cfg), pmpaddr17, value); Some(pmpaddr17) }, + (0x3C2, _) => { pmpaddr18 = pmpWriteAddr(pmpLocked(pmp18cfg), pmpTORLocked(pmp19cfg), pmpaddr18, value); Some(pmpaddr18) }, + (0x3C3, _) => { pmpaddr19 = pmpWriteAddr(pmpLocked(pmp19cfg), pmpTORLocked(pmp20cfg), pmpaddr19, value); Some(pmpaddr19) }, + (0x3C4, _) => { pmpaddr20 = pmpWriteAddr(pmpLocked(pmp20cfg), pmpTORLocked(pmp21cfg), pmpaddr20, value); Some(pmpaddr20) }, + (0x3C5, _) => { pmpaddr21 = pmpWriteAddr(pmpLocked(pmp21cfg), pmpTORLocked(pmp22cfg), pmpaddr21, value); Some(pmpaddr21) }, + (0x3C6, _) => { pmpaddr22 = pmpWriteAddr(pmpLocked(pmp22cfg), pmpTORLocked(pmp23cfg), pmpaddr22, value); Some(pmpaddr22) }, + (0x3C7, _) => { pmpaddr23 = pmpWriteAddr(pmpLocked(pmp23cfg), pmpTORLocked(pmp24cfg), pmpaddr23, value); Some(pmpaddr23) }, + (0x3C8, _) => { pmpaddr24 = pmpWriteAddr(pmpLocked(pmp24cfg), pmpTORLocked(pmp25cfg), pmpaddr24, value); Some(pmpaddr24) }, + (0x3C9, _) => { pmpaddr25 = pmpWriteAddr(pmpLocked(pmp25cfg), pmpTORLocked(pmp26cfg), pmpaddr25, value); Some(pmpaddr25) }, + (0x3CA, _) => { pmpaddr26 = pmpWriteAddr(pmpLocked(pmp26cfg), pmpTORLocked(pmp27cfg), pmpaddr26, value); Some(pmpaddr26) }, + (0x3CB, _) => { pmpaddr27 = pmpWriteAddr(pmpLocked(pmp27cfg), pmpTORLocked(pmp28cfg), pmpaddr27, value); Some(pmpaddr27) }, + (0x3CC, _) => { pmpaddr28 = pmpWriteAddr(pmpLocked(pmp28cfg), pmpTORLocked(pmp29cfg), pmpaddr28, value); Some(pmpaddr28) }, + (0x3CD, _) => { pmpaddr29 = pmpWriteAddr(pmpLocked(pmp29cfg), pmpTORLocked(pmp30cfg), pmpaddr29, value); Some(pmpaddr29) }, + (0x3CE, _) => { pmpaddr30 = pmpWriteAddr(pmpLocked(pmp30cfg), pmpTORLocked(pmp31cfg), pmpaddr30, value); Some(pmpaddr30) }, + (0x3CF, _) => { pmpaddr31 = pmpWriteAddr(pmpLocked(pmp31cfg), pmpTORLocked(pmp32cfg), pmpaddr31, value); Some(pmpaddr31) }, + (0x3D0, _) => { pmpaddr32 = pmpWriteAddr(pmpLocked(pmp32cfg), pmpTORLocked(pmp33cfg), pmpaddr32, value); Some(pmpaddr32) }, + (0x3D1, _) => { pmpaddr33 = pmpWriteAddr(pmpLocked(pmp33cfg), pmpTORLocked(pmp34cfg), pmpaddr33, value); Some(pmpaddr33) }, + (0x3D2, _) => { pmpaddr34 = pmpWriteAddr(pmpLocked(pmp34cfg), pmpTORLocked(pmp35cfg), pmpaddr34, value); Some(pmpaddr34) }, + (0x3D3, _) => { pmpaddr35 = pmpWriteAddr(pmpLocked(pmp35cfg), pmpTORLocked(pmp36cfg), pmpaddr35, value); Some(pmpaddr35) }, + (0x3D4, _) => { pmpaddr36 = pmpWriteAddr(pmpLocked(pmp36cfg), pmpTORLocked(pmp37cfg), pmpaddr36, value); Some(pmpaddr36) }, + (0x3D5, _) => { pmpaddr37 = pmpWriteAddr(pmpLocked(pmp37cfg), pmpTORLocked(pmp38cfg), pmpaddr37, value); Some(pmpaddr37) }, + (0x3D6, _) => { pmpaddr38 = pmpWriteAddr(pmpLocked(pmp38cfg), pmpTORLocked(pmp39cfg), pmpaddr38, value); Some(pmpaddr38) }, + (0x3D7, _) => { pmpaddr39 = pmpWriteAddr(pmpLocked(pmp39cfg), pmpTORLocked(pmp40cfg), pmpaddr39, value); Some(pmpaddr39) }, + (0x3D8, _) => { pmpaddr40 = pmpWriteAddr(pmpLocked(pmp40cfg), pmpTORLocked(pmp41cfg), pmpaddr40, value); Some(pmpaddr40) }, + (0x3D9, _) => { pmpaddr41 = pmpWriteAddr(pmpLocked(pmp41cfg), pmpTORLocked(pmp42cfg), pmpaddr41, value); Some(pmpaddr41) }, + (0x3DA, _) => { pmpaddr42 = pmpWriteAddr(pmpLocked(pmp42cfg), pmpTORLocked(pmp43cfg), pmpaddr42, value); Some(pmpaddr42) }, + (0x3DB, _) => { pmpaddr43 = pmpWriteAddr(pmpLocked(pmp43cfg), pmpTORLocked(pmp44cfg), pmpaddr43, value); Some(pmpaddr43) }, + (0x3DC, _) => { pmpaddr44 = pmpWriteAddr(pmpLocked(pmp44cfg), pmpTORLocked(pmp45cfg), pmpaddr44, value); Some(pmpaddr44) }, + (0x3DD, _) => { pmpaddr45 = pmpWriteAddr(pmpLocked(pmp45cfg), pmpTORLocked(pmp46cfg), pmpaddr45, value); Some(pmpaddr45) }, + (0x3DE, _) => { pmpaddr46 = pmpWriteAddr(pmpLocked(pmp46cfg), pmpTORLocked(pmp47cfg), pmpaddr46, value); Some(pmpaddr46) }, + (0x3DF, _) => { pmpaddr47 = pmpWriteAddr(pmpLocked(pmp47cfg), pmpTORLocked(pmp48cfg), pmpaddr47, value); Some(pmpaddr47) }, + (0x3E0, _) => { pmpaddr48 = pmpWriteAddr(pmpLocked(pmp48cfg), pmpTORLocked(pmp49cfg), pmpaddr48, value); Some(pmpaddr48) }, + (0x3E1, _) => { pmpaddr49 = pmpWriteAddr(pmpLocked(pmp49cfg), pmpTORLocked(pmp50cfg), pmpaddr49, value); Some(pmpaddr49) }, + (0x3E2, _) => { pmpaddr50 = pmpWriteAddr(pmpLocked(pmp50cfg), pmpTORLocked(pmp51cfg), pmpaddr50, value); Some(pmpaddr50) }, + (0x3E3, _) => { pmpaddr51 = pmpWriteAddr(pmpLocked(pmp51cfg), pmpTORLocked(pmp52cfg), pmpaddr51, value); Some(pmpaddr51) }, + (0x3E4, _) => { pmpaddr52 = pmpWriteAddr(pmpLocked(pmp52cfg), pmpTORLocked(pmp53cfg), pmpaddr52, value); Some(pmpaddr52) }, + (0x3E5, _) => { pmpaddr53 = pmpWriteAddr(pmpLocked(pmp53cfg), pmpTORLocked(pmp54cfg), pmpaddr53, value); Some(pmpaddr53) }, + (0x3E6, _) => { pmpaddr54 = pmpWriteAddr(pmpLocked(pmp54cfg), pmpTORLocked(pmp55cfg), pmpaddr54, value); Some(pmpaddr54) }, + (0x3E7, _) => { pmpaddr55 = pmpWriteAddr(pmpLocked(pmp55cfg), pmpTORLocked(pmp56cfg), pmpaddr55, value); Some(pmpaddr55) }, + (0x3E8, _) => { pmpaddr56 = pmpWriteAddr(pmpLocked(pmp56cfg), pmpTORLocked(pmp57cfg), pmpaddr56, value); Some(pmpaddr56) }, + (0x3E9, _) => { pmpaddr57 = pmpWriteAddr(pmpLocked(pmp57cfg), pmpTORLocked(pmp58cfg), pmpaddr57, value); Some(pmpaddr57) }, + (0x3EA, _) => { pmpaddr58 = pmpWriteAddr(pmpLocked(pmp58cfg), pmpTORLocked(pmp59cfg), pmpaddr58, value); Some(pmpaddr58) }, + (0x3EB, _) => { pmpaddr59 = pmpWriteAddr(pmpLocked(pmp59cfg), pmpTORLocked(pmp60cfg), pmpaddr59, value); Some(pmpaddr59) }, + (0x3EC, _) => { pmpaddr60 = pmpWriteAddr(pmpLocked(pmp60cfg), pmpTORLocked(pmp61cfg), pmpaddr60, value); Some(pmpaddr60) }, + (0x3ED, _) => { pmpaddr61 = pmpWriteAddr(pmpLocked(pmp61cfg), pmpTORLocked(pmp62cfg), pmpaddr61, value); Some(pmpaddr61) }, + (0x3EE, _) => { pmpaddr62 = pmpWriteAddr(pmpLocked(pmp62cfg), pmpTORLocked(pmp63cfg), pmpaddr62, value); Some(pmpaddr62) }, + (0x3EF, _) => { pmpaddr63 = pmpWriteAddr(pmpLocked(pmp63cfg), false, pmpaddr63, value); Some(pmpaddr63) }, /* machine mode counters */ (0xB00, _) => { mcycle[(sizeof(xlen) - 1) .. 0] = value; Some(value) }, diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 669725b5b..9233f3545 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -217,11 +217,204 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: atom('n), acc: Acce match pmpMatchEntry(addr, width, acc, priv, pmp15cfg, pmpaddr15, pmpaddr14) { PMP_Success => true, PMP_Fail => false, - PMP_Continue => match priv { - Machine => true, - _ => false - } - }}}}}}}}}}}}}}}}; + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp16cfg, pmpaddr16, pmpaddr15) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp17cfg, pmpaddr17, pmpaddr16) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp18cfg, pmpaddr18, pmpaddr17) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp19cfg, pmpaddr19, pmpaddr18) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp20cfg, pmpaddr20, pmpaddr19) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp21cfg, pmpaddr21, pmpaddr20) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp22cfg, pmpaddr22, pmpaddr21) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp23cfg, pmpaddr23, pmpaddr22) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp24cfg, pmpaddr24, pmpaddr23) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp25cfg, pmpaddr25, pmpaddr24) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp26cfg, pmpaddr26, pmpaddr25) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp27cfg, pmpaddr27, pmpaddr26) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp28cfg, pmpaddr28, pmpaddr27) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp29cfg, pmpaddr29, pmpaddr28) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp30cfg, pmpaddr30, pmpaddr29) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp31cfg, pmpaddr31, pmpaddr30) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp32cfg, pmpaddr32, pmpaddr31) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp33cfg, pmpaddr33, pmpaddr32) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp34cfg, pmpaddr34, pmpaddr33) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp35cfg, pmpaddr35, pmpaddr34) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp36cfg, pmpaddr36, pmpaddr35) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp37cfg, pmpaddr37, pmpaddr36) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp38cfg, pmpaddr38, pmpaddr37) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp39cfg, pmpaddr39, pmpaddr38) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp40cfg, pmpaddr40, pmpaddr39) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp41cfg, pmpaddr41, pmpaddr40) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp42cfg, pmpaddr42, pmpaddr41) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp43cfg, pmpaddr43, pmpaddr42) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp44cfg, pmpaddr44, pmpaddr43) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp45cfg, pmpaddr45, pmpaddr44) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp46cfg, pmpaddr46, pmpaddr45) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp47cfg, pmpaddr47, pmpaddr46) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp48cfg, pmpaddr48, pmpaddr47) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp49cfg, pmpaddr49, pmpaddr48) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp50cfg, pmpaddr50, pmpaddr49) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp51cfg, pmpaddr51, pmpaddr50) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp52cfg, pmpaddr52, pmpaddr51) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp53cfg, pmpaddr53, pmpaddr52) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp54cfg, pmpaddr54, pmpaddr53) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp55cfg, pmpaddr55, pmpaddr54) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp56cfg, pmpaddr56, pmpaddr55) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp57cfg, pmpaddr57, pmpaddr56) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp58cfg, pmpaddr58, pmpaddr57) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp59cfg, pmpaddr59, pmpaddr58) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp60cfg, pmpaddr60, pmpaddr59) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp61cfg, pmpaddr61, pmpaddr60) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp62cfg, pmpaddr62, pmpaddr61) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match pmpMatchEntry(addr, width, acc, priv, pmp63cfg, pmpaddr63, pmpaddr62) { + PMP_Success => true, + PMP_Fail => false, + PMP_Continue => + match priv { + Machine => true, + _ => false + + }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}; if check then None() @@ -249,5 +442,53 @@ function init_pmp() -> unit = { pmp12cfg = update_A(pmp12cfg, pmpAddrMatchType_to_bits(OFF)); pmp13cfg = update_A(pmp13cfg, pmpAddrMatchType_to_bits(OFF)); pmp14cfg = update_A(pmp14cfg, pmpAddrMatchType_to_bits(OFF)); - pmp15cfg = update_A(pmp15cfg, pmpAddrMatchType_to_bits(OFF)) + pmp15cfg = update_A(pmp15cfg, pmpAddrMatchType_to_bits(OFF)); + pmp16cfg = update_A(pmp16cfg, pmpAddrMatchType_to_bits(OFF)); + pmp17cfg = update_A(pmp17cfg, pmpAddrMatchType_to_bits(OFF)); + pmp18cfg = update_A(pmp18cfg, pmpAddrMatchType_to_bits(OFF)); + pmp19cfg = update_A(pmp19cfg, pmpAddrMatchType_to_bits(OFF)); + pmp20cfg = update_A(pmp20cfg, pmpAddrMatchType_to_bits(OFF)); + pmp21cfg = update_A(pmp21cfg, pmpAddrMatchType_to_bits(OFF)); + pmp22cfg = update_A(pmp22cfg, pmpAddrMatchType_to_bits(OFF)); + pmp23cfg = update_A(pmp23cfg, pmpAddrMatchType_to_bits(OFF)); + pmp24cfg = update_A(pmp24cfg, pmpAddrMatchType_to_bits(OFF)); + pmp25cfg = update_A(pmp25cfg, pmpAddrMatchType_to_bits(OFF)); + pmp26cfg = update_A(pmp26cfg, pmpAddrMatchType_to_bits(OFF)); + pmp27cfg = update_A(pmp27cfg, pmpAddrMatchType_to_bits(OFF)); + pmp28cfg = update_A(pmp28cfg, pmpAddrMatchType_to_bits(OFF)); + pmp29cfg = update_A(pmp29cfg, pmpAddrMatchType_to_bits(OFF)); + pmp30cfg = update_A(pmp30cfg, pmpAddrMatchType_to_bits(OFF)); + pmp31cfg = update_A(pmp31cfg, pmpAddrMatchType_to_bits(OFF)); + pmp32cfg = update_A(pmp32cfg, pmpAddrMatchType_to_bits(OFF)); + pmp33cfg = update_A(pmp33cfg, pmpAddrMatchType_to_bits(OFF)); + pmp34cfg = update_A(pmp34cfg, pmpAddrMatchType_to_bits(OFF)); + pmp35cfg = update_A(pmp35cfg, pmpAddrMatchType_to_bits(OFF)); + pmp36cfg = update_A(pmp36cfg, pmpAddrMatchType_to_bits(OFF)); + pmp37cfg = update_A(pmp37cfg, pmpAddrMatchType_to_bits(OFF)); + pmp38cfg = update_A(pmp38cfg, pmpAddrMatchType_to_bits(OFF)); + pmp39cfg = update_A(pmp39cfg, pmpAddrMatchType_to_bits(OFF)); + pmp40cfg = update_A(pmp40cfg, pmpAddrMatchType_to_bits(OFF)); + pmp41cfg = update_A(pmp41cfg, pmpAddrMatchType_to_bits(OFF)); + pmp42cfg = update_A(pmp42cfg, pmpAddrMatchType_to_bits(OFF)); + pmp43cfg = update_A(pmp43cfg, pmpAddrMatchType_to_bits(OFF)); + pmp44cfg = update_A(pmp44cfg, pmpAddrMatchType_to_bits(OFF)); + pmp45cfg = update_A(pmp45cfg, pmpAddrMatchType_to_bits(OFF)); + pmp46cfg = update_A(pmp46cfg, pmpAddrMatchType_to_bits(OFF)); + pmp47cfg = update_A(pmp47cfg, pmpAddrMatchType_to_bits(OFF)); + pmp48cfg = update_A(pmp48cfg, pmpAddrMatchType_to_bits(OFF)); + pmp49cfg = update_A(pmp49cfg, pmpAddrMatchType_to_bits(OFF)); + pmp50cfg = update_A(pmp50cfg, pmpAddrMatchType_to_bits(OFF)); + pmp51cfg = update_A(pmp51cfg, pmpAddrMatchType_to_bits(OFF)); + pmp52cfg = update_A(pmp52cfg, pmpAddrMatchType_to_bits(OFF)); + pmp53cfg = update_A(pmp53cfg, pmpAddrMatchType_to_bits(OFF)); + pmp54cfg = update_A(pmp54cfg, pmpAddrMatchType_to_bits(OFF)); + pmp55cfg = update_A(pmp55cfg, pmpAddrMatchType_to_bits(OFF)); + pmp56cfg = update_A(pmp56cfg, pmpAddrMatchType_to_bits(OFF)); + pmp57cfg = update_A(pmp57cfg, pmpAddrMatchType_to_bits(OFF)); + pmp58cfg = update_A(pmp58cfg, pmpAddrMatchType_to_bits(OFF)); + pmp59cfg = update_A(pmp59cfg, pmpAddrMatchType_to_bits(OFF)); + pmp60cfg = update_A(pmp60cfg, pmpAddrMatchType_to_bits(OFF)); + pmp61cfg = update_A(pmp61cfg, pmpAddrMatchType_to_bits(OFF)); + pmp62cfg = update_A(pmp62cfg, pmpAddrMatchType_to_bits(OFF)); + pmp63cfg = update_A(pmp63cfg, pmpAddrMatchType_to_bits(OFF)) } diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index a5e21edf5..de8d4ecd3 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -116,6 +116,54 @@ register pmp12cfg : Pmpcfg_ent register pmp13cfg : Pmpcfg_ent register pmp14cfg : Pmpcfg_ent register pmp15cfg : Pmpcfg_ent +register pmp16cfg : Pmpcfg_ent +register pmp17cfg : Pmpcfg_ent +register pmp18cfg : Pmpcfg_ent +register pmp19cfg : Pmpcfg_ent +register pmp20cfg : Pmpcfg_ent +register pmp21cfg : Pmpcfg_ent +register pmp22cfg : Pmpcfg_ent +register pmp23cfg : Pmpcfg_ent +register pmp24cfg : Pmpcfg_ent +register pmp25cfg : Pmpcfg_ent +register pmp26cfg : Pmpcfg_ent +register pmp27cfg : Pmpcfg_ent +register pmp28cfg : Pmpcfg_ent +register pmp29cfg : Pmpcfg_ent +register pmp30cfg : Pmpcfg_ent +register pmp31cfg : Pmpcfg_ent +register pmp32cfg : Pmpcfg_ent +register pmp33cfg : Pmpcfg_ent +register pmp34cfg : Pmpcfg_ent +register pmp35cfg : Pmpcfg_ent +register pmp36cfg : Pmpcfg_ent +register pmp37cfg : Pmpcfg_ent +register pmp38cfg : Pmpcfg_ent +register pmp39cfg : Pmpcfg_ent +register pmp40cfg : Pmpcfg_ent +register pmp41cfg : Pmpcfg_ent +register pmp42cfg : Pmpcfg_ent +register pmp43cfg : Pmpcfg_ent +register pmp44cfg : Pmpcfg_ent +register pmp45cfg : Pmpcfg_ent +register pmp46cfg : Pmpcfg_ent +register pmp47cfg : Pmpcfg_ent +register pmp48cfg : Pmpcfg_ent +register pmp49cfg : Pmpcfg_ent +register pmp50cfg : Pmpcfg_ent +register pmp51cfg : Pmpcfg_ent +register pmp52cfg : Pmpcfg_ent +register pmp53cfg : Pmpcfg_ent +register pmp54cfg : Pmpcfg_ent +register pmp55cfg : Pmpcfg_ent +register pmp56cfg : Pmpcfg_ent +register pmp57cfg : Pmpcfg_ent +register pmp58cfg : Pmpcfg_ent +register pmp59cfg : Pmpcfg_ent +register pmp60cfg : Pmpcfg_ent +register pmp61cfg : Pmpcfg_ent +register pmp62cfg : Pmpcfg_ent +register pmp63cfg : Pmpcfg_ent /* PMP address configuration */ @@ -135,21 +183,87 @@ register pmpaddr12 : xlenbits register pmpaddr13 : xlenbits register pmpaddr14 : xlenbits register pmpaddr15 : xlenbits +register pmpaddr16 : xlenbits +register pmpaddr17 : xlenbits +register pmpaddr18 : xlenbits +register pmpaddr19 : xlenbits +register pmpaddr20 : xlenbits +register pmpaddr21 : xlenbits +register pmpaddr22 : xlenbits +register pmpaddr23 : xlenbits +register pmpaddr24 : xlenbits +register pmpaddr25 : xlenbits +register pmpaddr26 : xlenbits +register pmpaddr27 : xlenbits +register pmpaddr28 : xlenbits +register pmpaddr29 : xlenbits +register pmpaddr30 : xlenbits +register pmpaddr31 : xlenbits +register pmpaddr32 : xlenbits +register pmpaddr33 : xlenbits +register pmpaddr34 : xlenbits +register pmpaddr35 : xlenbits +register pmpaddr36 : xlenbits +register pmpaddr37 : xlenbits +register pmpaddr38 : xlenbits +register pmpaddr39 : xlenbits +register pmpaddr40 : xlenbits +register pmpaddr41 : xlenbits +register pmpaddr42 : xlenbits +register pmpaddr43 : xlenbits +register pmpaddr44 : xlenbits +register pmpaddr45 : xlenbits +register pmpaddr46 : xlenbits +register pmpaddr47 : xlenbits +register pmpaddr48 : xlenbits +register pmpaddr49 : xlenbits +register pmpaddr50 : xlenbits +register pmpaddr51 : xlenbits +register pmpaddr52 : xlenbits +register pmpaddr53 : xlenbits +register pmpaddr54 : xlenbits +register pmpaddr55 : xlenbits +register pmpaddr56 : xlenbits +register pmpaddr57 : xlenbits +register pmpaddr58 : xlenbits +register pmpaddr59 : xlenbits +register pmpaddr60 : xlenbits +register pmpaddr61 : xlenbits +register pmpaddr62 : xlenbits +register pmpaddr63 : xlenbits /* Packing and unpacking pmpcfg regs for xlen-width accesses */ -val pmpReadCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n)) -> xlenbits effect {rreg} +val pmpReadCfgReg : forall 'n, 0 <= 'n < 16 . (atom('n)) -> xlenbits effect {rreg} function pmpReadCfgReg(n) = { if sizeof(xlen) == 32 then match n { 0 => append(pmp3cfg.bits(), append(pmp2cfg.bits(), append(pmp1cfg.bits(), pmp0cfg.bits()))), 1 => append(pmp7cfg.bits(), append(pmp6cfg.bits(), append(pmp5cfg.bits(), pmp4cfg.bits()))), 2 => append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(), pmp8cfg.bits()))), - 3 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), pmp12cfg.bits()))) + 3 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), pmp12cfg.bits()))), + 4 => append(pmp19cfg.bits(), append(pmp18cfg.bits(), append(pmp17cfg.bits(), pmp16cfg.bits()))), + 5 => append(pmp23cfg.bits(), append(pmp22cfg.bits(), append(pmp21cfg.bits(), pmp20cfg.bits()))), + 6 => append(pmp27cfg.bits(), append(pmp26cfg.bits(), append(pmp25cfg.bits(), pmp24cfg.bits()))), + 7 => append(pmp31cfg.bits(), append(pmp30cfg.bits(), append(pmp29cfg.bits(), pmp28cfg.bits()))), + 8 => append(pmp35cfg.bits(), append(pmp34cfg.bits(), append(pmp33cfg.bits(), pmp32cfg.bits()))), + 9 => append(pmp39cfg.bits(), append(pmp38cfg.bits(), append(pmp37cfg.bits(), pmp36cfg.bits()))), + 10 => append(pmp43cfg.bits(), append(pmp42cfg.bits(), append(pmp41cfg.bits(), pmp40cfg.bits()))), + 11 => append(pmp47cfg.bits(), append(pmp46cfg.bits(), append(pmp45cfg.bits(), pmp44cfg.bits()))), + 12 => append(pmp51cfg.bits(), append(pmp50cfg.bits(), append(pmp49cfg.bits(), pmp48cfg.bits()))), + 13 => append(pmp55cfg.bits(), append(pmp54cfg.bits(), append(pmp53cfg.bits(), pmp52cfg.bits()))), + 14 => append(pmp59cfg.bits(), append(pmp58cfg.bits(), append(pmp57cfg.bits(), pmp56cfg.bits()))), + 15 => append(pmp63cfg.bits(), append(pmp62cfg.bits(), append(pmp61cfg.bits(), pmp60cfg.bits()))) } else match n { // sizeof(xlen) == 64 0 => append(pmp7cfg.bits(), append(pmp6cfg.bits(), append(pmp5cfg.bits(), append(pmp4cfg.bits(), append(pmp3cfg.bits(), append(pmp2cfg.bits(), append(pmp1cfg.bits(), pmp0cfg.bits()))))))), - 2 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), append(pmp12cfg.bits(), append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(), pmp8cfg.bits()))))))) + 2 => append(pmp15cfg.bits(), append(pmp14cfg.bits(), append(pmp13cfg.bits(), append(pmp12cfg.bits(), append(pmp11cfg.bits(), append(pmp10cfg.bits(), append(pmp9cfg.bits(), pmp8cfg.bits()))))))), + 4 => append(pmp23cfg.bits(), append(pmp22cfg.bits(), append(pmp21cfg.bits(), append(pmp20cfg.bits(), append(pmp19cfg.bits(), append(pmp18cfg.bits(), append(pmp17cfg.bits(), pmp16cfg.bits()))))))), + 6 => append(pmp31cfg.bits(), append(pmp30cfg.bits(), append(pmp29cfg.bits(), append(pmp28cfg.bits(), append(pmp27cfg.bits(), append(pmp26cfg.bits(), append(pmp25cfg.bits(), pmp24cfg.bits()))))))), + 8 => append(pmp39cfg.bits(), append(pmp38cfg.bits(), append(pmp37cfg.bits(), append(pmp36cfg.bits(), append(pmp35cfg.bits(), append(pmp34cfg.bits(), append(pmp33cfg.bits(), pmp32cfg.bits()))))))), + 10 => append(pmp47cfg.bits(), append(pmp46cfg.bits(), append(pmp45cfg.bits(), append(pmp44cfg.bits(), append(pmp43cfg.bits(), append(pmp42cfg.bits(), append(pmp41cfg.bits(), pmp40cfg.bits()))))))), + 12 => append(pmp55cfg.bits(), append(pmp54cfg.bits(), append(pmp53cfg.bits(), append(pmp52cfg.bits(), append(pmp51cfg.bits(), append(pmp50cfg.bits(), append(pmp49cfg.bits(), pmp48cfg.bits()))))))), + 14 => append(pmp63cfg.bits(), append(pmp62cfg.bits(), append(pmp61cfg.bits(), append(pmp60cfg.bits(), append(pmp59cfg.bits(), append(pmp58cfg.bits(), append(pmp57cfg.bits(), pmp56cfg.bits()))))))) } } @@ -164,7 +278,7 @@ function pmpWriteCfg(cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = if pmpLocked(cfg) then cfg else Mk_Pmpcfg_ent(v & 0x9f) // Bits 5 and 6 are zero. -val pmpWriteCfgReg : forall 'n, 0 <= 'n < 4 . (atom('n), xlenbits) -> unit effect {rreg, wreg} +val pmpWriteCfgReg : forall 'n, 0 <= 'n < 16 . (atom('n), xlenbits) -> unit effect {rreg, wreg} function pmpWriteCfgReg(n, v) = { if sizeof(xlen) == 32 then match n { @@ -187,6 +301,66 @@ function pmpWriteCfgReg(n, v) = { pmp13cfg = pmpWriteCfg(pmp13cfg, v[15..8]); pmp14cfg = pmpWriteCfg(pmp14cfg, v[23..16]); pmp15cfg = pmpWriteCfg(pmp15cfg, v[31..24]); + }, + 4 => { pmp16cfg = pmpWriteCfg(pmp16cfg, v[7 ..0]); + pmp17cfg = pmpWriteCfg(pmp17cfg, v[15..8]); + pmp18cfg = pmpWriteCfg(pmp18cfg, v[23..16]); + pmp19cfg = pmpWriteCfg(pmp19cfg, v[31..24]); + }, + 5 => { pmp20cfg = pmpWriteCfg(pmp20cfg, v[7 ..0]); + pmp21cfg = pmpWriteCfg(pmp21cfg, v[15..8]); + pmp22cfg = pmpWriteCfg(pmp22cfg, v[23..16]); + pmp23cfg = pmpWriteCfg(pmp23cfg, v[31..24]); + }, + 6 => { pmp24cfg = pmpWriteCfg(pmp24cfg, v[7 ..0]); + pmp25cfg = pmpWriteCfg(pmp25cfg, v[15..8]); + pmp26cfg = pmpWriteCfg(pmp26cfg, v[23..16]); + pmp27cfg = pmpWriteCfg(pmp27cfg, v[31..24]); + }, + 7 => { pmp28cfg = pmpWriteCfg(pmp28cfg, v[7 ..0]); + pmp29cfg = pmpWriteCfg(pmp29cfg, v[15..8]); + pmp30cfg = pmpWriteCfg(pmp30cfg, v[23..16]); + pmp31cfg = pmpWriteCfg(pmp31cfg, v[31..24]); + }, + 8 => { pmp32cfg = pmpWriteCfg(pmp32cfg, v[7 ..0]); + pmp33cfg = pmpWriteCfg(pmp33cfg, v[15..8]); + pmp34cfg = pmpWriteCfg(pmp34cfg, v[23..16]); + pmp35cfg = pmpWriteCfg(pmp35cfg, v[31..24]); + }, + 9 => { pmp36cfg = pmpWriteCfg(pmp36cfg, v[7 ..0]); + pmp37cfg = pmpWriteCfg(pmp37cfg, v[15..8]); + pmp38cfg = pmpWriteCfg(pmp38cfg, v[23..16]); + pmp39cfg = pmpWriteCfg(pmp39cfg, v[31..24]); + }, + 10 => { pmp40cfg = pmpWriteCfg(pmp40cfg, v[7 ..0]); + pmp41cfg = pmpWriteCfg(pmp41cfg, v[15..8]); + pmp42cfg = pmpWriteCfg(pmp42cfg, v[23..16]); + pmp43cfg = pmpWriteCfg(pmp43cfg, v[31..24]); + }, + 11 => { pmp44cfg = pmpWriteCfg(pmp44cfg, v[7 ..0]); + pmp45cfg = pmpWriteCfg(pmp45cfg, v[15..8]); + pmp46cfg = pmpWriteCfg(pmp46cfg, v[23..16]); + pmp47cfg = pmpWriteCfg(pmp47cfg, v[31..24]); + }, + 12 => { pmp48cfg = pmpWriteCfg(pmp48cfg, v[7 ..0]); + pmp49cfg = pmpWriteCfg(pmp49cfg, v[15..8]); + pmp50cfg = pmpWriteCfg(pmp50cfg, v[23..16]); + pmp51cfg = pmpWriteCfg(pmp51cfg, v[31..24]); + }, + 13 => { pmp52cfg = pmpWriteCfg(pmp52cfg, v[7 ..0]); + pmp53cfg = pmpWriteCfg(pmp53cfg, v[15..8]); + pmp54cfg = pmpWriteCfg(pmp54cfg, v[23..16]); + pmp55cfg = pmpWriteCfg(pmp55cfg, v[31..24]); + }, + 14 => { pmp56cfg = pmpWriteCfg(pmp56cfg, v[7 ..0]); + pmp57cfg = pmpWriteCfg(pmp57cfg, v[15..8]); + pmp58cfg = pmpWriteCfg(pmp58cfg, v[23..16]); + pmp59cfg = pmpWriteCfg(pmp59cfg, v[31..24]); + }, + 15 => { pmp60cfg = pmpWriteCfg(pmp60cfg, v[7 ..0]); + pmp61cfg = pmpWriteCfg(pmp61cfg, v[15..8]); + pmp62cfg = pmpWriteCfg(pmp62cfg, v[23..16]); + pmp63cfg = pmpWriteCfg(pmp63cfg, v[31..24]); } } else if sizeof(xlen) == 64 @@ -208,7 +382,62 @@ function pmpWriteCfgReg(n, v) = { pmp13cfg = pmpWriteCfg(pmp13cfg, v[47..40]); pmp14cfg = pmpWriteCfg(pmp14cfg, v[55..48]); pmp15cfg = pmpWriteCfg(pmp15cfg, v[63..56]) + }, + 4 => { pmp16cfg = pmpWriteCfg(pmp16cfg, v[7 ..0]); + pmp17cfg = pmpWriteCfg(pmp17cfg, v[15..8]); + pmp18cfg = pmpWriteCfg(pmp18cfg, v[23..16]); + pmp19cfg = pmpWriteCfg(pmp19cfg, v[31..24]); + pmp20cfg = pmpWriteCfg(pmp19cfg, v[39..32]); + pmp21cfg = pmpWriteCfg(pmp19cfg, v[47..40]); + pmp22cfg = pmpWriteCfg(pmp19cfg, v[55..48]); + pmp23cfg = pmpWriteCfg(pmp19cfg, v[63..56]); + }, + 6 => { pmp24cfg = pmpWriteCfg(pmp24cfg, v[7 ..0]); + pmp25cfg = pmpWriteCfg(pmp25cfg, v[15..8]); + pmp26cfg = pmpWriteCfg(pmp26cfg, v[23..16]); + pmp27cfg = pmpWriteCfg(pmp27cfg, v[31..24]); + pmp28cfg = pmpWriteCfg(pmp27cfg, v[39..32]); + pmp29cfg = pmpWriteCfg(pmp27cfg, v[47..40]); + pmp30cfg = pmpWriteCfg(pmp27cfg, v[55..48]); + pmp31cfg = pmpWriteCfg(pmp27cfg, v[63..56]); + }, + 8 => { pmp32cfg = pmpWriteCfg(pmp32cfg, v[7 ..0]); + pmp33cfg = pmpWriteCfg(pmp33cfg, v[15..8]); + pmp34cfg = pmpWriteCfg(pmp34cfg, v[23..16]); + pmp35cfg = pmpWriteCfg(pmp35cfg, v[31..24]); + pmp36cfg = pmpWriteCfg(pmp35cfg, v[39..32]); + pmp37cfg = pmpWriteCfg(pmp35cfg, v[47..40]); + pmp38cfg = pmpWriteCfg(pmp35cfg, v[55..48]); + pmp39cfg = pmpWriteCfg(pmp35cfg, v[63..56]); + }, + 10 => { pmp40cfg = pmpWriteCfg(pmp40cfg, v[7 ..0]); + pmp41cfg = pmpWriteCfg(pmp41cfg, v[15..8]); + pmp42cfg = pmpWriteCfg(pmp42cfg, v[23..16]); + pmp43cfg = pmpWriteCfg(pmp43cfg, v[31..24]); + pmp44cfg = pmpWriteCfg(pmp43cfg, v[39..32]); + pmp45cfg = pmpWriteCfg(pmp43cfg, v[47..40]); + pmp46cfg = pmpWriteCfg(pmp43cfg, v[55..48]); + pmp47cfg = pmpWriteCfg(pmp43cfg, v[63..56]); + }, + 12 => { pmp48cfg = pmpWriteCfg(pmp48cfg, v[7 ..0]); + pmp49cfg = pmpWriteCfg(pmp49cfg, v[15..8]); + pmp50cfg = pmpWriteCfg(pmp50cfg, v[23..16]); + pmp51cfg = pmpWriteCfg(pmp51cfg, v[31..24]); + pmp52cfg = pmpWriteCfg(pmp51cfg, v[39..32]); + pmp53cfg = pmpWriteCfg(pmp51cfg, v[47..40]); + pmp54cfg = pmpWriteCfg(pmp51cfg, v[55..48]); + pmp55cfg = pmpWriteCfg(pmp51cfg, v[63..56]); + }, + 14 => { pmp56cfg = pmpWriteCfg(pmp56cfg, v[7 ..0]); + pmp57cfg = pmpWriteCfg(pmp57cfg, v[15..8]); + pmp58cfg = pmpWriteCfg(pmp58cfg, v[23..16]); + pmp59cfg = pmpWriteCfg(pmp59cfg, v[31..24]); + pmp60cfg = pmpWriteCfg(pmp59cfg, v[39..32]); + pmp61cfg = pmpWriteCfg(pmp59cfg, v[47..40]); + pmp62cfg = pmpWriteCfg(pmp59cfg, v[55..48]); + pmp63cfg = pmpWriteCfg(pmp59cfg, v[63..56]); } + } } diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6204ae59e..95ff2fbe4 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -102,6 +102,18 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x3A1 => p == Machine & (sizeof(xlen) == 32), // pmpcfg1 0x3A2 => p == Machine, // pmpcfg2 0x3A3 => p == Machine & (sizeof(xlen) == 32), // pmpcfg3 + 0x3A4 => p == Machine, // pmpcfg4 + 0x3A5 => p == Machine & (sizeof(xlen) == 32), // pmpcfg5 + 0x3A6 => p == Machine, // pmpcfg6 + 0x3A7 => p == Machine & (sizeof(xlen) == 32), // pmpcfg7 + 0x3A8 => p == Machine, // pmpcfg8 + 0x3A9 => p == Machine & (sizeof(xlen) == 32), // pmpcfg9 + 0x3AA => p == Machine, // pmpcfg10 + 0x3AB => p == Machine & (sizeof(xlen) == 32), // pmpcfg11 + 0x3AC => p == Machine, // pmpcfg12 + 0x3AD => p == Machine & (sizeof(xlen) == 32), // pmpcfg13 + 0x3AE => p == Machine, // pmpcfg14 + 0x3AF => p == Machine & (sizeof(xlen) == 32), // pmpcfg15 0x3B0 => p == Machine, // pmpaddr0 0x3B1 => p == Machine, // pmpaddr1 @@ -113,12 +125,61 @@ function is_CSR_defined (csr : csreg, p : Privilege) -> bool = 0x3B7 => p == Machine, // pmpaddr7 0x3B8 => p == Machine, // pmpaddr8 0x3B9 => p == Machine, // pmpaddr9 - 0x3BA => p == Machine, // pmpaddrA - 0x3BB => p == Machine, // pmpaddrB - 0x3BC => p == Machine, // pmpaddrC - 0x3BD => p == Machine, // pmpaddrD - 0x3BE => p == Machine, // pmpaddrE - 0x3BF => p == Machine, // pmpaddrF + 0x3BA => p == Machine, // pmpaddr10 + 0x3BB => p == Machine, // pmpaddr11 + 0x3BC => p == Machine, // pmpaddr12 + 0x3BD => p == Machine, // pmpaddr13 + 0x3BE => p == Machine, // pmpaddr14 + 0x3BF => p == Machine, // pmpaddr15 + 0x3C0 => p == Machine, // pmpaddr16 + 0x3C1 => p == Machine, // pmpaddr17 + 0x3C2 => p == Machine, // pmpaddr18 + 0x3C3 => p == Machine, // pmpaddr19 + 0x3C4 => p == Machine, // pmpaddr20 + 0x3C5 => p == Machine, // pmpaddr21 + 0x3C6 => p == Machine, // pmpaddr22 + 0x3C7 => p == Machine, // pmpaddr23 + 0x3C8 => p == Machine, // pmpaddr24 + 0x3C9 => p == Machine, // pmpaddr25 + 0x3CA => p == Machine, // pmpaddr26 + 0x3CB => p == Machine, // pmpaddr27 + 0x3CC => p == Machine, // pmpaddr28 + 0x3CD => p == Machine, // pmpaddr29 + 0x3CE => p == Machine, // pmpaddr30 + 0x3CF => p == Machine, // pmpaddr31 + 0x3D0 => p == Machine, // pmpaddr32 + 0x3D1 => p == Machine, // pmpaddr33 + 0x3D2 => p == Machine, // pmpaddr34 + 0x3D3 => p == Machine, // pmpaddr35 + 0x3D4 => p == Machine, // pmpaddr36 + 0x3D5 => p == Machine, // pmpaddr37 + 0x3D6 => p == Machine, // pmpaddr38 + 0x3D7 => p == Machine, // pmpaddr39 + 0x3D8 => p == Machine, // pmpaddr40 + 0x3D9 => p == Machine, // pmpaddr41 + 0x3DA => p == Machine, // pmpaddr42 + 0x3DB => p == Machine, // pmpaddr43 + 0x3DC => p == Machine, // pmpaddr44 + 0x3DD => p == Machine, // pmpaddr45 + 0x3DE => p == Machine, // pmpaddr46 + 0x3DF => p == Machine, // pmpaddr47 + 0x3E0 => p == Machine, // pmpaddr48 + 0x3E1 => p == Machine, // pmpaddr49 + 0x3E2 => p == Machine, // pmpaddr50 + 0x3E3 => p == Machine, // pmpaddr51 + 0x3E4 => p == Machine, // pmpaddr52 + 0x3E5 => p == Machine, // pmpaddr53 + 0x3E6 => p == Machine, // pmpaddr54 + 0x3E7 => p == Machine, // pmpaddr55 + 0x3E8 => p == Machine, // pmpaddr56 + 0x3E9 => p == Machine, // pmpaddr57 + 0x3EA => p == Machine, // pmpaddr58 + 0x3EB => p == Machine, // pmpaddr59 + 0x3EC => p == Machine, // pmpaddr60 + 0x3ED => p == Machine, // pmpaddr61 + 0x3EE => p == Machine, // pmpaddr62 + 0x3EF => p == Machine, // pmpaddr63 + /* counters */ 0xB00 => p == Machine, // mcycle