Evaluation, Conclusion, Future Work¶

The Yosys source tree contains over 200 test cases 1 which are used in the make test make-target. Besides these there is an external Yosys benchmark and test case package that contains a few larger designs . This package contains the designs listed in Tab. 1.1.

Tests included in the yosys-tests package.¶
Test-Design	Source	Gates	Description / Comments
`aes_core`	IWLS2005	: math:41{,}837	AES Cipher written by Rudolf Usselmann
`i2c`	IWLS2005	1{,}072	WISHBONE compliant I2C Master by Richard Herveille
`openmsp430`	OpenCores	7{,}173	MSP430 compatible CPU by Olivier Girard
`or1200`	OpenCores	: math:42{,}675	The OpenRISC 1200 CPU by Damjan Lampret
`sasc`	IWLS2005	456	Simple Async. Serial Comm. Device by Rudolf Usselmann
`simple_spi`	IWLS2005	690	MC68HC11E based SPI interface by Richard Herveille
`spi`	IWLS2005	2{,}478	SPI IP core by Simon Srot
`ss_pcm`	IWLS2005	279	PCM IO Slave by Rudolf Usselmann
`systemcaes`	IWLS2005	6{,}893	AES core (using SystemC to Verilog) by Javier Castillo
`usb_phy`	IWLS2005	515	USB 1.1 PHY by Rudolf Usselmann

Correctness of Synthesis Results¶

The following measures were taken to increase the confidence in the correctness of the Yosys synthesis results:

Yosys comes with a large selection 2 of small test cases that are evaluated when the command make test is executed. During development of Yosys it was shown that this collection of test cases is sufficient to catch most bugs. The following more sophisticated test procedures only caught a few additional bugs. Whenever this happened, an appropriate test case was added to the collection of small test cases for make test to ensure better testability of the feature in question in the future.
The designs listed in Tab. 1.1 where validated using the formal verification tool Synopsys Formality. The Yosys synthesis scripts used to synthesize the individual designs for this test are slightly different per design in order to broaden the coverage of Yosys features. The large majority of all errors encountered using these tests are false-negatives, mostly related to FSM encoding or signal naming in large array logic (such as in memory blocks). Therefore the fsm_recode pass was extended so it can be used to generate TCL commands for Synopsys Formality that describe the relationship between old and new state encodings. Also the method used to generate signal and cell names in the Verilog backend was slightly modified in order to improve the automatic matching of net names in Synopsys Formality. With these changes in place all designs in Tab. 1.1 validate successfully using Formality.
VlogHammer is a set of scripts that auto-generate a large collection of test cases 3 and synthesize them using Yosys and the following freely available proprietary synthesis tools.
- Xilinx Vivado WebPack (2013.2)
- Xilinx ISE (XST) WebPack (14.5)
- Altera Quartus II Web Edition (13.0)
The built-in SAT solver of Yosys is used to formally verify the Yosys RTL- and Gate-Level netlists against the netlists generated by this other tools. 4 When differences are found, the input pattern that result in different outputs are used for simulating the original Verilog code as well as the synthesis results using the following Verilog simulators.
- Xilinx ISIM (from Xilinx ISE 14.5 )
- Modelsim 10.1d (from Quartus II 13.0 )
- Icarus Verilog (no specific version)
The set of tests performed by VlogHammer systematically verify the correct behaviour of
- Yosys Verilog Frontend and RTL generation
- Yosys Gate-Level Technology Mapping
- Yosys SAT Models for RTL- and Gate-Level cells
- Yosys Constant Evaluator Models for RTL- and Gate-Level cells
against the reference provided by the other tools. A few bugs related to sign extensions and bit-width extensions where found (and have been fixed meanwhile) using this approach. This test also revealed a small number of bugs in the other tools (i.e. Vivado, XST, Quartus, ISIM and Icarus Verilog; no bugs where found in Modelsim using vlogHammer so far).

Although complex software can never be expected to be fully bug-free , it has been shown that Yosys is mature and feature-complete enough to handle most real-world cases correctly.

Quality of synthesis results¶

In this section an attempt to evaluate the quality of Yosys synthesis results is made. To this end the synthesis results of a commercial FPGA synthesis tool when presented with the original HDL code vs. when presented with the Yosys synthesis result are compared.

The OpenMSP430 and the OpenRISC 1200 test cases were synthesized using the following Yosys synthesis script:

hierarchy -check
proc; opt; fsm; opt; memory; opt
techmap; opt; abc; opt

The original RTL and the Yosys output where both passed to the Xilinx XST 14.5 FPGA synthesis tool. The following setting where used for XST:

-p artix7
-use_dsp48 NO
-iobuf NO
-ram_extract NO
-rom_extract NO
-fsm_extract YES
-fsm_encoding Auto

The results of this comparison is summarized in Tab. 1.2. The used FPGA resources (registers and LUTs) and performance (maximum frequency as reported by XST) are given per module (indentation indicates module hierarchy, the numbers are including all contained modules).

For most modules the results are very similar between XST and Yosys. XST is used in both cases for the final mapping of logic to LUTs. So this comparison only compares the high-level synthesis functions (such as FSM extraction and encoding) of Yosys and XST.

OpenRISC 1200

Without Yosys

With Yosys

Module

Regs

LUTs

Max. Freq.

Regs

LUTs

Max. Freq.

open MSP430

689

2210

71 MHz

719

2779

53 MHz

` 1em oms p_clock_ module`

21

30

645 MHz

21

30

644 MHz

`` 1em 1em omsp_syn c_cell``

2

—

1542 MHz

2

—

1542 MHz

1 em 1em o msp_sync _reset

2

—

1542 MHz

2

—

1542 MHz

1em om sp_dbg

143

344

292 MHz

149

430

353 MHz

` `1em 1em

omsp_db

g_uart``

76

135

377 MHz

79

139

389 MHz

1 em omsp_ executio n_unit

266

911

80 MHz

266

1034

137 MHz

1e m 1em om sp_alu

—

202

—

—

263

—

1em 1em omsp _registe r_file

231

478

285 MHz

231

506

293 MHz

``1em
omsp_fr

ontend``

115

340

178 MHz

118

527

206 MHz

` 1em oms p_mem_ba ckbone`

38

141

1087 MHz

38

144

1087 MHz

1em o msp_mult iplier

73

397

129 MHz

102

1053

55 MHz

1em om sp_sfr

6

18

1023 MHz

6

20

1023 MHz

``1em
omsp_wa

tchdog``

24

53

362 MHz

24

70

360 MHz

or12 00_top

7148

9969

135 MHz

7173

10238

108 MHz

`` 1em or12 00_alu``

—

681

—

—

641

—

1 em or120 0_cfgr

—

11

—

—

11

—

1 em or120 0_ctrl

175

186

464 MHz

174

279

377 MHz

``1em
or1200_

except``

241

451

313 MHz

241

353

301 MHz

``1em
or1200_

freeze``

6

18

507 MHz

6

16

515 MHz

` 1em or1 200_if`

68

143

806 MHz

68

139

790 MHz

`` 1em or12 00_lsu``

8

138

—

12

205

1306 MHz

`` 1em 1em or1200_m em2reg``

—

60

—

—

66

—

`` 1em 1em or1200_r eg2mem``

—

29

—

—

29

—

1em o r1200_mu lt_mac

394

2209

240 MHz

394

2230

241 MHz

1em 1e m or1200 _amultp2 _32x32

256

1783

240 MHz

256

1770

241 MHz

1 em or120 0_operan dmuxes

65

129

1145 MHz

65

129

1145 MHz

` 1em or1 200_rf`

1041

1722

822 MHz

1042

1722

581 MHz

1 em or120 0_sprs

18

432

724 MHz

18

469

722 MHz

1e m or1200 _wbmux

33

93

—

33

78

—

``1em
or1200_

dc_top``

—

5

—

—

5

—

1em o r1200_dm mu_top

2445

1004

—

2445

1043

—

1 em 1em o r1200_dm mu_tlb

2444

975

—

2444

1013

—

` 1em or1 200_du`

67

56

859 MHz

67

56

859 MHz

``1em
or1200_

ic_top``

39

100

527 MHz

41

136

514 MHz

` `1em 1em

or1200_

ic_fsm``

40

42

408 MHz

40

75

484 MHz

`` 1em or12 00_pic``

38

50

1169 MHz

38

50

1177 MHz

` 1em or1 200_tt`

64

112

370 MHz

64

186

437 MHz

Conclusion and Future Work¶

Yosys is capable of correctly synthesizing real-world Verilog designs. The generated netlists are of a decent quality. However, in cases where dedicated hardware resources should be used for certain functions it is of course necessary to implement proper technology mapping for these functions in Yosys. This can be as easy as calling the techmap pass with an architecture-specific mapping file in the synthesis script. As no such thing has been done in the above tests, it is only natural that the resulting designs cannot benefit from these dedicated hardware resources.

Therefore future work includes the implementation of architecture-specific technology mappings besides additional frontends (VHDL), backends (EDIF), and above all else, application specific passes. After all, this was the main motivation for the development of Yosys in the first place.

1: Most of this test cases are copied from HANA or the ASIC-WORLD website .
2: At the time of this writing 269 test cases.
3: At the time of this writing over 6600 test cases.
4: A SAT solver is a program that can solve the boolean satisfiability problem. The built-in SAT solver in Yosys can be used for formal equivalence checking, amongst other things. See Sec. [cmd:sat] for details.