spec: DVRM chip

[erik-3milabs]

This PR introduces the DVRM chip.

Note: this PR additionally widens the ZERO lookup from 16 to 20 bits. (see 582bc35)

[erik-3milabs]

Perhaps 8652c0f and c8d6896 should be merged separately?

[RobinJadoul]

Probably 5c983c9 rather than 8652c0f, but yeah, that could make sense

[erik-3milabs]

@greptileai

[greptile-apps]

Greptile Overview

Greptile Summary

This PR introduces the DVRM chip for division and remainder operations supporting both signed and unsigned 64-bit integers (DIV[U][W] and REM[U][W] instructions).

Key Changes

• New DVRM chip specification (spec/dvrm.typ): Comprehensive 143-line documentation explaining how the chip enforces all five ISA requirements for division/remainder operations, including proper handling of division-by-zero and overflow edge cases
• DVRM chip configuration (spec/src/dvrm.toml): Complete 380-line TOML defining 14 variables (inputs, outputs, auxiliary, virtual) and 24 constraints organized into 7 constraint groups
• ZERO lookup expansion (spec/src/bitwise.toml): Widened from 16-bit to 20-bit by adding Z component (X + 256*Y + 65536*Z), required for the DVRM overflow detection constraint
• Documentation updates (spec/bitwise.typ): Updated optimization notes to reflect ZERO now appears in both 16-bit and 20-bit lookup tables
• Cross-reference support (spec/chip.typ): Added lbl() function to enable labeled references for variables in generated tables
• Assumption labeling (spec/src/mul.toml): Added ref = "mul:a:rhs" to enable DVRM to reference this assumption

Technical Implementation

The DVRM chip correctly implements ISA requirements through:

• R1: Verifies n = qd + r using MUL chip with 128-bit arithmetic
• R2: Ensures rounding toward zero via |r| < |d| check using LT chip
• R3: Enforces remainder sign matches numerator sign
• R4: Handles division-by-zero (q = -1, r = n)
• R5: Handles overflow case (n = -2^63, d = -1)

The overflow detection uses a clever zero-sum check that requires exactly 20 bits (max sum = 458,746 < 2^19), justifying the ZERO lookup expansion.

Confidence Score: 4/5

• This PR is safe to merge with minor documentation corrections needed
• The implementation is mathematically sound with proper constraint definitions and the ZERO lookup expansion is correctly sized. Two minor documentation typos were found (incorrect reference label and requirement number mismatch) but these don't affect the actual implementation logic
• spec/dvrm.typ needs documentation fixes for reference labels and requirement numbering

Important Files Changed

Filename	Overview
spec/dvrm.typ	New comprehensive specification for DVRM chip implementing DIV/REM operations with signed/unsigned support and proper edge case handling
spec/src/dvrm.toml	Complete DVRM chip configuration with variables, constraints, and ISA requirement implementations

Sequence Diagram

sequenceDiagram
    participant CPU as CPU Chip
    participant DVRM as DVRM Chip
    participant MUL as MUL Chip
    participant SUB as SUB Chip
    participant BITWISE as BITWISE Chip
    participant LT as LT Chip
    
    CPU->>DVRM: DIV/REM request (n, d, signed)
    
    Note over DVRM: Compute sign flags
    DVRM->>BITWISE: SIGN<n[3], signed> → sign_n
    DVRM->>BITWISE: SIGN<d[3], signed> → sign_d
    DVRM->>BITWISE: SIGN<r[3], signed> → sign_r
    
    Note over DVRM: Check edge cases
    DVRM->>BITWISE: ZERO[d] → div_by_zero
    DVRM->>BITWISE: ZERO[overflow_sum] → overflow
    
    Note over DVRM: Compute absolute values
    alt sign_r = 1
        DVRM->>SUB: SUB<0, r> → abs_r
    end
    alt sign_d = 1
        DVRM->>SUB: SUB<0, d> → abs_d
    end
    
    Note over DVRM: Verify |r| < |d|
    DVRM->>LT: LT<abs_r, abs_d, 0> → !div_by_zero
    
    Note over DVRM: Verify n = qd + r
    DVRM->>SUB: SUB<n, r> → n_sub_r
    DVRM->>MUL: MUL<d, signed, q, sign_q, 0> → n_sub_r[lower]
    DVRM->>MUL: MUL<d, signed, q, sign_q, 1> → n_sub_r[upper]
    
    DVRM-->>CPU: Return (q, r)

Loading

[greptile-apps]

_{2 files reviewed, 2 comments}

_{Edit Code Review Agent Settings | Greptile}

[RobinJadoul]

I will definitely suggest a manual rebase -i and merge here, rather than a full squash, to keep #280 its own commit if it gets merged in here.

[erik-3milabs]

I will definitely suggest a manual rebase -i and merge here, rather than a full squash, to keep #280 its own commit if it gets merged in here.

I'm slating #280 to merge into this as a "chained" PR; this PR should be merged first, after which #280 will update to be based against spec/main. The reason I'm pointing #280 against this, is that I can use some of things here in there.
Once this PR is merged, I'll rebase the few left-over commits on #280 against spec/main.

[RobinJadoul]

Seems like #280 landed before this one to stay as separate history against spec/main :)

[RobinJadoul]

Nitpick: this could just be a single Half, or even integrated into extended_n_sub_r like we do for extended_n and extended_r

[erik-3milabs]

the reason it exists separately, is that we need it inside the second MUL lookup. And slicing was not going to be an option, really.

[erik-3milabs]

Seems like #280 landed before this one to stay as separate history against spec/main :)

yeah.. my bad

[erik-3milabs]

This was manually merged into spec/main; closing it now

[greptile-apps]

No reviewable files after applying ignore patterns.