Global SEC check

[nanocoh]

No description provided.

[gemini-code-assist]

Code Review

This pull request integrates sequential equivalence checking (SEC_CHECK) using the Kepler Formal PDR engine into the flow, alongside existing logical equivalence checks (LEC_CHECK). The changes update documentation, variables schemas, Makefiles, and synthesis/reporting scripts to support these checks, as well as updating the kepler-formal submodule. The code review feedback is highly constructive and should be addressed: it recommends adding helper functions (lec_check_enabled and sec_check_enabled) to safely guard execution rather than directly reading environment variables, verifying the existence of the SEC log file before running grep to avoid silent failures, and dynamically resolving step labels in run_sec_test for consistency.

[gemini-code-assist]

Checking for a pattern in the log file using grep without first verifying that the log file exists can lead to silent passes if the formal tool fails to run or crashes (since grep exiting with status 2 on a missing file will trigger the CHILDSTATUS trap and set count to 0). Additionally, using a hardcoded label like "Global output" is inconsistent with run_lec_test which uses formal_check_label to dynamically resolve the step label.

proc run_sec_test { step file1 file2 } {
  write_sec_script $step $file1 $file2
  # tclint-disable-next-line command-args
  eval exec $::env(KEPLER_FORMAL_EXE) --config $::env(OBJECTS_DIR)/${step}_sec_test.yml
  set log_file $::env(LOG_DIR)/${step}_sec_check.log
  if { ![file exists $log_file] } {
    error "SEC log file not found: $log_file"
  }
  try {
    set count [exec grep -c "SEC found a counterexample" $log_file]
  } trap CHILDSTATUS {results options} {
    # This block executes if grep returns a non-zero exit code
    set count 0
  }
  set label [formal_check_label $step]
  if { $count > 0 } {
    error "$label failed sec test"
  } else {
    puts "$label passed sec test"
  }
}

[gemini-code-assist]

Using raw environment variables like $::env(LEC_CHECK) and $::env(SEC_CHECK) directly to guard formal check execution can cause crashes if they are set to 1 but the formal tool executable is missing or not executable. Use the lec_check_enabled and sec_check_enabled helper functions to safely guard these steps.

if { [lec_check_enabled] || [sec_check_enabled] } {
  write_lec_verilog 6_final_lec.v
}

if { [lec_check_enabled] } {
  run_lec_test 6_final 1_synth_lec.v 6_final_lec.v
}

if { [sec_check_enabled] } {
  run_sec_test 6_final 1_synth_lec.v 6_final_lec.v
}

[gemini-code-assist]

Add a sec_check_enabled helper function to check if sequential equivalence checking is enabled and the Kepler Formal executable is available and executable, matching the design of lec_check_enabled.

proc formal_check_label { step } {
  if { [string equal $step 4_rsz] } {
    return "Repair timing output"
  }
  return "Global output"
}

proc sec_check_enabled { } {
  return [expr {
    [env_var_equals SEC_CHECK 1]
    && [info exists ::env(KEPLER_FORMAL_EXE)]
    && [file executable $::env(KEPLER_FORMAL_EXE)]
  }]
}

[gemini-code-assist]

Use lec_check_enabled and sec_check_enabled helper functions to guard writing the LEC verilog file, ensuring consistency and preventing unnecessary file generation when the formal check tool is not available.

if { [lec_check_enabled] || [sec_check_enabled] } {
  write_lec_verilog 1_synth_lec.v
}

[gemini-code-assist]

Use lec_check_enabled and sec_check_enabled helper functions to guard writing the LEC verilog file, ensuring consistency and preventing unnecessary file generation when the formal check tool is not available.

if { [lec_check_enabled] || [sec_check_enabled] } {
  write_lec_verilog 1_synth_lec.v
}