mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
aba1fba7ad
Security & correctness fixes from full adversarial review: Lean (7 fixes): - FixedPoint.lean: guard false theorem with n > 0 precondition - QFactor.lean: remove double-scaling error in energy decrease - AVMIsa/Step.lean: implement addSatQ16/subSatQ16 primitives - BraidEigensolid.lean: fix crossStep second output argument swap - SSMS.lean: complete ACI preservation proof (with rounding caveat) - HouseholderQR.lean: add n > 0 precondition to spectral theorem Verilog (7 fixes): - q16_lut_core.v: fix multiply shift (16 → 32 bits) - q16_lut_top.v: fix valid bit (0 → 1) - cff_accelerator.v: fix SHA-256 padding (len < 448 check) - research_stack_top.v: fix trigger aliasing (unique counters) - Blitter6502OISC_small.v: fix address width (15 → 16 bits) - spatial_hash_bram.v: add OOB write guard - tmr_oepi_safety_fsm.v: fix double-increment race WGSL (6 fixes): - shaders.wgsl: atomicAdd for concurrent writes - frustration_qubo.wgsl: double-buffer + CAS loop - braid_fft.wgsl: workgroupBarrier synchronization - burgers_scar_filter.wgsl: atomic E_bins array Rust (9 fixes): - thermodynamic.rs: Arc::from_raw → Arc::clone (double-free) - thermodynamic.rs: Box::into_raw → Box (leak) - tools/src/lib.rs: shell injection → shlex.quote - ene-node/src/lib.rs: LRU caps, constant-time HMAC, peer caps Python (6 fixes): - similarity/__init__.py: pickle.load → RestrictedUnpickler - AI-Feynman: torch.load → weights_only=True (14 calls) - fetch_arxiv.py, fetch_s2.py: eval → ast.literal_eval - topology.py: os.system → shutil.copy2 - SSH pipe: os.system → base64 pipe Build: lake build 3572 jobs, 0 errors
93 lines
3.1 KiB
Verilog
93 lines
3.1 KiB
Verilog
// Q16_16 LUT Core — Fixed-Point Arithmetic Unit
|
|
// Stub based on interface from q16_lut_top.v
|
|
// 8 operations, 2-stage pipeline
|
|
// Original was generated by Lean Semantics tooling and exists as .json netlist.
|
|
// This stub provides the same interface for unified builds.
|
|
//
|
|
// op_select encoding:
|
|
// 000 = add (a + b)
|
|
// 001 = sub (a - b)
|
|
// 010 = mul (a * b, Q16_16 product)
|
|
// 011 = div (a / b, Q16_16 quotient)
|
|
// 100 = sqrt (sqrt(a))
|
|
// 101 = abs (|a|)
|
|
// 110 = min (min(a,b))
|
|
// 111 = max (max(a,b))
|
|
|
|
`timescale 1ns / 1ps
|
|
|
|
module q16_lut_core (
|
|
input wire clk,
|
|
input wire rst,
|
|
input wire [2:0] op_select,
|
|
input wire [15:0] a,
|
|
input wire [15:0] b,
|
|
output reg [31:0] result,
|
|
output reg valid
|
|
);
|
|
|
|
// Pipeline stage 1: decode and latch inputs
|
|
reg [2:0] op_reg;
|
|
reg [15:0] a_reg;
|
|
reg [15:0] b_reg;
|
|
reg valid_s1;
|
|
|
|
// Pipeline stage 2: execute
|
|
reg [31:0] result_s2;
|
|
reg valid_s2;
|
|
|
|
// Intermediate computation (combinational)
|
|
reg [31:0] compute_result;
|
|
|
|
// FIX: Use signed arithmetic for Q16.16 add/sub; multiply requires >> 16 shift
|
|
wire signed [31:0] a_signed = {{16{a_reg[15]}}, a_reg};
|
|
wire signed [31:0] b_signed = {{16{b_reg[15]}}, b_reg};
|
|
wire signed [63:0] mul_product = a_signed * b_signed;
|
|
|
|
always @(*) begin
|
|
case (op_reg)
|
|
3'b000: compute_result = a_signed + b_signed; // add (signed)
|
|
3'b001: compute_result = a_signed - b_signed; // sub (signed)
|
|
3'b010: compute_result = mul_product[47:16]; // mul: Q16.16 * Q16.16 >> 16
|
|
3'b011: begin // div
|
|
if (b_reg != 16'd0)
|
|
compute_result = ({16'd0, a_reg} << 16) / {16'd0, b_reg};
|
|
else
|
|
compute_result = 32'h7FFFFFFF; // saturate
|
|
end
|
|
3'b100: compute_result = {16'd0, a_reg}; // sqrt (passthrough stub)
|
|
3'b101: compute_result = a_reg[15] ? {16'd0, (~a_reg + 16'd1)} : {16'd0, a_reg}; // abs
|
|
3'b110: compute_result = (a_reg <= b_reg) ? {16'd0, a_reg} : {16'd0, b_reg}; // min
|
|
3'b111: compute_result = (a_reg >= b_reg) ? {16'd0, a_reg} : {16'd0, b_reg}; // max
|
|
endcase
|
|
end
|
|
|
|
// Pipeline registers
|
|
always @(posedge clk) begin
|
|
if (rst) begin
|
|
op_reg <= 3'd0;
|
|
a_reg <= 16'd0;
|
|
b_reg <= 16'd0;
|
|
valid_s1 <= 1'b0;
|
|
result_s2 <= 32'd0;
|
|
valid_s2 <= 1'b0;
|
|
result <= 32'd0;
|
|
valid <= 1'b0;
|
|
end else begin
|
|
// Stage 1: latch inputs
|
|
op_reg <= op_select;
|
|
a_reg <= a;
|
|
b_reg <= b;
|
|
valid_s1 <= 1'b1; // always valid after first cycle
|
|
|
|
// Stage 2: compute
|
|
result_s2 <= compute_result;
|
|
valid_s2 <= valid_s1;
|
|
|
|
// Output
|
|
result <= result_s2;
|
|
valid <= valid_s2;
|
|
end
|
|
end
|
|
|
|
endmodule
|