From dc959cdf4abdcc696585cc8fa9d587042132018a Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 13 Oct 2025 09:11:46 +0200 Subject: [PATCH 1/4] verific: Fix error compiling without VERIFIC_LINEFILE_INCLUDES_COLUMNS --- frontends/verific/verific.cc | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 937789842..2d0e6959e 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -168,12 +168,12 @@ string get_full_netlist_name(Netlist *nl) std::string format_src_location(DesignObj *obj) { - if (obj == nullptr || obj->Linefile() == nullptr) + if (obj == nullptr || !obj->Linefile()) return std::string(); #ifdef VERIFIC_LINEFILE_INCLUDES_COLUMNS - return stringf("%s:%d.%d-%d.%d", LineFile::GetFileName(obj->Linefile()), obj->Linefile()->GetLeftLine(), obj->Linefile()->GetLeftCol(), obj->Linefile()->GetRightLine(), obj->Linefile()->GetRightCol()); + return stringf("%s:%d.%d-%d.%d", LineFile::GetFileName(obj->Linefile()), obj->Linefile()->GetLeftLine(), obj->Linefile()->GetLeftCol(), obj->Linefile()->GetRightLine(), obj->Linefile()->GetRightCol()); #else - return stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile())); + return stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile())); #endif } From 1f11b2c5299781c1e935ee60e06a3a1fdbe8c376 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 13 Oct 2025 15:16:10 +0200 Subject: [PATCH 2/4] verific: Add src to message missed in #5406 --- frontends/verific/verific.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 2d0e6959e..ff8932dac 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1995,7 +1995,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma if (import_netlist_instance_cells(inst, inst_name)) continue; if (inst->IsOperator() && !verific_sva_prims.count(inst->Type())) - log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name()); + log_warning("%sUnsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", announce_src_location(inst), inst->View()->Owner()->Name()); } else { if (import_netlist_instance_gates(inst, inst_name)) continue; From 4513783a02d8b67a16d9d9b3ccad2265c9766868 Mon Sep 17 00:00:00 2001 From: "N. Engelhardt" Date: Tue, 14 Oct 2025 15:48:16 +0200 Subject: [PATCH 3/4] add tests --- tests/verific/ext_ramnet_err.sv | 13 +++++++++++++ tests/verific/ext_ramnet_err.ys | 5 +++++ tests/verific/import_warning_operator.vhd | 15 +++++++++++++++ tests/verific/import_warning_operator.ys | 5 +++++ 4 files changed, 38 insertions(+) create mode 100644 tests/verific/ext_ramnet_err.sv create mode 100644 tests/verific/ext_ramnet_err.ys create mode 100644 tests/verific/import_warning_operator.vhd create mode 100644 tests/verific/import_warning_operator.ys diff --git a/tests/verific/ext_ramnet_err.sv b/tests/verific/ext_ramnet_err.sv new file mode 100644 index 000000000..ba8040004 --- /dev/null +++ b/tests/verific/ext_ramnet_err.sv @@ -0,0 +1,13 @@ +module sub_rom (input clk, input [3:0] addr, output reg [7:0] data); + reg [7:0] mem [0:15]; + + always @(posedge clk) + data <= mem[addr]; +endmodule + +module top (input clk, input [3:0] addr, output [7:0] data, input [3:0] f_addr, input [7:0] f_data); + sub_rom u_sub_rom (clk, addr, data); + + always @(posedge clk) + assume(u_sub_rom.mem[f_addr] == f_data); +endmodule diff --git a/tests/verific/ext_ramnet_err.ys b/tests/verific/ext_ramnet_err.ys new file mode 100644 index 000000000..f1d45bd47 --- /dev/null +++ b/tests/verific/ext_ramnet_err.ys @@ -0,0 +1,5 @@ +logger -expect error "ext_ramnet_err.sv:\d+.\d+-\d+.\d+: Memory net '\S+' missing, possibly no driver, use verific -flatten." 1 +verific -sv ext_ramnet_err.sv +verific -import top +logger -check-expected +design -reset diff --git a/tests/verific/import_warning_operator.vhd b/tests/verific/import_warning_operator.vhd new file mode 100644 index 000000000..0b7d51788 --- /dev/null +++ b/tests/verific/import_warning_operator.vhd @@ -0,0 +1,15 @@ +library IEEE; +use IEEE.STD_LOGIC_1164.ALL; + +entity top is + Port ( + a : in STD_LOGIC_VECTOR(3 downto 0); + b : in STD_LOGIC_VECTOR(3 downto 0); + y : out STD_LOGIC_VECTOR(3 downto 0) + ); +end top; + +architecture Behavioral of top is +begin + y <= a nor b; +end Behavioral; diff --git a/tests/verific/import_warning_operator.ys b/tests/verific/import_warning_operator.ys new file mode 100644 index 000000000..9d16e3c18 --- /dev/null +++ b/tests/verific/import_warning_operator.ys @@ -0,0 +1,5 @@ +logger -expect warning "import_warning_operator.vhd:\d+.\d+-\d+.\d+: Unsupported Verific operator: nor_4 (fallback to gate level implementation provided by verific)" 1 +verific -vhdl import_warning_operator.vhd +verific -import top +logger -check-expected +design -reset From 7d2857b30fdbaa3713f080ceb9218529faf7c5b3 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 14 Oct 2025 16:04:56 +0200 Subject: [PATCH 4/4] Fix regex checks --- tests/verific/ext_ramnet_err.ys | 2 +- tests/verific/import_warning_operator.ys | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/verific/ext_ramnet_err.ys b/tests/verific/ext_ramnet_err.ys index f1d45bd47..7456af444 100644 --- a/tests/verific/ext_ramnet_err.ys +++ b/tests/verific/ext_ramnet_err.ys @@ -1,4 +1,4 @@ -logger -expect error "ext_ramnet_err.sv:\d+.\d+-\d+.\d+: Memory net '\S+' missing, possibly no driver, use verific -flatten." 1 +logger -expect error "ext_ramnet_err.sv:[0-9]+\.[0-9]+-[0-9]+\.[0-9]+: Memory net '[^']+' missing, possibly no driver, use verific -flatten." 1 verific -sv ext_ramnet_err.sv verific -import top logger -check-expected diff --git a/tests/verific/import_warning_operator.ys b/tests/verific/import_warning_operator.ys index 9d16e3c18..1ecd6d296 100644 --- a/tests/verific/import_warning_operator.ys +++ b/tests/verific/import_warning_operator.ys @@ -1,4 +1,4 @@ -logger -expect warning "import_warning_operator.vhd:\d+.\d+-\d+.\d+: Unsupported Verific operator: nor_4 (fallback to gate level implementation provided by verific)" 1 +logger -expect warning "import_warning_operator.vhd:[0-9]+.[0-9]+-[0-9]+.[0-9]+: Unsupported Verific operator: nor_4 \(fallback to gate level implementation provided by verific\)" 1 verific -vhdl import_warning_operator.vhd verific -import top logger -check-expected