Formal verification, Assertion simplification

SystemVerilog
, , ,
1

Hello,
This example is extremely simple but I have to undertand the power of formal tool with this simple example.
Consider 2*1 MUX, to verify the design I can write assertions in two ways.

  1. assert property_1 ((@posedge clk)
    sel == 1 |-> out == a );
    assert property_2 ((@posedge clk)
    sel == 0 |-> out == b );

  2. assert property_1 ((@posedge clk)
    1 |-> out == a sel + b (!sel) );

Can anybody please explain how the first splitted assertion is equivalent to second assertion? How the tool drives input in second assertion?

2

In reply to Thanu:
In both of these assertions “out” has in its binary decision tree the inputs “sel a b”.
Thus, I would say that the tools drive those inputs in the identical manner, and those
two assertions are equivalent.

In this topic of formal verification I strongly recommend the book
Formal Verification: An Essential Toolkit for Modern VLSI Design by Erik Seligman, Tom Schubert, M V Achutha Kiran Kumar, ISBN: 9780128007273. That book covers essential aspects of formal verification, including theory; practical tips derived from actual usage of formal verification and from real designs; various approaches, or angles of attack, in using formal verification when verifying different types of designs and situations; and test case examples, and progression of solutions in achieving the end goals.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • 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
  • FREE this week at AMZN: Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
  • 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
  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
  4. FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy