From 8d8c5da8125290fae4e7e53b049087a71c9a7e76 Mon Sep 17 00:00:00 2001 From: Wilson Snyder Date: Sun, 16 Mar 2014 21:38:29 -0400 Subject: [PATCH] Add assertions on 'unique if', bug725. --- Changes | 2 + bin/verilator | 5 +- src/V3Assert.cpp | 55 ++++++++++++++ test_regress/t/t_uniqueif.pl | 20 ++++++ test_regress/t/t_uniqueif.v | 111 +++++++++++++++++++++++++++++ test_regress/t/t_uniqueif_fail1.pl | 28 ++++++++ test_regress/t/t_uniqueif_fail2.pl | 28 ++++++++ test_regress/t/t_uniqueif_fail3.pl | 28 ++++++++ test_regress/t/t_uniqueif_fail4.pl | 28 ++++++++ 9 files changed, 302 insertions(+), 3 deletions(-) create mode 100755 test_regress/t/t_uniqueif.pl create mode 100644 test_regress/t/t_uniqueif.v create mode 100755 test_regress/t/t_uniqueif_fail1.pl create mode 100755 test_regress/t/t_uniqueif_fail2.pl create mode 100755 test_regress/t/t_uniqueif_fail3.pl create mode 100755 test_regress/t/t_uniqueif_fail4.pl diff --git a/Changes b/Changes index de29f5b1f..539324890 100644 --- a/Changes +++ b/Changes @@ -9,6 +9,8 @@ indicates the contributor was also the author of the fix; Thanks! *** Add --no-trace-params. +*** Add assertions on 'unique if', bug725. [Jeff Bush] + **** Documentation fixes, bug723. [Glen Gibb] **** Fix tracing of package variables and real arrays. diff --git a/bin/verilator b/bin/verilator index 81e12ab4f..8dcb71a83 100755 --- a/bin/verilator +++ b/bin/verilator @@ -1991,9 +1991,8 @@ appropriate code to detect failing cases at runtime and print an "Assertion failed" error message. Verilator likewise also asserts any "unique" or "priority" SystemVerilog -keywords on case statements. However, "unique if" and "priority if" are -currently simply ignored. - +keywords on case statement, as well as "unique" on if statements. +However, "priority if" is currently simply ignored. =head1 LANGUAGE EXTENSIONS diff --git a/src/V3Assert.cpp b/src/V3Assert.cpp index fd5c593c8..5a446fb1d 100644 --- a/src/V3Assert.cpp +++ b/src/V3Assert.cpp @@ -174,6 +174,61 @@ private: // Bye pushDeletep(nodep); nodep=NULL; } + + virtual void visit(AstIf* nodep, AstNUser*) { + if (nodep->uniquePragma() || nodep->unique0Pragma()) { + AstNodeIf* ifp = nodep; + AstNode* propp = NULL; + bool hasDefaultElse = false; + do { + // If this statement ends with 'else if', then nextIf will point to the + // nextIf statement. Otherwise it will be null. + AstNodeIf* nextifp = dynamic_cast(ifp->elsesp()); + + // Recurse into the true case. + ifp->ifsp()->iterateChildren(*this); + + // If the last else is not an else if, recurse into that too. + if (ifp->elsesp() && !nextifp) { + ifp->elsesp()->iterateChildren(*this); + } + + // Build a bitmask of the true predicates + AstNode* predp = ifp->condp()->cloneTree(false); + if (propp) { + propp = new AstConcat(nodep->fileline(), predp, propp); + } else { + propp = predp; + } + + // Record if this ends with an 'else' that does not have an if + if (ifp->elsesp() && !nextifp) { + hasDefaultElse = true; + } + + ifp = nextifp; + } while (ifp); + + AstNode *newifp = nodep->cloneTree(false); + bool allow_none = nodep->unique0Pragma(); + + // Note: if this ends with an 'else', then we don't need to validate that one of the + // predicates evaluates to true. + AstNode* ohot = ((allow_none || hasDefaultElse) + ? (new AstOneHot0(nodep->fileline(), propp))->castNode() + : (new AstOneHot (nodep->fileline(), propp))->castNode()); + AstIf* checkifp = new AstIf (nodep->fileline(), + new AstLogNot (nodep->fileline(), ohot), + newFireAssert(nodep, "'unique if' statement violated"), + newifp); + checkifp->branchPred(AstBranchPred::BP_UNLIKELY); + nodep->replaceWith(checkifp); + pushDeletep(nodep); + } else { + nodep->ifsp()->iterateChildren(*this); + nodep->elsesp()->iterateChildren(*this); + } + } // VISITORS //========== Case assertions virtual void visit(AstCase* nodep, AstNUser*) { diff --git a/test_regress/t/t_uniqueif.pl b/test_regress/t/t_uniqueif.pl new file mode 100755 index 000000000..4eada89db --- /dev/null +++ b/test_regress/t/t_uniqueif.pl @@ -0,0 +1,20 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2009 by Wilson Snyder. This program is free software; you can +# redistribute it and/or modify it under the terms of either the GNU +# Lesser General Public License Version 3 or the Perl Artistic License +# Version 2.0. + +compile ( + verilator_flags2 => ['--assert'], + nc_flags2 => ['+assert'], + ); + +execute ( + check_finished=>1, + ); + +ok(1); +1; diff --git a/test_regress/t/t_uniqueif.v b/test_regress/t/t_uniqueif.v new file mode 100644 index 000000000..7700eb5cb --- /dev/null +++ b/test_regress/t/t_uniqueif.v @@ -0,0 +1,111 @@ +// DESCRIPTION: Verilator: Verilog Test module +// +// This file ONLY is placed into the Public Domain, for any use, +// without warranty, 2007 by Wilson Snyder. + +module t (/*AUTOARG*/ + // Inputs + clk + ); + + input clk; + + integer cyc=1; + integer a, b, c, d, e, f, g, h, i, j, k, l; + + always @ (posedge clk) begin + cyc <= cyc + 1; + + //==================== + // Positive test cases + //==================== + + // Single if, which is untrue sometimes + unique0 if (cyc > 5) + a <= 17; + + // single if with else + unique0 if (cyc < 3) + b <= 17; + else + b <= 19; + + // multi if, some cases may not be true + unique0 if (cyc < 3) + c <= 17; + else if (cyc > 3) + c <= 19; + + // multi if with else, else clause hit in some cases + unique0 if (cyc < 3) + d <= 17; + else if (cyc > 3) + d <= 19; + else + d <= 21; + + // single if with else + unique if (cyc < 3) + f <= 17; + else + f <= 19; + + // multi if + unique if (cyc < 3) + g <= 17; + else if (cyc >= 3) + g <= 19; + + // multi if with else, else clause hit in some cases + unique if (cyc < 3) + h <= 17; + else if (cyc > 3) + h <= 19; + else + h <= 21; + + //==================== + // Negative test cases + //==================== +`ifdef FAILING_ASSERTION1 + $display("testing fail 1: %d", cyc); + // multi if, multiple cases true + unique0 if (cyc < 3) + i <= 17; + else if (cyc < 5) + i <= 19; +`endif + +`ifdef FAILING_ASSERTION2 + // multi if, multiple cases true + unique if (cyc < 3) + j <= 17; + else if (cyc < 5) + j <= 19; +`endif + +`ifdef FAILING_ASSERTION3 + // multi if, no cases true + unique if (cyc > 1000) + k <= 17; + else if (cyc > 2000) + k <= 19; +`endif + +`ifdef FAILING_ASSERTION4 + // Single if, which is untrue sometimes. + // The LRM states: "A software tool shall also issue an error if it determines that no condition' + // is true, or it is possible that no condition is true, and the final if does not have a + // corresponding else." In this case, the final if is the only if, but I think the clause + // still applies. + unique if (cyc > 5) + l <= 17; +`endif + + + if (cyc==10) begin + $write("*-* All Finished *-*\n"); + $finish; + end + end +endmodule diff --git a/test_regress/t/t_uniqueif_fail1.pl b/test_regress/t/t_uniqueif_fail1.pl new file mode 100755 index 000000000..c63c5dfd3 --- /dev/null +++ b/test_regress/t/t_uniqueif_fail1.pl @@ -0,0 +1,28 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2009 by Wilson Snyder. This program is free software; you can +# redistribute it and/or modify it under the terms of either the GNU +# Lesser General Public License Version 3 or the Perl Artistic License +# Version 2.0. + +top_filename("t/t_uniqueif.v"); + +compile ( + v_flags2 => ['+define+FAILING_ASSERTION1'], + verilator_flags2 => ['--assert'], + nc_flags2 => ['+assert'], + fails => $Self->{nc}, + ); + +execute ( + fails => $Self->{vlt}, + expect=> +'.*%Error: t_uniqueif.v:\d+: Assertion failed in top.v: \'unique if\' statement violated +%Error: t/t_uniqueif.v:\d+: Verilog \$stop +.*', + ); + +ok(1); +1; diff --git a/test_regress/t/t_uniqueif_fail2.pl b/test_regress/t/t_uniqueif_fail2.pl new file mode 100755 index 000000000..6b1977571 --- /dev/null +++ b/test_regress/t/t_uniqueif_fail2.pl @@ -0,0 +1,28 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2009 by Wilson Snyder. This program is free software; you can +# redistribute it and/or modify it under the terms of either the GNU +# Lesser General Public License Version 3 or the Perl Artistic License +# Version 2.0. + +top_filename("t/t_uniqueif.v"); + +compile ( + v_flags2 => ['+define+FAILING_ASSERTION2'], + verilator_flags2 => ['--assert'], + nc_flags2 => ['+assert'], + fails => $Self->{nc}, + ); + +execute ( + fails => $Self->{vlt}, + expect=> +'.*%Error: t_uniqueif.v:\d+: Assertion failed in top.v: \'unique if\' statement violated +%Error: t/t_uniqueif.v:\d+: Verilog \$stop +.*', + ); + +ok(1); +1; diff --git a/test_regress/t/t_uniqueif_fail3.pl b/test_regress/t/t_uniqueif_fail3.pl new file mode 100755 index 000000000..3a069f18d --- /dev/null +++ b/test_regress/t/t_uniqueif_fail3.pl @@ -0,0 +1,28 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2009 by Wilson Snyder. This program is free software; you can +# redistribute it and/or modify it under the terms of either the GNU +# Lesser General Public License Version 3 or the Perl Artistic License +# Version 2.0. + +top_filename("t/t_uniqueif.v"); + +compile ( + v_flags2 => ['+define+FAILING_ASSERTION3'], + verilator_flags2 => ['--assert'], + nc_flags2 => ['+assert'], + fails => $Self->{nc}, + ); + +execute ( + fails => $Self->{vlt}, + expect=> +'.*%Error: t_uniqueif.v:\d+: Assertion failed in top.v: \'unique if\' statement violated +%Error: t/t_uniqueif.v:\d+: Verilog \$stop +.*', + ); + +ok(1); +1; diff --git a/test_regress/t/t_uniqueif_fail4.pl b/test_regress/t/t_uniqueif_fail4.pl new file mode 100755 index 000000000..2f16cd47f --- /dev/null +++ b/test_regress/t/t_uniqueif_fail4.pl @@ -0,0 +1,28 @@ +#!/usr/bin/perl +if (!$::Driver) { use FindBin; exec("$FindBin::Bin/bootstrap.pl", @ARGV, $0); die; } +# DESCRIPTION: Verilator: Verilog Test driver/expect definition +# +# Copyright 2003-2009 by Wilson Snyder. This program is free software; you can +# redistribute it and/or modify it under the terms of either the GNU +# Lesser General Public License Version 3 or the Perl Artistic License +# Version 2.0. + +top_filename("t/t_uniqueif.v"); + +compile ( + v_flags2 => ['+define+FAILING_ASSERTION4'], + verilator_flags2 => ['--assert'], + nc_flags2 => ['+assert'], + fails => $Self->{nc}, + ); + +execute ( + fails => $Self->{vlt}, + expect=> +'.*%Error: t_uniqueif.v:\d+: Assertion failed in top.v: \'unique if\' statement violated +%Error: t/t_uniqueif.v:\d+: Verilog \$stop +.*', + ); + +ok(1); +1;