test #25

n0thingNoob · 2025-12-08T23:08:00Z

add verify folder and remove analysis folder

verify/funcsim.go

+	src0 := fs.readOperand(x, y, &op.SrcOperands.Operands[0])
+	src1 := fs.readOperand(x, y, &op.SrcOperands.Operands[1])
+
+	val0 := int32(src0.First())


The best fix is to ensure that, before converting a value from uint32 (as provided by src0.First()) to int32, we check if it fits within the positive int32 bounds (i.e., is ≤ math.MaxInt32). If the value exceeds this bound, we should substitute a reasonable default (0 or perhaps the maximum allowed value in context), or otherwise handle the error appropriately (e.g., logging or panicking if this is truly unexpected).

The specific fix is to update the computation of val0 and val1 in runIcmp. For each value, check whether it is ≤ math.MaxInt32; if so, convert to int32, otherwise treat as 0 (or another safe fallback value) to prevent sign overflow. This edit is to be done in verify/funcsim.go, specifically around lines 579-580.

No new imports are required: math is already imported.

verify/funcsim.go

+	src1 := fs.readOperand(x, y, &op.SrcOperands.Operands[1])
+
+	val0 := int32(src0.First())
+	val1 := int32(src1.First())


To fix this issue, ensure that when parsing an immediate operand as a constant via strconv.ParseUint(..., 10, 32), if the value is to be used as a signed int32 elsewhere (i.e., by conversion), the parsed value must not exceed math.MaxInt32 (2147483647); otherwise, it could wrap around into a negative value when cast to int32. Therefore, introduce an explicit upper bound check before returning the parsed immediate. If the value is greater than math.MaxInt32, treat this as an error or clamp it to a safe default (as per the established pattern in the code), or (well-preferred) return a zero/error value. All changes should be limited to verify/funcsim.go inside the readOperand implementation (lines near the strconv.ParseUint) and must include the necessary math import only if not present (it already is).

Copilot

Pull request overview

This PR adds a comprehensive verification framework for Zeonica CGRA kernels with static lint checking, functional simulation, and reporting capabilities. The implementation includes ~2000 lines of code across core logic, tests, CLI tools, and documentation.

Key Changes:

Implements a two-stage verification system (lint + functional simulation) for CGRA kernel validation
Adds support for 35+ opcodes with predicate tracking and dataflow execution
Provides CLI tools for histogram and AXPY kernel verification with detailed reporting

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 14 comments.

Show a summary per file

File	Description
verify/verify.go	Core types, architecture model, PE state management, and coordinate system utilities
verify/lint.go	Static analysis for structural validation, port conflicts, and timing constraints with modulo scheduling support
verify/funcsim.go	Functional simulator implementing 35+ opcodes with topological execution order
verify/report.go	Report generation system with formatted output for lint issues and simulation results
verify/verify_test.go	Unit tests for basic lint checks, coordinate validation, and arithmetic operations
verify/histogram_integration_test.go	Integration tests for histogram kernel with lint and functional simulation
verify/funcsim.go	Comprehensive opcode implementations including arithmetic, bitwise, memory, and control flow operations
verify/cmd/verify-histogram/main.go	CLI tool for histogram kernel verification with architecture configuration
verify/cmd/verify-axpy/main.go	CLI tool for AXPY kernel verification with detailed progress output
verify/README.md	Complete documentation with API reference, examples, architecture internals, and troubleshooting guide

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2025-12-08T23:13:04Z

verify/report.go

+	if len(r.TimingIssues) > 0 {
+		fmt.Fprintln(w, "⚠ TIMING VIOLATIONS DETECTED")
+		fmt.Fprintln(w, "The histogram kernel has cross-PE communication constraints")


The recommendation section hardcodes histogram-specific text ("The histogram kernel has cross-PE communication constraints") even though this is a generic report generator. When used with other kernels like AXPY, this message would be confusing. The recommendation text should be generic or parameterized based on the kernel being verified.

Copilot · 2025-12-08T23:13:04Z

verify/report.go

+		fmt.Fprintln(w, "  3. Using buffering or pipelining strategies")
+	} else {
+		fmt.Fprintln(w, "✓ KERNEL PASSED ALL CHECKS")
+		fmt.Fprintln(w, "The histogram kernel is ready for simulation.")


The final recommendation message says "The histogram kernel is ready for simulation" which is hardcoded for histogram. This generic report generator is used by multiple kernels (AXPY, histogram, etc.) and should have a generic success message instead.

Suggested change

fmt.Fprintln(w, "The histogram kernel is ready for simulation.")

fmt.Fprintln(w, "The kernel is ready for simulation.")

Copilot · 2025-12-08T23:13:04Z

verify/lint.go

+// - Reading NORTH means producer is at (x, y-1) writing SOUTH
+// - Reading SOUTH means producer is at (x, y+1) writing NORTH
+// - Reading EAST means producer is at (x+1, y) writing WEST
+// - Reading WEST means producer is at (x-1, y) writing EAST
+func neighborCoord(x, y int, readDir string) (nx, ny int) {
+	switch strings.ToUpper(readDir) {
+	case "NORTH":
+		// Reading from north means the producer is north of us
+		return x, y - 1
+	case "SOUTH":
+		// Reading from south means the producer is south of us
+		return x, y + 1


The neighborCoord function has incorrect comment that conflicts with the implementation. The comment says "Reading NORTH means producer is at (x, y-1)" but in a standard coordinate system where Y increases upward, NORTH should be y+1, not y-1. The implementation returns y - 1 for NORTH, which suggests Y increases downward. However, the getNeighbor function in verify.go line 303 uses y + 1 for NORTH. This inconsistency between the two functions will cause bugs in producer-consumer matching.

Suggested change

// - Reading NORTH means producer is at (x, y-1) writing SOUTH

// - Reading SOUTH means producer is at (x, y+1) writing NORTH

// - Reading EAST means producer is at (x+1, y) writing WEST

// - Reading WEST means producer is at (x-1, y) writing EAST

func neighborCoord(x, y int, readDir string) (nx, ny int) {

switch strings.ToUpper(readDir) {

case "NORTH":

// Reading from north means the producer is north of us

return x, y - 1

case "SOUTH":

// Reading from south means the producer is south of us

return x, y + 1

// - Reading NORTH means producer is at (x, y+1) writing SOUTH

// - Reading SOUTH means producer is at (x, y-1) writing NORTH

// - Reading EAST means producer is at (x+1, y) writing WEST

// - Reading WEST means producer is at (x-1, y) writing EAST

func neighborCoord(x, y int, readDir string) (nx, ny int) {

switch strings.ToUpper(readDir) {

case "NORTH":

// Reading from north means the producer is north of us

return x, y + 1

case "SOUTH":

// Reading from south means the producer is south of us

return x, y - 1

Copilot · 2025-12-08T23:13:05Z

verify/lint.go

+
+							// Look for a producer at (prodX, prodY) that writes prodPort with same color
+							// We search across ALL timesteps in the producer's program
+							for prodT := 0; prodT < 1000; prodT++ { // arbitrary large number


The loop uses a hardcoded magic number 1000 to search for producers across timesteps. This arbitrary limit could miss valid producers if kernels have more than 1000 timesteps, and it's also inefficient as it iterates through all timesteps even when the producer program might have far fewer timesteps. Consider iterating through actual timesteps from the producer's program instead.

Suggested change

for prodT := 0; prodT < 1000; prodT++ { // arbitrary large number

// Find the producer's program using its coordinates

prodProgKey := fmt.Sprintf("%d,%d", prodX, prodY)

prodProg, ok := programs[prodProgKey]

if !ok {

continue // No program for producer PE

}

for prodT := 0; prodT < len(prodProg.InstructionGroups); prodT++ {

Copilot · 2025-12-08T23:13:05Z

verify/funcsim.go

+	// In functional model, we don't model network delays or buffering
+	// For now, return default value (in practice, would fetch from neighbor)
+	return core.NewScalarWithPred(0, false)


The readFromNeighbor function always returns invalid data (Pred: false) with a comment saying it doesn't model network delays. This means the functional simulator cannot actually simulate cross-PE communication at all, making it unable to verify any kernel with inter-PE data flow. The function should either be implemented to properly read from neighbor PE states, or the simulator should document this as a critical limitation that prevents testing of multi-PE kernels.

Suggested change

// In functional model, we don't model network delays or buffering

// For now, return default value (in practice, would fetch from neighbor)

return core.NewScalarWithPred(0, false)

// Determine neighbor coordinates based on port direction

nx, ny := x, y

switch portDir {

case "N":

ny = y - 1

case "S":

ny = y + 1

case "E":

nx = x + 1

case "W":

nx = x - 1

default:

// Unknown direction, return invalid

return core.NewScalarWithPred(0, false)

}

// Check bounds

if ny < 0 || ny >= len(fs.peStates) || nx < 0 || nx >= len(fs.peStates[0]) {

return core.NewScalarWithPred(0, false)

}

// For simplicity, assume port maps to register 0 in neighbor

return fs.peStates[ny][nx].ReadReg(0)

Copilot · 2025-12-08T23:13:06Z

verify/README.md

+func (fs *FunctionalSimulator) Run(maxSteps int) error
+
+// Preload data
+func (fs *FunctionalSimulator) PreloadMemory(x, y int, value, address uint32) error


The README documentation at line 289 has the same issue as the code comment - it shows the parameters in the order that doesn't match the actual function signature. It documents PreloadMemory(x, y int, value, address uint32) with value before address, but then at line 73 shows usage fs.PreloadMemory(0, 0, 0, 42) which would mean "address 0, value 42" with the documented signature but the comment says "addr 0, value 42" suggesting the signature should be (x, y, address, value).

Suggested change

func (fs *FunctionalSimulator) PreloadMemory(x, y int, value, address uint32) error

func (fs *FunctionalSimulator) PreloadMemory(x, y int, address, value uint32) error

Copilot · 2025-12-08T23:13:07Z

verify/verify.go

+}
+
+// PreloadMemory preloads a memory location with a value
+func (fs *FunctionalSimulator) PreloadMemory(x, y int, value uint32, address uint32) error {


The parameter order in PreloadMemory is inconsistent with convention. The function signature has (x, y int, value uint32, address uint32) but memory operations typically use (x, y, address, value) order. This ordering places the address before the value, which is counterintuitive as the address typically comes first in memory operations.

Suggested change

func (fs *FunctionalSimulator) PreloadMemory(x, y int, value uint32, address uint32) error {

func (fs *FunctionalSimulator) PreloadMemory(x, y int, address uint32, value uint32) error {

Copilot · 2025-12-08T23:13:07Z

verify/README.md

+```go
+fs := verify.NewFunctionalSimulator(programs, arch)
+fs.PreloadMemory(0, 0, 0, 42)  // PE(0,0), addr 0, value 42
+fs.Run(100)                     // Run up to 100 steps


Inconsistent documentation. Line 108 in README shows fs.PreloadMemory(0, 0, 0, 42) with comment "PE(0,0), addr 0, value 42", which implies the correct order should be (x, y, address, value), but the API reference at line 289 documents it as PreloadMemory(x, y int, value, address uint32) with value before address. This documentation inconsistency needs to be resolved to match the actual implementation.

Copilot · 2025-12-08T23:13:07Z

verify/funcsim.go

+	src1 := fs.readOperand(x, y, &op.SrcOperands.Operands[1])
+
+	var result uint32
+	if src0.First() < src1.First() {


The comment describes this as "Less Than Export" but the implementation uses unsigned comparison src0.First() < src1.First() where both values are uint32. The name "LT_EX" and context of other ICMP operations suggest this should use signed comparison like int32(src0.First()) < int32(src1.First()) to be consistent with ICMP_SLT (signed less than).

Suggested change

if src0.First() < src1.First() {

if int32(src0.First()) < int32(src1.First()) {

Copilot · 2025-12-08T23:13:08Z

verify/report.go

+	dash := strings.Repeat("-", 60)
+
+	fmt.Fprintln(w, separator)
+	fmt.Fprintln(w, "HISTOGRAM KERNEL VERIFICATION REPORT")


The report hardcodes "HISTOGRAM KERNEL VERIFICATION REPORT" as the title even though this is a generic report generator that can be used for any kernel (AXPY, histogram, etc.). The title should either be generic like "KERNEL VERIFICATION REPORT" or should be parameterized to accept a kernel name.

Jackcuii

LGTM

test

919f9d1

n0thingNoob requested review from Jackcuii, Copilot, syifan and yuchaosu December 8, 2025 23:08

Copilot started reviewing on behalf of n0thingNoob December 8, 2025 23:08 View session

github-advanced-security bot found potential problems Dec 8, 2025

View reviewed changes

Copilot AI reviewed Dec 8, 2025

View reviewed changes

Jackcuii approved these changes Dec 8, 2025

View reviewed changes

n0thingNoob merged commit 8b0ec48 into main Dec 8, 2025
9 of 11 checks passed

@@ -576,8 +576,17 @@
             	src0 := fs.readOperand(x, y, &op.SrcOperands.Operands[0])
             	src1 := fs.readOperand(x, y, &op.SrcOperands.Operands[1])
-            	val0 := int32(src0.First())
-            	val1 := int32(src1.First())
+            	var val0, val1 int32
+            	if src0.First() <= math.MaxInt32 {
+            		val0 = int32(src0.First())
+            	} else {
+            		val0 = 0
+            	}
+            	if src1.First() <= math.MaxInt32 {
+            		val1 = int32(src1.First())
+            	} else {
+            		val1 = 0
+            	}
             	var result uint32
             	switch strings.ToUpper(op.OpCode) {

@@ -776,6 +776,10 @@
             		if err != nil {
             			return core.NewScalarWithPred(0, false)
             		}
+            		// Prevent values exceeding int32 range from being used as immediate
+            		if val > math.MaxInt32 {
+            			return core.NewScalarWithPred(0, false)
+            		}
             		return core.NewScalar(uint32(val))
             	}

	fmt.Fprintln(w, "The histogram kernel is ready for simulation.")
	fmt.Fprintln(w, "The kernel is ready for simulation.")

-							for prodT := 0; prodT < 1000; prodT++ { // arbitrary large number
+							// Find the producer's program using its coordinates
+							prodProgKey := fmt.Sprintf("%d,%d", prodX, prodY)
+							prodProg, ok := programs[prodProgKey]
+							if !ok {
+								continue // No program for producer PE
+							}
+							for prodT := 0; prodT < len(prodProg.InstructionGroups); prodT++ {

-	// In functional model, we don't model network delays or buffering
-	// For now, return default value (in practice, would fetch from neighbor)
-	return core.NewScalarWithPred(0, false)
+	// Determine neighbor coordinates based on port direction
+	nx, ny := x, y
+	switch portDir {
+	case "N":
+		ny = y - 1
+	case "S":
+		ny = y + 1
+	case "E":
+		nx = x + 1
+	case "W":
+		nx = x - 1
+	default:
+		// Unknown direction, return invalid
+		return core.NewScalarWithPred(0, false)
+	}
+	// Check bounds
+	if ny < 0 || ny >= len(fs.peStates) || nx < 0 || nx >= len(fs.peStates[0]) {
+		return core.NewScalarWithPred(0, false)
+	}
+	// For simplicity, assume port maps to register 0 in neighbor
+	return fs.peStates[ny][nx].ReadReg(0)

	func (fs *FunctionalSimulator) PreloadMemory(x, y int, value, address uint32) error
	func (fs *FunctionalSimulator) PreloadMemory(x, y int, address, value uint32) error

	if src0.First() < src1.First() {
	if int32(src0.First()) < int32(src1.First()) {

test #25

test #25

Uh oh!

Conversation

n0thingNoob commented Dec 8, 2025

Uh oh!

Check failure

Uh oh!

Copilot Autofix

Check failure

Uh oh!

Copilot Autofix

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Dec 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 8, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 8, 2025

Choose a reason for hiding this comment

Uh oh!

Jackcuii left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants