Sugar semantics for VHDL/Verilog designs

Subject: Sugar semantics for VHDL/Verilog designs
From: Anthony McIsaac (anthony.mcisaac@st.com)
Date: Wed Jun 19 2002 - 01:36:02 PDT

Following my comments at the last phone conference, here are some thoughts about
how the semantics of Sugar formulae, as they apply to HDL designs, could be
tightened up.

First, I'd like to make it clear that it's absolutely right for the semantics to be
defined in terms of paths and models (transition systems). Sugar will be applied
to all sorts of representations other than HDL.

So the question is: given a synthesizable HDL design, what is the corresponding model?
I take it that we can assume a well-defined path from the HDL to a representation
in terms of combinational functions and flip-flops (... and also latches and tristates).
Given a flip-flop m, clocked on the rising edge of c, whose output is a function
f(v1,v2,...vn) of the design signals, what is the corresponding contribution to
the transition relation?

There appear to be at least two possible choices:
((c = 0) & (next(c) = 1)) -> (next(m) = f(v1,v2,...,vn))
or
(prev(c) = 0) & (c = 1)) -> (next(m) = f(v1,v2,...,vn))

I think the second may be the only viable one, but it should be made clear to users and
implementers exactly what the interpretation is.

The interpretation for latches and tristates will also have to be defined.

Mention of tristates leads me to another question:
The definition of the modelling layer allows signal identifiers as boolean identifiers
(i.e. we can write always(sig) instead of always(sig = '1')).
How are these identifiers interpreted if the signal takes the values X or Z?
Also, how is (sig = 'X') interpreted if the value of sig is, for example, 1?

I've got another point about the modelling layer.
There is a built-in function "next", so the following is legal in EDL:
assign next(s) :=
  case
    next(s) : 0;
    else : 1;
  esac;

Should this be disallowed in the language, or do we allow it and let the error
show up later?
I would prefer to discourage the use of next in the LHS of assign cases,
even when they do in fact work.

Anthony 

--
Anthony McIsaac

STMicroelectronics Limited
1000 Aztec West
Almondsbury
Bristol BS32 4SQ

Tel: ++44 (0)1454 462466
Fax: ++44 (0)1454 617910

Email: Anthony.McIsaac@st.com

This archive was generated by hypermail 2b28 : Wed Jun 19 2002 - 01:40:16 PDT