SNat output always 64-bits

[DigitalBrains1]

If you produce an SNat on an output port, it will always output 64 bits even if the number is larger:

topEntity ::
  SNat 70_000_000_000_000_000_000
topEntity = SNat
{-# OPAQUE topEntity #-}

generates Verilog:

module topEntity
    ( // No inputs
      // Outputs
      output wire [63:0] result
    );
  assign result = 64'd14659767778871345152;
endmodule

That's the number truncated to 64 unsigned bits.

I'd expect a 32-bit machine to produce 32 bits, by the way; mentioning this for completeness' sake.

[DigitalBrains1]

By the way, this specifically relates to having an SNat output port. The following code does produce the desired result:

topEntity :: Unsigned 66
topEntity = snatToNum (SNat @70_000_000_000_000_000_000)
{-# OPAQUE topEntity #-}

module topEntity
    ( // No inputs
      // Outputs
      output wire [65:0] result
    );
  assign result = 66'd70000000000000000000;
endmodule

[martijnbastiaan]

My guess is that this is because:

newtype SNat (n :: Nat) = UnsafeSNat_ Natural

I.e., Clash will just treat it as a Natural in its HWType (which are hardcoded to 64-bit numbers..).

[pieter-bos]

If we pretend that SNat has an NFDataX instance, you can also observe the truncating behaviour when storing an SNat:

module Test where

import Clash.Prelude

instance NFDataX (SNat n) where
  deepErrorX = undefined
  hasUndefined = undefined
  ensureSpine = undefined
  rnfX = undefined

topEntity :: HiddenClockResetEnable System => Signal System (Unsigned 66)
topEntity = snatToNum <$> state (SNat @70_000_000_000_000_000_000)

state s0 = mealy (\s _ -> (s, s)) s0 (pure ())

Generates:

/* AUTOMATICALLY GENERATED VERILOG-2001 SOURCE CODE.
** GENERATED BY CLASH 1.9.0. DO NOT MODIFY.
*/
`default_nettype none
`timescale 100fs/100fs
module topEntity
    ( // Inputs
      input wire  _$dCTuple3_0_0 // clock
    , input wire  _$dCTuple3_1_0 // reset
    , input wire  _$dCTuple3_2_0 // enable

      // Outputs
    , output wire [65:0] c$case_alt
    );
  // Test.hs:14:1-46
  reg [63:0] s = 64'd14659767778871345152;
  wire signed [63:0] c$app_arg;
  wire [2:0] _$dCTuple3;
  wire  c$rst;

  assign _$dCTuple3 = {_$dCTuple3_0_0,
                       _$dCTuple3_1_0,   _$dCTuple3_2_0};

  assign c$rst = _$dCTuple3[1:1];

  // register begin
  always @(posedge _$dCTuple3[2:2] or  posedge  c$rst) begin : s_register
    if ( c$rst) begin
      s <= 64'd14659767778871345152;
    end else if (_$dCTuple3[0:0]) begin
      s <= s;
    end
  end
  // register end

  assign c$app_arg = NO_TRANSLATION_FOR:GHC.Num.Integer.integerFromNatural;

  assign c$case_alt = $unsigned({{(66-64) {1'b0}},c$app_arg});


endmodule
`default_nettype wire

[DigitalBrains1]

My guess is that this is because:

newtype SNat (n :: Nat) = UnsafeSNat_ Natural

I.e., Clash will just treat it as a Natural in its HWType (which are hardcoded to 64-bit numbers..).

Right, yes, that makes sense. But tread carefully! The code you're quoting is correct but can be misleading. That code is the definition of GHC.TypeLits.SNat, not of Clash.Promoted.Nat.SNat. They are distinct (though also a bit of a Matroshka doll).

[DigitalBrains1]

If we can fix this by rendering SNats as 0-bit constructs (which'd make them disappear from the ports of the top entity), I think that would be the best fix.