[sv-ac] arguments passing

All,

here is a milestone in our effort to define arguments passing
to declared sequences and declared properties. Attached:

1. 1549_new_types_9.pdf - this is the section 17 (and Annex A),
   part of the proposal. It describes the new types, and the rules, which
   govern actual arguments to formal arguments assignments.

2. formal_semantics_arguments_passing.pdf. This is the Annex E part,
   which defines the semantics of instances of declared sequences and
   declared properties. The semantics is defined using a rewrite
   algorithm that translates an assertion with instances of sequences
   and properties(possibly with arguments,) into one flat assertion.

3. examples.txt - some examples for the rewrite algorithm.


Notes:

1. The current definition does not allow assigning of local variables
   to typed arguments. We wait for 1667, 1668 to be resolved first.

2. Currently, actual arguments of integral type must have an
   equivalent type to the formal arguments they are assigned
   to. Equivalent types are defined at 6.9.2. In general two types are
   equivalent if the have the same number of bits and either both are
   2 states types or 4 states types.  
   
   We are still debating this restriction. An alternative is to say
   that any actual argument that who's type can be casted into the formal
   argument's type, is legal (implicit casting). We think that this
   should be dicussed in the committee.





-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.



Example 1
======================================================
property p1(logic [2:0] a1, property a2);

    (a1 == 3'b010) |=> a2;

endproperty

property p2(a1, logic [1:3] a2);

    a1 ##1 (a2 == 3'b010);
endproperty

assert property (p1(g1, p2(g2, g3)));

---------------------------------
result of flatten_property(p1) - 
---------------------------------
property p1'(logic [2:0] a1, property a2);

    ((logic [2:0]'$var(g1)) == 3'b010) |=> $var(p2(g2, g3));

endproperty


property p2(a1, logic [1:3] a2);

    a1 ##1 (a2 == 3'b010);
endproperty

assert property  (($var((logic [2:0])'g1) == 3'b010) |=> $var(p2(g2, g3)));

---------------------------------
result of flatten_property(p2) - 
---------------------------------
property p2'(a1, logic [1:3] a2);

    $var(g2) ##1 ($var((logic [1:3])'g3) == 3'b010);
endproperty

assert property  (($var((logic [2:0])'g1) == 3'b010) |=> $var( $var(g2) ##1 ($var((logic [1:3])'g3) == 3'b010)));
==================================================




Example 2
==================================================
property p1(logic [2:0] a1, logic [0:2] a2);

a1[0] == a2[1] &&
a1[1] == a2[2] &&
a1[2] == a2[0];

endproperty

assert property (g2 |=> p1(g1[4:6], g1[8:10]));

---------------------------------
result of flatten_property(p1) - 
---------------------------------

property p1(logic [2:0] a1, logic [0:2] a2);

$var((logic [2:0])'(g1[4:6]))[0] == $var((logic [0:2])'(g1[8:10]))[1] &&
$var((logic [2:0])'(g1[4:6]))[1] == $var((logic [0:2])'(g1[8:10]))[2] &&
$var((logic [2:0])'(g1[4:6]))[2] == $var((logic [0:2])'(g1[8:10]))[0];

endproperty

assert property (g2 |=> 
$var((logic [2:0])'(g1[4:6]))[0] == $var((logic [0:2])'(g1[8:10]))[1] &&
$var((logic [2:0])'(g1[4:6]))[1] == $var((logic [0:2])'(g1[8:10]))[2] &&
$var((logic [2:0])'(g1[4:6]))[2] == $var((logic [0:2])'(g1[8:10]))[0];
);
==================================================



Example 3
==================================================
property p1(logic a1, logic [2:0] a2);

logic [2:0] l1;

(a1, l1 = a2) |=> !a1[->1] ##0 (l1 == a2);

endproperty


property p2;

logic [2:0] l1;

(g1, l1 = g2) |=> ((g3 == l1) or p1(g1,g2|g3));

endproperty


assert property (p2);

---------------------------------
result of flatten_property(p2) - 
---------------------------------
property p1(logic a1, logic [2:0] a2);

logic [2:0] l1;

(a1, l1 = a2) |=> !a1[->1] ##0 (l1 == a2);

endproperty


property p2';

logic [2:0] l1;

(g1, l1 = g2) |=> ((g3 == l1) or p1(g1,g2|g3));

endproperty


assert property(

logic [2:0] l1;

(g1, l1 = g2) |=> ((g3 == l1) or p1(g1,g2|g3));
);

---------------------------------
result of flatten_property(p1) - 
---------------------------------
 
property p1'(logic a1, logic [2:0] a2);

logic [2:0] l1_2;

($var((logic)'(g1)), l1_2 = $var(logic [2:0])'(g2|g3)) |=> !$var((logic)'(g1))[->1] ##0 (l1_2 == $var((logic [2:0])'(g2|g3));

endproperty



assert property(

logic [2:0] l1;
logic [2:0] l1_2;

(g1, l1 = g2) |=> ((g3 == l1) or ($var((logic)'(g1)), l1_2 = $var(logic [2:0])'(g2|g3)) |=> !$var((logic)'(g1))[->1] ##0 (l1_2 == $var((logic [2:0])'(g2|g3))))
);
==================================================



Example 4
==================================================
sequence s1(a1, logic [2:0] a2);

logic [2:0] l1;

(1, l1 = a2) ##1 ((a2 != l1), a1 = a1 + 1)[*0:$] ##1 (a2 == l1);
endsequence


assert property (

logic [3:0] l1, l2;

(g1, l1 = g2, l2 = g3) |-> s1(l2, g4) ##0 (l1 == l2)
);

---------------------------------
result of flatten_property(s1) - 
---------------------------------

sequence s1'(a1, logic [2:0] a2);

logic [2:0] l1_1;

(1, l1_1 = $var((logic[2:0])'(g4))) ##1 (($var((logic[2:0])'(g4)) != l1_1), (l2) = $var((l2)) + 1)[*0:$] ##1 ($var((logic[2:0])'(g4)) == l1_1);
endsequence


assert property (

logic [3:0] l1, l2;

(g1, l1 = g2, l2 = g3) |-> 
(1, l1_1 = $var((logic[2:0])'(g4))) ##1 (($var((logic[2:0])'(g4)) != l1_1), l2 = $var((l2)) + 1)[*0:$] ##1 ($var((logic[2:0])'(g4)) == l1_1) 
##0 (l1 == l2)
);