[Formal] SVA: how to localize assumptions for a particular SVA

SystemVerilog
, , ,
1

Want to apply some assumptions only to a particular SVA, is there a SystemVerilog way of doing this ?
by default all assumptions seems to be global for all assertions.

There are tool specific way of doing this, but I want to know if SVA addresses this ?
Can I use checker construct for this ?

2

In reply to ssureshgverifier@gmail.com:
In SVA you can use the assertion controls

$assertcontrol ( control_type [ , [ assertion_type ] [ , [ directive_type ]
[ , [ levels ] [ , list_of_scopes_or_assertions ] ] ] ] ) ;
let ON = 3; // assertion control type
let OFF = 4; // assertion control type
let CONCURRENT = 1; // assertion_type, concurrent
let ASSUME = 4; // directive_type for assertion control tasks
/* levels: This argument specifies the levels of hierarchy, consistent with the corresponding
argument to the $dumpvars system task (see 1800-2012 section 21.7.1.2). If this argument is not specified, it defaults to 0 (i.e., the specified module and in all module instances below the specified module). 
Example: $dumpvars (1, top); // Because the first argument is a 1,
// this invocation dumps all variables within the module top;
// it does not dump variables in any of the modules instantiated by module top. */
//
event start_sim; // /ch4/4.2/assertion_control.sv
int count1=0, count2=0;
ap_x1: assert property(Px1) count1 <= count1 + 1'b1;
ap_x2: assert property(Px1) count2 <= count2 + 1'b1;
initial begin
$assertcontrol(KILL); // Stop checking all assertions
wait (start_sim); // wait for subsystem to be ready to start checking for assertions
$assertcontrol(ON); // enable all assertions
// disable all pass action blocks except those needed
$assertcontrol(LOCK, ALL_ASSERTS, ALL_DIRECTIVES, 0, ap_x1); // lock any changes to ap_x1
$assertcontrol(PASSOFF); // pass off for ap_x2
$assertcontrol(UNLOCK, ALL_ASSERTS, ALL_DIRECTIVES, 0, ap_x1, ap_x2);

I explain all of this in my SVA book.
This link provides those pages on that topic
http://systemverilog.us/vf/assertion_cntrl.pdf

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
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
3

In reply to ben@SystemVerilog.us:

Thnx Ben, but the question is more on formal verification

4

In reply to ssureshgverifier@gmail.com:

Got this answer from a colleague who has extensively used formal verification:
"if I want to state that property P1 is true when we assume property P2, I think the most straightforward method would be
assert property (P2 implies P1)

Or am I missing some subtlety in the question?"

Ben systemverilog.us

5

In reply to ben@SystemVerilog.us:

I think this will be useful, let me try.
Thanks a lot.