Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add base address register as extra argument to ext_data_check_addr hook #5

Merged
merged 2 commits into from
May 2, 2019
Merged

Add base address register as extra argument to ext_data_check_addr hook #5

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
acc772b
Add base address register as extra argument to ext_data_check_addr ho…
rmn30 May 1, 2019
42df969
Push address calculation inside the data_check_addr hook and rename i…
rmn30 May 2, 2019
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
9 changes: 7 additions & 2 deletions model/riscv_addr_checks.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,11 +39,16 @@ function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_contro
function ext_handle_control_check_error(err : ext_control_addr_error) -> unit =
()

/* default data address checks */

/* The default data address function does not perform any checks so
just uses unit for error type. */
type ext_data_addr_error = unit

function ext_data_check_addr(addr : xlenbits, acc : AccessType, rt : ReadType, width : word_width)
/* Default data addr is just base register + immediate offset (may be zero).
Extensions might override and add additional checks. */
function ext_data_get_addr(base : regbits, offset : xlenbits, acc : AccessType, rt : ReadType, width : word_width)
-> Ext_DataAddr_Check(ext_data_addr_error) =
let addr = X(base) + offset in
Ext_DataAddr_OK(addr)

function ext_handle_data_check_error(err : ext_data_addr_error) -> unit =
Expand Down
21 changes: 12 additions & 9 deletions model/riscv_insts_aext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,9 +41,10 @@ function process_loadres(rd, addr, value, is_unsigned) =

function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
if haveAtomics() then {
let pre_vaddr : xlenbits = X(rs1);
/* Let extensions get the first check on address validity. */
match ext_data_check_addr(pre_vaddr, Read, Data, width) {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); false },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
Expand Down Expand Up @@ -99,9 +100,10 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
/* normal non-rmem case
* rmem: SC is allowed to succeed (but might fail later)
*/
pre_vaddr : xlenbits = X(rs1);
/* Let extensions get the first check on address validity. */
match ext_data_check_addr(pre_vaddr, Read, Data, width) {
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); false },
Ext_DataAddr_OK(vaddr) => {
let aligned : bool =
Expand Down Expand Up @@ -183,9 +185,10 @@ mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)
This may need revisiting. */
function clause execute (AMO(op, aq, rl, rs2, rs1, width, rd)) = {
if haveAtomics() then {
pre_vaddr : xlenbits = X(rs1);
/* Let extensions get the first check on address validity. */
match ext_data_check_addr(pre_vaddr, Read, Data, width) {
/* Get the address, X(rs1) (no offset).
* Some extensions perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Read, Data, width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); false },
Ext_DataAddr_OK(vaddr) => {
match translateAddr(vaddr, ReadWrite, Data) {
Expand Down
14 changes: 8 additions & 6 deletions model/riscv_insts_base.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -315,9 +315,10 @@ function check_misaligned(vaddr : xlenbits, width : word_width) -> bool =
}

function clause execute(LOAD(imm, rs1, rd, is_unsigned, width, aq, rl)) = {
let pre_vaddr : xlenbits = X(rs1) + EXTS(imm);
/* Let extensions get the first check on address validity. */
match ext_data_check_addr(pre_vaddr, Read, Data, width) {
let offset : xlenbits = EXTS(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Read, Data, width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); false },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down Expand Up @@ -370,9 +371,10 @@ mapping clause encdec = STORE(imm7 @ imm5, rs2, rs1, size, false, false)
/* NOTE: Currently, we only EA if address translation is successful.
This may need revisiting. */
function clause execute (STORE(imm, rs2, rs1, width, aq, rl)) = {
let pre_vaddr : xlenbits = X(rs1) + EXTS(imm);
/* Let extensions get the first check on address validity. */
match ext_data_check_addr(pre_vaddr, Write, Data, width) {
let offset : xlenbits = EXTS(imm);
/* Get the address, X(rs1) + offset.
Some extensions perform additional checks on address validity. */
match ext_data_get_addr(rs1, offset, Write, Data, width) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); false },
Ext_DataAddr_OK(vaddr) =>
if check_misaligned(vaddr, width)
Expand Down