Reference for .eqy file format

A .eqy file consists of sections. Each section start with a single-line section header in square brackets.

Options section

The optional [options] section contains one config setting per line, in the form of key-value pairs.

splitnets on

Supported options are:






Split vector nets and ports into individual bits when reading the designs

Gold and gate sections

The mandatory [gold] and 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, and a synthesis output file synth.v, with the top-module mytest:

read -sv
prep -top mytest

read -sv synth.v
prep -top mytest

Run 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 help prep.

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

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]
00 001
01 010
10 100

Match sections

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.

[match axi_xbar_*]
gold-match *_ff[] \2_reg[\3].Q

TBD: gold-match, gate-match, final-gold-match, final-gate-match, gold-nomatch, gate-nomatch

Collect sections

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.

[collect axi_xbar_*]
bind partial_sum_*

solo and nosolo

The 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.

The nosolo <pattern> command prevents all further solo commands from matching the specified nets.

group and nogroup

The group <pattern> command is used to group everything matching the given pattern into the same fragment.

The 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.

The 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.)

The nobind <pattern> command prevents all further bind commands from matching the speciefied nets.

join and nojoin

The join command operates on a multi-bit wires and groups all bits from such a net into the same fragment.

The nojoin command prevents further join commands from matching the given nets.

solo-group and solo-join

The solo-group <pattern> command is a convenient shortcut for running both solo and group on the same pattern.

The solo-join <pattern> command is a convenient shortcut for running both solo and join on the same pattern.

Partition sections

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.

[partition axi_xbar_*]
name pipeline_\1 /^(reader|buffer|arbiter|writer)_([0-7])$/

name and noname

The 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 output.

If multiple name commands assign the same name to different entities, then the corresponding partitions will be merged into one partition with the given name. If multiple 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.)

The noname <pattern> command can be used to prevent further name commands from mathing the given nets.

merge and nomerge

The merge and nomerge commands work similar to group and nogroup, but creates non-fragment partitions by merging the fragment partitions generated by the grouping commands.

path statements

The 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

The 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.

The nosticky <pattern> command preents further sticky commands from matching the given net.

amend, ramend, and noamend

The 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.

The amend <pattern> <pattern> command only amends partitions that are generating signals matching the second pattern.

The 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.

The noamend <pattern> command preents further amend and ramend commands from matching the given net.

final statements

The 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.

Strategy sections

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.

[strategy simple]
apply axi_xbar_*
use sat
depth 10

use statements

The 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, the depth command in the example above is a custom command only understood by the sat strategy type. See the EQY Strategies reference page for details on the individual strategy types.

apply and noapply

The 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 further 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.

Pattern Syntax

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 path, final, and apply statements.

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 char (?, *, or [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 [] token.

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.