Operands and parameters
SrcL- Reg5 atomic address source
SrcR- Reg5 expected word source
SrcD- Reg5 desired word source
RegDst- Reg5 old-value destination
aq- acquire ordering bit
rl- release ordering bit
CASW atomically compares and conditionally replaces one word, then publishes the prior value.
PTO-SCALAR-CASWcasw [SrcL], SrcR, SrcD, ->Rdcasw.aq [SrcL], SrcR, SrcD, ->Rdcasw.rl [SrcL], SrcR, SrcD, ->Rdcasw.aqrl [SrcL], SrcR, SrcD, ->Rd| Field | Bits | Signedness | Architectural role | Encoded zero |
|---|---|---|---|---|
RegDst | 5 | encoding-defined | Reg5 old-value destination | Encoded zero discards the prior value. |
SrcD | 5 | encoding-defined | Reg5 desired word source | Encoded zero supplies numeric zero as the desired value. |
SrcL | 5 | encoding-defined | Reg5 atomic address source | Encoded zero reads the architectural zero register as the address. |
SrcR | 5 | encoding-defined | Reg5 expected word source | Encoded zero supplies numeric zero as the expected value. |
aq | 1 | encoding-defined | acquire ordering bit | Encoded zero disables acquire ordering. |
rl | 1 | encoding-defined | release ordering bit | Encoded zero disables release ordering. |
Loading WaveDrom diagram… The encoding table and WaveJSON remain available below.
| Decoded item | Bit range | Value |
|---|---|---|
| SrcD | 31:27 | variable |
| aq | 26 | variable |
| rl | 25 | variable |
| SrcR | 24:20 | variable |
| SrcL | 19:15 | variable |
| Constant | 14:12 | 3'b010 |
| RegDst | 11:7 | variable |
| Constant | 6:0 | 7'b0011011 |
{
"reg": [
{
"bits": 7,
"name": "7'b0011011"
},
{
"bits": 5,
"name": "RegDst"
},
{
"bits": 3,
"name": "3'b010"
},
{
"bits": 5,
"name": "SrcL"
},
{
"bits": 5,
"name": "SrcR"
},
{
"bits": 1,
"name": "rl"
},
{
"bits": 1,
"name": "aq"
},
{
"bits": 5,
"name": "SrcD"
}
],
"config": {
"bits": 32,
"fontsize": 13,
"hspace": 900,
"lanes": 1,
"offset": 0
}
}casw<.{aq, rl, aqrl}> [SrcL], SrcR, SrcD, ->{t, u, Rd}
SrcLSrcRSrcDRegDstaqrlThis Operation comes directly from the instruction owner; the page does not rewrite its behavior.
readonly func InstructionContractOperation_CASW() => ScalarOperationbegin return ScalarOperation_CASW;end;readonly func InstructionContractHandler_CASW() => ScalarSemanticHandlerbegin return ScalarHandler_CompareAndSwap;end;
pure func InstructionContractCompareSizeBytes_CASW() => integer {1,2,4,8}begin return 4;end;
pure func InstructionContractHasFarField_CASW() => booleanbegin return FALSE;end;
pure func InstructionContractZeroExtendsOldValue_CASW() => booleanbegin return FALSE;end;
pure func InstructionContractSignExtendsOldValue_CASW() => booleanbegin return TRUE;end;// PTO-INSTRUCTION: {"assembly":["casw [SrcL], SrcR, SrcD, ->Rd","casw.aq [SrcL], SrcR, SrcD, ->Rd","casw.rl [SrcL], SrcR, SrcD, ->Rd","casw.aqrl [SrcL], SrcR, SrcD, ->Rd"],"block":[],"catalog_indices":[53],"catalog_records":[{"asm":"casw<.{aq, rl, aqrl}> [SrcL], SrcR, SrcD, ->{t, u, Rd}","constraints":[],"encoding":[{"index":0,"mask":"0x0000707f","match":"0x0000201b","width_bits":32}],"encoding_kind":"L32","fields":[{"name":"RegDst","pieces":[{"instruction_lsb":7,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"SrcD","pieces":[{"instruction_lsb":27,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"SrcL","pieces":[{"instruction_lsb":15,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"SrcR","pieces":[{"instruction_lsb":20,"value_lsb":0,"width":5}],"signedness":"encoding-defined","width":5},{"name":"aq","pieces":[{"instruction_lsb":26,"value_lsb":0,"width":1}],"signedness":"encoding-defined","width":1},{"name":"rl","pieces":[{"instruction_lsb":25,"value_lsb":0,"width":1}],"signedness":"encoding-defined","width":1}],"form_id":"casw_32_cb29e4287223","length_bits":32,"mnemonic":"CASW","semantic_family":"AMO","semantic_group":"AMO","semantic_handler":"CompareAndSwap","semantic_summary":"CASW atomically compares and conditionally replaces one word, then publishes the prior value.","status":"accepted"}],"classification":["amo"],"contract":{"block_composition":["none"],"canonical_assembly":["casw [SrcL], SrcR, SrcD, ->Rd","casw.aq [SrcL], SrcR, SrcD, ->Rd","casw.rl [SrcL], SrcR, SrcD, ->Rd","casw.aqrl [SrcL], SrcR, SrcD, ->Rd"],"defaults":["SrcL, SrcR, SrcD, and RegDst are required Reg5 fields. Encoded source zero reads the architectural zero register; encoded destination zero discards the old value.","aq=0 and rl=0 select relaxed ordering. aq=1 selects acquire, rl=1 selects release, and aq=1 with rl=1 selects acquire-release.","The short form has no far field and therefore uses the default flat-address route."],"encoding_class":"standalone-encoded","examples":["casw [a0], a1, a2, ->a3","casw.aqrl [t#1], u#1, a0, ->u"],"exceptions":["The effective address must be aligned to 4 bytes. Alignment, read translation/permission, write translation/permission, and translated-address equality are checked before effects.","On a fault, no destination, memory write, event, reservation update, or TPC advance occurs. Trap entry saves the original TPC and recovery restores it for full reissue.","An undecodable fixed-bit pattern raises Fault_IllegalInstruction before effects. All explicit field values are assigned."],"field_contracts":{},"field_zero_meanings":{"RegDst":"Encoded zero discards the prior value.","SrcL":"Encoded zero reads the architectural zero register as the address.","SrcR":"Encoded zero supplies numeric zero as the expected value.","SrcD":"Encoded zero supplies numeric zero as the desired value.","aq":"Encoded zero disables acquire ordering.","rl":"Encoded zero disables release ordering."},"legality":["All 32 SrcL, SrcR, and SrcD Reg5 encodings are assigned: 0..23 select absolute GPRs, 24..27 select T#1..T#4, and 28..31 select U#1..U#4.","All 32 RegDst encodings are assigned. Code 0 and codes 24..29 discard, code 30 pushes U, code 31 pushes T, and codes 1..23 write the named absolute GPR.","All aq and rl combinations are assigned; the short form has implicit far zero.","The effective address must be aligned to 4 bytes."],"memory_effects":["After aligned read and write preflight identify the same translated location, atomically read one 4-byte word and compare it with SrcR truncated to 4 bytes.","On equality, store SrcD truncated to 4 bytes and set write_performed in the atomic event. On mismatch, preserve memory and emit an ordered atomic event with write_performed false.","Only a successful overlapping write invalidates the local 64-byte-line reservation; mismatch and nonoverlap preserve it.","The 32-bit old value is sign-extended to XLEN."],"operands":[{"field":"SrcL","role":"Reg5 atomic address source"},{"field":"SrcR","role":"Reg5 expected word source"},{"field":"SrcD","role":"Reg5 desired word source"},{"field":"RegDst","role":"Reg5 old-value destination"},{"field":"aq","role":"acquire ordering bit"},{"field":"rl","role":"release ordering bit"}],"ordering":["aq=0,rl=0 records relaxed ordering; aq=1,rl=0 acquire; aq=0,rl=1 release; aq=1,rl=1 acquire-release for both match and mismatch.","The short form always uses the default flat-address route."],"standalone_opcode":true,"state_effects":["Snapshot SrcL, SrcR, and SrcD before any memory or destination effect.","Publish the prior value after every nonfaulting match or mismatch; publish no value on fault.","The 32-bit old value is sign-extended to XLEN.","Successful execution advances TPC by 4 bytes. A fault saves and later restores the original TPC for full reissue."]},"depends_on":["PTO-BLOCK-MODEL-SCHEMA-PROFILE-ENCODING"],"id":"PTO-SCALAR-CASW","mnemonic":"CASW","summary":"CASW atomically compares and conditionally replaces one word, then publishes the prior value.","surface":"scalar"}// PTO-REVIEW: {"review_method":"formal-definition-read","outcome":"FORMAL-COMPLETE","reviewed_fields":["assembly","encoding","defaults","operation","state","memory","ordering","faults","reserved"]}// DOC-BEGIN: decodereadonly func InstructionContractOperation_CASW() => ScalarOperationbegin return ScalarOperation_CASW;end;// DOC-END: decode// DOC-BEGIN: operationreadonly func InstructionContractHandler_CASW() => ScalarSemanticHandlerbegin return ScalarHandler_CompareAndSwap;end;
pure func InstructionContractCompareSizeBytes_CASW() => integer {1,2,4,8}begin return 4;end;
pure func InstructionContractHasFarField_CASW() => booleanbegin return FALSE;end;
pure func InstructionContractZeroExtendsOldValue_CASW() => booleanbegin return FALSE;end;
pure func InstructionContractSignExtendsOldValue_CASW() => booleanbegin return TRUE;end;// DOC-END: operation
CASW atomically reads one aligned 4-byte word, compares it with an expected word, conditionally stores a desired word, and publishes the prior memory value after either a nonfaulting match or mismatch.
Before any effect, CASW snapshots the address source SrcL, expected source SrcR, and desired source SrcD, then completes alignment plus read/write translation and permission preflight for one translated location.
The comparison uses the low 4 bytes of SrcR. On equality, the instruction stores the low 4 bytes of SrcD; on mismatch, it preserves memory.
Both outcomes emit one ordered atomic event. A matching event records write_performed=true; a mismatching event records write_performed=false and acts as an ordered atomic read without a coherence write.
The prior 32-bit word is sign-extended to XLEN before destination publication.
SrcL, SrcR, and SrcD accept every Reg5 source selector, including non-consuming T/U sources; RegDst accepts every Reg5 destination or discard selector.aq=0,rl=0 selects relaxed ordering; aq=1,rl=0 acquire; aq=0,rl=1 release; and aq=1,rl=1 acquire-release.The short form has no far-address field and always uses the default flat-address route.
On a match, CASW writes the desired low word, emits one read/write atomic event, and invalidates an overlapping local 64-byte-line reservation.
On a mismatch, it leaves memory and the reservation unchanged while still emitting the ordered atomic read event.
Every nonfaulting outcome publishes the sign-extended prior word and advances TPC by 4 bytes; a fault publishes no destination.
The effective address must be aligned to 4 bytes. Alignment, read access, write access, and translated-address equality are checked before memory, destination, event, reservation, or TPC effects.
On fault, trap entry preserves the original TPC; recovery restores it so the complete instruction can be reissued without retained progress.
This walkthrough illustrates the current contract; it does not replace the atomic operation.
Suppose memory holds the word 0x80000001, the expected word matches, and the desired XLEN value is 0x1122334455667788. CASW.aqrl stores 0x55667788, publishes the prior word sign-extended to XLEN, emits one acquire-release atomic event with write_performed=true, and invalidates an overlapping reservation.
Bodies come from owning ASL. Dragging or buttons change only this page-session view order.
No NDF clause is attached to this unit.
12 matching entries
PTO-AVS-SCALAR-CASW-DECODE-001tests/asl/scalar/amo/CASW/scalar-decode-casw-canonical-001.asl7deeb16d563247120889d86b83eaf7bc19b65f69fcb945d9fe4b97be224c9680PTO-AVS-SCALAR-CASW-MATCH-001tests/asl/scalar/amo/CASW/scalar-exec-casw-match-001.aslce3332def899ceda7a6077d7ba67851b0d21b18e1cda82e51fc8105094d74b37PTO-AVS-SCALAR-CASW-MISMATCH-001tests/asl/scalar/amo/CASW/scalar-bound-casw-mismatch-001.asl527ffa7f74f901586d9fba0deb04a694cca7454d5caf5f1742c5caed4345bdd4PTO-AVS-SCALAR-CASW-PRECISE-001tests/asl/scalar/amo/CASW/scalar-fault-casw-precise-001.asl7d0a7bf4c9c97fa16aeb8521bf5ba8d1a42e4f42b67e132fb5e433c2921f124fPTO-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-0020…
ADR-0020docs/status/decisions/0020-production-memory-events-and-atomic-corners.md215b18f05d0b53120949373fce6a5ce22f7ab534fb22df24743a9b2b4beb2decLoading ADR-0030…
ADR-0030docs/status/decisions/0030-scalar-amo-totality-and-reservation.md110bd32b3004a8383913ac6053cc7d0a1d0b8e03e3ef7c47d83292c94a6a17ebLoading ADR-0059…
ADR-0059docs/status/decisions/0059-mnemonic-field-encoding-closure.mdf18d13f735cfaf9f2803c754c5818f4af33d1cc42c489f0d9ce060b07bb3a196{
"classification": [
"amo"
],
"documentation": "docs/scalar/amo/CASW.md",
"id": "PTO-SCALAR-CASW",
"instruction_contract": {
"artifact": "spec/evidence/instruction-contract-closure.json",
"mnemonic": "CASW",
"ndf_clause": "PTO-INST-SCALAR-CASW"
},
"mnemonic": "CASW",
"readiness_subjects": [
"ADR-0020",
"ADR-0030",
"ADR-0059"
],
"semantic_tests": [
"PTO-AVS-SCALAR-CASW-MATCH-001",
"PTO-AVS-SCALAR-CASW-MISMATCH-001",
"PTO-AVS-SCALAR-CASW-PRECISE-001"
],
"source": "asl/scalar/amo/CASW.asl",
"surface": "scalar",
"tests": [
"PTO-AVS-SCALAR-CASW-DECODE-001",
"PTO-AVS-SCALAR-CASW-MATCH-001",
"PTO-AVS-SCALAR-CASW-MISMATCH-001",
"PTO-AVS-SCALAR-CASW-PRECISE-001"
]
}0.58.5 · Release candidate7dc8b7e5b121d2b2499a2273bebff29e2cd8681257c46a9bcafdb175635163341792870b2bb42a960f81d4d8ac2fd0bc1f5eafd6383a3538fe0df2ee403baeddb9c753e9451abb041b3e03c1ac56463215c7984aasl/scalar/amo/CASW.aslasl/scalar/amo/CASW.asl