hi all,
is there a way to link an assumption to specific assertions (or to disable an assumption for specific assertions)?
thanks
In reply to gidon:
hi all,
is there a way to link an assumption to specific assertions (or to disable an assumption for specific assertions)?
thanks
Is this what you are looking for?
The $assertcontrol provides finer granularity in how and which types of assertions are controlled. The syntax is repeated below:
$assertcontrol ( control_type [ , [ assertion_type ] [ , [ directive_type ]
[ , [ levels ] [ , list_of_scopes_or_assertions ] ] ] ] ) ;
// Assertion controls
let ON = 3; // assertion control type
let OFF= 4; // assertion control type
// Assertion types
let CONCURRENT = 1; // assertion_type, concurrent
let S_IMMEDIATE = 2; // assertion_type, simple immediate
..
let ALL_ASSERTS = (CONCURRENT|S_IMMEDIATE|D_IMMEDIATE|EXPECT); // (i.e., 31)
// Assertion directives
let ASSERT = 1; // directive_type for assertion control tasks
let COVER = 2; // directive_type for assertion control tasks
let ASSUME = 4; // directive_type for assertion control tasks
let ALL_DIRECTIVES = (ASSERT|COVER|ASSUME); // (i.e., 7)
— levels: This argument specifies the levels of hierarchy.
It defaults to 0 (i.e., the specified module and in all module instances below the specified module).
// Example
module akill; // /ch4/4.2/akill.sv
bit clk, a,b;
default clocking @(posedge clk); endclocking
ap_kill: assert property (a |=> b) $assertkill(0, akill.ap_test_kill);
ap_kill0: assert property(a |=> b) $assertcontrol(5, 15, 7, 0, akill.ap_kill0);
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
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- 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
- 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
See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
In reply to ben@SystemVerilog.us:
thank you Ben,
So just to clarify,in your example, while the tool is running “ap_kill” , “ap_test_kill” is disabled?
In reply to gidon:
from my SVA Handbook 4th Edition
Killed: An assertion can be aborted and stopped with the system function $assertkill (see 4.2.4.1). A killed assertion does not contribute to the statistics.
Control kill: This aborts execution of any currently executing attempts for the
specified assertions and then stop the checking of all specified assertions until a subsequent $assertcontrol with a control_type of 3 (On). This also flushes any queued pending reports of deferred assertions or pending procedural assertion instances that have not yet matured. This control_type value does not affect expect statements. For example,
$assertcontrol(KILL, CONCURRENT, ASSERT, 0);
Kill currently executing concurrent assertions, but do not kill concurrent covers, assumes and immediate/deferred asserts/covers/assumes. Using the appropriate directive type values for thread second arguments.
The following file from my book should help you in understanding the controls and in the coding style. Keep in mind that not all vendors may support all of that; thus, please don’t blame the messenger if it does not work :)
module test;
logic clk, a, b, c, d;
event start_sim;
int count1=0, count2=0;
// now define lets to make the code more readable
let LOCK = 1;
let UNLOCK = 2;
let ON = 3;
let OFF = 4;
let KILL = 5;
let CONCURRENT = 1;
let S_IMMEDIATE = 2; // simple immediate
let D_IMMEDIATE = 12; // Final and Observed deferred immediate
let EXPECT = 16;
let ASSERT = 1;
let COVER = 2;
let ASSUME = 4;
let ALL_DIRECTIVES = (ASSERT|COVER|ASSUME);
let ALL_ASSERTS = (CONCURRENT|S_IMMEDIATE|D_IMMEDIATE|EXPECT);
let VACUOUSOFF = 11;
a1: assert property (@(posedge clk) a |=> b) $info("assert passed");
else $error("assert failed");
c1: cover property (@(posedge clk) a ##1 b);
always @(posedge clk) begin
ia1: assert (a);
end
always_comb begin
if (c)
df1: assert #0 (d);
end
function automatic void pass();
$display("ap1 pass");
endfunction : pass
function automatic void fail();
$display("ap1 fail");
endfunction : fail
ap1: assert property(@ (posedge clk)
a |-> b) pass(); else fail();
initial begin
// the following systasks affect the whole design so no modules
// are specified
// disable vacuous pass action for all the concurrent asserts,
// covers and assumes in the design. Also disable vacuous pass
// action for expect statements.
$assertcontrol(VACUOUSOFF, CONCURRENT | EXPECT);
// disable concurrent and immediate asserts and covers.
// The following systask does not affect expect
// statements as control type is Off.
$assertcontrol(OFF); // using default values of all the
// arguments after first argument
// After 20 time units, enable assertions.
// explicitly specifying second, third and fourth arguments
// in the following task call
#20 $assertcontrol(ON, CONCURRENT|S_IMMEDIATE|D_IMMEDIATE,
ASSERT|COVER|ASSUME, 0);
// kill currently executing concurrent assertions after
// 100 time units but do not kill concurrent covers/assumes
// and immediate/deferred asserts/covers/assumes
// using appropriate values of second and third arguments
#100 $assertcontrol(KILL, CONCURRENT, ASSERT, 0);
// the following assertion control task does not have any effect as
// directive_type is assert but it has selected cover directive c1
#10 $assertcontrol(ON, CONCURRENT|S_IMMEDIATE|D_IMMEDIATE, ASSERT, 0, c1);
// now, after 10 time units, enable all the assertions except a1.
// To accomplish this, first we�ll lock a1 and then we�ll enable all
// the assertions and then unlock a1 as we want future assertion
// control tasks to affect a1.
#10 $assertcontrol(LOCK, ALL_ASSERTS, ALL_DIRECTIVES, 0, a1);
$assertcontrol(ON); // enable all the assertions except a1
$assertcontrol(UNLOCK, ALL_ASSERTS, ALL_DIRECTIVES, 0, a1);
if(!obj.randomize())
`uvm_error("run_phase", "seq randomization failure");
end
ap_x1: assert property(Px1) count1 <= count1 + 1'b1; // pass action block increments variable
ap_x2: assert property(Px1) count2 <= count2 + 1'b1; // pass action block increments variable
initial begin
$assertcontrol(KILL);
wait (start_sim);
$assertcontrol(ON);
// Optional if pass action does not update
$assertcontrol(LOCK, ALL_ASSERTS, ALL_DIRECTIVES, 0, ap_x1, ap_x2);
$assertcontrol(PASSOFF);
$assertcontrol(UNLOCK, ALL_ASSERTS, ALL_DIRECTIVES, 0, ap_x1, ap_x2);
if (!req.randomize()) `uvm_error("MYERR", "This is a randomize error");
end
endmodule
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
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- 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
- 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
See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions | Verification Academy