Repository navigation
v4 T-4.9: model extdeps/languages/verilog.dag — HW concurrency as 5 behaviors (IN-B probe PASS) - #3177
Closed
briansrls wants to merge 1 commit into
Closed
v4 T-4.9: model extdeps/languages/verilog.dag — HW concurrency as 5 behaviors (IN-B probe PASS)#3177briansrls wants to merge 1 commit into
briansrls wants to merge 1 commit into
Conversation
…ehaviors (IN-B probe PASS)
IN-B probe RESULT: PASS — Verilog hardware concurrency models cleanly
under the existing five L1 behaviors with NO 6th `Concurrent` behavior
and NO core/pipeline change. The probe surfaces the structurally-
correct intra-vs-cross-program partition: intra-program HW concurrency
(parallel always-blocks / continuous assigns within one module) is the
Conj-of-parallel-siblings + Bind-chain-within-always shape, with per-
language effect-typing intrinsic to the wire/reg/vector signal type;
cross-program coordination (Endpoint/DeploymentUnit/messaging) is a
distinct concern owned by extdeps/coordination.dag (T-4.8).
Declares closed-Disj coproducts (each with full 5-pattern Practice-4
ledger — Fact-placement / Variant-is-data / Algebraic-form / Dimensional
/ Parameterized-family-Practice-7 per modeling-discipline.md §4):
PortDirection, NetType, VariableType, EdgeTrigger,
ProceduralAssignKind, PackingShape, ModuleItem. Conj records (no
ledger): VectorRange (🟡 scaffold), NetDeclaration, VariableDeclaration,
PortDeclaration, ParameterDeclaration, SensitivityItem,
ContinuousAssign, AlwaysBlock, InitialBlock, PortConnection,
ModuleInstance, VerilogModule, VerilogCost (🟡 scaffold).
DEFERRED with named-owner+trigger (do not author, do not improvise):
- emit/parse ops ride D1 Outcome<T> (Produced{value:T}|Rejected{...})
when ratified in std/diagnostic.dag (v4 value-or-Diagnostic STOP
surfaced by T-4.6 keen-wren-419).
- Bit-vector inhabitance (Semiring<UInt<N>> / OrderedRing<Int<N>>) rides
pending D2 instance-value form (PR #3171's worker pushback precedent).
- Expression sub-grammar (RHS of assign, procedural-statement bodies,
control-flow conditions) ride the T-4 LanguageModel bundle; verbatim
String lexemes carry the textual surface in the interim (spice.dag
SpiceValue.lexeme precedent).
Scaffold-header Consumes line preserved verbatim with surfaced staleness
(primitive.dag deleted PR #3152; coordination.dag is an unfilled scaffold
modeling cross-program coordination — a different concern from intra-
program HW concurrency). The systemic per-file Consumes reconciliation
is pending operator ratification (T-4 mgr synthesis msg_1fddb75c).
Verification: `v2-compiler compile --source-root src/v4 --target dag`
= 63 modules / 0 diagnostics.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Duplicate — dashboard-tracked PR is #3176 (same branch). Consolidating to that one. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Concurrentbehavior and NO core/pipeline change. The probe was authored to falsify the IN-B claim (concurrency = Bind composition + effect typing, no behavior extension); it surfaces the structurally-correct intra-vs-cross-program partition along the way — intra-program HW concurrency (parallelalways-blocks within one module) is the Conj-of-parallel-siblings + Bind-chain shape with per-language effect-typing intrinsic to the wire/reg/vector signal type; cross-program coordination (Endpoint/DeploymentUnit/messaging) is a distinct concern owned byextdeps/coordination.dag(T-4.8).Consumesline preserved verbatim with surfaced staleness — primitive.dag deleted PR v4: decompose std/primitive.dag into six concept-anchored scalar files #3152; coordination.dag is an unfilled scaffold modeling a different concern. Pending the systemic per-file Consumes reconciliation (T-4 mgr synthesis msg_1fddb75c), uniform with ptx v4 T-4.14: model extdeps/languages/ptx.dag — SIMT-as-5-behaviors (B2-OMNI + IN-B probe, no STOP) #3170, spice v4 T-4.10: model extdeps/formats/spice.dag — Shape-B netlist (B2-OMNI probe ✓) #3168, llvm_ir T-4.12: model extdeps/languages/llvm_ir.dag — LLVM IR LanguageModel (B2-OMNI probe PASS) #3171.The IN-B mapping (member-by-member) lives in the modeling-notes "IN-B PROBE FINDING" section: module body ↦ Conj of parallel siblings; continuous assign ↦ Transform; always-block ↦ bounded Loop step + boundary-driven iteration (per node.dag A2 footnote); procedural statement sequence ↦ Bind; if/case ↦ Branch; signal declaration ↦ effect-typed value; module instance ↦ structural Conj child.
Test plan
v2-compiler compile --source-root src/v4 --target dag→ 63 modules / 0 diagnosticsScope/Owns/Stress/Clear winlines preserved verbatim; staleness surfaced inStatus, not silently rewritten (manager directive)parse/emitfunction bodies declared (D1 Outcome deferred)🤖 Generated with Claude Code