[cheriot,rtl] Debug Mode: bounds override results, silent SR fault, forwarded suppressed write

Đang mở
#2,567 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

Maintainer thường phản hồi trong vòng 2 ngày

Chưa có ai nhận issue này.

Đánh giá

Độ khó
4/5
Thời gian dự kiến
3-5 ngày
Mức phù hợp với người mới
35/100
Loại issue
Lỗi
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Sôi nổi
Lĩnh vực
operating-systems

Hướng nghiên cứu

Start with the Debug Mode section in debug.rst and the cited RTL locations: ibex_cheriot_ex.sv:774-775, ibex_cheriot_ex.sv:858, ibex_controller.sv:239-241, and ibex_wb_stage.sv:191. Trace the bounds, SR fault, and writeback forwarding behavior against the provided SymbiYosys observations. Done means the intended RTL or documentation changes are decided and the suppressed-value forwarding case is addressed.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

The "Debug Mode in CHERIoT" section that #2555 added to debug.rst does not cover three details yet. Two are questions on whether the RTL or the text should change. The third looks like a defect. All three predate #2555.

The bounds override changes instruction results, not only the load and store checks. In Debug Mode, the bounds check never reports a violation (ibex_cheriot_ex.sv:774-775). So CTestSubset can return 1 when the second capability's bounds extend outside the first. CSeal and CUnseal can keep a tag that their Sail bounds test would clear. Dropping the override would change only these three results, because the load and store fault has its own Debug Mode term (ibex_cheriot_ex.sv:858). Should the override go, or should the list in debug.rst mention these results?

The SR check on CSpecialRW also differs from the one on CSR accesses. In Debug Mode, when PCC lacks SR, a CSpecialRW of an implemented SCR writes neither its destination register nor the SCR, and raises no exception. An access to an SR-protected CSR such as dpc still traps in that state (ibex_controller.sv:239-241). PCC can lose SR in Debug Mode through a CJALR to a tagged, executable capability without SR. Should the SR fault also trap in Debug Mode, as a CSR access does, or should debug.rst say that the SCR access is suppressed?

The next instruction can still see the suppressed value. With the writeback stage present, forwarding follows rf_write_wb_o (ibex_wb_stage.sv:191). That signal still includes the decoder's write enable. The fault clears the CHERIoT write enable, not the decoder's. The register write on line 184 uses the CHERIoT one, so in this sequence c11 keeps its old value. The CMove can still copy mscratchc into c10:

cspecialrw c11, mscratchc, c6   # PCC lacks SR
cmove      c10, c11

A CJALR whose fault is masked forwards its link capability the same way. This looks worth fixing whichever way the SR question goes.

I checked these with SymbiYosys on ibex_core at master d513671d. The parameters are based on opentitan, with CHERIoT on and the register file included. Each run starts from reset and has no data-memory transactions. In Debug Mode each case is reachable in a few instructions from the reset capabilities. Outside Debug Mode the proof shows that, for well-formed operands, CTestSubset returns 1 and CSeal or CUnseal keep the tag only when the bounds condition holds. On a local tree where the SR fault traps, and with other masked faults excluded, no following instruction completes with the suppressed value. I did not simulate these, because no upstream bench enables CHERIoT.

Ngôn ngữ chính
SystemVerilog
Star
2.2k
Fork
836
Merge trung bình
5 ngày 8 giờ
Pull request đã merge (30 ngày)
22

Chuẩn bị môi trường

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của lowRISC/ibex

Tất cả issue của lowRISC/ibex

Issue tương tự

Thêm issue về Operating Systems

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.