[sv-ac] Formal semantics of extended booleans

Hi all,

 

Currently semantics of extended booleans is defined in a standalone mode
only. Thus, $stable is defined as

 

w^j |= @(c) $stable(e) iff there exists 0 < i < j so that w^{i,j}, {},
{} (c ##1 c [->1]) and e[w^i] = e[w^j].

 

But strictly speaking according to this definition expressions like
$stable(e) && a have no meaning. One way to fix this is to define them
like:

 

$stable(e, c)[w^j]  is 1 iff there exists 0 < i < j so that w^{i,j}, {},
{} (c ##1 c [->1]) and e[w^i] = e[w^j], otherwise, $stable(e, c)[w^j]
is 0.

 

Another possibility is to make all sampled value functions but $past
derived from $past:

 

$stable(e) == $past(e) = e

$changed(e) == $past(e) != e

$rose(e) == $past(LSB(e)) !=== 1 && LSB(e) === 1

$fell(e) == $past(LSB(e)) !=== 0 && LSB(e) === 0

 

Note, however, that there is a small discrepancy between two definitions
for functions $rose and $fell: e.g., if at the moment before the first
clock tick LSB(e) = 1, then according to the original definition
$rose(e) is false, while according to the second definition it is false.

 

The situation becomes worse if we assume that the initial value for past
is taken as a default value of the type, e.g., past(bit) is initially 0,
and not x.

 

What definition should we adopt?

 

Thanks,

Dmitry

 


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