Subject: RE: Desirable features for the standard FV property language
From: Sandeep K. Shukla (skshukla@ics.uci.edu)
Date: Thu Jan 31 2002 - 18:04:07 PST
>2. i am not sure what you mean by "allow to specify complex reset
>sequences as part of constraints." can you explain this a little more, and
>perhaps provide an example?
>
>It is intended to get the UDT to a specific state (initial state) before
>proving a property.
>For example, i would like the signal "rst" to start as low for 1 cycles
and
> go high for 3 cycles and stay low forever with respect to the clock ck.
____ ____ ____ ____ ____ ____
ck |___| |___| |___| |___| |___| |___|
> pattern 0000111110 and repeat
__________________________
rst _________| |_________________________
>rst {low} [1 cycle on ck] {high} [ 3 cycles on ck] {low} [forever]
>we hope we can easily specify this reset sequence as
>a constraint using a specification language or a similar kind.
have a boolean variable is_init
and 3 extra variables, p_is_init, pp_is_init, ppp_is_init
as follows:
init(is_init) := 1;
next(is_init) := 0 /* is_init is 1 only in the first cycle and 0 every
where */
init(p_is_init) := 0;
next(p_is_init) := is_init;
init(pp_is_init) := 0;
next(pp_is_init) := p_is_init;
init(ppp_is_init) := 0;
next(ppp_is_init) := pp_is_init;
property 1: G(is_init -> rst = 0);
property2: G((p_isinit | pp_isinit | ppp_isinit) -> rst = 1)
property2: G((~p_isinit & ~pp_isinit $ ~ppp_isinit) -> rst = 0)
then assume property1, property2, property3
to prove your other properties.
In case, the language has a auxiliary automaton construct, you can construct
the automaton as well.
This archive was generated by hypermail 2b28 : Thu Jan 31 2002 - 18:09:07 PST