Skip to content

Commit

Permalink
Added signoff report generation.
Browse files Browse the repository at this point in the history
Signed-off-by: Pascal Gouedo <[email protected]>
  • Loading branch information
Pascal Gouedo committed Jun 12, 2024
1 parent c3e86fc commit c753804
Showing 1 changed file with 8 additions and 2 deletions.
10 changes: 8 additions & 2 deletions scripts/riscv_isa_formal/common/setup.tcl
Original file line number Diff line number Diff line change
Expand Up @@ -427,8 +427,10 @@ if {$app eq "PRC"} {
puts "[expr $i * $nb_processes] [expr ((($i + 1) * $nb_processes) - 1)]"
puts "\n-INFO- Launching Check Command::\n\ncheck $checks\n"
check $checks
report_result -details
cd $app_dir
start_message_log round_[expr $i + 1].log
report_result -details
stop_message_log
save_database -force round_[expr $i + 1]
cd $cwd
}
Expand All @@ -437,13 +439,17 @@ if {$app eq "PRC"} {
puts "[expr $nb_round * $nb_processes] [expr (($nb_round * $nb_processes) + $nb_remain - 1)]"
puts "\n-INFO- Launching Check Command::\n\ncheck $checks\n"
check $checks
report_result -details
cd $app_dir
start_message_log round_[expr $i + 1].log
report_result -details
stop_message_log
save_database -force round_[expr $nb_round + 1]
cd $cwd
}

start_message_log round_[expr $i + 1]_signoff.log
report_result -signoff -details
stop_message_log

# set_check_option -prover_exec_order { { disprover1 disprover3 } }
# puts "\n-INFO- Launching Check Command::\n\ncheck RV32M.DIV16_a\n"
Expand Down

0 comments on commit c753804

Please sign in to comment.