From 15b9299f7f3d2e695e13a933387b85e0bee15eba Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 30 Aug 2024 16:43:24 -0700 Subject: [PATCH] aval/bval lowering for Verilog logical equality == and != return 'x' when either operand contains x or z. This lowers the operator to the aval/bval encoding. --- regression/verilog/expressions/equality1.desc | 15 ++++-- regression/verilog/expressions/equality1.v | 4 +- regression/verilog/expressions/equality2.desc | 15 +++++- regression/verilog/expressions/equality2.v | 4 +- src/hw_cbmc_irep_ids.h | 1 + src/verilog/aval_bval_encoding.cpp | 49 +++++++++++++++++++ src/verilog/aval_bval_encoding.h | 6 ++- src/verilog/expr2verilog.cpp | 8 +++ src/verilog/verilog_expr.h | 46 +++++++++++++++++ src/verilog/verilog_synthesis.cpp | 12 +++++ 10 files changed, 150 insertions(+), 10 deletions(-) diff --git a/regression/verilog/expressions/equality1.desc b/regression/verilog/expressions/equality1.desc index 8782aa9db..581c06efa 100644 --- a/regression/verilog/expressions/equality1.desc +++ b/regression/verilog/expressions/equality1.desc @@ -1,9 +1,18 @@ -KNOWNBUG +CORE broken-smt-backend equality1.v --bound 0 -^EXIT=0$ +^\[.*\] always 10 == 10 === 1: PROVED up to bound 0$ +^\[.*\] always 10 == 20 === 0: PROVED up to bound 0$ +^\[.*\] always 10 != 20 === 1: PROVED up to bound 0$ +^\[.*\] always 10 == 20 === 0: PROVED up to bound 0$ +^\[.*\] always 1'bx == 10 === 1'bx: PROVED up to bound 0$ +^\[.*\] always 1'bz == 20 === 1'bx: PROVED up to bound 0$ +^\[.*\] always 1'bx != 10 === 1'bx: PROVED up to bound 0$ +^\[.*\] always 1'bz != 20 === 1'bx: PROVED up to bound 0$ +^\[.*\] always 2'b11 == 2'b11 === 0: REFUTED$ +^\[.*\] always 2'sb-1 == 2'sb-1 === 1: PROVED up to bound 0$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -Missing Verilog case equality implementation. diff --git a/regression/verilog/expressions/equality1.v b/regression/verilog/expressions/equality1.v index f473a257e..11b24885a 100644 --- a/regression/verilog/expressions/equality1.v +++ b/regression/verilog/expressions/equality1.v @@ -8,7 +8,7 @@ module main; always assert property06: ('bz==20)==='bx; always assert property07: ('bx!=10)==='bx; always assert property08: ('bz!=20)==='bx; - always assert property09: ('sb1=='b11)===0; // zero extension - always assert property10: ('sb1=='sb11)===1; // sign extension + always assert property09: (1'sb1==2'b11)===0; // zero extension + always assert property10: (1'sb1==2'sb11)===1; // sign extension endmodule diff --git a/regression/verilog/expressions/equality2.desc b/regression/verilog/expressions/equality2.desc index 9861410f2..71c0c698b 100644 --- a/regression/verilog/expressions/equality2.desc +++ b/regression/verilog/expressions/equality2.desc @@ -1,9 +1,20 @@ CORE broken-smt-backend equality2.v --bound 0 -^EXIT=0$ +^\[.*\] always 10 === 10 == 1: PROVED up to bound 0$ +^\[.*\] always 10 === 20 == 0: PROVED up to bound 0$ +^\[.*\] always 10 !== 10 == 0: PROVED up to bound 0$ +^\[.*\] always 10 !== 20 == 1: PROVED up to bound 0$ +^\[.*\] always 1'bx === 1'bx == 1: PROVED up to bound 0$ +^\[.*\] always 1'bz === 1'bz == 1: PROVED up to bound 0$ +^\[.*\] always 1'bx === 1'bz == 0: PROVED up to bound 0$ +^\[.*\] always 1'bx === 1 == 0: PROVED up to bound 0$ +^\[.*\] always 1'bz === 1 == 0: PROVED up to bound 0$ +^\[.*\] always 1 === 1 == 1: PROVED up to bound 0$ +^\[.*\] always 3'b11 === 3'b111 == 1: REFUTED$ +^\[.*\] always 3'sb-1 === 3'sb-1 == 1: PROVED up to bound 0$ +^EXIT=10$ ^SIGNAL=0$ -- ^warning: ignoring -- -Missing Verilog case equality implementation. diff --git a/regression/verilog/expressions/equality2.v b/regression/verilog/expressions/equality2.v index c8b597e34..dfc31fabf 100644 --- a/regression/verilog/expressions/equality2.v +++ b/regression/verilog/expressions/equality2.v @@ -10,7 +10,7 @@ module main; always assert property08: ('bx==='b1)==0; always assert property09: ('bz==='b1)==0; always assert property10: ('b1==='b01)==1; // zero extension - always assert property11: ('b011==='sb11)==1; // zero extension - always assert property12: ('sb011==='sb11)==1; // sign extension + always assert property11: (3'b011===2'sb11)==1; // zero extension + always assert property12: (3'sb111===2'sb11)==1; // sign extension endmodule diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index a5a921598..7b81f6f8a 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/src/hw_cbmc_irep_ids.h @@ -211,6 +211,7 @@ IREP_ID_ONE(iff) IREP_ID_ONE(offset) IREP_ID_ONE(xnor) IREP_ID_ONE(specify) +IREP_ID_ONE(x) IREP_ID_ONE(verilog_empty_item) IREP_ID_ONE(verilog_import_item) IREP_ID_ONE(verilog_module) diff --git a/src/verilog/aval_bval_encoding.cpp b/src/verilog/aval_bval_encoding.cpp index 37b6e69aa..f51359843 100644 --- a/src/verilog/aval_bval_encoding.cpp +++ b/src/verilog/aval_bval_encoding.cpp @@ -14,6 +14,8 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +#include "verilog_types.h" + bv_typet aval_bval_type(std::size_t width, irep_idt source_type) { PRECONDITION(!source_type.empty()); @@ -34,12 +36,22 @@ bool is_aval_bval(const typet &type) return type.id() == ID_bv && !type.get(ID_C_verilog_aval_bval).empty(); } +bool is_aval_bval(const exprt &expr) +{ + return is_aval_bval(expr.type()); +} + std::size_t aval_bval_width(const typet &type) { PRECONDITION(is_aval_bval(type)); return to_bv_type(type).get_width() / 2; } +std::size_t aval_bval_width(const exprt &expr) +{ + return aval_bval_width(expr.type()); +} + typet aval_bval_underlying(const typet &src) { auto id = src.get(ID_C_verilog_aval_bval); @@ -198,3 +210,40 @@ exprt aval_bval_concatenation( return combine_aval_bval(concatenate(new_aval), concatenate(new_bval), type); } + +/// return true iff 'expr' contains either x or z +exprt has_xz(const exprt &expr) +{ + PRECONDITION(is_aval_bval(expr)); + auto width = aval_bval_width(expr); + return notequal_exprt{bval(expr), bv_typet{width}.all_zeros_expr()}; +} + +/// return 'x', one bit +exprt make_x() +{ + auto type = verilog_unsignedbv_typet{1}; + return lower_to_aval_bval(constant_exprt{ID_x, type}); +} + +exprt aval_bval(const verilog_logical_equality_exprt &expr) +{ + auto &type = expr.type(); + PRECONDITION(type.id() == ID_verilog_unsignedbv); + // returns 'x' if either operand contains x or z + auto has_xz = or_exprt{::has_xz(expr.lhs()), ::has_xz(expr.rhs())}; + auto equality = equal_exprt{expr.lhs(), expr.rhs()}; + return if_exprt{ + has_xz, make_x(), aval_bval_conversion(equality, lower_to_aval_bval(type))}; +} + +exprt aval_bval(const verilog_logical_inequality_exprt &expr) +{ + auto &type = expr.type(); + PRECONDITION(type.id() == ID_verilog_unsignedbv); + // returns 'x' if either operand contains x or z + auto has_xz = or_exprt{::has_xz(expr.lhs()), ::has_xz(expr.rhs())}; + auto equality = notequal_exprt{expr.lhs(), expr.rhs()}; + return if_exprt{ + has_xz, make_x(), aval_bval_conversion(equality, lower_to_aval_bval(type))}; +} diff --git a/src/verilog/aval_bval_encoding.h b/src/verilog/aval_bval_encoding.h index a6f900453..ff5c4894a 100644 --- a/src/verilog/aval_bval_encoding.h +++ b/src/verilog/aval_bval_encoding.h @@ -10,7 +10,8 @@ Author: Daniel Kroening, dkr@amazon.com #define CPROVER_VERILOG_AVAL_BVAL_H #include -#include + +#include "verilog_expr.h" // bit-concoding for four-valued types // @@ -36,4 +37,7 @@ exprt aval_bval_conversion(const exprt &, const typet &); exprt aval_bval_concatenation(const exprt::operandst &, const typet &); +exprt aval_bval(const verilog_logical_equality_exprt &); +exprt aval_bval(const verilog_logical_inequality_exprt &); + #endif diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index 6a8d103ba..ebd31cf73 100644 --- a/src/verilog/expr2verilog.cpp +++ b/src/verilog/expr2verilog.cpp @@ -1222,10 +1222,18 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence) return convert_binary( to_multi_ary_expr(src), "==", precedence = verilog_precedencet::EQUALITY); + else if(src.id() == ID_verilog_logical_equality) + return convert_binary( + to_multi_ary_expr(src), "==", precedence = verilog_precedencet::EQUALITY); + else if(src.id()==ID_notequal) return convert_binary( to_multi_ary_expr(src), "!=", precedence = verilog_precedencet::EQUALITY); + else if(src.id() == ID_verilog_logical_inequality) + return convert_binary( + to_multi_ary_expr(src), "!=", precedence = verilog_precedencet::EQUALITY); + else if(src.id()==ID_verilog_case_equality) return convert_binary( to_multi_ary_expr(src), diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index d7cdd25b7..8eb144852 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -62,6 +62,52 @@ to_hierarchical_identifier_expr(exprt &expr) return static_cast(expr); } +/// == +/// returns 'x' if either operand contains x or z +class verilog_logical_equality_exprt : public equal_exprt +{ +public: +}; + +inline const verilog_logical_equality_exprt & +to_verilog_logical_equality_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_verilog_logical_equality); + binary_exprt::check(expr); + return static_cast(expr); +} + +inline verilog_logical_equality_exprt & +to_verilog_logical_equality_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_verilog_logical_equality); + binary_exprt::check(expr); + return static_cast(expr); +} + +/// != +/// returns 'x' if either operand contains x or z +class verilog_logical_inequality_exprt : public equal_exprt +{ +public: +}; + +inline const verilog_logical_inequality_exprt & +to_verilog_logical_inequality_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_verilog_logical_inequality); + binary_exprt::check(expr); + return static_cast(expr); +} + +inline verilog_logical_inequality_exprt & +to_verilog_logical_inequality_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_verilog_logical_inequality); + binary_exprt::check(expr); + return static_cast(expr); +} + class function_call_exprt : public binary_exprt { public: diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index d98871f67..ae60389f6 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -390,6 +390,18 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state) .with_source_location(expr); } } + else if(expr.id() == ID_verilog_logical_equality) + { + for(auto &op : expr.operands()) + op = synth_expr(op, symbol_state); + return aval_bval(to_verilog_logical_equality_expr(expr)); + } + else if(expr.id() == ID_verilog_logical_inequality) + { + for(auto &op : expr.operands()) + op = synth_expr(op, symbol_state); + return aval_bval(to_verilog_logical_inequality_expr(expr)); + } else if(expr.has_operands()) { for(auto &op : expr.operands())