[sv-ac] more on 1900 checkers

Dmitry,

1. Doesn’t the following significantly change the requirements of a simulator relative to the processing of assume statements, and guarantee differences across simulators?  


checker observer_model(bit valid, reset);
   	default clocking @$global_clock;
freevar bit flag;
m1: assume property (reset |=> !flag);
m2: assume property (!reset && flag |=> flag);
m3: assume property (!$rising_gclk(flag) |-> valid);
endchecker : observer_model

In this example the free variable flag behaves as follows:
 If it is high it remains high as long as there is no reset.
 If there is a reset it becomes low.
 It may become high only when valid is high.

Note that although the behavior of the free variable flag has been restricted by the assumptions m1, m2,
and m3, it is still non-deterministic because it does not have to become high when valid is high. Figure
16.17 (Note to editor: please insert a correct figure number) shows two possible legal behaviors of this
variable given the same behaviors of reset and valid.  Note to editor: please number consistently with rest of chapter.

In simulation, a tool implementation-dependent decision may be made to use one of the following simulation methods to implement the non-deterministic choice:
 Symbolic simulation, where all possibilities are represented.
 Random values chosen at simulation time.
 Default values for their type used at simulation time.

2. I think that this proposal needs to be split into smaller chunks. 30 pages is a lot for one proposal, and it may come down to all or nothing. The free variables is a major chunk that could be separated.  There is also discussion on global clock and scheduling that does not need to be here. 

3. This is kind of a silly question. Do you need to explicitely state that comments are allowed in checkers?  It is not in the list of things allowed, but I’m not  sure if others do either.  Of course we want to allow comments. 

Lisa

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