From 8fe63c3d05fc3826e01222776430bea9bc5fef62 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 10 Sep 2024 08:04:12 -0700 Subject: [PATCH] Verilog: fix for output of -> This repairs the output of the Verilog (not: SVA) implication operator, to read ->, and not |->. --- regression/verilog/expressions/bit-extract6.desc | 4 ++-- regression/verilog/synthesis/always_comb2.desc | 6 +++--- src/verilog/expr2verilog.cpp | 4 ++-- src/verilog/expr2verilog_class.h | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/regression/verilog/expressions/bit-extract6.desc b/regression/verilog/expressions/bit-extract6.desc index b9848747f..7461c5d2c 100644 --- a/regression/verilog/expressions/bit-extract6.desc +++ b/regression/verilog/expressions/bit-extract6.desc @@ -1,8 +1,8 @@ CORE bit-extract6.sv --module main --bound 0 -^\[main\.p0\] always \(main\.index == 8 |-> main\.vector\[7 - main\.index - 1\] == 1\): PROVED up to bound 0$ -^\[main\.p1\] always \(main\.index >= 1 \&\& main\.index <= 7 |-> main\.vector\[7 - main\.index - 1\] == 0\): PROVED up to bound 0$ +^\[main\.p0\] always main\.index == 8 -> main\.vector\[7 - main\.index - 1\] == 1: PROVED up to bound 0$ +^\[main\.p1\] always main\.index >= 1 \&\& main\.index <= 7 -> main\.vector\[7 - main\.index - 1\] == 0: PROVED up to bound 0$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/verilog/synthesis/always_comb2.desc b/regression/verilog/synthesis/always_comb2.desc index 7b420ba11..cf435a6af 100644 --- a/regression/verilog/synthesis/always_comb2.desc +++ b/regression/verilog/synthesis/always_comb2.desc @@ -1,9 +1,9 @@ CORE always_comb2.sv --bound 0 -^\[main\.property\.p0\] always \(main\.data == 0 |-> main\.decoded == 1\): PROVED up to bound 0$ -^\[main\.property\.p1\] always \(main\.data == 1 |-> main\.decoded == 2\): PROVED up to bound 0$ -^\[main\.property\.p2\] always \(main\.data == 2 |-> main\.decoded == 4\): PROVED up to bound 0$ +^\[main\.p0\] always main\.data == 0 -> main\.decoded == 1: PROVED up to bound 0$ +^\[main\.p1\] always main\.data == 1 -> main\.decoded == 2: PROVED up to bound 0$ +^\[main\.p2\] always main\.data == 2 -> main\.decoded == 4: PROVED up to bound 0$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 9dbbdab76..d1b92568c 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1324,11 +1324,11 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence) else if(src.id()==ID_implies) return convert_binary( - to_multi_ary_expr(src), "|->", precedence = verilog_precedencet::MIN); + to_multi_ary_expr(src), "->", precedence = verilog_precedencet::IMPLIES); else if(src.id()==ID_iff) return convert_binary( - to_multi_ary_expr(src), "<->", precedence = verilog_precedencet::MIN); + to_multi_ary_expr(src), "<->", precedence = verilog_precedencet::IMPLIES); else if(src.id()==ID_reduction_or) return convert_unary( diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 6228eb5c1..fc53d4946 100644 --- a/src/verilog/expr2verilog_class.h +++ b/src/verilog/expr2verilog_class.h @@ -38,7 +38,7 @@ enum class verilog_precedencet AND = 7, // && OR = 6, // || IF = 5, // ?: - IMPLIES = 4, // -> + IMPLIES = 4, // -> <-> ASSIGN = 3, // = += -= etc. CONCAT = 18, // { } concatenation, {{ }} replication MIN = 0 // anything even weaker, e.g., SVA