#	Requirement	Explanation	Properties	Essential / Nice-to-have/Drop
	Expressiveness
	expressions and modeling
1	Support rich data types and expressions  (using syntax which is independent of VHDL or Verilog syntax)	have at least the expressive power of expression in VHDL and Verilog	72
2	Adopt Verilog data-types and expression
3	Adopt VHDL data-types and expression
4	Adopt "xx" language data-types and expression	where xx is SystemC  or Superlog or Verilog2000
5
6
7	Rich data types. e.g., enumerate, array, structures/classes, >32 bit in width		72
8	Rich vector expressions, e.g., arithmetic, logical, vectors		8,9
9	Expressions may  include reference to 'prior' times, i.e., refer to PAST	supported in OpenVera - has value in simplifying sequences	10-a, 9, 45,47
10	Use of 'zero-time' "computational" functions in expressions	Functions that typically have datapath values as parameters and return one result that can be used in an expression. These functions would be required not to alter model variables or signals, nor include ant delay statements, nor could they call any sub-functions that break these rules	51
11	Portions of the language may not be currently compiled into all known validation technologies
12	The entire language needs to be compiled into FV and DV	According to the current know limitation of Formal tools and simulation-based tools
	sequences (temporal)
13	Repeated sequences	most buses have read/write burst modes - like the ability of * in regular expressions	2,14,57,58
14	Finite sequences with time windows with anchoring success to end of sequence		2-b,3,4,5,7,10,14,58,59
16	Indentify only first occurence of event		1,3,4,10,16-a,53
17	Indentify all occurences of the event		18
18	Overlap of sequences	critical in pipelined address bus systems (Note : in 'e' this means two events can be satisfied in the same  clock cycle)	10-b,7
19	'or' combinations of sequences	PCI bus transactions can have about 6 different outcomes	17-b,20,45.1,45.5
20	'and' combinations of sequences		13
21	Sequential composition of finite sequences followed by formulae		48,68,18,1,16,20,57
22	Rich  Safety properties		Most of the properties
23	Minimal Livenss properties	eventaully p	59
24	Rich  Liveness properties	possibly:   stronge fairness	GFp -> GFp, 73
25	Allow arbitrary composition of formulae/temporal operator for simplicity and elegance
26	Language must be easy to learn by designer		1:18
27	Close assertions under negation	for efficient model-checking - allow to negate a formula instead of complementing an automaton
28	Enable finite time reasoning (static and dynamic)	partial path computations (identify failure in simulation as soon as possible)
29	Explicit and short-hand notation for Finite State Machines (fsm)	need to be support assume-guarantee	Roy
30	Include for-all path quantifier		1
31	Datapath properties specify the transformation of data over a period of many cycles.	1) Specifying that a 8 bit parrallel input will outputed in order bit by bit.	20,21,22
32	Include existential path quantifier		AG EF (state=idle) AG(fram-fall -> E[irdy U !trdy]. 63,64
	clocks
33	Allow Asynchronous modeling/properties		65
34	level sensitive clocks and rich set of edge-sensitive clocks, e.g. after/before-rise, after/before-fall, after/before-change	some example exist (older ARM & M68000) (note : edge instead of posedge/negedge is not adequate)	65,2,15
35	weak and strong clocks	weak clocks may not tick, strong clocks must tick	66,15,68
36	Support multiple clocks		65,15,2
37	Support abstract clocks	even the occurrence of a sequence of events may define the occurrence of the tick	9,15
38	Support discrete event and synchronous models	has semantics that can handle event based simulator	24
	reset
39	Inhibit of some or all rules during reset and/or re-sync	Can cause false assertion failures during simulation	Roy
40	Suspend properties (via reset)		50
41	Check other property when reset		Hillel
42	Reject or Accept on reset	you usually want "accept" the property when reset occurs, however when you have reset nested within negation you also need reject	46,55,62
	Other
43	Only property language	expression + temporals   or  even just temporal
44	property & modeling		Roy
	Meta language requirements
45	Named sub-rules	important for accuracy and clarity and for building complex properties using other properties as building blocks	45 definition, 20
46	templates with parameters	to allow user defined constructs	1,3, 12,14,18
47	Ability to build library of properties	parameteroized lib.	1,3
48	recursive definition of templates
49	blocks/instantiation/ name's scoping	a variable for each instance and sometimes global variables	55 , 20, 11, 49
50	for different instantiation of RTL blocks you may get different instantiations of the corresponding properties		11,51,66,67,13
51	for-loops, parameterized signal names	succinct creation of similar formulas	66, 67
52	shorthand for specifying signals are constant	most buses require signals to be stable throughout a sequence	45.4
53	shorthand for 'rose' and 'fell' (or posedge/negedge if you prefer)		2-a,45
54	Allow composition (non monolithic properties)		45,65,20
	Validation requirements
55	Well defined semantics and intuitive semantics
56	Well defined semantics for simulation
57	Allow Calls to procedural code during simulation	for support of datapath checks in simulation - see exec in 'e'
58	Vendor support in Formal Model checker	Commercial availability is essential for adoption of any language : simulation support is far easier and cheaper to develop than a Formal Model checker
59	Vendor support in simulation
60	Enable infinite domain static reasoning	example of IEEE spec for arithmetic	Limor
61	Not specifically tied to a particular class of reasoning
62	ability of "Efficient" model checking algorithms
63	Full support of the assume/guarantee paradigm		Roy
64	Reasonable complexity of compilation
65	efficient negation/complementation of properties	when
66	Compositionality	Semantics of the formula is defined from the semantics of its sub-formulas
67
68	Support hierarchical verification	for properties pertaining to interfaces - ability to interchange constraints and properties
69	known model checking algorithms
	Other
70	Enable the definition of properties, constraints (assumptions) and events (sequence)
71	Support for checkers, assumptions with proof obligation, assumptions for case splitting (no proof obligation), modeling with fomulae
72	Introduce a minimal number of concepts
73	Small and simple to use		13
74	Easy to use: learn, write, read		1:18
75	succinct		1:18