文件列表:

sva_labs_public\Labs (0, 2008-03-10)
sva_labs_public\Labs\1_Lab (0, 2008-03-10)
sva_labs_public\Labs\1_Lab\Makefile (3496, 2005-07-23)
sva_labs_public\Labs\2_Lab (0, 2008-03-10)
sva_labs_public\Labs\2_Lab\aep_dir (0, 2008-03-10)
sva_labs_public\Labs\2_Lab\aep_dir\aep.cfg (12327, 2005-04-16)
sva_labs_public\Labs\2_Lab\aep_dir\aep.prj (579, 2005-05-31)
sva_labs_public\Labs\2_Lab\aep_dir\wb_dma_rf.v (63343, 2005-04-21)
sva_labs_public\Labs\2_Lab\dma_engine.sva (3758, 2006-01-14)
sva_labs_public\Labs\2_Lab\Makefile (3596, 2005-07-23)
sva_labs_public\Labs\2_Lab\solutions (0, 2008-03-10)
sva_labs_public\Labs\2_Lab\solutions\aep.cfg (12327, 2005-04-16)
sva_labs_public\Labs\2_Lab\solutions\aep.prj (570, 2005-04-16)
sva_labs_public\Labs\2_Lab\solutions\dma_engine.sva (2919, 2005-05-24)
sva_labs_public\Labs\3_Lab (0, 2008-03-10)
sva_labs_public\Labs\3_Lab\dma_engine.sva (2919, 2005-04-02)
sva_labs_public\Labs\3_Lab\Makefile (3602, 2006-01-14)
sva_labs_public\Labs\3_Lab\solutions (0, 2008-03-10)
sva_labs_public\Labs\3_Lab\solutions\#wb_int.sva# (5393, 2005-07-23)
sva_labs_public\Labs\3_Lab\solutions\dma_engine.sva (2919, 2005-04-05)
sva_labs_public\Labs\3_Lab\solutions\wb_int.sva (5394, 2005-07-23)
sva_labs_public\Labs\3_Lab\wb_int.sva (7321, 2006-01-14)
sva_labs_public\Labs\4_Lab (0, 2008-03-10)
sva_labs_public\Labs\4_Lab\dma_engine.sva (4271, 2005-04-07)
sva_labs_public\Labs\4_Lab\Makefile (3585, 2005-07-23)
sva_labs_public\Labs\4_Lab\solutions (0, 2008-03-10)
sva_labs_public\Labs\4_Lab\solutions\dma_engine.sva (3607, 2005-04-07)
sva_labs_public\Labs\4_Lab\solutions\wb_int.sva (5391, 2005-07-23)
sva_labs_public\Labs\4_Lab\wb_int.sva (5690, 2006-01-14)
sva_labs_public\Labs\5_Lab (0, 2008-03-10)
sva_labs_public\Labs\5_Lab\dma_engine.sva (8610, 2006-01-14)
sva_labs_public\Labs\5_Lab\Makefile (3609, 2005-07-23)
sva_labs_public\Labs\5_Lab\simv.vdb (0, 2008-03-10)
sva_labs_public\Labs\5_Lab\simv.vdb\.assertDeclInfo (5048, 2005-06-10)
sva_labs_public\Labs\5_Lab\simv.vdb\fcov (0, 2008-03-10)
sva_labs_public\Labs\5_Lab\simv.vdb\fcov\results.db (28797, 2005-06-10)
... ...

Lab Ojectives: This is a review lab, looking at concepts covered in the begginers assertion seminar. To bind a checker from the VCS checker library to the DMA engine. Also write simple assertions to check the control signals in the DMA engine. In the file dma_engine.sva: 1. Check 9-bit chunk size counter 'chunk_cnt' and 12-bit total size counter 'tsz_cnt' do not underflow. For this you can use the assert_no_underflow template in the checker library. The source for the assert_underflow checker is in the comments of dma_engine.sva for your reference. Look in the module bindings, This checker is bound to wb_dma (../../wb_dma/rtl/verilog/wb_dma_de.v). a. In module binding, bind assert_no_underflow to the module wb_dma to check underflow in chunk_cnt. Make sure that you set the enabling condition so that theassertion fires only when both rst is high and de_start is low. b: In module binding, bind assert_no_underflow to the module wb_dma to check underflow in tsz_cnt. Make sure that you set the enabling condition so that theassertion fires only when both rst is high, de_start is low and ptr_set is low. c: Run the testbench (make test) and examine the results. If you wish to look at the waveforms, excute make test_debug_postprocess. 2. Check control signals chunk_dec, tot_dec, adr0_inc, adr1_inc, read, write. chunk_dec, tot_dec, adr0_inc should be asserted when data has been read. adr1_inc should be asserted when data has been written. write should follow read. a. Uncomment the module assert_control_signals.Also uncomment the binding of this module in module bindings. This module contains several assertions to check control signals for the dma engine. All the assertions in this module are enabled when rstn is high (active low), They are sampled on the posedge of clk. This module is bound to wb_dma_de. b. Create an assert statement to check that chunk_dec is set correctly. Chunk_dec is asserted when the current state is READ (11'b000_0000_0010) and the state in the previous cycle is not READ. Hint: use the $past operator. Create a similar check for the tot_dec signal. Its be is identical to chunk_dec. c. Create an assert statement to check that adro_inc signal is set correctly. Signal adr0_inc is set to 1 if the state is READ (11'b000_0000_0010) and rd_ack signal is high. d. Create an assert statement to check that adr1_inc signal is set correctly. Signal adr1_inc is set to 1 if the state is READ (11'b000_0000_0010) and wr_ack signal is high. e. Create an assert statement to check that the posedge of the write signal (changes from 0 to 1), implies a negedge for the read signal (changes from 1 to 0). Hint: use $rose, $fell and implication. f. Run the testbench (make test) and examine the results. If you wish to look at the waveforms, excute make test_debug_postprocess. ========================================================== Running Magellan AEP session: In last part of this lab you'll be generating checkers for Automatically Extracted Properties using Magellan. A Magellan project file has already been created for this purpose. 1) To start type %> "mgui aep.prj & " 2) From the Run tab click on "Build/Run" button 3) View the results select the "Report" tab 4) View the failing property use "list_aep aep_all -falsified" command 4) To create the counter example select the "Run" tab and click on "TestBench" button 5) Extra credit load the VirSim aep.cfg file and start debug

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：