Hardware Reference
In-Depth Information
C4 . posedge b/ D $rising_gclk( b ) .
C5 . negedge b/ D $falling_gclk( b ) .
C6 . edge b/ D . posedge b/ || . negedge b/.
C7 .e iff b/ D .e/ && b.
C8 .e 1 or e 2 / D .e 1 / || .e 2 /.
C9 .e 1 , e 2 / D .e 1 / || .e 2 /.
For example,
. posedge clk iff enable / D $rising_gclk(clk) && enable
After transforming clocking events into Boolean expressions, the formal seman-
tics eliminates the clocking event controls by folding the associated Boolean
expressions into the underlying sequences and properties. The resulting unclocked
sequences and properties are then interpreted over traces (i.e., finite and infinite
words). The elimination of the clocking event controls is accomplished by a system
of clock rewrite rules . The rewrite rules define a function
s that transforms a
sequence and the Boolean expression for a clock into an unclocked sequence. They
also define a function
T
p for transforming properties similarly. The clock rewrite
rules are as follows, where c denotes a clocking event:
T
s . ( r ) ;c/ D ( T
s .r; c/ ) .
SCR0
T
s .b; c/ D ! c [ * ] ##1 c && b.
SCR1
T
s . (1, v = h ) ;c/ D T
s . 1 ;c/ ##0 (1, v = h ) .
SCR2
T
s . @( c 2 ) r; c 1 / D T
s .r; c 2 /. 4
SCR3
T
s .r 2 ;c/, where op can be any of the
operators ##0 , ##1 , or , and intersect .
s .r 1
s .r 1 ;c/ op
SCR4
T
op r 2 ;c/ D T
T
s . first_match ( r ) ;c/ D first_match ( T
s .r; c/ ) .
SCR5
T
s .r [ * n ] ;c/ D T
s .r; c/ [ * n ] . The same rule applies to ranged repetition
SCR6
T
operators.
p . ( p ) ;c/ D ( T
p .p; c/ ) .
PCR0
T
p . op ( r ) ;c/ D op ( T
s .r; c/ ) , where op is either strong or weak .
PCR1
T
p . @( c 2 ) p; c 1 / D T
p .p; c 2 /. 5
PCR2
T
p .p; c/, where op is any of not , disable iff ( b ) ,
accept_on ( b ) , and reject_on ( b ) .
p . op p; c/ D op
PCR3
T
T
p .p 1 op p 2 ;c/ D T
p .p 1 ;c/ op
p .p 2 ;c/, where op can be any of the
PCR4
T
T
operators and , or , implies , and iff .
p .p; c/.An
analogous rule applies to rewrite the synchronous reject in terms of the
asynchronous reject.
p . sync_accept_on ( b ) p; c/ D accept_on ( b && c ) T
PCR5
T
4 This rule can be applied only after applying the clock flow rules in Sect. 12.2.4.1 .
5 See footnote 4 .
Search WWH ::




Custom Search