Hongce Zhang

Support SVA assert/assume

1

This pull request partially address the issue (https://github.com/PyHDI/Pyverilog/issues/87) as it adds support for `assert property (...)`, `always @(...) begin assert (...); end`, `assume property (...)`, `always @(...) begin assume (...);...

Update Refinement Handling in Verilog Verification Target Generation

10

~~Work in progress, do not merge at this point!~~ This pull request is to see if the test coverage is sufficient.

**Describe your feature request.** - Separate refinement relation parsing & error checking from property generation. - Add expression parsing functionality so that in the future we can easily extend it...

- Add interface to specify parameterized data types - SMT support for operators on parameterized data types: using UF? - Add simulator generation support for parameterized data types

Current ILA verification target generation only supports Verilog. The automation part needs analysis of Verilog to create a well-formed wrapper. Some suggestions to the possible System Verilog parser we can...

I’m not sure if I understand it correctly. Please correct me if I’m wrong. Are there any registers in FADD? I understand that there is a near path and a...

Parsing multiple files

2

In `scan_end` function, the lexer state was popped. However in `scan_begin`, it was not pushed. Initially, I was thinking this should be okay. But it turned out that if I...

Previously, we wrote all our constraints in Alloy, however, due to speed issue, I want to shift to ocelot. I found that the preliminary Alloy-style support in lib/alloy.rkt very useful....

SMT target and SystemVerilog target?

1

In the Makefile, I see there is the `riscv.smt_model` target, I was hoping it can generate models in SMT-LIB2 format (is that what it means to be?), but it seems...

GTKWave does not support signal names with a colon `:`

4

Some EDA tools will generate VCD files where signal names contain a colon `:` Is it possible to support signal names with colons? Thanks!