From fbf5d89587decd2886d501d8c6e1cde076a5476f Mon Sep 17 00:00:00 2001
From: George Rennie <georgerennie@gmail.com>
Date: Thu, 23 Dec 2021 01:10:32 +0000
Subject: equiv_make: Add -make_assert option

This adds a -make_assert flag to equiv_make. When used, the pass generates
$eqx and $assert cells to encode equivalence instead of $equiv.
---
 tests/various/equiv_make_make_assert.ys | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 tests/various/equiv_make_make_assert.ys

(limited to 'tests')

diff --git a/tests/various/equiv_make_make_assert.ys b/tests/various/equiv_make_make_assert.ys
new file mode 100644
index 000000000..1c2efa723
--- /dev/null
+++ b/tests/various/equiv_make_make_assert.ys
@@ -0,0 +1,32 @@
+read_verilog <<EOT
+module gold(
+	input wire [7:0] a,
+	input wire [7:0] b,
+	output wire [7:0] c
+);
+
+wire [7:0] b_neg;
+assign b_neg = -b;
+assign c = a + b_neg;
+endmodule
+
+module gate(
+	input wire [7:0] a,
+	input wire [7:0] b,
+	output wire [7:0] c
+);
+
+wire [7:0] b_neg;
+assign b_neg = ~b + 1;
+assign c = a + b_neg;
+endmodule
+
+EOT
+
+equiv_make -make_assert gold gate miter
+
+select -assert-count 0 t:$equiv
+select -assert-count 2 t:$assert
+
+prep -top miter
+sat -prove-asserts -verify
-- 
cgit v1.2.3