Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

BDD fails with: "no support for $past when using AIG backends" #686

Open
ShashankVM opened this issue Sep 10, 2024 · 0 comments
Open

BDD fails with: "no support for $past when using AIG backends" #686

ShashankVM opened this issue Sep 10, 2024 · 0 comments

Comments

@ShashankVM
Copy link

Project link: https://github.com/ShashankVM/hamming_encoder_decoder_bmc

Run command:
ebmc -D FORMAL --bdd --top dut dut.sv cc_encoder.sv piso.sv lfsr_encoder.sv cc_decoder_ht.sv lfsr_decoder.sv buffer_reg.sv error_correction_and_detection.sv channel.sv --reset reset==1

Output:

Parsing dut.sv
Parsing cc_encoder.sv
Parsing piso.sv
Parsing lfsr_encoder.sv
Parsing cc_decoder_ht.sv
Parsing lfsr_decoder.sv
Parsing buffer_reg.sv
Parsing error_correction_and_detection.sv
Parsing channel.sv
Converting
Type-checking Verilog::buffer_reg
Type-checking Verilog::error_correction_and_detection
file error_correction_and_detection.sv line 7: Making error_correction_and_detection.error_pos a wire
Making error_correction_and_detection.error_det a wire
Making error_correction_and_detection.code_out a wire
Type-checking Verilog::lfsr_decoder
Type-checking Verilog::cc_decoder_ht
file cc_decoder_ht.sv line 17: Making cc_decoder_ht.next a wire
file cc_decoder_ht.sv line 11: Making cc_decoder_ht.clear_2 a wire
file cc_decoder_ht.sv line 11: Making cc_decoder_ht.clear_1 a wire
file cc_decoder_ht.sv line 11: Making cc_decoder_ht.valid_code_in a wire
file cc_decoder_ht.sv line 10: Making cc_decoder_ht.code_in_2 a wire
file cc_decoder_ht.sv line 10: Making cc_decoder_ht.code_in_1 a wire
Making cc_decoder_ht.code_out a wire
Making cc_decoder_ht.error_det a wire
Making cc_decoder_ht.valid_out a wire
file cc_decoder_ht.sv line 11: Making cc_decoder_ht.error_det_signal a wire
file cc_decoder_ht.sv line 13: Making cc_decoder_ht.buffer_out a wire
file cc_decoder_ht.sv line 15: Making cc_decoder_ht.syndrome_val a wire
file cc_decoder_ht.sv line 15: Making cc_decoder_ht.syndrome_val_1 a wire
file cc_decoder_ht.sv line 15: Making cc_decoder_ht.syndrome_val_2 a wire
Type-checking Verilog::lfsr_encoder
Type-checking Verilog::piso
Making piso.piso_out a wire
Type-checking Verilog::cc_encoder
Making piso(4).piso_out a wire
Making cc_encoder.valid a wire
file cc_encoder.sv line 13: Making cc_encoder.next a wire
Making cc_encoder.ready a wire
Making cc_encoder.code_out a wire
file cc_encoder.sv line 9: Making cc_encoder.lfsr_reg a wire
file cc_encoder.sv line 10: Making cc_encoder.piso_load a wire
file cc_encoder.sv line 10: Making cc_encoder.piso_out a wire
file cc_encoder.sv line 11: Making cc_encoder.piso_in a wire
Type-checking Verilog::channel
Making channel.channel_out a wire
Making channel.valid_out a wire
Type-checking Verilog::dut
Making dut.rx a wire
Making dut.tx a wire
Making dut.error_det a wire
Making dut.tx_valid a wire
Making dut.encoder_ready a wire
Making dut.rx_valid a wire
file dut.sv line 17: Making dut.channel_out a wire
file dut.sv line 15: Making dut.code_out_encoded a wire
file dut.sv line 16: Making dut.channel_valid_out a wire
file dut.sv line 29: Making dut.tx_final a wire
Building netlist
file dut.sv line 58: error: no support for $past when using AIG backends
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant