In reply to puranik.sunil@tcs.com:
Your equivalent equations are too complex, and hard to follow.
Formal verification tools do support the intersect.
One of the best way to check for equivalency is to use constrained-random tests on your test model. I use the following constrained-random tests to verify assertions.
You can vary your constraints to test various combinations. If your original and equivalent assertions behave exactly the same, in all respects, they they are equivalent. However, the 2 assertions may express different notions of the requirements, but are not identical.
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
bit clk, a, b;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(a, din) with
{ a dist {1'b1:=1, 1'b0:=3};
b dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error")
end
$finish;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
// For 10% discount, use code 45KJT5GN @ https://www.createspace.com/5810350 - A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115