Reference for .eqy file format¶
.eqy file consists of sections. Each section start with a single-line
section header in square brackets.
[options] section contains one config setting per line, in the
form of key-value pairs.
Supported options are:
Split vector nets and ports into individual bits when reading the designs
Gold and gate sections¶
gate sections contains the Yosys script that
reads and elaborates the “gold” and “gate” versions of the design under test.
For example, for a simple project contained in a single design file
mytest.sv, and a synthesis output file
synth.v, with the
read -sv mytest.sv
prep -top mytest
read -sv synth.v
prep -top mytest
yosys in a terminal window and enter
help on the Yosys prompt
for a command list. Run
help <command> for a detailed description of the
command, for example
The contents of
[script] sections are added to the gold and gate scripts.
This simplifies the configuration file in cases where both scripts share
larger sequences of commands.
Recode sections contain encodings for FSM state registers, for the cases when the sythesis tool changes those encodings. (Alternatively the state registers can be excluded as match points and strategies for sequential equivalence checking can be employed for proving equivalence of the FSM as a whole.)
These sections start with a header that contains two arguments: A module name from the (gold) design and the name of a wire within that module. (Those arguments are actually both regular expressions, but are rarely used to match more than one entity.)
The section itself listst binary representation of values in the gold design and their corresponding gate encodings. Values not listed should never be produced by the gold design.
[recode mytest state]
Match sections contain rules for matching net names in the gold design to net names in the gate design. The match section header contains an optional pattern matching module names. The lines within the match section are only applied to modules matching that pattern, or all modules if the pattern is omitted.
gold-match *_ff \2_reg[\3].Q
TBD: gold-match, gate-match, final-gold-match, final-gate-match, gold-nomatch, gate-nomatch
Collect sections contain rules for the first step of the partition algorithm, in which individual bits from matched nets are grouped into /fragments/, i.e. small circuits that are closely related and thus should be put in the same partition.
solo and nosolo¶
solo <pattern> command prevents the auto-grouping mechanism to
group this net with other nets into the same fragment. Per default
auto-grouping does group nets when
they are driven by the same cell, either in the gold or gate design, or
gold nets are aliases, i.e. are implemented by the same gate net.
nosolo <pattern> command prevents all further
from matching the specified nets.
group and nogroup¶
group <pattern> command is used to group everything matching the given
pattern into the same fragment.
group <pattern> <pattern> command is pairing matches for the first pattern with the sets
of nets matching the (dependent) second pattern, and is grouping them accordingly.
nogroup <pattern> command prevents all further
group commands from
matching the specified nets.
bind and nobind¶
Marking a net as
bind prevents that net from becoming a primary input of
a fragment. (This has no effect on nets that are module inputs.)
nobind <pattern> command prevents all further
bind commands from
matching the speciefied nets.
join and nojoin¶
join command operates on a multi-bit wires and groups all bits
from such a net into the same fragment.
nojoin command prevents further
join commands from matching
the given nets.
solo-group and solo-join¶
solo-group <pattern> command is a convenient shortcut for running
group on the same pattern.
solo-join <pattern> command is a convenient shortcut for running
join on the same pattern.
Partition sections contain rules for creating matching partitions in the gold and gate designs. The partition section header contains an optional pattern matching module names. The lines within the partition section are only applied to modules matching that pattern, or all modules if the pattern is omitted.
name pipeline_\1 /^(reader|buffer|arbiter|writer)_([0-7])$/
name and noname¶
name <string> <pattern> command is looking for nets matching the given pattern,
and then applies the given name to the partition that contains that net as primary
name commands assign the same name to different entities, then the
corresponding partitions will be merged into one partition with the given name. If
name commands apply to the same partition, then the earlier name command
will be used to name the partition. (Both names are used for merging partitions tho.)
noname <pattern> command can be used to prevent further name commands from
mathing the given nets.
merge and nomerge¶
nomerge commands work similar to
but creates non-fragment partitions by merging the fragment partitions generated
by the grouping commands.
path <pattern> <pattern> command will determine the shortest path from the
first net to the second net, and then merge all partitions along that path.
If the first pattern matches a net name then the partition generating that net is not included in the path itself. If the first pattern matches a partition name then that partition is included in the path.
If the second pattern matches a net name then partitions consuming that signal are not included in the path itself. If the second pattern matches a partition name then that partition is included in the path.
sticky and nosticky¶
sticky <pattern> command marks nets as sticky. The partition generating the
sticky net as primary output will then be merged with any partition using the
sticky net as primary input.
nosticky <pattern> command preents further
sticky commands from matching
the given net.
amend, ramend, and noamend¶
amend <pattern> command finds the fragment(s) generating the
specified net(s), and amends all partitions using those signals with the gold
definition of that signal.
amend <pattern> <pattern> command only amends partitions that are
generating signals matching the second pattern.
amend command only amends partitions that are currently consuming
the specified signal. The
ramend command amends the target partition
unconditionally. This is useful when the signals being amended are themself
only used by other partitions that are being amended to the target partition.
noamend <pattern> command preents further
commands from matching the given net.
final <pattern> command marks the partitions generating the
nets matching the pattern as final. No furter statements will have any
effect on a partition after it is marked as final.
Each strategy section creates a verification strategy used to prove partitions to be equal. The section header contains the name of the strategy as an argument.
use strategy_type command selects a strategy type for this strategy. Each
strategy type defines its own custom commands for the strategy section. For example,
depth command in the example above is a custom command only understood by
sat strategy type. See the EQY Strategies reference page for details on the individual strategy types.
apply and noapply¶
apply <pattern> [<pattern>] command is used to enable the given strategy
in modules matching the first pattern, for partitions matching
the second pattern. The
noapply <pattern> [<pattern>] command prevents
apply commands in the same strategy section from matching the
specified partitions. If the second pattern is omitted, then the strategy will
be applied to all partitions in the modules matching the first pattern.
Patterns are comma-seperated lists of any combinations of the following types of expressions.
names of modules or nets, or shell wildcard pattern matching those names,
regular expressions matching enity names, enclosed in forward slashes,
at-sign (@) followed by an attribute name, matching all entities with that attribute set,
at-sign and attribute name, followed by an equal sign (=) and an attribute value,
or ampercent-sign (&) followed by a partition name.
A regular expression can be enclosed in
//i instead of
//, in which
case it is evaluated case-insensitive.
Attribute names and partition names can also be shell wildcard patterns, or regular expressions.
The partition name syntax is only available in
In commands that accept pairs of patterns, numeric backreferences (0, 1, 2) and named backreferences (g<1>, g<name>) are replaced in the second pattern by the contents of the corresponding group from the first pattern.
In shell wildcard patterns, the entire name is stored in 0 and each wildcard
[abcd] groups) stores the matching text in a numbered
group. The special string
 in shell wildcard patterns match to an integer
in square brackets, storing the text preceding the square brackets in 1 and the
integer in the group corresponding to the
If the first pattern in a pair used the at-sign syntax for attributes, then g<name> in the second pattern is replaced with the attribute name and g<value> with the corresponding attribute value.