HTTPS SSH

Template-based Synthesis of Instruction-Level Abstractions for SoC Verification

Dear Reader,

In this repository, we have provided the experimental artefacts and source code for our FMCAD 2015 submission titled, "Template-based Synthesis of Instruction-Level Abstractions for SoC Verification."

Overview

All code and binaries in this repository were created using Ubuntu Linux 12.04. Other versions of Linux may work, but we have not tested them.

Note you will need to have the Z3 SMT solver installed on your machine.

To clone this repository, use the following command:

$ hg clone https://bitbucket.org/spramod/fmcad-15-soc-ila

This assumes that you have the Mercurial distributed version control tool installed. If you don't, you can also download the repository as an archive by clicking the download button.

Organization

This repository is organized as follows.

  1. The subdirectory 'bin' contains binaries for our slightly-modified versions of ABC and Yosys. ABC is the verification tool we used and we used Yosys to synthesize netlists from behavioral Verilog.

  2. The subdirectory 'src' contains the source code for the instruction-level simulation i8051sim and the all the RTL source code for the 8051 and the AES and SHA accelerators.

  3. The subdirectory 'synthesis' contains the synthesis library developed in our paper and the generated instruction-level abstractions (ILAs).

  4. The subdirectory 'netlists' contains all the netlists we used for property verification.

Organization of the RTL Source

This is in the directory src/rtl.

Most of the files with the files 'oc8051' prefix are from the OpenCores.org implementation of the 8051. The files we have created have the prefix 'oc8051_gm_'. The file oc8051_gm_top.v is the top-level module that contains the properties that determine equality between the monolithic golden module and the RTL implementation. The files inside the ind_models subdirectory contain the compositional version of the properties, of which there are one for each opcode. The files oc8051_gm_ram_top.v, oc8051_gm_indi_addr etc. contain the abstracted versions of the 8051 RTL: these were modifications we had to implement to reduce the size of the 8051 IRAM from 256 bytes to 16 bytes.

The files with the prefix 'aes' and 'sha' are the accelerator modules. The files that we implemented are 'aes_top.v', 'sha_top.v' and oc8051_xiommu.v. These are the interface modules that "connect" the 8051 to the accelerators and XRAM.

The file oc8051_xiommu_gm_top.v defines the properties stating the equivalence between the AES+SHA+XRAM modules with the corresponding golden models.

Organization of the Synthesis Source

The synthesis library is defined in the files synthesizer.py, ast.py and ast2verilog.py.

8051 Synthesis

The files uc8051syn.py, uc8051sim.py, sim51.py and uc8051ast.py together implement the synthesis of the 8051 ILA. One example for running the synthesis algorithm is shown below:

$ python uc8051syn.py --output PC_33.ast 0x33 PC

When this command is run, it synthesizes the transition relation for the PC (program counter) for opcode 0x33 and stores this as an abstract syntax tree in the file PC_33.ast.

To read the AST, use the readast.py script.

$ python readast.py PC_33.ast
opcode: 33
PC
(add PC (bv 1 16))

The output tells us that for the instruction 0x33, the PC is just incremented by 1.

Synthesis Output

All the synthesis output for the 8051 is stored in the synthesis/ila/8051/ subdirectory.

8051 Golden Model

The monolithic 8051 golden model can be generated using the following command:

$ python uc8051gm.py ila/8051/ ila/8051/opcnst8051.ast oc8051_golden_model.v

The per-instruction golden model can be generated using the following command:

$ python uc8051gmop.py ila/8051/ ila/8051/opcnst8051.ast 0x44 oc8051_golden_model_44.v

The above command generates the golden model for opcode 44 and stores it in the file oc8051_golden_model_44.v. You can repeat this for each opcode you are interested in.

Luckily, we have already generated all the golden models and stored them in the directory synthesis/golden-models.

AES+SHA+XRAM Synthesis

The scripts for this are all prefixed with xm8051. An example of running the synthesis is shown below:

$ python xm8051syn.py --output state0_aes_addr.ast 0x0 aes_addr

This synthesizes the 'aes_addr' transition relation output when the AES and SHA states are both zero. We can examine the transition relations using the readast.py script.

$ ./readast.py state0_aes_addr.ast 
opcode: 00
aes_addr
(if (and (eq (bv 65282 16) (concat (extract 15 1 addrin) (bv 0 1))) (and (eq (extract 3 2 op) (bv 2 2)) (eq aes_state (bv 0 8)))) (if (eq (extract 0 0 addrin) (bv 0 1)) (concat (extract 15 8 aes_addr) datain) (concat datain (extract 7 0 aes_addr))) aes_addr)

Synthesis Output

The synthesis output for the AES+SHA+XRAM model is stored in the subdirectory synthesis/ila/xrma-aes-sha.

AES+SHA+XRAM Golden Model

This can be generated using the following command:

$ python xm8051gm.py ila/xram-aes-sha/ oc8051_xiommu_gm.v

oc8051_xiommu_gm.v is the generated output file.

Netlists for Verification

The directory netlists/ contains the synthesized netlists for all the properties in our evaluation.

Verilog Subdirectory

The files in the Verilog directory are:

  • oc8051_gm_{opcode}_{property}.v: These are netlists for each compositional property.
  • oc8051_gm_top_yosys_all.v: This is the netlist with the monolithic golden model of the 8051 and all associated properties.
  • oc8051_xiommu_gm.v: This is the netlist with the monolithic golden for the AES+SHA+XRAM ILA.

The following three files contains the AES-specific properties for which we obtained proofs using PDR.

  • oc8051_xiommu_gm_aes_addr.v
  • oc8051_xiommu_gm_aes_len.v
  • oc8051_xiommu_gm_aes_state.v

AIG Subdirectory

This contains AIGs for the compositional properties after gate-level abstraction was performed on them.

Verification Scripts

The scripts run-bmc.py and run-gla-pdr.py contain useful ABC "recipes" which perform some simplification/gata-level abstraction and then simplification before running BMC or PDR on a verilog netlist.

Conclusion

We acknowledge this is not an exhaustive tutorial of all the code used in our experiments, but hopefully there is enough information here to get an idea of the synthesis methodology in the paper.

Contact

We are of course very happy to answer questions.

Pramod Subramanyan: psubrama@princeton.edu Yakir Vizel: yvizel@princeton.edu Sayak Ray: sayakr@princeton.edu Sharad Malik: sharad@princeton.edu