spec(course): the FPGA course lesson specs compile, pass and assert at run time (Closes #10013)

specs/boards/wukong_v1.t27

@@ -50,7 +50,7 @@ module BoardWukongV1 {
 
     // The prjxray-db entry used for place-and-route. Same die, same BGA-676
     // pinout; Xilinx publishes only `xc7a200tfbg676pkg.txt`. See
-    // fpga/HARDWARE_SSOT.md §2026-07-05.
+    // fpga/HARDWARE_SSOT.md, section 2026-07-05.
     const PNR_PART     : &str = "xc7a200tfbg676-1";
 
     // Fabric, from the Artix-7 datasheet for the 200T.
@@ -155,6 +155,40 @@ module BoardWukongV1 {
         return (KV_BYTES_PER_TOKEN * ctx_tokens);
     }
 
+    // ---- Decoders for the identifiers above ----
+    //
+    // A test that compares a constant with its own literal folds away at compile
+    // time and checks nothing. These read the fields the way a JTAG or SPI host
+    // does, so the tests below assert on what the identifier says, not on how it
+    // was typed.
+
+    // IEEE 1149.1 IDCODE: version [31:28], part [27:12], maker [11:1], 1 [0].
+    fn idcode_part(code: u32) -> u32 {
+        return ((code >> 12) & 0xFFFF);
+    }
+
+    fn idcode_maker(code: u32) -> u32 {
+        return ((code >> 1) & 0x7FF);
+    }
+
+    // SPI flash JEDEC id: maker [23:16], type [15:8], log2(bytes) [7:0].
+    fn jedec_maker(id: u32) -> u32 {
+        return ((id >> 16) & 0xFF);
+    }
+
+    fn jedec_capacity_log2(id: u32) -> u32 {
+        return (id & 0xFF);
+    }
+
+    // One Mbit is 1048576 bits, which is 131072 bytes.
+    fn mbit_to_bytes(mbit: u32) -> u32 {
+        return (mbit * 131072);
+    }
+
+    fn dram_capacity_known() -> bool {
+        return DRAM_BYTES_MEASURED;
+    }
+
     // ---- Combinational port surface (T81) ----
     //
     // Without a data port the module has no boundary and synthesises to nothing.
@@ -172,17 +206,22 @@ module BoardWukongV1 {
 
     // ---- Tests ----
 
+    // Part 0x3636 is the XC7A200T; maker 0x049 is Xilinx (JEP106 bank 0, 0x49).
     test idcode_is_the_two_hundred_t
-        given v = JTAG_IDCODE
-        then v == 0x03636093
+        given part = idcode_part(JTAG_IDCODE)
+        and   maker = idcode_maker(JTAG_IDCODE)
+        then part == 0x3636 and maker == 0x049
 
+    // Maker 0x20 is Micron; 2^24 bytes is 128 Mbit.
     test flash_is_one_twenty_eight_mbit
-        given v = FLASH_MBIT
-        then v == 128
+        given maker = jedec_maker(FLASH_JEDEC_ID)
+        and   log2 = jedec_capacity_log2(FLASH_JEDEC_ID)
+        and   bytes = mbit_to_bytes(FLASH_MBIT)
+        then maker == 0x20 and log2 == 24 and bytes == 16777216
 
     test flash_bytes_follow_from_mbit
-        given v = FLASH_BYTES
-        then v == 16777216
+        given bytes = mbit_to_bytes(FLASH_MBIT)
+        then bytes == FLASH_BYTES
 
     // THE RESULT. The weights do not fit the flash, and this is the constraint
     // no plan on the table lists.
@@ -196,7 +235,7 @@ module BoardWukongV1 {
 
     // The DRAM question is refused, not answered.
     test dram_capacity_is_not_measured
-        given m = DRAM_BYTES_MEASURED
+        given m = dram_capacity_known()
         then m == false
 
     test dram_fit_refuses_to_answer

specs/boards/xc7a100t_minimal.t27

@@ -193,6 +193,22 @@ module BoardMinimalXC7A100T {
         return HAS_SPI;
     }
 
+    fn has_mac_debug() -> bool {
+        return HAS_MAC_DEBUG;
+    }
+
+    // Clock arithmetic. A test that compares a constant with its own literal
+    // folds away at compile time and checks nothing, so the clock tests go
+    // through these instead: the period is derived from the frequency, and the
+    // frequency is read back as cycles per millisecond.
+    fn period_ns_from_hz(hz: u32) -> u32 {
+        return (1_000_000_000 / hz);
+    }
+
+    fn cycles_per_ms(hz: u32) -> u32 {
+        return (hz / 1000);
+    }
+
     fn is_prjxray_verified(pin: PinAssignment) -> bool {
         if (pin.package_pin == "E3") { return true; }
         if (pin.package_pin == "C18") { return true; }
@@ -237,16 +253,16 @@ module BoardMinimalXC7A100T {
         then family == "artix7"
 
     test clock_freq_12mhz
-        given freq = CLOCK_FREQ_HZ
-        then freq == 12_000_000
+        given c = cycles_per_ms(CLOCK_FREQ_HZ)
+        then c == 12_000
 
     test clock_period_83ns
-        given period = CLOCK_PERIOD_NS
-        then period == 83
+        given period = period_ns_from_hz(CLOCK_FREQ_HZ)
+        then period == 83 and period == CLOCK_PERIOD_NS
 
     test num_leds_is_8
-        given n = NUM_LEDS
-        then n == 8
+        given n = count_leds()
+        then n == 8 and n == NUM_LEDS
 
     test has_uart_true
         given result = has_uart()
@@ -257,7 +273,7 @@ module BoardMinimalXC7A100T {
         then result == false
 
     test has_mac_debug_false
-        given result = HAS_MAC_DEBUG
+        given result = has_mac_debug()
         then result == false
 
     test count_pins_is_12

specs/demos/hello_world.t27

@@ -44,7 +44,7 @@ module HelloWorld {
     // Explicit signatures ensure type safety across hardware boundaries.
     pub fn calculate_area(config : ConfigPacked) -> u16 {
         // Type conversion is explicit: u8 * u8 -> u16 prevents overflow
-        let area : u16 = cast(config.width) * cast(config.height);
+        let area : u16 = (config.width as u16) * (config.height as u16);
         return area;
     }
 

specs/fpga/placement.t27

@@ -98,6 +98,7 @@ pub struct Floorplan {
         return Floorplan{
             .name = name,
             .device = device,
+            ._dummy = 0,
         };
     }
 

specs/fpga/stdlib.t27

@@ -68,6 +68,10 @@ module Stdlib {
 
     // === Constructor helpers ===
 
+    fn kind_code(k: IpKind) -> i8 {
+        return @intFromEnum(k);
+    }
+
     fn zero_resources() -> ResourceEstimate {
         return ResourceEstimate{
             .luts = 0,
@@ -328,9 +332,15 @@ module Stdlib {
         and board = xc7a100t_resources()
         then luts_remaining(cat, board) == 63400
 
+    // The kind codes are what an IpCore stores, so they are read back through
+    // kind_code() at run time; comparing two literals checks nothing.
     test ip_kind_values
-        then 0 == 0
-        and 1 == 1
+        given first = kind_code(IpKind.uart_tx)
+        and   gpio = kind_code(IpKind.gpio)
+        and   last = kind_code(IpKind.ternary_alu)
+        then first == 0
+        and gpio == 5
+        and last == 12
 
     test ip_core_vendor
         given ip = ip_core("uart_tx", 0, 200, 100, 1, 0, 4, 100)

specs/tutorial/01_values_and_types.t27

@@ -0,0 +1,126 @@
+// SPDX-License-Identifier: Apache-2.0
+; 01 -- Values and types
+; Lesson 1 of the t27 tutorial. Every constant carries an explicit width,
+; because a spec has to say what reaches hardware rather than let a compiler
+; pick for it. Nothing here is inferred.
+; phi^2 + 1/phi^2 = 3 | TRINITY
+
+module tutorial-01-values;
+
+// ============================================================================
+// Integers
+//
+// Width and signedness are part of the name's type, always written out.
+// u = unsigned, i = signed, and the number is the bit width.
+// ============================================================================
+
+pub const SMALL_UNSIGNED : u8 = 200;
+pub const SMALL_SIGNED : i8 = -100;
+pub const WIDE_UNSIGNED : u16 = 65535;
+pub const WIDER : u32 = 4000000000;
+pub const SIGNED_32 : i32 = -2000000;
+
+// ============================================================================
+// Other bases
+//
+// Hex and binary are ordinary integer literals. Binary is worth using wherever
+// the value IS a bit pattern -- a mask written as 0b111111111 documents its own
+// width in a way that 511 does not.
+// ============================================================================
+
+pub const AS_HEX : u16 = 0xFFFF;
+pub const AS_BINARY : u8 = 0b1010;
+pub const MANTISSA_MASK : u16 = 0b111111111;
+
+// ============================================================================
+// Floats and booleans
+// ============================================================================
+
+pub const RATIO : f32 = 1.5;
+pub const PRECISE : f64 = 2.25;
+
+pub const ENABLED : bool = true;
+pub const DISABLED : bool = false;
+
+// ============================================================================
+// The trit
+//
+// This language is built on three states rather than two. A trit is stored in
+// an i8 and is only ever -1, 0 or +1; the invariant at the bottom is what
+// makes that a claim rather than a comment.
+// ============================================================================
+
+pub const TRIT_NEG : i8 = -1;
+pub const TRIT_ZERO : i8 = 0;
+pub const TRIT_POS : i8 = 1;
+
+pub const TRINITY : i8 = 3;
+
+// ============================================================================
+// Invariants
+//
+// An invariant states something that must hold for the module as a whole. It
+// is checked, not decorative.
+// ============================================================================
+
+// ============================================================================
+// Tests
+//
+// A test states something about the values above that would break if one of
+// them were written wrong. Each assert names a concrete number, so a typo in a
+// constant fails here rather than in whatever reads it later.
+//
+// Each test first copies the constants into `var` locals. A constant compared
+// with a constant is settled by the compiler before any test runs, so nothing
+// would be checked at run time; a `var` is a value the program holds, and
+// reading it is the run-time check. That is also the difference between the
+// two: `const` is a fact about the spec, `var` is storage.
+// ============================================================================
+
+test "each base spells the number it claims" {
+    var hex : u16 = AS_HEX;
+    var bin : u8 = AS_BINARY;
+    var mask : u16 = MANTISSA_MASK;
+    try std.testing.expectEqual(@as(u16, 65535), hex);
+    try std.testing.expectEqual(WIDE_UNSIGNED, hex);
+    try std.testing.expectEqual(@as(u8, 10), bin);
+    try std.testing.expectEqual(@as(u16, 511), mask);
+}
+
+test "signed and unsigned constants hold their written values" {
+    var small_u : u8 = SMALL_UNSIGNED;
+    var small_i : i8 = SMALL_SIGNED;
+    var wider : u32 = WIDER;
+    var signed_32 : i32 = SIGNED_32;
+    try std.testing.expectEqual(@as(u8, 200), small_u);
+    try std.testing.expectEqual(@as(i8, -100), small_i);
+    try std.testing.expectEqual(@as(u32, 4000000000), wider);
+    try std.testing.expectEqual(@as(i32, -2000000), signed_32);
+}
+
+test "the three trits are distinct and sum to zero" {
+    var neg : i8 = TRIT_NEG;
+    var zero : i8 = TRIT_ZERO;
+    var pos : i8 = TRIT_POS;
+    try std.testing.expectEqual(@as(i8, 0), neg + zero + pos);
+    try std.testing.expectEqual(TRINITY, pos - neg + 1);
+    try std.testing.expect(neg < zero);
+    try std.testing.expect(zero < pos);
+}
+
+test "floats and booleans" {
+    var ratio : f32 = RATIO;
+    var precise : f64 = PRECISE;
+    var on : bool = ENABLED;
+    var off : bool = DISABLED;
+    try std.testing.expectEqual(@as(f32, 3.0), ratio * 2.0);
+    try std.testing.expectEqual(@as(f64, 4.5), precise * 2.0);
+    try std.testing.expect(on);
+    try std.testing.expect(!off);
+}
+
+invariant trit_range_is_three_states
+    assert TRIT_POS - TRIT_NEG + 1 == TRINITY
+
+invariant masks_match_their_widths
+    assert MANTISSA_MASK == 511

specs/tutorial/02_functions.t27

@@ -0,0 +1,83 @@
+// SPDX-License-Identifier: Apache-2.0
+; 02 -- Functions
+; Lesson 2. Parameter types and the return type are always written out. A
+; signature is part of the specification, so it is never inferred.
+; phi^2 + 1/phi^2 = 3 | TRINITY
+
+module tutorial-02-functions;
+
+pub const TRIT_NEG : i8 = -1;
+pub const TRIT_POS : i8 = 1;
+
+// ============================================================================
+// A function
+//
+//   pub fn NAME(param: TYPE, ...) RETURN_TYPE { ... }
+//
+// The return type sits after the parameter list with no arrow before it.
+// ============================================================================
+
+pub fn double(a: i8) i8 {
+    return a + a;
+}
+
+pub fn add(a: i8, b: i8) i8 {
+    return a + b;
+}
+
+// ============================================================================
+// Locals
+//
+// `const` inside a body is a local binding. Prefer it: an immutable local
+// cannot be accidentally rebound, and lesson 05 shows the one sharp edge that
+// mutable locals still have.
+// ============================================================================
+
+pub fn scaled_sum(a: i8, b: i8) i8 {
+    const sum = a + b;
+    const scaled = sum + sum;
+    return scaled;
+}
+
+// ============================================================================
+// Calling
+//
+// Functions call each other by name. There is no forward-declaration step --
+// order in the file does not matter.
+// ============================================================================
+
+pub fn quadruple(a: i8) i8 {
+    return double(double(a));
+}
+
+// ============================================================================
+// Unary operators
+// ============================================================================
+
+pub fn negate(a: i8) i8 {
+    return -a;
+}
+
+pub fn invert(flag: bool) bool {
+    return !flag;
+}
+
+// ============================================================================
+// Tests
+//
+// A test states a concrete example. It is emitted into every target that can
+// express one, so the same claim gets checked in Zig, C and Rust alike.
+// ============================================================================
+
+test "double and add agree on the same value" {
+    try std.testing.expectEqual(@as(i8, 4), double(2));
+    try std.testing.expectEqual(@as(i8, 4), add(2, 2));
+}
+
+test "quadruple composes double with itself" {
+    try std.testing.expectEqual(@as(i8, 8), quadruple(2));
+}
+
+test "negate flips a trit" {
+    try std.testing.expectEqual(@as(i8, TRIT_NEG), negate(TRIT_POS));
+}