Operands and parameters
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| Field | Bits | Signedness | Architectural role | Encoded zero |
|---|---|---|---|---|
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 and Operation come directly from the instruction owner and remain separated by execution phase.
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 is a standalone General Queue Management command whose queue update, status result, and optional event are one ordered instruction effect.
HL.QPUSH executes as a standalone 48-bit command and does not require placement inside a BSTART/BSTOP body.
The accepted carrier uses the HL48 encoding class and resolves every displayed field before the command reads bindings or changes state.
The command snapshots every required source before its first visible effect, then follows the owner-defined commit or restart boundary.
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.Source validation and snapshot precede every register, queue, frame, memory, event, or control-flow effect.
The command publishes its state and result as one ordered instruction effect, then advances or transfers control as defined by the owner.
Fixed bits, reserved values, selector domains, and required Block placement are checked before architectural effects.
The current owner reports invalid schema, state, address, or continuation conditions through Fault_IllegalInstruction; no prose on this page creates an additional fault rule.
Rejection occurs before effects unless the current owner explicitly defines a restart boundary with retained progress; completion order remains the ASL order.
This example demonstrates placement and carrier flow only; exact behavior remains in the current ASL and instruction contract.
hl.qpush a0, a1, ->a2The shown accepted spelling resolves its fields from the current carrier, snapshots required sources, and then follows the owner-defined state and ordering transition.
Bodies come from owning ASL. Dragging or buttons change only this page-session view order.
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 · Release candidate7dc8b7e5b121d2b2499a2273bebff29e2cd868127eacde3838de2f920447cb725e4c7e122362da7ff5ce36dfd474701d4f9da11cb722484830ed08d96ccda6309b7f990577c58663a7da0ccfa2a74ffa43e9c66casl/block/lifecycle/HL.QPUSH.aslasl/block/lifecycle/HL.QPUSH.aslasl/block/lifecycle/HL.QPUSH.asl