Bug-fix batch

compiler/ir/src/main/scala/dfhdl/compiler/analysis/DFValAnalysis.scala

@@ -32,6 +32,43 @@ object Ident:
     if (alias.hasTagOf[IdentTag]) Some(alias.relValRef.get)
     else None
 
+extension (member: DFMember)
+  // The kind-level half of the unreferenced-anonymous sweeps: whether this member MAY be
+  // dropped when nothing reads it. SHARED by the `DropUnreferencedAnons` compiler stage and
+  // elaboration's end-of-design sweep (`DesignContext.sweepUnreadAnons`), so the two can never
+  // drift. The "is it read" half is deliberately NOT shared: the stage asks
+  // `originMembers.isEmpty` on the immutable DB, while the elaboration sweep computes
+  // reachability over `getRefs` on the mutable snapshot (where origin tracking is not final).
+  def isDroppableIfUnread(using MemberGetSet): Boolean = member match
+    // conditional headers can be values (referenced by nothing, driven per branch)
+    case _: DFConditional.Header => false
+    // idents are always kept
+    case Ident(_) => false
+    // a procedural (Unit-return) method call is a statement: referenced by nothing,
+    // dropped by nothing
+    case DFVal.Func.Call(call, _) if call.dfType =~ DFUnit => false
+    // a declaration is a PLACE, not an expression: an anonymous dcl must survive the
+    // elaboration sweep so the elaboration check can REJECT it ("anonymous port/var
+    // declarations are forbidden"), and unreferenced named dcls belong to
+    // `DropUnreferencedVars`. No change for the stage: post-check DBs hold no anonymous dcls.
+    case _: DFVal.Dcl => false
+    case dfVal: DFVal => dfVal.isAnonymous
+    case _: DFRange   => true
+    case _            => false
+end extension
+
+extension (dfVal: DFVal)
+  // Dereferences type-preserving `AsIs` wrappers (idents and other identity casts) down to the
+  // first value of a different shape. SHARED by `IntExprCalc.Calc.strip` and `SimplifyFunc`'s
+  // structural comparisons, so simplifications see through `Ident(a)` to `a` (a named ident is
+  // value-identical to what it wraps).
+  @tailrec def stripTypePreservingAliases(using MemberGetSet): DFVal = dfVal match
+    case alias: DFVal.Alias.AsIs =>
+      val relVal = alias.relValRef.get
+      if (alias.dfType == relVal.dfType) relVal.stripTypePreservingAliases
+      else alias
+    case _ => dfVal
+
 //A design parameter is an as-is alias that:
 //1. has `DesignParamTag` tag
 //TODO: This is not yet working. more complicated than initially thought.

compiler/ir/src/main/scala/dfhdl/compiler/ir/ConnectToMap.scala

@@ -16,19 +16,27 @@ object ConnectToMap:
   extension (ctm: ConnectToMap)(using MemberGetSet)
     def connectToVals: Set[ConnectToVal] = ctm.keySet
 
-    /** All nets whose slice overlaps `slice` on `dcl`, including ones whose overlap status is
-      * merely `Unknown` (conservative).
+    /** All nets whose slice overlaps `slice` on `connectToVal`, each with its overlap verdict:
+      * `Tri.Yes` for a proven overlap, `Tri.Unknown` when the relation could not be proven either
+      * way (conservatively included). Provably disjoint nets are excluded.
       */
-    def getNets(connectToVal: ConnectToVal, slice: Slice): Set[DFNet] =
+    def getNetsVerdicts(connectToVal: ConnectToVal, slice: Slice): Vector[(DFNet, Tri)] =
       ctm.get(connectToVal) match
         case Some(entry) =>
           val widthOpt = connectToVal.widthIntOpt
-          entry.nets.collect {
-            case (storedSlice, net)
-                if ConnectToMap.overlapsSlices(storedSlice, slice, widthOpt) != Tri.No =>
-              net
-          }.toSet
-        case None => Set.empty
+          entry.nets.view
+            .map { (storedSlice, net) =>
+              (net, ConnectToMap.overlapsSlices(storedSlice, slice, widthOpt))
+            }
+            .filter(_._2 != Tri.No)
+            .toVector
+        case None => Vector.empty
+
+    /** All nets whose slice overlaps `slice` on `dcl`, including ones whose overlap status is
+      * merely `Unknown` (conservative).
+      */
+    def getNets(connectToVal: ConnectToVal, slice: Slice): Set[DFNet] =
+      getNetsVerdicts(connectToVal, slice).view.map(_._1).toSet
     def getNets(dfVal: DFVal): Set[DFNet] =
       dfVal.departialPBNS match
         case Some(connectToVal, slice) => getNets(connectToVal, slice)
@@ -62,7 +70,7 @@ object ConnectToMap:
   /** Pairwise slice-overlap predicate used by `getNets`. Returns `Tri.Yes` only when provably
     * overlapping, `Tri.No` only when provably disjoint, `Tri.Unknown` otherwise.
     */
-  private def overlapsSlices(a: Slice, b: Slice, widthOpt: Option[Int]): Tri =
+  private def overlapsSlices(a: Slice, b: Slice, widthOpt: Option[Int])(using MemberGetSet): Tri =
     (a, b) match
       case (Slice.Concrete(ra), Slice.Concrete(rb)) =>
         if (ra.intersect(rb).nonEmpty) Tri.Yes else Tri.No
@@ -71,5 +79,40 @@ object ConnectToMap:
       case (Slice.Full, Slice.Concrete(r)) =>
         if (r.isEmpty) Tri.No else Tri.Yes
       case (Slice.Full, Slice.Full) => Tri.Yes
-      case _                        => Tri.Unknown
+      // a symbolic slice is a valid (nonempty) selection, so it always overlaps the full value
+      case (_: Slice.Symbolic, Slice.Full) | (Slice.Full, _: Slice.Symbolic) => Tri.Yes
+      case (Slice.Symbolic(loA, wA), Slice.Symbolic(loB, wB))                =>
+        symbolicOverlap(loA, wA, loB, wB)
+      case (Slice.Symbolic(loA, wA), Slice.Concrete(rb)) =>
+        import IntExprCalc.DataCalc.const
+        symbolicOverlap(loA, wA, const(rb.start), const(rb.length))
+      case (Slice.Concrete(ra), Slice.Symbolic(loB, wB)) =>
+        import IntExprCalc.DataCalc.const
+        symbolicOverlap(const(ra.start), const(ra.length), loB, wB)
+      case _ => Tri.Unknown
+
+  /** Overlap of `[loA, loA + wA)` and `[loB, loB + wB)` decided on the linear forms, for every
+    * valid parameter assignment. The slice widths serve as the `>= 1` facts for the inequality
+    * proofs (see [[IntExprCalc.DataCalc.proveNonNeg]]).
+    */
+  private def symbolicOverlap(
+      loA: IntExprCalc.Linear,
+      wA: IntExprCalc.Linear,
+      loB: IntExprCalc.Linear,
+      wB: IntExprCalc.Linear
+  )(using MemberGetSet): Tri =
+    import IntExprCalc.DataCalc.*
+    val facts = List(wA, wB)
+    def nonNeg(e: IntExprCalc.Linear): Boolean = proveNonNeg(e, facts)
+    // disjoint when one slice provably ends before the other begins:
+    // hiA < loB  <=>  loB - loA - wA >= 0 (and symmetrically)
+    if (nonNeg(sub(sub(loB, loA), wA)) || nonNeg(sub(sub(loA, loB), wB))) Tri.No
+    // overlapping when each slice provably begins no later than the other ends:
+    // loB <= hiA  <=>  loA + wA - 1 - loB >= 0 (and symmetrically)
+    else if (
+      nonNeg(addConst(sub(add(loA, wA), loB), -1)) &&
+      nonNeg(addConst(sub(add(loB, wB), loA), -1))
+    ) Tri.Yes
+    else Tri.Unknown
+  end symbolicOverlap
 end ConnectToMap

compiler/ir/src/main/scala/dfhdl/compiler/ir/Coverage.scala

@@ -6,19 +6,26 @@ import scala.collection.immutable
   * [[DFMember.departial]] to describe which bits of the underlying declaration an alias chain
   * touches.
   *
-  * The representation is deliberately conservative: when a slice's endpoints depend on a design
-  * parameter, we fall back to [[Slice.Unknown]] rather than attempting symbolic interval
-  * arithmetic.
+  * Parameter-dependent endpoints are kept as [[Slice.Symbolic]] linear forms (see
+  * [[IntExprCalc.DataCalc]]), so provably-disjoint parametric slices are recognized as such;
+  * [[Slice.Unknown]] remains the conservative fallback when the bounds cannot be linearized.
   */
 enum Slice derives CanEqual:
   /** A concrete bit range in the root value's coordinates. */
   case Concrete(range: Range)
 
+  /** A bit range `[lo, lo + width)` whose endpoints are linear forms over unresolved (top-design)
+    * parameters, in the root value's coordinates. Constructed only via [[Slice.symbolic]], so at
+    * least one of the two forms is non-constant.
+    */
+  case Symbolic(lo: IntExprCalc.Linear, width: IntExprCalc.Linear)
+
   /** The entire value. Used when the value's width itself is symbolic. */
   case Full
 
   /** A slice whose endpoints are symbolic and could not be resolved. */
   case Unknown
+end Slice
 
 object Slice:
   def fromRange(range: Range): Slice = Concrete(range)
@@ -28,23 +35,46 @@ object Slice:
     case Some(w) => Concrete(0 until w)
     case None    => Full
 
+  /** Build a symbolic slice, collapsing to [[Concrete]] when both forms are constant. */
+  def symbolic(lo: IntExprCalc.Linear, width: IntExprCalc.Linear): Slice =
+    if (lo.terms.isEmpty && width.terms.isEmpty)
+      Concrete(lo.offset until lo.offset + width.offset)
+    else Symbolic(lo, width)
+
+  /** Map an outer selection `outer` (relative to an alias whose selected region starts at bit
+    * `loBits` of the relative value and spans `selWidthBits` bits) into the relative value's
+    * coordinates.
+    */
+  def compose(outer: Slice, loBits: IntExprCalc.Linear, selWidthBits: IntExprCalc.Linear)(using
+      MemberGetSet
+  ): Slice =
+    import IntExprCalc.DataCalc.{add, const}
+    outer match
+      case Concrete(r)     => symbolic(add(loBits, const(r.start)), const(r.length))
+      case Symbolic(lo, w) => symbolic(add(lo, loBits), w)
+      case Full            => symbolic(loBits, selWidthBits)
+      case Unknown         => Unknown
+
   extension (slice: Slice)
     /** Shift the slice by a (concrete) delta in bit positions. Unknown/Full stay themselves —
       * shifting an unknown slice is still unknown.
       */
     def shift(delta: Int): Slice = slice match
-      case Concrete(r) => Concrete(Range(r.start + delta, r.end + delta))
-      case other       => other
+      case Concrete(r)     => Concrete(Range(r.start + delta, r.end + delta))
+      case Symbolic(lo, w) => Symbolic(lo.copy(offset = lo.offset + delta), w)
+      case other           => other
     def isEmpty: Boolean = slice match
-      case Concrete(r) => r.isEmpty
-      case _           => false
+      case Concrete(r)    => r.isEmpty
+      case Symbolic(_, w) => w.terms.isEmpty && w.offset <= 0
+      case _              => false
 
     /** Does this slice cover the full width of the underlying value? `Tri.Unknown` when either the
       * slice or the width is symbolic.
       */
     def isFullOf(widthOpt: Option[Int]): Tri = slice match
       case Full        => Tri.Yes
       case Unknown     => Tri.Unknown
+      case _: Symbolic => Tri.Unknown
       case Concrete(r) =>
         widthOpt match
           case Some(w) => if (r.start == 0 && r.end == w) Tri.Yes else Tri.No
@@ -64,9 +94,9 @@ object Tri:
 /** Accumulated write coverage over one DFVal.
   *
   *   - `bits` holds the concretely-tracked bit positions that are proven assigned/connected.
-  *   - `unknownTouched` is set when a write with a [[Slice.Unknown]] or a [[Slice.Full]] over an
-  *     unknown width has been observed, meaning we know the value was touched but not precisely
-  *     where.
+  *   - `unknownTouched` is set when a write with a [[Slice.Unknown]], a [[Slice.Symbolic]], or a
+  *     [[Slice.Full]] over an unknown width has been observed, meaning we know the value was
+  *     touched but not precisely where.
   *   - `fullyCovered` is a latch flag set when we observe a write that covers the entire value,
   *     even if the value's width is symbolic (so we cannot represent it as a concrete BitSet). Once
   *     set, any coverage query returns `Yes` regardless of `bits`.
@@ -97,7 +127,8 @@ final case class Coverage(
         widthOpt match
           case Some(w) => copy(bits = bits ++ immutable.BitSet.fromSpecific(0 until w))
           case None    => copy(fullyCovered = true)
-      case Slice.Unknown => copy(unknownTouched = true)
+      // a symbolic slice has no concrete bit positions to track, so it degrades to "touched"
+      case _: Slice.Symbolic | Slice.Unknown => copy(unknownTouched = true)
 
   /** Does this coverage touch any bit of `slice`? */
   def overlaps(slice: Slice, widthOpt: Option[Int]): Tri =
@@ -116,7 +147,7 @@ final case class Coverage(
           if (bits.nonEmpty) Tri.Yes
           else if (unknownTouched) Tri.Unknown
           else Tri.No
-        case Slice.Unknown =>
+        case _: Slice.Symbolic | Slice.Unknown =>
           if (bits.nonEmpty || unknownTouched) Tri.Unknown
           else Tri.No
 
@@ -139,7 +170,7 @@ final case class Coverage(
               else Tri.No
             case None =>
               if (unknownTouched) Tri.Unknown else Tri.No
-        case Slice.Unknown => Tri.Unknown
+        case _: Slice.Symbolic | Slice.Unknown => Tri.Unknown
 
   /** Is this coverage full for the given (possibly unknown) width? */
   def isFull(widthOpt: Option[Int]): Tri = contains(Slice.Full, widthOpt)

compiler/ir/src/main/scala/dfhdl/compiler/ir/DB.scala

@@ -611,7 +611,8 @@ final case class DB private (
         toValAndSliceOption match
           // found target variable or port declaration for the given connection/assignment
           case Some(connectToVal, slice) =>
-            val prevNets = connToMap.getNets(connectToVal, slice)
+            val prevNetsVerdicts = connToMap.getNetsVerdicts(connectToVal, slice)
+            val prevNets = prevNetsVerdicts.view.map(_._1).toSet
             // checking multiple assignments from different domains, except for a condition
             // where the declaration is a shared variable.
             // this is used to define a shared variable which is against the RT model,
@@ -620,22 +621,34 @@ final case class DB private (
               case dcl: DFVal.Dcl if dcl.modifier.isShared => true
               case _                                       => false
             if (!isSharedVar)
-              prevNets.headOption.foreach: prevNet =>
+              prevNetsVerdicts.headOption.foreach: (prevNet, _) =>
                 if (prevNet.getOwnerDomain != net.getOwnerDomain)
                   newError(
                     s"""|Found multiple domain assignments to the same variable/port `${connectToVal.getFullName}`.
                         |Only variables declared as `VAR.SHARED` under ED domain allow this.
                         |The previous write occurred at ${prevNet.meta.position}""".stripMargin
                   )
             // go through all previous nets and check for collisions
-            prevNets.foreach: prevNet =>
+            prevNetsVerdicts.foreach: (prevNet, verdict) =>
               // multiple assignments are allowed in the same range, but not multiple
               // connections or a combination of an assignment and a connection
               if (prevNet.isConnection || prevNet.isAssignment && !net.isAssignment)
-                newError(
-                  s"""Found multiple connections write to the same variable/port `${connectToVal.getFullName}`.
-                     |The previous write occurred at ${prevNet.meta.position}""".stripMargin
-                )
+                if (verdict == Tri.Yes)
+                  newError(
+                    s"""Found multiple connections write to the same variable/port `${connectToVal.getFullName}`.
+                       |The previous write occurred at ${prevNet.meta.position}""".stripMargin
+                  )
+                // the slices could not be proven overlapping NOR disjoint (parameter-dependent
+                // indices the slice calculus cannot relate), so the write is conservatively
+                // rejected with an error that names the actual problem
+                else
+                  newError(
+                    s"""|Found a write to the same variable/port `${connectToVal.getFullName}` that cannot be proven to be
+                        |disjoint from a previous write, because their parameter-dependent bit ranges could not be
+                        |resolved. If the ranges never overlap, restructure their indexing so the compiler can relate
+                        |them, or use assignments within a process instead of connections.
+                        |The previous write occurred at ${prevNet.meta.position}""".stripMargin
+                  )
             // if no previous connection in this range, we add it to the range map
             if (prevNets.isEmpty)
               getConnToMap(
@@ -1670,19 +1683,62 @@ final case class DB private (
   //   * Rule 4: a loop containing an RT-domain shared-variable write moves whole into the
   //     clocked process, so all its content must be sequential-sink writes with settled
   //     reads; otherwise the loop must be split.
+  // The process block a member statement resides in, if any (walks out of nested
+  // conditional/step blocks; a domain owner boundary means the member is not in a process).
+  @tailrec private def ownerProcessOpt(member: DFMember): Option[ProcessBlock] =
+    member.ownerRef.get match
+      case pb: ProcessBlock => Some(pb)
+      case _: DFDomainOwner => None
+      case owner: DFBlock   => ownerProcessOpt(owner)
+      case _                => None
+
+  // A variable (or any part of it) written with both a blocking (`:=`) and a non-blocking
+  // (`:==`) assignment inside the same process commits at two different times, which is a
+  // semantic contradiction; the generated HDL then mixes `=`/`<=` on one variable inside a
+  // single process, which downstream tools reject (issue #446). The rule is per declaration
+  // and per process: which parts are assigned is irrelevant, and a consistently-assigned
+  // variable is fine with either kind (a blocking-assigned temporary in a clocked process
+  // is legitimate; see DropBAssignFromSeqProc). Shared variables are excluded, since their
+  // writes are already restricted to `:==` at compile time.
+  def mixedAssignKindCheck(): Unit =
+    val errors = collection.mutable.ArrayBuffer[String]()
+    val firstNets = collection.mutable.Map.empty[(ProcessBlock, DFVal.Dcl), DFNet]
+    val reported = collection.mutable.Set.empty[(ProcessBlock, DFVal.Dcl)]
+    members.foreach {
+      case net @ DFNet.Assignment(toVal, _) =>
+        toVal.departialDcl match
+          case Some((dcl, _)) if !dcl.modifier.isShared =>
+            ownerProcessOpt(net).foreach { pb =>
+              val key = (pb, dcl)
+              firstNets.get(key) match
+                case Some(prevNet) =>
+                  if (prevNet.op != net.op && !reported.contains(key))
+                    reported += key
+                    errors +=
+                      s"""|DFiant HDL connectivity error!
+                          |Position:  ${net.meta.position}
+                          |Hierarchy: ${net.getOwnerDesign.getFullName}
+                          |LHS:       ${printer.csDFValRef(net.lhsRef.get, net.getOwnerDesign)}
+                          |RHS:       ${printer.csDFValRef(net.rhsRef.get, net.getOwnerDesign)}
+                          |Message:   Found both blocking (`:=`) and non-blocking (`:==`) assignments to the same variable/port `${dcl.getFullName}` within the same process.
+                          |Use one assignment kind consistently for this variable inside the process.
+                          |The previous write occurred at ${prevNet.meta.position}""".stripMargin
+                case None => firstNets(key) = net
+            }
+          case _ =>
+      case _ =>
+    }
+    if (errors.nonEmpty)
+      throw new IllegalArgumentException(errors.mkString("\n\n"))
+  end mixedAssignKindCheck
+
   def sharedVarCheck(): Unit =
     val errors = collection.mutable.ArrayBuffer[String]()
     def memberError(member: DFMember, msg: String): Unit =
       errors += s"""|DFiant HDL shared variable error!
                     |Position:  ${member.meta.position}
                     |Hierarchy: ${member.getOwnerDesign.getFullName}
                     |Message:   $msg""".stripMargin
-    @tailrec def ownerProcessOpt(member: DFMember): Option[ProcessBlock] =
-      member.ownerRef.get match
-        case pb: ProcessBlock => Some(pb)
-        case _: DFDomainOwner => None
-        case owner: DFBlock   => ownerProcessOpt(owner)
-        case _                => None
     members.foreach { m =>
       // Rule 1: a write to a shared variable inside a `process(all)`
       m match
@@ -2031,6 +2087,7 @@ final case class DB private (
     condExprNamedValCheck()
     blockScopeCheck()
     sharedVarCheck()
+    mixedAssignKindCheck()
 
   // Whole-tree checks, run once on the root: the cross-design connectivity /
   // RT-domain / device-top checks, via the `*` clones that navigate the