操作数与参数
SrcL- Reg5 source of the queue address
SrcR- Reg5 source of the 64-bit entry
RegDst- Reg5 destination for the operation result
h- head-insertion selector
e- success-event selector
r- relaxed-ordering selector
Atomically pushes one 64-bit entry at the tail or head of a General Queue Management queue.
PTO-BLOCK-HL-QPUSHhl.qpush SrcL, SrcR, ->RegDsthl.qpush.h SrcL, SrcR, ->RegDsthl.qpush.e SrcL, SrcR, ->RegDsthl.qpush.r SrcL, SrcR, ->RegDsthl.qpush.he SrcL, SrcR, ->RegDsthl.qpush.hr SrcL, SrcR, ->RegDsthl.qpush.er SrcL, SrcR, ->RegDsthl.qpush.her SrcL, SrcR, ->RegDst| 字段 | 位宽 | 有符号性 | 架构角色 | 编码零 |
|---|---|---|---|---|
RegDst | 5 | encoding-defined | Reg5 destination for the operation result | Encoded zero names R0; reads produce zero and writes are discarded. |
SrcL | 5 | encoding-defined | Reg5 source of the queue address | Encoded zero names R0; reads produce zero and writes are discarded. |
SrcR | 5 | encoding-defined | Reg5 source of the 64-bit entry | Encoded zero names R0; reads produce zero and writes are discarded. |
e | 1 | encoding-defined | success-event selector | Zero suppresses event notification. |
h | 1 | encoding-defined | head-insertion selector | Zero appends at the queue tail. |
r | 1 | encoding-defined | relaxed-ordering selector | Zero selects release ordering. |
Loading WaveDrom diagram… The encoding table and WaveJSON remain available below.
| Decoded item | Bit range | Value |
|---|---|---|
| Constant | 47:44 | 4'b0000 |
| h | 43 | variable |
| r | 42 | variable |
| e | 41 | variable |
| SrcR | 40:36 | variable |
| SrcL | 35:31 | variable |
| Constant | 30:28 | 3'b001 |
| RegDst | 27:23 | variable |
| Constant | 22:0 | 23'b11111010000000000001110 |
{
"reg": [
{
"bits": 23,
"name": "23'b11111010000000000001110"
},
{
"bits": 5,
"name": "RegDst"
},
{
"bits": 3,
"name": "3'b001"
},
{
"bits": 5,
"name": "SrcL"
},
{
"bits": 5,
"name": "SrcR"
},
{
"bits": 1,
"name": "e"
},
{
"bits": 1,
"name": "r"
},
{
"bits": 1,
"name": "h"
},
{
"bits": 4,
"name": "4'b0000"
}
],
"config": {
"bits": 48,
"fontsize": 13,
"hspace": 900,
"lanes": 2,
"offset": 0
}
}hl.qpush[.{h,e,r,he,hr,er,her}] SrcL, SrcR, ->RegDst
SrcLSrcRRegDstherDecode 与 Operation 均直接来自指令所有者,并按执行阶段分开显示。
readonly func InstructionContractMatches_HL_QPUSH(operation: CommandOperation) => booleanbegin return (operation == CommandOperation_hl_qpush_48_3eab8e05d61a);end;readonly func InstructionContractHandler_HL_QPUSH() => CommandSemanticHandlerbegin return CommandHandler_ExecuteQueuePush;end;
func ExecuteHLQPUSH(destination: Reg5Selector, address: Word, entry: Word, flags: bits(4))begin ExecuteQueueManagerPush( destination, address, entry, flags);end;
pure func InstructionContractChangesQueueManagerState_HL_QPUSH() => booleanbegin return TRUE;end;
pure func InstructionContractSnapshotsSourcesBeforeWrite_HL_QPUSH() => booleanbegin return TRUE;end;// PTO-INSTRUCTION: {"assembly":["hl.qpush SrcL, SrcR, ->RegDst","hl.qpush.h SrcL, SrcR, ->RegDst","hl.qpush.e SrcL, SrcR, ->RegDst","hl.qpush.r SrcL, SrcR, ->RegDst","hl.qpush.he SrcL, SrcR, ->RegDst","hl.qpush.hr SrcL, SrcR, ->RegDst","hl.qpush.er SrcL, SrcR, ->RegDst","hl.qpush.her SrcL, SrcR, ->RegDst"],"block":[],"catalog_indices":[68],"catalog_records":[{"asm":"hl.qpush[.{h,e,r,he,hr,er,her}] SrcL, SrcR, ->RegDst","constraints":[],"encoding":[{"index":0,"mask":"0xf000707fffff","match":"0x0000107d000e","width_bits":48}],"encoding_kind":"HL48","fields":[{"name":"RegDst","pieces":[{"instruction_lsb":23,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"SrcL","pieces":[{"instruction_lsb":31,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"SrcR","pieces":[{"instruction_lsb":36,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"e","pieces":[{"instruction_lsb":41,"value_lsb":0,"width":1}],"signedness":"encoding-defined","width":1},{"name":"h","pieces":[{"instruction_lsb":43,"value_lsb":0,"width":1}],"signedness":"encoding-defined","width":1},{"name":"r","pieces":[{"instruction_lsb":42,"value_lsb":0,"width":1}],"signedness":"encoding-defined","width":1}],"form_id":"hl_qpush_48_3eab8e05d61a","length_bits":48,"mnemonic":"HL.QPUSH","semantic_family":"CMD","semantic_group":"General","semantic_handler":"ExecuteQueuePush","semantic_summary":"Atomically pushes one 64-bit entry at the tail or head of a General Queue Management queue.","status":"accepted"}],"classification":["lifecycle"],"contract":{"block_composition":["none"],"canonical_assembly":["hl.qpush SrcL, SrcR, ->RegDst","hl.qpush.h SrcL, SrcR, ->RegDst","hl.qpush.e SrcL, SrcR, ->RegDst","hl.qpush.r SrcL, SrcR, ->RegDst","hl.qpush.he SrcL, SrcR, ->RegDst","hl.qpush.hr SrcL, SrcR, ->RegDst","hl.qpush.er SrcL, SrcR, ->RegDst","hl.qpush.her SrcL, SrcR, ->RegDst"],"defaults":["The bare form appends at the tail, publishes no event, and has release semantics.","h=0 selects tail insertion, e=0 suppresses notification, and r=0 selects release ordering."],"encoding_class":"standalone-encoded","examples":["hl.qpush a0, a1, ->a2","hl.qpush.he t#1, u#1, ->t#2","hl.qpush.r sp, zero, ->u#1"],"exceptions":["Selector failures raise Fault_IllegalInstruction before source reads, queue observation, events, destination writes, or TPC advance.","Full, suspended, missing, and corrupt queues report status in RegDst and do not trap."],"field_contracts":{},"field_zero_meanings":{"SrcL":"Encoded zero names R0; reads produce zero and writes are discarded.","SrcR":"Encoded zero names R0; reads produce zero and writes are discarded.","RegDst":"Encoded zero names R0; reads produce zero and writes are discarded.","h":"Zero appends at the queue tail.","e":"Zero suppresses event notification.","r":"Zero selects release ordering."},"legality":["Reg5 values 0..23 select absolute R0..R23 and 24..31 select the block-relative T#1..T#4 or U#1..U#4 entries; unavailable relative sources and invalid relative destinations reject before queue state changes.","All eight h/e/r flag combinations are assigned; the event suffix is e and b is not an alias."],"memory_effects":["No direct memory access. A non-relaxed successful push releases memory operations ordered before it to an acquiring pop that observes the entry."],"operands":[{"field":"SrcL","role":"Reg5 source of the queue address"},{"field":"SrcR","role":"Reg5 source of the 64-bit entry"},{"field":"RegDst","role":"Reg5 destination for the operation result"},{"field":"h","role":"head-insertion selector"},{"field":"e","role":"success-event selector"},{"field":"r","role":"relaxed-ordering selector"}],"ordering":["Queue validation precedes insertion. A successful insertion precedes optional event notification and result publication.","r=0 establishes the release edge; r=1 is relaxed and records no release edge."],"standalone_opcode":true,"state_effects":["h=0 appends one entry at the tail; h=1 inserts one entry at the head. The queue update, optional event, and destination result are atomic.","Result bits [9:0] hold post-push remaining capacity and [63:62] hold status; unused bits are zero. Status 0 is success, 1 is full or suspended, 2 is missing or corrupt, and 3 is reserved.","Only a successful push with e=1 broadcasts an event."]},"depends_on":["PTO-BLOCK-MODEL-SCHEMA-PROFILE-ENCODING"],"id":"PTO-BLOCK-HL-QPUSH","mnemonic":"HL.QPUSH","summary":"Atomically pushes one 64-bit entry at the tail or head of a General Queue Management queue.","surface":"block"}// NDF-BEGIN: PTO-HL-QPUSH-GQM-001// ndf: kind=contract level=L1 layer=block status=accepted// HL.QPUSH MUST atomically insert one entry at the tail or head, optionally// notify after success, and provide release ordering unless r=1.// Full, suspended, missing, or corrupt queues MUST report status without insertion.// NDF-END: PTO-HL-QPUSH-GQM-001// DOC-BEGIN: decodereadonly func InstructionContractMatches_HL_QPUSH(operation: CommandOperation) => booleanbegin return (operation == CommandOperation_hl_qpush_48_3eab8e05d61a);end;// DOC-END: decode// DOC-BEGIN: operationreadonly func InstructionContractHandler_HL_QPUSH() => CommandSemanticHandlerbegin return CommandHandler_ExecuteQueuePush;end;
func ExecuteHLQPUSH(destination: Reg5Selector, address: Word, entry: Word, flags: bits(4))begin ExecuteQueueManagerPush( destination, address, entry, flags);end;
pure func InstructionContractChangesQueueManagerState_HL_QPUSH() => booleanbegin return TRUE;end;
pure func InstructionContractSnapshotsSourcesBeforeWrite_HL_QPUSH() => booleanbegin return TRUE;end;// DOC-END: operation// PTO-REVIEW: {"review_method":"formal-definition-read","outcome":"FORMAL-COMPLETE","reviewed_fields":["assembly","encoding","defaults","operation","state","memory","ordering","faults","reserved"]}
HL.QPUSH 是独立的通用队列管理命令;队列更新、状态结果与可选事件构成一个有序指令效果。
HL.QPUSH 作为独立的 48 位命令执行,不要求放在 BSTART/BSTOP Block 体内。
已接受载体使用 HL48 编码类别;命令在读取绑定或改变状态前,会先解析所有显示字段。
命令会在第一个可见效果前快照所有必需源,随后遵循归属单元定义的提交或重启边界。
SrcL — 提供队列地址的 Reg5 源; SrcR — 提供 64 位条目的 Reg5 源; RegDst — 接收操作结果的 Reg5 目的端; h — 头部插入选择器; e — 成功事件选择器; r — relaxed 顺序选择器。源验证与快照发生在所有寄存器、队列、栈帧、内存、事件或控制流效果之前。
命令把状态与结果作为一个有序指令效果发布,再按归属单元规定前移或转移控制。
固定比特、保留值、选择器取值域与必需的 Block 放置关系都在架构效果之前检查。
当前归属单元通过 Fault_IllegalInstruction 报告无效模式、状态、地址或后继条件;本页说明文字不创建额外故障规则。
除非当前归属单元明确规定带保留进度的重启边界,否则拒绝发生在效果之前;完成顺序始终采用 ASL 顺序。
该示例只演示放置关系与载体流;精确行为仍由当前 ASL 和指令契约定义。
hl.qpush a0, a1, ->a2所示已接受拼写从当前载体解析字段,快照必需源,再执行归属单元规定的状态与顺序转换。
正文来自 owning ASL。拖拽或按钮只临时改变当前页面显示顺序。
HL.QPUSH MUST atomically insert one entry at the tail or head, optionally notify after success, and provide release ordering unless r=1. Full, suspended, missing, or corrupt queues MUST report status without insertion.
PTO-HL-QPUSH-GQM-001asl/block/lifecycle/HL.QPUSH.asl7eacde3838de2f920447cb725e4c7e122362da7ff5ce36dfd474701d4f9da11ce7fd686c2eb20d408d2ea284a7ca271035007c90c9be7eeb976c6e7abdd9db0f12 matching entries
PTO-AVS-BLOCK-HL-QPUSH-DECODE-001tests/asl/block/lifecycle/HL.QPUSH/block-decode-hl-qpush-canonical-001.asl8c31f934646f18c489e864dca1d8cefde874feff03376e554746b9c50ca68998PTO-AVS-BLOCK-HL-QPUSH-ORDER-001tests/asl/block/lifecycle/HL.QPUSH/block-exec-hl-qpush-order-001.asl00b224fe5f1bbba870d0c3d552ed685c3b93744eef5cbbd786f76ae13058171cPTO-AVS-BLOCK-HL-QPUSH-STATUS-001tests/asl/block/lifecycle/HL.QPUSH/block-bound-hl-qpush-status-001.asl52fcbd3bb101d968ffee71f1922497da5fc88f676b68f52a38fe8b9fde8cf826PTO-EVIDENCE-RELEASE-TRACEABILITYPTO-EVIDENCE-RELEASE-TRACEABILITYspec/evidence/release-traceability-readiness.jsonc7327021d39dc67ac5564bc55073b3870a397d79ac8d9648284d56e33bc14a3ePTO-EVIDENCE-INSTRUCTION-CONTRACT-CLOSUREPTO-EVIDENCE-INSTRUCTION-CONTRACT-CLOSUREspec/evidence/instruction-contract-closure.json3ef2bb62421c79dff8fa77a1c7983923b523244b8090812883ef81286ca8106aPTO-EVIDENCE-ARCHITECTURE-READINESSPTO-EVIDENCE-ARCHITECTURE-READINESSspec/evidence/architecture-readiness.json4b0b85199101251bea744e0f3591cc31906909dc80d5ab651c417a936036a004PTO-EVIDENCE-RELEASE-GATE-READINESSPTO-EVIDENCE-RELEASE-GATE-READINESSspec/evidence/release-gate-readiness.jsona0f4d2b6920c08981ea55fd8ef820708a40d4feb5402c5150e8e9ab532d84ce0PTO-EVIDENCE-RELEASE-MANIFESTPTO-EVIDENCE-RELEASE-MANIFESTspec/release-manifest.json1a64c109ed7a90351c41e2a418b3c0ebaf8ad975838986d2101385186b85c0d8Loading ADR-0032…
ADR-0032docs/status/decisions/0032-bundle-command-totality-and-profile-boundaries.mde1f91826817343c0977a565a91e495a15397b83fa2af227124f225821ffa54aeLoading ADR-0052…
ADR-0052docs/status/decisions/0052-direct-tile-and-bundle-catalog-closure.md5fdb38bf480e37affe5075f93b35a57d32803018c986bfe05160f188a19ccaf6Loading ADR-0059…
ADR-0059docs/status/decisions/0059-mnemonic-field-encoding-closure.mdf18d13f735cfaf9f2803c754c5818f4af33d1cc42c489f0d9ce060b07bb3a196Loading ADR-0084…
ADR-0084docs/status/decisions/0084-scalar-system-and-queue-operations.mde068992fa81e2c4ac46e492391a2f784141d68e041bf0b9e0586c37217d1e08c{
"classification": [
"lifecycle"
],
"documentation": "docs/block/lifecycle/HL.QPUSH.md",
"id": "PTO-BLOCK-HL-QPUSH",
"instruction_contract": {
"artifact": "spec/evidence/instruction-contract-closure.json",
"mnemonic": "HL.QPUSH",
"ndf_clause": "PTO-INST-BLOCK-HL-QPUSH"
},
"mnemonic": "HL.QPUSH",
"readiness_subjects": [
"ADR-0032",
"ADR-0052",
"ADR-0059",
"ADR-0084"
],
"semantic_tests": [
"PTO-AVS-BLOCK-HL-QPUSH-ORDER-001",
"PTO-AVS-BLOCK-HL-QPUSH-STATUS-001"
],
"source": "asl/block/lifecycle/HL.QPUSH.asl",
"surface": "block",
"tests": [
"PTO-AVS-BLOCK-HL-QPUSH-DECODE-001",
"PTO-AVS-BLOCK-HL-QPUSH-ORDER-001",
"PTO-AVS-BLOCK-HL-QPUSH-STATUS-001"
]
}0.58.5 · 候选发布7dc8b7e5b121d2b2499a2273bebff29e2cd868127eacde3838de2f920447cb725e4c7e122362da7ff5ce36dfd474701d4f9da11c7599e59dea7404d7f6d633d5775f0c0bc271ac9844f10d84de287ed049bbc197asl/block/lifecycle/HL.QPUSH.aslasl/block/lifecycle/HL.QPUSH.aslasl/block/lifecycle/HL.QPUSH.asl